Structure errorLogMonadTheory

signature errorLogMonadTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val bind_def : thm
    val choice_def : thm
    val error_def : thm
    val log_def : thm
    val return_def : thm
    val silently_def : thm
  
  (*  Theorems  *)
    val M_CASES : thm
    val bind_EQ_success : thm
    val bind_IDL : thm
    val bind_IDR : thm
    val choice_return : thm
(*
   [errorMonad] Parent theory of "errorLogMonad"
   
   [bind_def]  Definition
      
      ⊢ ∀M f.
          bind M f =
          case M of
            (emret u,ms1) => (I ## $++ ms1) (f u)
          | (error e,ms1) => (error e,ms1)
   
   [choice_def]  Definition
      
      ⊢ ∀M1 M2.
          choice M1 M2 =
          case M1 of
            (emret v,ms1) => (emret v,ms1)
          | (error e,ms1) => (I ## $++ ms1) M2
   
   [error_def]  Definition
      
      ⊢ ∀e. error e = (error e,[])
   
   [log_def]  Definition
      
      ⊢ ∀m. log m = (emret (),[m])
   
   [return_def]  Definition
      
      ⊢ ∀v. return v = (emret v,[])
   
   [silently_def]  Definition
      
      ⊢ ∀M. silently M = (I ## K []) M
   
   [M_CASES]  Theorem
      
      ⊢ ∀M. (∃v ms. M = (emret v,ms)) ∨ ∃e ms. M = (error e,ms)
   
   [bind_EQ_success]  Theorem
      
      ⊢ bind M f = (emret v,ms) ⇔
        ∃u ms0 ms1.
          M = (emret u,ms0) ∧ f u = (emret v,ms1) ∧ ms = ms0 ⧺ ms1
   
   [bind_IDL]  Theorem
      
      ⊢ bind (return v) f = f v
   
   [bind_IDR]  Theorem
      
      ⊢ bind M return = M
   
   [choice_return]  Theorem
      
      ⊢ choice (return v) M = return v
   
   
*)
end

HOL 4, Trindemossen-2