1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath; 9 10map load 11 ["pred_setTheory", "pairTheory", "arithmeticTheory", "tuerk_tacticsLib", 12 "containerTheory", "listTheory", "prop_logicTheory"]; 13*) 14 15 16open pred_setTheory pairTheory arithmeticTheory tuerk_tacticsLib 17 containerTheory listTheory prop_logicTheory; 18open Sanity; 19 20val _ = hide "S"; 21val _ = hide "I"; 22 23(* 24show_assums := false; 25show_assums := true; 26show_types := true; 27show_types := false; 28quietdec := false; 29*) 30 31 32 33val _ = new_theory "infinite_path"; 34 35 36(****************************************************************************** 37* Elementary functions and predicates on temporal_paths 38******************************************************************************) 39val EMPTY_PATH_def = 40 Define 41 `EMPTY_PATH = (\n:num. EMPTY)`; 42 43 44val PATH_TAIL_def = 45 Define 46 `PATH_TAIL t v = (\n:num. v (n+t))`; 47 48 49val PATH_MAP_def = 50 Define 51 `(PATH_MAP (f: num -> 'a -> 'b) v) = (\n:num. (f n (v n)))`; 52 53 54val PATH_RESTRICT_def = 55 Define 56 `PATH_RESTRICT v r = PATH_MAP (\n s. (s INTER r)) v`; 57 58 59val PATH_RESTN_def = 60 Define 61 `(PATH_RESTN v (n:num)) = (\t:num. v (t+n))`; 62 63 64val PATH_REST_def = 65 Define 66 `(PATH_REST v) = (PATH_RESTN v 1)`; 67 68 69val PATH_UNION_def = 70 Define 71 `PATH_UNION v w = (\n:num. ((v n) UNION (w n)))`; 72 73 74val PATH_DIFF_def = 75 Define 76 `PATH_DIFF v w = (\n:num. ((v n) DIFF w))`; 77 78 79val PATH_SUBSET_def = 80 Define 81 `(PATH_SUBSET v (w:'a set)) = (!n:num. ((v n) SUBSET w))`; 82 83 84val PATH_VAR_RENAMING_def = 85 Define 86 `(PATH_VAR_RENAMING (f:'a->'b) v) = 87 (PATH_MAP (\n:num. \s. IMAGE f s) v)`; 88 89 90val PATH_USED_VARS_def = 91 Define 92 `(PATH_USED_VARS w = BIGUNION {w n | n >= 0})`; 93 94 95val IMP_ON_PATH_RESTN_def = 96 Define 97 `IMP_ON_PATH_RESTN (k:num) v a b = !t:num. (t >= k) ==> ((P_SEM (v t) a) ==> (P_SEM (v t) b))`; 98 99 100val EQUIV_ON_PATH_RESTN_def = 101 Define 102 `EQUIV_ON_PATH_RESTN (k:num) v a b = !t:num. (t >= k) ==> ((P_SEM (v t) a) = (P_SEM (v t) b))`; 103 104 105val NAND_ON_PATH_RESTN_def = 106 Define 107 `NAND_ON_PATH_RESTN (k:num) v a b = !t:num. (t >= k) ==> (~(P_SEM (v t) a) \/ ~(P_SEM (v t) b))`; 108 109 110val BEFORE_ON_PATH_RESTN_def = 111 Define 112 `BEFORE_ON_PATH_RESTN (t:num) v a b = !t':num. (t <= t' /\ (P_SEM (v t') b)) ==> (?u:num. t <= u /\ u <= t' /\ P_SEM (v u) a)`; 113 114 115val BEFORE_ON_PATH_RESTN_STRONG_def = 116 Define 117 `BEFORE_ON_PATH_RESTN_STRONG (t:num) v a b = !t':num. (t <= t' /\ (P_SEM (v t') b)) ==> (?u:num. t <= u /\ u < t' /\ P_SEM (v u) a)`; 118 119 120val NOT_ON_PATH_RESTN_def = 121 Define 122 `NOT_ON_PATH_RESTN (t:num) v a = !t':num. (t <= t') ==> ~P_SEM (v t') a`; 123 124 125val IS_ON_PATH_RESTN_def = 126 Define 127 `IS_ON_PATH_RESTN (t:num) v a = ~(NOT_ON_PATH_RESTN t v a)`; 128 129 130val EQUIV_PATH_RESTN_def = 131 Define `EQUIV_PATH_RESTN (t:num) v1 v2 = 132 ((!l:num. t <= l ==> ((v1 l) = (v2 l))))`; 133 134 135val PATH_EXTENSION_def = 136 Define 137 `(PATH_EXTENSION w (q:'a) (P:num->bool)) = 138 (\n:num. (if (P n) then (q INSERT w n) else (w n)))`; 139 140val CHOOSEN_PATH_def = 141Define 142 `(CHOOSEN_PATH S0 S 0 = @x. x IN S0) /\ 143 (CHOOSEN_PATH S0 S (SUC n) = @x. x IN (S (CHOOSEN_PATH S0 S n) (SUC n)))`; 144 145val INF_ELEMENTS_OF_PATH_def = 146Define 147`INF_ELEMENTS_OF_PATH w = {s | !n. ?m. m > n /\ (w m = s)}`; 148 149val ELEMENTS_OF_PATH_def = 150Define 151`ELEMENTS_OF_PATH w = {s | ?m:num. (w m = s)}`; 152 153 154(****************************************************************************** 155* Lemmata about paths 156******************************************************************************) 157 158val PATH_USED_VARS_THM = 159 store_thm 160 ("PATH_USED_VARS_THM", 161 ``!w x. (?n. x IN w n) = (x IN PATH_USED_VARS w)``, 162 163 SIMP_TAC arith_ss [PATH_USED_VARS_def, IN_BIGUNION, GSPECIFICATION, EXISTS_PROD] THEN 164 METIS_TAC[]) 165 166 167val PATH_DIFF_EMPTY = 168 store_thm 169 ("PATH_DIFF_EMPTY", 170 ``!v. PATH_DIFF v EMPTY = v``, 171 172 REWRITE_TAC[PATH_DIFF_def, PATH_MAP_def, DIFF_DEF, NOT_IN_EMPTY] THEN 173 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 174 SIMP_TAC arith_ss [EXTENSION, GSPECIFICATION]); 175 176 177val PATH_DIFF_PATH_RESTRICT = 178 store_thm 179 ("PATH_DIFF_PATH_RESTRICT", 180 ``!v S. (PATH_DIFF v (COMPL S) = PATH_RESTRICT v S) /\ 181 (PATH_RESTRICT v (COMPL S) = PATH_DIFF v S)``, 182 183 REWRITE_TAC[PATH_DIFF_def, INTER_DEF, PATH_RESTRICT_def, PATH_MAP_def, DIFF_DEF, NOT_IN_EMPTY, IN_COMPL] THEN 184 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 185 SIMP_TAC arith_ss [EXTENSION, GSPECIFICATION]); 186 187 188val PATH_UNION_COMM = 189 store_thm 190 ("PATH_UNION_COMM", 191 ``!v w. PATH_UNION v w = PATH_UNION w v``, 192 193 REWRITE_TAC[PATH_UNION_def] THEN 194 PROVE_TAC [UNION_COMM]); 195 196 197val PATH_UNION_ASSOC = 198 store_thm 199 ("PATH_UNION_ASSOC", 200 ``!s t u. PATH_UNION s (PATH_UNION t u) = PATH_UNION (PATH_UNION s t) u``, 201 202 REWRITE_TAC[PATH_UNION_def] THEN 203 PROVE_TAC [UNION_ASSOC]); 204 205 206val PATH_UNION_EMPTY_PATH = 207 store_thm 208 ("PATH_UNION_EMPTY_PATH", 209 ``!v. (PATH_UNION v EMPTY_PATH = v) /\ (PATH_UNION EMPTY_PATH v = v)``, 210 211 REWRITE_TAC[PATH_UNION_def, EMPTY_PATH_def, UNION_EMPTY] THEN 212 METIS_TAC []); 213 214 215val PATH_RESTRICT_SUBSET = 216 store_thm 217 ("PATH_RESTRICT_SUBSET", 218 ``!v w S. (v = PATH_RESTRICT w S) ==> (!n. (v n) SUBSET S)``, 219 220 SIMP_TAC arith_ss [PATH_RESTRICT_def, PATH_MAP_def, SUBSET_DEF, INTER_DEF, GSPECIFICATION]); 221 222 223val PATH_RESTRICT_PATH_SUBSET = 224 store_thm 225 ("PATH_RESTRICT_PATH_SUBSET", 226 ``!w S. (PATH_RESTRICT w S = w) = PATH_SUBSET w S``, 227 228 SIMP_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, SUBSET_DEF] THEN 229 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 230 ASM_SIMP_TAC std_ss [EXTENSION, IN_INTER] THEN 231 PROVE_TAC[] 232 ); 233 234 235val PATH_SUBSET_PATH_DIFF = 236 store_thm 237 ("PATH_SUBSET_PATH_DIFF", 238 ``!w S1 S2. PATH_SUBSET (PATH_DIFF w S1) S2 = PATH_SUBSET w (S2 UNION S1)``, 239 240 SIMP_TAC std_ss [PATH_SUBSET_def, PATH_DIFF_def, SUBSET_DEF, IN_DIFF, IN_UNION] THEN 241 METIS_TAC[]); 242 243 244val PATH_PARTITION = 245 store_thm 246 ("PATH_PARTITION", 247 248 ``!w S1 S2. (PATH_SUBSET w (S1 UNION S2)) ==> (w = PATH_UNION (PATH_RESTRICT w S1) (PATH_RESTRICT w S2))``, 249 250 SIMP_TAC std_ss [PATH_UNION_def, 251 PATH_MAP_def, 252 PATH_RESTRICT_def, 253 INTER_DEF, 254 UNION_DEF, 255 PATH_SUBSET_def, 256 SUBSET_DEF] THEN 257 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 258 SIMP_TAC arith_ss [EXTENSION, GSPECIFICATION] THEN 259 REPEAT STRIP_TAC THEN 260 METIS_TAC [] 261) 262 263 264val PATH_VAR_RENAMING_11 = 265 store_thm 266 ("PATH_VAR_RENAMING_11", 267 268 ``!f S x y. (PATH_SUBSET x S /\ PATH_SUBSET y S /\ INJ f S UNIV) ==> 269 ((PATH_VAR_RENAMING f x = PATH_VAR_RENAMING f y) = (x = y))``, 270 271 SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, INJ_DEF, PATH_VAR_RENAMING_def, IN_UNIV, 272 PATH_MAP_def, IMAGE_DEF] THEN 273 REPEAT STRIP_TAC THEN 274 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 275 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN 276 METIS_TAC[]); 277 278 279val PATH_SUBSET_UNIV = 280 store_thm 281 ("PATH_SUBSET_UNIV", 282 283 ``!w. PATH_SUBSET w UNIV``, 284 285 REWRITE_TAC [PATH_SUBSET_def, SUBSET_UNIV]); 286 287 288val PATH_RESTN_PATH_RESTN_ELIM = 289 store_thm 290 ("PATH_RESTN_PATH_RESTN_ELIM", 291 ``!v n1 n2. (PATH_RESTN (PATH_RESTN v n1) n2) = PATH_RESTN v (n1+n2)``, 292 293 SIMP_TAC arith_ss [PATH_RESTN_def]); 294 295 296val IMP_ON_PATH_RESTN___GREATER_IMPL = 297 store_thm 298 ("IMP_ON_PATH_RESTN___GREATER_IMPL", 299 ``!v t a b. IMP_ON_PATH_RESTN t v a b = (!t'. t' >= t ==> IMP_ON_PATH_RESTN t' v a b)``, 300 SIMP_TAC arith_ss [IMP_ON_PATH_RESTN_def] THEN 301 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 302 METIS_TAC[GREATER_EQ, LESS_EQ_TRANS], 303 METIS_TAC[GREATER_EQ, LESS_EQ_REFL] 304 ]); 305 306 307val EQUIV_ON_PATH_RESTN___IMP_ON_PATH_RESTN = 308 store_thm 309 ("EQUIV_ON_PATH_RESTN___IMP_ON_PATH_RESTN", 310 ``!t v a1 a2. (EQUIV_ON_PATH_RESTN t v a1 a2) = 311 (IMP_ON_PATH_RESTN t v a1 a2 /\ IMP_ON_PATH_RESTN t v a2 a1)``, 312 313 REWRITE_TAC[IMP_ON_PATH_RESTN_def, EQUIV_ON_PATH_RESTN_def] THEN 314 METIS_TAC[]); 315 316 317val EQUIV_ON_PATH_RESTN___GREATER_IMPL = 318 store_thm 319 ("EQUIV_ON_PATH_RESTN___GREATER_IMPL", 320 ``!v t a b. EQUIV_ON_PATH_RESTN t v a b = (!t'. t' >= t ==> EQUIV_ON_PATH_RESTN t' v a b)``, 321 METIS_TAC[IMP_ON_PATH_RESTN___GREATER_IMPL,EQUIV_ON_PATH_RESTN___IMP_ON_PATH_RESTN]); 322 323 324val NAND_ON_PATH_RESTN___GREATER_IMPL = 325 store_thm 326 ("NAND_ON_PATH_RESTN___GREATER_IMPL", 327 ``!v t a b. NAND_ON_PATH_RESTN t v a b = (!t'. t' >= t ==> NAND_ON_PATH_RESTN t' v a b)``, 328 SIMP_TAC arith_ss [NAND_ON_PATH_RESTN_def] THEN 329 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 330 METIS_TAC[GREATER_EQ, LESS_EQ_TRANS], 331 METIS_TAC[GREATER_EQ, LESS_EQ_REFL] 332 ]); 333 334 335val NOT_ON_PATH_RESTN___GREATER_IMPL = 336 store_thm 337 ("NOT_ON_PATH_RESTN___GREATER_IMPL", 338 ``!v t a. NOT_ON_PATH_RESTN t v a = (!t'. t' >= t ==> NOT_ON_PATH_RESTN t' v a)``, 339 SIMP_TAC arith_ss [NOT_ON_PATH_RESTN_def] THEN 340 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 341 METIS_TAC[GREATER_EQ, LESS_EQ_TRANS], 342 METIS_TAC[GREATER_EQ, LESS_EQ_REFL] 343 ]); 344 345 346val IS_ON_PATH_RESTN___GREATER_IMPL = 347 store_thm 348 ("IS_ON_PATH_RESTN___GREATER_IMPL", 349 ``!v t a. IS_ON_PATH_RESTN t v a = (?t0. (t <= t0) /\ (P_SEM (v t0) a) /\ (!t'. (t <= t' /\ t' <= t0) ==> IS_ON_PATH_RESTN t' v a))``, 350 351 SIMP_TAC arith_ss [IS_ON_PATH_RESTN_def, NOT_ON_PATH_RESTN_def] THEN 352 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 353 EXISTS_TAC ``t':num`` THEN 354 METIS_TAC[], 355 356 EXISTS_TAC ``t0:num`` THEN 357 METIS_TAC[] 358 ]); 359 360 361val EQUIV_PATH_RESTN___GREATER_IMPL = 362 store_thm 363 ("EQUIV_PATH_RESTN___GREATER_IMPL", 364 ``!t v1 v2. EQUIV_PATH_RESTN t v1 v2 = (!t'. t' >= t ==> EQUIV_PATH_RESTN t' v1 v2)``, 365 SIMP_TAC arith_ss [EQUIV_PATH_RESTN_def] THEN 366 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 367 METIS_TAC[GREATER_EQ, LESS_EQ_TRANS], 368 METIS_TAC[GREATER_EQ, LESS_EQ_REFL] 369 ]); 370 371 372val EQUIV_PATH_RESTN___PATH_RESTN = 373 store_thm 374 ("EQUIV_PATH_RESTN___PATH_RESTN", 375 ``!t v1 v2. (EQUIV_PATH_RESTN t v1 v2) = (PATH_RESTN v1 t = PATH_RESTN v2 t)``, 376 SIMP_TAC arith_ss [EQUIV_PATH_RESTN_def, PATH_RESTN_def, EXTENSION] THEN 377 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 378 SIMP_TAC std_ss [EXTENSION] THEN 379 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 380 `t <= t+x` by DECIDE_TAC THEN 381 METIS_TAC[], 382 383 `?x. t + x = l` by METIS_TAC[LESS_EQ_EXISTS] THEN 384 METIS_TAC[] 385 ]); 386 387 388val EQUIV_PATH_RESTN_SYM = 389 store_thm 390 ("EQUIV_PATH_RESTN_SYM", 391 ``!v1 v2 t. EQUIV_PATH_RESTN t v1 v2 = EQUIV_PATH_RESTN t v2 v1``, 392 EVAL_TAC THEN PROVE_TAC[]); 393 394 395val BEFORE_ON_PATH_STRONG___BEFORE_ON_PATH = 396 store_thm 397 ("BEFORE_ON_PATH_STRONG___BEFORE_ON_PATH", 398 ``!v t a b. BEFORE_ON_PATH_RESTN_STRONG t v a b ==> BEFORE_ON_PATH_RESTN t v a b``, 399 REWRITE_TAC [BEFORE_ON_PATH_RESTN_STRONG_def, BEFORE_ON_PATH_RESTN_def] THEN 400 REPEAT STRIP_TAC THEN 401 `?u. t <= u /\ u < t' /\ P_SEM (v u) a` by PROVE_TAC[] THEN 402 EXISTS_TAC ``u:num`` THEN 403 FULL_SIMP_TAC arith_ss []); 404 405 406val BEFORE_ON_PATH___SUC = 407 store_thm 408 ("BEFORE_ON_PATH___SUC", 409 ``!v t a b. ((BEFORE_ON_PATH_RESTN t v a b) /\ ~(P_SEM (v t) a)) ==> (BEFORE_ON_PATH_RESTN (SUC t) v a b)``, 410 REWRITE_TAC [BEFORE_ON_PATH_RESTN_def] THEN 411 REPEAT STRIP_TAC THEN 412 `t <= t'` by DECIDE_TAC THEN 413 RES_TAC THEN 414 EXISTS_TAC ``u:num`` THEN 415 ASM_REWRITE_TAC[] THEN 416 `~(u = t)` by METIS_TAC[] THEN 417 DECIDE_TAC); 418 419 420val BEFORE_ON_PATH_STRONG___SUC = 421 store_thm 422 ("BEFORE_ON_PATH_STRONG___SUC", 423 ``!v t a b. ((BEFORE_ON_PATH_RESTN_STRONG t v a b) /\ ~(P_SEM (v t) a)) ==> (BEFORE_ON_PATH_RESTN_STRONG (SUC t) v a b)``, 424 REWRITE_TAC [BEFORE_ON_PATH_RESTN_STRONG_def] THEN 425 REPEAT STRIP_TAC THEN 426 `t <= t'` by DECIDE_TAC THEN 427 RES_TAC THEN 428 EXISTS_TAC ``u:num`` THEN 429 ASM_REWRITE_TAC[] THEN 430 `~(u = t)` by METIS_TAC[] THEN 431 DECIDE_TAC); 432 433 434val NOT_ON_PATH___IMP_ON_PATH = 435 store_thm 436 ("NOT_ON_PATH___IMP_ON_PATH", 437 ``!v t a1 a2. NOT_ON_PATH_RESTN t v a1 ==> IMP_ON_PATH_RESTN t v a1 a2``, 438 439 METIS_TAC[NOT_ON_PATH_RESTN_def, IMP_ON_PATH_RESTN_def, GREATER_EQ] 440); 441 442 443val NOT_ON_PATH___BEFORE_ON_PATH_STRONG = 444 store_thm 445 ("NOT_ON_PATH___BEFORE_ON_PATH_STRONG", 446 ``!v t a1 a2. NOT_ON_PATH_RESTN t v a2 ==> BEFORE_ON_PATH_RESTN_STRONG t v a1 a2``, 447 448 PROVE_TAC[NOT_ON_PATH_RESTN_def, BEFORE_ON_PATH_RESTN_STRONG_def] 449); 450 451 452val BEFORE_ON_PATH_STRONG___LESS_IMPL = 453 store_thm 454 ("BEFORE_ON_PATH_STRONG___LESS_IMPL", 455 ``!v t t2 a1 a2. 456 (t <= t2 /\ (!j. (t <= j /\ j < t2) ==> ~(P_SEM (v j) a2)) /\ 457 BEFORE_ON_PATH_RESTN_STRONG t2 v a1 a2) ==> (BEFORE_ON_PATH_RESTN_STRONG t v a1 a2)``, 458 459 REWRITE_TAC[BEFORE_ON_PATH_RESTN_STRONG_def] THEN 460 REPEAT STRIP_TAC THEN 461 `~(t' < t2)` by METIS_TAC[] THEN 462 `t2 <= t'` by DECIDE_TAC THEN 463 `?u. t2 <= u /\ u < t' /\ P_SEM (v u) a1` by METIS_TAC[] THEN 464 EXISTS_TAC ``u:num`` THEN 465 ASM_REWRITE_TAC[] THEN 466 DECIDE_TAC); 467 468 469val BEFORE_ON_PATH___LESS_IMPL = 470 store_thm 471 ("BEFORE_ON_PATH___LESS_IMPL", 472 ``!v t t2 a1 a2. 473 (t <= t2 /\ (!j. (t <= j /\ j < t2) ==> ~(P_SEM (v j) a2)) /\ 474 BEFORE_ON_PATH_RESTN t2 v a1 a2) ==> (BEFORE_ON_PATH_RESTN t v a1 a2)``, 475 476 REWRITE_TAC[BEFORE_ON_PATH_RESTN_def] THEN 477 REPEAT STRIP_TAC THEN 478 `~(t' < t2)` by METIS_TAC[] THEN 479 `t2 <= t'` by DECIDE_TAC THEN 480 `?u. t2 <= u /\ u <= t' /\ P_SEM (v u) a1` by METIS_TAC[] THEN 481 EXISTS_TAC ``u:num`` THEN 482 ASM_REWRITE_TAC[] THEN 483 DECIDE_TAC); 484 485 486val BEFORE_ON_PATH_STRONG___GREATER_IMPL = 487 store_thm 488 ("BEFORE_ON_PATH_STRONG___GREATER_IMPL", 489 ``!v t t2 a1 a2. 490 (t <= t2 /\ (!j. (t <= j /\ j < t2) ==> ~(P_SEM (v j) a1)) /\ 491 BEFORE_ON_PATH_RESTN_STRONG t v a1 a2) ==> (BEFORE_ON_PATH_RESTN_STRONG t2 v a1 a2)``, 492 493 REWRITE_TAC[BEFORE_ON_PATH_RESTN_STRONG_def] THEN 494 REPEAT STRIP_TAC THEN 495 `t <= t'` by DECIDE_TAC THEN 496 `?u. t <= u /\ u < t' /\ P_SEM (v u) a1` by METIS_TAC[] THEN 497 EXISTS_TAC ``u:num`` THEN 498 ASM_REWRITE_TAC[] THEN 499 `~(u < t2)` by METIS_TAC[] THEN 500 DECIDE_TAC); 501 502 503val BEFORE_ON_PATH___GREATER_IMPL = 504 store_thm 505 ("BEFORE_ON_PATH___GREATER_IMPL", 506 ``!v t t2 a1 a2. 507 (t <= t2 /\ (!j. (t <= j /\ j < t2) ==> ~(P_SEM (v j) a1)) /\ 508 BEFORE_ON_PATH_RESTN t v a1 a2) ==> (BEFORE_ON_PATH_RESTN t2 v a1 a2)``, 509 510 REWRITE_TAC[BEFORE_ON_PATH_RESTN_def] THEN 511 REPEAT STRIP_TAC THEN 512 `t <= t'` by DECIDE_TAC THEN 513 `?u. t <= u /\ u <= t' /\ P_SEM (v u) a1` by METIS_TAC[] THEN 514 EXISTS_TAC ``u:num`` THEN 515 ASM_REWRITE_TAC[] THEN 516 `~(u < t2)` by METIS_TAC[] THEN 517 DECIDE_TAC); 518 519 520val BEFORE_ON_PATH___IMPL_START = 521 store_thm 522 ("BEFORE_ON_PATH___IMPL_START", 523 ``!v t a1 a2. (BEFORE_ON_PATH_RESTN t v a1 a2 /\ P_SEM (v t) a2) ==> P_SEM (v t) a1``, 524 525 REWRITE_TAC[BEFORE_ON_PATH_RESTN_def] THEN 526 METIS_TAC[LESS_EQ_REFL, EQ_LESS_EQ]); 527 528 529val BEFORE_ON_PATH___IMPL_START2 = 530 store_thm 531 ("BEFORE_ON_PATH___IMPL_START2", 532 ``!v t a1 a2. P_SEM (v t) a1 ==> BEFORE_ON_PATH_RESTN t v a1 a2``, 533 534 REWRITE_TAC[BEFORE_ON_PATH_RESTN_def] THEN 535 METIS_TAC[LESS_EQ_REFL]); 536 537 538val BEFORE_ON_PATH_STRONG___IMPL_START = 539 store_thm 540 ("BEFORE_ON_PATH_STRONG___IMPL_START", 541 ``!v t a1 a2. (BEFORE_ON_PATH_RESTN_STRONG t v a1 a2) ==> ~P_SEM (v t) a2``, 542 543 REWRITE_TAC[BEFORE_ON_PATH_RESTN_STRONG_def] THEN 544 METIS_TAC[NOT_LESS, LESS_EQ_REFL]); 545 546 547val BEFORE_ON_PATH_STRONG___IMPL_START2 = 548 store_thm 549 ("BEFORE_ON_PATH_STRONG___IMPL_START2", 550 ``!v t a1 a2. P_SEM (v t) a1 /\ ~P_SEM (v t) a2 ==> BEFORE_ON_PATH_RESTN_STRONG t v a1 a2``, 551 REWRITE_TAC[BEFORE_ON_PATH_RESTN_STRONG_def] THEN 552 REPEAT STRIP_TAC THEN 553 `~(t = t')` by PROVE_TAC[] THEN 554 `t < t'` by DECIDE_TAC THEN 555 EXISTS_TAC ``t:num`` THEN 556 PROVE_TAC[LESS_EQ_REFL]); 557 558 559val BEFORE_ON_PATH_CASES = 560 store_thm 561 ("BEFORE_ON_PATH_CASES", 562 ``!v t a1 a2. BEFORE_ON_PATH_RESTN t v a1 a2 \/ BEFORE_ON_PATH_RESTN t v a2 a1``, 563 564 REPEAT STRIP_TAC THEN 565 Cases_on `BEFORE_ON_PATH_RESTN t v a1 a2` THENL [ 566 ASM_REWRITE_TAC[], 567 568 ASM_REWRITE_TAC [] THEN 569 FULL_SIMP_TAC arith_ss [BEFORE_ON_PATH_RESTN_def] THEN 570 REPEAT STRIP_TAC THEN 571 `~(t'' <= t')` by PROVE_TAC[] THEN 572 `t' <= t''` by DECIDE_TAC THEN 573 EXISTS_TAC ``t':num`` THEN 574 PROVE_TAC[] 575 ]); 576 577 578val BEFORE_ON_PATH___SUC = 579 store_thm 580 ("BEFORE_ON_PATH___SUC", 581 ``!v t a1 a2. BEFORE_ON_PATH_RESTN t v a1 a2 ==> (P_SEM (v t) a1 \/ BEFORE_ON_PATH_RESTN (SUC t) v a1 a2)``, 582 583 REPEAT STRIP_TAC THENL [ 584 Cases_on `P_SEM (v t) a1` THENL [ 585 ASM_REWRITE_TAC[], 586 587 FULL_SIMP_TAC arith_ss [BEFORE_ON_PATH_RESTN_def] THEN 588 REPEAT STRIP_TAC THEN 589 `t <= t'` by DECIDE_TAC THEN 590 `?u. t <= u /\ u <= t' /\ P_SEM (v u) a1` by METIS_TAC[] THEN 591 `~(u = t)` by METIS_TAC[] THEN 592 `SUC t <= u` by DECIDE_TAC THEN 593 METIS_TAC[] 594 ] 595 ]); 596 597 598val BEFORE_ON_PATH_STRONG___SUC = 599 store_thm 600 ("BEFORE_ON_PATH_STRONG___SUC", 601 ``!v t a1 a2. BEFORE_ON_PATH_RESTN_STRONG t v a1 a2 ==> (P_SEM (v t) a1 \/ BEFORE_ON_PATH_RESTN_STRONG (SUC t) v a1 a2)``, 602 603 REPEAT STRIP_TAC THENL [ 604 Cases_on `P_SEM (v t) a1` THENL [ 605 ASM_REWRITE_TAC[], 606 607 FULL_SIMP_TAC arith_ss [BEFORE_ON_PATH_RESTN_STRONG_def] THEN 608 REPEAT STRIP_TAC THEN 609 `t <= t'` by DECIDE_TAC THEN 610 `?u. t <= u /\ u < t' /\ P_SEM (v u) a1` by METIS_TAC[] THEN 611 `~(u = t)` by METIS_TAC[] THEN 612 `SUC t <= u` by DECIDE_TAC THEN 613 METIS_TAC[] 614 ] 615 ]); 616 617 618val BEFORE_ON_PATH_RESTN___NEGATION_IMPL = 619 store_thm 620 ("BEFORE_ON_PATH_RESTN___NEGATION_IMPL", 621 ``!t v a b. ~(BEFORE_ON_PATH_RESTN t v a b) ==> BEFORE_ON_PATH_RESTN_STRONG t v b a``, 622 623 SIMP_TAC arith_ss [BEFORE_ON_PATH_RESTN_def, BEFORE_ON_PATH_RESTN_STRONG_def] THEN 624 REPEAT STRIP_TAC THEN 625 EXISTS_TAC ``t':num`` THEN 626 ASM_REWRITE_TAC[] THEN 627 CCONTR_TAC THEN 628 `t'' <= t'` by DECIDE_TAC THEN 629 METIS_TAC[]); 630 631 632val ELEMENTS_OF_PATH_NOT_EMPTY = 633 store_thm 634 ("ELEMENTS_OF_PATH_NOT_EMPTY", 635 ``!w. ~(ELEMENTS_OF_PATH w = EMPTY)``, 636 637 SIMP_TAC std_ss [ELEMENTS_OF_PATH_def, EXTENSION, GSPECIFICATION, NOT_IN_EMPTY]); 638 639 640val INF_ELEMENTS_OF_PATH_NOT_EMPTY = 641 store_thm 642 ("INF_ELEMENTS_OF_PATH_NOT_EMPTY", 643 ``!S. FINITE S ==> (!w. ((!n. w n IN S) ==> ~(INF_ELEMENTS_OF_PATH w = EMPTY)))``, 644 645 PSet_ind.SET_INDUCT_TAC FINITE_INDUCT THEN1 REWRITE_TAC[NOT_IN_EMPTY] THEN 646 647 REPEAT STRIP_TAC THEN 648 Cases_on `e IN INF_ELEMENTS_OF_PATH w` THEN1 ( 649 METIS_TAC[NOT_IN_EMPTY] 650 ) THEN 651 SUBGOAL_THEN ``~(s:'a set = EMPTY)`` ASSUME_TAC THEN1 ( 652 CCONTR_TAC THEN 653 FULL_SIMP_TAC arith_ss [INF_ELEMENTS_OF_PATH_def, EXTENSION, GSPECIFICATION, 654 NOT_IN_EMPTY, IN_SING, IN_INSERT] THEN 655 `SUC n > n` by DECIDE_TAC THEN 656 PROVE_TAC[] 657 ) THEN 658 `?x. x IN s` by PROVE_TAC [MEMBER_NOT_EMPTY] THEN 659 660 `?w'. w' = \n. if (w n = e) then x else w n` by METIS_TAC[] THEN 661 SUBGOAL_THEN ``!n:num. w' n IN (s:'a set)`` ASSUME_TAC THEN1 ( 662 ASM_SIMP_TAC std_ss [] THEN 663 REPEAT STRIP_TAC THEN 664 Cases_on `w n = e` THEN ASM_REWRITE_TAC[] THEN 665 PROVE_TAC[IN_INSERT] 666 ) THEN 667 668 SUBGOAL_THEN ``?n. !m. m > n ==> (w m = w' m)`` STRIP_ASSUME_TAC THEN1 ( 669 FULL_SIMP_TAC std_ss [INF_ELEMENTS_OF_PATH_def, GSPECIFICATION] THEN 670 PROVE_TAC[] 671 ) THEN 672 673 SUBGOAL_THEN ``INF_ELEMENTS_OF_PATH w = INF_ELEMENTS_OF_PATH w'`` ASSUME_TAC THEN1 ( 674 SIMP_TAC std_ss [INF_ELEMENTS_OF_PATH_def, EXTENSION, GSPECIFICATION] THEN 675 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 676 `?n''. n'' > n /\ n'' > n'` by (EXISTS_TAC ``SUC(n + n')`` THEN DECIDE_TAC) THEN 677 `?m. m > n'' /\ (w m = x') /\ (w' m = x')` by METIS_TAC[] THEN 678 METIS_TAC[], 679 680 `?n''. n'' > n /\ n'' > n'` by (EXISTS_TAC ``SUC(n + n')`` THEN DECIDE_TAC) THEN 681 `?m. m > n'' /\ (w' m = x')` by METIS_TAC[] THEN 682 `m > n /\ m > n'` by DECIDE_TAC THEN 683 `w m = x'` by PROVE_TAC[] THEN 684 METIS_TAC[] 685 ] 686 ) THEN 687 688 PROVE_TAC[]); 689 690 691 692 693val PATH_EXTENSION_EQUIV_THM = 694 store_thm 695 ("PATH_EXTENSION_EQUIV_THM", 696 ``!w q P S. (PATH_SUBSET w S /\ ~(q IN S)) ==> ( 697 698 !w'. (w' = (PATH_EXTENSION w q P)) = 699 ((PATH_SUBSET w' (q INSERT S)) /\ 700 ((PATH_DIFF w' {q}) = w) /\ 701 ((PATH_RESTRICT w' S) = w) /\ 702 (!n. (q IN (w' n)) = (P n))))``, 703 704 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 705 REPEAT DISCH_TAC THEN 706 ASM_SIMP_TAC std_ss [] THEN 707 `S SUBSET q INSERT S` by SIMP_TAC std_ss [SUBSET_DEF, IN_INSERT] THEN 708 ONCE_REWRITE_TAC[FUN_EQ_THM, PATH_SUBSET_def] THEN 709 SIMP_TAC std_ss [GSYM FORALL_AND_THM, PATH_EXTENSION_def] THEN 710 GEN_TAC THEN 711 Cases_on `P n` THEN ( 712 FULL_SIMP_TAC std_ss [PATH_DIFF_def, SUBSET_DEF, IN_INSERT, DIFF_DEF, EXTENSION, GSPECIFICATION, 713 NOT_IN_EMPTY, PATH_RESTRICT_def, PATH_MAP_def, IN_INTER, PATH_SUBSET_def] THEN 714 METIS_TAC[] 715 ), 716 717 REWRITE_TAC[PATH_EXTENSION_def] THEN 718 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 719 REPEAT STRIP_TAC THEN 720 Cases_on `P x` THEN ( 721 FULL_SIMP_TAC std_ss [PATH_DIFF_def, SUBSET_DEF, IN_INSERT, DIFF_DEF, EXTENSION, GSPECIFICATION, 722 NOT_IN_EMPTY, PATH_RESTRICT_def, PATH_MAP_def, IN_INTER, PATH_SUBSET_def] THEN 723 METIS_TAC[] 724 ) 725 ]); 726 727 728val PATH_VAR_RENAMING___ORIG_PATH_EXISTS = 729 store_thm 730 ("PATH_VAR_RENAMING___ORIG_PATH_EXISTS", 731 732 ``!w f S. (PATH_SUBSET w (IMAGE f S)) ==> (?w'. (PATH_SUBSET w' S) /\ (w = PATH_VAR_RENAMING f w'))``, 733 734 SIMP_TAC std_ss [IMAGE_DEF, PATH_SUBSET_def, PATH_VAR_RENAMING_def, PATH_MAP_def, SUBSET_DEF, GSPECIFICATION] THEN 735 REPEAT STRIP_TAC THEN 736 SUBGOAL_TAC `?w'. !x n. x IN (w' n) = ((f x) IN w n /\ x IN S)` THEN1 ( 737 Q_TAC EXISTS_TAC `\n:num x. (f x) IN w n /\ x IN S` THEN 738 SIMP_TAC std_ss [IN_DEF] 739 ) THEN 740 Q_TAC EXISTS_TAC `w'` THEN 741 REPEAT STRIP_TAC THENL [ 742 PROVE_TAC[], 743 744 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 745 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN 746 PROVE_TAC[] 747 ]); 748 749 750val IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE_def = 751 Define 752 `IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE p n0 n = 753 !m. (m >= n0) ==> ((p m) = (p (m+n)))`; 754 755 756val IS_ULTIMATIVELY_PERIODIC_PATH_def = 757 Define 758 `IS_ULTIMATIVELY_PERIODIC_PATH p = 759 ?n0 n. 0 < n /\ IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE p n0 n`; 760 761 762val IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE___ALTERNATIVE_DEF = 763 store_thm ("IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE___ALTERNATIVE_DEF", 764 ``!p n0 n. 0 < n ==> 765 (IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE p n0 n = 766 (!m. p (n0 + m) = p (n0 + m MOD n)))``, 767 768 SIMP_TAC std_ss [IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE_def] THEN 769 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 770 Induct_on `m DIV n` THENL [ 771 REPEAT STRIP_TAC THEN 772 `m = (m DIV n)*n + m MOD n` by PROVE_TAC[DIVISION] THEN 773 UNDISCH_HD_TAC THEN 774 GSYM_NO_TAC 2 THEN 775 ASM_SIMP_TAC std_ss [], 776 777 REPEAT STRIP_TAC THEN 778 `m = (SUC v)*n + m MOD n` by PROVE_TAC[DIVISION] THEN 779 SIMP_ALL_TAC std_ss [MULT] THEN 780 `n <= m` by DECIDE_TAC THEN 781 `n*1 = n` by DECIDE_TAC THEN 782 `(m-n) DIV n = (SUC v) - 1` by METIS_TAC[DIV_SUB] THEN 783 `(m-n) MOD n = m MOD n` by METIS_TAC[MOD_SUB] THEN 784 `((SUC v) - 1) = v` by DECIDE_TAC THEN 785 786 Q_SPECL_NO_ASSUM 9 [`m - n`, `n`] THEN 787 UNDISCH_HD_TAC THEN 788 ASM_SIMP_TAC std_ss [] THEN 789 Q_SPEC_NO_ASSUM 6 `n0 + (m - n)` THEN 790 FULL_SIMP_TAC arith_ss [] 791 ], 792 793 `?m'. m' = m - n0` by METIS_TAC[] THEN 794 `m = n0 + m'` by DECIDE_TAC THEN 795 METIS_TAC[ADD_ASSOC, ADD_MODULUS] 796 ]); 797 798 799val CUT_PATH_PERIODICALLY_def = 800 Define 801 `CUT_PATH_PERIODICALLY p n0 n = 802 \x. if (x < n0) then (p x) else (p (n0 + (x - n0) MOD n))`; 803 804 805val CUT_PATH_PERIODICALLY___BEGINNING = 806 store_thm ("CUT_PATH_PERIODICALLY___BEGINNING", 807 ``!n0 n p t. (t < (n+n0)) ==> (((CUT_PATH_PERIODICALLY p n0 n) t) = (p t))``, 808 809 SIMP_TAC std_ss [CUT_PATH_PERIODICALLY_def] THEN 810 REPEAT STRIP_TAC THEN 811 Cases_on `t < n0` THENL [ 812 ASM_REWRITE_TAC[], 813 814 `t - n0 < n` by DECIDE_TAC THEN 815 ASM_SIMP_TAC arith_ss [LESS_MOD] 816 ]); 817 818 819val CUT_PATH_PERIODICALLY_1 = 820 store_thm ("CUT_PATH_PERIODICALLY_1", 821 ``!n0 p t. (t >= n0) ==> (((CUT_PATH_PERIODICALLY p n0 1) t) = (p n0))``, 822 823 ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY_def]); 824 825 826 827val CUT_PATH_PERIODICALLY___IS_ULTIMATIVELY_PERIODIC = 828 store_thm ("CUT_PATH_PERIODICALLY___IS_ULTIMATIVELY_PERIODIC", 829 ``!p n0 n. IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE (CUT_PATH_PERIODICALLY p n0 n) n0 n``, 830 831 SIMP_TAC std_ss [IS_ULTIMATIVELY_PERIODIC_PATH___CONCRETE_def, 832 CUT_PATH_PERIODICALLY_def] THEN 833 REPEAT STRIP_TAC THEN 834 ASM_SIMP_TAC arith_ss [] THEN 835 Cases_on `n = 0` THENL [ 836 ASM_SIMP_TAC arith_ss [], 837 838 `0 < n /\ ((m + n - n0) = (n + (m - n0)))` by DECIDE_TAC THEN 839 ASM_SIMP_TAC std_ss [arithmeticTheory.ADD_MODULUS_RIGHT] 840 ]); 841 842 843 844 845val PATH_RESTRICT___CUT_PATH_PERIODICALLY = 846 store_thm ( 847 "PATH_RESTRICT___CUT_PATH_PERIODICALLY", 848 849 ``!p n0 n S. 850 (PATH_RESTRICT (CUT_PATH_PERIODICALLY p n0 n) S) = 851 (CUT_PATH_PERIODICALLY (PATH_RESTRICT p S) n0 n)``, 852 853 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 854 REPEAT GEN_TAC THEN 855 SIMP_TAC std_ss [CUT_PATH_PERIODICALLY_def, PATH_RESTRICT_def, PATH_MAP_def, COND_RAND]); 856 857 858val PATH_SUBSET_RESTRICT = store_thm ("PATH_SUBSET_RESTRICT", 859 ``!w S. PATH_SUBSET (PATH_RESTRICT w S) S``, 860SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INTER_SUBSET, PATH_SUBSET_def]) 861 862 863val _ = export_theory(); 864