Theory Munta_Error_Monad_Add

(* Author: Peter Lammich *)
section ‹More Material on the Error Monad›

theory Munta_Error_Monad_Add
imports
  Certification_Monads.Check_Monad
  Show.Show_Instances
begin
(* TODO: Move *)
abbreviation "assert_opt Φ ≡ if Φ then Some () else None"

definition "lift_opt m e ≡ case m of Some x ⇒ Error_Monad.return x | None ⇒ Error_Monad.error e"

lemma lift_opt_simps[simp]:
  "lift_opt None e = error e"
  "lift_opt (Some v) e = return v"
  by (auto simp: lift_opt_def)

(* TODO: Move *)
lemma reflcl_image_iff[simp]: "R⇧=``S = S∪R``S" by blast

named_theorems return_iff

lemma bind_return_iff[return_iff]: "Error_Monad.bind m f = Inr y ⟷ (∃x. m = Inr x ∧ f x = Inr y)"
  by auto

lemma lift_opt_return_iff[return_iff]: "lift_opt m e = Inr x ⟷ m=Some x"
  unfolding lift_opt_def by (auto split: option.split)

lemma check_return_iff[return_iff]: "check Φ e = Inr uu ⟷ Φ"
  by (auto simp: check_def)


lemma check_simps[simp]:
  "check True e = succeed"
  "check False e = error e"
  by (auto simp: check_def)

lemma Let_return_iff[return_iff]: "(let x=v in f x) = Inr w ⟷ f v = Inr w" by simp


abbreviation ERR :: "shows ⇒ (unit ⇒ shows)" where "ERR s ≡ λ_. s"
abbreviation ERRS :: "string ⇒ (unit ⇒ shows)" where "ERRS s ≡ ERR (shows s)"


lemma error_monad_bind_split:
"P (bind m f) ⟷ (∀v. m = Inl v ⟶ P (Inl v)) ∧ (∀v. m = Inr v ⟶ P (f v))"
by (cases m) auto

lemma error_monad_bind_split_asm:
"P (bind m f) ⟷ ¬ (∃x. m = Inl x ∧ ¬ P (Inl x) ∨ (∃x. m = Inr x ∧ ¬ P (f x)))"
  by (cases m) auto

lemmas error_monad_bind_splits =error_monad_bind_split error_monad_bind_split_asm

end