state_transformerScript.sml

1Theory state_transformer
2Ancestors
3  pair combin list
4Libs
5  pairSyntax simpLib BasicProvers boolSimps metisLib
6
7(* ------------------------------------------------------------------------- *)
8(* Definitions.                                                              *)
9(* ------------------------------------------------------------------------- *)
10
11Type M[local] = “:'state -> 'a # 'state”
12
13(* identity of the Kleisli category *)
14Definition UNIT_DEF:   UNIT (x:'b) = \(s:'a). (x, s)
15End
16
17Definition BIND_DEF:   BIND (g: ('b, 'a) M) (f: 'b -> ('c, 'a) M) = UNCURRY f o g
18End
19
20Definition IGNORE_BIND_DEF:   IGNORE_BIND f g = BIND f (\x. g)
21End
22
23val _ =
24    monadsyntax.declare_monad (
25      "state",
26      { bind = “BIND”, ignorebind = SOME “IGNORE_BIND”, unit = “UNIT”,
27        choice = NONE, fail = NONE, guard = NONE
28      }
29    )
30val _ = monadsyntax.add_monadsyntax()
31val _ = monadsyntax.enable_monad "state"
32
33Definition MMAP_DEF:   MMAP (f: 'c -> 'b) (m: ('c, 'a) M) = BIND m (UNIT o f)
34End
35
36Definition JOIN_DEF:   JOIN (z: (('b, 'a) M, 'a) M) = BIND z I
37End
38
39(* functor (on arrows) from the Kleisli category *)
40Definition EXT_DEF:   EXT (f: 'b -> ('c, 's) M) (m: ('b, 's) M) = UNCURRY f o m
41End
42
43(* composition in the Kleisli category *)
44Definition MCOMP_DEF:
45   MCOMP (g: 'b -> ('c, 's) M) (f: 'a -> ('b, 's) M) = EXT g o f
46End
47
48val FOR_def = TotalDefn.tDefine "FOR"
49 `(FOR : num # num # (num -> (unit, 'state) M) -> (unit, 'state) M) (i, j, a) =
50     if i = j then
51        a i
52     else
53        BIND (a i) (\u. FOR (if i < j then i + 1 else i - 1, j, a))`
54  (TotalDefn.WF_REL_TAC `measure (\(i, j, a). if i < j then j - i else i - j)`)
55
56Definition FOREACH_def:
57   ((FOREACH : 'a list # ('a -> (unit, 'state) M) -> (unit, 'state) M) ([], a) =
58       UNIT ()) /\
59   (FOREACH (h :: t, a) = BIND (a h) (\u. FOREACH (t, a)))
60End
61
62Definition READ_def:
63   (READ : ('state -> 'a) -> ('a, 'state) M) f = \s. (f s, s)
64End
65
66Definition WRITE_def:
67   (WRITE : ('state -> 'state) -> (unit, 'state) M) f = \s. ((), f s)
68End
69
70Definition NARROW_def:
71   (NARROW : 'b -> ('a, 'b # 'state) M -> ('a, 'state) M) v f =
72   \s. let (r, s1) = f (v, s) in (r, SND s1)
73End
74
75Definition WIDEN_def:
76   (WIDEN : ('a, 'state) M -> ('a, 'b # 'state) M) f =
77   \(s1, s2). let (r, s3) = f s2 in (r, (s1, s3))
78End
79
80Definition sequence_def:
81   sequence = FOLDR (\m ms. BIND m (\x. BIND ms (\xs. UNIT (x::xs)))) (UNIT [])
82End
83
84Definition mapM_def:
85   mapM f = sequence o MAP f
86End
87
88Theorem mwhile_exists[local]:
89    !g b. ?f.
90      f = BIND g (\gv. if gv then IGNORE_BIND b f else UNIT ())
91Proof
92  MAP_EVERY Q.X_GEN_TAC [`g`, `b`] THEN
93  Q.EXISTS_TAC
94    `\s0. if ?n. ~FST (g (FUNPOW (SND o b o SND o g) n s0)) then
95            let n = LEAST n. ~FST (g (FUNPOW (SND o b o SND o g) n s0))
96            in
97              ((), SND (g (FUNPOW (SND o b o SND o g) n s0)))
98          else ARB` THEN
99  SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN Q.X_GEN_TAC `s` THEN
100  COND_CASES_TAC THENL [
101    POP_ASSUM (Q.X_CHOOSE_THEN `n0` ASSUME_TAC) THEN
102    SIMP_TAC (srw_ss()) [SimpLHS, LET_THM] THEN
103    numLib.LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC[] THEN
104    Q.X_GEN_TAC `n` THEN SIMP_TAC (srw_ss()) [] THEN STRIP_TAC THEN
105    SIMP_TAC (srw_ss()) [BIND_DEF] THEN
106    Q.SPEC_THEN `g s` (Q.X_CHOOSE_THEN `gv1`
107                                       (Q.X_CHOOSE_THEN `s1` ASSUME_TAC))
108                pairTheory.pair_CASES THEN
109    ASM_SIMP_TAC (srw_ss()) [] THEN REVERSE (Cases_on `gv1`)
110    THEN1 (`n = 0`
111             by (SPOSE_NOT_THEN ASSUME_TAC THEN
112                 `0 < n` by SRW_TAC [numSimps.ARITH_ss][] THEN
113                 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
114                 SRW_TAC [][]) THEN
115           SRW_TAC [][UNIT_DEF]) THEN
116    ASM_SIMP_TAC (srw_ss()) [IGNORE_BIND_DEF, BIND_DEF] THEN
117    Q.SPEC_THEN `b s1` (Q.X_CHOOSE_THEN `bv1`
118                                        (Q.X_CHOOSE_THEN `s2` ASSUME_TAC))
119                pairTheory.pair_CASES THEN
120    ASM_SIMP_TAC (srw_ss()) [] THEN
121    `?m. n = SUC m`
122      by (Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) []) THEN
123    Q.SUBGOAL_THEN `?n. ~FST (g (FUNPOW (SND o b o SND o g) n s2))`
124      ASSUME_TAC
125    THEN1 (Q.EXISTS_TAC `m` THEN
126           FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.FUNPOW]) THEN
127    ASM_SIMP_TAC (srw_ss()) [arithmeticTheory.FUNPOW] THEN
128    Q_TAC SUFF_TAC
129       `(LEAST n. ~FST (g (FUNPOW (SND o b o SND o g) n s2))) = m`
130       THEN1 SRW_TAC [][] THEN
131    numLib.LEAST_ELIM_TAC THEN CONJ_TAC THEN1 SRW_TAC [][] THEN
132    Q.X_GEN_TAC `p` THEN SRW_TAC [][] THEN
133    Q_TAC SUFF_TAC `~(m < p) /\ ~(p < m)` THEN1 numLib.ARITH_TAC THEN
134    REPEAT STRIP_TAC THENL [
135      `FST (g (FUNPOW (SND o b o SND o g) m s2))` by METIS_TAC[] THEN
136      `FST (g (FUNPOW (SND o b o SND o g) (SUC m) s))`
137         by (SIMP_TAC (srw_ss())[arithmeticTheory.FUNPOW] THEN
138             SRW_TAC [][]),
139      `SUC p < SUC m` by SRW_TAC [numSimps.ARITH_ss][] THEN
140      RES_THEN MP_TAC THEN
141      SIMP_TAC (srw_ss()) [arithmeticTheory.FUNPOW] THEN
142      SRW_TAC [][]
143    ],
144    FULL_SIMP_TAC (srw_ss()) [BIND_DEF] THEN
145    Q.SPEC_THEN `g s` (Q.X_CHOOSE_THEN `gv1`
146                                       (Q.X_CHOOSE_THEN `s1` ASSUME_TAC))
147                pairTheory.pair_CASES THEN
148    REVERSE (SRW_TAC [][])
149      THEN1(FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN SRW_TAC [][]) THEN
150    SRW_TAC [][IGNORE_BIND_DEF, BIND_DEF] THEN
151    Q.SPEC_THEN `b s1` (Q.X_CHOOSE_THEN `bv1`
152                                        (Q.X_CHOOSE_THEN `s2` ASSUME_TAC))
153                pairTheory.pair_CASES THEN
154    SRW_TAC [][] THEN
155    FIRST_X_ASSUM (Q.SPEC_THEN `SUC m` (MP_TAC o Q.GEN `m`)) THEN
156    SRW_TAC [][arithmeticTheory.FUNPOW]
157  ]
158QED
159
160val MWHILE_DEF = new_specification(
161  "MWHILE_DEF", ["MWHILE"],
162  mwhile_exists |> SIMP_RULE bool_ss [SKOLEM_THM]);
163
164(* ------------------------------------------------------------------------- *)
165(* Theorems.                                                                 *)
166(* ------------------------------------------------------------------------- *)
167
168val Suff = Q_TAC SUFF_TAC
169val Know = Q_TAC KNOW_TAC
170val FUN_EQ_TAC = CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV)
171
172(* UNIT and MCOMP are identity and composition of the Kleisli category *)
173Theorem UNIT_CURRY:
174     UNIT = CURRY I
175Proof
176   REWRITE_TAC [CURRY_DEF, UNIT_DEF, FUN_EQ_THM, combinTheory.I_THM]
177    >> BETA_TAC >> REWRITE_TAC []
178QED
179
180Theorem MCOMP_ALT:
181    MCOMP g f = CURRY (UNCURRY g o UNCURRY f)
182Proof
183  REWRITE_TAC [MCOMP_DEF, CURRY_DEF, FUN_EQ_THM, o_THM, UNCURRY_DEF, EXT_DEF]
184QED
185
186Theorem MCOMP_ID:
187     (MCOMP g UNIT = g) /\ (MCOMP UNIT f = f)
188Proof
189  REWRITE_TAC [MCOMP_ALT, UNIT_CURRY,
190    UNCURRY_CURRY_THM, CURRY_UNCURRY_THM, I_o_ID]
191QED
192
193Theorem MCOMP_ASSOC:
194     MCOMP f (MCOMP g h) = MCOMP (MCOMP f g) h
195Proof
196  REWRITE_TAC [MCOMP_ALT, o_ASSOC, UNCURRY_CURRY_THM, CURRY_UNCURRY_THM]
197QED
198
199(* EXT is a functor from the Kleisli category into the (I,o) category *)
200Theorem EXT_UNIT:
201    EXT UNIT = I
202Proof
203  REWRITE_TAC [FUN_EQ_THM, EXT_DEF, UNIT_CURRY,
204    UNCURRY_CURRY_THM, o_THM, I_THM]
205QED
206
207Theorem EXT_MCOMP:
208    EXT (MCOMP g f) = EXT g o EXT f
209Proof
210  REWRITE_TAC [FUN_EQ_THM, EXT_DEF, UNCURRY_CURRY_THM, o_THM, MCOMP_ALT]
211QED
212
213Theorem EXT_o_UNIT:
214    EXT f o UNIT = f
215Proof
216  REWRITE_TAC [GSYM MCOMP_DEF, MCOMP_ID]
217QED
218
219(* UNIT o _ is the functor in the opposite direction *)
220Theorem UNIT_o_MCOMP:
221    MCOMP (UNIT o g) (UNIT o f) = UNIT o g o f
222Proof
223  REWRITE_TAC [MCOMP_DEF, o_ASSOC, EXT_o_UNIT]
224QED
225
226Theorem BIND_EXT:
227    BIND m f = EXT f m
228Proof
229  REWRITE_TAC [BIND_DEF, EXT_DEF]
230QED
231
232Theorem MMAP_EXT:
233    MMAP f = EXT (UNIT o f)
234Proof
235  REWRITE_TAC [FUN_EQ_THM, MMAP_DEF, BIND_EXT]
236QED
237
238Theorem JOIN_EXT:
239    JOIN = EXT I
240Proof
241  REWRITE_TAC [FUN_EQ_THM, JOIN_DEF, BIND_EXT]
242QED
243
244Theorem EXT_JM:
245    EXT f = JOIN o MMAP f
246Proof
247  REWRITE_TAC [JOIN_EXT, BIND_EXT, MMAP_EXT, GSYM EXT_MCOMP,
248    MCOMP_DEF, o_ASSOC, EXT_o_UNIT, I_o_ID]
249QED
250
251Theorem BIND_LEFT_UNIT:
252     !(k:'a->'b->'c#'b) x. BIND (UNIT x) k = k x
253Proof
254   REPEAT STRIP_TAC
255   >> MATCH_MP_TAC EQ_EXT
256   >> REWRITE_TAC [BIND_DEF, UNIT_DEF, o_DEF]
257   >> CONV_TAC (DEPTH_CONV BETA_CONV)
258   >> REWRITE_TAC [UNCURRY_DEF]
259QED
260
261Theorem UNIT_UNCURRY:
262     !(s:'a#'b). UNCURRY UNIT s = s
263Proof
264   REWRITE_TAC [UNCURRY_VAR, UNIT_DEF]
265   >> CONV_TAC (DEPTH_CONV BETA_CONV)
266   >> REWRITE_TAC [PAIR]
267QED
268
269Theorem BIND_RIGHT_UNIT:
270     !(k:'a->'b#'a). BIND k UNIT = k
271Proof
272   REPEAT STRIP_TAC
273   >> MATCH_MP_TAC EQ_EXT
274   >> REWRITE_TAC [BIND_DEF, UNIT_UNCURRY, o_DEF]
275   >> CONV_TAC (DEPTH_CONV BETA_CONV)
276   >> REWRITE_TAC []
277QED
278
279Theorem BIND_ASSOC:
280     !(k:'a->'b#'a) (m:'b->'a->'c#'a) (n:'c->'a->'d#'a).
281       BIND k (\a. BIND (m a) n) = BIND (BIND k m) n
282Proof
283   REWRITE_TAC [BIND_DEF, UNCURRY_VAR, o_DEF]
284   >> CONV_TAC (DEPTH_CONV BETA_CONV)
285   >> REWRITE_TAC []
286QED
287
288Theorem MMAP_ID:
289     MMAP I = (I:('a->'b#'a)->('a->'b#'a))
290Proof
291   REWRITE_TAC [MMAP_EXT, I_o_ID, EXT_UNIT]
292QED
293
294Theorem MMAP_COMP:
295     !f g. (MMAP (f o g):('a->'b#'a)->('a->'d#'a))
296           = (MMAP f:('a->'c#'a)->('a->'d#'a)) o MMAP g
297Proof
298   REWRITE_TAC [MMAP_EXT, o_THM, GSYM EXT_MCOMP, UNIT_o_MCOMP]
299QED
300
301Theorem MMAP_UNIT:
302     !(f:'b->'c). MMAP f o UNIT = (UNIT:'c->'a->'c#'a) o f
303Proof
304   REWRITE_TAC [MMAP_EXT, EXT_o_UNIT]
305QED
306
307Theorem EXT_o_JOIN:
308     !f. EXT f o JOIN = EXT (EXT f:('a->'b#'a)->('a->'c#'a))
309Proof
310   REWRITE_TAC [JOIN_EXT, GSYM EXT_MCOMP, MCOMP_DEF, I_o_ID]
311QED
312
313Theorem MMAP_JOIN:
314     !f. MMAP f o JOIN = JOIN o MMAP (MMAP f:('a->'b#'a)->('a->'c#'a))
315Proof
316   REWRITE_TAC [GSYM EXT_JM] >> REWRITE_TAC [MMAP_EXT, EXT_o_JOIN]
317QED
318
319Theorem JOIN_UNIT:
320     JOIN o UNIT = (I:('a->'b#'a)->('a->'b#'a))
321Proof
322   REWRITE_TAC [JOIN_EXT, EXT_o_UNIT]
323QED
324
325Theorem JOIN_MMAP_UNIT:
326     JOIN o MMAP UNIT = (I:('a->'b#'a)->('a->'b#'a))
327Proof
328   REWRITE_TAC [GSYM EXT_JM, EXT_UNIT]
329QED
330
331Theorem JOIN_MAP_JOIN:
332     JOIN o MMAP JOIN = ((JOIN o JOIN)
333       :('a -> ('a -> ('a -> 'b # 'a) # 'a) # 'a) -> 'a -> 'b # 'a)
334Proof
335   REWRITE_TAC [GSYM EXT_JM] >> REWRITE_TAC [JOIN_EXT, GSYM EXT_o_JOIN]
336QED
337
338Theorem JOIN_MAP:
339     !k (m:'b->'a->'c#'a). BIND k m = JOIN (MMAP m k)
340Proof
341   REWRITE_TAC [BIND_EXT, EXT_JM, o_THM]
342QED
343
344Theorem FST_o_UNIT:
345     !x. FST o UNIT x = K x
346Proof
347   FUN_EQ_TAC
348   >> REWRITE_TAC [o_THM, UNIT_DEF, K_THM]
349   >> BETA_TAC
350   >> REWRITE_TAC [FST]
351QED
352
353Theorem SND_o_UNIT:
354     !x. SND o UNIT x = I
355Proof
356   FUN_EQ_TAC
357   >> REWRITE_TAC [o_THM, UNIT_DEF, I_THM]
358   >> BETA_TAC
359   >> REWRITE_TAC [SND]
360QED
361
362Theorem FST_o_MMAP:
363     !f g. FST o MMAP f g = f o FST o g
364Proof
365   FUN_EQ_TAC
366   >> REWRITE_TAC [MMAP_DEF, BIND_DEF, UNCURRY, o_THM, UNIT_DEF]
367   >> BETA_TAC
368   >> REWRITE_TAC [FST]
369QED
370
371Theorem sequence_nil[simp]:
372    sequence [] = UNIT []
373Proof
374  BasicProvers.SRW_TAC[][sequence_def]
375QED
376
377Theorem mapM_nil[simp]:
378    mapM f [] = UNIT []
379Proof
380  BasicProvers.SRW_TAC[][mapM_def]
381QED
382
383Theorem mapM_cons:
384    mapM f (x::xs) = BIND (f x) (\y. BIND (mapM f xs) (\ys. UNIT (y::ys)))
385Proof
386  BasicProvers.SRW_TAC[][mapM_def,sequence_def]
387QED
388
389(*---------------------------------------------------------------------------*)
390(* Support for termination condition extraction for recursive monadic defns. *)
391(*---------------------------------------------------------------------------*)
392(*
393Theorem BIND_CONG[defncong]:
394 !a b c d.
395   (a = c) /\
396   (!x y s. (c s = (x,y)) ==> (b x y = d x y))
397    ==>
398   (BIND a b = BIND c d)
399Proof
400 SRW_TAC [] [BIND_DEF,pairTheory.UNCURRY_VAR,combinTheory.o_DEF,FUN_EQ_THM]
401  THEN FIRST_ASSUM MATCH_MP_TAC
402  THEN METIS_TAC [pairTheory.PAIR]
403QED
404
405val _ = TotalDefn.export_termsimp "UNIT_DEF"
406*)
407
408(* ------------------------------------------------------------------------- *)