Structure errorStateMonadTheory

signature errorStateMonadTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BIND_DEF : thm
    val ES_APPLY_DEF : thm
    val ES_CHOICE_DEF : thm
    val ES_FAIL_DEF : thm
    val ES_GUARD_DEF : thm
    val ES_LIFT2_DEF : thm
    val EXT_DEF : thm
    val FOREACH_primitive_def : thm
    val FOR_primitive_def : thm
    val IGNORE_BIND_DEF : thm
    val JOIN_DEF : thm
    val MCOMP_DEF : thm
    val MMAP_DEF : thm
    val MWHILE_DEF : thm
    val MWHILE_UNIT_DEF : thm
    val NARROW_def : thm
    val READ_def : thm
    val UNIT_DEF : thm
    val WIDEN_def : thm
    val WRITE_def : thm
    val mapM_def : thm
    val mwhile_step_def : thm
    val mwhile_unit_step_def : thm
    val sequence_def : thm
  
  (*  Theorems  *)
    val APPLY_UNIT : thm
    val APPLY_UNIT_UNIT : thm
    val BIND_ASSOC : thm
    val BIND_ESGUARD : thm
    val BIND_FAIL_L : thm
    val BIND_LEFT_UNIT : thm
    val BIND_RIGHT_UNIT : thm
    val ES_CHOICE_ASSOC : thm
    val ES_CHOICE_FAIL_LID : thm
    val ES_CHOICE_FAIL_RID : thm
    val FOREACH_def : thm
    val FOREACH_ind : thm
    val FOR_def : thm
    val FOR_ind : thm
    val IGNORE_BIND_ESGUARD : thm
    val IGNORE_BIND_FAIL : thm
    val JOIN_MAP : thm
    val JOIN_MAP_JOIN : thm
    val JOIN_MMAP_UNIT : thm
    val JOIN_UNIT : thm
    val MCOMP_ASSOC : thm
    val MCOMP_ID : thm
    val MCOMP_THM : thm
    val MMAP_COMP : thm
    val MMAP_ID : thm
    val MMAP_JOIN : thm
    val MMAP_UNIT : thm
    val UNIT_CURRY : thm
    val mapM_cons : thm
    val mapM_nil : thm
    val mwhile_step_compute : thm
    val mwhile_unit_step_compute : thm
    val sequence_nil : thm
  
  val errorStateMonad_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "errorStateMonad"
   
   [patternMatches] Parent theory of "errorStateMonad"
   
   [BIND_DEF]  Definition
      
      ⊢ ∀g f s0.
          BIND g f s0 = case g s0 of NONE => NONE | SOME (b,s) => f b s
   
   [ES_APPLY_DEF]  Definition
      
      ⊢ ∀fM xM. fM <*> xM = BIND fM (λf. BIND xM (λx. UNIT (f x)))
   
   [ES_CHOICE_DEF]  Definition
      
      ⊢ ∀xM yM s.
          ES_CHOICE xM yM s =
          case xM s of NONE => yM s | SOME v1 => SOME v1
   
   [ES_FAIL_DEF]  Definition
      
      ⊢ ∀s. ES_FAIL s = NONE
   
   [ES_GUARD_DEF]  Definition
      
      ⊢ ∀b. ES_GUARD b = if b then UNIT () else ES_FAIL
   
   [ES_LIFT2_DEF]  Definition
      
      ⊢ ∀f xM yM. ES_LIFT2 f xM yM = MMAP f xM <*> yM
   
   [EXT_DEF]  Definition
      
      ⊢ ∀g m. EXT g m = BIND m g
   
   [FOREACH_primitive_def]  Definition
      
      ⊢ FOREACH =
        WFREC (@R. WF R ∧ ∀h a t. R (t,a) (h::t,a))
          (λFOREACH a'.
               case a' of
                 ([],a) => I (UNIT ())
               | (h::t,a) => I (BIND (a h) (λu. FOREACH (t,a))))
   
   [FOR_primitive_def]  Definition
      
      ⊢ FOR =
        WFREC
          (@R. WF R ∧
               ∀a j i.
                 i ≠ j ⇒ R (if i < j then i + 1 else i − 1,j,a) (i,j,a))
          (λFOR a'.
               case a' of
                 (i,j,a) =>
                   I
                     (if i = j then a i
                      else
                        BIND (a i)
                          (λu. FOR (if i < j then i + 1 else i − 1,j,a))))
   
   [IGNORE_BIND_DEF]  Definition
      
      ⊢ ∀f g. IGNORE_BIND f g = BIND f (λx. g)
   
   [JOIN_DEF]  Definition
      
      ⊢ ∀z. JOIN z = BIND z I
   
   [MCOMP_DEF]  Definition
      
      ⊢ ∀g f. MCOMP g f = CURRY (OPTION_MCOMP (UNCURRY g) (UNCURRY f))
   
   [MMAP_DEF]  Definition
      
      ⊢ ∀f m. MMAP f m = BIND m (UNIT ∘ f)
   
   [MWHILE_DEF]  Definition
      
      ⊢ ∀P g x s.
          MWHILE P g x s =
          BIND (P x) (λb. if b then BIND (g x) (MWHILE P g) else UNIT x) s
   
   [MWHILE_UNIT_DEF]  Definition
      
      ⊢ ∀P g s.
          MWHILE_UNIT P g s =
          BIND P
            (λb. if b then IGNORE_BIND g (MWHILE_UNIT P g) else UNIT ()) s
   
   [NARROW_def]  Definition
      
      ⊢ ∀v f.
          NARROW v f =
          (λs.
               case f (v,s) of
                 NONE => NONE
               | SOME (r,s1) => SOME (r,SND s1))
   
   [READ_def]  Definition
      
      ⊢ ∀f. READ f = (λs. SOME (f s,s))
   
   [UNIT_DEF]  Definition
      
      ⊢ ∀x. UNIT x = (λs. SOME (x,s))
   
   [WIDEN_def]  Definition
      
      ⊢ ∀f. WIDEN f =
            (λ(s1,s2).
                 case f s2 of NONE => NONE | SOME (r,s3) => SOME (r,s1,s3))
   
   [WRITE_def]  Definition
      
      ⊢ ∀f. WRITE f = (λs. SOME ((),f s))
   
   [mapM_def]  Definition
      
      ⊢ ∀f. mapM f = sequence ∘ MAP f
   
   [mwhile_step_def]  Definition
      
      ⊢ (∀P g x s. mwhile_step P g x 0 s = BIND (P x) (λb. UNIT (b,x)) s) ∧
        ∀P g x n s.
          mwhile_step P g x (SUC n) s =
          BIND (P x)
            (λb.
                 if b then BIND (g x) (λgx. mwhile_step P g gx n)
                 else UNIT (b,x)) s
   
   [mwhile_unit_step_def]  Definition
      
      ⊢ (∀P g s. mwhile_unit_step P g 0 s = P s) ∧
        ∀P g n s.
          mwhile_unit_step P g (SUC n) s =
          BIND P
            (λb.
                 if b then IGNORE_BIND g (mwhile_unit_step P g n)
                 else UNIT b) s
   
   [sequence_def]  Definition
      
      ⊢ sequence =
        FOLDR (λm ms. BIND m (λx. BIND ms (λxs. UNIT (x::xs)))) (UNIT [])
   
   [APPLY_UNIT]  Theorem
      
      ⊢ UNIT f <*> xM = MMAP f xM
   
   [APPLY_UNIT_UNIT]  Theorem
      
      ⊢ UNIT f <*> UNIT x = UNIT (f x)
   
   [BIND_ASSOC]  Theorem
      
      ⊢ ∀k m n. BIND k (λa. BIND (m a) n) = BIND (BIND k m) n
   
   [BIND_ESGUARD]  Theorem
      
      ⊢ BIND (ES_GUARD F) fM = ES_FAIL ∧ BIND (ES_GUARD T) fM = fM ()
   
   [BIND_FAIL_L]  Theorem
      
      ⊢ BIND ES_FAIL fM = ES_FAIL
   
   [BIND_LEFT_UNIT]  Theorem
      
      ⊢ ∀k x. BIND (UNIT x) k = k x
   
   [BIND_RIGHT_UNIT]  Theorem
      
      ⊢ ∀k. BIND k UNIT = k
   
   [ES_CHOICE_ASSOC]  Theorem
      
      ⊢ ES_CHOICE xM (ES_CHOICE yM zM) = ES_CHOICE (ES_CHOICE xM yM) zM
   
   [ES_CHOICE_FAIL_LID]  Theorem
      
      ⊢ ES_CHOICE ES_FAIL xM = xM
   
   [ES_CHOICE_FAIL_RID]  Theorem
      
      ⊢ ES_CHOICE xM ES_FAIL = xM
   
   [FOREACH_def]  Theorem
      
      ⊢ (∀a. FOREACH ([],a) = UNIT ()) ∧
        ∀t h a. FOREACH (h::t,a) = BIND (a h) (λu. FOREACH (t,a))
   
   [FOREACH_ind]  Theorem
      
      ⊢ ∀P. (∀a. P ([],a)) ∧ (∀h t a. P (t,a) ⇒ P (h::t,a)) ⇒
            ∀v v1. P (v,v1)
   
   [FOR_def]  Theorem
      
      ⊢ ∀j i a.
          FOR (i,j,a) =
          if i = j then a i
          else BIND (a i) (λu. FOR (if i < j then i + 1 else i − 1,j,a))
   
   [FOR_ind]  Theorem
      
      ⊢ ∀P. (∀i j a.
               (i ≠ j ⇒ P (if i < j then i + 1 else i − 1,j,a)) ⇒ P (i,j,a)) ⇒
            ∀v v1 v2. P (v,v1,v2)
   
   [IGNORE_BIND_ESGUARD]  Theorem
      
      ⊢ IGNORE_BIND (ES_GUARD F) xM = ES_FAIL ∧
        IGNORE_BIND (ES_GUARD T) xM = xM
   
   [IGNORE_BIND_FAIL]  Theorem
      
      ⊢ IGNORE_BIND ES_FAIL xM = ES_FAIL ∧ IGNORE_BIND xM ES_FAIL = ES_FAIL
   
   [JOIN_MAP]  Theorem
      
      ⊢ ∀k m. BIND k m = JOIN (MMAP m k)
   
   [JOIN_MAP_JOIN]  Theorem
      
      ⊢ JOIN ∘ MMAP JOIN = JOIN ∘ JOIN
   
   [JOIN_MMAP_UNIT]  Theorem
      
      ⊢ JOIN ∘ MMAP UNIT = I
   
   [JOIN_UNIT]  Theorem
      
      ⊢ JOIN ∘ UNIT = I
   
   [MCOMP_ASSOC]  Theorem
      
      ⊢ MCOMP f (MCOMP g h) = MCOMP (MCOMP f g) h
   
   [MCOMP_ID]  Theorem
      
      ⊢ MCOMP g UNIT = g ∧ MCOMP UNIT f = f
   
   [MCOMP_THM]  Theorem
      
      ⊢ MCOMP g f = EXT g ∘ f
   
   [MMAP_COMP]  Theorem
      
      ⊢ ∀f g. MMAP (f ∘ g) = MMAP f ∘ MMAP g
   
   [MMAP_ID]  Theorem
      
      ⊢ MMAP I = I
   
   [MMAP_JOIN]  Theorem
      
      ⊢ ∀f. MMAP f ∘ JOIN = JOIN ∘ MMAP (MMAP f)
   
   [MMAP_UNIT]  Theorem
      
      ⊢ ∀f. MMAP f ∘ UNIT = UNIT ∘ f
   
   [UNIT_CURRY]  Theorem
      
      ⊢ UNIT = CURRY SOME
   
   [mapM_cons]  Theorem
      
      ⊢ mapM f (x::xs) =
        BIND (f x) (λy. BIND (mapM f xs) (λys. UNIT (y::ys)))
   
   [mapM_nil]  Theorem
      
      ⊢ mapM f [] = UNIT []
   
   [mwhile_step_compute]  Theorem
      
      ⊢ (∀P g x s. mwhile_step P g x 0 s = BIND (P x) (λb. UNIT (b,x)) s) ∧
        (∀P g x n s.
           mwhile_step P g x (NUMERAL (BIT1 n)) s =
           BIND (P x)
             (λb.
                  if b then
                    BIND (g x)
                      (λgx. mwhile_step P g gx (NUMERAL (BIT1 n) − 1))
                  else UNIT (b,x)) s) ∧
        ∀P g x n s.
          mwhile_step P g x (NUMERAL (BIT2 n)) s =
          BIND (P x)
            (λb.
                 if b then
                   BIND (g x) (λgx. mwhile_step P g gx (NUMERAL (BIT1 n)))
                 else UNIT (b,x)) s
   
   [mwhile_unit_step_compute]  Theorem
      
      ⊢ (∀P g s. mwhile_unit_step P g 0 s = P s) ∧
        (∀P g n s.
           mwhile_unit_step P g (NUMERAL (BIT1 n)) s =
           BIND P
             (λb.
                  if b then
                    IGNORE_BIND g
                      (mwhile_unit_step P g (NUMERAL (BIT1 n) − 1))
                  else UNIT b) s) ∧
        ∀P g n s.
          mwhile_unit_step P g (NUMERAL (BIT2 n)) s =
          BIND P
            (λb.
                 if b then
                   IGNORE_BIND g (mwhile_unit_step P g (NUMERAL (BIT1 n)))
                 else UNIT b) s
   
   [sequence_nil]  Theorem
      
      ⊢ sequence [] = UNIT []
   
   
*)
end

HOL 4, Kananaskis-14