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