Theory Error_Monad_Add

theory 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)"
  abbreviation ERRS_literal :: "String.literal ⇒ (unit ⇒ shows)" where "ERRS_literal 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