Structure readerMonadTheory

signature readerMonadTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BIND_def : thm
    val FMAP_def : thm
    val JOIN_def : thm
    val MCOMPOSE_def : thm
    val UNIT_def : thm
  
  (*  Theorems  *)
    val BIND_JOIN : thm
    val BIND_UNITL : thm
    val BIND_UNITR : thm
    val FMAP_BIND : thm
    val FMAP_ID : thm
    val FMAP_o : thm
    val JOIN_BIND : thm
    val MCOMPOSE_ASSOC : thm
    val MCOMPOSE_LEFT_ID : thm
    val MCOMPOSE_RIGHT_ID : thm
  
  val readerMonad_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "readerMonad"
   
   [patternMatches] Parent theory of "readerMonad"
   
   [BIND_def]  Definition
      
      ⊢ ∀M f s. BIND M f s = f (M s) s
   
   [FMAP_def]  Definition
      
      ⊢ ∀f M1. FMAP f M1 = f ∘ M1
   
   [JOIN_def]  Definition
      
      ⊢ ∀MM s. JOIN MM s = MM s s
   
   [MCOMPOSE_def]  Definition
      
      ⊢ ∀f1 f2 a. MCOMPOSE f1 f2 a = BIND (f1 a) f2
   
   [UNIT_def]  Definition
      
      ⊢ ∀x s. UNIT x s = x
   
   [BIND_JOIN]  Theorem
      
      ⊢ BIND M f = JOIN (FMAP f M)
   
   [BIND_UNITL]  Theorem
      
      ⊢ BIND (UNIT x) f = f x
   
   [BIND_UNITR]  Theorem
      
      ⊢ BIND m UNIT = m
   
   [FMAP_BIND]  Theorem
      
      ⊢ FMAP f M = BIND M (UNIT ∘ f)
   
   [FMAP_ID]  Theorem
      
      ⊢ FMAP (λx. x) M = M ∧ FMAP I M = M
   
   [FMAP_o]  Theorem
      
      ⊢ FMAP (f ∘ g) = FMAP f ∘ FMAP g
   
   [JOIN_BIND]  Theorem
      
      ⊢ JOIN M = BIND M I
   
   [MCOMPOSE_ASSOC]  Theorem
      
      ⊢ MCOMPOSE f (MCOMPOSE g h) = MCOMPOSE (MCOMPOSE f g) h
   
   [MCOMPOSE_LEFT_ID]  Theorem
      
      ⊢ MCOMPOSE UNIT g = g
   
   [MCOMPOSE_RIGHT_ID]  Theorem
      
      ⊢ MCOMPOSE f UNIT = f
   
   
*)
end

HOL 4, Kananaskis-13