Discrete probability semantics of failure

The operational failure law and discrete support/probability compatibility identify failure with zero successful-output probability and an absent result in the discrete distribution.

@[simp]

theorem probOutput_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadAttach m] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] (x : α) : Pr[= x | failure] = 0

@[simp]

theorem probEvent_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadAttach m] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] (p : α → Prop) : probEvent failure p = 0

@[simp]

theorem probFailure_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadAttach m] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] : Pr[⊥ | failure] = 1

@[simp]

theorem evalSPMF_failure {m : Type u → Type v} [AlternativeMonad m] {α : Type u} [MonadLiftT m SPMF] [MonadAttach m] [EvalDistCompatible m] [HasEvalSet.LawfulFailure m] : 𝒮[failure] = failure