itreeScript.sml
1(*
2 This file defines a type for potentially infinite interaction
3 trees. We take inspiration from the itree type of Xia et al.'s
4 POPL'20 paper titled "Interaction Trees".
5
6 Interaction trees are interesting because they can both represent a
7 program's observable I/O behaviour and also model of the I/O
8 behaviour of the external world.
9
10 Our version of the type for interaction trees, itree, has the
11 following constructors. Here Ret ends an interaction tree with a
12 return value; Div is internal silent divergence (an infinite run of
13 Taus); Vis is a visible event that returns a value that the rest of
14 the interaction tree can depend on.
15
16 ('a,'e,'r) itree =
17 Ret 'r -- termination with result 'r
18 | Div -- end in silent divergence
19 | Vis 'e ('a -> ('a,'e,'r) itree) -- visible event 'e with answer 'a,
20 then continue based on answer
21
22 The POPL paper includes a silent Tau action:
23
24 | Tau (('a,'e,'r) itree) -- a silent action, then continue
25
26 We omit Tau since it makes reasoning about intereaction trees
27 messy. It causes a mess because one then has to deal with equality
28 up to deletion of finite runs of Tau actions, ugh. We model an
29 infinite run of Taus using Div.
30*)
31Theory itree
32Ancestors
33 list combin
34Libs
35 dep_rewrite
36
37(* make type definition *)
38
39Datatype:
40 itree_el = Event 'e | Return 'r | Stuck
41End
42
43Type itree_rep[local] = ``:'a list -> ('e,'r) itree_el``;
44val f = ``(f: ('a,'e,'r) itree_rep)``
45
46Definition path_ok_def:
47 path_ok path ^f <=>
48 !xs y ys.
49 path = xs ++ y::ys ==>
50 f xs <> Stuck /\
51 !z. f xs <> Return z (* a path cannot continue past a Stuck/Return *)
52End
53
54Definition itree_rep_ok_def:
55 itree_rep_ok ^f <=>
56 (* every bad path leads to the Return ARB element *)
57 !path. ~path_ok path f ==> f path = Return ARB
58End
59
60Theorem type_inhabited[local]:
61 ?f. itree_rep_ok ^f
62Proof
63 qexists_tac `\p. Return ARB` \\ fs [itree_rep_ok_def]
64QED
65
66val itree_tydef = new_type_definition ("itree", type_inhabited);
67
68val repabs_fns = define_new_type_bijections
69 { name = "itree_absrep",
70 ABS = "itree_abs",
71 REP = "itree_rep",
72 tyax = itree_tydef};
73
74
75(* prove basic theorems about rep and abs fucntions *)
76
77val itree_absrep = CONJUNCT1 repabs_fns
78val itree_repabs = CONJUNCT2 repabs_fns
79
80Theorem itree_rep_ok_itree_rep[local,simp]:
81 !t. itree_rep_ok (itree_rep t)
82Proof
83 fs [itree_repabs, itree_absrep]
84QED
85
86Theorem itree_abs_11[local]:
87 itree_rep_ok r1 /\ itree_rep_ok r2 ==>
88 (itree_abs r1 = itree_abs r2 <=> r1 = r2)
89Proof
90 fs [itree_repabs, EQ_IMP_THM] \\ metis_tac []
91QED
92
93Theorem itree_rep_11[local]:
94 (itree_rep t1 = itree_rep t2) = (t1 = t2)
95Proof
96 fs [EQ_IMP_THM] \\ metis_tac [itree_absrep]
97QED
98
99
100(* define constructors *)
101
102Definition Ret_rep_def:
103 Ret_rep (x:'r) =
104 \path. if path = [] then Return x else Return ARB
105End
106
107Definition Div_rep_def:
108 Div_rep =
109 \path. if path = [] then Stuck else Return ARB
110End
111
112Definition Vis_rep_def:
113 Vis_rep e g =
114 \path. case path of
115 | [] => Event e
116 | (a::rest) => g a rest
117End
118
119Definition Ret_def:
120 Ret x = itree_abs (Ret_rep x)
121End
122
123Definition Div_def:
124 Div = itree_abs Div_rep
125End
126
127Definition Vis_def:
128 Vis e g = itree_abs (Vis_rep e (itree_rep o g))
129End
130
131Theorem itree_rep_ok_Ret[local]:
132 !x. itree_rep_ok (Ret_rep x : ('a,'b,'c) itree_rep)
133Proof
134 fs [itree_rep_ok_def,Ret_rep_def]
135 \\ rw [] \\ fs [path_ok_def]
136QED
137
138Theorem itree_rep_ok_Div[local]:
139 itree_rep_ok (Div_rep : ('a,'b,'c) itree_rep)
140Proof
141 fs [itree_rep_ok_def,Div_rep_def]
142 \\ rw [] \\ fs [path_ok_def]
143QED
144
145Theorem itree_rep_ok_Vis[local]:
146 !a g. (!a. itree_rep_ok (g a)) ==>
147 itree_rep_ok (Vis_rep e g : ('a,'b,'c) itree_rep)
148Proof
149 fs [itree_rep_ok_def,Vis_rep_def]
150 \\ rw [] \\ CCONTR_TAC \\ fs [AllCaseEqs()]
151 \\ Cases_on `path` \\ fs [] THEN1 fs [path_ok_def]
152 \\ qpat_x_assum `~(path_ok _ _)` mp_tac \\ fs []
153 \\ simp [path_ok_def] \\ rw [] \\ rename [‘h::t = path ++ [y] ++ ys’]
154 \\ Cases_on `path` \\ fs [] \\ rw []
155 \\ CCONTR_TAC \\ fs []
156 \\ rename [`xs ++ [y] ++ ys`] \\ fs []
157 \\ first_x_assum (qspecl_then [`h`,`xs ++ [y] ++ ys`] mp_tac)
158 \\ fs [] \\ rw [] \\ fs [path_ok_def]
159 \\ metis_tac []
160QED
161
162
163(* prove injectivity *)
164
165Theorem Ret_rep_11[local]:
166 !x y. Ret_rep x = Ret_rep y <=> x = y
167Proof
168 fs [Ret_rep_def,FUN_EQ_THM]
169 \\ rpt gen_tac \\ eq_tac \\ rw []
170 \\ first_x_assum (qspec_then `[]` mp_tac) \\ fs []
171QED
172
173Theorem Ret_11:
174 !x y. Ret x = Ret y <=> x = y
175Proof
176 rw [Ret_def] \\ eq_tac \\ strip_tac \\ fs []
177 \\ metis_tac [itree_rep_ok_Ret,itree_abs_11,Ret_rep_11]
178QED
179
180Theorem Vis_rep_11[local]:
181 !x y g g'. Vis_rep x g = Vis_rep y g' <=> x = y /\ g = g'
182Proof
183 fs [Vis_rep_def,Once FUN_EQ_THM]
184 \\ rpt gen_tac \\ eq_tac \\ simp [] \\ strip_tac
185 \\ first_assum (qspec_then `[]` assume_tac) \\ fs []
186 \\ fs [FUN_EQ_THM] \\ rw []
187 \\ rename [`g x1 x2 = _`]
188 \\ first_x_assum (qspec_then `x1 :: x2` mp_tac) \\ fs []
189QED
190
191Theorem Vis_11:
192 !x f y g. Vis x f = Vis y g <=> x = y /\ f = g
193Proof
194 rw [Vis_def] \\ eq_tac \\ strip_tac \\ fs []
195 \\ qmatch_assum_abbrev_tac `_ x1 = _ x2`
196 \\ `itree_rep_ok x1 /\ itree_rep_ok x2` by
197 (unabbrev_all_tac \\ rw [] \\ match_mp_tac itree_rep_ok_Vis \\ fs [])
198 \\ fs [itree_abs_11] \\ unabbrev_all_tac \\ fs [Vis_rep_11]
199 \\ fs [FUN_EQ_THM,itree_rep_11]
200 \\ fs [GSYM itree_rep_11] \\ fs [FUN_EQ_THM]
201QED
202
203Theorem itree_11 = LIST_CONJ [Ret_11, Vis_11];
204
205
206(* distinctness theorem *)
207
208Theorem itree_all_distinct[local]:
209 !x e g. ALL_DISTINCT [Ret x; Div; Vis e g :('a,'b,'c) itree]
210Proof
211 rw [Ret_def,Div_def,Vis_def]
212 \\ assume_tac itree_rep_ok_Div
213 \\ qspec_then `x` assume_tac itree_rep_ok_Ret
214 \\ qspec_then `t` assume_tac itree_rep_ok_itree_rep
215 \\ qspecl_then [`e`,`itree_rep o g`] mp_tac itree_rep_ok_Vis
216 \\ impl_tac THEN1 fs []
217 \\ rw [] \\ simp [itree_abs_11]
218 \\ rw [] \\ fs [FUN_EQ_THM]
219 \\ qexists_tac `[]` \\ fs [Ret_rep_def,Div_rep_def,Vis_rep_def]
220QED
221
222Theorem itree_distinct = itree_all_distinct
223 |> SIMP_RULE std_ss [ALL_DISTINCT,MEM,GSYM CONJ_ASSOC] |> SPEC_ALL |>
224 CONJUNCTS |> map GEN_ALL |> LIST_CONJ;
225
226
227(* prove cases theorem *)
228
229Theorem rep_exists[local]:
230 itree_rep_ok f ==>
231 (?x. f = Ret_rep x) \/
232 (f = Div_rep) \/
233 ?a g. f = Vis_rep a g /\ !v. itree_rep_ok (g v)
234Proof
235 fs [itree_rep_ok_def] \\ rw []
236 \\ reverse (Cases_on `f []`)
237 THEN1
238 (disj2_tac \\ disj1_tac
239 \\ fs [FUN_EQ_THM]
240 \\ Cases \\ fs [Div_rep_def]
241 \\ first_x_assum match_mp_tac
242 \\ fs [path_ok_def]
243 \\ qexists_tac `[]` \\ fs [])
244 THEN1
245 (disj1_tac
246 \\ qexists_tac ‘r’ \\ fs []
247 \\ fs [FUN_EQ_THM]
248 \\ Cases \\ fs [Ret_rep_def]
249 \\ first_x_assum match_mp_tac
250 \\ fs [path_ok_def]
251 \\ qexists_tac `[]` \\ fs [])
252 \\ rpt disj2_tac
253 \\ fs [Vis_rep_def,FUN_EQ_THM]
254 \\ qexists_tac `e`
255 \\ qexists_tac `\a path. f (a::path)`
256 \\ rw [] THEN1 (Cases_on `x` \\ fs [])
257 \\ first_x_assum match_mp_tac
258 \\ fs [path_ok_def]
259 \\ metis_tac [APPEND,APPEND_ASSOC]
260QED
261
262Theorem itree_cases:
263 !t. (?x. t = Ret x) \/ (t = Div) \/ (?a g. t = Vis a g)
264Proof
265 fs [GSYM itree_rep_11,Ret_def,Div_def,Vis_def] \\ gen_tac
266 \\ qabbrev_tac `f = itree_rep t`
267 \\ `itree_rep_ok f` by fs [Abbr`f`]
268 \\ drule rep_exists \\ strip_tac \\ fs [] \\ rw []
269 \\ imp_res_tac itree_repabs \\ fs []
270 THEN1 metis_tac []
271 \\ rpt disj2_tac
272 \\ qexists_tac `a`
273 \\ qexists_tac `itree_abs o g`
274 \\ qsuff_tac `itree_rep o itree_abs o g = g` THEN1 fs []
275 \\ fs [o_DEF,Once FUN_EQ_THM]
276 \\ metis_tac [itree_repabs]
277QED
278
279
280(* itree_CASE constant *)
281
282Definition itree_CASE[nocompute]:
283 itree_CASE (t:('a,'e,'r) itree) ret div vis =
284 case itree_rep t [] of
285 | Return r => ret r
286 | Stuck => div
287 | Event e => vis e (\a. (itree_abs (\path. itree_rep t (a::path))))
288End
289
290Theorem itree_CASE[compute,allow_rebind]:
291 itree_CASE (Ret r) ret div vis = ret r /\
292 itree_CASE Div ret div vis = div /\
293 itree_CASE (Vis a g) ret div vis = vis a g
294Proof
295 rw [itree_CASE,Ret_def,Div_def,Vis_def]
296 \\ qmatch_goalsub_abbrev_tac `itree_rep (itree_abs xx)`
297 THEN1
298 (`itree_rep_ok xx` by fs [Abbr`xx`,itree_rep_ok_Ret]
299 \\ fs [itree_repabs] \\ unabbrev_all_tac
300 \\ fs [Ret_rep_def])
301 THEN1
302 (`itree_rep_ok xx` by fs [Abbr`xx`,itree_rep_ok_Div]
303 \\ fs [itree_repabs] \\ unabbrev_all_tac
304 \\ fs [Div_rep_def])
305 THEN1
306 (`itree_rep_ok xx` by
307 (fs [Abbr`xx`] \\ match_mp_tac itree_rep_ok_Vis \\ fs [])
308 \\ fs [itree_repabs] \\ unabbrev_all_tac
309 \\ fs [Vis_rep_def]
310 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs [itree_absrep]
311 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs [])
312QED
313
314Theorem itree_CASE_eq:
315 itree_CASE t ret div vis = v <=>
316 (?r. t = Ret r /\ ret r = v) \/
317 (t = Div /\ div = v) \/
318 (?a g. t = Vis a g /\ vis a g = v)
319Proof
320 qspec_then `t` strip_assume_tac itree_cases \\ rw []
321 \\ fs [itree_CASE,itree_11,itree_distinct]
322QED
323
324Theorem itree_CASE_elim:
325 !f.
326 f(itree_CASE t ret div vis) <=>
327 (?r. t = Ret r /\ f(ret r)) \/
328 (t = Div /\ f(div)) \/
329 (?a g. t = Vis a g /\ f(vis a g))
330Proof
331 qspec_then `t` strip_assume_tac itree_cases \\ rw []
332 \\ fs [itree_CASE,itree_11,itree_distinct]
333QED
334
335(* itree unfold *)
336
337Datatype:
338 itree_next = Ret' 'r
339 | Div'
340 | Vis' 'e ('a -> 'seed)
341End
342
343Definition itree_unfold_path_def:
344 (itree_unfold_path f seed [] =
345 case f seed of
346 | Ret' r => Return r
347 | Div' => Stuck
348 | Vis' e g => Event e) /\
349 (itree_unfold_path f seed (n::rest) =
350 case f seed of
351 | Ret' r => Return ARB
352 | Div' => Return ARB
353 | Vis' e g => itree_unfold_path f (g n) rest)
354End
355
356Definition itree_unfold:
357 itree_unfold f seed = itree_abs (itree_unfold_path f seed)
358End
359
360Theorem itree_rep_abs_itree_unfold_path[local]:
361 itree_rep (itree_abs (itree_unfold_path f s)) = itree_unfold_path f s
362Proof
363 fs [GSYM itree_repabs] \\ fs [itree_rep_ok_def]
364 \\ qid_spec_tac `s`
365 \\ Induct_on `path` THEN1 fs [path_ok_def]
366 \\ fs [itree_unfold_path_def]
367 \\ rw [] \\ Cases_on `f s` \\ fs [] \\ rw []
368 \\ first_x_assum match_mp_tac
369 \\ fs [path_ok_def]
370 \\ Cases_on `xs` \\ fs [] \\ rw []
371 \\ fs [itree_unfold_path_def] \\ metis_tac []
372QED
373
374Theorem itree_unfold[allow_rebind]:
375 itree_unfold f seed =
376 case f seed of
377 | Ret' r => Ret r
378 | Div' => Div
379 | Vis' e g => Vis e (itree_unfold f o g)
380Proof
381 Cases_on `f seed` \\ fs []
382 THEN1
383 (fs [itree_unfold,Ret_def] \\ AP_TERM_TAC \\ fs [FUN_EQ_THM]
384 \\ Cases \\ fs [itree_unfold_path_def,Ret_rep_def]
385 \\ Cases_on `h` \\ fs [itree_unfold_path_def,Ret_rep_def])
386 THEN1
387 (fs [itree_unfold,Div_def] \\ AP_TERM_TAC \\ fs [FUN_EQ_THM]
388 \\ Cases \\ fs [itree_unfold_path_def,Div_rep_def]
389 \\ Cases_on `h` \\ fs [itree_unfold_path_def,Div_rep_def])
390 \\ fs [itree_unfold,Vis_def] \\ AP_TERM_TAC \\ fs [FUN_EQ_THM]
391 \\ Cases \\ fs [itree_unfold_path_def,Vis_rep_def]
392 \\ fs [itree_unfold_path_def,Vis_rep_def]
393 \\ fs [itree_unfold,itree_rep_abs_itree_unfold_path]
394QED
395
396
397(* itree_unfold with errors - i.e. the environment can return an error *)
398
399Definition itree_unfold_err_path_def:
400 (itree_unfold_err_path f (rel, err_f, err) seed [] =
401 case f seed of
402 | Ret' r => Return r
403 | Div' => Stuck
404 | Vis' e g => Event e) /\
405 (itree_unfold_err_path f (rel, err_f, err) seed (n::rest) =
406 case f seed of
407 | Ret' r => Return ARB
408 | Div' => Return ARB
409 | Vis' e g =>
410 case n of
411 | INL x => if rest = [] then Return (err_f e x) else Return ARB
412 | INR y =>
413 if rel e y then itree_unfold_err_path f (rel, err_f, err) (g y) rest
414 else if rest = [] then Return $ err e else Return ARB)
415End
416
417Definition itree_unfold_err:
418 itree_unfold_err f err seed =
419 itree_abs (itree_unfold_err_path f err seed)
420End
421
422Theorem itree_rep_abs_itree_unfold_err_path[local]:
423 itree_rep (itree_abs (itree_unfold_err_path f err s)) =
424 itree_unfold_err_path f err s
425Proof
426 gvs[GSYM itree_repabs, itree_rep_ok_def] >>
427 qid_spec_tac `s` >> Induct_on `path` >- gvs[path_ok_def] >>
428 PairCases_on `err` >> gvs[itree_unfold_err_path_def] >> rw[] >>
429 Cases_on ‘f s’ >> fs [] >>
430 rename [‘h::path’] >> Cases_on ‘h’ >> fs []
431 >- gvs[path_ok_def, APPEND_EQ_CONS, itree_unfold_err_path_def] >>
432 reverse IF_CASES_TAC >> fs []
433 >- gvs[path_ok_def, APPEND_EQ_CONS, itree_unfold_err_path_def] >>
434 first_x_assum irule >>
435 gvs [path_ok_def] >>
436 gvs[path_ok_def, APPEND_EQ_CONS, itree_unfold_err_path_def] >>
437 metis_tac []
438QED
439
440Theorem itree_unfold_err[allow_rebind]:
441 itree_unfold_err f (rel, err_f, err) seed =
442 case f seed of
443 | Ret' r => Ret r
444 | Div' => Div
445 | Vis' e g =>
446 Vis e
447 (λa. case a of
448 INL x => Ret $ err_f e x
449 | INR y =>
450 if rel e y then itree_unfold_err f (rel, err_f, err) (g y)
451 else Ret $ err e)
452Proof
453 Cases_on ‘f seed’ >> once_rewrite_tac [itree_unfold_err] >>
454 gvs[Ret_def, Div_def, Vis_def] >> AP_TERM_TAC >> simp[FUN_EQ_THM] >>
455 Cases >> gvs[itree_unfold_err_path_def,Ret_rep_def,Div_rep_def,Vis_rep_def] >>
456 Cases_on ‘h’ >> gvs[itree_rep_abs_itree_unfold_err_path] >>
457 TRY IF_CASES_TAC >> Cases_on ‘t’ >> gvs[itree_rep_abs_itree_unfold_err_path]>>
458 Cases_on ‘f (f' y)’ >> gvs [] >>
459 once_rewrite_tac [itree_unfold_err] >> gvs [] >>
460 once_rewrite_tac [GSYM itree_unfold_err] >> gvs [] >>
461 gvs[Ret_def, Div_def, Vis_def, Ret_rep_def, Div_rep_def, Vis_rep_def] >>
462 DEP_REWRITE_TAC[iffLR itree_repabs] >> simp[] >>
463 gvs[itree_rep_ok_def, path_ok_def, PULL_EXISTS]
464QED
465
466
467(* proving equivalences *)
468
469Definition itree_el_def:
470 itree_el t [] =
471 itree_CASE t (\r. Return r) Stuck (\e g. Event e) /\
472 itree_el t (a::ns) =
473 itree_CASE t (\r. Return ARB) (Return ARB) (\e g. itree_el (g a) ns)
474End
475
476Theorem itree_el_def[allow_rebind]:
477 itree_el (Ret r) [] = Return r /\
478 itree_el Div [] = Stuck /\
479 itree_el (Vis e g) [] = Event e /\
480 itree_el (Ret r) (a::ns) = Return ARB /\
481 itree_el Div (a::ns) = Return ARB /\
482 itree_el (Vis e g) (a::ns) = itree_el (g a) ns
483Proof
484 fs [itree_el_def,itree_CASE]
485QED
486
487Theorem itree_el_eqv:
488 !t1 t2. t1 = t2 <=> !path. itree_el t1 path = itree_el t2 path
489Proof
490 rw [] \\ eq_tac \\ rw []
491 \\ fs [GSYM itree_rep_11,FUN_EQ_THM] \\ rw []
492 \\ pop_assum mp_tac
493 \\ qid_spec_tac `t1` \\ qid_spec_tac `t2`
494 \\ Induct_on `x` \\ rw []
495 \\ `itree_rep_ok (itree_rep t1) /\ itree_rep_ok (itree_rep t2)`
496 by fs [itree_rep_ok_itree_rep]
497 \\ qspec_then `t1` strip_assume_tac itree_cases
498 \\ qspec_then `t2` strip_assume_tac itree_cases
499 \\ rpt BasicProvers.var_eq_tac
500 \\ TRY (first_x_assum (qspec_then `[]` mp_tac)
501 \\ fs [itree_el_def] \\ NO_TAC)
502 \\ first_assum (qspec_then `[]` mp_tac)
503 \\ rewrite_tac [itree_el_def] \\ rw []
504 \\ fs [Vis_def]
505 \\ qmatch_abbrev_tac
506 `itree_rep (itree_abs t1) _ = itree_rep (itree_abs t2) _`
507 \\ `itree_rep_ok t1 /\ itree_rep_ok t2` by
508 (rw [] \\ unabbrev_all_tac
509 \\ TRY (match_mp_tac itree_rep_ok_Vis) \\ fs [])
510 \\ fs [itree_repabs]
511 \\ TRY (unabbrev_all_tac \\ fs [Vis_rep_def] \\ NO_TAC)
512 \\ unabbrev_all_tac \\ fs [GSYM Vis_def]
513 \\ fs [Vis_rep_def] \\ fs []
514 \\ first_x_assum (qspecl_then [`g h`,`g' h`] mp_tac)
515 \\ impl_tac THEN1
516 (rw [] \\ first_x_assum (qspec_then `h::path` mp_tac) \\ fs [itree_el_def])
517 \\ fs [Vis_rep_def]
518QED
519
520Theorem itree_bisimulation:
521 !t1 t2.
522 t1 = t2 <=>
523 ?R. R t1 t2 /\
524 (!x t. R (Ret x) t ==> t = Ret x) /\
525 (!t. R Div t ==> t = Div) /\
526 (!a f t. R (Vis a f) t ==> ?b g. t = Vis a g /\ !s. R (f s) (g s))
527Proof
528 rw [] \\ eq_tac \\ rw []
529 THEN1 (qexists_tac `(=)` \\ fs [itree_11])
530 \\ simp [itree_el_eqv] \\ strip_tac
531 \\ last_x_assum mp_tac \\ qid_spec_tac `t1` \\ qid_spec_tac `t2`
532 \\ Induct_on `path` \\ rw []
533 \\ qspec_then `t1` strip_assume_tac itree_cases
534 \\ qspec_then `t2` strip_assume_tac itree_cases
535 \\ fs [itree_el_def]
536 \\ res_tac \\ fs [itree_11,itree_distinct] \\ rw []
537 \\ Cases_on `h` \\ fs [itree_el_def]
538QED
539
540
541(* register with TypeBase *)
542
543Theorem itree_CASE_cong:
544 !M M' ret div vis ret' div' vis'.
545 M = M' /\
546 (!x. M' = Ret x ==> ret x = ret' x) /\
547 (M' = Div ==> div = div') /\
548 (!a g. M' = Vis a g ==> vis a g = vis' a g) ==>
549 itree_CASE M ret div vis = itree_CASE M' ret' div' vis'
550Proof
551 rw [] \\ qspec_then `M` strip_assume_tac itree_cases
552 \\ rw [] \\ fs [itree_CASE]
553QED
554
555Theorem datatype_itree:
556 DATATYPE ((itree
557 (Ret : 'r -> ('a, 'e, 'r) itree)
558 (Div : ('a, 'e, 'r) itree)
559 (Vis : 'e -> ('a -> ('a, 'e, 'r) itree) -> ('a, 'e, 'r) itree)):bool)
560Proof
561 rw [boolTheory.DATATYPE_TAG_THM]
562QED
563
564val _ = TypeBase.export
565 [TypeBasePure.mk_datatype_info
566 { ax = TypeBasePure.ORIG TRUTH,
567 induction = TypeBasePure.ORIG itree_bisimulation,
568 case_def = itree_CASE,
569 case_cong = itree_CASE_cong,
570 case_eq = itree_CASE_eq,
571 case_elim = itree_CASE_elim,
572 nchotomy = itree_cases,
573 size = NONE,
574 encode = NONE,
575 lift = NONE,
576 one_one = SOME itree_11,
577 distinct = SOME itree_distinct,
578 fields = [],
579 accessors = [],
580 updates = [],
581 destructors = [],
582 recognizers = [] } ]
583
584
585(* tidy up theory exports *)
586
587val _ = List.app Theory.delete_binding
588 ["Ret_rep_def", "Ret_def",
589 "Div_rep_def", "Div_def",
590 "Vis_rep_def", "Vis_def",
591 "path_ok_def", "itree_rep_ok_def",
592 "itree_unfold_path_def", "itree_unfold_path_ind",
593 "itree_unfold_err_path_def", "itree_unfold_err_path_ind",
594 "itree_el_TY_DEF", "itree_absrep", "itree_next_TY_DEF"];
595
596Definition iflat_def:
597iflat itr = itree_unfold (λx. case x of
598 INL(Ret r) =>
599 (case r of
600 Ret r0 => Ret' r0
601 | Div => Div'
602 | Vis e f => Vis' e (λi. INR (f i)))
603 | INL(Div) => Div'
604 | INL(Vis e f) => Vis' e (λi. INL (f i))
605 | INR(Ret r) => Ret' r
606 | INR(Div) => Div'
607 | INR(Vis e f) => Vis' e (λi. INR (f i))
608 ) (INL itr)
609End
610
611Theorem iflat_div[simp]:
612 iflat Div = Div
613Proof
614 simp[itree_unfold, iflat_def]
615QED
616
617Theorem iflat_ret[simp]:
618 iflat (Ret r) = r
619Proof
620 simp[iflat_def,itree_unfold] >> Cases_on ‘r’ >> simp[] >>
621 qmatch_abbrev_tac ‘itree_unfold FF o (λi. INR (g i)) = g’ >> simp[FUN_EQ_THM] >>
622 simp[Once itree_bisimulation] >> gen_tac >>
623 qexists ‘λi1 i2.
624 i1 = itree_unfold FF (INR i2)’ >> rw[]
625 >- gs[itree_unfold, AllCaseEqs(),Abbr ‘FF’]
626 >- gs[itree_unfold, AllCaseEqs(),Abbr ‘FF’]
627 >- (RULE_ASSUM_TAC(SRULE[itree_unfold, AllCaseEqs()]) >> gvs[] >>
628 gvs[Abbr ‘FF’, AllCaseEqs()])
629QED
630
631Theorem iflat_vis[simp]:
632 iflat (Vis ov f) = Vis ov (iflat o f)
633Proof
634 simp[iflat_def,itree_unfold,FUN_EQ_THM] >> gs[iflat_def]
635QED
636
637Theorem iflat_eq_ret[simp]:
638 (iflat itr = Ret rv <=> itr = Ret (Ret rv)) /\ (Ret rv = iflat itr <=> itr = Ret (Ret rv))
639Proof
640 Cases_on ‘itr’ >> rw[] >> metis_tac[]
641QED
642
643Theorem iflat_eq_vis:
644 iflat itr = Vis ov f <=> (? g. itr = Vis ov g /\ iflat o g = f) \/
645 itr = Ret (Vis ov f)
646Proof
647 Cases_on ‘itr’ >> simp[]
648QED
649
650Theorem iflat_eq_div[simp]:
651 iflat itr = Div <=> itr = Div \/ itr = Ret Div
652Proof
653 Cases_on ‘itr’ >> simp[]
654QED
655
656Definition imap_def:
657imap g itr = itree_unfold (λx. case x of
658 Ret r => Ret' (g r)
659 | Div => Div'
660 | Vis e f => Vis' e f
661 ) itr
662End
663
664Theorem imap_ret[simp]:
665 imap g (Ret rv) = Ret (g rv)
666Proof
667 simp[imap_def,itree_unfold]
668QED
669
670Theorem imap_div[simp]:
671 imap g Div = Div
672Proof
673 simp[imap_def,itree_unfold]
674QED
675
676Theorem imap_vis[simp]:
677 imap f (Vis ov g) = Vis ov ((imap f) o g)
678Proof
679 simp[imap_def,itree_unfold,FUN_EQ_THM]
680QED
681
682Theorem imap_eq_ret[simp]:
683 Ret r = imap g itr <=> ?x. itr = Ret x /\ g x = r
684Proof
685 simp[imap_def,itree_unfold,AllCaseEqs()]
686QED
687
688Theorem imap_eq_vis:
689 Vis rv f = imap g itr <=> ?h. itr = Vis rv h /\ imap g o h = f
690Proof
691 simp[imap_def,itree_unfold,AllCaseEqs()] >> simp[itree_unfold, imap_def,FUN_EQ_THM]
692QED
693
694Theorem imap_eq_div[simp]:
695 (imap g itr = Div <=> itr = Div) /\ (Div = imap g itr <=> itr = Div)
696Proof
697 gs[imap_def,itree_unfold,AllCaseEqs()]
698QED
699
700Theorem imap_id:
701 imap (λx. x) itr = itr
702Proof
703 simp[Once itree_bisimulation] >>
704 qexists ‘λ itr1 itr2. itr1 = imap (λx. x) itr2’ >> simp[] >> rw[]
705 >> gvs[imap_eq_vis]
706QED
707
708Theorem imap_composition:
709 imap (f o g) itr = imap f (imap g itr)
710Proof
711 simp[Once itree_bisimulation] >>
712 qexists ‘λi1 i2. ?itr. i2 = imap f (imap g itr) /\ i1 = imap (f o g) itr’
713 >> rw[]
714 >- metis_tac[]
715 >- simp[]
716 >> gvs[imap_eq_vis] >> metis_tac[]
717QED
718
719Overload ireturn = “Ret”
720
721Definition ibind_def:
722 ibind itr f = iflat (imap f itr)
723End
724
725Theorem ibind_left_id:
726 ibind (ireturn itr) f = f itr
727Proof
728 simp[ibind_def]
729QED
730
731Theorem ibind_right_id:
732 ibind itr ireturn = itr
733Proof
734 simp[Once itree_bisimulation] >> qexists ‘λi1 i2. i1 = iflat (imap ireturn i2)’
735 >> rw[iflat_eq_vis]
736 >- simp[ibind_def]
737 >> gvs[imap_eq_vis]
738QED
739
740Theorem ibind_eq_ret:
741 ibind itr f = Ret v <=> ?v'. itr = Ret v' /\ f v' = Ret v
742Proof
743 simp[ibind_def]
744QED
745
746Theorem ibind_eq_div:
747 ibind itr f = Div <=> itr = Div \/ (?x. itr = Ret x /\ f x = Div)
748Proof
749 simp[ibind_def]
750QED
751
752Theorem ibind_eq_vis:
753 ibind itr f = Vis rv g <=> (?h. itr = Vis rv h /\ iflat o imap f o h = g) \/
754 (?x. itr = ireturn x /\ f x = Vis rv g)
755Proof
756 simp[ibind_def,iflat_eq_vis,imap_eq_vis, PULL_EXISTS]
757QED
758
759Theorem ibind_assoc:
760 ibind itr (λx. ibind (f x) g) = ibind (ibind itr f) g
761Proof
762 simp[Once itree_bisimulation] >>
763 qexists ‘λi1 i2. ?itr. i1 = ibind itr (λx. ibind (f x) g) /\ i2 = ibind (ibind itr f) g \/ i1 = i2’
764 >> rw[]
765 >- metis_tac[]
766 >- gvs[ibind_eq_ret]
767 >- gvs[ibind_eq_div,ibind_eq_ret]
768 >> gvs[ibind_eq_vis,ibind_eq_ret] >> simp[GSYM ibind_def] >> metis_tac[]
769QED
770
771Inductive iset:
772[~ret:]
773 !e. iset (Ret e) e
774[~vis:]
775 iset (f i) e ==> iset (Vis ov f) e
776End
777
778Theorem iset_thm[simp]:
779 (iset (Ret e) e' <=> e = e') /\
780 (iset Div e = F) /\
781 (iset (Vis ov f) e <=> ?i. iset (f i) e)
782Proof
783 rpt strip_tac >> simp[Once iset_cases]
784QED
785
786Inductive ifinite:
787[~ret:]
788 ifinite (Ret e)
789[~div:]
790 ifinite Div
791[~vis:]
792 (! iv. ifinite (f iv)) ==> ifinite (Vis ov f)
793End
794
795Definition itruncate_def:
796 itruncate 0 itr = Div /\
797 itruncate n Div = Div /\
798 itruncate n (Ret rv) = Ret rv /\
799 itruncate n (Vis ov f) = Vis ov (λx. itruncate (n-1) (f x))
800End
801
802Theorem itruncate_ret[simp]:
803 !n. itruncate n itr = Ret r <=> (itr = Ret r /\ n <> 0)
804Proof
805 strip_tac >> eq_tac >> rpt strip_tac
806 >- (Cases_on ‘itr’ >> Cases_on ‘n’ >> gs[itruncate_def])
807 >> gvs[itruncate_def] >> Cases_on ‘n’ >> simp[itruncate_def]
808QED
809
810Theorem itruncate_implies_ifinite:
811 !itr. itruncate n itr = itr ==> ifinite itr
812Proof
813 Induct_on ‘n’ >- gs[itruncate_def,ifinite_div] >> Cases_on ‘itr’ >- simp[ifinite_ret]
814 >- simp[ifinite_div] >> rw[] >> gs[itruncate_def,FUN_EQ_THM] >> gs[ifinite_vis]
815QED
816
817Theorem iset_truncate:
818 iset itr elem ==> ? n. iset (itruncate n itr) elem
819Proof
820 Induct_on ‘iset’ >> rw[] >- metis_tac[itruncate_def,iset_ret] >>
821 qexists ‘SUC n’ >> simp[itruncate_def] >> metis_tac[iset_vis]
822QED
823
824Theorem iset_flat_1:
825 ! itr e. iset (iflat itr) e ==> ?t0. iset itr t0 /\ iset t0 e
826Proof
827 Induct_on ‘iset’ >> rpt strip_tac >> gvs[iflat_eq_vis] >> metis_tac[]
828QED
829
830Theorem iset_flat_2:
831 ! itr t0 e. iset itr t0 /\ iset t0 e ==> iset (iflat itr) e
832Proof
833 Induct_on ‘iset’ >> rw[] >> metis_tac[]
834QED
835
836Theorem iset_flat:
837 ! itr e. iset (iflat itr) e <=> ?t0. iset itr t0 /\ iset t0 e
838Proof
839 metis_tac[iset_flat_1,iset_flat_2]
840QED
841
842Theorem iset_map_1:
843 ! itr x. iset (imap f itr) x ==> ?y. x = f y /\ iset itr y
844Proof
845 Induct_on ‘iset’ >> rpt strip_tac >> gvs[imap_eq_vis] >> metis_tac[]
846QED
847
848Theorem iset_map_2:
849 ! itr. iset itr y ==> iset (imap f itr) (f y)
850Proof
851 Induct_on ‘iset’ >> rpt strip_tac >> simp[] >> metis_tac[]
852QED
853
854Theorem iset_map:
855 iset (imap f itr) = IMAGE f (iset itr)
856Proof
857 simp[pred_setTheory.EXTENSION] >> simp[IN_DEF] >> metis_tac[iset_map_1,iset_map_2]
858QED
859
860Inductive at_path:
861[~ret:]
862 at_path (Ret e) [] e
863[~vis:]
864 (at_path (f i) p e ==> at_path (Vis ov f) ((ov,i)::p) e)
865End
866
867Theorem at_path_thm[simp]:
868 (at_path Div p e = F) /\
869 (at_path (Ret e) p a <=> (p = [] /\ a = e)) /\
870 (at_path (Vis ov f) p e <=> ?i l. (p = (ov,i)::l /\ at_path (f i) l e))
871Proof
872 rpt strip_tac >> simp[Once at_path_cases] >- metis_tac[]
873QED
874
875Theorem at_path_implies_iset:
876 at_path itree p e ==> iset itree e
877Proof
878 Induct_on ‘at_path’ >> rpt strip_tac >> simp[] >> metis_tac[]
879QED
880
881Theorem iset_iff_exists_path:
882 iset itree e <=> ?p. at_path itree p e
883Proof
884 eq_tac >> simp[at_path_implies_iset] >> Induct_on ‘iset’ >> rpt strip_tac
885 >> metis_tac[at_path_thm]
886QED
887
888CoInductive ievery:
889[~div:]
890 (ievery P Div)
891[~ret:]
892 (P e ==> ievery P (Ret e))
893[~vis:]
894 ((! iv. ievery P (f iv)) ==> ievery P (Vis ov f))
895End
896
897Theorem ievery_thm[simp]:
898 (ievery P Div = T) /\
899 (ievery P (Ret e) <=> P e) /\
900 (ievery P (Vis ov f) <=> ! iv. ievery P (f iv))
901Proof
902 rpt strip_tac >> simp[Once ievery_cases]
903QED
904
905Inductive iexists:
906[~ret:]
907 (P e ==> iexists P (Ret e))
908[~vis:]
909 (? iv. iexists P (f iv)) ==> iexists P (Vis ov f)
910End
911
912Theorem iexists_thm[simp]:
913 (iexists P Div = F) /\
914 (iexists P (Ret e) <=> P e) /\
915 (iexists P (Vis ov f) <=> ? iv. iexists P (f iv))
916Proof
917 rpt strip_tac >> simp[Once iexists_cases]
918QED
919
920Theorem not_ievery_exists:
921 ~ ievery P itr <=> iexists (λx. ~ P x) itr
922Proof
923 eq_tac
924 >- (CONV_TAC CONTRAPOS_CONV >> simp[] >> qid_spec_tac ‘itr’ >> ho_match_mp_tac ievery_coind
925 >> rw[] >> Cases_on ‘itr’ >> gs[])
926 >> Induct_on ‘iexists’ >> simp[] >> metis_tac[]
927QED
928
929Theorem ievery_set:
930 ! itr. ievery P itr <=> ! rv. (iset itr rv ==> P rv)
931Proof
932 simp[EQ_IMP_THM, FORALL_AND_THM] >> strip_tac
933 >- (gen_tac >> CONV_TAC CONTRAPOS_CONV >> simp[PULL_EXISTS] >> Induct_on ‘iset’ >> simp[]
934 >> metis_tac[])
935 >> ho_match_mp_tac ievery_coind >> rw[] >> Cases_on ‘itr’ >> gs[] >> metis_tac[]
936QED
937
938Theorem iexists_set = not_ievery_exists |> SYM |> Q.INST [‘P’ |-> ‘λx. ~ P x’]
939 |> SRULE[SF ETA_ss,ievery_set]
940
941