itreeTauScript.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; Tau is the silent action; Vis is a visible event that
13 returns a value that the rest of the interaction tree can depend on.
14
15 ('a,'e,'r) itree =
16 Ret 'r -- termination with result 'r
17 | Tau (('a,'e,'r) itree) -- a silent action, then continue
18 | Vis 'e ('a -> ('a,'e,'r) itree) -- visible event 'e with answer 'a,
19 then continue based on answer
20*)
21
22Theory itreeTau
23Ancestors
24 arithmetic list llist alist option pred_set relation pair
25 combin itree companion fixedPoint set_relation
26Libs
27 term_tactic mp_then
28
29(* make type definition *)
30
31Datatype:
32 itree_el = Event 'e | Return 'r | Silence
33End
34
35Type itree_rep[local] = “:('a option) list -> ('e,'r) itree_el”;
36val f = “(f: ('a,'e,'r) itree_rep)”
37
38Definition path_ok_def:
39 path_ok path ^f <=>
40 !xs y ys.
41 path = xs ++ y::ys ==>
42 case f xs of
43 | Return _ => F (* a path cannot continue past a Return *)
44 | Silence => y = NONE (* Silence consumes no input *)
45 | Event e => IS_SOME y (* the next element must be an input *)
46End
47
48Definition itree_rep_ok_def:
49 itree_rep_ok ^f <=>
50 (* every bad path leads to the Silence element *)
51 !path. ~path_ok path f ==> f path = Silence
52End
53
54Theorem type_inhabited[local]:
55 ?f. itree_rep_ok ^f
56Proof
57 qexists_tac ‘\p. Silence’ \\ fs [itree_rep_ok_def]
58QED
59
60val itree_tydef = new_type_definition ("itree", type_inhabited);
61
62val repabs_fns = define_new_type_bijections
63 { name = "itree_absrep",
64 ABS = "itree_abs",
65 REP = "itree_rep",
66 tyax = itree_tydef};
67
68
69(* prove basic theorems about rep and abs fucntions *)
70
71val itree_absrep = CONJUNCT1 repabs_fns
72val itree_repabs = CONJUNCT2 repabs_fns
73
74Theorem itree_rep_ok_itree_rep[local,simp]:
75 !t. itree_rep_ok (itree_rep t)
76Proof
77 fs [itree_repabs, itree_absrep]
78QED
79
80Theorem itree_abs_11[local]:
81 itree_rep_ok r1 /\ itree_rep_ok r2 ==>
82 (itree_abs r1 = itree_abs r2 <=> r1 = r2)
83Proof
84 fs [itree_repabs, EQ_IMP_THM] \\ metis_tac []
85QED
86
87Theorem itree_rep_11[local]:
88 (itree_rep t1 = itree_rep t2) = (t1 = t2)
89Proof
90 fs [EQ_IMP_THM] \\ metis_tac [itree_absrep]
91QED
92
93
94(* define constructors *)
95
96Definition Ret_rep_def:
97 Ret_rep (x:'r) =
98 \path. if path = [] then Return x else Silence
99End
100
101Definition Tau_rep_def:
102 Tau_rep ^f =
103 \path. case path of
104 | (NONE::rest) => f rest
105 | _ => Silence
106End
107
108Definition Vis_rep_def:
109 Vis_rep e g =
110 \path. case path of
111 | [] => Event e
112 | (NONE::rest) => Silence
113 | (SOME a::rest) => g a rest
114End
115
116Definition Ret_def:
117 Ret x = itree_abs (Ret_rep x)
118End
119
120Definition Tau_def:
121 Tau t = itree_abs (Tau_rep (itree_rep t))
122End
123
124Definition Vis_def:
125 Vis e g = itree_abs (Vis_rep e (itree_rep o g))
126End
127
128Theorem itree_rep_ok_Ret[local]:
129 !x. itree_rep_ok (Ret_rep x : ('a,'e,'r) itree_rep)
130Proof
131 fs [itree_rep_ok_def,Ret_rep_def]
132 \\ rw [] \\ fs [path_ok_def]
133QED
134
135Theorem itree_rep_ok_Tau[local]:
136 !f. itree_rep_ok f ==> itree_rep_ok (Tau_rep ^f)
137Proof
138 fs [itree_rep_ok_def,Tau_rep_def]
139 \\ rw [] \\ CCONTR_TAC \\ fs [AllCaseEqs()]
140 \\ Cases_on ‘path’ \\ fs []
141 \\ Cases_on ‘h’ \\ fs [] \\ rw []
142 \\ qpat_x_assum ‘~(path_ok _ _)’ mp_tac \\ fs []
143 \\ simp [path_ok_def] \\ rw []
144 \\ rename [‘NONE :: t = path ++ [y] ++ ys’]
145 \\ Cases_on ‘path’ \\ fs [] \\ rw []
146 \\ rename [‘xs ++ [y] ++ ys’]
147 \\ first_x_assum (qspec_then ‘xs ++ [y] ++ ys’ mp_tac)
148 \\ fs [] \\ rw [] \\ fs [path_ok_def]
149QED
150
151Theorem itree_rep_ok_Vis[local]:
152 !a g. (!a. itree_rep_ok (g a)) ==> itree_rep_ok (Vis_rep e g)
153Proof
154 fs [itree_rep_ok_def,Vis_rep_def]
155 \\ rw [] \\ CCONTR_TAC \\ fs [AllCaseEqs()]
156 \\ Cases_on ‘path’ \\ fs [] THEN1 fs [path_ok_def]
157 \\ Cases_on ‘h’ \\ fs [] \\ rw []
158 \\ qpat_x_assum ‘~(path_ok _ _)’ mp_tac \\ fs []
159 \\ simp [path_ok_def] \\ rw []
160 \\ rename [‘SOME _ :: _ = path ++ [y] ++ ys’]
161 \\ Cases_on ‘path’ \\ fs [] \\ rw []
162 \\ rename [‘xs ++ [y] ++ ys’]
163 \\ first_x_assum (qspecl_then [‘x’,‘xs ++ [y] ++ ys’] mp_tac)
164 \\ fs [] \\ rw [] \\ fs [path_ok_def]
165QED
166
167
168(* prove injectivity *)
169
170Theorem Ret_rep_11[local]:
171 !x y. Ret_rep x = Ret_rep y <=> x = y
172Proof
173 fs [Ret_rep_def,FUN_EQ_THM]
174 \\ rpt gen_tac \\ eq_tac \\ rw []
175 \\ first_x_assum (qspec_then ‘[]’ mp_tac) \\ fs []
176QED
177
178Theorem Ret_11:
179 !x y. Ret x = Ret y <=> x = y
180Proof
181 rw [Ret_def] \\ eq_tac \\ strip_tac \\ fs []
182 \\ metis_tac [itree_rep_ok_Ret,itree_abs_11,Ret_rep_11]
183QED
184
185Theorem Tau_rep_11[local]:
186 !x y. Tau_rep x = Tau_rep y <=> x = y
187Proof
188 fs [Tau_rep_def,Once FUN_EQ_THM]
189 \\ rpt gen_tac \\ eq_tac \\ rw []
190 \\ fs [FUN_EQ_THM] \\ strip_tac
191 \\ rename [‘_ path = _’]
192 \\ first_x_assum (qspec_then ‘NONE::path’ mp_tac) \\ fs []
193QED
194
195Theorem Tau_11:
196 !x y. Tau x = Tau y <=> x = y
197Proof
198 rw [Tau_def] \\ eq_tac \\ strip_tac \\ fs []
199 \\ qspec_then ‘x’ assume_tac itree_rep_ok_itree_rep
200 \\ drule itree_rep_ok_Tau
201 \\ qspec_then ‘y’ assume_tac itree_rep_ok_itree_rep
202 \\ drule itree_rep_ok_Tau \\ rw []
203 \\ fs [itree_abs_11,Tau_rep_11,itree_rep_11]
204QED
205
206Theorem Vis_rep_11[local]:
207 !x y g g'. Vis_rep x g = Vis_rep y g' <=> x = y /\ g = g'
208Proof
209 fs [Vis_rep_def,Once FUN_EQ_THM]
210 \\ rpt gen_tac \\ eq_tac \\ simp [] \\ strip_tac
211 \\ first_assum (qspec_then ‘[]’ assume_tac) \\ fs []
212 \\ fs [FUN_EQ_THM] \\ rw []
213 \\ rename [‘g x1 x2 = _’]
214 \\ first_x_assum (qspec_then ‘SOME x1 :: x2’ mp_tac) \\ fs []
215QED
216
217Theorem Vis_11:
218 !x f y g. Vis x f = Vis y g <=> x = y /\ f = g
219Proof
220 rw [Vis_def] \\ eq_tac \\ strip_tac \\ fs []
221 \\ qmatch_assum_abbrev_tac ‘_ x1 = _ x2’
222 \\ ‘itree_rep_ok x1 /\ itree_rep_ok x2’ by
223 (unabbrev_all_tac \\ rw [] \\ match_mp_tac itree_rep_ok_Vis \\ fs [])
224 \\ fs [itree_abs_11] \\ unabbrev_all_tac \\ fs [Vis_rep_11]
225 \\ fs [FUN_EQ_THM,itree_rep_11]
226 \\ fs [GSYM itree_rep_11] \\ fs [FUN_EQ_THM]
227QED
228
229Theorem itree_11 = LIST_CONJ [Ret_11, Tau_11, Vis_11];
230
231
232(* distinctness theorem *)
233
234Theorem itree_distinct_lemma[local]:
235 ALL_DISTINCT [Ret x; Tau t; Vis e g]
236Proof
237 fs [ALL_DISTINCT,Ret_def,Tau_def,Vis_def]
238 \\ qpat_abbrev_tac ‘xx = Ret_rep x’
239 \\ ‘itree_rep_ok xx’ by fs [Abbr‘xx’,itree_rep_ok_Ret]
240 \\ fs [Abbr‘xx’]
241 \\ qspec_then ‘x’ assume_tac itree_rep_ok_Ret
242 \\ qspec_then ‘t’ assume_tac itree_rep_ok_itree_rep
243 \\ drule itree_rep_ok_Tau
244 \\ qspecl_then [‘e’,‘itree_rep o g’] mp_tac itree_rep_ok_Vis
245 \\ impl_tac THEN1 fs []
246 \\ rpt (disch_then assume_tac)
247 \\ simp [itree_abs_11]
248 \\ rw [] \\ fs [FUN_EQ_THM]
249 \\ qexists_tac ‘[]’ \\ fs [Ret_rep_def,Tau_rep_def,Vis_rep_def]
250QED
251
252Theorem itree_distinct =
253 itree_distinct_lemma |> SIMP_RULE std_ss [ALL_DISTINCT,MEM,GSYM CONJ_ASSOC];
254
255
256(* prove cases theorem *)
257
258Theorem rep_exists[local]:
259 itree_rep_ok f ==>
260 (?x. f = Ret_rep x) \/
261 (?u. f = Tau_rep u /\ itree_rep_ok u) \/
262 ?a g. f = Vis_rep a g /\ !v. itree_rep_ok (g v)
263Proof
264 fs [itree_rep_ok_def] \\ rw []
265 \\ reverse (Cases_on ‘f []’)
266 THEN1
267 (disj2_tac \\ disj1_tac
268 \\ fs [Tau_rep_def,FUN_EQ_THM]
269 \\ qexists_tac ‘\path. f (NONE::path)’
270 \\ rw [] THEN1
271 (Cases_on ‘x’ \\ fs []
272 \\ Cases_on ‘h’ \\ fs []
273 \\ first_x_assum match_mp_tac
274 \\ fs [path_ok_def]
275 \\ qexists_tac ‘[]’ \\ fs [])
276 \\ first_x_assum match_mp_tac
277 \\ fs [path_ok_def] \\ rw []
278 \\ metis_tac [APPEND,APPEND_ASSOC])
279 THEN1
280 (disj1_tac
281 \\ fs [Ret_rep_def,FUN_EQ_THM]
282 \\ qexists_tac ‘r’ \\ rw []
283 \\ first_x_assum match_mp_tac
284 \\ fs [path_ok_def] \\ rw []
285 \\ Cases_on ‘x'’ \\ fs []
286 \\ qexists_tac ‘[]’ \\ fs [])
287 \\ rpt disj2_tac
288 \\ fs [Vis_rep_def,FUN_EQ_THM]
289 \\ qexists_tac ‘e’
290 \\ qexists_tac ‘\a path. f (SOME a::path)’
291 \\ rw [] THEN1
292 (Cases_on ‘x’ \\ fs []
293 \\ Cases_on ‘h’ \\ fs []
294 \\ first_x_assum match_mp_tac
295 \\ fs [path_ok_def]
296 \\ qexists_tac ‘[]’ \\ fs [])
297 \\ first_x_assum match_mp_tac
298 \\ fs [path_ok_def]
299 \\ metis_tac [APPEND,APPEND_ASSOC]
300QED
301
302Theorem itree_cases:
303 !t. (?x. t = Ret x) \/ (?u. t = Tau u) \/ (?a g. t = Vis a g)
304Proof
305 fs [GSYM itree_rep_11,Ret_def,Tau_def,Vis_def] \\ gen_tac
306 \\ qabbrev_tac ‘f = itree_rep t’
307 \\ ‘itree_rep_ok f’ by fs [Abbr‘f’]
308 \\ drule rep_exists \\ strip_tac \\ fs [] \\ rw []
309 \\ imp_res_tac itree_repabs \\ fs []
310 THEN1 metis_tac [] THEN1 metis_tac []
311 \\ rpt disj2_tac
312 \\ qexists_tac ‘a’
313 \\ qexists_tac ‘itree_abs o g’
314 \\ qsuff_tac ‘itree_rep o itree_abs o g = g’ THEN1 fs []
315 \\ fs [o_DEF,Once FUN_EQ_THM]
316 \\ metis_tac [itree_repabs]
317QED
318
319
320(* itree_CASE constant *)
321
322Definition itree_CASE[nocompute]:
323 itree_CASE (t:('a,'e,'r) itree) ret tau vis =
324 case itree_rep t [] of
325 | Return r => ret r
326 | Silence => tau (itree_abs (\path. itree_rep t (NONE::path)))
327 | Event e => vis e (\a. (itree_abs (\path. itree_rep t (SOME a::path))))
328End
329
330Theorem itree_CASE[compute,allow_rebind]:
331 itree_CASE (Ret r) ret tau vis = ret r /\
332 itree_CASE (Tau t) ret tau vis = tau t /\
333 itree_CASE (Vis a g) ret tau vis = vis a g
334Proof
335 rw [itree_CASE,Ret_def,Vis_def,Tau_def]
336 \\ qmatch_goalsub_abbrev_tac ‘itree_rep (itree_abs xx)’
337 THEN1
338 (‘itree_rep_ok xx’ by fs [Abbr‘xx’,itree_rep_ok_Ret]
339 \\ fs [itree_repabs] \\ unabbrev_all_tac
340 \\ fs [Ret_rep_def])
341 THEN1
342 (‘itree_rep_ok xx’ by
343 (fs [Abbr‘xx’] \\ match_mp_tac itree_rep_ok_Tau \\ fs [])
344 \\ fs [itree_repabs] \\ unabbrev_all_tac
345 \\ fs [Tau_rep_def]
346 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs [itree_absrep])
347 THEN1
348 (‘itree_rep_ok xx’ by
349 (fs [Abbr‘xx’] \\ match_mp_tac itree_rep_ok_Vis \\ fs [])
350 \\ fs [itree_repabs] \\ unabbrev_all_tac
351 \\ fs [Vis_rep_def]
352 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs [itree_absrep]
353 \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs [])
354QED
355
356Theorem itree_CASE_eq:
357 itree_CASE t ret tau vis = v <=>
358 (?r. t = Ret r /\ ret r = v) \/
359 (?u. t = Tau u /\ tau u = v) \/
360 (?a g. t = Vis a g /\ vis a g = v)
361Proof
362 qspec_then ‘t’ strip_assume_tac itree_cases \\ rw []
363 \\ fs [itree_CASE,itree_11,itree_distinct]
364QED
365
366Theorem itree_CASE_elim:
367 !f.
368 f(itree_CASE t ret tau vis) <=>
369 (?r. t = Ret r /\ f(ret r)) \/
370 (?u. t = Tau u /\ f(tau u)) \/
371 (?a g. t = Vis a g /\ f(vis a g))
372Proof
373 qspec_then ‘t’ strip_assume_tac itree_cases \\ rw []
374 \\ fs [itree_CASE,itree_11,itree_distinct]
375QED
376
377(* itree unfold *)
378
379Datatype:
380 itree_next = Ret' 'r
381 | Tau' 'seed
382 | Vis' 'e ('a -> 'seed)
383End
384
385Definition itree_unfold_path_def:
386 (itree_unfold_path f seed [] =
387 case f seed of
388 | Ret' r => Return r
389 | Tau' s => Silence
390 | Vis' e g => Event e) /\
391 (itree_unfold_path f seed (NONE::rest) =
392 case f seed of
393 | Ret' r => Silence
394 | Tau' s => itree_unfold_path f s rest
395 | Vis' e g => Silence) /\
396 (itree_unfold_path f seed (SOME n::rest) =
397 case f seed of
398 | Ret' r => Silence
399 | Tau' s => Silence
400 | Vis' e g => itree_unfold_path f (g n) rest)
401End
402
403Definition itree_unfold:
404 itree_unfold f seed = itree_abs (itree_unfold_path f seed)
405End
406
407Theorem itree_rep_abs_itree_unfold_path[local]:
408 itree_rep (itree_abs (itree_unfold_path f s)) = itree_unfold_path f s
409Proof
410 fs [GSYM itree_repabs] \\ fs [itree_rep_ok_def]
411 \\ qid_spec_tac ‘s’
412 \\ Induct_on ‘path’ THEN1 fs [path_ok_def]
413 \\ Cases_on ‘h’ \\ fs [itree_unfold_path_def]
414 THEN1
415 (rw [] \\ Cases_on ‘f s’ \\ fs [] \\ rw []
416 \\ first_x_assum match_mp_tac
417 \\ fs [path_ok_def]
418 \\ Cases_on ‘xs’ \\ fs [] \\ rw []
419 THEN1 (rfs [itree_unfold_path_def])
420 \\ fs [itree_unfold_path_def] \\ metis_tac [])
421 \\ rw [] \\ Cases_on ‘f s’ \\ fs [] \\ rw []
422 \\ first_x_assum match_mp_tac
423 \\ fs [path_ok_def]
424 \\ Cases_on ‘xs’ \\ fs [] \\ rw []
425 THEN1 (rfs [itree_unfold_path_def])
426 \\ fs [itree_unfold_path_def] \\ metis_tac []
427QED
428
429Theorem itree_unfold[allow_rebind]:
430 itree_unfold f seed =
431 case f seed of
432 | Ret' r => Ret r
433 | Tau' s => Tau (itree_unfold f s)
434 | Vis' e g => Vis e (itree_unfold f o g)
435Proof
436 Cases_on ‘f seed’ \\ fs []
437 THEN1
438 (fs [itree_unfold,Ret_def] \\ AP_TERM_TAC \\ fs [FUN_EQ_THM]
439 \\ Cases \\ fs [itree_unfold_path_def,Ret_rep_def]
440 \\ Cases_on ‘h’ \\ fs [itree_unfold_path_def,Ret_rep_def])
441 THEN1
442 (fs [itree_unfold,Tau_def] \\ AP_TERM_TAC \\ fs [FUN_EQ_THM]
443 \\ Cases \\ fs [itree_unfold_path_def,Tau_rep_def]
444 \\ Cases_on ‘h’ \\ fs [itree_unfold_path_def,Tau_rep_def]
445 \\ fs [itree_rep_abs_itree_unfold_path])
446 \\ fs [itree_unfold,Vis_def] \\ AP_TERM_TAC \\ fs [FUN_EQ_THM]
447 \\ Cases \\ fs [itree_unfold_path_def,Vis_rep_def]
448 \\ Cases_on ‘h’ \\ fs [itree_unfold_path_def,Vis_rep_def]
449 \\ fs [itree_unfold,itree_rep_abs_itree_unfold_path]
450QED
451
452(* proving equivalences *)
453
454Theorem itree_el_thm[simp,compute]:
455 itree_rep (Ret r) [] = Return r /\
456 itree_rep (Tau t) [] = Silence /\
457 itree_rep (Vis e g) [] = Event e /\
458 itree_rep (Ret r) (NONE::ns) = Silence /\
459 itree_rep (Tau t) (NONE::ns) = itree_rep t ns /\
460 itree_rep (Vis e g) (NONE::ns) = Silence /\
461 itree_rep (Ret r) (SOME a::ns) = Silence /\
462 itree_rep (Tau t) (SOME a::ns) = Silence /\
463 itree_rep (Vis e g) (SOME a::ns) = itree_rep (g a) ns
464Proof
465 rw[Ret_def, Tau_def, Vis_def]
466 \\ qmatch_goalsub_abbrev_tac `itree_rep (itree_abs tt)`
467 \\ `itree_rep_ok tt` by rw[Abbr`tt`, itree_rep_ok_Ret, itree_rep_ok_Tau, itree_rep_ok_Vis]
468 \\ dxrule_then strip_assume_tac $ iffLR itree_repabs
469 \\ rw[Abbr`tt`, Ret_rep_def, Tau_rep_def, Vis_rep_def]
470QED
471
472Theorem itree_bisimulation:
473 !t1 t2.
474 t1 = t2 <=>
475 ?R. R t1 t2 /\
476 (!x t. R (Ret x) t ==> t = Ret x) /\
477 (!u t. R (Tau u) t ==> ?v. t = Tau v /\ R u v) /\
478 (!a f t. R (Vis a f) t ==> ?g. t = Vis a g /\ !s. R (f s) (g s))
479Proof
480 rw [] \\ eq_tac \\ rw []
481 THEN1 (qexists_tac ‘(=)’ \\ fs [itree_11])
482 \\ rw [GSYM itree_rep_11, FUN_EQ_THM] \\ rename[`itree_rep t1 path`]
483 \\ last_x_assum mp_tac \\ qid_spec_tac ‘t1’ \\ qid_spec_tac ‘t2’
484 \\ Induct_on ‘path’ \\ rw []
485 \\ qspec_then ‘t1’ strip_assume_tac itree_cases
486 \\ qspec_then ‘t2’ strip_assume_tac itree_cases
487 \\ fs []
488 \\ res_tac \\ fs [itree_11,itree_distinct] \\ rw[]
489 \\ Cases_on ‘h’ \\ fs []
490QED
491
492Theorem itree_strong_bisimulation:
493 !t1 t2.
494 t1 = t2 <=>
495 ?R. R t1 t2 /\
496 (!x t. R (Ret x) t ==> t = Ret x) /\
497 (!u t. R (Tau u) t ==> ?v. t = Tau v /\ (R u v \/ u = v)) /\
498 (!a f t. R (Vis a f) t ==> ?g. t = Vis a g /\
499 !s. R (f s) (g s) \/ f s = g s)
500Proof
501 rpt strip_tac >>
502 EQ_TAC
503 >- (strip_tac >> first_x_assum $ irule_at $ Pos hd >> metis_tac[]) >>
504 strip_tac >>
505 ONCE_REWRITE_TAC[itree_bisimulation] >>
506 qexists_tac ‘\x y. R x y \/ x = y’ >>
507 metis_tac[]
508QED
509
510(* register with TypeBase *)
511
512Theorem itree_CASE_cong:
513 !M M' ret tau vis ret' tau' vis'.
514 M = M' /\
515 (!x. M' = Ret x ==> ret x = ret' x) /\
516 (!t. M' = Tau t ==> tau t = tau' t) /\
517 (!a g. M' = Vis a g ==> vis a g = vis' a g) ==>
518 itree_CASE M ret tau vis = itree_CASE M' ret' tau' vis'
519Proof
520 rw [] \\ qspec_then ‘M’ strip_assume_tac itree_cases
521 \\ rw [] \\ fs [itree_CASE]
522QED
523
524Theorem datatype_itree:
525 DATATYPE ((itree
526 (Ret : 'r -> ('a, 'e, 'r) itree)
527 (Tau : ('a, 'e, 'r) itree -> ('a, 'e, 'r) itree)
528 (Vis : 'e -> ('a -> ('a, 'e, 'r) itree) -> ('a, 'e, 'r) itree)):bool)
529Proof
530 rw [boolTheory.DATATYPE_TAG_THM]
531QED
532
533val _ = TypeBase.export
534 [TypeBasePure.mk_datatype_info
535 { ax = TypeBasePure.ORIG TRUTH,
536 induction = TypeBasePure.ORIG itree_bisimulation,
537 case_def = itree_CASE,
538 case_cong = itree_CASE_cong,
539 case_eq = itree_CASE_eq,
540 case_elim = itree_CASE_elim,
541 nchotomy = itree_cases,
542 size = NONE,
543 encode = NONE,
544 lift = NONE,
545 one_one = SOME itree_11,
546 distinct = SOME itree_distinct,
547 fields = [],
548 accessors = [],
549 updates = [],
550 destructors = [],
551 recognizers = [] } ]
552
553Overload "case" = “itree_CASE”
554
555(* itree combinators *)
556
557Definition itree_bind_def:
558 itree_bind t k =
559 itree_unfold
560 (λx.
561 case x of
562 INL(Ret r) =>
563 (case k r of
564 Ret s =>
565 Ret' s
566 | Tau t =>
567 Tau' (INR t)
568 | Vis e g =>
569 Vis' e (INR o g))
570 | INL(Vis e g) => Vis' e (INL o g)
571 | INL(Tau t) => Tau' (INL t)
572 | INR(Ret r) => Ret' r
573 | INR(Vis e g) => Vis' e (INR o g)
574 | INR(Tau t) => Tau' (INR t)
575 )
576 (INL t)
577End
578
579Theorem itree_unfold_bind_INR[local]:
580 itree_unfold
581 (λx.
582 case x of
583 INL (Ret r) =>
584 itree_CASE (k r) (λs. Ret' s) (λt. Tau' (INR t))
585 (λe g. Vis' e (INR o g))
586 | INL (Tau t) => Tau' (INL t)
587 | INL (Vis e g) => Vis' e (INL o g)
588 | INR (Ret r') => Ret' r'
589 | INR (Tau t') => Tau' (INR t')
590 | INR (Vis e' g') => Vis' e' (INR o g')) (INR u) =
591 u
592Proof
593 rw[Once itree_bisimulation] >>
594 qexists_tac ‘λx y. (x =
595 itree_unfold (λx.
596 case x of
597 INL (Ret r) =>
598 itree_CASE (k r) (λs. Ret' s) (λt. Tau' (INR t))
599 (λe g. Vis' e (INR o g))
600 | INL (Tau t) => Tau' (INL t)
601 | INL (Vis e g) => Vis' e (INL o g)
602 | INR (Ret r') => Ret' r'
603 | INR (Tau t') => Tau' (INR t')
604 | INR (Vis e' g') => Vis' e' (INR o g')) (INR y))’ >>
605 rw[] >>
606 Cases_on ‘t’ >>
607 first_x_assum (strip_assume_tac o ONCE_REWRITE_RULE[itree_unfold]) >>
608 gvs[] >>
609 rw[Once itree_unfold] >>
610 gvs[]
611QED
612
613Theorem itree_bind_thm[simp]:
614 itree_bind (Ret r) k = k r /\
615 itree_bind (Tau t) k = Tau (itree_bind t k) /\
616 itree_bind (Vis e k') k = Vis e (λx. itree_bind (k' x) k)
617Proof
618 rw[itree_bind_def]
619 >- (rw[Once itree_unfold] >>
620 Cases_on ‘k r’ >> rw[] >>
621 rw[itree_unfold_bind_INR,FUN_EQ_THM]) >>
622 rw[Once itree_unfold,FUN_EQ_THM]
623QED
624
625Theorem itree_bind_right_identity[simp]:
626 itree_bind t Ret = t
627Proof
628 rw[Once itree_bisimulation] >>
629 qexists_tac ‘λx y. (x = itree_bind y Ret)’ >>
630 rw[] >>
631 Cases_on ‘t’ >>
632 gvs[itree_bind_thm]
633QED
634
635Theorem itree_bind_assoc:
636 itree_bind (itree_bind t k) k' =
637 itree_bind t (λx. itree_bind (k x) k')
638Proof
639 rw[Once itree_bisimulation] >>
640 qexists_tac ‘λx y. (?t. ((x = itree_bind (itree_bind t k) k') /\
641 (y = itree_bind t (λx. itree_bind (k x) k')))) \/
642 x = y’ >>
643 rw[]
644 >- metis_tac[] >>
645 rename1 ‘itree_bind (itree_bind t _)’ >> Cases_on ‘t’ >>
646 gvs[itree_bind_thm] >> metis_tac[]
647QED
648
649Definition itree_iter_def:
650 itree_iter body seed =
651 itree_unfold
652 (λx.
653 case x of
654 Ret(INL seed') => Tau'(body seed')
655 | Ret(INR v) => Ret' v
656 | Tau u => Tau' u
657 | Vis e g => Vis' e g)
658 (body seed)
659End
660
661Theorem itree_iter_thm:
662 itree_iter body seed =
663 itree_bind (body seed)
664 (λx. case x of INL a => Tau(itree_iter body a)
665 | INR b => Ret b)
666Proof
667 rw[Once itree_bisimulation] >>
668 (* TODO: bisimulation up-to context would probably help here *)
669 qexists_tac
670 ‘λx y.
671 (?t. x = itree_unfold (λx.
672 case x of
673 Ret(INL seed') => Tau'(body seed')
674 | Ret(INR v) => Ret' v
675 | Tau u => Tau' u
676 | Vis e g => Vis' e g)
677 t /\
678 y = itree_bind t ((λx. case x of INL a => Tau (itree_iter body a)
679 | INR b => Ret b))) \/ x = y
680 ’ >>
681 rw[itree_iter_def]
682 >- metis_tac[] >>
683 first_x_assum (strip_assume_tac o ONCE_REWRITE_RULE[itree_unfold]) >>
684 gvs[AllCaseEqs(),itree_bind_thm] >>
685 metis_tac[]
686QED
687
688Definition itree_loop_def:
689 itree_loop body seed =
690 itree_iter (λx.
691 itree_bind (body x)
692 (λcb. case cb of INL c => Ret (INL(INL c))
693 | INR b => Ret (INR b)))
694 (INR seed)
695End
696
697(* weak termination-sensitive bisimulation *)
698
699Inductive strip_tau:
700 (strip_tau t t' ==> strip_tau (Tau t) t') /\
701 (strip_tau (Vis e k) (Vis e k)) /\
702 (strip_tau (Ret v) (Ret v))
703End
704
705Theorem strip_tau_simps[simp]:
706 (strip_tau t' (Tau t) = F) /\
707 (strip_tau (Ret v) (Vis e k) = F) /\
708 (strip_tau (Vis e k) (Ret v) = F) /\
709 (strip_tau (Tau t) t' = strip_tau t t')
710Proof
711 conj_tac
712 THEN1 (‘!t t'. strip_tau t t' ==> (?t''. t' = Tau t'') ==> F’
713 by(Induct_on ‘strip_tau’ \\ rw[]) \\ metis_tac[]) \\
714 rw[EQ_IMP_THM] \\ TRY $ spose_not_then strip_assume_tac \\
715 qhdtm_x_assum ‘strip_tau’
716 (strip_assume_tac o ONCE_REWRITE_RULE[strip_tau_cases]) \\
717 gvs[] \\
718 metis_tac[strip_tau_cases]
719QED
720
721Theorem strip_tau_simps2[simp]:
722 strip_tau (Ret v) (Ret v') = (v = v')
723Proof
724 rw[Once strip_tau_cases] \\ rw[EQ_IMP_THM]
725QED
726
727Theorem strip_tau_simps3[simp]:
728 strip_tau (Vis e k) (Vis e' k') = (e = e' /\ k = k')
729Proof
730 rw[Once strip_tau_cases] \\ rw[EQ_IMP_THM]
731QED
732
733Theorem strip_tau_inj:
734 !t t' t''. strip_tau t t' /\ strip_tau t t'' ==> t' = t''
735Proof
736 Induct_on ‘strip_tau’ \\
737 rw[] \\ gvs[Once strip_tau_cases]
738QED
739
740CoInductive itree_wbisim:
741 (itree_wbisim t t' ==> itree_wbisim (Tau t) (Tau t')) /\
742 (strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
743 (!r. itree_wbisim (k r) (k' r)) ==>
744 itree_wbisim t t') /\
745 (strip_tau t (Ret r) /\ strip_tau t' (Ret r) ==> itree_wbisim t t')
746End
747
748Definition wbisim_functional_def:
749 wbisim_functional R =
750 ({ (t,t') | ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)} UNION
751 { (t,t') | ?e k k'. strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
752 !r. (k r, k' r) IN R } UNION
753 { (Tau t, Tau t') | (t,t') IN R })
754End
755
756Theorem wbisim_functional_mono[simp]:
757 monotone wbisim_functional
758Proof
759 rw[monotone_def, wbisim_functional_def, SUBSET_DEF] >>
760 metis_tac[]
761QED
762
763Theorem wbisim_functional_cancel:
764 X SUBSET Y ==>
765 wbisim_functional X SUBSET wbisim_functional Y
766Proof
767 metis_tac[wbisim_functional_mono, monotone_def]
768QED
769
770Theorem wbisim_functional_gfp:
771 gfp wbisim_functional = rel_to_reln itree_wbisim
772Proof
773 rw[SET_EQ_SUBSET] >-
774 (simp[SUBSET_DEF] >> Cases >>
775 rw[in_rel_to_reln] >>
776 irule itree_wbisim_coind >>
777 qexists_tac ‘reln_to_rel $ gfp wbisim_functional’ >> rw[] >>
778 pop_assum mp_tac >>
779 dep_rewrite.DEP_ONCE_REWRITE_TAC[GSYM $ cj 1 gfp_greatest_fixedpoint] >>
780 rw[Once wbisim_functional_def, cj 1 gfp_greatest_fixedpoint] >> metis_tac[]) >>
781 irule $ MP_CANON gfp_coinduction >>
782 simp[SUBSET_DEF] >> Cases >>
783 fs[wbisim_functional_def, in_rel_to_reln] >>
784 metis_tac[itree_wbisim_cases]
785QED
786
787Theorem itree_wbisim_refl:
788 itree_wbisim t (t:('a,'b,'c) itree)
789Proof
790 ‘!t:('a,'b,'c) itree t'. t = t' ==> itree_wbisim t t'’
791 suffices_by metis_tac[] \\
792 ho_match_mp_tac itree_wbisim_coind \\ Cases \\ rw[] \\
793 metis_tac[strip_tau_rules]
794QED
795
796Theorem itree_wbisim_sym:
797 !t t'. itree_wbisim t t' ==> itree_wbisim t' t
798Proof
799 CONV_TAC SWAP_FORALL_CONV \\
800 ho_match_mp_tac itree_wbisim_coind \\
801 Cases \\ rw[] \\
802 pop_assum (strip_assume_tac o ONCE_REWRITE_RULE[itree_wbisim_cases]) \\
803 gvs[] \\
804 metis_tac[strip_tau_rules,itree_wbisim_rules]
805QED
806
807Theorem itree_wbisim_tau_eq:
808 itree_wbisim (Tau t) t
809Proof
810 ‘!t t'. t = Tau t' \/ t = t' ==> itree_wbisim t t'’ suffices_by metis_tac[] \\
811 ho_match_mp_tac itree_wbisim_coind \\ ntac 2 Cases \\ rw[] \\
812 metis_tac[strip_tau_rules]
813QED
814
815Theorem itree_wbisim_strong_coind:
816 !R.
817 (!t t'.
818 R t t' ==>
819 (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/
820 (?e k k'.
821 strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
822 !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/
823 ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) ==>
824 !t t'. R t t' ==> itree_wbisim t t'
825Proof
826 rpt strip_tac \\
827 Q.SUBGOAL_THEN ‘R t t' \/ itree_wbisim t t'’ mp_tac THEN1 simp[] \\
828 pop_assum kall_tac \\
829 MAP_EVERY qid_spec_tac [‘t'’,‘t’] \\
830 ho_match_mp_tac itree_wbisim_coind \\
831 rw[] \\
832 res_tac \\
833 gvs[] \\
834 pop_assum (strip_assume_tac o ONCE_REWRITE_RULE[itree_wbisim_cases]) \\
835 metis_tac[]
836QED
837
838Theorem itree_wbisim_coind_upto_equiv[local]:
839 !R t t'.
840 itree_wbisim t t' ==>
841 (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/
842 (?e k k'.
843 strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
844 !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/
845 ?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)
846Proof
847 metis_tac[itree_wbisim_cases]
848QED
849
850Theorem itree_wbisim_coind_upto:
851 !R.
852 (!t t'.
853 R t t' ==>
854 (?t2 t3. t = Tau t2 /\ t' = Tau t3 /\ (R t2 t3 \/ itree_wbisim t2 t3)) \/
855 (?e k k'.
856 strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
857 !r. R (k r) (k' r) \/ itree_wbisim (k r) (k' r)) \/
858 (?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r))
859 \/ itree_wbisim t t')
860 ==> !t t'. R t t' ==> itree_wbisim t t'
861Proof
862 rpt strip_tac >>
863 irule itree_wbisim_strong_coind >>
864 qexists_tac ‘R’ >>
865 fs[] >>
866 pop_assum kall_tac >>
867 metis_tac[itree_wbisim_coind_upto_equiv]
868QED
869
870(* more compositional variant using the enhanced functional (bt) *)
871(* proof: x < gfp \/ btx < b(K gfp \/ t)x < btx *)
872Theorem itree_wbisim_coind_upto':
873 !R. rel_to_reln R SUBSET
874 rel_to_reln itree_wbisim UNION
875 wbisim_functional (set_companion wbisim_functional (rel_to_reln R))
876 ==> rel_to_reln R SUBSET rel_to_reln itree_wbisim
877Proof
878 rw[] >>
879 fs[Once $ GSYM wbisim_functional_gfp] >>
880 irule set_companion_coinduct >> rw[] >>
881 drule_then irule SUBSET_TRANS >>
882 dep_rewrite.DEP_ONCE_REWRITE_TAC [GSYM $ cj 1 gfp_greatest_fixedpoint] >> rw[] >>
883 ‘gfp wbisim_functional SUBSET set_companion wbisim_functional (rel_to_reln R)’
884 suffices_by metis_tac[monotone_def, wbisim_functional_mono] >>
885 rw[set_gfp_sub_companion]
886QED
887
888Theorem itree_wbisim_vis:
889 !e k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==> itree_wbisim (Vis e k1) (Vis e k2)
890Proof
891 metis_tac[strip_tau_cases, itree_wbisim_cases]
892QED
893
894Theorem itree_wbisim_vis_vis:
895 itree_wbisim (Vis a g) (Vis a' g') <=>
896 a = a' /\ !r. itree_wbisim (g r) (g' r)
897Proof
898 iff_tac
899 >- (disch_tac
900 \\ drule $ iffLR itree_wbisim_cases \\ gvs[]
901 )
902 \\ gvs[itree_wbisim_vis]
903QED
904
905Theorem itree_wbisim_tau:
906 !t t'. itree_wbisim (Tau t) t' ==> itree_wbisim t t'
907Proof
908 ho_match_mp_tac itree_wbisim_strong_coind \\ rw[] \\
909 qhdtm_x_assum ‘itree_wbisim’
910 (strip_assume_tac o ONCE_REWRITE_RULE[itree_wbisim_cases]) \\
911 gvs[] \\
912 metis_tac[itree_wbisim_cases]
913QED
914
915Theorem itree_wbisim_tau_eqn0[local]:
916 !t t'. (?t0. t = Tau t0 /\ itree_wbisim t0 t') ==> itree_wbisim t t'
917Proof
918 ho_match_mp_tac itree_wbisim_strong_coind >> rw[] >>
919 pop_assum (strip_assume_tac o ONCE_REWRITE_RULE [itree_wbisim_cases]) >>
920 gvs[] >> metis_tac[]
921QED
922
923Theorem itree_wbisim_tau_eqn[simp]:
924 (itree_wbisim (Tau t1) t2 <=> itree_wbisim t1 t2) /\
925 (itree_wbisim t1 (Tau t2) <=> itree_wbisim t1 t2)
926Proof
927 metis_tac[itree_wbisim_sym, itree_wbisim_tau_eqn0, itree_wbisim_tau]
928QED
929
930Theorem itree_wbisim_strip_tau:
931 !t t' t''. itree_wbisim t t' /\ strip_tau t t'' ==> itree_wbisim t'' t'
932Proof
933 Induct_on ‘strip_tau’ \\
934 rw[] \\ imp_res_tac itree_wbisim_tau \\
935 res_tac
936QED
937
938Theorem itree_wbisim_strip_tau_sym:
939 !t t' t''. itree_wbisim t t' /\ strip_tau t' t'' ==> itree_wbisim t t''
940Proof
941 metis_tac[itree_wbisim_sym,itree_wbisim_strip_tau]
942QED
943
944Theorem itree_wbisim_strip_tau_Ret:
945 !t t' v. itree_wbisim t t' /\ strip_tau t (Ret v) ==> strip_tau t' (Ret v)
946Proof
947 Induct_on ‘strip_tau’ \\
948 rw[] \\ imp_res_tac itree_wbisim_tau \\
949 res_tac \\
950 gvs[Once itree_wbisim_cases]
951QED
952
953Theorem itree_wbisim_strip_tau_Vis:
954 !t t' e k. itree_wbisim t t' /\ strip_tau t (Vis e k)
955 ==> ?k'. strip_tau t' (Vis e k') /\ !r. itree_wbisim (k r) (k' r)
956Proof
957 Induct_on ‘strip_tau’ \\
958 rw[] \\ imp_res_tac itree_wbisim_tau \\
959 res_tac \\
960 gvs[Once itree_wbisim_cases] \\
961 first_x_assum $ irule_at Any \\
962 simp[]
963QED
964
965Theorem itree_wbisim_trans:
966 !t t' t''. itree_wbisim t t' /\ itree_wbisim t' t'' ==> itree_wbisim t t''
967Proof
968 CONV_TAC $ QUANT_CONV $ SWAP_FORALL_CONV \\
969 Ho_Rewrite.PURE_REWRITE_TAC[GSYM PULL_EXISTS] \\
970 ho_match_mp_tac itree_wbisim_coind \\
971 Cases \\ rw[] \\
972 last_x_assum (strip_assume_tac o ONCE_REWRITE_RULE[itree_wbisim_cases]) \\
973 gvs[]
974 >- (imp_res_tac itree_wbisim_strip_tau_Ret)
975 >- (last_x_assum (strip_assume_tac o ONCE_REWRITE_RULE[itree_wbisim_cases]) \\
976 gvs[] \\
977 metis_tac[itree_wbisim_strip_tau_Vis,
978 itree_wbisim_strip_tau_Ret,
979 itree_wbisim_sym]) \\
980 metis_tac[itree_wbisim_strip_tau_Vis,
981 itree_wbisim_strip_tau_Ret,
982 itree_wbisim_sym]
983QED
984
985(* common bind base case *)
986Theorem itree_bind_ret_inv:
987 itree_bind t k = Ret r ==> ?r'. t = Ret r' /\ (k r') = Ret r
988Proof
989 Cases_on ‘t’ >> fs[itree_bind_thm]
990QED
991
992(* combinators respect weak bisimilarity *)
993Theorem itree_bind_strip_tau_wbisim:
994 !u u' k. strip_tau u u' ==> itree_wbisim (itree_bind u k) (itree_bind u' k)
995Proof
996 Induct_on ‘strip_tau’ >>
997 rw[] >>
998 metis_tac[itree_wbisim_refl, itree_wbisim_tau_eq, itree_wbisim_trans]
999QED
1000
1001Theorem itree_bind_vis_strip_tau:
1002 !u k k' e. strip_tau u (Vis e k') ==>
1003 strip_tau (itree_bind u k) (Vis e (λx. itree_bind (k' x) k))
1004Proof
1005 rpt strip_tac >>
1006 pop_assum mp_tac >>
1007 Induct_on ‘strip_tau’ >>
1008 rpt strip_tac >>
1009 rw[itree_bind_thm]
1010QED
1011
1012Theorem itree_bind_vis_tau_wbisim[local]:
1013 itree_wbisim (Vis a g) (Tau u) ==>
1014 ?e k' k''.
1015 strip_tau (itree_bind (Vis a g) k) (Vis e k') /\
1016 strip_tau (itree_bind (Tau u) k) (Vis e k'') /\
1017 !r. (?t1 t2. itree_wbisim t1 t2 /\
1018 k' r = itree_bind t1 k /\ k'' r = itree_bind t2 k) \/
1019 itree_wbisim (k' r) (k'' r)
1020Proof
1021 rpt strip_tac >>
1022 fs[Once itree_wbisim_cases, itree_bind_thm] >>
1023 fs[Once $ GSYM itree_wbisim_cases] >>
1024 qexists_tac ‘λx. itree_bind (k' x) k’ >>
1025 rw[itree_bind_vis_strip_tau] >>
1026 metis_tac[]
1027QED
1028
1029Theorem itree_bind_resp_t_wbisim:
1030 !a b k. itree_wbisim a b ==> itree_wbisim (itree_bind a k) (itree_bind b k)
1031Proof
1032 rpt strip_tac >>
1033 qspecl_then [‘λa b. ?t1 t2. itree_wbisim t1 t2 /\
1034 a = itree_bind t1 k /\ b = itree_bind t2 k’]
1035 strip_assume_tac itree_wbisim_coind_upto >>
1036 pop_assum irule >>
1037 rw[] >-
1038 (last_x_assum kall_tac >>
1039 Cases_on ‘t1’ >>
1040 Cases_on ‘t2’ >-
1041 (fs[Once itree_wbisim_cases, itree_bind_thm] >>
1042 Cases_on ‘k x’ >> rw[itree_wbisim_refl]) >-
1043 (disj2_tac >> disj2_tac >> disj2_tac >>
1044 irule itree_wbisim_sym >>
1045 irule itree_bind_strip_tau_wbisim >>
1046 fs[Once itree_wbisim_cases]) >-
1047 (fs[Once itree_wbisim_cases]) >-
1048 (disj2_tac >> disj2_tac >> disj2_tac >>
1049 irule itree_bind_strip_tau_wbisim >>
1050 fs[Once itree_wbisim_cases]) >-
1051 (rw[itree_bind_thm] >>
1052 ‘itree_wbisim u u'’ by metis_tac[itree_wbisim_tau, itree_wbisim_sym] >>
1053 metis_tac[]) >-
1054 (metis_tac[itree_wbisim_sym, itree_bind_vis_tau_wbisim]) >-
1055 (fs[Once itree_wbisim_cases]) >-
1056 (metis_tac[itree_wbisim_sym, itree_bind_vis_tau_wbisim]) >-
1057 (fs[itree_bind_thm, Once itree_wbisim_cases] >> metis_tac[]))
1058 >- metis_tac[]
1059QED
1060
1061Theorem itree_bind_resp_k_wbisim:
1062 !t k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==>
1063 itree_wbisim (itree_bind t k1) (itree_bind t k2)
1064Proof
1065 rpt strip_tac >>
1066 qspecl_then [‘λa b. ?t. a = itree_bind t k1 /\ b = itree_bind t k2’]
1067 strip_assume_tac itree_wbisim_coind_upto >>
1068 pop_assum irule >>
1069 rw[] >-
1070 (Cases_on ‘t''’ >> rw[itree_bind_thm] >> metis_tac[]) >-
1071 metis_tac[]
1072QED
1073
1074Theorem itree_bind_resp_wbisim:
1075 !a b k1 k2. itree_wbisim a b /\ (!r. itree_wbisim (k1 r) (k2 r)) ==>
1076 itree_wbisim (itree_bind a k1) (itree_bind b k2)
1077Proof
1078 metis_tac[itree_bind_resp_t_wbisim, itree_bind_resp_k_wbisim, itree_wbisim_trans]
1079QED
1080
1081Theorem itree_iter_ret_tau_wbisim[local]:
1082 itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a) | INR b => Ret b) /\
1083 itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a) | INR b => Ret b) /\
1084 itree_wbisim (Ret x) (Tau u) /\ (!r. itree_wbisim (k1 r) (k2 r))
1085 ==>
1086 (?t2 t3.
1087 itree_bind (Ret x) itcb1 = Tau t2 /\ itree_bind (Tau u) itcb2 = Tau t3 /\
1088 ((?sa sb. itree_wbisim sa sb /\
1089 t2 = itree_bind sa itcb1 /\ t3 = itree_bind sb itcb2)
1090 \/ itree_wbisim t2 t3)) \/
1091 (?e k k'.
1092 strip_tau (itree_bind (Ret x) itcb1) (Vis e k) /\
1093 strip_tau (itree_bind (Tau u) itcb2) (Vis e k') /\
1094 !r. (?sa sb. itree_wbisim sa sb /\
1095 k r = itree_bind sa itcb1 /\ k' r = itree_bind sb itcb2)
1096 \/ itree_wbisim (k r) (k' r)) \/
1097 ?r. strip_tau (itree_bind (Ret x) itcb1) (Ret r) /\
1098 strip_tau (itree_bind (Tau u) itcb2) (Ret r)
1099Proof
1100 rpt strip_tac >>
1101 rw[itree_bind_thm] >>
1102 qabbrev_tac ‘itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a)
1103 | INR b => Ret b)’ >>
1104 qabbrev_tac ‘itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a)
1105 | INR b => Ret b)’ >>
1106 fs[Once itree_wbisim_cases] >> fs[Once $ GSYM itree_wbisim_cases] >>
1107 qpat_x_assum ‘strip_tau _ _’ mp_tac >>
1108 Induct_on ‘strip_tau’ >>
1109 rw[itree_bind_thm] >-
1110 (disj1_tac >>
1111 metis_tac[itree_bind_thm,
1112 itree_wbisim_tau_eq, itree_wbisim_trans, itree_wbisim_sym]) >-
1113 (disj1_tac >>
1114 metis_tac[itree_wbisim_tau_eq, itree_wbisim_trans, itree_wbisim_sym]) >-
1115 (disj2_tac >> disj1_tac >> metis_tac[]) >-
1116 (disj2_tac >> disj2_tac >> metis_tac[]) >-
1117 (Cases_on ‘v’ >-
1118 (qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
1119 rw[] >>
1120 disj1_tac >> disj1_tac >>
1121 qexistsl_tac [‘k1 x’, ‘Tau (k2 x)’] >>
1122 simp[Once itree_iter_thm] >>
1123 simp[Once itree_iter_thm, itree_bind_thm] >>
1124 metis_tac[itree_wbisim_tau_eq, itree_wbisim_sym, itree_wbisim_trans]) >-
1125 (qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
1126 rw[]))
1127QED
1128
1129Theorem itree_iter_resp_wbisim:
1130 !t k1 k2. (!r. itree_wbisim (k1 r) (k2 r)) ==>
1131 itree_wbisim (itree_iter k1 t) (itree_iter k2 t)
1132Proof
1133 rpt strip_tac >>
1134 qabbrev_tac ‘itcb1 = (λx. case x of INL a => Tau (itree_iter k1 a)
1135 | INR b => Ret b)’ >>
1136 qabbrev_tac ‘itcb2 = (λx. case x of INL a => Tau (itree_iter k2 a)
1137 | INR b => Ret b)’ >>
1138 qspecl_then [‘λia ib. ?sa sb x. itree_wbisim sa sb /\
1139 ia = itree_bind sa itcb1 /\
1140 ib = itree_bind sb itcb2’]
1141 strip_assume_tac itree_wbisim_strong_coind >>
1142 pop_assum irule >>
1143 rw[] >-
1144 (Cases_on ‘sa’ >>
1145 Cases_on ‘sb’ >-
1146 (‘x' = x’ by fs[Once itree_wbisim_cases] >>
1147 gvs[] >>
1148 Cases_on ‘x’ >-
1149 (disj1_tac >> (* Ret INL by wbisim *)
1150 qexistsl_tac [‘itree_bind (k1 x') itcb1’, ‘itree_bind (k2 x') itcb2’] >>
1151 qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
1152 simp[Once itree_iter_thm, itree_bind_thm] >>
1153 simp[Once itree_iter_thm, itree_bind_thm] >>
1154 metis_tac[]) >-
1155 (disj2_tac >> disj2_tac >> (* Ret INR by equality *)
1156 qunabbrev_tac ‘itcb1’ >> qunabbrev_tac ‘itcb2’ >>
1157 rw[Once itree_iter_thm, itree_bind_thm])) >-
1158 (irule itree_iter_ret_tau_wbisim >> metis_tac[]) >-
1159 (fs[Once itree_wbisim_cases]) >-
1160 (‘itree_wbisim (Ret x) (Tau u)’ by fs[itree_wbisim_sym] >>
1161 rpt $ qpat_x_assum ‘Abbrev _’
1162 $ assume_tac o PURE_REWRITE_RULE[markerTheory.Abbrev_def] >>
1163 pop_assum mp_tac >>
1164 drule itree_iter_ret_tau_wbisim >>
1165 rpt strip_tac >>
1166 first_x_assum drule >>
1167 disch_then drule >>
1168 impl_tac >> metis_tac[itree_wbisim_sym]) >-
1169 (disj1_tac >>
1170 rw[itree_bind_thm] >>
1171 metis_tac[itree_wbisim_tau_eq, itree_wbisim_sym, itree_wbisim_trans]) >-
1172 (rw[itree_bind_thm] >>
1173 fs[Once itree_wbisim_cases] >> fs[Once $ GSYM itree_wbisim_cases] >>
1174 qexists_tac ‘(λx. itree_bind (k x) itcb1)’ >>
1175 metis_tac[itree_bind_vis_strip_tau]) >-
1176 (fs[Once itree_wbisim_cases]) >-
1177 (rw[itree_bind_thm] >>
1178 fs[Once itree_wbisim_cases] >> fs[Once $ GSYM itree_wbisim_cases] >>
1179 qexists_tac ‘(λx. itree_bind (k' x) itcb2)’ >>
1180 metis_tac[itree_bind_vis_strip_tau]) >-
1181 (disj2_tac >> disj1_tac >>
1182 simp[itree_bind_thm] >>
1183 fs[Once itree_wbisim_cases] >> fs[GSYM $ Once itree_wbisim_cases] >>
1184 metis_tac[]))
1185 >- (qexistsl_tac [‘k1 t’, ‘k2 t’] >> rw[itree_iter_thm])
1186QED
1187
1188Theorem itree_iter_seed_wbisim:
1189 !body seed seed'. (itree_wbisim seed seed') /\
1190 (itree_wbisim (body seed) (body seed')) ==>
1191 itree_wbisim (itree_iter body seed) (itree_iter body seed')
1192Proof
1193 rpt strip_tac
1194 \\ PURE_ONCE_REWRITE_TAC[itree_iter_thm]
1195 \\ irule itree_bind_resp_wbisim
1196 \\ rw[itree_wbisim_refl]
1197QED
1198
1199Theorem itree_iter_body_seed_wbisim:
1200 !body body' seed seed'. (itree_wbisim seed seed') /\
1201 (!seed seed'. itree_wbisim (body seed) (body' seed')) ==>
1202 itree_wbisim (itree_iter body seed) (itree_iter body' seed')
1203Proof
1204 rpt strip_tac
1205 \\ PURE_ONCE_REWRITE_TAC[itree_iter_thm]
1206 \\ irule itree_bind_resp_wbisim
1207 \\ rw[]
1208 \\ Cases_on ‘r’ \\ rw[itree_wbisim_refl]
1209 \\ irule itree_iter_resp_wbisim
1210 \\ metis_tac[]
1211QED
1212
1213(* coinduction upto stripping finite taus, useful for iter and friends *)
1214Inductive after_taus:
1215[~rel:]
1216 (R x y ==> after_taus R x y)
1217[~tauL:]
1218 (after_taus R x y ==> after_taus R (Tau x) y)
1219[~tauR:]
1220 (after_taus R x y ==> after_taus R x (Tau y))
1221End
1222
1223Theorem after_taus_FUNPOW_TauL:
1224 after_taus R x y ==> after_taus R (FUNPOW Tau n x) y
1225Proof
1226 Induct_on ‘n’ \\ rw[FUNPOW_SUC]
1227 \\ irule after_taus_tauL \\ gvs[]
1228QED
1229
1230Theorem after_taus_FUNPOW_TauR:
1231 after_taus R x y ==> after_taus R x (FUNPOW Tau n y)
1232Proof
1233 Induct_on ‘n’ \\ rw[FUNPOW_SUC]
1234 \\ irule after_taus_tauR \\ gvs[]
1235QED
1236
1237Definition upto_taus_func_def:
1238 upto_taus_func R = R UNION rel_to_reln (after_taus (reln_to_rel R))
1239End
1240
1241Theorem upto_taus_compatible:
1242 set_compatible wbisim_functional upto_taus_func
1243Proof
1244 rw[set_compatible_def, wbisim_functional_def, upto_taus_func_def, monotone_def] >-
1245 (metis_tac[SUBSET_TRANS, SUBSET_UNION]) >-
1246 (irule SUBSET_TRANS >>
1247 qexists_tac ‘rel_to_reln (after_taus (reln_to_rel Y))’ >>
1248 simp[SUBSET_DEF, in_rel_to_reln] >>
1249 Cases >> simp[] >>
1250 Induct_on ‘after_taus’ >> rw[] >>
1251 rw[Once after_taus_cases] >>
1252 metis_tac[SUBSET_DEF]) >-
1253 (metis_tac[SUBSET_TRANS, SUBSET_UNION]) >-
1254 (rw[SUBSET_DEF, IN_DEF] >> metis_tac[]) >-
1255 (rw[SUBSET_DEF, IN_DEF] >> metis_tac[]) >>
1256 simp[SUBSET_DEF, rel_to_reln_def] >>
1257 Induct_on ‘after_taus’ >>
1258 fs[wbisim_functional_def] >>
1259 metis_tac[after_taus_cases, reln_to_rel_app]
1260QED
1261
1262(* example: compatibility can be used like so *)
1263Theorem itree_coind_upto_taus:
1264 !R.
1265 rel_to_reln R SUBSET
1266 rel_to_reln itree_wbisim UNION
1267 wbisim_functional (upto_taus_func (rel_to_reln R) UNION
1268 rel_to_reln itree_wbisim)
1269 ==> rel_to_reln R SUBSET rel_to_reln itree_wbisim
1270Proof
1271 rw[] >>
1272 irule itree_wbisim_coind_upto' >>
1273 dxrule_then irule SUBSET_TRANS >>
1274 rw[UNION_SUBSET] >>
1275 irule SUBSET_TRANS >>
1276 irule_at (Pos last) (cj 2 SUBSET_UNION) >>
1277 irule wbisim_functional_cancel >> rw[] >-
1278 (irule set_compatible_enhance >> rw[] >>
1279 metis_tac[upto_taus_compatible, SUBSET_REFL]) >>
1280 metis_tac[set_gfp_sub_companion, wbisim_functional_mono, wbisim_functional_gfp]
1281QED
1282
1283(* misc *)
1284
1285Definition spin:
1286 spin = itree_unfold (K (Tau' ())) ()
1287End
1288
1289Theorem spin[allow_rebind]:
1290 spin = Tau spin (* an infinite sequence of silent actions *)
1291Proof
1292 fs [spin] \\ simp [Once itree_unfold]
1293QED
1294
1295(* relation to tauless itrees *)
1296
1297Theorem strip_tau_spin:
1298 (!t'. ~strip_tau t t') ==> t = spin
1299Proof
1300 rw[Once itree_bisimulation] \\
1301 qexists_tac ‘λt t'. (!t'. ~strip_tau t t') /\ t' = spin’ \\
1302 rw[GSYM spin] \\
1303 metis_tac[strip_tau_simps2,strip_tau_simps3]
1304QED
1305
1306Definition untau_def:
1307 untau = itree$itree_unfold
1308 (λt. case some t'. strip_tau t t' of
1309 NONE => Div'
1310 | SOME(Tau t') => Div' (* impossible *)
1311 | SOME(Ret v) => Ret' v
1312 | SOME(Vis e k) => Vis' e k)
1313End
1314
1315Theorem spin_strip_tau:
1316 !t. strip_tau spin t ==> F
1317Proof
1318 Induct_on ‘strip_tau’ \\
1319 rw[] \\
1320 metis_tac[spin,itree_distinct,itree_11]
1321QED
1322
1323Theorem untau_spin[simp]:
1324 untau spin = Div
1325Proof
1326 rw[untau_def,Once itreeTheory.itree_unfold] \\
1327 DEEP_INTRO_TAC some_intro \\
1328 rw[] \\
1329 imp_res_tac spin_strip_tau
1330QED
1331
1332Theorem untau_IMP_wbisim:
1333 !t t'. untau t = untau t' ==> itree_wbisim t t'
1334Proof
1335 ho_match_mp_tac itree_wbisim_strong_coind \\
1336 rw[] \\
1337 gvs[untau_def] \\
1338 pop_assum (strip_assume_tac o ONCE_REWRITE_RULE[itreeTheory.itree_unfold]) \\
1339 gvs[AllCaseEqs()] \\
1340 rpt(pop_assum mp_tac) \\
1341 ntac 2 (DEEP_INTRO_TAC some_intro \\ simp[]) \\
1342 rw[]
1343 THEN1 metis_tac[]
1344 THEN1 metis_tac[strip_tau_spin,spin,itree_wbisim_refl]
1345 THEN1 metis_tac[combinTheory.o_DEF]
1346QED
1347
1348Theorem wbisim_IMP_untau:
1349 !t t'. itree_wbisim t t' ==> untau t = untau t'
1350Proof
1351 rw[Once itreeTheory.itree_bisimulation] \\
1352 qexists_tac
1353 ‘λt t1. (?t2 t3. itree_wbisim t2 t3 /\ t = untau t2 /\ t1 = untau t3)’ \\
1354 gvs[] \\
1355 conj_tac THEN1 metis_tac[] \\
1356 pop_assum kall_tac \\
1357 rw[untau_def] \\
1358 pop_assum (strip_assume_tac o ONCE_REWRITE_RULE[itreeTheory.itree_unfold]) \\
1359 gvs[AllCaseEqs()] \\
1360 rpt(pop_assum mp_tac) \\
1361 DEEP_INTRO_TAC some_intro \\ simp[] \\
1362 rw[]
1363 THEN1
1364 (imp_res_tac itree_wbisim_strip_tau_Ret \\
1365 simp[Once itreeTheory.itree_unfold] \\
1366 DEEP_INTRO_TAC some_intro \\ simp[] \\
1367 reverse conj_tac THEN1 first_x_assum $ irule_at Any \\
1368 rw[] \\
1369 dxrule_all_then strip_assume_tac strip_tau_inj \\
1370 gvs[])
1371 THEN1
1372 (rename [‘itree_wbisim t1 t2’] \\
1373 ‘!x. ~strip_tau t2 x’
1374 by(Cases \\ gvs[] \\ spose_not_then strip_assume_tac \\
1375 metis_tac[itree_wbisim_strip_tau_Ret,
1376 itree_wbisim_strip_tau_Vis,
1377 itree_wbisim_sym]) \\
1378 imp_res_tac strip_tau_spin \\
1379 simp[GSYM untau_def]) \\
1380 drule_all_then strip_assume_tac itree_wbisim_strip_tau_Vis \\
1381 simp[Once itreeTheory.itree_unfold] \\
1382 DEEP_INTRO_TAC some_intro \\
1383 reverse $ rw[] THEN1 metis_tac[] \\
1384 dxrule_all_then strip_assume_tac strip_tau_inj \\
1385 gvs[] \\
1386 metis_tac[]
1387QED
1388
1389(** FUNPOW **)
1390
1391Theorem Tau_INJ[simp]:
1392 INJ Tau UNIV UNIV
1393Proof
1394 simp[INJ_DEF]
1395QED
1396
1397Theorem FUNPOW_Tau_neq[simp]:
1398 Ret x <> FUNPOW Tau n (Vis a g) /\
1399 Vis a g <> FUNPOW Tau n (Ret x)
1400Proof
1401 MAP_EVERY qid_spec_tac [‘x’,‘a’,‘g’,‘n’]>>
1402 Induct>>rw[FUNPOW_SUC]
1403QED
1404
1405Theorem FUNPOW_Tau_neq2[simp]:
1406 FUNPOW Tau n' (Ret x) <> FUNPOW Tau n (Vis a g)
1407Proof
1408 Cases_on ‘n < n'’>>fs[NOT_LESS]>>strip_tac
1409 >- (imp_res_tac (GSYM LESS_ADD)>>fs[FUNPOW_ADD]>>
1410 fs[FUNPOW_eq_elim,Tau_INJ])>>
1411 gvs[FUNPOW_min_cancel,Tau_INJ]
1412QED
1413
1414Theorem strip_tau_FUNPOW:
1415 !t1 t2. strip_tau t1 t2 ==>
1416 ?n. t1 = FUNPOW Tau n $ t2
1417Proof
1418 Induct_on ‘strip_tau’ >>
1419 rw[]
1420 >- (qrefine ‘SUC _’ >>
1421 rw[FUNPOW_SUC] >>
1422 metis_tac[]
1423 ) >>
1424 qexists ‘0’ >>
1425 rw[]
1426QED
1427
1428Theorem FUNPOW_Tau_wbisim:
1429 itree_wbisim (FUNPOW Tau n x) x
1430Proof
1431 Induct_on ‘n’ >>
1432 rw[itree_wbisim_refl,FUNPOW_SUC]
1433QED
1434
1435Theorem FUNPOW_Tau_wbisim_intro:
1436 itree_wbisim x y ==>
1437 itree_wbisim (FUNPOW Tau n x) (FUNPOW Tau n' y)
1438Proof
1439 metis_tac[FUNPOW_Tau_wbisim,itree_wbisim_trans,itree_wbisim_refl,itree_wbisim_sym]
1440QED
1441
1442Theorem strip_tau_vis_wbisim:
1443 !e k k'. strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
1444 (!r. itree_wbisim (k r) (k' r)) ==>
1445 itree_wbisim t t'
1446Proof
1447 rpt strip_tac >>
1448 imp_res_tac strip_tau_FUNPOW >>
1449 gvs[] >>
1450 irule FUNPOW_Tau_wbisim_intro >>
1451 rw[Once itree_wbisim_cases]
1452QED
1453
1454Theorem itree_wbisim_Ret_FUNPOW:
1455 itree_wbisim t (Ret x) ==> ?n. t = FUNPOW Tau n $ Ret x
1456Proof
1457 rw[Once itree_wbisim_cases] >>
1458 drule_then irule strip_tau_FUNPOW
1459QED
1460
1461Theorem FUNPOW_Tau_imp_wbisim:
1462 t = FUNPOW Tau n $ t' ==> itree_wbisim t t'
1463Proof
1464 strip_tac >>
1465 irule itree_wbisim_trans >>
1466 irule_at Any FUNPOW_Tau_wbisim>>fs[]>>
1467 irule_at Any itree_wbisim_refl
1468QED
1469
1470Theorem itree_wbisim_Vis_FUNPOW:
1471 itree_wbisim t (Vis a g) ==>
1472 ?n k. t = FUNPOW Tau n $ Vis a k /\ (!r. itree_wbisim (k r) (g r))
1473Proof
1474 simp[Once itree_wbisim_cases] >> rw[] >>
1475 imp_res_tac strip_tau_FUNPOW>>
1476 pop_assum $ irule_at Any>>fs[]
1477QED
1478
1479Theorem wbisim_FUNPOW_Tau:
1480 (itree_wbisim t (FUNPOW Tau n ht) <=> itree_wbisim t ht) /\
1481 (itree_wbisim (FUNPOW Tau n ht) t <=> itree_wbisim ht t)
1482Proof
1483 rw[EQ_IMP_THM]>>
1484 TRY (irule itree_wbisim_trans>>
1485 irule_at Any FUNPOW_Tau_wbisim>>
1486 fs[]>>metis_tac[]>>NO_TAC)>>
1487 irule itree_wbisim_trans>>
1488 first_assum $ irule_at Any>>
1489 irule itree_wbisim_sym>>
1490 irule FUNPOW_Tau_wbisim
1491QED
1492
1493Theorem FUNPOW_Tau_bind:
1494 itree_bind (FUNPOW Tau n t)g = FUNPOW Tau n (itree_bind t g)
1495Proof
1496 MAP_EVERY qid_spec_tac [‘t’,‘n’]>>
1497 Induct_on ‘n’>>rw[]>>
1498 simp[FUNPOW]
1499QED
1500
1501Theorem strip_tau_FUNPOW_cancel:
1502 (!u. t <> Tau u) ==>
1503 strip_tau (FUNPOW Tau n t) t
1504Proof
1505 Induct_on ‘n’>>rw[]
1506 >- (Cases_on ‘t’>>rw[])>>
1507 Cases_on ‘t’>>rw[FUNPOW_SUC]
1508QED
1509
1510Theorem FUNPOW_Tau_Vis_eq:
1511 FUNPOW Tau n (Vis a g) = FUNPOW Tau m (Vis e k) ==>
1512 n = m /\ a = e /\ g = k
1513Proof
1514 strip_tac>>
1515 Cases_on ‘n < m’>>fs[NOT_LESS]
1516 >- (fs[FUNPOW_min_cancel,Tau_INJ]>>
1517 Cases_on ‘m - n’>>fs[FUNPOW_SUC])>>
1518 last_x_assum $ assume_tac o GSYM>>
1519 rfs[FUNPOW_min_cancel,Tau_INJ]>>
1520 Cases_on ‘n - m’>>fs[FUNPOW_SUC]
1521QED
1522
1523Theorem FUNPOW_Tau_Ret_eq:
1524 FUNPOW Tau n (Ret x) = FUNPOW Tau m (Ret y) ==>
1525 n = m /\ x = y
1526Proof
1527 strip_tac>>
1528 Cases_on ‘n < m’>>fs[NOT_LESS]
1529 >- (fs[FUNPOW_min_cancel,Tau_INJ]>>
1530 Cases_on ‘m - n’>>fs[FUNPOW_SUC])>>
1531 last_x_assum $ assume_tac o GSYM>>
1532 rfs[FUNPOW_min_cancel,Tau_INJ]>>
1533 Cases_on ‘n - m’>>fs[FUNPOW_SUC]
1534QED
1535
1536(* more on spin *)
1537
1538Theorem spin_bind:
1539 itree_bind spin k = spin
1540Proof
1541 simp[Once itree_bisimulation]>>
1542 qexists ‘CURRY {(itree_bind spin k, spin)}’>>
1543 simp[]>>rw[]
1544 >- fs[Once spin]
1545 >- irule (GSYM spin)
1546 >- fs[Once spin,itree_bind_thm]>>
1547 fs[Once spin]
1548QED
1549
1550Theorem spin_FUNPOW_Tau:
1551 !n. spin = FUNPOW Tau n spin
1552Proof
1553 Induct>>rw[]>>fs[FUNPOW_SUC]>>
1554 irule (GSYM spin)
1555QED
1556
1557Theorem wbisim_spin_eq:
1558 itree_wbisim t spin <=> t = spin
1559Proof
1560 rw[EQ_IMP_THM]
1561 >- (simp[Once itree_bisimulation]>>
1562 qexists ‘CURRY {(t,spin)|t|itree_wbisim t spin}’>>
1563 rw[]
1564 >- fs[Once itree_wbisim_cases,spin_strip_tau]
1565 >- irule (GSYM spin)>>
1566 fs[Once itree_wbisim_cases,spin_strip_tau])>>
1567 irule itree_wbisim_refl
1568QED
1569
1570Theorem strip_tau_FUNPOW_strip_tau:
1571 !t t' n. strip_tau t t' ==> strip_tau (FUNPOW Tau n t) t'
1572Proof
1573 rpt strip_tac
1574 \\ drule strip_tau_FUNPOW
1575 \\ rpt strip_tac
1576 \\ gvs[GSYM FUNPOW_ADD]
1577 \\ Cases_on ‘t'’ \\ gvs[]
1578 \\ irule strip_tau_FUNPOW_cancel
1579 \\ gvs[]
1580QED
1581
1582Theorem FUNPOW_Ret_spin_F:
1583 FUNPOW Tau n (Ret x) = spin ==> F
1584Proof
1585 disch_tac
1586 \\ ‘FUNPOW Tau n (Ret x) = FUNPOW Tau n spin’ by (PURE_REWRITE_TAC[GSYM spin_FUNPOW_Tau] \\ rw[])
1587 \\ subgoal ‘!t t'. FUNPOW Tau n t = FUNPOW Tau n t' <=> t = t'’
1588 >- (irule FUNPOW_eq_elim
1589 \\ rw[]
1590 )
1591 \\ pop_assum $ assume_tac o iffLR
1592 \\ res_tac
1593 \\ pop_assum mp_tac
1594 \\ PURE_ONCE_REWRITE_TAC[spin]
1595 \\ rw[]
1596QED
1597
1598Theorem FUNPOW_Vis_spin_F:
1599 FUNPOW Tau n (Vis e k) = spin ==> F
1600Proof
1601 disch_tac
1602 \\ ‘FUNPOW Tau n (Vis e k) = FUNPOW Tau n spin’ by (PURE_REWRITE_TAC[GSYM spin_FUNPOW_Tau] \\ rw[])
1603 \\ subgoal ‘!t t'. FUNPOW Tau n t = FUNPOW Tau n t' <=> t = t'’
1604 >- (irule FUNPOW_eq_elim
1605 \\ rw[]
1606 )
1607 \\ pop_assum $ assume_tac o iffLR
1608 \\ res_tac
1609 \\ pop_assum mp_tac
1610 \\ PURE_ONCE_REWRITE_TAC[spin]
1611 \\ rw[]
1612QED
1613
1614Theorem FUNPOW_Tau_SUC_cyclic_spin:
1615 t = FUNPOW Tau (SUC n) t <=> t = spin
1616Proof
1617 iff_tac
1618 >- (rpt strip_tac
1619 \\ Cases_on ‘?t'. strip_tau t t'’ \\ gvs[]
1620 >- (Cases_on ‘t'’ \\ gvs[]
1621 \\ imp_res_tac strip_tau_FUNPOW
1622 \\ gvs[GSYM FUNPOW_ADD]
1623 >- (drule FUNPOW_Tau_Ret_eq
1624 \\ gvs[]
1625 )
1626 \\ drule FUNPOW_Tau_Vis_eq
1627 \\ gvs[]
1628 )
1629 \\ rw[strip_tau_spin]
1630 )
1631 \\ rw[spin_FUNPOW_Tau]
1632QED
1633
1634Theorem FUNPOW_Tau_abs_cyclic_spin:
1635 (!r. ?n r'. abs r = FUNPOW Tau (SUC n) (abs r')) <=> (!r. abs r = spin)
1636Proof
1637 iff_tac
1638 >- (rpt strip_tac
1639 \\ irule $ iffLR wbisim_spin_eq
1640 \\ irule itree_wbisim_coind_upto
1641 \\ qexists ‘CURRY {(FUNPOW Tau n (abs r), spin) | (n, r) | T }’
1642 \\ reverse $ rw[UNCURRY]
1643 >- (qexists ‘(0, r)’ \\ rw[]
1644 )
1645 \\ Cases_on ‘x’ \\ gvs[]
1646 \\ gvs[FUNPOW_SUC]
1647 \\ disj1_tac
1648 \\ first_x_assum $ qspec_then ‘r’ assume_tac
1649 \\ gvs[]
1650 \\ rw[Once spin]
1651 \\ rw[GSYM FUNPOW_SUC, GSYM FUNPOW_ADD, GSYM ADD_SUC]
1652 \\ rw[FUNPOW_SUC]
1653 \\ disj1_tac
1654 \\ qexists ‘(n + q, r')’ \\ rw[]
1655 )
1656 \\ rpt strip_tac
1657 \\ qexistsl [‘ARB’, ‘ARB’] \\ rw[FUNPOW_Tau_SUC_cyclic_spin]
1658QED
1659
1660Theorem itree_wbisim_strip_tau_cases:
1661 itree_wbisim t t' <=> (t = spin /\ t' = spin) \/
1662 (?r. strip_tau t (Ret r) /\ strip_tau t' (Ret r)) \/
1663 (?e k k'. strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
1664 !l. itree_wbisim (k l) (k' l))
1665Proof
1666 iff_tac
1667 >- (strip_tac
1668 \\ reverse $ Cases_on ‘?t''. strip_tau t t''’ \\ gvs[]
1669 >- (drule strip_tau_spin
1670 \\ metis_tac[wbisim_spin_eq, itree_wbisim_sym]
1671 )
1672 \\ Cases_on ‘t''’ \\ gvs[]
1673 >- (drule_all itree_wbisim_strip_tau_Ret
1674 \\ metis_tac[]
1675 )
1676 \\ drule_all itree_wbisim_strip_tau_Vis
1677 \\ metis_tac[]
1678 )
1679 \\ rpt strip_tac
1680 >- rw[wbisim_spin_eq]
1681 \\ metis_tac[itree_wbisim_rules]
1682QED
1683
1684Theorem after_taus_itree_strong_bisim_spin_spin:
1685 after_taus ($=) t t' ==> t' = spin ==> t = spin
1686Proof
1687 qid_spec_tac ‘t'’
1688 \\ qid_spec_tac ‘t’
1689 \\ ho_match_mp_tac after_taus_strongind
1690 \\ rw[spin, GSYM spin]
1691 \\ ‘Tau t' = Tau spin’ by metis_tac[spin]
1692 \\ gvs[]
1693QED
1694
1695Theorem after_taus_itree_strong_bisim_strip_tau:
1696 after_taus ($=) t t' <=> (?t''. strip_tau t t'' /\ strip_tau t' t'') \/ (t = spin /\ t' = spin)
1697Proof
1698 iff_tac
1699 >- (qid_spec_tac ‘t'’
1700 \\ qid_spec_tac ‘t’
1701 \\ ho_match_mp_tac after_taus_strongind
1702 \\ rw[spin, GSYM spin]
1703 \\ metis_tac[strip_tau_spin, spin]
1704 )
1705 \\ reverse $ rw[]
1706 >- (irule after_taus_rel \\ rw[]
1707 )
1708 \\ imp_res_tac strip_tau_FUNPOW
1709 \\ rw[]
1710 \\ irule after_taus_FUNPOW_TauL
1711 \\ irule after_taus_FUNPOW_TauR
1712 \\ irule after_taus_rel \\ rw[]
1713QED
1714
1715Theorem after_taus_itree_wbisim_spin_spin:
1716 after_taus itree_wbisim t t' ==> t' = spin ==> t = spin
1717Proof
1718 qid_spec_tac ‘t'’
1719 \\ qid_spec_tac ‘t’
1720 \\ ho_match_mp_tac after_taus_strongind
1721 \\ gvs[spin, GSYM spin, wbisim_spin_eq]
1722 \\ rpt strip_tac
1723 \\ ‘Tau t' = Tau spin’ by metis_tac[spin]
1724 \\ gvs[]
1725QED
1726
1727Theorem after_taus_itree_wbisim_itree_wbisim:
1728 after_taus itree_wbisim t t' <=> itree_wbisim t t'
1729Proof
1730 iff_tac
1731 >- (qid_spec_tac ‘t'’
1732 \\ qid_spec_tac ‘t’
1733 \\ ho_match_mp_tac after_taus_strongind
1734 \\ rw[spin, GSYM spin]
1735 )
1736 \\ disch_tac
1737 \\ irule $ cj 1 after_taus_rules
1738 \\ simp[]
1739QED
1740
1741(* strong bisimulation from an instance up to full tree of an abstraction *)
1742CoInductive strong_bisim_upfrom_abs:
1743 (strong_bisim_upfrom_abs (abs, abs') (Ret x) (Ret x)) /\
1744 ((!l. strong_bisim_upfrom_abs (abs, abs') (k l) (k' l) \/ ?r. (k l = (abs r) /\ k' l = (abs' r))) ==>
1745 strong_bisim_upfrom_abs (abs, abs') (Vis e k) (Vis e k')) /\
1746 ((?r. t = (abs r) /\ t' = (abs' r)) ==> strong_bisim_upfrom_abs (abs, abs') (Tau t) (Tau t')) /\
1747 ((strong_bisim_upfrom_abs (abs, abs') t t') ==> (strong_bisim_upfrom_abs (abs, abs') (Tau t) (Tau t')))
1748End
1749
1750Theorem strong_bisim_upfrom_abs_FUNPOW_Tau:
1751 strong_bisim_upfrom_abs (abs, abs') t t' ==>
1752 strong_bisim_upfrom_abs (abs, abs') (FUNPOW Tau n t) (FUNPOW Tau n t')
1753Proof
1754 Induct_on ‘n’ \\ gvs[]
1755 \\ disch_tac
1756 \\ gvs[FUNPOW_SUC]
1757 \\ irule $ cj 4 strong_bisim_upfrom_abs_rules
1758 \\ last_assum $ irule
1759QED
1760
1761Theorem strong_bisim_upfrom_abs_FUNPOW_Tau_SUC_abs:
1762 strong_bisim_upfrom_abs (abs, abs') (FUNPOW Tau (SUC n) (abs r)) (FUNPOW Tau (SUC n) (abs' r))
1763Proof
1764 gvs[FUNPOW]
1765 \\ irule strong_bisim_upfrom_abs_FUNPOW_Tau
1766 \\ metis_tac[strong_bisim_upfrom_abs_rules]
1767QED
1768
1769Theorem strong_bisim_upfrom_abs_strong:
1770 !abs t t'. strong_bisim_upfrom_abs (abs, abs) t t' <=> t = t'
1771Proof
1772 rpt strip_tac
1773 \\ iff_tac
1774 >- (strip_tac
1775 \\ irule $ iffRL itree_strong_bisimulation
1776 \\ qexists ‘CURRY {(t, t') | t, t' | strong_bisim_upfrom_abs (abs, abs) t t'}’ \\ rw[UNCURRY]
1777 \\ drule $ iffLR strong_bisim_upfrom_abs_cases
1778 \\ rw[]
1779 \\ strip_tac
1780 \\ pop_assum $ qspec_then ‘s’ assume_tac
1781 \\ gvs[]
1782 )
1783 \\ rw[]
1784 \\ irule strong_bisim_upfrom_abs_coind
1785 \\ qexists ‘\ap t t'. ap = (abs, abs) /\ t = t'’
1786 \\ rw[]
1787 \\ Cases_on ‘a1’ \\ rw[]
1788QED
1789
1790Theorem cyclic_strong_bisim_upfrom_abs:
1791 (!r. strong_bisim_upfrom_abs (abs, abs') (abs r) (abs' r)) <=> abs = abs'
1792Proof
1793 iff_tac
1794 >- (rpt strip_tac
1795 \\ irule $ iffRL FUN_EQ_THM \\ rw[]
1796 \\ irule $ iffRL itree_strong_bisimulation
1797 \\ qexists ‘CURRY {(t, t') | t, t' | strong_bisim_upfrom_abs (abs, abs') t t'}’ \\ rw[UNCURRY]
1798 \\ drule $ iffLR strong_bisim_upfrom_abs_cases \\ rw[]
1799 \\ metis_tac[]
1800 )
1801 \\ rw[strong_bisim_upfrom_abs_strong]
1802QED
1803
1804Theorem strong_bisim_upfrom_abs_strong_bind:
1805 (!r. strong_bisim_upfrom_abs (abs, abs') (k r) (k' r)) ==>
1806 strong_bisim_upfrom_abs (abs, abs') (itree_bind t k) (itree_bind t k')
1807Proof
1808 rpt strip_tac
1809 \\ irule strong_bisim_upfrom_abs_coind
1810 \\ qexists ‘\ap tk tk'. ap = (abs, abs') /\ ((?t. tk = itree_bind t k /\ tk' = itree_bind t k')
1811 \/ strong_bisim_upfrom_abs (abs, abs') tk tk')’
1812 \\ reverse $ rw[]
1813 >- (disj1_tac
1814 \\ qexists ‘t’ \\ rw[]
1815 )
1816 >- (drule $ iffLR strong_bisim_upfrom_abs_cases
1817 \\ rw[]
1818 \\ metis_tac[]
1819 )
1820 \\ reverse $ Cases_on ‘?t'. strip_tau t t'’ \\ gvs[]
1821 >- (drule strip_tau_spin
1822 \\ rw[]
1823 \\ rw[spin_bind, spin, spin_FUNPOW_Tau]
1824 \\ metis_tac[spin_bind, GSYM spin_FUNPOW_Tau, spin]
1825 )
1826 \\ Cases_on ‘t'’ \\ gvs[]
1827 >- (imp_res_tac strip_tau_FUNPOW
1828 \\ rw[FUNPOW_Tau_bind]
1829 \\ first_x_assum $ qspec_then ‘x’ assume_tac \\ gvs[]
1830 \\ imp_res_tac strong_bisim_upfrom_abs_FUNPOW_Tau
1831 \\ pop_assum $ qspec_then ‘n’ assume_tac
1832 \\ drule $ iffLR strong_bisim_upfrom_abs_cases \\ rw[]
1833 \\ metis_tac[]
1834 )
1835 \\ imp_res_tac strip_tau_FUNPOW
1836 \\ rw[FUNPOW_Tau_bind]
1837 \\ Cases_on ‘n’ \\ gvs[]
1838 >- metis_tac[]
1839 \\ gvs[FUNPOW_SUC]
1840 \\ disj2_tac
1841 \\ disj1_tac
1842 \\ qexists ‘FUNPOW Tau n' (Vis a g)’ \\ rw[FUNPOW_Tau_bind]
1843QED
1844
1845Theorem cyclic_strong_bisim_upfrom_abs_strong_upfrom:
1846 (!r. strong_bisim_upfrom_abs (abs, abs') (abs r) (abs' r)) /\ strong_bisim_upfrom_abs (abs, abs') t t' ==> t = t'
1847Proof
1848 rpt strip_tac
1849 \\ irule $ iffRL itree_bisimulation
1850 \\ qexists ‘CURRY ({(t'', t''') | t'', t''' | (strong_bisim_upfrom_abs (abs, abs') t'' t''')})’ \\ rw[UNCURRY]
1851 \\ drule $ iffLR strong_bisim_upfrom_abs_cases
1852 \\ rw[]
1853 \\ metis_tac[]
1854QED
1855
1856Theorem itree_strong_bisim_upfrom_abs:
1857 strong_bisim_upfrom_abs (abs, abs') t t
1858Proof
1859 irule $ strong_bisim_upfrom_abs_coind
1860 \\ qexists ‘\ap t t'. ap = (abs, abs') /\ t = t'’ \\ rw[]
1861 \\ Cases_on ‘a1’ \\ gvs[]
1862QED
1863
1864(* strong bisimulation from an instance up to full tree of an abstraction *)
1865CoInductive weak_bisim_upfrom_abs:
1866 (strip_tau t (Ret x) /\ strip_tau t' (Ret x) ==> weak_bisim_upfrom_abs (abs, abs') t t') /\
1867 (strip_tau t (Vis e k) /\ strip_tau t' (Vis e k') /\
1868 (!l. weak_bisim_upfrom_abs (abs, abs') (k l) (k' l) \/ k l = FUNPOW Tau n (abs r) /\ k' l = FUNPOW Tau n' (abs' r)) ==>
1869 weak_bisim_upfrom_abs (abs, abs') t t') /\
1870 weak_bisim_upfrom_abs (abs, abs') (FUNPOW Tau (SUC n) (abs r)) (FUNPOW Tau (SUC n') (abs' r)) /\
1871 ((weak_bisim_upfrom_abs (abs, abs') t t') ==> (weak_bisim_upfrom_abs (abs, abs') (FUNPOW Tau (SUC n) t) (FUNPOW Tau (SUC n') t')))
1872End
1873
1874Theorem weak_bisim_upfrom_abs_spin:
1875 weak_bisim_upfrom_abs (abs, abs') spin spin
1876Proof
1877 irule weak_bisim_upfrom_abs_coind
1878 \\ qexists ‘\ap t t'. ap = (abs, abs') /\ t = spin /\ t' = spin’ \\ rw[]
1879 \\ metis_tac[FUNPOW, spin]
1880QED
1881
1882Theorem weak_bisim_upfrom_abs_tauL:
1883 weak_bisim_upfrom_abs (abs, abs') t'' t''' ==>
1884 weak_bisim_upfrom_abs (abs, abs') (Tau t'') t'''
1885Proof
1886 strip_tac
1887 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
1888 \\ rw[]
1889 >- (irule $ cj 1 weak_bisim_upfrom_abs_rules
1890 \\ metis_tac[strip_tau_simps]
1891 )
1892 >- (irule $ cj 2 weak_bisim_upfrom_abs_rules
1893 \\ metis_tac[strip_tau_simps]
1894 )
1895 \\ rw[GSYM FUNPOW_SUC, weak_bisim_upfrom_abs_rules]
1896QED
1897
1898Theorem weak_bisim_upfrom_abs_tauR:
1899 weak_bisim_upfrom_abs (abs, abs') t'' t''' ==>
1900 weak_bisim_upfrom_abs (abs, abs') t'' (Tau t''')
1901Proof
1902 strip_tac
1903 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
1904 \\ rw[]
1905 >- (irule $ cj 1 weak_bisim_upfrom_abs_rules
1906 \\ metis_tac[strip_tau_simps]
1907 )
1908 >- (irule $ cj 2 weak_bisim_upfrom_abs_rules
1909 \\ metis_tac[strip_tau_simps]
1910 )
1911 \\ rw[GSYM FUNPOW_SUC, weak_bisim_upfrom_abs_rules]
1912QED
1913
1914Theorem weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau:
1915 weak_bisim_upfrom_abs (abs, abs') t'' t''' ==>
1916 weak_bisim_upfrom_abs (abs, abs') (FUNPOW Tau n t'') (FUNPOW Tau n' t''')
1917Proof
1918 rpt strip_tac
1919 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
1920 \\ rw[]
1921 >- (irule $ cj 1 weak_bisim_upfrom_abs_rules
1922 \\ ‘itree_wbisim t'' (FUNPOW Tau n t'')’ by rw[FUNPOW_Tau_wbisim, itree_wbisim_sym]
1923 \\ drule_all itree_wbisim_strip_tau_Ret
1924 \\ disch_tac
1925 \\ ‘itree_wbisim t''' (FUNPOW Tau n' t''')’ by rw[FUNPOW_Tau_wbisim, itree_wbisim_sym]
1926 \\ drule_all itree_wbisim_strip_tau_Ret
1927 \\ disch_tac
1928 \\ metis_tac[]
1929 )
1930 >- (irule $ cj 2 weak_bisim_upfrom_abs_rules
1931 \\ imp_res_tac strip_tau_FUNPOW
1932 \\ rw[GSYM FUNPOW_ADD]
1933 \\ qexistsl [‘e’, ‘k’, ‘k'’, ‘n''’, ‘n'''’, ‘r’] \\ rw[strip_tau_FUNPOW_cancel]
1934 )
1935 \\ rw[GSYM FUNPOW_SUC, GSYM FUNPOW_ADD, GSYM ADD_SUC, weak_bisim_upfrom_abs_rules]
1936QED
1937
1938Theorem weak_bisim_upfrom_abs_wbisim_bind:
1939 itree_wbisim t t' /\ (!r. weak_bisim_upfrom_abs (abs, abs') (k r) (k' r)) ==>
1940 weak_bisim_upfrom_abs (abs, abs') (itree_bind t k) (itree_bind t' k')
1941Proof
1942 rpt strip_tac
1943 \\ irule weak_bisim_upfrom_abs_coind
1944 \\ qexists ‘\ap t t'. ap = (abs, abs') /\
1945 ((?t'' t'''.t = itree_bind t'' k /\ t' = itree_bind t''' k'
1946 /\ itree_wbisim t'' t''')
1947 \/ weak_bisim_upfrom_abs (abs, abs') t t')’
1948 \\ reverse $ rw[]
1949 >- (disj1_tac
1950 \\ qexistsl [‘t’, ‘t'’] \\ rw[]
1951 )
1952 >- (drule $ iffLR weak_bisim_upfrom_abs_cases
1953 \\ rw[]
1954 \\ metis_tac[]
1955 )
1956 \\ reverse $ Cases_on ‘?t. strip_tau t''' t’ \\ gvs[]
1957 >- (drule strip_tau_spin
1958 \\ rw[]
1959 \\ drule $ iffLR $ wbisim_spin_eq
1960 \\ rw[spin_bind, spin, spin_FUNPOW_Tau]
1961 \\ metis_tac[weak_bisim_upfrom_abs_spin, spin_bind, GSYM spin_FUNPOW_Tau, spin]
1962 )
1963 \\ Cases_on ‘t''''’ \\ gvs[]
1964 >- (drule itree_wbisim_sym
1965 \\ strip_tac
1966 \\ drule_all itree_wbisim_strip_tau_Ret
1967 \\ strip_tac
1968 \\ imp_res_tac strip_tau_FUNPOW
1969 \\ rw[FUNPOW_Tau_bind]
1970 \\ first_x_assum $ qspec_then ‘x’ assume_tac \\ gvs[]
1971 \\ imp_res_tac weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau
1972 \\ pop_assum $ qspecl_then [‘n'’, ‘n’] assume_tac
1973 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
1974 \\ rw[]
1975 \\ metis_tac[]
1976 )
1977 \\ drule itree_wbisim_sym
1978 \\ strip_tac
1979 \\ drule_all itree_wbisim_strip_tau_Vis
1980 \\ strip_tac
1981 \\ imp_res_tac strip_tau_FUNPOW
1982 \\ rw[FUNPOW_Tau_bind]
1983 \\ disj2_tac
1984 \\ disj1_tac
1985 \\ qexistsl [‘a’, ‘\x. itree_bind (k'' x) k’, ‘\x. itree_bind (g x) k'’, ‘n’, ‘n'’] \\ rw[strip_tau_FUNPOW_cancel]
1986 \\ metis_tac[itree_wbisim_sym]
1987QED
1988
1989Theorem itree_wbisim_weak_upfrom_abs:
1990 itree_wbisim t' t'' ==> weak_bisim_upfrom_abs (abs, abs) t' t''
1991Proof
1992 disch_tac
1993 \\ irule weak_bisim_upfrom_abs_coind
1994 \\ qexists ‘\ap t t'. ap = (abs, abs) /\ itree_wbisim t t'’
1995 \\ rw[]
1996 \\ reverse $ Cases_on ‘?x. strip_tau a1 x’ \\ gvs[]
1997 >- (drule strip_tau_spin \\ rw[]
1998 \\ ‘a2 = spin’ by metis_tac[wbisim_spin_eq, itree_wbisim_sym]
1999 \\ metis_tac[spin_FUNPOW_Tau]
2000 )
2001 \\ Cases_on ‘x’ \\ gvs[]
2002 >- (subgoal ‘strip_tau a2 (Ret x')’
2003 >- (irule itree_wbisim_strip_tau_Ret
2004 \\ metis_tac[]
2005 )
2006 \\ imp_res_tac strip_tau_FUNPOW
2007 \\ metis_tac[]
2008 )
2009 \\ qspecl_then [‘a1’, ‘a2’, ‘a’, ‘g’] assume_tac itree_wbisim_strip_tau_Vis
2010 \\ gvs[]
2011 \\ imp_res_tac strip_tau_FUNPOW
2012 \\ metis_tac[]
2013QED
2014
2015Theorem weak_bisim_upfrom_weak_abs:
2016 weak_bisim_upfrom_abs (abs, abs) t' t'' <=> itree_wbisim t' t''
2017Proof
2018 reverse $ iff_tac
2019 >- fs[itree_wbisim_weak_upfrom_abs]
2020 \\ strip_tac
2021 \\ irule itree_wbisim_strong_coind
2022 \\ qexists ‘CURRY {(t', t'') | t', t'' | weak_bisim_upfrom_abs (abs, abs) t' t''}’ \\ reverse $ rw[UNCURRY]
2023 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
2024 \\ rw[]
2025 \\ rpt strip_tac
2026 >- (ntac 2 disj2_tac
2027 \\ qexists ‘x’ \\ gvs[strip_tau_FUNPOW_cancel]
2028 )
2029 >- (disj2_tac
2030 \\ disj1_tac
2031 \\ qexistsl [‘e’, ‘k’, ‘k'’] \\ rw[strip_tau_FUNPOW_cancel]
2032 \\ pop_assum $ qspec_then ‘r'’ assume_tac \\ rw[]
2033 >- rw[FUNPOW_Tau_wbisim, itree_wbisim_sym]
2034 \\ rw[]
2035 \\ disj2_tac
2036 \\ irule FUNPOW_Tau_wbisim_intro
2037 \\ irule itree_wbisim_refl
2038 )
2039 >- (rw[FUNPOW_SUC]
2040 \\ metis_tac[FUNPOW_Tau_wbisim_intro, itree_wbisim_refl]
2041 )
2042 \\ rw[FUNPOW_SUC, weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau]
2043QED
2044
2045Theorem cyclic_weak_bisim_upfrom_abs:
2046 (!r. weak_bisim_upfrom_abs (abs, abs') (abs r) (abs' r)) <=> (!r. itree_wbisim (abs r) (abs' r))
2047Proof
2048 iff_tac
2049 >- (rpt strip_tac
2050 \\ irule itree_wbisim_coind_upto
2051 \\ qexists ‘CURRY ({(t'', t''') | t'', t''' | (weak_bisim_upfrom_abs (abs, abs') t'' t''')})’ \\ rw[UNCURRY]
2052 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
2053 \\ rw[]
2054 \\ rpt strip_tac
2055 >- metis_tac[]
2056 >- (disj2_tac
2057 \\ disj1_tac
2058 \\ qexistsl [‘e’, ‘k’, ‘k'’] \\ rw[strip_tau_FUNPOW_cancel]
2059 \\ pop_assum $ qspec_then ‘r'’ assume_tac \\ reverse $ rw[] \\ rw[]
2060 \\ disj1_tac
2061 \\ irule weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau
2062 \\ metis_tac[]
2063 )
2064 \\ gvs[FUNPOW_SUC, weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau]
2065 )
2066 \\ rpt strip_tac
2067 \\ irule $ weak_bisim_upfrom_abs_coind
2068 \\ qexists ‘\ap t t'. ap = (abs, abs') /\ itree_wbisim t t'’ \\ rw[]
2069 \\ drule $ iffLR itree_wbisim_strip_tau_cases
2070 \\ rw[]
2071 \\ metis_tac[FUNPOW_Tau_SUC_cyclic_spin, itree_wbisim_refl]
2072QED
2073
2074Theorem cyclic_weak_bisim_upfrom_abs_weak_upfrom:
2075 (!r. weak_bisim_upfrom_abs (abs, abs') (abs r) (abs' r)) /\ weak_bisim_upfrom_abs (abs, abs') t t' ==> itree_wbisim t t'
2076Proof
2077 rpt strip_tac
2078 \\ irule itree_wbisim_coind_upto
2079 \\ qexists ‘CURRY ({(t'', t''') | t'', t''' | (weak_bisim_upfrom_abs (abs, abs') t'' t''')})’ \\ rw[UNCURRY]
2080 \\ drule $ iffLR weak_bisim_upfrom_abs_cases
2081 \\ rw[]
2082 \\ rpt strip_tac
2083 >- metis_tac[]
2084 >- (disj2_tac
2085 \\ disj1_tac
2086 \\ qexistsl [‘e’, ‘k’, ‘k'’] \\ rw[strip_tau_FUNPOW_cancel]
2087 \\ pop_assum $ qspec_then ‘r'’ assume_tac \\ reverse $ rw[] \\ rw[]
2088 \\ disj1_tac
2089 \\ irule weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau
2090 \\ metis_tac[]
2091 )
2092 \\ gvs[FUNPOW_SUC, weak_bisim_upfrom_cyclic_abs_FUNPOW_Tau]
2093QED
2094
2095Theorem itree_wbisim_weak_bisim_upfrom_abs:
2096 itree_wbisim t t' ==> weak_bisim_upfrom_abs (abs, abs') t t'
2097Proof
2098 rpt strip_tac
2099 \\ irule $ weak_bisim_upfrom_abs_coind
2100 \\ qexists ‘\ap t t'. ap = (abs, abs') /\ itree_wbisim t t'’ \\ rw[]
2101 \\ drule $ iffLR itree_wbisim_strip_tau_cases
2102 \\ rw[]
2103 \\ metis_tac[FUNPOW_Tau_SUC_cyclic_spin, itree_wbisim_refl]
2104QED
2105
2106Overload itree_el = ``itree_rep``;
2107
2108(* tidy up theory exports *)
2109
2110val _ = List.app Theory.delete_binding
2111 ["Ret_rep_def", "Ret_def",
2112 "Tau_rep_def", "Tau_def",
2113 "Vis_rep_def", "Vis_def",
2114 "path_ok_def", "itree_rep_ok_def",
2115 "itree_unfold_path_def", "itree_unfold_path_ind",
2116 "itree_el_TY_DEF", "itree_absrep", "itree_next_TY_DEF"];