pathScript.sml
1Theory path
2Ancestors
3 llist fixedPoint[qualified] rich_list[qualified]
4Libs
5 BasicProvers metisLib pred_setLib[qualified]
6
7val _ = augment_srw_ss [rewrites [LET_THM]]
8
9val path_TY_DEF = new_type_definition (
10 "path",
11 prove(``?x :('a # ('b # 'a) llist). (\x. T) x``,
12 BETA_TAC THEN REWRITE_TAC [EXISTS_SIMP]));
13
14val path_absrep_bijections =
15 define_new_type_bijections { ABS = "toPath", REP = "fromPath",
16 name = "path_absrep_bijections",
17 tyax = path_TY_DEF};
18
19Theorem path_rep_bijections_thm =
20 REWRITE_RULE [] (BETA_RULE path_absrep_bijections);
21
22Theorem toPath_11 =
23 REWRITE_RULE [] (BETA_RULE (prove_abs_fn_one_one path_absrep_bijections));
24Theorem fromPath_11 =
25 prove_rep_fn_one_one path_absrep_bijections;
26
27
28Theorem fromPath_onto =
29 REWRITE_RULE [] (BETA_RULE (prove_rep_fn_onto path_absrep_bijections));
30Theorem toPath_onto =
31 SIMP_RULE std_ss [] (prove_abs_fn_onto path_absrep_bijections);
32
33val _ = augment_srw_ss [rewrites [path_rep_bijections_thm,
34 toPath_11, fromPath_11]]
35
36Theorem path_eq_fromPath[local]:
37 !p q. (p = q) = (fromPath p = fromPath q)
38Proof
39 SRW_TAC [][]
40QED
41
42Theorem forall_path[local]:
43 (!p. P p) = !r. P (toPath r)
44Proof
45 SRW_TAC [][EQ_IMP_THM] THEN PROVE_TAC [toPath_onto]
46QED
47Theorem exists_path[local]:
48 (?p. P p) = ?r. P (toPath r)
49Proof
50 SRW_TAC [][EQ_IMP_THM] THEN PROVE_TAC [toPath_onto]
51QED
52
53Definition first_def: first (p:('a,'b) path) = FST (fromPath p)
54End
55Definition stopped_at_def: stopped_at x:('a,'b) path = toPath (x, LNIL)
56End
57Definition pcons_def:
58 pcons x r p : ('a,'b) path =
59 toPath (x, LCONS (r, first p) (SND (fromPath p)))
60End
61
62Theorem stopped_at_11[simp]:
63 !x y. (stopped_at x = stopped_at y : ('a,'b) path) = (x = y)
64Proof
65 SRW_TAC [][stopped_at_def]
66QED
67
68Theorem pcons_11[simp]:
69 !x r p y s q.
70 (pcons x r p = pcons y s q) <=> (x = y) /\ (r = s) /\ (p = q)
71Proof
72 SRW_TAC [][pcons_def, first_def] THEN
73 REWRITE_TAC [path_eq_fromPath, pairTheory.PAIR_FST_SND_EQ, CONJ_ASSOC]
74QED
75
76Theorem stopped_at_not_pcons[simp]:
77 !x y r p. ~(stopped_at x = pcons y r p) /\ ~(pcons y r p = stopped_at x)
78Proof
79 SRW_TAC [][stopped_at_def, pcons_def]
80QED
81
82Theorem path_cases:
83 !p. (?x. p = stopped_at x) \/ (?x r q. p = pcons x r q)
84Proof
85 SIMP_TAC (srw_ss()) [stopped_at_def, pcons_def, forall_path,
86 exists_path, first_def, pairTheory.EXISTS_PROD,
87 pairTheory.FORALL_PROD] THEN
88 PROVE_TAC [pairTheory.ABS_PAIR_THM, llistTheory.llist_CASES]
89QED
90
91Theorem FORALL_path:
92 !P. (!p. P p) <=> (!x. P (stopped_at x)) /\ (!x r p. P (pcons x r p))
93Proof
94 GEN_TAC THEN EQ_TAC THEN SRW_TAC [][] THEN
95 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN SRW_TAC [][]
96QED
97
98Theorem EXISTS_path:
99 !P. (?p. P p) <=> (?x. P (stopped_at x)) \/ (?x r p. P (pcons x r p))
100Proof
101 SRW_TAC [][EQ_IMP_THM] THEN1
102 (Q.SPEC_THEN `p` FULL_STRUCT_CASES_TAC path_cases THEN METIS_TAC []) THEN
103 METIS_TAC []
104QED
105
106Theorem first_thm[simp]:
107 (!x. first (stopped_at x : ('a,'b) path) = x) /\
108 (!x r p. first (pcons x r p : ('a,'b) path) = x)
109Proof
110 SRW_TAC [][first_def, stopped_at_def, pcons_def]
111QED
112
113Definition finite_def:
114 finite (sigma : ('a,'b) path) = LFINITE (SND (fromPath sigma))
115End
116
117Overload "infinite" = “\p. ~finite p”
118
119Theorem finite_thm[simp]:
120 (!x. finite (stopped_at x : ('a,'b) path) = T) /\
121 (!x r p. finite (pcons x r p : ('a,'b) path) = finite p)
122Proof
123 SRW_TAC [][finite_def, pcons_def, stopped_at_def, llistTheory.LFINITE_THM]
124QED
125
126
127val last_thm =
128 new_specification
129 ("last_thm", ["last"],
130 prove(
131 ``?f. (!x. f (stopped_at x) = x) /\
132 (!x r p. f (pcons x r p) = f p)``,
133 Q.EXISTS_TAC `\p. if finite p then
134 if SND (fromPath p) = LNIL then first p
135 else SND (LAST (THE (toList (SND (fromPath p)))))
136 else ARB` THEN
137 SRW_TAC [][finite_def, stopped_at_def, first_def, pcons_def,
138 toList_THM, LFINITE_THM] THEN
139 IMP_RES_TAC LFINITE_toList THEN
140 `?h t. SND (fromPath p) = LCONS h t` by PROVE_TAC [llist_CASES] THEN
141 FULL_SIMP_TAC (srw_ss()) [toList_THM]));
142
143val _ = export_rewrites ["last_thm"]
144
145Theorem path_bisimulation:
146 !p1 p2.
147 (p1 = p2) =
148 ?R. R p1 p2 /\
149 !q1 q2.
150 R q1 q2 ==>
151 (?x. (q1 = stopped_at x) /\ (q2 = stopped_at x)) \/
152 (?x r q1' q2'.
153 (q1 = pcons x r q1') /\ (q2 = pcons x r q2') /\
154 R q1' q2')
155Proof
156 SIMP_TAC (srw_ss()) [pcons_def, stopped_at_def, pairTheory.FORALL_PROD,
157 EQ_IMP_THM, FORALL_AND_THM, forall_path,
158 GSYM LEFT_FORALL_IMP_THM] THEN
159 CONJ_TAC THENL [
160 REPEAT GEN_TAC THEN
161 Q.REFINE_EXISTS_TAC `\p q. R' (SND (fromPath p)) (SND (fromPath q)) /\
162 (first p = first q)` THEN
163 SRW_TAC [][first_def] THEN
164 Q.ISPECL_THEN [`p_2`,`p_2`] (STRIP_ASSUME_TAC o
165 REWRITE_RULE []) LLIST_BISIMULATION THEN
166 Q.EXISTS_TAC `R` THEN SRW_TAC [][] THEN
167 Q.ISPEC_THEN `p_2''` (STRIP_ALL_THEN SUBST_ALL_TAC)
168 llist_CASES THEN
169 SRW_TAC [][] THEN
170 Q.ISPEC_THEN `p_2'''` (STRIP_ALL_THEN SUBST_ALL_TAC)
171 llist_CASES THEN SRW_TAC [][]
172 THENL [
173 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [LHD_THM],
174 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [LHD_THM],
175 `(LHD (LCONS h t) = LHD (LCONS h' t')) /\
176 R (THE (LTL (LCONS h t))) (THE (LTL (LCONS h' t')))` by
177 PROVE_TAC [llistTheory.LCONS_NOT_NIL] THEN
178 FULL_SIMP_TAC (srw_ss()) [LHD_THM, LTL_THM] THEN
179 Cases_on `h` THEN SRW_TAC [][] THEN
180 MAP_EVERY Q.EXISTS_TAC [`toPath (r, t)`, `toPath (r, t')`] THEN
181 SRW_TAC [][]
182 ],
183
184 REPEAT STRIP_TAC THENL [
185 RES_TAC THEN SRW_TAC [][],
186 ONCE_REWRITE_TAC [LLIST_BISIMULATION] THEN
187 Q.EXISTS_TAC `\x y. ?x' y'. R (toPath (x', x)) (toPath (y', y))` THEN
188 SRW_TAC [][] THENL [
189 PROVE_TAC [],
190 `(ll3 = LNIL) /\ (ll4 = LNIL) \/
191 ?r q1' q2'. (ll3 = LCONS (r, first q1') (SND (fromPath q1'))) /\
192 (ll4 = LCONS (r, first q2') (SND (fromPath q2'))) /\
193 (x' = y') /\ R q1' q2'`
194 by (RES_TAC THEN SRW_TAC [][] THEN
195 PROVE_TAC [])
196 THENL [
197 SRW_TAC [][],
198 SRW_TAC [][LHD_THM, LTL_THM] THENL [
199 `?q11 q12 q21 q22. (q1' = toPath (q11, q12)) /\
200 (q2' = toPath (q21, q22))` by
201 PROVE_TAC [toPath_onto, pairTheory.ABS_PAIR_THM] THEN
202 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN
203 RES_TAC THEN SRW_TAC [][first_def],
204 MAP_EVERY Q.EXISTS_TAC [`FST (fromPath q1')`,
205 `FST (fromPath q2')`] THEN
206 SRW_TAC [][]
207 ]
208 ]
209 ]
210 ]
211 ]
212QED
213
214Theorem finite_path_ind:
215 !P. (!x. P (stopped_at x)) /\
216 (!x r p. finite p /\ P p ==> P (pcons x r p)) ==>
217 (!q. finite q ==> P q)
218Proof
219 GEN_TAC THEN STRIP_TAC THEN
220 SIMP_TAC (srw_ss()) [forall_path, pairTheory.FORALL_PROD, finite_def] THEN
221 Q_TAC SUFF_TAC
222 `(!pl. LFINITE pl ==> !x. P (toPath (x, pl)))` THEN1 PROVE_TAC [] THEN
223 HO_MATCH_MP_TAC LFINITE_STRONG_INDUCTION THEN
224 FULL_SIMP_TAC (srw_ss()) [finite_def, pcons_def, stopped_at_def,
225 pairTheory.FORALL_PROD, first_def, forall_path]
226QED
227
228
229Definition pmap_def:
230 pmap f g (p:('a,'b) path):('c,'d) path =
231 toPath ((f ## LMAP (g ## f)) (fromPath p))
232End
233
234Theorem pmap_thm[simp]:
235 (!x. pmap f g (stopped_at x) = stopped_at (f x)) /\
236 (!x r p.
237 pmap f g (pcons x r p) = pcons (f x) (g r) (pmap f g p))
238Proof
239 SRW_TAC [][pmap_def, stopped_at_def, pcons_def, first_def]
240QED
241
242Theorem first_pmap[simp]:
243 !p. first (pmap f g p) = f (first p)
244Proof
245 CONV_TAC (HO_REWR_CONV FORALL_path) THEN SRW_TAC [][]
246QED
247
248Theorem last_pmap[simp]:
249 !p. finite p ==> (last (pmap f g p) = f (last p))
250Proof
251 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][]
252QED
253
254Theorem finite_pmap[simp]:
255 !(f:'a -> 'c) (g:'b -> 'd) p. finite (pmap f g p) = finite p
256Proof
257 Q_TAC SUFF_TAC
258 `(!p. finite p ==> !(f:'a -> 'c) (g:'b -> 'd). finite (pmap f g p)) /\
259 (!p. finite p ==> !(f:'a -> 'c) (g:'b -> 'd) p0. (
260 p = pmap f g p0) ==> finite p0)`
261 THEN1 METIS_TAC [] THEN
262 CONJ_TAC THEN HO_MATCH_MP_TAC finite_path_ind THEN
263 SRW_TAC [][] THEN
264 Q.ISPEC_THEN `p0` (STRIP_ALL_THEN SUBST_ALL_TAC)
265 path_cases THEN
266 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
267QED
268
269
270
271val tail_def =
272 new_specification
273 ("tail_def", ["tail"],
274 prove(``?f. !x r p. f (pcons x r p) = p``,
275 Q.EXISTS_TAC `\p. if ?x r q. p = pcons x r q then
276 @q. ?x r. p = pcons x r q
277 else ARB` THEN
278 SRW_TAC [][]));
279
280val _ = export_rewrites ["tail_def"]
281
282val first_label_def =
283 new_specification
284 ("first_label_def",["first_label"],
285 prove(``?f. !x r p. f (pcons x r p) = r``,
286 Q.EXISTS_TAC `\p. if ?x r q. p = pcons x r q then
287 @r. ?x q. p = pcons x r q
288 else ARB` THEN SRW_TAC [][]));
289
290val _ = export_rewrites ["first_label_def"]
291
292
293(* ----------------------------------------------------------------------
294 length : ('a,'b) path -> num option
295 NONE indicates an infinite path
296 SOME n indicates a path with n states, and n - 1 transitions
297 ---------------------------------------------------------------------- *)
298
299Definition length_def:
300 length p = if finite p then
301 SOME (LENGTH (THE (toList (SND (fromPath p)))) + 1)
302 else NONE
303End
304
305Theorem length_thm:
306 (!x. length (stopped_at x) = SOME 1) /\
307 (!x r p. length (pcons x r p) =
308 if finite p then SOME (THE (length p) + 1)
309 else NONE)
310Proof
311 SRW_TAC [][length_def, finite_def, stopped_at_def, pcons_def, toList_THM,
312 LFINITE_THM] THEN
313 IMP_RES_TAC LFINITE_toList THEN
314 SRW_TAC [numSimps.ARITH_ss][]
315QED
316
317Theorem alt_length_thm:
318 (!x. length (stopped_at x) = SOME 1) /\
319 (!x r p. length (pcons x r p) = OPTION_MAP SUC (length p))
320Proof
321 SRW_TAC [][length_def, finite_def, stopped_at_def, pcons_def, toList_THM,
322 LFINITE_THM] THEN
323 IMP_RES_TAC LFINITE_toList THEN
324 SRW_TAC [numSimps.ARITH_ss][]
325QED
326
327Theorem length_never_zero:
328 !p. ~(length p = SOME 0)
329Proof
330 GEN_TAC THEN
331 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN
332 SRW_TAC [][alt_length_thm]
333QED
334
335Theorem finite_length_lemma[local]:
336 !p. finite p = ?n. length p = SOME n
337Proof
338 SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
339 HO_MATCH_MP_TAC finite_path_ind THEN
340 SRW_TAC [][length_thm],
341 SIMP_TAC (srw_ss()) [GSYM LEFT_FORALL_IMP_THM] THEN
342 Induct_on `n` THEN GEN_TAC THEN
343 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN
344 SRW_TAC [][length_thm]
345 ]
346QED
347
348
349Theorem finite_length:
350 !p. (finite p = (?n. length p = SOME n)) /\
351 (~finite p = (length p = NONE))
352Proof
353 PROVE_TAC [finite_length_lemma, optionTheory.option_CASES,
354 optionTheory.NOT_NONE_SOME]
355QED
356
357Theorem length_cases :
358 !p. (finite p <=> (?n. length p = SOME (SUC n))) /\
359 (~finite p <=> (length p = NONE))
360Proof
361 rw [finite_length]
362 >> reverse EQ_TAC >> rw []
363 >- (Q.EXISTS_TAC ‘SUC n’ >> rw [])
364 >> Cases_on ‘n’ >- fs [length_never_zero]
365 >> rename1 ‘length p = SOME (SUC n1)’
366 >> Q.EXISTS_TAC ‘n1’ >> rw []
367QED
368
369Theorem length_pmap[simp]:
370 !f g p. length (pmap f g p) = length p
371Proof
372 REPEAT GEN_TAC THEN Cases_on `finite p` THENL [
373 Q_TAC SUFF_TAC `!p. finite p ==> (length (pmap f g p) = length p)` THEN1
374 METIS_TAC [] THEN
375 HO_MATCH_MP_TAC finite_path_ind THEN
376 SRW_TAC [][length_thm],
377 `~finite (pmap f g p)` by METIS_TAC [finite_pmap] THEN
378 METIS_TAC [finite_length]
379 ]
380QED
381
382(* ----------------------------------------------------------------------
383 el : num -> ('a, 'b) path -> 'a
384
385 return the nth state, counting from zero. To be a valid index,
386 n must be IN PL p.
387 ---------------------------------------------------------------------- *)
388
389Definition el_def[simp]:
390 (el 0 p = first p) /\ (el (SUC n) p = el n (tail p))
391End
392
393(* ----------------------------------------------------------------------
394 nth_label : num -> ('a,'b) path -> 'b
395
396 returns the nth label, counting from zero up. To be a valid index,
397 n + 1 must be in PL p.
398 ---------------------------------------------------------------------- *)
399
400Definition nth_label_def[simp]:
401 (nth_label 0 p = first_label p) /\
402 (nth_label (SUC n) p = nth_label n (tail p))
403End
404
405Theorem path_Axiom:
406 !f: 'a -> 'b # ('c # 'a) option.
407 ?g : 'a -> ('b, 'c) path.
408 !x. g x = case f x of
409 (y, NONE) => stopped_at y
410 | (y, SOME (l, v)) => pcons y l (g v)
411Proof
412 GEN_TAC THEN
413 STRIP_ASSUME_TAC
414 (Q.ISPEC `λ(x:'a,ks:'c option).
415 case ks of
416 NONE => NONE
417 | SOME k => (case f x : 'b # ('c # 'a) option of
418 (y, NONE) => SOME((x, NONE), (k,y))
419 | (y, SOME (l, v)) => SOME((v, SOME l), (k,y)))`
420 llist_Axiom) THEN
421 Q.EXISTS_TAC `\x. case f x of
422 (y, NONE) => stopped_at y
423 | (y, SOME (l, v)) => toPath (y, g (v, SOME l))` THEN
424 SRW_TAC [][] THEN
425 `?y lvs. f x = (y, lvs)` by PROVE_TAC [pairTheory.ABS_PAIR_THM] THEN
426 SRW_TAC [][] THEN
427 `(lvs = NONE) \/ (?l v. lvs = SOME(l, v))` by
428 PROVE_TAC [pairTheory.ABS_PAIR_THM, optionTheory.option_CASES] THEN
429 SRW_TAC [][] THEN
430 SRW_TAC [][pcons_def] THEN
431 ASM_SIMP_TAC (srw_ss()) [LHDTL_EQ_SOME] THEN
432 `?u lvt. f v = (u, lvt)` by PROVE_TAC [pairTheory.ABS_PAIR_THM] THEN
433 ASM_SIMP_TAC (srw_ss()) [] THEN
434 `(lvt = NONE) \/ (?m t. lvt = SOME (m, t))` by
435 PROVE_TAC [pairTheory.ABS_PAIR_THM, optionTheory.option_CASES] THEN
436 ASM_SIMP_TAC (srw_ss()) [] THENL [
437 SRW_TAC [][stopped_at_def] THEN
438 Q_TAC SUFF_TAC `LHD (g (v, NONE)) = NONE` THEN1
439 PROVE_TAC [LHD_EQ_NONE] THEN
440 ASM_SIMP_TAC std_ss [],
441 ASM_SIMP_TAC (srw_ss()) [first_def]
442 ]
443QED
444
445
446Definition pconcat_def:
447 pconcat p1 lab p2 =
448 toPath (first p1, LAPPEND (SND (fromPath p1))
449 (LCONS (lab,first p2)
450 (SND (fromPath p2))))
451End
452
453Theorem pconcat_thm:
454 (!x lab p2. pconcat (stopped_at x) lab p2 = pcons x lab p2) /\
455 (!x r p lab p2.
456 pconcat (pcons x r p) lab p2 = pcons x r (pconcat p lab p2))
457Proof
458 SRW_TAC [][pconcat_def, pcons_def, first_def, stopped_at_def]
459QED
460
461Theorem pconcat_eq_stopped:
462 !p1 lab p2 x. ~(pconcat p1 lab p2 = stopped_at x) /\
463 ~(stopped_at x = pconcat p1 lab p2)
464Proof
465 GEN_TAC THEN
466 Q.ISPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN
467 SRW_TAC [][pconcat_thm]
468QED
469
470Theorem pconcat_eq_pcons:
471 !x r p p1 lab p2.
472 ((pconcat p1 lab p2 = pcons x r p) <=>
473 (lab = r) /\ (p1 = stopped_at x) /\ (p = p2) \/
474 (?p1'. (p1 = pcons x r p1') /\ (p = pconcat p1' lab p2))) /\
475 ((pcons x r p = pconcat p1 lab p2) <=>
476 (lab = r) /\ (p1 = stopped_at x) /\ (p = p2) \/
477 (?p1'. (p1 = pcons x r p1') /\ (p = pconcat p1' lab p2)))
478Proof
479 REPEAT GEN_TAC THEN
480 Q.ISPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN
481 SRW_TAC [][pconcat_thm] THEN PROVE_TAC []
482QED
483
484Theorem finite_pconcat:
485 !p1 lab p2. finite (pconcat p1 lab p2) <=> finite p1 /\ finite p2
486Proof
487 Q_TAC SUFF_TAC
488 `(!p1 : ('a,'b) path.
489 finite p1 ==>
490 !lab p2. finite p2 ==> finite (pconcat p1 lab p2)) /\
491 (!p : ('a, 'b) path.
492 finite p ==> !p1 p2 lab. (p = pconcat p1 lab p2) ==>
493 finite p1 /\ finite p2)` THEN1
494 PROVE_TAC [] THEN
495 CONJ_TAC THEN HO_MATCH_MP_TAC finite_path_ind THEN
496 SRW_TAC [][pconcat_thm, pconcat_eq_stopped,
497 pconcat_eq_pcons] THEN
498 SRW_TAC [][] THEN PROVE_TAC []
499QED
500
501(* ----------------------------------------------------------------------
502 PL : ('a,'b) path -> num set
503
504 PL(p) returns the set of valid indices into a path, where the index
505 is going to extract a state. When extracting labels (with nth_label),
506 index + 1 must be in PL set for the path. E.g., it's only valid to
507 talk about the 0th label, if the list is two states long, and thus
508 accepts indices {0, 1}.
509 ---------------------------------------------------------------------- *)
510
511Definition PL_def: PL p = { i | finite p ==> i < THE (length p) }
512End
513
514Theorem infinite_PL:
515 !p. ~finite p ==> !i. i IN PL p
516Proof
517 SRW_TAC [][PL_def]
518QED
519
520Theorem PL_pcons:
521 !x r q. PL (pcons x r q) = 0 INSERT IMAGE SUC (PL q)
522Proof
523 SRW_TAC [ARITH_ss]
524 [PL_def, pred_setTheory.EXTENSION, length_thm,
525 EQ_IMP_THM, arithmeticTheory.ADD1]
526 THENL [
527 Cases_on `x'` THEN
528 SRW_TAC [ARITH_ss][arithmeticTheory.ADD1] THEN
529 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [],
530 DECIDE_TAC,
531 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []
532 ]
533QED
534
535Theorem PL_stopped_at:
536 !x. PL (stopped_at x) = {0}
537Proof
538 SRW_TAC [ARITH_ss][pred_setTheory.EXTENSION, PL_def, length_thm]
539QED
540
541Theorem PL_thm[simp] = CONJ PL_stopped_at PL_pcons;
542
543Theorem PL_0[simp]:
544 !p. 0 IN PL p
545Proof
546 CONV_TAC (HO_REWR_CONV FORALL_path) THEN SRW_TAC [][]
547QED
548
549
550Theorem PL_downward_closed:
551 !i p. i IN PL p ==> !j. j < i ==> j IN PL p
552Proof
553 SRW_TAC [][PL_def] THEN PROVE_TAC [arithmeticTheory.LESS_TRANS]
554QED
555
556
557Theorem PL_pmap[simp]:
558 PL (pmap f g p) = PL p
559Proof
560 SRW_TAC [][PL_def, length_pmap, pred_setTheory.EXTENSION]
561QED
562
563Theorem el_pmap[simp]:
564 !i p. i IN PL p ==> (el i (pmap f g p) = f (el i p))
565Proof
566 Induct THEN CONV_TAC (HO_REWR_CONV FORALL_path) THEN SRW_TAC [][]
567QED
568
569Theorem nth_label_pmap[simp]:
570 !i p. SUC i IN PL p ==> (nth_label i (pmap f g p) = g (nth_label i p))
571Proof
572 Induct THEN GEN_TAC THEN
573 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN
574 SRW_TAC [][]
575QED
576
577(* ---------------------------------------------------------------------- *)
578
579Definition firstP_at_def:
580 firstP_at P p i <=> i IN PL p /\ P (el i p) /\ !j. j < i ==> ~P(el j p)
581End
582
583Theorem firstP_at_stopped[local]:
584 !P x n. firstP_at P (stopped_at x) n <=> (n = 0) /\ P x
585Proof
586 SIMP_TAC (srw_ss() ++ ARITH_ss) [firstP_at_def, EQ_IMP_THM,
587 FORALL_AND_THM]
588QED
589
590Theorem firstP_at_pcons[local]:
591 !P n x r p.
592 firstP_at P (pcons x r p) n <=>
593 (n = 0) /\ P x \/ 0 < n /\ ~P x /\ firstP_at P p (n - 1)
594Proof
595 REPEAT GEN_TAC THEN Cases_on `n` THENL [
596 SRW_TAC [ARITH_ss][firstP_at_def, PL_pcons],
597 SRW_TAC [ARITH_ss][firstP_at_def, PL_pcons, EQ_IMP_THM]
598 THENL [
599 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
600 SRW_TAC [ARITH_ss][],
601 FIRST_X_ASSUM (Q.SPEC_THEN `SUC j` MP_TAC) THEN
602 SRW_TAC [ARITH_ss][],
603 Cases_on `j` THEN SRW_TAC [ARITH_ss][]
604 ]
605 ]
606QED
607
608Theorem firstP_at_thm =
609 CONJ firstP_at_stopped firstP_at_pcons;
610
611
612
613Theorem firstP_at_zero:
614 !P p. firstP_at P p 0 = P (first p)
615Proof
616 GEN_TAC THEN CONV_TAC (HO_REWR_CONV FORALL_path) THEN
617 SIMP_TAC (srw_ss()) [firstP_at_thm]
618QED
619
620Definition exists_def: exists P p = ?i. firstP_at P p i
621End
622Definition every_def: every P p = ~exists ($~ o P) p
623End
624
625Theorem exists_thm[simp]:
626 !P. (!x. exists P (stopped_at x) = P x) /\
627 (!x r p. exists P (pcons x r p) <=> P x \/ exists P p)
628Proof
629 SRW_TAC [][exists_def, firstP_at_thm, EQ_IMP_THM, EXISTS_OR_THM] THEN
630 SRW_TAC [][] THENL [
631 PROVE_TAC [],
632 Cases_on `P x` THEN SRW_TAC [][] THEN
633 Q.EXISTS_TAC `SUC i` THEN SRW_TAC [ARITH_ss][]
634 ]
635QED
636
637Theorem every_thm[simp]:
638 !P. (!x. every P (stopped_at x) = P x) /\
639 (!x r p. every P (pcons x r p) <=> P x /\ every P p)
640Proof SRW_TAC [][every_def, exists_thm]
641QED
642
643Theorem not_every[simp]:
644 !P p. ~every P p = exists ($~ o P) p
645Proof
646 SRW_TAC [][every_def]
647QED
648
649Theorem not_exists[simp]:
650 !P p. ~exists P p = every ($~ o P) p
651Proof
652 SRW_TAC [boolSimps.ETA_ss][every_def, combinTheory.o_DEF]
653QED
654
655
656Theorem exists_el:
657 !P p. exists P p = ?i. i IN PL p /\ P (el i p)
658Proof
659 SRW_TAC [][exists_def, firstP_at_def] THEN EQ_TAC THENL [
660 PROVE_TAC [],
661 DISCH_THEN (STRIP_ASSUME_TAC o CONV_RULE numLib.EXISTS_LEAST_CONV) THEN
662 PROVE_TAC [PL_downward_closed]
663 ]
664QED
665
666Theorem every_el:
667 !P p. every P p = !i. i IN PL p ==> P (el i p)
668Proof
669 REWRITE_TAC [every_def, exists_el] THEN SRW_TAC [][] THEN PROVE_TAC []
670QED
671
672Theorem every_coinduction:
673 !P Q. (!x. P (stopped_at x) ==> Q x) /\
674 (!x r p. P (pcons x r p) ==> Q x /\ P p) ==>
675 (!p. P p ==> every Q p)
676Proof
677 REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [every_def, exists_def] THEN
678 SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN
679 CONV_TAC SWAP_VARS_CONV THEN Induct THEN
680 CONV_TAC (HO_REWR_CONV FORALL_path) THENL [
681 SRW_TAC [][firstP_at_thm, combinTheory.o_THM] THEN PROVE_TAC [],
682 SRW_TAC [ARITH_ss][firstP_at_thm] THEN PROVE_TAC []
683 ]
684QED
685
686Theorem double_neg_lemma[local]:
687 $~ o $~ o P = P
688Proof
689 SRW_TAC [][FUN_EQ_THM, combinTheory.o_THM]
690QED
691
692Theorem exists_induction =
693 (SIMP_RULE (srw_ss()) [double_neg_lemma] o
694 Q.SPECL [`(~) o P`, `(~) o Q`] o
695 CONV_RULE (STRIP_QUANT_CONV
696 (FORK_CONV (EVERY_CONJ_CONV
697 (STRIP_QUANT_CONV CONTRAPOS_CONV),
698 STRIP_QUANT_CONV CONTRAPOS_CONV)) THENC
699 SIMP_CONV (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM]))
700 every_coinduction;
701
702Definition mem_def: mem s p = ?i. i IN PL p /\ (s = el i p)
703End
704
705Theorem mem_thm[simp]:
706 (!x s. mem s (stopped_at x) = (s = x)) /\
707 (!x r p s. mem s (pcons x r p) <=> (s = x) \/ mem s p)
708Proof
709 SRW_TAC [][mem_def, RIGHT_AND_OVER_OR,
710 EXISTS_OR_THM, GSYM LEFT_EXISTS_AND_THM]
711QED
712
713(* ----------------------------------------------------------------------
714 drop n p
715 drops n elements from the front of p and returns what's left
716 ---------------------------------------------------------------------- *)
717
718Definition drop_def[simp]:
719 (drop 0 p = p) /\
720 (drop (SUC n) p = drop n (tail p))
721End
722Theorem numeral_drop[simp] =
723 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV (CONJUNCT2 drop_def);
724
725
726Theorem finite_drop[simp]:
727 !p n. n IN PL p ==> (finite (drop n p) = finite p)
728Proof
729 Induct_on `n` THENL [
730 SRW_TAC [][],
731 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
732 SRW_TAC [][]
733 ]
734QED
735
736Theorem length_drop:
737 !p n. n IN PL p ==>
738 (length (drop n p) = case (length p) of
739 NONE => NONE
740 | SOME m => SOME (m - n))
741Proof
742 Induct_on `n` THENL [
743 REPEAT STRIP_TAC THEN
744 Cases_on `length p` THEN SRW_TAC [][drop_def],
745 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
746 SRW_TAC [][length_thm] THEN
747 Cases_on `length p` THEN SRW_TAC [numSimps.ARITH_ss][] THEN
748 PROVE_TAC [finite_length]
749 ]
750QED
751
752
753Theorem PL_drop:
754 !p i. i IN PL p ==> (PL (drop i p) = IMAGE (\n. n - i) (PL p))
755Proof
756 Induct_on `i` THENL [
757 SRW_TAC [][],
758 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
759 SRW_TAC [][pred_setTheory.EXTENSION, EQ_IMP_THM] THENL [
760 SRW_TAC [][LEFT_AND_OVER_OR, EXISTS_OR_THM,
761 GSYM RIGHT_EXISTS_AND_THM] THEN PROVE_TAC [],
762 SRW_TAC [][] THEN PROVE_TAC [arithmeticTheory.LESS_EQ_REFL],
763 SRW_TAC [][] THEN PROVE_TAC []
764 ]
765 ]
766QED
767
768Theorem IN_PL_drop[simp]:
769 !i j p. i IN PL p ==> (j IN PL (drop i p) <=> i + j IN PL p)
770Proof
771 SRW_TAC [][PL_drop, EQ_IMP_THM] THENL [
772 `(i + (n - i) = n) \/ (i + (n - i) = i)` by DECIDE_TAC THEN
773 SRW_TAC [][],
774 Q.EXISTS_TAC `i + j` THEN SRW_TAC [numSimps.ARITH_ss][]
775 ]
776QED
777
778Theorem first_drop[simp]:
779 !i p. i IN PL p ==> (first (drop i p) = el i p)
780Proof
781 Induct THENL [
782 SRW_TAC [][],
783 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
784 SRW_TAC [][]
785 ]
786QED
787
788Theorem first_label_drop[simp]:
789 !i p. i IN PL p ==> (first_label (drop i p) = nth_label i p)
790Proof
791 Induct THENL [
792 SRW_TAC [][nth_label_def],
793 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
794 SRW_TAC [][nth_label_def]
795 ]
796QED
797
798Theorem tail_drop[simp]:
799 !i p. (i + 1) IN PL p ==> (tail (drop i p) = drop (i + 1) p)
800Proof
801 Induct THEN
802 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
803 SRW_TAC [][CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV drop_def] THEN
804 FULL_SIMP_TAC (srw_ss()) [DECIDE ``SUC x + y = SUC (x + y)``]
805QED
806
807(* from examples/lambda/barengregt/head_reductionScript.sml *)
808Theorem drop_tail_commute :
809 !i p. SUC i IN PL p ==> (drop i (tail p) = tail (drop i p))
810Proof
811 Induct THEN SIMP_TAC (srw_ss()) [Once FORALL_path] THEN
812 SRW_TAC [][]
813QED
814
815(* from examples/lambda/barengregt/head_reductionScript.sml *)
816Theorem drop_not_stopped :
817 !i p. SUC i IN PL p ==> ?v r q. drop i p = pcons v r q
818Proof
819 Induct THEN GEN_TAC THEN
820 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN
821 SRW_TAC [][]
822QED
823
824Theorem el_drop[simp]:
825 !i j p. i + j IN PL p ==> (el i (drop j p) = el (i + j) p)
826Proof
827 Induct_on `j` THENL [
828 SRW_TAC [][],
829 GEN_TAC THEN CONV_TAC (HO_REWR_CONV FORALL_path) THEN
830 SRW_TAC [][arithmeticTheory.ADD_CLAUSES]
831 ]
832QED
833
834Theorem nth_label_drop[simp]:
835 !i j p. SUC(i + j) IN PL p ==>
836 (nth_label i (drop j p) = nth_label (i + j) p)
837Proof
838 Induct_on `j` THENL [
839 SRW_TAC [][],
840 GEN_TAC THEN CONV_TAC (HO_REWR_CONV FORALL_path) THEN
841 SRW_TAC [][arithmeticTheory.ADD_CLAUSES]
842 ]
843QED
844
845(* ----------------------------------------------------------------------
846 ``take n p`` takes n _labels_ from p
847 ---------------------------------------------------------------------- *)
848
849Definition take_def[simp]:
850 (take 0 p = stopped_at (first p)) /\
851 (take (SUC n) p = pcons (first p) (first_label p) (take n (tail p)))
852End
853
854Theorem first_take[simp]:
855 !p i. first (take i p) = first p
856Proof
857 REPEAT GEN_TAC THEN Cases_on `i` THEN SRW_TAC [][]
858QED
859
860Theorem finite_take[simp]:
861 !p i. i IN PL p ==> finite (take i p)
862Proof
863 Induct_on `i` THENL [
864 SRW_TAC [][finite_thm, take_def],
865 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
866 SRW_TAC [][take_def]
867 ]
868QED
869
870Theorem length_take[simp]:
871 !p i. i IN PL p ==> (length (take i p) = SOME (i + 1))
872Proof
873 Induct_on `i` THENL [
874 SRW_TAC [][length_thm, take_def],
875 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
876 SRW_TAC [][length_thm, arithmeticTheory.ADD1]
877 ]
878QED
879
880
881Theorem PL_take[simp]:
882 !p i. i IN PL p ==> (PL (take i p) = { n | n <= i })
883Proof
884 Induct_on `i` THENL [
885 SRW_TAC [][],
886 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
887 SRW_TAC [][pred_setTheory.EXTENSION, EQ_IMP_THM] THEN
888 SRW_TAC [][] THEN POP_ASSUM MP_TAC THEN Cases_on `x'` THEN SRW_TAC [][]
889 ]
890QED
891
892Theorem last_take[simp]:
893 !i p. i IN PL p ==> (last (take i p) = el i p)
894Proof
895 Induct_on `i` THENL [
896 SRW_TAC [][],
897 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
898 SRW_TAC [][]
899 ]
900QED
901
902Theorem nth_label_take:
903 !n p i. i < n /\ n IN PL p ==> (nth_label i (take n p) = nth_label i p)
904Proof
905 Induct THENL [
906 SRW_TAC [][],
907 GEN_TAC THEN
908 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN SRW_TAC [][] THEN
909 Cases_on `i` THEN SRW_TAC [][] THEN
910 FULL_SIMP_TAC (srw_ss()) []
911 ]
912QED
913
914(* ----------------------------------------------------------------------
915 seg i j p
916 is a path consisting of elements i to j from p
917 has no useful meaning if i > j \/ j indexes beyond end of p
918 ---------------------------------------------------------------------- *)
919
920Definition seg_def:
921 seg i j p = take (j - i) (drop i p)
922End
923
924Theorem singleton_seg[simp]:
925 !i p. i IN PL p ==> (seg i i p = stopped_at (el i p))
926Proof
927 SRW_TAC [][seg_def]
928QED
929
930Theorem recursive_seg:
931 !i j p. i < j /\ j IN PL p ==>
932 (seg i j p = pcons (el i p) (nth_label i p) (seg (i + 1) j p))
933Proof
934 SRW_TAC [][seg_def] THEN
935 `~(j - i = 0)` by DECIDE_TAC THEN
936 `?v. j - i = SUC v` by PROVE_TAC [arithmeticTheory.num_CASES] THEN
937 SRW_TAC [][] THENL [
938 PROVE_TAC [PL_downward_closed, first_drop],
939 PROVE_TAC [PL_downward_closed, first_label_drop],
940 `j - (i + 1) = v` by DECIDE_TAC THEN
941 SRW_TAC [][] THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
942 `i + 1 < j \/ (i + 1 = j)` by DECIDE_TAC THEN
943 PROVE_TAC [tail_drop, PL_downward_closed]
944 ]
945QED
946
947
948Theorem PLdc_le[local]:
949 i <= j ==> j IN PL p ==> i IN PL p
950Proof
951 PROVE_TAC [arithmeticTheory.LESS_OR_EQ, PL_downward_closed]
952QED
953
954Theorem PL_seg[simp]:
955 !i j p. i <= j /\ j IN PL p ==> (PL (seg i j p) = {n | n <= j - i})
956Proof
957 SRW_TAC [][seg_def] THEN `i IN PL p` by IMP_RES_TAC PLdc_le THEN
958 SRW_TAC [numSimps.ARITH_ss][]
959QED
960
961
962Theorem finite_seg[simp]:
963 !p i j. i <= j /\ j IN PL p ==> finite (seg i j p)
964Proof
965 REPEAT STRIP_TAC THEN
966 `i IN PL p` by IMP_RES_TAC PLdc_le THEN
967 SRW_TAC [numSimps.ARITH_ss][seg_def]
968QED
969
970Theorem first_seg[simp]:
971 !i j p. i <= j /\ j IN PL p ==> (first (seg i j p) = el i p)
972Proof
973 SRW_TAC [][seg_def] THEN IMP_RES_TAC PLdc_le THEN SRW_TAC [][]
974QED
975
976Theorem last_seg[simp]:
977 !i j p. i <= j /\ j IN PL p ==> (last (seg i j p) = el j p)
978Proof
979 REPEAT STRIP_TAC THEN IMP_RES_TAC PLdc_le THEN
980 SRW_TAC [numSimps.ARITH_ss][seg_def]
981QED
982
983(* ----------------------------------------------------------------------
984 labels p = lazy list of a path's labels
985 ---------------------------------------------------------------------- *)
986
987val labels_def =
988 new_specification
989 ("labels_def", ["labels"],
990 prove(``?f. (!x. f (stopped_at x) = LNIL) /\
991 (!x r p. f (pcons x r p) = LCONS r (f p))``,
992 STRIP_ASSUME_TAC
993 (Q.ISPEC `\p. if ?x. p = stopped_at x then NONE
994 else SOME (tail p, first_label p)`
995 llist_Axiom_1) THEN
996 Q.EXISTS_TAC `g` THEN
997 REPEAT STRIP_TAC THEN
998 POP_ASSUM
999 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN
1000 SRW_TAC [][]));
1001
1002val _ = export_rewrites ["labels_def"]
1003
1004
1005Theorem firstP_at_unique:
1006 !P p n. firstP_at P p n ==> !m. firstP_at P p m = (m = n)
1007Proof
1008 SIMP_TAC (srw_ss()) [EQ_IMP_THM] THEN GEN_TAC THEN
1009 CONV_TAC SWAP_VARS_CONV THEN Induct THENL [
1010 SIMP_TAC (srw_ss()) [firstP_at_zero] THEN
1011 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
1012 SRW_TAC [][firstP_at_thm],
1013 CONV_TAC (HO_REWR_CONV FORALL_path) THEN
1014 SRW_TAC [ARITH_ss][firstP_at_thm] THEN
1015 `m - 1 = n` by PROVE_TAC [] THEN SRW_TAC [ARITH_ss][]
1016 ]
1017QED
1018
1019Definition is_stopped_def: is_stopped p = ?x. p = stopped_at x
1020End
1021
1022Theorem is_stopped_thm[simp]:
1023 (!x. is_stopped (stopped_at x) = T) /\
1024 (!x r p. is_stopped (pcons x r p) = F)
1025Proof
1026 SRW_TAC [][is_stopped_def]
1027QED
1028
1029
1030val filter_def =
1031 new_specification
1032 ("filter_def", ["filter"],
1033 prove(``?f. !P.
1034 (!x. P x ==> (f P (stopped_at x) = stopped_at x)) /\
1035 (!x r p.
1036 f P (pcons x r p) =
1037 if P x then
1038 if exists P p then pcons x r (f P p)
1039 else stopped_at x
1040 else f P p)``,
1041 STRIP_ASSUME_TAC
1042 ((CONV_RULE SKOLEM_CONV o
1043 GEN_ALL o
1044 Q.ISPEC `\p. let n = @n. firstP_at P p n in
1045 let r = drop n p in
1046 (first r,
1047 if is_stopped r \/ ~exists P (tail r) then NONE
1048 else SOME(first_label r, tail r))`)
1049 path_Axiom) THEN
1050 Q.EXISTS_TAC `\P p. if exists P p then g P p else ARB` THEN
1051 SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THENL [
1052 ONCE_ASM_REWRITE_TAC [] THEN
1053 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN
1054 ASM_SIMP_TAC (srw_ss()) [firstP_at_thm, drop_def,
1055 is_stopped_def],
1056 Cases_on `P x` THENL [
1057 FIRST_ASSUM (fn th => REWRITE_TAC [th]) THEN
1058 FIRST_X_ASSUM (CONV_TAC o LAND_CONV o REWR_CONV o
1059 assert (is_forall o concl)) THEN
1060 SRW_TAC [][firstP_at_thm] THEN
1061 FULL_SIMP_TAC bool_ss [every_def, double_neg_lemma],
1062 FIRST_ASSUM (fn th => REWRITE_TAC [th]) THEN
1063 COND_CASES_TAC THEN REWRITE_TAC [] THEN
1064 FIRST_X_ASSUM (fn th =>
1065 ONCE_REWRITE_TAC
1066 [assert (is_forall o concl) th]) THEN
1067 ASM_SIMP_TAC (srw_ss()) [firstP_at_thm] THEN
1068 Q.ABBREV_TAC `n = @n. firstP_at P p n` THEN
1069 `(@n. 0 < n /\ firstP_at P p (n - 1)) = SUC n` by
1070 (FULL_SIMP_TAC (srw_ss()) [exists_def] THEN
1071 `!m. firstP_at P p m = (m = i)`
1072 by PROVE_TAC [firstP_at_unique] THEN
1073 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [
1074 DECIDE ``0 < n /\ (n - 1 = m) <=> (n = m + 1)``]) THEN
1075 ASM_SIMP_TAC (srw_ss())[drop_def]
1076 ]
1077 ]));
1078
1079
1080Theorem filter_eq_stopped[local]:
1081 !P p. exists P p ==> !x. (filter P p = stopped_at x) ==> P x
1082Proof
1083 GEN_TAC THEN HO_MATCH_MP_TAC exists_induction THEN
1084 SRW_TAC [][filter_def]
1085QED
1086
1087Theorem filter_eq_pcons[local]:
1088 !P p. exists P p ==> !x r q. (filter P p = pcons x r q) ==>
1089 P x /\
1090 ?q0. (q = filter P q0) /\ exists P q0
1091Proof
1092 GEN_TAC THEN HO_MATCH_MP_TAC exists_induction THEN
1093 SRW_TAC [][filter_def] THEN PROVE_TAC []
1094QED
1095
1096Theorem filter_every:
1097 !P p. exists P p ==> every P (filter P p)
1098Proof
1099 GEN_TAC THEN
1100 Q_TAC SUFF_TAC `!p. (?q. (p = filter P q) /\ exists P q) ==>
1101 every P p` THEN1 PROVE_TAC [] THEN
1102 HO_MATCH_MP_TAC every_coinduction THEN
1103 PROVE_TAC [filter_eq_stopped, filter_eq_pcons]
1104QED
1105
1106val _ = print "Defining generation of paths from functions\n"
1107
1108val pgenerate_t = ``\f. (FST (f 0), SOME (SND (f 0), f o SUC))``
1109
1110val pgenerate_def = new_specification ("pgenerate_def",
1111 ["pgenerate"],
1112 prove(``?pg. !f g. pg f g = pcons (f 0) (g 0) (pg (f o SUC) (g o SUC))``,
1113 Q.X_CHOOSE_THEN `h` ASSUME_TAC
1114 (CONV_RULE SKOLEM_CONV (ISPEC pgenerate_t path_Axiom)) THEN
1115 Q.EXISTS_TAC `\f g. h (\x. (f x, g x))` THEN
1116 SIMP_TAC (srw_ss()) [] THEN REPEAT GEN_TAC THEN
1117 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN
1118 SIMP_TAC (srw_ss()) [combinTheory.o_DEF]));
1119
1120Theorem pgenerate_infinite:
1121 !f g. ~finite (pgenerate f g)
1122Proof
1123 Q_TAC SUFF_TAC `!p. finite p ==> !f g. ~(p = pgenerate f g)` THEN1
1124 PROVE_TAC [] THEN
1125 HO_MATCH_MP_TAC finite_path_ind THEN CONJ_TAC THENL [
1126 ONCE_REWRITE_TAC [pgenerate_def] THEN SRW_TAC [][],
1127 REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC [pgenerate_def] THEN
1128 SRW_TAC [][]
1129 ]
1130QED
1131
1132Theorem pgenerate_not_stopped[simp]:
1133 !f g x. ~(stopped_at x = pgenerate f g)
1134Proof
1135 PROVE_TAC [pgenerate_infinite, finite_thm]
1136QED
1137
1138
1139Theorem el_pgenerate:
1140 !n f g. el n (pgenerate f g) = f n
1141Proof
1142 Induct THEN ONCE_REWRITE_TAC [pgenerate_def] THEN SRW_TAC [][el_def]
1143QED
1144
1145Theorem nth_label_pgenerate:
1146 !n f g. nth_label n (pgenerate f g) = g n
1147Proof
1148 Induct THEN ONCE_REWRITE_TAC [pgenerate_def] THEN SRW_TAC [][nth_label_def]
1149QED
1150
1151Theorem pgenerate_11:
1152 !f1 g1 f2 g2. (pgenerate f1 g1 = pgenerate f2 g2) <=>
1153 (f1 = f2) /\ (g1 = g2)
1154Proof
1155 SIMP_TAC (srw_ss()) [FORALL_AND_THM, EQ_IMP_THM] THEN
1156 SRW_TAC [][FUN_EQ_THM] THEN PROVE_TAC [el_pgenerate, nth_label_pgenerate]
1157QED
1158
1159
1160Theorem pgenerate_onto:
1161 !p. ~finite p ==> ?f g. p = pgenerate f g
1162Proof
1163 REPEAT STRIP_TAC THEN
1164 MAP_EVERY Q.EXISTS_TAC [`\n. el n p`, `\n. nth_label n p`] THEN
1165 ONCE_REWRITE_TAC [path_bisimulation] THEN
1166 Q.EXISTS_TAC
1167 `\x y. ~finite x /\ (y = pgenerate (\n. el n x) (\n. nth_label n x))` THEN
1168 ASM_SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN
1169 Q.SPEC_THEN `q1` (STRIP_ALL_THEN SUBST_ALL_TAC) path_cases THEN
1170 FULL_SIMP_TAC (srw_ss()) [] THEN
1171 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [pgenerate_def])) THEN
1172 SRW_TAC [][el_def, nth_label_def, combinTheory.o_DEF]
1173QED
1174
1175val _ = print "Defining path OK-ness\n"
1176
1177Definition okpath_f_def:
1178 okpath_f R (X :('a,'b) path set) =
1179 { stopped_at x | x IN UNIV } UNION
1180 { pcons x r p | R x r (first p) /\ p IN X }
1181End
1182
1183Theorem okpath_monotone:
1184 !R. monotone (okpath_f R)
1185Proof
1186 SRW_TAC [][fixedPointTheory.monotone_def, okpath_f_def,
1187 pred_setTheory.SUBSET_DEF] THEN PROVE_TAC []
1188QED
1189
1190Definition okpath_def: okpath R = gfp (okpath_f R)
1191End
1192
1193Theorem okpath_co_ind =
1194 okpath_monotone |> SPEC_ALL
1195 |> MATCH_MP fixedPointTheory.gfp_coinduction
1196 |> SIMP_RULE (srw_ss()) [pred_setTheory.SUBSET_DEF,
1197 GSYM okpath_def,
1198 okpath_f_def]
1199 |> SIMP_RULE bool_ss [IN_DEF]
1200 |> CONV_RULE (RENAME_VARS_CONV ["P"])
1201 |> CONV_RULE
1202 (STRIP_QUANT_CONV
1203 (LAND_CONV (HO_REWR_CONV FORALL_path)))
1204 |> SIMP_RULE (srw_ss()) []
1205 |> CONV_RULE
1206 (STRIP_QUANT_CONV
1207 (LAND_CONV (RENAME_VARS_CONV ["x", "r", "p"]) THENC
1208 RAND_CONV (RENAME_VARS_CONV ["p"])))
1209
1210Theorem okpath_cases =
1211 MATCH_MP fixedPointTheory.gfp_greatest_fixedpoint (SPEC_ALL okpath_monotone)
1212 |> CONJUNCT1 |> SYM
1213 |> SIMP_RULE (srw_ss()) [pred_setTheory.EXTENSION,
1214 okpath_f_def, GSYM okpath_def]
1215 |> SIMP_RULE (srw_ss()) [IN_DEF]
1216 |> GEN_ALL
1217
1218Theorem okpath_thm[simp]:
1219 !R. (!x. okpath R (stopped_at x)) /\
1220 (!x r p. okpath R (pcons x r p) <=> R x r (first p) /\ okpath R p)
1221Proof
1222 REPEAT STRIP_TAC THENL [
1223 ONCE_REWRITE_TAC [okpath_cases] THEN SRW_TAC [][],
1224 CONV_TAC (LAND_CONV (REWR_CONV okpath_cases)) THEN SRW_TAC [][]
1225 ]
1226QED
1227
1228Theorem finite_okpath_ind:
1229 !R.
1230 (!x. P (stopped_at x)) /\
1231 (!x r p. okpath R p /\ finite p /\ R x r (first p) /\ P p ==>
1232 P (pcons x r p)) ==>
1233 !sigma. okpath R sigma /\ finite sigma ==> P sigma
1234Proof
1235 GEN_TAC THEN STRIP_TAC THEN
1236 Q_TAC SUFF_TAC `!sigma. finite sigma ==> okpath R sigma ==> P sigma` THEN1
1237 PROVE_TAC [] THEN
1238 HO_MATCH_MP_TAC finite_path_ind THEN
1239 ASM_SIMP_TAC (srw_ss()) []
1240QED
1241
1242Theorem okpath_pmap:
1243 !R f g p. okpath R p /\ (!x r y. R x r y ==> R (f x) (g r) (f y)) ==>
1244 okpath R (pmap f g p)
1245Proof
1246 REPEAT STRIP_TAC THEN
1247 Q_TAC SUFF_TAC
1248 `!p. (?p0. okpath R p0 /\ (p = pmap f g p0)) ==> okpath R p` THEN1
1249 METIS_TAC[] THEN
1250 HO_MATCH_MP_TAC okpath_co_ind THEN SRW_TAC [][] THEN
1251 Q.SPEC_THEN `p0` (STRIP_ALL_THEN SUBST_ALL_TAC) path_cases THEN
1252 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
1253QED
1254
1255val plink_def = new_specification(
1256 "plink_def",
1257 ["plink"],
1258 prove(``?f. (!x p. f (stopped_at x) p = p) /\
1259 (!x r p1 p2. f (pcons x r p1) p2 = pcons x r (f p1 p2))``,
1260 STRIP_ASSUME_TAC
1261 (Q.ISPEC `\pair. let pullapart g p = (first p,
1262 if is_stopped p then NONE
1263 else SOME (first_label p,
1264 g (tail p)))
1265 in
1266 case pair of
1267 (NONE, p) => pullapart (\t. (NONE, t)) p
1268 | (SOME p1, p2) =>
1269 if is_stopped p1 then
1270 pullapart (\t. (NONE, t)) p2
1271 else
1272 pullapart (\t. (SOME t, p2)) p1`
1273 path_Axiom) THEN
1274 Q.EXISTS_TAC `\p1 p2. g (SOME p1, p2)` THEN
1275 SIMP_TAC (srw_ss()) [] THEN
1276 FIRST_ASSUM (fn th => CONV_TAC
1277 (BINOP_CONV
1278 (STRIP_QUANT_CONV
1279 (LAND_CONV (REWR_CONV th))))) THEN
1280 SIMP_TAC (srw_ss()) [] THEN
1281 Ho_Rewrite.ONCE_REWRITE_TAC [FORALL_path] THEN
1282 SIMP_TAC (srw_ss()) [] THEN
1283 ONCE_REWRITE_TAC [path_bisimulation] THEN GEN_TAC THEN
1284 Q.EXISTS_TAC `\p1 p2. (p1 = g (NONE, p2))` THEN
1285 SIMP_TAC (srw_ss()) [] THEN
1286 Ho_Rewrite.ONCE_REWRITE_TAC [FORALL_path] THEN
1287 SIMP_TAC (srw_ss()) [] THEN
1288 POP_ASSUM (fn th => CONV_TAC
1289 (BINOP_CONV
1290 (STRIP_QUANT_CONV
1291 (LAND_CONV (REWR_CONV th))))) THEN
1292 SRW_TAC [][]));
1293
1294val _ = export_rewrites ["plink_def"]
1295
1296
1297Theorem finite_plink[simp]:
1298 !p1 p2. finite (plink p1 p2) <=> finite p1 /\ finite p2
1299Proof
1300 Q_TAC SUFF_TAC
1301 `(!p1:('a,'b)path. finite p1 ==>
1302 !p2. finite p2 ==> finite (plink p1 p2)) /\
1303 !p:('a,'b)path. finite p ==>
1304 !p1 p2. (p = plink p1 p2) ==> finite p1 /\ finite p2`
1305 THEN1 PROVE_TAC [] THEN CONJ_TAC THEN
1306 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THEN
1307 Q.SPEC_THEN `p1` (STRIP_ALL_THEN SUBST_ALL_TAC) path_cases THEN
1308 FULL_SIMP_TAC (srw_ss()) [] THEN
1309 SRW_TAC [][] THEN PROVE_TAC []
1310QED
1311
1312Theorem first_plink[simp]:
1313 !p1 p2. (last p1 = first p2) ==> (first (plink p1 p2) = first p1)
1314Proof
1315 CONV_TAC (HO_REWR_CONV FORALL_path) THEN SRW_TAC [][]
1316QED
1317
1318
1319Theorem last_plink[simp]:
1320 !p1 p2. finite p1 /\ finite p2 /\ (last p1 = first p2) ==>
1321 (last (plink p1 p2) = last p2)
1322Proof
1323 Q_TAC SUFF_TAC `!p1. finite p1 ==>
1324 !p2. finite p2 /\ (last p1 = first p2) ==>
1325 (last (plink p1 p2) = last p2)`
1326 THEN1 PROVE_TAC [] THEN
1327 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][]
1328QED
1329
1330
1331Theorem okpath_plink[simp]:
1332 !R p1 p2. finite p1 /\ (last p1 = first p2) ==>
1333 (okpath R (plink p1 p2) <=> okpath R p1 /\ okpath R p2)
1334Proof
1335 GEN_TAC THEN
1336 Q_TAC SUFF_TAC
1337 `!p1. finite p1 ==>
1338 !p2. (last p1 = first p2) ==>
1339 (okpath R (plink p1 p2) <=> okpath R p1 /\ okpath R p2)`
1340 THEN1 PROVE_TAC [] THEN
1341 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THEN PROVE_TAC []
1342QED
1343
1344Theorem okpath_take[simp]:
1345 !R p i. i IN PL p /\ okpath R p ==> okpath R (take i p)
1346Proof
1347 Induct_on `i` THEN1 SRW_TAC [][] THEN
1348 GEN_TAC THEN CONV_TAC (HO_REWR_CONV FORALL_path) THEN SRW_TAC [][]
1349QED
1350
1351Theorem okpath_drop[simp]:
1352 !R p i. i IN PL p /\ okpath R p ==> okpath R (drop i p)
1353Proof
1354 Induct_on `i` THEN1 SRW_TAC [][] THEN
1355 GEN_TAC THEN CONV_TAC (HO_REWR_CONV FORALL_path) THEN SRW_TAC [][]
1356QED
1357
1358Theorem okpath_seg[simp]:
1359 !R p i j. i <= j /\ j IN PL p /\ okpath R p ==> okpath R (seg i j p)
1360Proof
1361 SRW_TAC [][seg_def] THEN IMP_RES_TAC PLdc_le THEN
1362 SRW_TAC [numSimps.ARITH_ss][]
1363QED
1364
1365(* "strongly normalising" for labelled transition relations *)
1366Definition SN_def:
1367 SN R = WF (\x y. ?l. R y l x)
1368End
1369
1370Theorem SN_finite_paths:
1371 !R p. SN R /\ okpath R p ==> finite p
1372Proof
1373 SIMP_TAC (srw_ss()) [SN_def, GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN
1374 GEN_TAC THEN
1375 DISCH_THEN (MP_TAC o MATCH_MP relationTheory.WF_INDUCTION_THM) THEN
1376 SIMP_TAC (srw_ss()) [GSYM LEFT_FORALL_IMP_THM] THEN STRIP_TAC THEN
1377 Q_TAC SUFF_TAC `!x p. (x = first p) /\ okpath R p ==> finite p`
1378 THEN1 SRW_TAC [][] THEN
1379 POP_ASSUM HO_MATCH_MP_TAC THEN SIMP_TAC (srw_ss()) [] THEN GEN_TAC THEN
1380 STRIP_TAC THEN GEN_TAC THEN
1381 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN
1382 SRW_TAC [][] THEN PROVE_TAC []
1383QED
1384
1385Theorem finite_paths_SN:
1386 !R. (!p. okpath R p ==> finite p) ==> SN R
1387Proof
1388 SRW_TAC [][SN_def, prim_recTheory.WF_IFF_WELLFOUNDED,
1389 prim_recTheory.wellfounded_def] THEN
1390 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
1391 POP_ASSUM (Q.X_CHOOSE_THEN `g` ASSUME_TAC o CONV_RULE SKOLEM_CONV) THEN
1392 Q_TAC SUFF_TAC `okpath R (pgenerate f g)` THEN1
1393 PROVE_TAC [pgenerate_infinite] THEN
1394 Q_TAC SUFF_TAC `!p. (?n. p = pgenerate (f o (+) n) (g o (+) n)) ==>
1395 okpath R p` THEN1
1396 (SIMP_TAC (srw_ss()) [GSYM LEFT_FORALL_IMP_THM] THEN
1397 DISCH_THEN (Q.SPEC_THEN `0` MP_TAC) THEN
1398 SIMP_TAC (srw_ss() ++ boolSimps.ETA_ss)
1399 [combinTheory.o_DEF]) THEN
1400 HO_MATCH_MP_TAC okpath_co_ind THEN REPEAT GEN_TAC THEN
1401 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [pgenerate_def])) THEN
1402 SRW_TAC [][] THENL [
1403 ONCE_REWRITE_TAC [pgenerate_def] THEN
1404 ASM_SIMP_TAC (srw_ss()) [GSYM arithmeticTheory.ADD1],
1405 Q.EXISTS_TAC `SUC n` THEN
1406 SIMP_TAC (srw_ss()) [combinTheory.o_DEF, arithmeticTheory.ADD_CLAUSES]
1407 ]
1408QED
1409
1410Theorem SN_finite_paths_EQ:
1411 !R. SN R = !p. okpath R p ==> finite p
1412Proof
1413 PROVE_TAC [finite_paths_SN, SN_finite_paths]
1414QED
1415
1416Theorem labels_LMAP:
1417 !p. labels p = LMAP FST (SND (fromPath p))
1418Proof
1419 HO_MATCH_MP_TAC LLIST_EQ THEN
1420 SRW_TAC [] [] THEN
1421 ASSUME_TAC (Q.SPEC `p` path_cases) THEN
1422 SRW_TAC [] [] THEN
1423 FULL_SIMP_TAC (srw_ss()) [] THEN
1424 FULL_SIMP_TAC (srw_ss()) [stopped_at_def, pcons_def,
1425 path_rep_bijections_thm] THEN
1426 METIS_TAC []
1427QED
1428
1429local
1430
1431val lemma = Q.prove (
1432 `!x.
1433 labels (plink (FST x) (SND x)) = LAPPEND (labels (FST x)) (labels (SND x))`,
1434 HO_MATCH_MP_TAC LLIST_EQ THEN
1435 SRW_TAC [] [] THEN
1436 Cases_on `x` THEN
1437 SRW_TAC [] [] THEN
1438 ASSUME_TAC (Q.SPEC `q` path_cases) THEN
1439 ASSUME_TAC (Q.SPEC `r` path_cases) THEN
1440 SRW_TAC [] [] THEN
1441 SRW_TAC [] [] THEN
1442 METIS_TAC [pairTheory.FST, pairTheory.SND, labels_def, plink_def, LAPPEND]);
1443
1444in
1445
1446Theorem labels_plink:
1447 !p1 p2. labels (plink p1 p2) = LAPPEND (labels p1) (labels p2)
1448Proof
1449 METIS_TAC [pairTheory.FST, pairTheory.SND, lemma]
1450QED
1451
1452end;
1453
1454Theorem finite_labels:
1455 !p. LFINITE (labels p) = finite p
1456Proof
1457 SRW_TAC [] [labels_LMAP, LFINITE_MAP, finite_def]
1458QED
1459
1460Definition unfold_def:
1461 unfold proj f s =
1462 toPath
1463 (proj s,
1464 LUNFOLD (\s. OPTION_MAP (λ(next_s,lbl).
1465 (next_s,(lbl,proj next_s)))
1466 (f s))
1467 s)
1468End
1469
1470Theorem unfold_thm:
1471 !proj f s.
1472 unfold proj f s =
1473 case f s of
1474 NONE => stopped_at (proj s)
1475 | SOME (s',l) => pcons (proj s) l (unfold proj f s')
1476Proof
1477 SRW_TAC [] [unfold_def] THEN
1478 Cases_on `f s` THEN
1479 SRW_TAC [] [stopped_at_def, pcons_def, toPath_11, Once LUNFOLD] THEN
1480 Cases_on `x` THEN
1481 SRW_TAC [] [toPath_11, path_rep_bijections_thm, first_def]
1482QED
1483
1484Theorem unfold_thm2:
1485 !proj f x v1 v2.
1486 ((f x = NONE) ==> (unfold proj f x = stopped_at (proj x))) /\
1487 ((f x = SOME (v1,v2)) ==>
1488 (unfold proj f x = pcons (proj x) v2 (unfold proj f v1)))
1489Proof
1490 SRW_TAC [] [] THEN1
1491 SRW_TAC [] [Once unfold_thm] THEN
1492 SRW_TAC [] [Once unfold_thm]
1493QED
1494
1495Theorem labels_unfold:
1496 !proj f s. labels (unfold proj f s) = LUNFOLD f s
1497Proof
1498 SRW_TAC [] [labels_LMAP, unfold_def, path_rep_bijections_thm, LMAP_LUNFOLD,
1499 optionTheory.OPTION_MAP_COMPOSE, combinTheory.o_DEF] THEN
1500 `!s. (OPTION_MAP (\x. (λ(x,y). (x,FST y))
1501 ((λ(next_s,lbl). (next_s,lbl,proj next_s)) x))
1502 (f s) =
1503 f s)`
1504 by (Cases_on `f s` THEN
1505 SRW_TAC [] [] THEN
1506 Cases_on `x` THEN
1507 SRW_TAC [] []) THEN
1508SRW_TAC [] [] THEN
1509METIS_TAC []
1510QED
1511
1512Theorem okpath_co_ind2[local]:
1513 !P R p.
1514 (!x r p. P (pcons x r p) ==> R x r (first p) /\ P p) /\ P p ==> okpath R p
1515Proof
1516METIS_TAC [okpath_co_ind]
1517QED
1518
1519Theorem okpath_unfold:
1520 !P m proj f s.
1521 P s /\
1522 (!s s' l. P s /\ (f s = SOME (s', l)) ==> P s') /\
1523 (!s s' l. P s /\ (f s = SOME (s',l)) ==> m (proj s) l (proj s'))
1524 ==>
1525 okpath m (unfold proj f s)
1526Proof
1527 SRW_TAC [] [] THEN
1528 HO_MATCH_MP_TAC okpath_co_ind2 THEN
1529 SRW_TAC [] [] THEN
1530 Q.EXISTS_TAC `\p. ?s. P s /\ (p = unfold proj f s)` THEN
1531 SRW_TAC [] [] THENL
1532 [FULL_SIMP_TAC (srw_ss()) [Once unfold_thm] THEN
1533 Cases_on `f s'` THEN
1534 FULL_SIMP_TAC (srw_ss()) [] THEN
1535 Cases_on `x'` THEN
1536 FULL_SIMP_TAC (srw_ss()) [] THEN
1537 SRW_TAC [] [Once unfold_thm] THEN
1538 Cases_on `f q` THEN
1539 SRW_TAC [] [] THEN
1540 Cases_on `x` THEN
1541 SRW_TAC [] [],
1542 POP_ASSUM (MP_TAC o SIMP_RULE (srw_ss()) [Once unfold_thm]) THEN
1543 SRW_TAC [] [] THEN
1544 Cases_on `f s'` THEN
1545 FULL_SIMP_TAC (srw_ss()) [] THEN
1546 Cases_on `x'` THEN
1547 FULL_SIMP_TAC (srw_ss()) [] THEN
1548 SRW_TAC [] [] THEN
1549 METIS_TAC [],
1550 METIS_TAC []]
1551QED
1552
1553Definition trace_machine_def:
1554 trace_machine P s l s' <=> (P (s++[l])) /\ (s' = s++[l])
1555End
1556
1557local
1558
1559val lemma1 = Q.prove (
1560`!l h t. LTAKE (SUC (LENGTH l)) (LAPPEND (fromList l) (h:::t)) = SOME (l++[h])`,
1561Induct THEN
1562SRW_TAC [] [LTAKE_CONS_EQ_SOME]);
1563
1564val lemma2 = Q.prove (
1565`!l h t. LAPPEND (fromList l) (h:::t) = LAPPEND (fromList (l++[h])) t`,
1566Induct THEN
1567SRW_TAC [] []);
1568
1569in
1570
1571Theorem trace_machine_thm:
1572 !P tr.
1573 (!n l. (LTAKE n tr = SOME l) ==> P l)
1574 ==>
1575 ?p. (tr = labels p) /\ okpath (trace_machine P) p /\ (first p = [])
1576Proof
1577 SRW_TAC [] [] THEN
1578 Q.EXISTS_TAC `unfold (λ(s,tr). s)
1579 (λ(s,tr).
1580 (if tr = [||] then
1581 NONE
1582 else
1583 SOME ((s++[(THE (LHD tr))],(THE (LTL tr))),
1584 THE (LHD tr))))
1585 ([],tr)` THEN
1586 SRW_TAC [] [labels_unfold] THENL
1587 [MATCH_MP_TAC (GSYM LUNFOLD_EQ) THEN
1588 Q.EXISTS_TAC `λ(s,tr) tr'. (tr = tr')` THEN
1589 SRW_TAC [] [] THEN
1590 Cases_on `s` THEN
1591 FULL_SIMP_TAC (srw_ss()) [] THEN
1592 SRW_TAC [] [] THEN
1593 `(ll = [||]) \/ ?h t. ll = h:::t` by METIS_TAC [llist_CASES] THEN
1594 SRW_TAC [] [],
1595 MATCH_MP_TAC okpath_unfold THEN
1596 Q.EXISTS_TAC `λ(s,tr). (!n l. (LTAKE n (LAPPEND (fromList s) tr) = SOME l)
1597 ==>
1598 P l)` THEN
1599 SRW_TAC [] [] THEN1
1600 METIS_TAC [] THENL
1601 [Cases_on `s'` THEN
1602 SRW_TAC [] [] THEN
1603 Cases_on `s` THEN
1604 FULL_SIMP_TAC (srw_ss()) [] THEN
1605 `?h t. r' = h:::t` by METIS_TAC [llist_CASES] THEN
1606 FULL_SIMP_TAC (srw_ss()) [] THEN
1607 METIS_TAC [lemma2],
1608 SRW_TAC [] [trace_machine_def] THEN
1609 Cases_on `s` THEN
1610 Cases_on `s'` THEN
1611 FULL_SIMP_TAC (srw_ss()) [] THEN
1612 `?h t. r = h:::t` by METIS_TAC [llist_CASES] THEN
1613 SRW_TAC [] [] THEN
1614 FULL_SIMP_TAC (srw_ss()) [] THEN
1615 METIS_TAC [lemma1]],
1616 SRW_TAC [] [Once unfold_thm]]
1617QED
1618
1619end;
1620
1621Theorem trace_machine_thm2:
1622 !n l P p init.
1623 okpath (trace_machine P) p /\
1624 P (first p)
1625 ==>
1626 ((LTAKE n (labels p) = SOME l) ==> P (first p ++ l))
1627Proof
1628 Induct_on `n` THEN
1629 SRW_TAC [] [] THEN
1630 SRW_TAC [] [] THEN
1631 FULL_SIMP_TAC (srw_ss()) [LTAKE] THEN
1632 Cases_on `LHD (labels p)` THEN
1633 FULL_SIMP_TAC (srw_ss()) [] THEN
1634 Cases_on `LTAKE n (THE (LTL (labels p)))` THEN
1635 FULL_SIMP_TAC (srw_ss()) [] THEN
1636 SRW_TAC [] [] THEN
1637 `(?x. p = stopped_at x) \/ (?h l p'. p = pcons h l p')`
1638 by METIS_TAC [path_cases] THEN
1639 FULL_SIMP_TAC (srw_ss()) [trace_machine_def] THEN
1640 SRW_TAC [] [] THEN
1641 METIS_TAC [listTheory.APPEND, listTheory.APPEND_ASSOC]
1642QED
1643
1644local
1645
1646val lemma = Q.prove (
1647`!n p. (LTAKE n (labels p) = NONE) <=> n NOTIN PL p`,
1648 Induct THEN
1649 SRW_TAC [] [] THEN
1650 `(?x. p = stopped_at x) \/ (?h l t. p = pcons h l t)`
1651 by METIS_TAC [path_cases] THEN
1652 SRW_TAC [] []);
1653
1654in
1655
1656Theorem LTAKE_labels:
1657 !n p l.
1658 (LTAKE n (labels p) = SOME l)
1659 <=>
1660 n IN PL p /\ (toList (labels (take n p)) = SOME l)
1661Proof
1662 Induct THEN
1663 SRW_TAC [] [toList_THM, LTAKE] THEN
1664 `(?x. p = stopped_at x) \/ (?h l t. p = pcons h l t)`
1665 by METIS_TAC [path_cases] THEN
1666 FULL_SIMP_TAC (srw_ss()) [] THEN
1667 SRW_TAC [] [] THEN
1668 Cases_on `LTAKE n (labels t)` THEN
1669 FULL_SIMP_TAC (srw_ss()) [] THENL
1670 [METIS_TAC [lemma],
1671 METIS_TAC [optionTheory.SOME_11]]
1672QED
1673
1674end;
1675
1676Theorem drop_eq_pcons:
1677 !n p h l t. n IN PL p /\ (drop n p = pcons h l t) ==> n + 1 IN PL p
1678Proof
1679 Induct THEN
1680 SRW_TAC [] [] THEN
1681 `(?x. p = stopped_at x) \/ (?h l t. p = pcons h l t)`
1682 by METIS_TAC [path_cases] THEN
1683 SRW_TAC [] [] THEN
1684 FULL_SIMP_TAC (srw_ss()) [] THEN
1685 RES_TAC THEN
1686 Q.EXISTS_TAC `n+1` THEN
1687 SRW_TAC [] [] THEN
1688 DECIDE_TAC
1689QED
1690
1691Definition parallel_comp_def:
1692 parallel_comp m1 m2 (s1,s2) l (s1',s2') <=>
1693 m1 s1 l s1' /\ m2 s2 l s2'
1694End
1695
1696Theorem okpath_parallel_comp:
1697 !p m1 m2.
1698 okpath (parallel_comp m1 m2) p
1699 <=>
1700 okpath m1 (pmap FST (\x.x) p) /\ okpath m2 (pmap SND (\x.x) p)
1701Proof
1702 SRW_TAC [] [] THEN
1703 EQ_TAC THEN
1704 SRW_TAC [] [] THEN
1705 MATCH_MP_TAC okpath_co_ind2 THENL
1706 [Q.EXISTS_TAC `\p'. ?n. n IN PL p /\ okpath (parallel_comp m1 m2) (drop n p) /\
1707 (p' = pmap FST (\x.x) (drop n p))` THEN
1708 SRW_TAC [] [] THENL
1709 [`(?x. (drop n p) = stopped_at x) \/ (?h l t. (drop n p) = pcons h l t)`
1710 by METIS_TAC [path_cases] THEN
1711 SRW_TAC [] [] THEN
1712 FULL_SIMP_TAC (srw_ss()) [okpath_thm] THEN
1713 SRW_TAC [] [] THEN
1714 Cases_on `h` THEN
1715 Cases_on `first t` THEN
1716 FULL_SIMP_TAC (srw_ss()) [parallel_comp_def],
1717 `(?x. (drop n p) = stopped_at x) \/ (?h l t. (drop n p) = pcons h l t)`
1718 by METIS_TAC [path_cases] THEN
1719 SRW_TAC [] [] THEN
1720 FULL_SIMP_TAC (srw_ss()) [] THEN
1721 SRW_TAC [] [] THEN
1722 IMP_RES_TAC drop_eq_pcons THEN
1723 Q.EXISTS_TAC `n+1` THEN
1724 SRW_TAC [] [] THEN
1725 METIS_TAC [tail_drop, tail_def],
1726 Q.EXISTS_TAC `0` THEN
1727 SRW_TAC [] []],
1728 Q.EXISTS_TAC `\p'. ?n. n IN PL p /\ okpath (parallel_comp m1 m2) (drop n p) /\
1729 (p' = pmap SND (\x.x) (drop n p))` THEN
1730 SRW_TAC [] [] THENL
1731 [`(?x. (drop n p) = stopped_at x) \/ (?h l t. (drop n p) = pcons h l t)`
1732 by METIS_TAC [path_cases] THEN
1733 SRW_TAC [] [] THEN
1734 FULL_SIMP_TAC (srw_ss()) [okpath_thm] THEN
1735 SRW_TAC [] [] THEN
1736 Cases_on `h` THEN
1737 Cases_on `first t` THEN
1738 FULL_SIMP_TAC (srw_ss()) [parallel_comp_def],
1739 `(?x. (drop n p) = stopped_at x) \/ (?h l t. (drop n p) = pcons h l t)`
1740 by METIS_TAC [path_cases] THEN
1741 SRW_TAC [] [] THEN
1742 FULL_SIMP_TAC (srw_ss()) [] THEN
1743 SRW_TAC [] [] THEN
1744 IMP_RES_TAC drop_eq_pcons THEN
1745 Q.EXISTS_TAC `n+1` THEN
1746 SRW_TAC [] [] THEN
1747 METIS_TAC [tail_drop, tail_def],
1748 Q.EXISTS_TAC `0` THEN
1749 SRW_TAC [] []],
1750 Q.EXISTS_TAC `\p'. ?n. n IN PL p /\ okpath m1 (pmap FST (\x.x) p') /\
1751 okpath m2 (pmap SND (\x.x) p') /\ (p' = drop n p)` THEN
1752 SRW_TAC [] [] THENL
1753 [Cases_on `x` THEN
1754 Cases_on `first p'` THEN
1755 FULL_SIMP_TAC (srw_ss()) [parallel_comp_def],
1756 `(?x. (drop n p) = stopped_at x) \/ (?h l t. (drop n p) = pcons h l t)`
1757 by METIS_TAC [path_cases] THEN
1758 SRW_TAC [] [] THEN
1759 FULL_SIMP_TAC (srw_ss()) [] THEN
1760 SRW_TAC [] [] THEN
1761 IMP_RES_TAC drop_eq_pcons THEN
1762 Q.EXISTS_TAC `n+1` THEN
1763 SRW_TAC [] [] THEN
1764 METIS_TAC [tail_drop, tail_def],
1765 Q.EXISTS_TAC `0` THEN
1766 SRW_TAC [] []]]
1767QED
1768
1769Theorem build_pcomp_trace:
1770 !m1 p1 m2 p2.
1771 okpath m1 p1 /\ okpath m2 p2 /\ (labels p1 = labels p2)
1772 ==>
1773 ?p. okpath (parallel_comp m1 m2) p /\ (labels p = labels p1) /\
1774 (first p = (first p1, first p2))
1775Proof
1776 SRW_TAC [] [] THEN
1777 Q.EXISTS_TAC `unfold (λ(p1,p2). (first p1, first p2))
1778 (λ(p1,p2).
1779 if is_stopped p1 \/ is_stopped p2 then
1780 NONE
1781 else
1782 SOME ((tail p1, tail p2), first_label p1))
1783 (p1,p2)` THEN
1784 SRW_TAC [] [labels_unfold] THENL
1785 [HO_MATCH_MP_TAC okpath_unfold THEN
1786 Q.EXISTS_TAC `λ(p1,p2). okpath m1 p1 /\ okpath m2 p2 /\
1787 (labels p1 = labels p2)` THEN
1788 SRW_TAC [] [] THEN
1789 Cases_on `s` THEN
1790 Cases_on `s'` THEN
1791 FULL_SIMP_TAC (srw_ss()) [] THEN
1792 `?s l p s' l' p'. (r = pcons s l p) /\ (q = pcons s' l' p')`
1793 by METIS_TAC [path_cases, is_stopped_def] THEN
1794 FULL_SIMP_TAC (srw_ss()) [] THEN
1795 SRW_TAC [] [parallel_comp_def],
1796 MATCH_MP_TAC LUNFOLD_EQ THEN
1797 Q.EXISTS_TAC `λ(p1,p2) tr. (labels p1 = tr) /\
1798 (labels p1 = labels p2)` THEN
1799 SRW_TAC [] [] THEN
1800 Cases_on `s` THEN
1801 SRW_TAC [] [] THEN
1802 FULL_SIMP_TAC (srw_ss()) [] THEN
1803 SRW_TAC [] [] THEN
1804 `(?x. q = stopped_at x) \/ ?h t p. q = pcons h t p`
1805 by METIS_TAC [path_cases] THEN
1806 `(?x. r = stopped_at x) \/ ?h t p. r = pcons h t p`
1807 by METIS_TAC [path_cases] THEN
1808 FULL_SIMP_TAC (srw_ss()) [],
1809 SRW_TAC [] [Once unfold_thm]]
1810QED
1811
1812Theorem nth_label_LNTH:
1813 !n p x.
1814 (LNTH n (labels p) = SOME x) = (n + 1 IN PL p /\ (nth_label n p = x))
1815Proof
1816 Induct THEN
1817 SRW_TAC [] [] THEN
1818 `(labels p = [||]) \/ ?h t. labels p = h:::t` by METIS_TAC [llist_CASES] THEN
1819 FULL_SIMP_TAC (srw_ss()) [] THEN
1820 SRW_TAC [] [] THEN
1821 `(?x. p = stopped_at x) \/ ?h l p'. p = pcons h l p'`
1822 by METIS_TAC [path_cases] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1823 SRW_TAC [] [] THEN
1824 EQ_TAC THEN
1825 SRW_TAC [] [] THENL
1826 [Q.EXISTS_TAC `n + 1` THEN
1827 SRW_TAC [] [] THEN
1828 DECIDE_TAC,
1829 `n + 1 = x'` by DECIDE_TAC THEN
1830 SRW_TAC [] []]
1831QED
1832
1833Theorem nth_label_LTAKE:
1834 !n p l i v.
1835 (LTAKE n (labels p) = SOME l) /\
1836 i < LENGTH l
1837 ==>
1838 (nth_label i p = EL i l)
1839Proof
1840 Induct THEN
1841 SRW_TAC [] [] THEN
1842 FULL_SIMP_TAC (srw_ss()) [LTAKE_SNOC_LNTH] THEN
1843 Cases_on `LTAKE n (labels p)` THEN
1844 FULL_SIMP_TAC (srw_ss()) [] THEN
1845 Cases_on `LNTH n (labels p)` THEN
1846 FULL_SIMP_TAC (srw_ss()) [] THEN
1847 SRW_TAC [] [] THEN
1848 FULL_SIMP_TAC (srw_ss()) [] THEN
1849 `i < LENGTH x \/ (i = LENGTH x)` by DECIDE_TAC THEN
1850 FULL_SIMP_TAC (srw_ss()) [] THEN1
1851 METIS_TAC [rich_listTheory.EL_APPEND1] THEN
1852 SRW_TAC [] [] THEN
1853 FULL_SIMP_TAC (srw_ss()) [nth_label_LNTH] THEN
1854 METIS_TAC [LTAKE_LENGTH, listTheory.SNOC_APPEND, listTheory.EL_LENGTH_SNOC]
1855QED
1856
1857Theorem finite_path_end_cases:
1858 !p.
1859 finite p ==>
1860 (?x. p = stopped_at x) \/
1861 (?p' l s. p = plink p' (pcons (last p') l (stopped_at s)))
1862Proof
1863 HO_MATCH_MP_TAC finite_path_ind THEN
1864 SRW_TAC [] [] THENL
1865 [Q.EXISTS_TAC `stopped_at x` THEN
1866 SRW_TAC [] [],
1867 Q.EXISTS_TAC `pcons x r p'` THEN
1868 SRW_TAC [] [] THEN
1869 METIS_TAC []]
1870QED
1871
1872Theorem simulation_trace_inclusion:
1873 !R M1 M2 p t_init.
1874 (!s1 l s2 t1. R s1 t1 /\ M1 s1 l s2 ==> ?t2. R s2 t2 /\ M2 t1 l t2) /\
1875 okpath M1 p /\
1876 R (first p) t_init
1877 ==>
1878 ?q. okpath M2 q /\ (labels p = labels q) /\ (first q = t_init)
1879Proof
1880SRW_TAC [] [] THEN
1881`?next_t. !s1 l s2 t1. R s1 t1 /\ M1 s1 l s2 ==>
1882 R s2 (next_t s1 l s2 t1) /\ M2 t1 l (next_t s1 l s2 t1)` by
1883 METIS_TAC [SKOLEM_THM] THEN
1884Q.EXISTS_TAC `unfold (λ(p,t). t)
1885 (λ(p,t). if is_stopped p then
1886 NONE
1887 else
1888 SOME ((tail p,
1889 next_t (first p)
1890 (first_label p)
1891 (first (tail p)) t),
1892 first_label p))
1893 (p,t_init)` THEN
1894SRW_TAC [] [] THENL
1895[HO_MATCH_MP_TAC okpath_unfold THEN
1896 Q.EXISTS_TAC `λ(p',t_init'). okpath M1 p' /\ R (first p') t_init'` THEN
1897 SRW_TAC [] [] THEN
1898 FULL_SIMP_TAC (srw_ss()) [] THEN
1899 Cases_on `s` THEN
1900 Cases_on `s'` THEN
1901 FULL_SIMP_TAC (srw_ss()) [] THEN
1902 `?s l p. q = pcons s l p` by METIS_TAC [path_cases, is_stopped_def] THEN
1903 FULL_SIMP_TAC (srw_ss()) [] THEN
1904 SRW_TAC [] [],
1905 SRW_TAC [] [labels_unfold] THEN
1906 MATCH_MP_TAC (GSYM LUNFOLD_EQ) THEN
1907 Q.EXISTS_TAC `λ(p,i) tr'. (labels p = tr')` THEN
1908 SRW_TAC [] [] THEN
1909 Cases_on `s` THEN
1910 FULL_SIMP_TAC (srw_ss()) [] THEN
1911 SRW_TAC [] [] THEN
1912 `(?x. q = stopped_at x) \/ ?h l p. q = pcons h l p`
1913 by METIS_TAC [path_cases] THEN
1914 SRW_TAC [] [],
1915 SRW_TAC [] [Once unfold_def, first_def, path_rep_bijections_thm]]
1916QED
1917
1918Theorem infinite_path_cases :
1919 !p. infinite p ==> ?x r q. (p = pcons x r q) /\ infinite q
1920Proof
1921 rpt STRIP_TAC
1922 >> STRIP_ASSUME_TAC (Q.SPEC ‘p’ path_cases)
1923 >- (‘length p = NONE’ by PROVE_TAC [length_def] \\
1924 ‘length p = SOME 1’ by PROVE_TAC [alt_length_thm] \\
1925 fs [])
1926 >> qexistsl_tac [‘x’, ‘r’, ‘q’]
1927 >> ASM_REWRITE_TAC []
1928 >> CCONTR_TAC >> fs []
1929QED
1930
1931Theorem finite_take_all :
1932 !p. finite p ==> (take (PRE (THE (length p))) p = p)
1933Proof
1934 HO_MATCH_MP_TAC finite_path_ind
1935 >> rw [length_thm]
1936 >> POP_ASSUM MP_TAC
1937 >> ‘?n. length p = SOME (SUC n)’ by METIS_TAC [length_cases]
1938 >> rw [arithmeticTheory.PRE_SUB1, take_def]
1939QED
1940
1941Theorem finite_last_el :
1942 !p. finite p ==> (last p = el (PRE (THE (length p))) p)
1943Proof
1944 rpt STRIP_TAC
1945 >> ‘last p = last (take (PRE (THE (length p))) p)’
1946 by PROVE_TAC [finite_take_all]
1947 >> POP_ASSUM (fn th => ONCE_REWRITE_TAC [th])
1948 >> MATCH_MP_TAC last_take
1949 >> rw [PL_def]
1950 >> ‘?n. length p = SOME (SUC n)’ by METIS_TAC [length_cases]
1951 >> rw []
1952QED