readerMonadScript.sml

1Theory readerMonad
2Ancestors[qualified]
3  list
4
5(* the dependency on bossLib equates to an unnecessary dependency on
6   listTheory *)
7
8Definition BIND_def:
9  BIND (M : 's -> 'a) (f: 'a -> 's -> 'b) s = f (M s) s
10End
11
12Definition UNIT_def:
13  UNIT (x:'a) s = x
14End
15
16Definition MCOMPOSE_def:
17  MCOMPOSE (f1 : 'a -> ('s -> 'b)) (f2 : 'b -> ('s -> 'c)) a = BIND (f1 a) f2
18End
19
20Theorem BIND_UNITR[simp]: BIND m UNIT = m
21Proof
22  simp[FUN_EQ_THM, BIND_def, UNIT_def]
23QED
24
25Theorem BIND_UNITL[simp]: BIND (UNIT x) f = f x
26Proof
27  simp[FUN_EQ_THM, BIND_def, UNIT_def]
28QED
29
30Theorem MCOMPOSE_LEFT_ID[simp]: MCOMPOSE UNIT g = g
31Proof
32  simp[FUN_EQ_THM, UNIT_def, MCOMPOSE_def]
33QED
34
35Theorem MCOMPOSE_RIGHT_ID[simp]: MCOMPOSE f UNIT = f
36Proof
37  simp[FUN_EQ_THM, UNIT_def, MCOMPOSE_def]
38QED
39
40Theorem MCOMPOSE_ASSOC:
41  MCOMPOSE f (MCOMPOSE g h) = MCOMPOSE (MCOMPOSE f g) h
42Proof simp[MCOMPOSE_def, FUN_EQ_THM, BIND_def]
43QED
44
45Definition FMAP_def:
46  FMAP (f : 'a -> 'b) (M1 : 's -> 'a) = f o M1
47End
48
49Theorem FMAP_ID[simp]:
50  (FMAP (\x. x) M = M) /\ (FMAP I M = M)
51Proof simp[FMAP_def, FUN_EQ_THM]
52QED
53
54Theorem FMAP_o:
55  FMAP (f o g) = FMAP f o FMAP g
56Proof
57  simp[FMAP_def, FUN_EQ_THM]
58QED
59
60Theorem FMAP_BIND:
61  FMAP f M = BIND M (UNIT o f)
62Proof simp[FMAP_def, UNIT_def, BIND_def, FUN_EQ_THM]
63QED
64
65(* aka the W combinator *)
66Definition JOIN_def:
67  JOIN (MM : 's -> ('s -> 'a)) s = MM s s
68End
69
70Theorem BIND_JOIN:
71  BIND M f = JOIN (FMAP f M)
72Proof
73  simp[FUN_EQ_THM, JOIN_def, FMAP_def, BIND_def]
74QED
75
76Theorem JOIN_BIND:
77  JOIN M = BIND M I
78Proof
79  simp[FUN_EQ_THM, BIND_def, JOIN_def]
80QED
81
82val _ =
83    monadsyntax.declare_monad (
84      "reader",
85      {
86        bind = “readerMonad$BIND”, unit = “readerMonad$UNIT”,
87        ignorebind = NONE, choice = NONE, guard = NONE, fail = NONE
88      }
89    )
90
91
92