Source File Identifier index Theory binding index

```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

(*

[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

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1