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