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