Structure state_transformerTheory

signature state_transformerTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BIND_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 NARROW_def : thm
    val READ_def : thm
    val UNIT_DEF : thm
    val WIDEN_def : thm
    val WRITE_def : thm
    val mapM_def : thm
    val sequence_def : thm
  
  (*  Theorems  *)
    val BIND_ASSOC : thm
    val BIND_EXT : thm
    val BIND_LEFT_UNIT : thm
    val BIND_RIGHT_UNIT : thm
    val EXT_JM : thm
    val EXT_MCOMP : thm
    val EXT_UNIT : thm
    val EXT_o_JOIN : thm
    val EXT_o_UNIT : thm
    val FOREACH_def : thm
    val FOREACH_ind : thm
    val FOR_def : thm
    val FOR_ind : thm
    val FST_o_MMAP : thm
    val FST_o_UNIT : thm
    val JOIN_EXT : thm
    val JOIN_MAP : thm
    val JOIN_MAP_JOIN : thm
    val JOIN_MMAP_UNIT : thm
    val JOIN_UNIT : thm
    val MCOMP_ALT : thm
    val MCOMP_ASSOC : thm
    val MCOMP_ID : thm
    val MMAP_COMP : thm
    val MMAP_EXT : thm
    val MMAP_ID : thm
    val MMAP_JOIN : thm
    val MMAP_UNIT : thm
    val SND_o_UNIT : thm
    val UNIT_CURRY : thm
    val UNIT_UNCURRY : thm
    val UNIT_o_MCOMP : thm
    val mapM_cons : thm
    val mapM_nil : thm
    val sequence_nil : thm
  
  val state_transformer_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [list] Parent theory of "state_transformer"
   
   [BIND_DEF]  Definition
      
      ⊢ ∀g f. monad_bind g f = UNCURRY f ∘ g
   
   [EXT_DEF]  Definition
      
      ⊢ ∀f m. EXT f m = UNCURRY f ∘ m
   
   [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 do u <- a h; FOREACH (t,a) od)
   
   [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
                        do
                          u <- a i;
                          FOR (if i < j then i + 1 else i − 1,j,a)
                        od))
   
   [IGNORE_BIND_DEF]  Definition
      
      ⊢ ∀f g. do f; g od = do x <- f; g od
   
   [JOIN_DEF]  Definition
      
      ⊢ ∀z. JOIN z = monad_bind z I
   
   [MCOMP_DEF]  Definition
      
      ⊢ ∀g f. MCOMP g f = EXT g ∘ f
   
   [MMAP_DEF]  Definition
      
      ⊢ ∀f m. MMAP f m = monad_bind m (UNIT ∘ f)
   
   [MWHILE_DEF]  Definition
      
      ⊢ ∀g b.
          MWHILE g b =
          do gv <- g; if gv then do b; MWHILE g b od else UNIT () od
   
   [NARROW_def]  Definition
      
      ⊢ ∀v f. NARROW v f = (λs. (let (r,s1) = f (v,s) in (r,SND s1)))
   
   [READ_def]  Definition
      
      ⊢ ∀f. READ f = (λs. (f s,s))
   
   [UNIT_DEF]  Definition
      
      ⊢ ∀x. UNIT x = (λs. (x,s))
   
   [WIDEN_def]  Definition
      
      ⊢ ∀f. WIDEN f = (λ(s1,s2). (let (r,s3) = f s2 in (r,s1,s3)))
   
   [WRITE_def]  Definition
      
      ⊢ ∀f. WRITE f = (λs. ((),f s))
   
   [mapM_def]  Definition
      
      ⊢ ∀f. mapM f = sequence ∘ MAP f
   
   [sequence_def]  Definition
      
      ⊢ sequence =
        FOLDR (λm ms. do x <- m; xs <- ms; UNIT (x::xs) od) (UNIT [])
   
   [BIND_ASSOC]  Theorem
      
      ⊢ ∀k m n.
          do a <- k; monad_bind (m a) n od = monad_bind (monad_bind k m) n
   
   [BIND_EXT]  Theorem
      
      ⊢ monad_bind m f = EXT f m
   
   [BIND_LEFT_UNIT]  Theorem
      
      ⊢ ∀k x. monad_bind (UNIT x) k = k x
   
   [BIND_RIGHT_UNIT]  Theorem
      
      ⊢ ∀k. monad_bind k UNIT = k
   
   [EXT_JM]  Theorem
      
      ⊢ EXT f = JOIN ∘ MMAP f
   
   [EXT_MCOMP]  Theorem
      
      ⊢ EXT (MCOMP g f) = EXT g ∘ EXT f
   
   [EXT_UNIT]  Theorem
      
      ⊢ EXT UNIT = I
   
   [EXT_o_JOIN]  Theorem
      
      ⊢ ∀f. EXT f ∘ JOIN = EXT (EXT f)
   
   [EXT_o_UNIT]  Theorem
      
      ⊢ EXT f ∘ UNIT = f
   
   [FOREACH_def]  Theorem
      
      ⊢ (∀a. FOREACH ([],a) = UNIT ()) ∧
        ∀t h a. FOREACH (h::t,a) = do u <- a h; FOREACH (t,a) od
   
   [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 do u <- a i; FOR (if i < j then i + 1 else i − 1,j,a) od
   
   [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)
   
   [FST_o_MMAP]  Theorem
      
      ⊢ ∀f g. FST ∘ MMAP f g = f ∘ FST ∘ g
   
   [FST_o_UNIT]  Theorem
      
      ⊢ ∀x. FST ∘ UNIT x = K x
   
   [JOIN_EXT]  Theorem
      
      ⊢ JOIN = EXT I
   
   [JOIN_MAP]  Theorem
      
      ⊢ ∀k m. monad_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_ALT]  Theorem
      
      ⊢ MCOMP g f = CURRY (UNCURRY g ∘ UNCURRY f)
   
   [MCOMP_ASSOC]  Theorem
      
      ⊢ MCOMP f (MCOMP g h) = MCOMP (MCOMP f g) h
   
   [MCOMP_ID]  Theorem
      
      ⊢ MCOMP g UNIT = g ∧ MCOMP UNIT f = f
   
   [MMAP_COMP]  Theorem
      
      ⊢ ∀f g. MMAP (f ∘ g) = MMAP f ∘ MMAP g
   
   [MMAP_EXT]  Theorem
      
      ⊢ MMAP f = EXT (UNIT ∘ f)
   
   [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
   
   [SND_o_UNIT]  Theorem
      
      ⊢ ∀x. SND ∘ UNIT x = I
   
   [UNIT_CURRY]  Theorem
      
      ⊢ UNIT = CURRY I
   
   [UNIT_UNCURRY]  Theorem
      
      ⊢ ∀s. UNCURRY UNIT s = s
   
   [UNIT_o_MCOMP]  Theorem
      
      ⊢ MCOMP (UNIT ∘ g) (UNIT ∘ f) = UNIT ∘ g ∘ f
   
   [mapM_cons]  Theorem
      
      ⊢ mapM f (x::xs) = do y <- f x; ys <- mapM f xs; UNIT (y::ys) od
   
   [mapM_nil]  Theorem
      
      ⊢ mapM f [] = UNIT []
   
   [sequence_nil]  Theorem
      
      ⊢ sequence [] = UNIT []
   
   
*)
end

HOL 4, Kananaskis-14