1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6 7loadPath := (Globals.HOLDIR ^ "/examples/PSL/path") :: 8 (Globals.HOLDIR ^ "/examples/PSL/1.1/official-semantics") :: 9 (Globals.HOLDIR ^ "/examples/temporal_deep/src/tools") :: 10 !loadPath; 11 12map load 13 ["FinitePSLPathTheory", "PSLPathTheory", "ClockedSemanticsTheory", "UnclockedSemanticsTheory", "LemmasTheory", "RewritesTheory", "numLib", 14 "RewritesPropertiesTheory", "ProjectionTheory", "SyntacticSugarTheory", "arithmeticTheory", "ModelTheory", "res_quanTools", 15 "rich_listTheory", "pred_setTheory", "combinTheory", "tuerk_tacticsLib", "temporal_deep_mixedTheory", 16 "set_lemmataTheory"]; 17*) 18 19open FinitePSLPathTheory PSLPathTheory UnclockedSemanticsTheory ClockedSemanticsTheory LemmasTheory RewritesTheory RewritesPropertiesTheory 20 ProjectionTheory SyntacticSugarTheory arithmeticTheory ModelTheory rich_listTheory pred_setTheory combinTheory 21 res_quanTools numLib tuerk_tacticsLib temporal_deep_mixedTheory set_lemmataTheory listTheory; 22open Sanity; 23 24val _ = hide "S"; 25val _ = hide "I"; 26 27(* 28show_assums := false; 29show_assums := true; 30show_types := true; 31show_types := false; 32quietdec := false; 33*) 34 35 36 37 38val _ = new_theory "psl_lemmata"; 39 40 41val IS_INFINITE_PROPER_PATH_def = 42 Define 43 `IS_INFINITE_PROPER_PATH f = ?p. ((f = INFINITE p) /\ (!n. (p n = TOP) ==> (p (SUC n) = TOP)) /\ 44 (!n. (p n = BOTTOM) ==> (p (SUC n) = BOTTOM)))`; 45 46 47val IS_FINITE_PROPER_PATH_def = 48 Define 49 `IS_FINITE_PROPER_PATH f = ?p. ((f = FINITE p) /\ PATH_TOP_FREE f /\ PATH_BOTTOM_FREE f)`; 50 51 52val IS_INFINITE_TOP_BOTTOM_FREE_PATH_def = 53 Define 54 `IS_INFINITE_TOP_BOTTOM_FREE_PATH f = ?p. ((f = INFINITE p) /\ (!n. ?s. (p n = STATE s)))`; 55 56 57val IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT = 58 store_thm 59 ("IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT", 60 ``!f. IS_INFINITE_TOP_BOTTOM_FREE_PATH f ==> 61 (COMPLEMENT f = f)``, 62 63 REWRITE_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH_def] THEN 64 REPEAT STRIP_TAC THEN 65 ASM_SIMP_TAC std_ss [COMPLEMENT_def, path_11, o_DEF] THEN 66 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 67 BETA_TAC THEN GEN_TAC THEN 68 `?s. p x = STATE s` by PROVE_TAC[] THEN 69 ASM_REWRITE_TAC[COMPLEMENT_LETTER_def]); 70 71 72val IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN = 73 store_thm 74 ("IS_INFINITE_TOP_BOTTOM_FREE_PATH___RESTN", 75 ``!f. IS_INFINITE_TOP_BOTTOM_FREE_PATH f ==> 76 !n. IS_INFINITE_TOP_BOTTOM_FREE_PATH (RESTN f n)``, 77 78 REWRITE_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH_def] THEN 79 REPEAT STRIP_TAC THEN 80 ASM_SIMP_TAC std_ss [RESTN_INFINITE, path_11]); 81 82 83val IS_PROPER_PATH_def = 84 Define 85 `IS_PROPER_PATH f = IS_INFINITE_PROPER_PATH f \/ IS_FINITE_PROPER_PATH f`; 86 87val BOTTOM_OMEGA_def = 88 Define `BOTTOM_OMEGA = INFINITE(\n. BOTTOM)`; 89 90val COMPLEMENT_LETTER_Cases = 91 store_thm 92 ("COMPLEMENT_LETTER_Cases", 93 ``!l s. ((COMPLEMENT_LETTER l = STATE s) = (l = STATE s)) /\ 94 ((COMPLEMENT_LETTER l = TOP) = (l = BOTTOM)) /\ 95 ((COMPLEMENT_LETTER l = BOTTOM) = (l = TOP))``, 96 Cases_on `l` THEN EVAL_TAC THEN PROVE_TAC[]); 97 98val HEAD_ELEM = 99 store_thm 100 ("HEAD_ELEM", 101 ``!p. HEAD p = ELEM p 0``, 102 REWRITE_TAC[ELEM_def, RESTN_def]); 103 104 105val RESTN_MAP = 106 store_thm 107 ("RESTN_MAP", 108 ``!f v t. t < LENGTH v ==> (RESTN (MAP f v) t = MAP f (RESTN v t))``, 109 Induct_on `v` THENL [ 110 EVAL_TAC THEN PROVE_TAC[], 111 112 Induct_on `t` THENL [ 113 EVAL_TAC THEN PROVE_TAC[], 114 115 EVAL_TAC THEN 116 REPEAT STRIP_TAC THEN 117 `t < LENGTH v` by DECIDE_TAC THEN 118 PROVE_TAC[] 119 ] 120 ]); 121 122 123val REST_RESTN = 124 store_thm 125 ("REST_RESTN", 126 ``(!l:'a list. (REST l) = (RESTN l 1)) /\ 127 (!p:'a path. (REST p) = (RESTN p 1))``, 128 129 `1 = SUC 0` by DECIDE_TAC THEN 130 ASM_REWRITE_TAC [RESTN_def, FinitePSLPathTheory.RESTN_def]); 131 132 133val RESTN_REST = 134 store_thm 135 ("RESTN_REST", 136 ``(!l:'a list n. (RESTN (REST l) n) = (REST (RESTN l n))) /\ 137 (!p:'a path n. (RESTN (REST p) n) = (REST (RESTN p n)))``, 138 139 SIMP_TAC arith_ss [FinitePSLPathTheory.RESTN_RESTN, RESTN_RESTN, REST_RESTN]); 140 141 142val ELEM_CAT___LESS = 143 store_thm 144 ("ELEM_CAT___LESS", 145 ``!l l' p. l < LENGTH l' ==> (ELEM (CAT (l',p)) l = EL l l')``, 146 147 Induct_on `l` THENL [ 148 Cases_on `l'` THENL [ 149 SIMP_TAC list_ss [], 150 SIMP_TAC list_ss [CAT_def, ELEM_def, RESTN_def, HEAD_CONS] 151 ], 152 153 Cases_on `l'` THENL [ 154 SIMP_TAC list_ss [], 155 SIMP_TAC list_ss [CAT_def, ELEM_def, RESTN_def, REST_CONS] THEN PROVE_TAC [ELEM_def] 156 ] 157 ]); 158 159 160 161val EL_SEL_REC = 162 store_thm 163 ("EL_SEL_REC", 164 ``!j k l p. (j < k) ==> 165 (EL j (SEL_REC k l p) = ELEM p (j+l))``, 166 167Induct_on `l` THENL [ 168 SIMP_TAC std_ss [] THEN 169 Induct_on `j` THENL [ 170 Cases_on `k` THEN SIMP_TAC std_ss [] THEN 171 SIMP_TAC list_ss [SEL_REC_def, ELEM_def, RESTN_def], 172 173 Cases_on `k` THEN SIMP_TAC std_ss [] THEN 174 REPEAT STRIP_TAC THEN 175 SIMP_TAC list_ss [SEL_REC_def] THEN 176 Q_SPECL_NO_ASSUM 1 [`n`, `REST p`] THEN 177 RES_TAC THEN 178 ASM_REWRITE_TAC[ELEM_def, RESTN_def] 179 ], 180 181 REPEAT STRIP_TAC THEN 182 REWRITE_TAC[GSYM SEL_REC_REST] THEN 183 Q_SPECL_NO_ASSUM 1 [`j`, `k`, `REST p`] THEN 184 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 185 ASM_SIMP_TAC std_ss [prove (``j+SUC l = SUC(j+l)``, DECIDE_TAC)] THEN 186 SIMP_TAC std_ss [ELEM_def, RESTN_def] 187]); 188 189 190val ELEM_CAT_SEL___LESS_EQ = 191 store_thm 192 ("ELEM_CAT_SEL___LESS_EQ", 193 ``!v l u p. l <= u ==> (ELEM (CAT (SEL v (0, u),p)) l = ELEM v l)``, 194 195 REPEAT STRIP_TAC THEN 196 `LENGTH (SEL v (0, u)) = u -0 + 1` by PROVE_TAC[LENGTH_SEL] THEN 197 ASM_SIMP_TAC arith_ss [ELEM_CAT___LESS, EL_SEL0]); 198 199 200val ELEM_CAT___GREATER_EQ = 201 store_thm 202 ("ELEM_CAT___GREATER_EQ", 203 ``!l l' p. l >= LENGTH l' ==> (ELEM (CAT (l',p)) l = ELEM p (l - (LENGTH l')))``, 204 205 Induct_on `l` THENL [ 206 Cases_on `l'` THENL [ 207 SIMP_TAC list_ss [CAT_def], 208 SIMP_TAC list_ss [] 209 ], 210 211 Cases_on `l'` THENL [ 212 SIMP_TAC list_ss [CAT_def], 213 214 SIMP_TAC list_ss [ELEM_def, CAT_def, REST_CONS, RESTN_def] THEN 215 REPEAT STRIP_TAC THEN 216 `l >= LENGTH t` by DECIDE_TAC THEN 217 PROVE_TAC[ELEM_def] 218 ] 219 ]); 220 221 222val ELEM_CAT_SEL___GREATER = 223 store_thm 224 ("ELEM_CAT_SEL___GREATER", 225 ``!v l u p. l > u ==> (ELEM (CAT (SEL v (0, u),p)) l = ELEM p (l - SUC u))``, 226 227 REPEAT STRIP_TAC THEN 228 `LENGTH (SEL v (0, u)) = u -0 + 1` by PROVE_TAC[LENGTH_SEL] THEN 229 ASM_SIMP_TAC arith_ss [ELEM_CAT___GREATER_EQ, SUC_ONE_ADD]); 230 231 232val MAP_EQ_CONCAT = 233 store_thm 234 ("MAP_EQ_CONCAT", 235 236 ``!f l L. (MAP f l = CONCAT L) = 237 (?L'. (l = CONCAT L') /\ (L = MAP (\l. MAP f l) L'))``, 238 239Induct_on `L` THENL [ 240 SIMP_TAC list_ss [CONCAT_def], 241 242 ASM_SIMP_TAC list_ss [CONCAT_def, MAP_EQ_APPEND, GSYM LEFT_EXISTS_AND_THM, 243 GSYM RIGHT_EXISTS_AND_THM] THEN 244 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 245 Q_TAC EXISTS_TAC `l10::L'` THEN 246 ASM_SIMP_TAC list_ss [CONCAT_def], 247 248 249 Cases_on `L'` THEN 250 FULL_SIMP_TAC list_ss [CONCAT_def] THEN 251 Q_TAC EXISTS_TAC `h'` THEN 252 Q_TAC EXISTS_TAC `t` THEN 253 ASM_SIMP_TAC list_ss [] 254 ] 255]) 256 257val CONCAT_APPEND = 258 store_thm 259 ("CONCAT_APPEND", 260 ``!l1 l2. CONCAT (l1 <> l2) = (CONCAT l1 <> CONCAT l2)``, 261 262 Induct_on `l1` THENL [ 263 SIMP_TAC list_ss [CONCAT_def], 264 ASM_SIMP_TAC list_ss [CONCAT_def] 265 ]); 266 267val IS_FINITE_EXISTS = 268 store_thm 269 ("IS_FINITE_EXISTS", 270 ``!w. IS_FINITE w = ?p. w = FINITE p``, 271 272 Cases_on `w` THEN 273 REWRITE_TAC[IS_FINITE_def] THEN 274 METIS_TAC[path_distinct]); 275 276 277val REST_REPLICATE = 278 store_thm 279 ("REST_REPLICATE", 280 281 ``!n e. n > 0 ==> ((REST (REPLICATE n e)) = (REPLICATE (PRE n) e))``, 282 283 Induct_on `n` THENL [ 284 SIMP_TAC arith_ss [], 285 SIMP_TAC list_ss [REPLICATE, FinitePSLPathTheory.REST_def] 286 ]); 287 288 289val RESTN_REPLICATE = 290 store_thm 291 ("RESTN_REPLICATE", 292 ``!m n e. m <= n ==> ((RESTN (REPLICATE n e)) m = (REPLICATE (n-m) e))``, 293 294 Induct_on `m` THENL [ 295 SIMP_TAC arith_ss [FinitePSLPathTheory.RESTN_def], 296 297 ASM_SIMP_TAC arith_ss [FinitePSLPathTheory.RESTN_def, RESTN_REST] THEN 298 REPEAT STRIP_TAC THEN 299 `n - m > 0` by DECIDE_TAC THEN 300 `PRE (n - m) = (n - SUC m)` by DECIDE_TAC THEN 301 ASM_SIMP_TAC std_ss [REST_REPLICATE] 302 ]); 303 304 305val FIRSTN_REPLICATE = 306 store_thm 307 ("FIRSTN_REPLICATE", 308 ``!m n e. m <= n ==> ((FIRSTN m (REPLICATE n e)) = (REPLICATE m e))``, 309 310 Induct_on `m` THENL [ 311 SIMP_TAC list_ss [FIRSTN, REPLICATE], 312 313 REPEAT STRIP_TAC THEN 314 `~(n = 0)` by DECIDE_TAC THEN 315 `?n'. n = SUC n'` by PROVE_TAC[num_CASES] THEN 316 ASM_SIMP_TAC list_ss [FIRSTN, REPLICATE] 317 ]); 318 319 320val ELEM_REPLICATE = 321 store_thm 322 ("ELEM_REPLICATE", 323 ``!m n e. m < n ==> ((ELEM (REPLICATE n e)) m = e)``, 324 325 SIMP_TAC list_ss [FinitePSLPathTheory.ELEM_def, RESTN_REPLICATE] THEN 326 REPEAT STRIP_TAC THEN 327 `~(n - m = 0)` by DECIDE_TAC THEN 328 `?n':num. (n - m) = SUC n'` by PROVE_TAC[num_CASES] THEN 329 ASM_SIMP_TAC list_ss [REPLICATE, FinitePSLPathTheory.HEAD_def] 330); 331 332 333val REPLICATE_CONCAT = 334 store_thm 335 ("REPLICATE_CONCAT", 336 ``!n e v1 v2. (REPLICATE n e = (v1 <> v2)) = (?n1 n2. (v1 = REPLICATE n1 e) /\ (v2 = REPLICATE n2 e) /\ (n = n1 + n2))``, 337 338 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 339 EXISTS_TAC ``LENGTH (v1:'a list)`` THEN 340 EXISTS_TAC ``LENGTH (v2:'a list)`` THEN 341 `LENGTH (v1 <> v2) = LENGTH (REPLICATE n e)` by PROVE_TAC[] THEN 342 FULL_SIMP_TAC list_ss [LENGTH_REPLICATE] THEN 343 REPEAT STRIP_TAC THENL [ 344 `?m. LENGTH v1 = m` by PROVE_TAC[] THEN 345 `FIRSTN m (REPLICATE n e) = FIRSTN m (v1 <> v2)` by PROVE_TAC[] THEN 346 `m <= LENGTH v1 /\ m <= n` by DECIDE_TAC THEN 347 FULL_SIMP_TAC list_ss [FIRSTN_REPLICATE] THEN 348 ASM_SIMP_TAC std_ss [FIRSTN_APPEND1] THEN 349 PROVE_TAC[FIRSTN_LENGTH_ID], 350 351 `RESTN (REPLICATE n e) (LENGTH v1) = RESTN (v1 <> v2) (LENGTH v1)` by PROVE_TAC[] THEN 352 `(LENGTH v1 <= n) /\ (n - LENGTH v1 = (LENGTH v2))` by DECIDE_TAC THEN 353 FULL_SIMP_TAC list_ss [RESTN_REPLICATE, RESTN_APPEND] 354 ], 355 356 ASM_REWRITE_TAC[] THEN 357 REPEAT (WEAKEN_TAC (fn t => true)) THEN 358 SPEC_TAC (``n1:num``,``n1:num``) THEN 359 SPEC_TAC (``n2:num``,``n2:num``) THEN 360 Induct_on `n1` THENL [ 361 SIMP_TAC list_ss [REPLICATE], 362 ASM_SIMP_TAC list_ss [GSYM ADD_SUC, REPLICATE] 363 ] 364 ]); 365 366val REPLICATE_11 = 367 store_thm 368 ("REPLICATE_11", 369 370 ``!n e n' e'. (REPLICATE n e = REPLICATE n' e') = ((n = n') /\ ((n = 0) \/ (e = e')))``, 371 372 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 373 PROVE_TAC[LENGTH_REPLICATE], 374 375 Cases_on `n = 0` THEN ASM_REWRITE_TAC[] THEN 376 `n = n'` by METIS_TAC[LENGTH_REPLICATE] THEN 377 FULL_SIMP_TAC list_ss [] THEN 378 `?n''. n' = SUC n''` by PROVE_TAC[num_CASES] THEN 379 FULL_SIMP_TAC list_ss [REPLICATE], 380 381 PROVE_TAC[REPLICATE], 382 383 ASM_REWRITE_TAC[] 384 ]); 385 386 387val REPLICATE_SING_LIST = 388 store_thm 389 ("REPLICATE_SING_LIST", 390 391 ``!n e l. ([l] = REPLICATE n e) = ((n = 1) /\ (e = l))``, 392 393 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 394 DISCH_TAC THEN 395 `LENGTH (REPLICATE n e) = LENGTH [l]` by PROVE_TAC[] THEN 396 FULL_SIMP_TAC list_ss [LENGTH_REPLICATE] THEN 397 WEAKEN_TAC (fn t => true) THEN 398 UNDISCH_TAC ``[l] = REPLICATE 1 e`` THEN 399 `1 = SUC 0` by DECIDE_TAC THEN 400 ASM_REWRITE_TAC [REPLICATE] THEN 401 SIMP_TAC list_ss [], 402 403 REPEAT STRIP_TAC THEN 404 `n = SUC 0` by DECIDE_TAC THEN 405 ASM_REWRITE_TAC [REPLICATE] 406 ]); 407 408 409val SEL_x_OMEGA___REPLICATE = 410 store_thm 411 ("SEL_x_OMEGA___REPLICATE", 412 ``!n m x. (SEL (INFINITE (\n. x)) (n,m)) = REPLICATE (m-n+1) x``, 413 414 REPEAT STRIP_TAC THEN 415 `?t:num. (m-n+1) = t` by PROVE_TAC[] THEN 416 ASM_REWRITE_TAC[SEL_def] THEN 417 WEAKEN_TAC (fn t => true) THEN 418 Induct_on `t` THENL [ 419 SIMP_TAC list_ss [SEL_REC_def, REPLICATE], 420 421 SIMP_TAC list_ss [SEL_REC_SUC, REPLICATE, ELEM_INFINITE] THEN 422 Cases_on `t` THENL [ 423 SIMP_TAC list_ss [SEL_REC_def, REPLICATE], 424 ASM_SIMP_TAC list_ss [SEL_REC_def, REST_INFINITE] 425 ] 426 ]); 427 428 429val SEL_TOP_BOTTOM_OMEGA___REPLICATE = 430 store_thm 431 ("SEL_TOP_BOTTOM_OMEGA___REPLICATE", 432 433 ``(!n m. (SEL TOP_OMEGA (n,m)) = REPLICATE (m-n+1) TOP) /\ 434 (!n m. (SEL BOTTOM_OMEGA (n,m)) = REPLICATE (m-n+1) BOTTOM)``, 435 436 REWRITE_TAC[TOP_OMEGA_def, BOTTOM_OMEGA_def, SEL_x_OMEGA___REPLICATE]); 437 438 439val CAT_SEL_x_OMEGA_x_OMEGA = 440 store_thm 441 ("CAT_SEL_x_OMEGA_x_OMEGA", 442 443 ``!m x. (CAT (SEL (INFINITE (\n. x)) (0,m),INFINITE (\n. x))) = INFINITE (\n. x)``, 444 445 REPEAT STRIP_TAC THEN 446 `IS_INFINITE (CAT (SEL (INFINITE (\n. x)) (0,m),INFINITE (\n. x)))` by PROVE_TAC[CAT_INFINITE] THEN 447 `?q. (CAT (SEL (INFINITE (\n. x)) (0,m),INFINITE (\n. x))) = INFINITE q` by PROVE_TAC[IS_INFINITE_EXISTS] THEN 448 ASM_REWRITE_TAC[path_11, FUN_EQ_THM] THEN 449 ONCE_REWRITE_TAC[GSYM ELEM_INFINITE] THEN 450 GEN_TAC THEN 451 Cases_on `x' > m` THENL [ 452 `ELEM (INFINITE q) x' = ELEM (INFINITE (\n. x)) (x' - SUC m)` by PROVE_TAC[ELEM_CAT_SEL___GREATER] THEN 453 ASM_SIMP_TAC std_ss [ELEM_INFINITE], 454 455 `x' <= m` by DECIDE_TAC THEN 456 `ELEM (INFINITE q) x' = ELEM (INFINITE (\n. x)) x'` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 457 ASM_SIMP_TAC std_ss [ELEM_INFINITE] 458 ]); 459 460 461val SEL_NOT_EMPTY_LIST = 462 store_thm 463 ("SEL_NOT_EMPTY_LIST", 464 ``!v m n. ~(SEL v (n, m) = [])``, 465 466 REPEAT GEN_TAC THEN 467 REWRITE_TAC[SEL_def] THEN 468 `(m - n) + 1 = SUC (m - n)` by DECIDE_TAC THEN 469 ASM_REWRITE_TAC[SEL_REC_SUC] THEN 470 SIMP_TAC list_ss []); 471 472 473val TOP_ITER___EQ___REPLICATE_TOP = 474 store_thm 475 ("TOP_ITER___EQ___REPLICATE_TOP", 476 ``!n. TOP_ITER n = REPLICATE n TOP``, 477 478 Induct_on `n` THENL [ 479 REWRITE_TAC[TOP_ITER_def, REPLICATE], 480 ASM_SIMP_TAC list_ss [TOP_ITER_def, REPLICATE] 481 ]); 482 483 484val IS_INFINITE_COMPLEMENT = 485 store_thm 486 ("IS_INFINITE_COMPLEMENT", 487 ``!v. IS_INFINITE v ==> IS_INFINITE (COMPLEMENT v)``, 488 489 490 Cases_on `v` THEN REWRITE_TAC [IS_INFINITE_def] THEN 491 REWRITE_TAC[COMPLEMENT_def, IS_INFINITE_def] 492); 493 494 495val IS_FINITE_COMPLEMENT = 496 store_thm 497 ("IS_FINITE_COMPLEMENT", 498 ``!v. IS_FINITE v ==> IS_FINITE (COMPLEMENT v)``, 499 500 501 Cases_on `v` THEN REWRITE_TAC [IS_FINITE_def] THEN 502 REWRITE_TAC[COMPLEMENT_def, IS_FINITE_def] 503); 504 505 506val IN_LESSX_REWRITE = 507 store_thm 508 ("IN_LESSX_REWRITE", 509 ``!(m:num) (x:xnum). (m IN LESS x) = (m < x)``, 510 511 Cases_on `x` THEN 512 REWRITE_TAC[IN_LESSX, LS]); 513 514 515val LENGTH_RESTN_LE = 516 store_thm 517 ("LENGTH_RESTN_LE", 518 ``!n p. IS_FINITE p /\ n <= LENGTH p 519 ==> (LENGTH(RESTN p n) = LENGTH p - n)``, 520 521 Induct_on `n` THENL [ 522 REWRITE_TAC [RESTN_def] THEN 523 Cases_on `LENGTH p` THEN SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, xnum_11], 524 525 REWRITE_TAC [RESTN_def] THEN 526 REPEAT STRIP_TAC THEN 527 `IS_FINITE (REST p)` by PROVE_TAC[IS_FINITE_REST] THEN 528 `n <= LENGTH (REST p)` by (Cases_on `p` THEN 529 FULL_SIMP_TAC arith_ss [REST_def, LENGTH_def, LE_num_xnum_def, LENGTH_TL]) THEN 530 `LENGTH (RESTN (REST p) n) = LENGTH (REST p) - n` by PROVE_TAC[] THEN 531 ASM_REWRITE_TAC[] THEN 532 Cases_on `p` THEN 533 FULL_SIMP_TAC arith_ss [REST_def, LENGTH_def, LE_num_xnum_def, LENGTH_TL, 534 xnum_11, SUB_xnum_num_def] 535 ]); 536 537 538val LENGTH_RESTN_THM_LE = 539 store_thm 540 ("LENGTH_RESTN_THM_LE", 541 ``!n p. (n <= LENGTH p) 542 ==> (LENGTH(RESTN p n) = LENGTH p - n)``, 543 544 Cases_on `p` THENL [ 545 METIS_TAC[LENGTH_RESTN_LE, IS_FINITE_def], 546 SIMP_TAC arith_ss [LENGTH_def, RESTN_INFINITE, SUB_xnum_num_def] 547 ]); 548 549 550val FINITE_INFINITE_PROPER_PATH_DISTINCT = 551 store_thm 552 ("FINITE_INFINITE_PROPER_PATH_DISTINCT", 553 ``!v. ~(IS_INFINITE_PROPER_PATH v /\ IS_FINITE_PROPER_PATH v)``, 554 555 SIMP_TAC std_ss [IS_INFINITE_PROPER_PATH_def, IS_FINITE_PROPER_PATH_def] THEN 556 Cases_on `v` THEN 557 SIMP_TAC std_ss [path_distinct]); 558 559 560val COMPLEMENT_CONS = 561 store_thm 562 ("COMPLEMENT_CONS", 563 ``!h v. COMPLEMENT (CONS (h, v)) = CONS (COMPLEMENT_LETTER h, COMPLEMENT v)``, 564 565 Cases_on `v` THENL [ 566 REWRITE_TAC[PSLPathTheory.CONS_def, COMPLEMENT_def, GSYM MAP], 567 568 SIMP_TAC std_ss [PSLPathTheory.CONS_def, COMPLEMENT_def, FUN_EQ_THM, path_11] THEN 569 PROVE_TAC[] 570 ]); 571 572 573val COMPLEMENT_CAT = 574 store_thm 575 ("COMPLEMENT_CAT", 576 ``!p v. COMPLEMENT (CAT (p, v)) = CAT (MAP COMPLEMENT_LETTER p, COMPLEMENT v)``, 577 578 Induct_on `p` THENL [ 579 REWRITE_TAC [CAT_def, MAP], 580 REWRITE_TAC [CAT_def, MAP, COMPLEMENT_CONS] THEN PROVE_TAC[] 581 ]); 582 583 584 585 586val TOP_BOTTOM_OMEGA___COMPLEMENT = 587 store_thm 588 ("TOP_BOTTOM_OMEGA___COMPLEMENT", 589 ``(COMPLEMENT TOP_OMEGA = BOTTOM_OMEGA) /\ 590 (COMPLEMENT BOTTOM_OMEGA = TOP_OMEGA)``, 591 592 SIMP_TAC std_ss [COMPLEMENT_def, TOP_OMEGA_def, 593 BOTTOM_OMEGA_def, path_11, o_DEF, COMPLEMENT_LETTER_def]); 594 595 596val SEL_REC_CAT___LESS_EQ = 597 store_thm 598 ("SEL_REC_CAT___LESS_EQ", 599 ``!v p n m. (n + m <= LENGTH p) ==> (SEL_REC m n (CAT (p, v)) = SEL_REC m n (FINITE p))``, 600 601 Induct_on `m` THENL [ 602 SIMP_TAC arith_ss [SEL_REC_def], 603 604 SIMP_TAC list_ss [SEL_REC_SUC] THEN 605 REPEAT STRIP_TAC THENL [ 606 `n < LENGTH p` by DECIDE_TAC THEN 607 ASM_SIMP_TAC std_ss [ELEM_CAT___LESS, ELEM_FINITE], 608 609 `SUC n + m <= LENGTH p` by DECIDE_TAC THEN 610 PROVE_TAC[] 611 ] 612 ]); 613 614 615val SEL_CAT___LESS = 616 store_thm 617 ("SEL_CAT___LESS", 618 ``!p v m n. (n + m < LENGTH p) ==> (SEL (CAT (p,v)) (m,n) = SEL (FINITE p) (m, n))``, 619 620 REWRITE_TAC[SEL_def] THEN 621 REPEAT STRIP_TAC THEN 622 `?n':num. n - m + 1 = n'` by PROVE_TAC[] THEN 623 ASM_REWRITE_TAC[] THEN 624 `m + n' <= LENGTH p` by DECIDE_TAC THEN 625 METIS_TAC[SEL_REC_CAT___LESS_EQ]); 626 627val PATH_EQ_ELEM_THM = 628 store_thm 629 ("PATH_EQ_ELEM_THM", 630 ``!v w. (v = w) = ((LENGTH v = LENGTH w) /\ (!j. j < LENGTH v ==> (ELEM v j = ELEM w j)))``, 631 632 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 633 ASM_REWRITE_TAC[], 634 ASM_REWRITE_TAC[], 635 636 Cases_on `v` THEN 637 Cases_on `w` THEN 638 FULL_SIMP_TAC list_ss [ELEM_FINITE, LENGTH_def, path_11, xnum_11, LS, xnum_distinct, 639 ELEM_INFINITE] THENL [ 640 641 PROVE_TAC[LIST_EQ_REWRITE], 642 PROVE_TAC[FUN_EQ_THM] 643 ] 644 ]); 645 646 647 648 649 650val RESTN_CAT___LESS = 651 store_thm 652 ("RESTN_CAT___LESS", 653 ``!p v l. (l < LENGTH p) ==> ((RESTN (CAT (p, v)) l) = CAT (RESTN p l, v))``, 654 655 Induct_on `l` THENL [ 656 SIMP_TAC std_ss [RESTN_def, FinitePSLPathTheory.RESTN_def], 657 658 Cases_on `p` THEN SIMP_TAC list_ss [] THEN 659 SIMP_TAC list_ss [RESTN_def, CAT_def, FinitePSLPathTheory.RESTN_def, 660 FinitePSLPathTheory.REST_def, REST_CONS] THEN 661 PROVE_TAC[] 662 ]); 663 664 665val RESTN_CAT___EQ = 666 store_thm 667 ("RESTN_CAT___EQ", 668 ``!p v. (RESTN (CAT (p, v)) (LENGTH p)) = v``, 669 670 Induct_on `LENGTH (p:'a list)` THENL [ 671 REPEAT STRIP_TAC THEN 672 `p = []` by (Cases_on `p` THEN FULL_SIMP_TAC list_ss []) THEN 673 ASM_REWRITE_TAC[] THEN 674 SIMP_TAC list_ss [CAT_def, RESTN_def], 675 676 Cases_on `p` THEN SIMP_TAC list_ss [] THEN 677 REPEAT STRIP_TAC THEN 678 SIMP_TAC std_ss [RESTN_def, CAT_def, REST_CONS] THEN 679 PROVE_TAC[] 680 ]); 681 682 683val RESTN_CAT___GREATER_EQ = 684 store_thm 685 ("RESTN_CAT___GREATER_EQ", 686 ``!p v l. (l >= LENGTH p) ==> ((RESTN (CAT (p, v)) l) = RESTN v (l- LENGTH p))``, 687 688 Induct_on `l:num - (LENGTH (p:'a list))` THENL [ 689 REPEAT STRIP_TAC THEN 690 `l = LENGTH p` by DECIDE_TAC THEN 691 ASM_REWRITE_TAC[] THEN 692 SIMP_TAC arith_ss [RESTN_CAT___EQ, RESTN_def], 693 694 REPEAT STRIP_TAC THEN 695 `~(l = 0)` by DECIDE_TAC THEN 696 `?l'. l = SUC l'` by PROVE_TAC[num_CASES] THEN 697 ASM_SIMP_TAC std_ss [RESTN_def, RESTN_REST] THEN 698 `(l' >= LENGTH p) /\ (v = l' - LENGTH p) /\ (SUC l' - LENGTH p = l' - LENGTH p + 1)` by DECIDE_TAC THEN 699 `RESTN (CAT (p,v')) l' = RESTN v' (l' - LENGTH p)` by PROVE_TAC[] THEN 700 ASM_REWRITE_TAC[] THEN 701 REWRITE_TAC[RESTN_RESTN, REST_RESTN] 702 ]); 703 704 705val SEG_EL = 706 store_thm 707 ("SEG_EL", 708 ``!n' n m l. (n + m <= LENGTH l /\ n' < n) ==> (EL n' (SEG n m l) = EL (n'+m) l)``, 709 710 SIMP_TAC list_ss [EL_SEG, LENGTH_SEG, SEG_SEG]); 711 712 713val SEG_SUC = 714 store_thm 715 ("SEG_SUC", 716 ``!n m l. (LENGTH l > m) ==> (SEG (SUC n) m l = (EL m l)::SEG n (SUC m) l)``, 717 718 Induct_on `m` THENL [ 719 Cases_on `l` THEN 720 SIMP_TAC list_ss [SEG] THEN 721 `1 = SUC 0` by DECIDE_TAC THEN 722 Cases_on `n` THEN 723 ASM_REWRITE_TAC[SEG], 724 725 Cases_on `l` THEN 726 SIMP_TAC list_ss [SEG] THEN 727 REPEAT STRIP_TAC THEN 728 `LENGTH t > m` by DECIDE_TAC THEN 729 RES_TAC THEN 730 ASM_SIMP_TAC list_ss [] THEN 731 Cases_on `n` THEN 732 ASM_REWRITE_TAC[SEG] 733 ]); 734 735 736val SEG_SING_LIST = 737 store_thm 738 ("SEG_SING_LIST", 739 ``!n m l. ((m < LENGTH l) /\ (n > 0)) ==> ([HD (SEG n m l)] = SEG 1 m l)``, 740 741 Induct_on `m` THENL [ 742 Cases_on `l` THEN Cases_on `n` THEN 743 ASM_SIMP_TAC list_ss [SEG] THEN 744 `1 = SUC 0` by DECIDE_TAC THEN 745 PROVE_TAC [SEG], 746 747 Cases_on `l` THEN Cases_on `n` THEN 748 ASM_SIMP_TAC list_ss [SEG] THEN 749 `1 = SUC 0` by DECIDE_TAC THEN 750 ONCE_ASM_REWRITE_TAC[] THEN 751 REWRITE_TAC[SEG] 752 ]); 753 754 755val SEG_SPLIT = 756 store_thm 757 ("SEG_SPLIT", 758 ``!n1 n2 m l. (n1+n2+m <= LENGTH l) ==> (SEG (n1+n2) m l = (SEG n1 m l ++ SEG n2 (n1+m) l))``, 759 760 Induct_on `n1` THEN 761 SIMP_TAC list_ss [SEG] THEN 762 REPEAT STRIP_TAC THEN 763 `n1 + (SUC n2) + m <= LENGTH l` by DECIDE_TAC THEN 764 RES_TAC THEN 765 `n2 + SUC n1 = n1 + SUC n2` by DECIDE_TAC THEN 766 ASM_REWRITE_TAC[] THEN 767 `(n1 + 1 + m <= LENGTH l) /\ (SUC n1 = n1 + 1)` by DECIDE_TAC THEN 768 RES_TAC THEN 769 ASM_REWRITE_TAC[] THEN 770 Tactical.REVERSE (SUBGOAL_THEN ``SEG (SUC n2) (n1 + m) (l:'a list) = SEG 1 (n1 + m) l ++ SEG n2 (m + (n1 + 1)) l`` ASSUME_TAC) THEN1 ( 771 ASM_REWRITE_TAC[APPEND_ASSOC] 772 ) THEN 773 774 `(LENGTH l > n1 + m) /\ 1:num > 0:num /\ (m + n1 < LENGTH l)` by DECIDE_TAC THEN 775 `SEG 1 (m + n1) l = [HD (SEG 1 (m + n1) l)]` by PROVE_TAC[SEG_SING_LIST] THEN 776 ASM_SIMP_TAC list_ss [SEG_SUC] THEN 777 ONCE_ASM_REWRITE_TAC[] THEN 778 SIMP_TAC list_ss [SUC_ONE_ADD] THEN 779 PROVE_TAC[EL_SEG]); 780 781 782 783val EL_FIRSTN = 784 store_thm 785 ("EL_FIRSTN", 786 ``!m n l. (m <= LENGTH l /\ n < m) ==> (EL n (FIRSTN m l) = EL n l)``, 787 788 Induct_on `m` THENL [ 789 SIMP_TAC arith_ss [], 790 791 REPEAT STRIP_TAC THEN 792 Cases_on `l` THEN FULL_SIMP_TAC list_ss [] THEN 793 SIMP_TAC std_ss [FIRSTN] THEN 794 Cases_on `n` THEN SIMP_TAC list_ss [] THEN 795 `n' < m` by DECIDE_TAC THEN 796 PROVE_TAC[] 797 ]); 798 799 800val LENGTH_CAT_SEL_TOP_OMEGA = 801 store_thm 802 ("LENGTH_CAT_SEL_TOP_OMEGA", 803 ``!l v. LENGTH (CAT (SEL v (0,l),TOP_OMEGA)) = INFINITY``, 804 805 REPEAT STRIP_TAC THEN 806 REWRITE_TAC[TOP_OMEGA_def, LENGTH_CAT]); 807 808 809val MEM_SEL_REC = 810 store_thm 811 ("MEM_SEL_REC", 812 ``!x m n p. MEM x (SEL_REC m n p) = 813 ?n':num. (x = ELEM p n') /\ (n' >= n) /\ (n' < n + m)``, 814 815 816 Induct_on `m` THENL [ 817 SIMP_TAC list_ss [SEL_REC_def], 818 819 Induct_on `n` THENL [ 820 ASM_SIMP_TAC list_ss [SEL_REC_def] THEN 821 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 822 EXISTS_TAC ``0:num`` THEN 823 FULL_SIMP_TAC std_ss [HEAD_ELEM], 824 825 Q_TAC EXISTS_TAC `n' + 1` THEN 826 ASM_SIMP_TAC std_ss [REST_RESTN, ELEM_RESTN, SUC_ONE_ADD], 827 828 Cases_on `n'` THENL [ 829 ASM_REWRITE_TAC[HEAD_ELEM], 830 831 DISJ2_TAC THEN 832 Q_TAC EXISTS_TAC `n` THEN 833 FULL_SIMP_TAC std_ss [REST_RESTN, ELEM_RESTN, SUC_ONE_ADD] THEN 834 PROVE_TAC[ADD_COMM] 835 ] 836 ], 837 838 ASM_SIMP_TAC std_ss [SEL_REC_def] THEN 839 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 840 Q_TAC EXISTS_TAC `n' + 1` THEN 841 ASM_SIMP_TAC arith_ss [REST_RESTN, ELEM_RESTN, SUC_ONE_ADD], 842 843 Cases_on `n'` THEN SIMP_ALL_TAC arith_ss [] THEN 844 Q_TAC EXISTS_TAC `n''` THEN 845 ASM_SIMP_TAC arith_ss [REST_RESTN, ELEM_RESTN, SUC_ONE_ADD] 846 ] 847 ] 848 ]); 849 850 851 852val MEM_SEL = 853 store_thm 854 ("MEM_SEL", 855 ``!x m n p. MEM x (SEL p (m, n)) = 856 if (n < m) then x = ELEM p m else 857 ?n':num. (x = ELEM p n') /\ (n' >= m) /\ 858 (n' <= n)``, 859 860 SIMP_TAC std_ss [SEL_def, MEM_SEL_REC] THEN 861 REPEAT STRIP_TAC THEN 862 Cases_on `n < m` THENL [ 863 `!n':num. (n' >= m /\ n' < SUC m) = (n' = m)` by DECIDE_TAC THEN 864 `m + (n - m + 1) = SUC m` by DECIDE_TAC THEN 865 ASM_SIMP_TAC std_ss [], 866 867 868 `!x:num y:num. (x < SUC y) = (x <= y)` by DECIDE_TAC THEN 869 `m + (n - m + 1) = (SUC n)` by DECIDE_TAC THEN 870 ASM_SIMP_TAC std_ss [] 871 ]); 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891val PATH_PROP_FREE_def = 892 Define 893 `PATH_PROP_FREE (p:'prop) v = !n. !s. (n < LENGTH v) ==> ((ELEM v n = STATE s) ==> ~(p IN s))`; 894 895 896 897val INSERT_PROP_def = 898 Define 899 `(INSERT_PROP (c:'prop) TOP = TOP) /\ 900 (INSERT_PROP (c:'prop) BOTTOM = BOTTOM) /\ 901 (INSERT_PROP (c:'prop) (STATE (s:'prop set)) = STATE (\x. ((s x) \/ (x = c))))`; 902 903 904val INSERT_PROP_CASES = 905 store_thm 906 ("INSERT_PROP_CASES", 907 908 ``!c l. ((INSERT_PROP c l = TOP) = (l = TOP)) /\ 909 ((INSERT_PROP c l = BOTTOM) = (l = BOTTOM))``, 910 911 Cases_on `l` THEN SIMP_TAC std_ss [INSERT_PROP_def, letter_distinct]); 912 913 914val F_SERE_FREE_def = 915 Define 916 `(F_SERE_FREE (F_STRONG_BOOL b) = T) 917 /\ 918 (F_SERE_FREE (F_WEAK_BOOL b) = T) 919 /\ 920 (F_SERE_FREE (F_NOT f) = F_SERE_FREE f) 921 /\ 922 (F_SERE_FREE (F_AND(f1,f2)) = F_SERE_FREE f1 /\ F_SERE_FREE f2) 923 /\ 924 (F_SERE_FREE (F_STRONG_SERE r) = F) 925 /\ 926 (F_SERE_FREE (F_WEAK_SERE r) = F) 927 /\ 928 (F_SERE_FREE (F_NEXT f) = F_SERE_FREE f) 929 /\ 930 (F_SERE_FREE (F_UNTIL(f1,f2)) = F_SERE_FREE f1 /\ F_SERE_FREE f2) 931 /\ 932 (F_SERE_FREE (F_ABORT (f,b)) = F_SERE_FREE f) 933 /\ 934 (F_SERE_FREE (F_SUFFIX_IMP(r,f)) = F) 935 /\ 936 (F_SERE_FREE (F_CLOCK (f,c)) = F_SERE_FREE f)`; 937 938 939val F_CLOCK_SERE_FREE_def = 940 Define 941 `F_CLOCK_SERE_FREE f = (F_CLOCK_FREE f /\ F_SERE_FREE f)`; 942 943 944 945val bexp_induct = 946 save_thm 947 ("bexp_induct", 948 Q.GEN 949 `P` 950 (MATCH_MP 951 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 952 (SIMP_RULE 953 std_ss 954 [pairTheory.FORALL_PROD, 955 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 956 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 957 (Q.SPECL 958 [`P`,`\(f1,f2). P f1 /\ P f2`] 959 (TypeBase.induction_of ``:'a bexp``))))); 960 961 962 963val LETTER_RESTRICT_def = 964 Define 965 `(LETTER_RESTRICT S TOP = TOP) /\ 966 (LETTER_RESTRICT S BOTTOM = BOTTOM) /\ 967 (LETTER_RESTRICT S (STATE s) = STATE (s INTER S))` 968 969 970val LETTER_RESTRICT_Cases = 971 store_thm 972 ("LETTER_RESTRICT_Cases", 973 ``!l s S. ((LETTER_RESTRICT S l = STATE s) = (?s'. (l = STATE s') /\ (s = s' INTER S))) /\ 974 ((LETTER_RESTRICT S l = TOP) = (l = TOP)) /\ 975 ((LETTER_RESTRICT S l = BOTTOM) = (l = BOTTOM))``, 976 Cases_on `l` THEN 977 SIMP_TAC std_ss [LETTER_RESTRICT_def, letter_distinct, letter_11] THEN 978 PROVE_TAC[]); 979 980 981val PATH_MAP_def = 982 Define 983 `(PATH_MAP f (FINITE l) = FINITE (MAP f l)) /\ 984 (PATH_MAP f (INFINITE p) = INFINITE (\n. f (p n)))`; 985 986 987val LENGTH_PATH_MAP = 988 store_thm 989 ("LENGTH_PATH_MAP", 990 ``!f p. LENGTH (PATH_MAP f p) = LENGTH p``, 991 992 Cases_on `p` THEN 993 SIMP_TAC std_ss [PATH_MAP_def, LENGTH_def, LENGTH_MAP]); 994 995 996val ELEM_PATH_MAP = 997 store_thm 998 ("ELEM_PATH_MAP", 999 ``!f p n. (LENGTH p > n) ==> 1000 ((ELEM (PATH_MAP f p) n) = (f (ELEM p n)))``, 1001 1002 Cases_on `p` THENL [ 1003 SIMP_TAC list_ss [PATH_MAP_def, LENGTH_def, ELEM_FINITE, 1004 EL_MAP, GT_xnum_num_def], 1005 1006 SIMP_TAC std_ss [PATH_MAP_def, LENGTH_def, GT, ELEM_INFINITE] 1007 ]); 1008 1009 1010val REST_PATH_MAP = 1011 store_thm 1012 ("REST_PATH_MAP", 1013 ``!f p. LENGTH p > 0 ==> ((REST (PATH_MAP f p)) = (PATH_MAP f (REST p)))``, 1014 1015 Cases_on `p` THENL [ 1016 REWRITE_TAC [REST_def, PATH_MAP_def, TL_MAP, LENGTH_def, GT] THEN 1017 REPEAT STRIP_TAC THEN 1018 SUBGOAL_TAC `~(l = [])` THEN1 ( 1019 CCONTR_TAC THEN 1020 FULL_SIMP_TAC list_ss [] 1021 ) THEN 1022 PROVE_TAC[TL_MAP], 1023 1024 SIMP_TAC std_ss [REST_def, PATH_MAP_def] 1025 ]); 1026 1027 1028val RESTN_PATH_MAP = 1029 store_thm 1030 ("RESTN_PATH_MAP", 1031 ``!f p n. LENGTH p >= n ==> (((RESTN (PATH_MAP f p) n) = (PATH_MAP f (RESTN p n))))``, 1032 1033 Cases_on `p` THENL [ 1034 SIMP_TAC std_ss [LENGTH_def, GE] THEN 1035 Induct_on `n` THENL [ 1036 REWRITE_TAC [RESTN_def], 1037 1038 ASM_SIMP_TAC list_ss [RESTN_def, REST_def, RESTN_REST] THEN 1039 REPEAT STRIP_TAC THEN 1040 SUBGOAL_TAC `LENGTH (RESTN (FINITE l) n) > 0` THEN1 ( 1041 SUBGOAL_TAC `(LENGTH (RESTN (FINITE l) n)) = (LENGTH (FINITE l) - n)` THEN1 ( 1042 MATCH_MP_TAC LENGTH_RESTN THEN 1043 ASM_SIMP_TAC arith_ss [IS_FINITE_def, LENGTH_def, LS] 1044 ) THEN 1045 ASM_SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, GT] 1046 ) THEN 1047 ASM_SIMP_TAC std_ss [REST_PATH_MAP] 1048 ], 1049 1050 SIMP_TAC std_ss [PATH_MAP_def, LENGTH_def, GE, ELEM_INFINITE, 1051 RESTN_INFINITE] 1052 ]); 1053 1054 1055 1056val SEL_REC_PATH_MAP = 1057 store_thm 1058 ("SEL_REC_PATH_MAP", 1059 ``!m n f p. LENGTH p >= m + n ==> 1060 ((SEL_REC m n (PATH_MAP f p)) = (MAP f (SEL_REC m n p)))``, 1061 1062 Induct_on `m` THENL [ 1063 SIMP_TAC list_ss [SEL_REC_def], 1064 1065 Induct_on `n` THENL [ 1066 SIMP_TAC list_ss [SEL_REC_def, SEL_REC_REST, HEAD_ELEM, 1067 ELEM_PATH_MAP] THEN 1068 REPEAT STRIP_TAC THENL [ 1069 SUBGOAL_TAC `LENGTH p > 0` THEN1 ( 1070 Cases_on `p` THENL [ 1071 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE], 1072 REWRITE_TAC[LENGTH_def, GT] 1073 ] 1074 ) THEN 1075 PROVE_TAC[ELEM_PATH_MAP], 1076 1077 Q_SPEC_NO_ASSUM 1 `1:num` THEN 1078 `m + 1 = SUC m` by DECIDE_TAC THEN 1079 FULL_SIMP_TAC std_ss [] 1080 ], 1081 1082 SIMP_TAC list_ss [SEL_REC_def] THEN 1083 REPEAT STRIP_TAC THEN 1084 SUBGOAL_TAC `(LENGTH (REST p) >= SUC m + n) /\ (LENGTH p > 0)` THEN1 ( 1085 Cases_on `p` THENL [ 1086 SUBGOAL_TAC `LENGTH (REST (FINITE l)) = LENGTH (FINITE l) - 1` THEN1 ( 1087 MATCH_MP_TAC LENGTH_REST THEN 1088 FULL_SIMP_TAC arith_ss [IS_FINITE_def, LENGTH_def, GT, LS, GE] 1089 ) THEN 1090 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, SUB_xnum_num_def, GE], 1091 1092 1093 REWRITE_TAC[LENGTH_def, GT, REST_def, GE] 1094 ] 1095 ) THEN 1096 FULL_SIMP_TAC std_ss [REST_PATH_MAP] 1097 ] 1098 ]); 1099 1100 1101val SEL_PATH_MAP = 1102 store_thm 1103 ("SEL_PATH_MAP", 1104 ``!m n f p. (LENGTH p > n /\ n >= m) ==> 1105 ((SEL (PATH_MAP f p) (m, n)) = (MAP f (SEL p (m, n))))``, 1106 1107 REWRITE_TAC[SEL_def] THEN 1108 REPEAT STRIP_TAC THEN 1109 MATCH_MP_TAC SEL_REC_PATH_MAP THEN 1110 Cases_on `p` THENL [ 1111 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE], 1112 REWRITE_TAC[LENGTH_def, GE] 1113 ]); 1114 1115val PATH_LETTER_RESTRICT_def = 1116 Define 1117 `PATH_LETTER_RESTRICT S p = PATH_MAP (LETTER_RESTRICT S) p`; 1118 1119 1120val LENGTH_PATH_LETTER_RESTRICT = 1121 store_thm 1122 ("LENGTH_PATH_LETTER_RESTRICT", 1123 ``!S p. LENGTH (PATH_LETTER_RESTRICT S p) = LENGTH p``, 1124 REWRITE_TAC[PATH_LETTER_RESTRICT_def, LENGTH_PATH_MAP]); 1125 1126 1127val ELEM_PATH_LETTER_RESTRICT = 1128 store_thm 1129 ("ELEM_PATH_LETTER_RESTRICT", 1130 ``!S p n. (LENGTH p > n) ==> 1131 ((ELEM (PATH_LETTER_RESTRICT S p) n) = (LETTER_RESTRICT S (ELEM p n)))``, 1132 REWRITE_TAC[PATH_LETTER_RESTRICT_def, ELEM_PATH_MAP]); 1133 1134 1135val RESTN_PATH_LETTER_RESTRICT = 1136 store_thm 1137 ("RESTN_PATH_LETTER_RESTRICT", 1138 ``!S p n. LENGTH p >= n ==> (((RESTN (PATH_LETTER_RESTRICT S p) n) = (PATH_LETTER_RESTRICT S (RESTN p n))))``, 1139 REWRITE_TAC[PATH_LETTER_RESTRICT_def, RESTN_PATH_MAP]); 1140 1141 1142val COMPLEMENT_PATH_LETTER_RESTRICT = 1143 store_thm 1144 ("COMPLEMENT_PATH_LETTER_RESTRICT", 1145 ``!S p. COMPLEMENT (PATH_LETTER_RESTRICT S p) = PATH_LETTER_RESTRICT S (COMPLEMENT p)``, 1146 1147 SUBGOAL_TAC `!S x. COMPLEMENT_LETTER (LETTER_RESTRICT S x) = 1148 LETTER_RESTRICT S (COMPLEMENT_LETTER x)` THEN1 ( 1149 Cases_on `x` THEN 1150 REWRITE_TAC[LETTER_RESTRICT_def, COMPLEMENT_LETTER_def] 1151 ) THEN 1152 Cases_on `p` THENL [ 1153 ASM_SIMP_TAC std_ss [PATH_LETTER_RESTRICT_def, PATH_MAP_def, COMPLEMENT_def, 1154 MAP_MAP_o, o_DEF], 1155 1156 ASM_SIMP_TAC std_ss [PATH_LETTER_RESTRICT_def, PATH_MAP_def, COMPLEMENT_def, 1157 o_DEF] 1158 ]); 1159 1160 1161val LETTER_USED_VARS_def = 1162 Define 1163 `(LETTER_USED_VARS TOP = EMPTY) /\ 1164 (LETTER_USED_VARS BOTTOM = EMPTY) /\ 1165 (LETTER_USED_VARS (STATE s) = s)`; 1166 1167val PATH_USED_VARS_def = 1168 Define 1169 `PATH_USED_VARS v = 1170 \x. (?n. LENGTH v > n /\ x IN LETTER_USED_VARS (ELEM v n))` 1171 1172val B_USED_VARS_def = 1173 Define 1174 `(B_USED_VARS (B_PROP(p:'prop)) = {p}) /\ 1175 (B_USED_VARS B_TRUE = EMPTY) /\ 1176 (B_USED_VARS B_FALSE = EMPTY) /\ 1177 (B_USED_VARS (B_NOT b) = B_USED_VARS b) /\ 1178 (B_USED_VARS (B_AND(b1,b2)) = B_USED_VARS b1 UNION B_USED_VARS b2)`; 1179 1180 1181val S_USED_VARS_def = 1182 Define 1183 `(S_USED_VARS (S_BOOL b) = B_USED_VARS b) /\ 1184 (S_USED_VARS (S_CAT(r1,r2)) = S_USED_VARS r1 UNION S_USED_VARS r2) /\ 1185 (S_USED_VARS (S_FUSION(r1,r2)) = S_USED_VARS r1 UNION S_USED_VARS r2) /\ 1186 (S_USED_VARS (S_OR(r1,r2)) = S_USED_VARS r1 UNION S_USED_VARS r2) /\ 1187 (S_USED_VARS (S_AND(r1,r2)) = S_USED_VARS r1 UNION S_USED_VARS r2) /\ 1188 (S_USED_VARS S_EMPTY = EMPTY) /\ 1189 (S_USED_VARS (S_CLOCK (r, c)) = S_USED_VARS r UNION B_USED_VARS c) /\ 1190 (S_USED_VARS (S_REPEAT r) = S_USED_VARS r)`; 1191 1192 1193val F_USED_VARS_def = 1194 Define 1195 `(F_USED_VARS (F_STRONG_BOOL b) = B_USED_VARS b) /\ 1196 (F_USED_VARS (F_WEAK_BOOL b) = B_USED_VARS b) /\ 1197 (F_USED_VARS (F_NOT f) = F_USED_VARS f) /\ 1198 (F_USED_VARS (F_AND (f,g)) = (F_USED_VARS f UNION F_USED_VARS g)) /\ 1199 (F_USED_VARS (F_NEXT f) = F_USED_VARS f) /\ 1200 (F_USED_VARS (F_UNTIL(f,g)) = (F_USED_VARS f UNION F_USED_VARS g)) /\ 1201 (F_USED_VARS (F_ABORT (f,p)) = (F_USED_VARS f UNION B_USED_VARS p)) /\ 1202 (F_USED_VARS (F_STRONG_SERE r) = S_USED_VARS r) /\ 1203 (F_USED_VARS (F_WEAK_SERE r) = S_USED_VARS r) /\ 1204 (F_USED_VARS (F_SUFFIX_IMP (r,f)) = S_USED_VARS r UNION F_USED_VARS f) /\ 1205 (F_USED_VARS (F_CLOCK (f, p)) = (F_USED_VARS f UNION B_USED_VARS p))`; 1206 1207 1208val BEXP_PROP_FREE_def = Define `BEXP_PROP_FREE c b = ~(c IN B_USED_VARS b)`; 1209val S_PROP_FREE_def = Define `S_PROP_FREE c r = ~(c IN S_USED_VARS r)`; 1210val F_PROP_FREE_def = Define `F_PROP_FREE c f = ~(c IN F_USED_VARS f)`; 1211 1212 1213val FINITE___B_USED_VARS = 1214 store_thm 1215 ("FINITE___B_USED_VARS", 1216 1217 ``!b. FINITE(B_USED_VARS b)``, 1218 1219 INDUCT_THEN bexp_induct ASSUME_TAC THEN ( 1220 ASM_SIMP_TAC std_ss [B_USED_VARS_def, FINITE_SING, FINITE_UNION, 1221 FINITE_EMPTY] 1222 )); 1223 1224 1225val FINITE___S_USED_VARS = 1226 store_thm 1227 ("FINITE___S_USED_VARS", 1228 1229 ``!r. FINITE(S_USED_VARS r)``, 1230 1231 INDUCT_THEN sere_induct ASSUME_TAC THEN ( 1232 ASM_SIMP_TAC std_ss [S_USED_VARS_def, FINITE_UNION, 1233 FINITE_EMPTY, FINITE___B_USED_VARS] 1234 )); 1235 1236 1237val FINITE___F_USED_VARS = 1238 store_thm 1239 ("FINITE___F_USED_VARS", 1240 1241 ``!f. FINITE(F_USED_VARS f)``, 1242 1243 INDUCT_THEN fl_induct ASSUME_TAC THEN ( 1244 ASM_SIMP_TAC std_ss [F_USED_VARS_def, FINITE_UNION, 1245 FINITE_EMPTY, FINITE___B_USED_VARS, FINITE___S_USED_VARS] 1246 )); 1247 1248 1249val LETTER_USED_VARS_COMPLEMENT = 1250 store_thm 1251 ("LETTER_USED_VARS_COMPLEMENT", 1252 ``!l. LETTER_USED_VARS (COMPLEMENT_LETTER l) = 1253 LETTER_USED_VARS l``, 1254 1255 Cases_on `l` THEN 1256 REWRITE_TAC[COMPLEMENT_LETTER_def, LETTER_USED_VARS_def]); 1257 1258val PATH_USED_VARS_COMPLEMENT = 1259 store_thm 1260 ("PATH_USED_VARS_COMPLEMENT", 1261 ``!v. PATH_USED_VARS (COMPLEMENT v) = PATH_USED_VARS v``, 1262 1263 SIMP_TAC std_ss [PATH_USED_VARS_def, FUN_EQ_THM, LENGTH_COMPLEMENT] THEN 1264 METIS_TAC[LETTER_USED_VARS_COMPLEMENT, GT_LS, ELEM_COMPLEMENT, 1265 LENGTH_COMPLEMENT]); 1266 1267 1268val RESTN_PATH_USED_VARS = 1269 store_thm 1270 ("RESTN_PATH_USED_VARS", 1271 ``!n p. LENGTH p > n ==> (PATH_USED_VARS (RESTN p n) SUBSET PATH_USED_VARS p)``, 1272 SIMP_TAC std_ss [PATH_USED_VARS_def, SUBSET_DEF, IN_ABS] THEN 1273 REPEAT STRIP_TAC THEN 1274 Q_TAC EXISTS_TAC `n' + n` THEN 1275 FULL_SIMP_TAC std_ss [ELEM_RESTN] THEN 1276 Cases_on `p` THENL [ 1277 `LENGTH (FINITE l) - n > n'` by 1278 METIS_TAC[IS_FINITE_def, LENGTH_RESTN, GT_LS] THEN 1279 UNDISCH_HD_TAC THEN 1280 SIMP_TAC arith_ss [LENGTH_def, GT, SUB_xnum_num_def], 1281 1282 REWRITE_TAC[LENGTH_def, GT] 1283 ]); 1284 1285 1286val PATH_USED_VARS___TOP_OMEGA = 1287 store_thm 1288 ("PATH_USED_VARS___TOP_OMEGA", 1289 ``PATH_USED_VARS TOP_OMEGA = EMPTY``, 1290 1291 SIMP_TAC std_ss [PATH_USED_VARS_def, EXTENSION, NOT_IN_EMPTY, 1292 IN_ABS, TOP_OMEGA_def, ELEM_INFINITE, LETTER_USED_VARS_def]); 1293 1294 1295val SEL_REC_PATH_USED_VARS = 1296 store_thm 1297 ("SEL_REC_PATH_USED_VARS", 1298 ``!m n p. (LENGTH p >= m + n) ==> 1299 (LIST_BIGUNION (MAP LETTER_USED_VARS (SEL_REC m n p)) SUBSET (PATH_USED_VARS p))``, 1300 1301 Induct_on `m` THENL [ 1302 SIMP_TAC list_ss [SEL_REC_def, LIST_BIGUNION_def, EMPTY_SUBSET], 1303 1304 Induct_on `n` THENL [ 1305 SIMP_TAC list_ss [SEL_REC_def, SEL_REC_REST, LIST_BIGUNION_def, 1306 UNION_SUBSET] THEN 1307 REPEAT STRIP_TAC THENL [ 1308 SUBGOAL_TAC `LENGTH p > 0` THEN1 ( 1309 Cases_on `p` THENL [ 1310 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE], 1311 REWRITE_TAC[LENGTH_def, GT] 1312 ] 1313 ) THEN 1314 SIMP_TAC std_ss [HEAD_ELEM, PATH_USED_VARS_def, SUBSET_DEF, IN_ABS] THEN 1315 PROVE_TAC[], 1316 1317 Q_SPEC_NO_ASSUM 1 `1:num` THEN 1318 `m + 1 = SUC m` by DECIDE_TAC THEN 1319 FULL_SIMP_TAC std_ss [] 1320 ], 1321 1322 REPEAT STRIP_TAC THEN 1323 SUBGOAL_TAC `(LENGTH (REST p) >= SUC m + n) /\ (LENGTH p > 1)` THEN1 ( 1324 Cases_on `p` THENL [ 1325 SUBGOAL_TAC `LENGTH (REST (FINITE l)) = LENGTH (FINITE l) - 1` THEN1 ( 1326 MATCH_MP_TAC LENGTH_REST THEN 1327 FULL_SIMP_TAC arith_ss [IS_FINITE_def, LENGTH_def, GT, LS, GE] 1328 ) THEN 1329 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, SUB_xnum_num_def, GE], 1330 1331 REWRITE_TAC[LENGTH_def, GT, REST_def, GE] 1332 ] 1333 ) THEN 1334 1335 RES_TAC THEN 1336 UNDISCH_HD_TAC THEN 1337 REWRITE_TAC[SEL_REC_REST, REST_RESTN] THEN 1338 `PATH_USED_VARS (RESTN p 1) SUBSET PATH_USED_VARS p` 1339 by PROVE_TAC[RESTN_PATH_USED_VARS] THEN 1340 PROVE_TAC [SUBSET_TRANS] 1341 ] 1342 ]); 1343 1344 1345val SEL_PATH_USED_VARS = 1346 store_thm 1347 ("SEL_PATH_USED_VARS", 1348 ``!m n p. (LENGTH p > n /\ n >= m) ==> 1349 (LIST_BIGUNION (MAP LETTER_USED_VARS (SEL p (m, n))) SUBSET (PATH_USED_VARS p))``, 1350 1351 REWRITE_TAC[SEL_def] THEN 1352 REPEAT STRIP_TAC THEN 1353 MATCH_MP_TAC SEL_REC_PATH_USED_VARS THEN 1354 Cases_on `p` THENL [ 1355 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE], 1356 REWRITE_TAC[LENGTH_def, GE] 1357 ]); 1358 1359 1360 1361val CONS_PATH_USED_VARS = 1362 store_thm 1363 ("CONS_PATH_USED_VARS", 1364 ``!h p. PATH_USED_VARS (CONS (h, p)) = 1365 (LETTER_USED_VARS h) UNION PATH_USED_VARS p``, 1366 1367 Cases_on `p` THENL [ 1368 SIMP_TAC list_ss [PATH_USED_VARS_def, CONS_def, EXTENSION, IN_ABS, 1369 IN_UNION, LENGTH_def, GT] THEN 1370 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1371 Cases_on `n` THENL [ 1372 DISJ1_TAC THEN 1373 FULL_SIMP_TAC list_ss [ELEM_def, RESTN_def, HEAD_def], 1374 1375 DISJ2_TAC THEN 1376 Q_TAC EXISTS_TAC `n'` THEN 1377 FULL_SIMP_TAC list_ss [ELEM_def, RESTN_def, REST_def] 1378 ], 1379 1380 EXISTS_TAC ``0:num`` THEN 1381 FULL_SIMP_TAC list_ss [ELEM_def, RESTN_def, HEAD_def], 1382 1383 EXISTS_TAC ``SUC n`` THEN 1384 FULL_SIMP_TAC list_ss [ELEM_def, RESTN_def, REST_def] 1385 ], 1386 1387 1388 SIMP_TAC std_ss [CONS_def, PATH_USED_VARS_def, LENGTH_def, GT, 1389 EXTENSION, IN_UNION, IN_ABS, ELEM_INFINITE] THEN 1390 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1391 Cases_on `n` THENL [ 1392 FULL_SIMP_TAC std_ss [], 1393 1394 FULL_SIMP_TAC arith_ss [] THEN 1395 PROVE_TAC[] 1396 ], 1397 1398 PROVE_TAC[], 1399 1400 EXISTS_TAC ``SUC n`` THEN 1401 FULL_SIMP_TAC arith_ss [] 1402 ] 1403 ]); 1404 1405 1406val CAT_PATH_USED_VARS = 1407 store_thm 1408 ("CAT_PATH_USED_VARS", 1409 ``!l p. PATH_USED_VARS (CAT (l, p)) = 1410 (LIST_BIGUNION (MAP LETTER_USED_VARS l)) UNION PATH_USED_VARS p``, 1411 1412 Induct_on `l` THENL [ 1413 SIMP_TAC std_ss [CAT_def, MAP, LIST_BIGUNION_def, UNION_EMPTY], 1414 1415 ASM_SIMP_TAC list_ss [CAT_def, CONS_PATH_USED_VARS, EXTENSION, IN_UNION, 1416 LIST_BIGUNION_def] THEN 1417 PROVE_TAC[] 1418 ]) 1419 1420 1421val B_USED_VARS_INTER_SUBSET_THM = 1422 store_thm 1423 ("B_USED_VARS_INTER_SUBSET_THM", 1424 ``!l b S. (B_USED_VARS b) SUBSET S ==> (B_SEM l b = B_SEM (LETTER_RESTRICT S l) b)``, 1425 1426 Cases_on `l` THEN REWRITE_TAC[B_SEM_def, LETTER_RESTRICT_def] THEN 1427 INDUCT_THEN bexp_induct ASSUME_TAC THENL [ 1428 SIMP_TAC std_ss [B_USED_VARS_def, B_SEM_def, IN_INTER] THEN 1429 PROVE_TAC[SUBSET_DEF, IN_SING], 1430 1431 REWRITE_TAC[B_SEM_def], 1432 REWRITE_TAC[B_SEM_def], 1433 1434 REWRITE_TAC[B_SEM_def, B_USED_VARS_def] THEN 1435 PROVE_TAC[], 1436 1437 REWRITE_TAC[B_SEM_def, B_USED_VARS_def, UNION_SUBSET] THEN 1438 PROVE_TAC[] 1439 ]); 1440 1441 1442 1443 1444 1445 1446val S_USED_VARS_INTER_SUBSET_THM = 1447 store_thm 1448 ("S_USED_VARS_INTER_SUBSET_THM", 1449 ``!r l S. (S_CLOCK_FREE r) ==> 1450 (S_USED_VARS r) SUBSET S ==> (US_SEM l r = US_SEM (MAP (LETTER_RESTRICT S) l) r)``, 1451 1452 INDUCT_THEN sere_induct ASSUME_TAC THENL [ (* 8 subgoals *) 1453 SIMP_TAC list_ss [S_USED_VARS_def, US_SEM_def, ELEM_EL, 1454 HD_MAP] THEN 1455 REPEAT STRIP_TAC THEN 1456 BOOL_EQ_STRIP_TAC THEN 1457 SUBGOAL_TAC `~(l = [])` THEN1 ( 1458 CCONTR_TAC THEN 1459 FULL_SIMP_TAC list_ss [] 1460 ) THEN 1461 ASM_SIMP_TAC std_ss [HD_MAP] THEN 1462 PROVE_TAC[B_USED_VARS_INTER_SUBSET_THM], 1463 1464 SIMP_TAC list_ss [US_SEM_def, S_USED_VARS_def, UNION_SUBSET, 1465 MAP_EQ_APPEND, GSYM LEFT_EXISTS_AND_THM, 1466 S_CLOCK_FREE_def] THEN 1467 METIS_TAC[], 1468 1469 SIMP_TAC list_ss [US_SEM_def, S_USED_VARS_def, UNION_SUBSET, 1470 S_CLOCK_FREE_def, MAP_EQ_APPEND, GSYM LEFT_EXISTS_AND_THM, 1471 GSYM RIGHT_EXISTS_AND_THM] THEN 1472 REPEAT STRIP_TAC THEN 1473 SUBGOAL_TAC `!x l. ((LETTER_RESTRICT S x)::MAP (LETTER_RESTRICT S) l = 1474 MAP (LETTER_RESTRICT S) (x::l)) /\ 1475 1476 ((MAP (LETTER_RESTRICT S) l) <> [LETTER_RESTRICT S x] = 1477 MAP (LETTER_RESTRICT S) (l<>[x]))` THEN1 ( 1478 SIMP_TAC list_ss [] 1479 ) THEN 1480 ASM_SIMP_TAC std_ss [] THEN 1481 METIS_TAC[], 1482 1483 1484 SIMP_TAC list_ss [US_SEM_def, S_USED_VARS_def, S_CLOCK_FREE_def, UNION_SUBSET] THEN 1485 METIS_TAC[], 1486 1487 1488 SIMP_TAC list_ss [US_SEM_def, S_USED_VARS_def, S_CLOCK_FREE_def, UNION_SUBSET] THEN 1489 METIS_TAC[], 1490 1491 1492 SIMP_TAC list_ss [US_SEM_def], 1493 1494 SIMP_TAC list_ss [US_SEM_def, S_USED_VARS_def, S_CLOCK_FREE_def, 1495 MAP_EQ_CONCAT, GSYM LEFT_EXISTS_AND_THM, listTheory.EVERY_MAP] THEN 1496 REPEAT STRIP_TAC THEN 1497 EXISTS_EQ_STRIP_TAC THEN 1498 BOOL_EQ_STRIP_TAC THEN 1499 `!l. (US_SEM l r = US_SEM (MAP (LETTER_RESTRICT S) l) r)` by 1500 METIS_TAC[] THEN 1501 POP_NO_ASSUM 0 (fn thm => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [thm]))) THEN 1502 PROVE_TAC[], 1503 1504 1505 SIMP_TAC list_ss [S_CLOCK_FREE_def] 1506 ]); 1507 1508 1509 1510val F_USED_VARS_INTER_SUBSET_THM = 1511 store_thm 1512 ("F_USED_VARS_INTER_SUBSET_THM", 1513 ``!f p S. (F_CLOCK_FREE f) ==> 1514 (F_USED_VARS f) SUBSET S ==> 1515 (UF_SEM p f = UF_SEM (PATH_LETTER_RESTRICT S p) f)``, 1516 1517 INDUCT_THEN fl_induct ASSUME_TAC THENL [ (* 11 subgoals *) 1518 SIMP_TAC std_ss [UF_SEM_def, LENGTH_PATH_LETTER_RESTRICT, 1519 F_USED_VARS_def] THEN 1520 REPEAT STRIP_TAC THEN 1521 BOOL_EQ_STRIP_TAC THEN 1522 ASM_SIMP_TAC std_ss [ELEM_PATH_LETTER_RESTRICT] THEN 1523 PROVE_TAC[B_USED_VARS_INTER_SUBSET_THM], 1524 1525 1526 SIMP_TAC std_ss [UF_SEM_def, LENGTH_PATH_LETTER_RESTRICT, 1527 F_USED_VARS_def] THEN 1528 REPEAT STRIP_TAC THEN 1529 BOOL_EQ_STRIP_TAC THEN 1530 SUBGOAL_TAC `LENGTH p > 0` THEN1 ( 1531 Cases_on `LENGTH p` THENL [ 1532 REWRITE_TAC[GT], 1533 FULL_SIMP_TAC arith_ss [xnum_11, GT] 1534 ] 1535 ) THEN 1536 ASM_SIMP_TAC std_ss [ELEM_PATH_LETTER_RESTRICT] THEN 1537 PROVE_TAC[B_USED_VARS_INTER_SUBSET_THM], 1538 1539 1540 SIMP_TAC std_ss [UF_SEM_def, F_USED_VARS_def, COMPLEMENT_PATH_LETTER_RESTRICT, 1541 F_CLOCK_FREE_def] THEN 1542 PROVE_TAC[], 1543 1544 1545 SIMP_TAC std_ss [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1546 UNION_SUBSET] THEN 1547 PROVE_TAC[], 1548 1549 1550 1551 SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1552 LENGTH_PATH_LETTER_RESTRICT] THEN 1553 REPEAT STRIP_TAC THEN 1554 EXISTS_EQ_STRIP_TAC THEN 1555 BOOL_EQ_STRIP_TAC THEN 1556 SUBGOAL_TAC `LENGTH p > j /\ j >= 0` THEN1 ( 1557 SIMP_TAC std_ss [] THEN 1558 Cases_on `p` THENL [ 1559 FULL_SIMP_TAC arith_ss [LENGTH_def, IN_LESSX, GT], 1560 REWRITE_TAC[LENGTH_def, GT] 1561 ] 1562 ) THEN 1563 ASM_SIMP_TAC std_ss [PATH_LETTER_RESTRICT_def, SEL_PATH_MAP] THEN 1564 METIS_TAC[PATH_LETTER_RESTRICT_def, S_USED_VARS_INTER_SUBSET_THM], 1565 1566 1567 SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1568 LENGTH_PATH_LETTER_RESTRICT, LENGTH_CAT, TOP_OMEGA_def, IN_LESSX] THEN 1569 REPEAT STRIP_TAC THEN 1570 FORALL_EQ_STRIP_TAC THEN 1571 Cases_on `j IN LESS (LENGTH p)` THEN ASM_REWRITE_TAC[] THEN 1572 EXISTS_EQ_STRIP_TAC THEN 1573 REMAINS_TAC `(SEL (CAT (SEL (PATH_LETTER_RESTRICT S p) (0,j),INFINITE (\n. TOP))) 1574 (0,k)) = 1575 MAP (LETTER_RESTRICT S) (SEL (CAT (SEL p (0,j),INFINITE (\n. TOP))) (0,k))` THEN1 ( 1576 PROVE_TAC[S_USED_VARS_INTER_SUBSET_THM] 1577 ) THEN 1578 ONCE_REWRITE_TAC [LIST_EQ_REWRITE] THEN 1579 SIMP_TAC arith_ss [LENGTH_SEL, LENGTH_MAP, EL_MAP] THEN 1580 REPEAT STRIP_TAC THEN 1581 rename1 `n < k + 1` THEN 1582 `(0:num) + n <= k` by DECIDE_TAC THEN 1583 ASM_SIMP_TAC std_ss [EL_SEL_THM] THEN 1584 Cases_on `n > j` THENL [ 1585 ASM_SIMP_TAC std_ss [ELEM_CAT_SEL___GREATER, ELEM_INFINITE, LETTER_RESTRICT_def], 1586 1587 `n <= j` by DECIDE_TAC THEN 1588 ASM_SIMP_TAC std_ss [ELEM_CAT_SEL___LESS_EQ] THEN 1589 MATCH_MP_TAC ELEM_PATH_LETTER_RESTRICT THEN 1590 Cases_on `p` THENL [ 1591 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, IN_LESSX], 1592 REWRITE_TAC[LENGTH_def, GT] 1593 ] 1594 ], 1595 1596 1597 1598 SIMP_TAC std_ss [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1599 LENGTH_PATH_LETTER_RESTRICT] THEN 1600 REPEAT STRIP_TAC THEN 1601 BOOL_EQ_STRIP_TAC THEN 1602 SUBGOAL_TAC `LENGTH p >= 1` THEN1 ( 1603 Cases_on `p` THEN 1604 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE] 1605 ) THEN 1606 ASM_SIMP_TAC std_ss [RESTN_PATH_LETTER_RESTRICT], 1607 1608 1609 1610 SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1611 UNION_SUBSET, LENGTH_PATH_LETTER_RESTRICT, IN_LESSX_REWRITE, IN_LESS] THEN 1612 REPEAT STRIP_TAC THEN 1613 EXISTS_EQ_STRIP_TAC THEN 1614 BOOL_EQ_STRIP_TAC THEN 1615 BINOP_TAC THENL [ 1616 REMAINS_TAC `LENGTH p >= k` THEN1 ( 1617 METIS_TAC[RESTN_PATH_LETTER_RESTRICT] 1618 ) THEN 1619 Cases_on `p` THEN 1620 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE, LS], 1621 1622 FORALL_EQ_STRIP_TAC THEN 1623 Cases_on `j < k` THEN ASM_REWRITE_TAC[] THEN 1624 REMAINS_TAC `LENGTH p >= j` THEN1 ( 1625 METIS_TAC[RESTN_PATH_LETTER_RESTRICT] 1626 ) THEN 1627 Cases_on `p` THEN 1628 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE, LS] 1629 ], 1630 1631 1632 1633 SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1634 UNION_SUBSET, LENGTH_PATH_LETTER_RESTRICT, IN_LESSX_REWRITE, IN_LESS] THEN 1635 REPEAT STRIP_TAC THEN 1636 BINOP_TAC THEN1 METIS_TAC[] THEN 1637 EXISTS_EQ_STRIP_TAC THEN 1638 REPEAT BOOL_EQ_STRIP_TAC THEN 1639 BINOP_TAC THENL [ 1640 ASM_SIMP_TAC std_ss [ELEM_PATH_LETTER_RESTRICT, GT_LS] THEN 1641 PROVE_TAC[B_USED_VARS_INTER_SUBSET_THM], 1642 1643 Cases_on `j = 0` THEN ASM_REWRITE_TAC[TOP_OMEGA_def] THEN 1644 REMAINS_TAC `(CAT (SEL (PATH_LETTER_RESTRICT S p) (0,j-1),INFINITE (\n. TOP))) = 1645 PATH_LETTER_RESTRICT S (CAT (SEL p (0,j-1),INFINITE (\n. TOP)))` THEN1 ( 1646 METIS_TAC[] 1647 ) THEN 1648 ONCE_REWRITE_TAC [PATH_EQ_ELEM_THM] THEN 1649 SIMP_TAC arith_ss [LENGTH_CAT, LENGTH_PATH_LETTER_RESTRICT, LS] THEN 1650 GEN_TAC THEN 1651 `LENGTH (CAT (SEL p (0,j - 1),INFINITE (\n. TOP))) > j'` by 1652 SIMP_TAC std_ss [LENGTH_CAT, GT] THEN 1653 ASM_SIMP_TAC std_ss [ELEM_PATH_LETTER_RESTRICT] THEN 1654 Cases_on `j' > j-1` THENL [ 1655 ASM_SIMP_TAC std_ss [ELEM_CAT_SEL___GREATER, ELEM_INFINITE, LETTER_RESTRICT_def], 1656 1657 `j' <= j - 1` by DECIDE_TAC THEN 1658 ASM_SIMP_TAC std_ss [ELEM_CAT_SEL___LESS_EQ] THEN 1659 SUBGOAL_TAC `LENGTH p > j'` THEN1 ( 1660 Cases_on `p` THEN 1661 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, LS] 1662 ) THEN 1663 ASM_SIMP_TAC std_ss [ELEM_PATH_LETTER_RESTRICT] 1664 ] 1665 ], 1666 1667 1668 REWRITE_TAC[F_CLOCK_FREE_def], 1669 1670 1671 SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, F_USED_VARS_def, F_CLOCK_FREE_def, 1672 UNION_SUBSET, LENGTH_PATH_LETTER_RESTRICT, IN_LESSX_REWRITE, IN_LESS, 1673 COMPLEMENT_PATH_LETTER_RESTRICT] THEN 1674 REPEAT STRIP_TAC THEN 1675 FORALL_EQ_STRIP_TAC THEN 1676 Cases_on `j < LENGTH p` THEN ASM_REWRITE_TAC [] THEN 1677 BINOP_TAC THENL [ 1678 `LENGTH (COMPLEMENT p) > j` by PROVE_TAC[GT_LS, LENGTH_COMPLEMENT] THEN 1679 `j >= 0` by DECIDE_TAC THEN 1680 ASM_SIMP_TAC std_ss [SEL_PATH_MAP, PATH_LETTER_RESTRICT_def] THEN 1681 PROVE_TAC[S_USED_VARS_INTER_SUBSET_THM], 1682 1683 1684 SUBGOAL_TAC `LENGTH p >= j` THEN1 ( 1685 Cases_on `p` THEN 1686 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE, LS] 1687 ) THEN 1688 PROVE_TAC[RESTN_PATH_LETTER_RESTRICT] 1689 ] 1690 ]); 1691 1692 1693val LETTER_VAR_RENAMING_def = 1694 Define 1695 `(LETTER_VAR_RENAMING (f:'a->'b) TOP = TOP) /\ 1696 (LETTER_VAR_RENAMING f BOTTOM = BOTTOM) /\ 1697 (LETTER_VAR_RENAMING f (STATE s) = STATE (IMAGE f s))`; 1698 1699val PATH_VAR_RENAMING_def = 1700 Define 1701 `PATH_VAR_RENAMING f p = PATH_MAP (LETTER_VAR_RENAMING f) p`; 1702 1703 1704val LENGTH_PATH_VAR_RENAMING = 1705 store_thm 1706 ("LENGTH_PATH_VAR_RENAMING", 1707 ``!f p. LENGTH (PATH_VAR_RENAMING f p) = LENGTH p``, 1708 REWRITE_TAC[PATH_VAR_RENAMING_def, LENGTH_PATH_MAP]); 1709 1710val SEL_PATH_VAR_RENAMING = 1711 store_thm 1712 ("SEL_PATH_VAR_RENAMING", 1713 ``!m n f p. (LENGTH p > n /\ n >= m) ==> 1714 ((SEL (PATH_VAR_RENAMING f p) (m, n)) = (MAP (LETTER_VAR_RENAMING f) (SEL p (m, n))))``, 1715 1716 REWRITE_TAC[PATH_VAR_RENAMING_def, SEL_PATH_MAP]); 1717 1718 1719val ELEM_PATH_VAR_RENAMING = 1720 store_thm 1721 ("ELEM_PATH_VAR_RENAMING", 1722 ``!f p n. (LENGTH p > n) ==> 1723 ((ELEM (PATH_VAR_RENAMING f p) n) = (LETTER_VAR_RENAMING f (ELEM p n)))``, 1724 REWRITE_TAC[PATH_VAR_RENAMING_def, ELEM_PATH_MAP]); 1725 1726 1727val RESTN_PATH_VAR_RENAMING = 1728 store_thm 1729 ("RESTN_PATH_VAR_RENAMING", 1730 ``!f p n. LENGTH p >= n ==> (((RESTN (PATH_VAR_RENAMING f p) n) = (PATH_VAR_RENAMING f (RESTN p n))))``, 1731 REWRITE_TAC[PATH_VAR_RENAMING_def, RESTN_PATH_MAP]); 1732 1733 1734val COMPLEMENT_PATH_VAR_RENAMING = 1735 store_thm 1736 ("COMPLEMENT_PATH_VAR_RENAMING", 1737 ``!f p. COMPLEMENT (PATH_VAR_RENAMING f p) = PATH_VAR_RENAMING f (COMPLEMENT p)``, 1738 1739 SUBGOAL_TAC `!f x. COMPLEMENT_LETTER (LETTER_VAR_RENAMING f x) = 1740 LETTER_VAR_RENAMING f (COMPLEMENT_LETTER x)` THEN1 ( 1741 Cases_on `x` THEN 1742 REWRITE_TAC[LETTER_VAR_RENAMING_def, COMPLEMENT_LETTER_def] 1743 ) THEN 1744 Cases_on `p` THENL [ 1745 ASM_SIMP_TAC std_ss [PATH_VAR_RENAMING_def, PATH_MAP_def, COMPLEMENT_def, 1746 MAP_MAP_o, o_DEF], 1747 1748 ASM_SIMP_TAC std_ss [PATH_VAR_RENAMING_def, PATH_MAP_def, COMPLEMENT_def, 1749 o_DEF] 1750 ]); 1751 1752 1753val PATH_VAR_RENAMING___CONS = 1754 store_thm 1755 ("PATH_VAR_RENAMING___CONS", 1756 1757 ``!l v f. 1758 PATH_VAR_RENAMING f (CONS (l, v)) = 1759 CONS (LETTER_VAR_RENAMING f l, PATH_VAR_RENAMING f v)``, 1760 1761 Cases_on `v` THENL [ 1762 SIMP_TAC std_ss [CONS_def, PATH_VAR_RENAMING_def, PATH_MAP_def, MAP], 1763 SIMP_TAC std_ss [CONS_def, PATH_VAR_RENAMING_def, PATH_MAP_def, COND_RAND] 1764 ]); 1765 1766 1767val PATH_VAR_RENAMING___CAT = 1768 store_thm 1769 ("PATH_VAR_RENAMING___CAT", 1770 ``!f l p. 1771 PATH_VAR_RENAMING f (CAT(l, p)) = 1772 CAT (MAP (LETTER_VAR_RENAMING f) l, PATH_VAR_RENAMING f p)``, 1773 1774 Induct_on `l` THENL [ 1775 SIMP_TAC std_ss [CAT_def, MAP], 1776 ASM_SIMP_TAC std_ss [CAT_def, PATH_VAR_RENAMING___CONS, MAP] 1777 ]); 1778 1779 1780val PATH_VAR_RENAMING___TOP_OMEGA = 1781 store_thm 1782 ("PATH_VAR_RENAMING___TOP_OMEGA", 1783 1784 ``!f. PATH_VAR_RENAMING f TOP_OMEGA = TOP_OMEGA``, 1785 REWRITE_TAC[PATH_VAR_RENAMING_def, TOP_OMEGA_def, PATH_MAP_def, LETTER_VAR_RENAMING_def]); 1786 1787 1788val PATH_VAR_RENAMING___BOTTOM_OMEGA = 1789 store_thm 1790 ("PATH_VAR_RENAMING___BOTTOM_OMEGA", 1791 1792 ``!f. PATH_VAR_RENAMING f BOTTOM_OMEGA = BOTTOM_OMEGA``, 1793 REWRITE_TAC[PATH_VAR_RENAMING_def, BOTTOM_OMEGA_def, PATH_MAP_def, LETTER_VAR_RENAMING_def]); 1794 1795 1796val B_VAR_RENAMING_def = 1797 Define 1798 `(B_VAR_RENAMING (f:'a->'b) (B_TRUE) = B_TRUE) /\ 1799 (B_VAR_RENAMING f (B_FALSE) = B_FALSE) /\ 1800 (B_VAR_RENAMING f (B_PROP p) = (B_PROP (f p))) /\ 1801 (B_VAR_RENAMING f (B_NOT b) = B_NOT (B_VAR_RENAMING f b)) /\ 1802 (B_VAR_RENAMING f (B_AND(b1,b2)) = (B_AND(B_VAR_RENAMING f b1, B_VAR_RENAMING f b2)))`; 1803 1804 1805val S_VAR_RENAMING_def = 1806 Define 1807 `(S_VAR_RENAMING f (S_BOOL b) = S_BOOL (B_VAR_RENAMING f b)) /\ 1808 (S_VAR_RENAMING f (S_CAT(r1,r2)) = S_CAT(S_VAR_RENAMING f r1, S_VAR_RENAMING f r2)) /\ 1809 (S_VAR_RENAMING f (S_FUSION(r1,r2)) = S_FUSION(S_VAR_RENAMING f r1, S_VAR_RENAMING f r2)) /\ 1810 (S_VAR_RENAMING f (S_OR(r1,r2)) = S_OR(S_VAR_RENAMING f r1, S_VAR_RENAMING f r2)) /\ 1811 (S_VAR_RENAMING f (S_AND(r1,r2)) = S_AND(S_VAR_RENAMING f r1, S_VAR_RENAMING f r2)) /\ 1812 (S_VAR_RENAMING f S_EMPTY = S_EMPTY) /\ 1813 (S_VAR_RENAMING f (S_CLOCK (r, c)) = S_CLOCK (S_VAR_RENAMING f r, B_VAR_RENAMING f c)) /\ 1814 (S_VAR_RENAMING f (S_REPEAT r) = S_REPEAT (S_VAR_RENAMING f r))`; 1815 1816 1817val F_VAR_RENAMING_def = 1818 Define 1819 `(F_VAR_RENAMING f' (F_STRONG_BOOL b) = F_STRONG_BOOL (B_VAR_RENAMING f' b)) /\ 1820 (F_VAR_RENAMING f' (F_WEAK_BOOL b) = F_WEAK_BOOL (B_VAR_RENAMING f' b)) /\ 1821 (F_VAR_RENAMING f' (F_NOT f) = F_NOT (F_VAR_RENAMING f' f)) /\ 1822 (F_VAR_RENAMING f' (F_AND (f,g)) = F_AND(F_VAR_RENAMING f' f, F_VAR_RENAMING f' g)) /\ 1823 (F_VAR_RENAMING f' (F_NEXT f) = F_NEXT(F_VAR_RENAMING f' f)) /\ 1824 (F_VAR_RENAMING f' (F_UNTIL(f,g)) = F_UNTIL(F_VAR_RENAMING f' f, F_VAR_RENAMING f' g)) /\ 1825 (F_VAR_RENAMING f' (F_ABORT (f,p)) = F_ABORT(F_VAR_RENAMING f' f, B_VAR_RENAMING f' p)) /\ 1826 (F_VAR_RENAMING f' (F_STRONG_SERE r) = F_STRONG_SERE (S_VAR_RENAMING f' r)) /\ 1827 (F_VAR_RENAMING f' (F_WEAK_SERE r) = F_WEAK_SERE (S_VAR_RENAMING f' r)) /\ 1828 (F_VAR_RENAMING f' (F_SUFFIX_IMP (r,f)) = F_SUFFIX_IMP(S_VAR_RENAMING f' r, F_VAR_RENAMING f' f)) /\ 1829 (F_VAR_RENAMING f' (F_CLOCK (f, p)) = F_CLOCK(F_VAR_RENAMING f' f, B_VAR_RENAMING f' p))`; 1830 1831 1832val B_SEM___VAR_RENAMING = 1833 store_thm 1834 ("B_SEM___VAR_RENAMING", 1835 ``!p l f. (INJ f (LETTER_USED_VARS l UNION B_USED_VARS p) UNIV) ==> ((B_SEM l p) = (B_SEM (LETTER_VAR_RENAMING f l) (B_VAR_RENAMING f p)))``, 1836 1837 Cases_on `l` THEN ( 1838 REWRITE_TAC[B_SEM_def, LETTER_VAR_RENAMING_def] 1839 ) THEN 1840 INDUCT_THEN bexp_induct ASSUME_TAC THENL [ 1841 SIMP_TAC std_ss [B_SEM_def, B_VAR_RENAMING_def, IN_IMAGE, 1842 INJ_DEF, IN_UNIV, LETTER_USED_VARS_def, IN_UNION, 1843 B_USED_VARS_def, IN_SING] THEN 1844 PROVE_TAC[], 1845 1846 REWRITE_TAC[B_SEM_def, B_VAR_RENAMING_def], 1847 REWRITE_TAC[B_SEM_def, B_VAR_RENAMING_def], 1848 ASM_SIMP_TAC std_ss [B_SEM_def, B_VAR_RENAMING_def, B_USED_VARS_def], 1849 1850 ASM_SIMP_TAC std_ss [B_SEM_def, B_VAR_RENAMING_def, B_USED_VARS_def] THEN 1851 REPEAT STRIP_TAC THEN 1852 REMAINS_TAC `INJ f' (LETTER_USED_VARS (STATE f) UNION B_USED_VARS p) UNIV /\ 1853 INJ f' (LETTER_USED_VARS (STATE f) UNION B_USED_VARS p') UNIV` THEN1 ( 1854 PROVE_TAC[] 1855 ) THEN 1856 UNDISCH_HD_TAC THEN 1857 SIMP_TAC std_ss [INJ_DEF, IN_UNION, IN_UNIV] THEN 1858 PROVE_TAC[] 1859 ]); 1860 1861 1862 1863val US_SEM___VAR_RENAMING = 1864 store_thm 1865 ("US_SEM___VAR_RENAMING", 1866 ``!r l f. ((S_CLOCK_FREE r) /\ 1867 (INJ f ((LIST_BIGUNION (MAP LETTER_USED_VARS l)) UNION S_USED_VARS r) UNIV)) ==> 1868 (US_SEM l r = US_SEM ((MAP (LETTER_VAR_RENAMING f)) l) (S_VAR_RENAMING f r))``, 1869 1870INDUCT_THEN sere_induct ASSUME_TAC THENL [ (* 8 subgoals *) 1871 Cases_on `l` THEN 1872 SIMP_TAC list_ss [US_SEM_def, S_VAR_RENAMING_def, 1873 S_USED_VARS_def, 1874 LENGTH_NIL, FinitePSLPathTheory.ELEM_def, FinitePSLPathTheory.RESTN_def, 1875 FinitePSLPathTheory.HEAD_def, LIST_BIGUNION_def] THEN 1876 REPEAT STRIP_TAC THEN 1877 BOOL_EQ_STRIP_TAC THEN 1878 MATCH_MP_TAC B_SEM___VAR_RENAMING THEN 1879 UNDISCH_NO_TAC 1 THEN 1880 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 1881 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1882 PROVE_TAC[], 1883 1884 1885 SIMP_TAC std_ss [US_SEM_def, S_USED_VARS_def, S_VAR_RENAMING_def, 1886 MAP_EQ_APPEND, GSYM LEFT_EXISTS_AND_THM, S_CLOCK_FREE_def] THEN 1887 REPEAT STRIP_TAC THEN 1888 REPEAT EXISTS_EQ_STRIP_TAC THEN 1889 BOOL_EQ_STRIP_TAC THEN 1890 REMAINS_TAC `INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS v1) UNION S_USED_VARS r) UNIV /\ 1891 INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS v2) UNION S_USED_VARS r') UNIV` THEN1 ( 1892 PROVE_TAC[] 1893 ) THEN 1894 STRIP_TAC THEN 1895 UNDISCH_NO_TAC 1 THEN 1896 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 1897 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, MAP_APPEND, 1898 LIST_BIGUNION_APPEND] THEN 1899 PROVE_TAC[], 1900 1901 1902 SIMP_TAC std_ss [US_SEM_def, S_USED_VARS_def, S_VAR_RENAMING_def, 1903 MAP_EQ_APPEND, GSYM LEFT_EXISTS_AND_THM, 1904 GSYM RIGHT_EXISTS_AND_THM, S_CLOCK_FREE_def, MAP_EQ_SING] THEN 1905 1906 (*Reorder Variables for later EXISTS_EQ_STRIP_TAC*) 1907 REPEAT STRIP_TAC THEN 1908 `(?v1 v2 l'. (l = v1 <> [l'] <> v2) /\ US_SEM (v1 <> [l']) r /\ US_SEM ([l'] <> v2) r') = 1909 (?v2 v1 l'. (l = v1 <> [l'] <> v2) /\ US_SEM (v1 <> [l']) r /\ US_SEM ([l'] <> v2) r')` by PROVE_TAC[] THEN 1910 ONCE_ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1911 1912 REPEAT EXISTS_EQ_STRIP_TAC THEN 1913 BOOL_EQ_STRIP_TAC THEN 1914 SUBGOAL_TAC `(MAP (LETTER_VAR_RENAMING f) v1 <> [LETTER_VAR_RENAMING f l'] = 1915 MAP (LETTER_VAR_RENAMING f) (v1 <> [l'])) /\ 1916 ([LETTER_VAR_RENAMING f l'] <> MAP (LETTER_VAR_RENAMING f) v2 = 1917 MAP (LETTER_VAR_RENAMING f) ([l'] <> v2))` THEN1 ( 1918 SIMP_TAC std_ss [MAP_APPEND, MAP] 1919 ) THEN 1920 ASM_REWRITE_TAC[] THEN NTAC 2 WEAKEN_HD_TAC THEN 1921 REMAINS_TAC `INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS (v1<>[l'])) UNION S_USED_VARS r) UNIV /\ 1922 INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS ([l']<>v2)) UNION S_USED_VARS r') UNIV` THEN1 ( 1923 PROVE_TAC[] 1924 ) THEN 1925 STRIP_TAC THEN 1926 UNDISCH_NO_TAC 1 THEN 1927 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 1928 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, MAP_APPEND, 1929 LIST_BIGUNION_APPEND, MAP] THEN 1930 PROVE_TAC[], 1931 1932 1933 1934 SIMP_TAC std_ss [US_SEM_def, S_USED_VARS_def, S_VAR_RENAMING_def, S_CLOCK_FREE_def] THEN 1935 REPEAT STRIP_TAC THEN 1936 REMAINS_TAC `INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS l) UNION S_USED_VARS r) UNIV /\ 1937 INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS l) UNION S_USED_VARS r') UNIV` THEN1 ( 1938 PROVE_TAC[] 1939 ) THEN 1940 STRIP_TAC THEN 1941 UNDISCH_HD_TAC THEN 1942 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 1943 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1944 PROVE_TAC[], 1945 1946 1947 1948 SIMP_TAC std_ss [US_SEM_def, S_USED_VARS_def, S_VAR_RENAMING_def, S_CLOCK_FREE_def] THEN 1949 REPEAT STRIP_TAC THEN 1950 REMAINS_TAC `INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS l) UNION S_USED_VARS r) UNIV /\ 1951 INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS l) UNION S_USED_VARS r') UNIV` THEN1 ( 1952 PROVE_TAC[] 1953 ) THEN 1954 STRIP_TAC THEN 1955 UNDISCH_HD_TAC THEN 1956 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 1957 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1958 PROVE_TAC[], 1959 1960 1961 SIMP_TAC list_ss [US_SEM_def, S_VAR_RENAMING_def], 1962 1963 1964 SIMP_TAC list_ss [US_SEM_def, S_VAR_RENAMING_def, S_USED_VARS_def, 1965 MAP_EQ_CONCAT, GSYM LEFT_EXISTS_AND_THM, listTheory.EVERY_MAP, S_CLOCK_FREE_def] THEN 1966 REPEAT STRIP_TAC THEN 1967 EXISTS_EQ_STRIP_TAC THEN 1968 BOOL_EQ_STRIP_TAC THEN 1969 FULL_SIMP_TAC std_ss [] THEN 1970 WEAKEN_HD_TAC THEN 1971 Induct_on `vlist` THENL [ 1972 SIMP_TAC list_ss [], 1973 1974 SIMP_TAC list_ss [MAP_APPEND, LIST_BIGUNION_APPEND, CONCAT_def] THEN 1975 REPEAT STRIP_TAC THEN 1976 REMAINS_TAC `INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS (CONCAT vlist)) UNION S_USED_VARS r) UNIV /\ 1977 INJ f (LIST_BIGUNION (MAP LETTER_USED_VARS h) UNION S_USED_VARS r) UNIV` THEN1 ( 1978 PROVE_TAC[] 1979 ) THEN 1980 STRIP_TAC THEN 1981 UNDISCH_HD_TAC THEN 1982 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 1983 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1984 PROVE_TAC[] 1985 ], 1986 1987 1988 REWRITE_TAC[S_CLOCK_FREE_def] 1989]); 1990 1991 1992 1993val UF_SEM___VAR_RENAMING = 1994 store_thm 1995 ("UF_SEM___VAR_RENAMING", 1996 ``!f v f'. ((F_CLOCK_FREE f) /\ 1997 (INJ f' (PATH_USED_VARS v UNION F_USED_VARS f) UNIV)) ==> 1998 (UF_SEM v f = UF_SEM (PATH_VAR_RENAMING f' v) (F_VAR_RENAMING f' f))``, 1999 2000 INDUCT_THEN fl_induct ASSUME_TAC THENL [ (* 11 subgoals *) 2001 SIMP_TAC std_ss [F_CLOCK_FREE_def, F_USED_VARS_def, 2002 F_VAR_RENAMING_def, UF_SEM_def, 2003 LENGTH_PATH_VAR_RENAMING] THEN 2004 REPEAT STRIP_TAC THEN 2005 BOOL_EQ_STRIP_TAC THEN 2006 ASM_SIMP_TAC std_ss [ELEM_PATH_VAR_RENAMING] THEN 2007 MATCH_MP_TAC B_SEM___VAR_RENAMING THEN 2008 UNDISCH_NO_TAC 1 THEN 2009 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2010 SIMP_TAC std_ss [SUBSET_DEF, PATH_USED_VARS_def, IN_ABS, 2011 IN_UNION] THEN 2012 PROVE_TAC[], 2013 2014 2015 SIMP_TAC std_ss [F_CLOCK_FREE_def, F_USED_VARS_def, 2016 F_VAR_RENAMING_def, UF_SEM_def, 2017 LENGTH_PATH_VAR_RENAMING] THEN 2018 REPEAT STRIP_TAC THEN 2019 BOOL_EQ_STRIP_TAC THEN 2020 SUBGOAL_TAC `LENGTH v > 0` THEN1 ( 2021 Cases_on `v` THEN 2022 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, xnum_11] 2023 ) THEN 2024 ASM_SIMP_TAC std_ss [ELEM_PATH_VAR_RENAMING] THEN 2025 MATCH_MP_TAC B_SEM___VAR_RENAMING THEN 2026 UNDISCH_NO_TAC 2 THEN 2027 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2028 SIMP_TAC std_ss [SUBSET_DEF, PATH_USED_VARS_def, IN_ABS, 2029 IN_UNION] THEN 2030 PROVE_TAC[], 2031 2032 2033 SIMP_TAC std_ss [F_CLOCK_FREE_def, F_USED_VARS_def, UF_SEM_def, 2034 F_VAR_RENAMING_def, COMPLEMENT_PATH_VAR_RENAMING] THEN 2035 PROVE_TAC[PATH_USED_VARS_COMPLEMENT], 2036 2037 2038 SIMP_TAC std_ss [F_CLOCK_FREE_def, F_USED_VARS_def, UF_SEM_def, 2039 F_VAR_RENAMING_def] THEN 2040 REPEAT STRIP_TAC THEN 2041 REMAINS_TAC `INJ f'' (PATH_USED_VARS v UNION F_USED_VARS f) UNIV /\ 2042 INJ f'' (PATH_USED_VARS v UNION F_USED_VARS f') UNIV` THEN1 ( 2043 PROVE_TAC[] 2044 ) THEN 2045 STRIP_TAC THEN 2046 UNDISCH_HD_TAC THEN 2047 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 2048 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2049 PROVE_TAC[], 2050 2051 2052 2053 SIMP_TAC (std_ss++resq_SS) [F_CLOCK_FREE_def, F_USED_VARS_def, UF_SEM_def, 2054 F_VAR_RENAMING_def, IN_LESSX_REWRITE, LENGTH_PATH_VAR_RENAMING] THEN 2055 REPEAT STRIP_TAC THEN 2056 EXISTS_EQ_STRIP_TAC THEN 2057 BOOL_EQ_STRIP_TAC THEN 2058 `LENGTH v > j /\ j >= 0` by FULL_SIMP_TAC std_ss [GT_LS] THEN 2059 ASM_SIMP_TAC std_ss [SEL_PATH_VAR_RENAMING] THEN 2060 MATCH_MP_TAC US_SEM___VAR_RENAMING THEN 2061 ASM_REWRITE_TAC[] THEN 2062 UNDISCH_NO_TAC 3 THEN 2063 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2064 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2065 PROVE_TAC[SEL_PATH_USED_VARS, SUBSET_DEF], 2066 2067 2068 2069 SIMP_TAC (std_ss++resq_SS) [F_CLOCK_FREE_def, F_USED_VARS_def, UF_SEM_def, 2070 F_VAR_RENAMING_def, IN_LESSX_REWRITE, LENGTH_PATH_VAR_RENAMING, 2071 LENGTH_CAT_SEL_TOP_OMEGA, LS] THEN 2072 REPEAT STRIP_TAC THEN 2073 FORALL_EQ_STRIP_TAC THEN 2074 BOOL_EQ_STRIP_TAC THEN 2075 EXISTS_EQ_STRIP_TAC THEN 2076 2077 SUBGOAL_TAC `(SEL (CAT (SEL (PATH_VAR_RENAMING f' v) (0,j),TOP_OMEGA)) (0,k)) = 2078 MAP (LETTER_VAR_RENAMING f') (SEL (CAT (SEL v (0,j),TOP_OMEGA)) (0,k))` THEN1 ( 2079 `TOP_OMEGA = PATH_VAR_RENAMING f' TOP_OMEGA` by REWRITE_TAC[PATH_VAR_RENAMING___TOP_OMEGA] THEN 2080 `LENGTH v > j /\ j >= 0` by FULL_SIMP_TAC std_ss [GT_LS] THEN 2081 `LENGTH (CAT (SEL v (0,j),TOP_OMEGA)) > k /\ k >= 0` by 2082 SIMP_TAC std_ss [LENGTH_CAT_SEL_TOP_OMEGA, GT] THEN 2083 ASM_SIMP_TAC std_ss [SEL_PATH_VAR_RENAMING, GSYM PATH_VAR_RENAMING___CAT] 2084 ) THEN 2085 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 2086 2087 MATCH_MP_TAC US_SEM___VAR_RENAMING THEN 2088 ASM_REWRITE_TAC[] THEN 2089 UNDISCH_NO_TAC 1 THEN 2090 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2091 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2092 REPEAT STRIP_TAC THENL [ 2093 ALL_TAC, 2094 ASM_REWRITE_TAC[] 2095 ] THEN 2096 DISJ1_TAC THEN 2097 UNDISCH_HD_TAC THEN 2098 SIMP_TAC list_ss [PATH_USED_VARS_def, IN_ABS, IN_LIST_BIGUNION, 2099 listTheory.MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_SEL] THEN 2100 REPEAT STRIP_TAC THEN 2101 UNDISCH_HD_TAC THEN 2102 Cases_on `n' > j` THENL [ 2103 ASM_SIMP_TAC std_ss [ELEM_CAT_SEL___GREATER, TOP_OMEGA_def, ELEM_INFINITE, 2104 LETTER_USED_VARS_def, NOT_IN_EMPTY], 2105 2106 ASM_SIMP_TAC arith_ss [ELEM_CAT_SEL___LESS_EQ, TOP_OMEGA_def] THEN 2107 REPEAT STRIP_TAC THEN 2108 Q_TAC EXISTS_TAC `n'` THEN 2109 ASM_REWRITE_TAC[] THEN 2110 Cases_on `v` THEN 2111 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, LS] 2112 ], 2113 2114 2115 2116 SIMP_TAC std_ss [F_CLOCK_FREE_def, UF_SEM_def, F_VAR_RENAMING_def, 2117 F_USED_VARS_def, LENGTH_PATH_VAR_RENAMING] THEN 2118 REPEAT STRIP_TAC THEN 2119 BOOL_EQ_STRIP_TAC THEN 2120 SUBGOAL_TAC `LENGTH v >= 1` THEN1 ( 2121 Cases_on `v` THEN 2122 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE] 2123 ) THEN 2124 ASM_SIMP_TAC std_ss [RESTN_PATH_VAR_RENAMING] THEN 2125 REMAINS_TAC `INJ f' (PATH_USED_VARS (RESTN v 1) UNION F_USED_VARS f) UNIV` THEN1 ( 2126 PROVE_TAC[] 2127 ) THEN 2128 UNDISCH_NO_TAC 2 THEN 2129 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2130 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2131 PROVE_TAC[RESTN_PATH_USED_VARS, SUBSET_DEF], 2132 2133 2134 SIMP_TAC (std_ss++resq_SS) [F_CLOCK_FREE_def, UF_SEM_def, F_VAR_RENAMING_def, 2135 IN_LESSX_REWRITE, IN_LESS, F_USED_VARS_def, LENGTH_PATH_VAR_RENAMING] THEN 2136 REPEAT STRIP_TAC THEN 2137 EXISTS_EQ_STRIP_TAC THEN 2138 BOOL_EQ_STRIP_TAC THEN 2139 BINOP_TAC THENL [ 2140 SUBGOAL_TAC `LENGTH v >= k` THEN1 ( 2141 Cases_on `v` THEN 2142 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE, LS] 2143 ) THEN 2144 ASM_SIMP_TAC std_ss [RESTN_PATH_VAR_RENAMING] THEN 2145 REMAINS_TAC `INJ f'' (PATH_USED_VARS (RESTN v k) UNION F_USED_VARS f') UNIV` THEN1 ( 2146 PROVE_TAC[] 2147 ) THEN 2148 UNDISCH_NO_TAC 2 THEN 2149 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2150 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2151 PROVE_TAC[RESTN_PATH_USED_VARS, SUBSET_DEF, GT_LS], 2152 2153 2154 FORALL_EQ_STRIP_TAC THEN 2155 BOOL_EQ_STRIP_TAC THEN 2156 SUBGOAL_TAC `LENGTH v >= j /\ LENGTH v > j` THEN1 ( 2157 Cases_on `v` THEN 2158 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, GE, LS] 2159 ) THEN 2160 ASM_SIMP_TAC std_ss [RESTN_PATH_VAR_RENAMING] THEN 2161 REMAINS_TAC `INJ f'' (PATH_USED_VARS (RESTN v j) UNION F_USED_VARS f) UNIV` THEN1 ( 2162 PROVE_TAC[] 2163 ) THEN 2164 UNDISCH_NO_TAC 4 THEN 2165 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2166 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2167 PROVE_TAC[RESTN_PATH_USED_VARS, SUBSET_DEF] 2168 ], 2169 2170 2171 2172 SIMP_TAC (std_ss++resq_SS) [F_CLOCK_FREE_def, UF_SEM_def, F_VAR_RENAMING_def, 2173 IN_LESSX_REWRITE, IN_LESS, F_USED_VARS_def, LENGTH_PATH_VAR_RENAMING] THEN 2174 REPEAT STRIP_TAC THEN 2175 BINOP_TAC THENL [ 2176 REMAINS_TAC `INJ f' (PATH_USED_VARS v UNION F_USED_VARS f) UNIV` THEN1 ( 2177 PROVE_TAC[] 2178 ) THEN 2179 UNDISCH_HD_TAC THEN 2180 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2181 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2182 PROVE_TAC[], 2183 2184 2185 EXISTS_EQ_STRIP_TAC THEN 2186 BOOL_EQ_STRIP_TAC THEN 2187 BINOP_TAC THENL [ 2188 ASM_SIMP_TAC std_ss [ELEM_PATH_VAR_RENAMING, GT_LS] THEN 2189 MATCH_MP_TAC B_SEM___VAR_RENAMING THEN 2190 UNDISCH_NO_TAC 1 THEN 2191 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2192 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, PATH_USED_VARS_def, IN_ABS] THEN 2193 PROVE_TAC[GT_LS], 2194 2195 Cases_on `j` THENL [ 2196 REWRITE_TAC[] THEN 2197 REMAINS_TAC `INJ f' (PATH_USED_VARS TOP_OMEGA UNION F_USED_VARS f) UNIV` THEN1 ( 2198 PROVE_TAC[PATH_VAR_RENAMING___TOP_OMEGA] 2199 ) THEN 2200 UNDISCH_NO_TAC 1 THEN 2201 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2202 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, PATH_USED_VARS_def, 2203 PATH_USED_VARS___TOP_OMEGA, NOT_IN_EMPTY], 2204 2205 2206 SIMP_TAC arith_ss [] THEN 2207 SUBGOAL_TAC `CAT (SEL (PATH_VAR_RENAMING f' v) (0,n),TOP_OMEGA) = 2208 PATH_VAR_RENAMING f' (CAT (SEL v (0,n),TOP_OMEGA))` THEN1 ( 2209 SUBGOAL_TAC `LENGTH v > n /\ n >= 0` THEN1 ( 2210 Cases_on `v` THEN 2211 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, LS] 2212 ) THEN 2213 ASM_SIMP_TAC std_ss [PATH_VAR_RENAMING___CAT, 2214 SEL_PATH_VAR_RENAMING, PATH_VAR_RENAMING___TOP_OMEGA] 2215 ) THEN 2216 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 2217 2218 REMAINS_TAC `INJ f' (PATH_USED_VARS (CAT (SEL v (0,n),TOP_OMEGA)) UNION F_USED_VARS f) UNIV` THEN1 ( 2219 PROVE_TAC[PATH_VAR_RENAMING___TOP_OMEGA] 2220 ) THEN 2221 UNDISCH_NO_TAC 1 THEN 2222 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2223 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, CAT_PATH_USED_VARS, PATH_USED_VARS___TOP_OMEGA, 2224 NOT_IN_EMPTY] THEN 2225 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 2226 DISJ1_TAC THEN 2227 SUBGOAL_TAC `LENGTH v > n /\ n >= 0` THEN1 ( 2228 Cases_on `v` THEN 2229 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, LS] 2230 ) THEN 2231 PROVE_TAC[SEL_PATH_USED_VARS, SUBSET_DEF] 2232 ] 2233 ] 2234 ], 2235 2236 2237 REWRITE_TAC[F_CLOCK_FREE_def], 2238 2239 2240 SIMP_TAC (std_ss++resq_SS) [F_CLOCK_FREE_def, UF_SEM_def, F_VAR_RENAMING_def, 2241 IN_LESSX_REWRITE, IN_LESS, F_USED_VARS_def, LENGTH_PATH_VAR_RENAMING] THEN 2242 REPEAT STRIP_TAC THEN 2243 FORALL_EQ_STRIP_TAC THEN 2244 BOOL_EQ_STRIP_TAC THEN 2245 BINOP_TAC THENL [ 2246 SUBGOAL_TAC `LENGTH (COMPLEMENT v) > j /\ j >= 0` THEN1 ( 2247 FULL_SIMP_TAC arith_ss [LENGTH_def, LENGTH_COMPLEMENT, GT_LS] 2248 ) THEN 2249 ASM_SIMP_TAC std_ss [COMPLEMENT_PATH_VAR_RENAMING, SEL_PATH_VAR_RENAMING] THEN 2250 MATCH_MP_TAC US_SEM___VAR_RENAMING THEN 2251 ASM_REWRITE_TAC[] THEN 2252 UNDISCH_NO_TAC 3 THEN 2253 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2254 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, CAT_PATH_USED_VARS, PATH_USED_VARS___TOP_OMEGA, 2255 NOT_IN_EMPTY] THEN 2256 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 2257 DISJ1_TAC THEN 2258 PROVE_TAC[SEL_PATH_USED_VARS, SUBSET_DEF, PATH_USED_VARS_COMPLEMENT], 2259 2260 2261 SUBGOAL_TAC `LENGTH v >= j` THEN1 ( 2262 Cases_on `v` THEN 2263 FULL_SIMP_TAC arith_ss [LENGTH_def, GT, LS, GE] 2264 ) THEN 2265 ASM_SIMP_TAC std_ss [RESTN_PATH_VAR_RENAMING] THEN 2266 REMAINS_TAC `INJ f' (PATH_USED_VARS (RESTN v j) UNION F_USED_VARS f) UNIV` THEN1 ( 2267 PROVE_TAC[] 2268 ) THEN 2269 UNDISCH_NO_TAC 2 THEN 2270 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 2271 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2272 PROVE_TAC[RESTN_PATH_USED_VARS, GT_LS, SUBSET_DEF] 2273 ] 2274 ]); 2275 2276 2277 2278val S_VAR_RENAMING___S_CLOCK_FREE = 2279 store_thm 2280 ("S_VAR_RENAMING___S_CLOCK_FREE", 2281 2282 ``!r g. S_CLOCK_FREE (S_VAR_RENAMING g r) = 2283 S_CLOCK_FREE r``, 2284 2285 INDUCT_THEN sere_induct ASSUME_TAC THEN ( 2286 ASM_SIMP_TAC std_ss [S_VAR_RENAMING_def, 2287 S_CLOCK_FREE_def] 2288 )); 2289 2290 2291val F_VAR_RENAMING___F_CLOCK_SERE_FREE = 2292 store_thm 2293 ("F_VAR_RENAMING___F_CLOCK_SERE_FREE", 2294 2295 ``!f g. (F_CLOCK_SERE_FREE (F_VAR_RENAMING g f) = 2296 F_CLOCK_SERE_FREE f) /\ 2297 (F_CLOCK_FREE (F_VAR_RENAMING g f) = 2298 F_CLOCK_FREE f) /\ 2299 (F_SERE_FREE (F_VAR_RENAMING g f) = 2300 F_SERE_FREE f)``, 2301 2302 INDUCT_THEN fl_induct ASSUME_TAC THEN ( 2303 ASM_SIMP_TAC std_ss [F_VAR_RENAMING_def, 2304 F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, 2305 F_SERE_FREE_def, S_VAR_RENAMING___S_CLOCK_FREE] 2306 )); 2307 2308 2309val WEAK_UF_SEM_def = 2310 Define 2311 `WEAK_UF_SEM v f = UF_SEM (PATH_APPEND v TOP_OMEGA) f`; 2312 2313 2314val STRONG_UF_SEM_def = 2315 Define 2316 `STRONG_UF_SEM v f = UF_SEM (PATH_APPEND v BOTTOM_OMEGA) f`; 2317 2318 2319val IS_PATH_WITH_REPLACEMENTS_def = 2320 Define 2321 `IS_PATH_WITH_REPLACEMENTS v w x = (LENGTH v = LENGTH w) /\ 2322 (!n. n < LENGTH v ==> ((ELEM v n = ELEM w n) \/ (ELEM v n = x)))`; 2323 2324 2325val IS_LIST_WITH_REPLACEMENTS_def = 2326 Define 2327 `IS_LIST_WITH_REPLACEMENTS v w x = (LENGTH v = LENGTH w) /\ 2328 (!n. n < LENGTH v ==> ((EL n v = EL n w) \/ (EL n v = x)))`; 2329 2330 2331val IS_TOP_BOTTOM_WELL_BEHAVED_def = 2332 Define 2333 `(IS_TOP_BOTTOM_WELL_BEHAVED (F_STRONG_BOOL b) = T) 2334 /\ 2335 (IS_TOP_BOTTOM_WELL_BEHAVED (F_WEAK_BOOL b) = T) 2336 /\ 2337 (IS_TOP_BOTTOM_WELL_BEHAVED (F_NOT f) = IS_TOP_BOTTOM_WELL_BEHAVED f) 2338 /\ 2339 (IS_TOP_BOTTOM_WELL_BEHAVED (F_AND(f1,f2)) = IS_TOP_BOTTOM_WELL_BEHAVED f1 /\ IS_TOP_BOTTOM_WELL_BEHAVED f2) 2340 /\ 2341 (IS_TOP_BOTTOM_WELL_BEHAVED (F_STRONG_SERE r) = ((UF_SEM TOP_OMEGA (F_STRONG_SERE r)) /\ ~(UF_SEM BOTTOM_OMEGA (F_STRONG_SERE r)))) 2342 /\ 2343 (IS_TOP_BOTTOM_WELL_BEHAVED (F_WEAK_SERE r) = ((UF_SEM TOP_OMEGA (F_WEAK_SERE r)) /\ ~(UF_SEM BOTTOM_OMEGA (F_WEAK_SERE r)))) 2344 /\ 2345 (IS_TOP_BOTTOM_WELL_BEHAVED (F_NEXT f) = IS_TOP_BOTTOM_WELL_BEHAVED f) 2346 /\ 2347 (IS_TOP_BOTTOM_WELL_BEHAVED (F_UNTIL(f1,f2)) = IS_TOP_BOTTOM_WELL_BEHAVED f1 /\ IS_TOP_BOTTOM_WELL_BEHAVED f2) 2348 /\ 2349 (IS_TOP_BOTTOM_WELL_BEHAVED (F_ABORT (f,b)) = IS_TOP_BOTTOM_WELL_BEHAVED f) 2350 /\ 2351 (IS_TOP_BOTTOM_WELL_BEHAVED (F_SUFFIX_IMP(r,f)) = ((UF_SEM TOP_OMEGA (F_SUFFIX_IMP (r, f))) /\ ~(UF_SEM BOTTOM_OMEGA (F_SUFFIX_IMP (r, f)))) /\ IS_TOP_BOTTOM_WELL_BEHAVED f)`; 2352 2353 2354 2355 2356 2357val IS_PSL_G_def = 2358 Define 2359 `(IS_PSL_G (F_STRONG_BOOL b) = T) /\ 2360 (IS_PSL_G (F_WEAK_BOOL b) = T) /\ 2361 (IS_PSL_G (F_NOT f) = IS_PSL_F f) /\ 2362 (IS_PSL_G (F_AND (f,g)) = (IS_PSL_G f /\ IS_PSL_G g)) /\ 2363 (IS_PSL_G (F_NEXT f) = IS_PSL_G f) /\ 2364 (IS_PSL_G (F_UNTIL(f,g)) = F) /\ 2365 (IS_PSL_G (F_ABORT (f,p)) = IS_PSL_G f) /\ 2366 (IS_PSL_G (F_STRONG_SERE r) = F) /\ 2367 (IS_PSL_G (F_WEAK_SERE r) = F) /\ 2368 (IS_PSL_G (F_SUFFIX_IMP (r,f)) = F) /\ 2369 (IS_PSL_G (F_CLOCK v) = F) /\ 2370 (IS_PSL_F (F_STRONG_BOOL b) = T) /\ 2371 (IS_PSL_F (F_WEAK_BOOL b) = T) /\ 2372 (IS_PSL_F (F_NOT f) = IS_PSL_G f) /\ 2373 (IS_PSL_F (F_AND (f,g)) = (IS_PSL_F f /\ IS_PSL_F g)) /\ 2374 (IS_PSL_F (F_NEXT f) = IS_PSL_F f) /\ 2375 (IS_PSL_F (F_UNTIL(f,g)) = (IS_PSL_F f /\ IS_PSL_F g)) /\ 2376 (IS_PSL_F (F_ABORT (f,p)) = IS_PSL_F f) /\ 2377 (IS_PSL_F (F_STRONG_SERE r) = F) /\ 2378 (IS_PSL_F (F_WEAK_SERE r) = F) /\ 2379 (IS_PSL_F (F_SUFFIX_IMP (r,f)) = F) /\ 2380 (IS_PSL_F (F_CLOCK v) = F)`; 2381 2382 2383val IS_PSL_PREFIX_def = 2384 Define 2385 `(IS_PSL_PREFIX (F_NOT f) = IS_PSL_PREFIX f) /\ 2386 (IS_PSL_PREFIX (F_AND (f,g)) = (IS_PSL_PREFIX f /\ IS_PSL_PREFIX g)) /\ 2387 (IS_PSL_PREFIX (F_ABORT (f, p)) = (IS_PSL_PREFIX f)) /\ 2388 (IS_PSL_PREFIX f = (IS_PSL_G f \/ IS_PSL_F f))`; 2389 2390 2391val IS_PSL_GF_def= 2392 Define 2393 `(IS_PSL_GF (F_STRONG_BOOL b) = T) /\ 2394 (IS_PSL_GF (F_WEAK_BOOL b) = T) /\ 2395 (IS_PSL_GF (F_NOT f) = IS_PSL_FG f) /\ 2396 (IS_PSL_GF (F_AND (f,g)) = (IS_PSL_GF f /\ IS_PSL_GF g)) /\ 2397 (IS_PSL_GF (F_NEXT f) = IS_PSL_GF f) /\ 2398 (IS_PSL_GF (F_UNTIL(f,g)) = (IS_PSL_GF f /\ IS_PSL_F g)) /\ 2399 (IS_PSL_GF (F_ABORT (f,p)) = IS_PSL_GF f) /\ 2400 (IS_PSL_GF (F_STRONG_SERE r) = F) /\ 2401 (IS_PSL_GF (F_WEAK_SERE r) = F) /\ 2402 (IS_PSL_GF (F_SUFFIX_IMP (r,f)) = F) /\ 2403 (IS_PSL_GF (F_CLOCK v) = F) /\ 2404 2405 (IS_PSL_FG (F_STRONG_BOOL b) = T) /\ 2406 (IS_PSL_FG (F_WEAK_BOOL b) = T) /\ 2407 (IS_PSL_FG (F_NOT f) = IS_PSL_GF f) /\ 2408 (IS_PSL_FG (F_AND (f,g)) = (IS_PSL_FG f /\ IS_PSL_FG g)) /\ 2409 (IS_PSL_FG (F_NEXT f) = IS_PSL_FG f) /\ 2410 (IS_PSL_FG (F_UNTIL(f,g)) = (IS_PSL_FG f /\ IS_PSL_FG g)) /\ 2411 (IS_PSL_FG (F_ABORT (f,p)) = IS_PSL_FG f) /\ 2412 (IS_PSL_FG (F_STRONG_SERE r) = F) /\ 2413 (IS_PSL_FG (F_WEAK_SERE r) = F) /\ 2414 (IS_PSL_FG (F_SUFFIX_IMP (r,f)) = F) /\ 2415 (IS_PSL_FG (F_CLOCK v) = F)`; 2416 2417 2418val IS_PSL_STREET_def = 2419 Define 2420 `(IS_PSL_STREET (F_NOT f) = IS_PSL_STREET f) /\ 2421 (IS_PSL_STREET (F_AND (f,g)) = (IS_PSL_STREET f /\ IS_PSL_STREET g)) /\ 2422 (IS_PSL_STREET (F_ABORT (f, p)) = (IS_PSL_STREET f)) /\ 2423 (IS_PSL_STREET f = (IS_PSL_GF f \/ IS_PSL_FG f))`; 2424 2425 2426val IS_PSL_THM = save_thm("IS_PSL_THM", 2427 LIST_CONJ [IS_PSL_G_def, 2428 IS_PSL_GF_def, 2429 IS_PSL_PREFIX_def, 2430 IS_PSL_STREET_def]); 2431 2432 2433(*============================================================================= 2434= General lemmata about PSL 2435============================================================================*) 2436 2437val IS_INFINITE_TOP_BOTTOM_FREE_PATH___IMPLIES___IS_INFINITE_PROPER_PATH = 2438 store_thm 2439 ("IS_INFINITE_TOP_BOTTOM_FREE_PATH___IMPLIES___IS_INFINITE_PROPER_PATH", 2440 ``!f. IS_INFINITE_TOP_BOTTOM_FREE_PATH f ==> IS_INFINITE_PROPER_PATH f``, 2441 2442 REWRITE_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, IS_INFINITE_PROPER_PATH_def] THEN 2443 PROVE_TAC[letter_distinct]); 2444 2445 2446 2447val BEXP_PROP_FREE___B_SEM = 2448 store_thm 2449 ("BEXP_PROP_FREE___B_SEM", 2450 2451 ``!b s c. BEXP_PROP_FREE c b ==> (B_SEM s b = B_SEM (INSERT_PROP c s) b)``, 2452 2453 REPEAT STRIP_TAC THEN 2454 REMAINS_TAC `LETTER_RESTRICT (B_USED_VARS b) s = 2455 LETTER_RESTRICT (B_USED_VARS b) (INSERT_PROP c s)` THEN1 ( 2456 PROVE_TAC[B_USED_VARS_INTER_SUBSET_THM, SUBSET_REFL] 2457 ) THEN 2458 Cases_on `s` THEN 2459 REWRITE_TAC[LETTER_RESTRICT_def, INSERT_PROP_def, letter_11] THEN 2460 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_ABS] THEN 2461 REPEAT STRIP_TAC THEN 2462 BOOL_EQ_STRIP_TAC THEN 2463 `~(x = c)` by PROVE_TAC [BEXP_PROP_FREE_def] THEN 2464 ASM_SIMP_TAC std_ss [IN_DEF]); 2465 2466 2467val S_CLOCK_FREE___S_CLOCK_COMP = 2468 store_thm 2469 ("S_CLOCK_FREE___S_CLOCK_COMP", 2470 ``!r c. (S_CLOCK_FREE (S_CLOCK_COMP c r))``, 2471 2472 INDUCT_THEN sere_induct ASSUME_TAC THEN 2473 ASM_SIMP_TAC std_ss [S_CLOCK_COMP_def, S_CLOCK_FREE_def]); 2474 2475 2476val F_CLOCK_FREE___F_CLOCK_COMP = 2477 store_thm 2478 ("F_CLOCK_FREE___F_CLOCK_COMP", 2479 ``!f c. (F_CLOCK_FREE (F_CLOCK_COMP c f))``, 2480 2481 INDUCT_THEN fl_induct ASSUME_TAC THEN 2482 ASM_SIMP_TAC std_ss [F_CLOCK_COMP_def, 2483 F_CLOCK_FREE_def, 2484 F_U_CLOCK_def, 2485 F_W_CLOCK_def, 2486 F_W_def, 2487 F_OR_def, 2488 F_G_def, 2489 F_F_def, 2490 F_IMPLIES_def, 2491 S_CLOCK_FREE___S_CLOCK_COMP]); 2492 2493 2494val F_SERE_FREE___IMPLIES___F_SERE_FREE_F_CLOCK_COMP = 2495 store_thm 2496 ("F_SERE_FREE___IMPLIES___F_SERE_FREE_F_CLOCK_COMP", 2497 ``!f c. F_SERE_FREE f ==> (F_SERE_FREE (F_CLOCK_COMP c f))``, 2498 2499 INDUCT_THEN fl_induct ASSUME_TAC THEN 2500 ASM_SIMP_TAC std_ss [F_CLOCK_COMP_def, 2501 F_SERE_FREE_def, 2502 F_U_CLOCK_def, 2503 F_W_CLOCK_def, 2504 F_W_def, 2505 F_OR_def, 2506 F_G_def, 2507 F_F_def, 2508 F_IMPLIES_def]); 2509 2510 2511val S_USED_VARS___CLOCK_COMP = 2512 store_thm 2513 ("S_USED_VARS___CLOCK_COMP", 2514 ``!s c. S_USED_VARS (S_CLOCK_COMP c s) SUBSET S_USED_VARS s UNION B_USED_VARS c``, 2515 2516 REWRITE_TAC[SUBSET_DEF, IN_UNION] THEN 2517 INDUCT_THEN sere_induct ASSUME_TAC THEN 2518 ASM_SIMP_TAC std_ss [S_CLOCK_COMP_def, S_USED_VARS_def, 2519 B_USED_VARS_def, IN_UNION, 2520 NOT_IN_EMPTY] THEN 2521 REPEAT STRIP_TAC THEN 2522 REPEAT BOOL_EQ_STRIP_TAC THEN 2523 ASM_SIMP_TAC std_ss [] THEN 2524 METIS_TAC[]); 2525 2526val F_USED_VARS___CLOCK_COMP = 2527 store_thm 2528 ("F_USED_VARS___CLOCK_COMP", 2529 ``!f c. F_USED_VARS (F_CLOCK_COMP c f) SUBSET (F_USED_VARS f UNION B_USED_VARS c)``, 2530 2531 ASSUME_TAC S_USED_VARS___CLOCK_COMP THEN 2532 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 2533 INDUCT_THEN fl_induct ASSUME_TAC THEN 2534 ASM_SIMP_TAC std_ss [F_CLOCK_COMP_def, 2535 F_USED_VARS_def, 2536 B_USED_VARS_def, 2537 F_U_CLOCK_def, 2538 F_W_CLOCK_def, 2539 F_W_def, 2540 F_OR_def, 2541 F_G_def, 2542 F_F_def, 2543 F_IMPLIES_def, 2544 IN_UNION, 2545 NOT_IN_EMPTY] THEN 2546 REPEAT STRIP_TAC THEN 2547 REPEAT BOOL_EQ_STRIP_TAC THEN 2548 ASM_REWRITE_TAC [] THEN 2549 METIS_TAC[]); 2550 2551 2552 2553val INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA = 2554 store_thm 2555 ("INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA", 2556 ``(!v t t'. ((IS_INFINITE_PROPER_PATH v) /\ (ELEM v t = TOP) /\ (t <= t')) ==> 2557 (RESTN v t' = TOP_OMEGA)) /\ 2558 (!v t t'. ((IS_INFINITE_PROPER_PATH v) /\ (ELEM v t = BOTTOM) /\ (t <= t')) ==> 2559 (RESTN v t' = BOTTOM_OMEGA))``, 2560 2561 REWRITE_TAC[IS_INFINITE_PROPER_PATH_def, TOP_OMEGA_def, BOTTOM_OMEGA_def] THEN 2562 REPEAT STRIP_TAC THEN 2563 ASM_SIMP_TAC std_ss [RESTN_INFINITE, path_11, FUN_EQ_THM] THEN 2564 REPEAT STRIP_TAC THEN ( 2565 `t <= n + t'` by DECIDE_TAC THEN 2566 `?u. n + t' = t + u` by PROVE_TAC[LESS_EQ_EXISTS] THEN 2567 FULL_SIMP_TAC arith_ss [] THEN 2568 WEAKEN_TAC (fn t => true) THEN 2569 Induct_on `u` THENL [ 2570 EVAL_TAC THEN ASM_SIMP_TAC arith_ss [] THEN PROVE_TAC[ELEM_INFINITE], 2571 ASM_SIMP_TAC arith_ss [GSYM ADD_SUC] 2572 ] 2573 )); 2574 2575 2576val PROPER_PATH___IS_INFINITE_TOP_BOTTOM = 2577 store_thm 2578 ("PROPER_PATH___IS_INFINITE_TOP_BOTTOM", 2579 ``(!v t. ((IS_PROPER_PATH v) /\ (t < LENGTH v) /\ ((ELEM v t = TOP) \/ (ELEM v t = BOTTOM))) ==> 2580 IS_INFINITE_PROPER_PATH v)``, 2581 2582 SIMP_TAC std_ss [IS_PROPER_PATH_def, IS_FINITE_PROPER_PATH_def] THEN 2583 REPEAT STRIP_TAC THEN 2584 PROVE_TAC[PATH_TOP_FREE_ELEM, PATH_BOTTOM_FREE_ELEM]); 2585 2586 2587 2588 2589 2590val PATH_PROP_FREE_SEM = 2591 store_thm 2592 ("PATH_PROP_FREE_SEM", 2593 ``!s t f p. (PATH_PROP_FREE p (INFINITE f)) ==> ((f t = STATE s) ==> (~ s p))``, 2594 2595 REWRITE_TAC [PATH_PROP_FREE_def, ELEM_INFINITE, IN_DEF] THEN 2596 EVAL_TAC THEN 2597 PROVE_TAC[] 2598); 2599 2600 2601val PATH_PROP_FREE_RESTN = 2602 store_thm 2603 ("PATH_PROP_FREE_RESTN", 2604 ``!v t p. t < LENGTH v ==> PATH_PROP_FREE p v ==> PATH_PROP_FREE p (RESTN v t)``, 2605 2606 REWRITE_TAC [LENGTH_def, LS, PATH_PROP_FREE_def, ELEM_RESTN] THEN 2607 Cases_on `v` THEN REPEAT STRIP_TAC THENL [ 2608 `LENGTH (RESTN (FINITE l) t) = LENGTH (FINITE l) - t` by PROVE_TAC[LENGTH_RESTN_COR] THEN 2609 FULL_SIMP_TAC list_ss [] THEN 2610 `n < (LENGTH l) - t` by PROVE_TAC [LENGTH_def, LS, SUB_xnum_num_def] THEN 2611 `n+t < LENGTH l` by DECIDE_TAC THEN 2612 `n + t < LENGTH (FINITE l)` by PROVE_TAC [LENGTH_def, LS, SUB_xnum_num_def] THEN 2613 PROVE_TAC[], 2614 2615 FULL_SIMP_TAC list_ss [LENGTH_def, LS] THEN 2616 PROVE_TAC[] 2617 ]); 2618 2619 2620val PATH_PROP_FREE_COMPLEMENT = 2621 store_thm 2622 ("PATH_PROP_FREE_COMPLEMENT", 2623 ``!t f. PATH_PROP_FREE t f = PATH_PROP_FREE t (COMPLEMENT f)``, 2624 2625 SIMP_TAC list_ss [PATH_PROP_FREE_def, LENGTH_COMPLEMENT, ELEM_COMPLEMENT, COMPLEMENT_LETTER_Cases] 2626); 2627 2628 2629val IS_INFINITE_PROPER_PATH___COMPLEMENT = 2630 store_thm 2631 ("IS_INFINITE_PROPER_PATH___COMPLEMENT", 2632 ``!v. IS_INFINITE_PROPER_PATH v = IS_INFINITE_PROPER_PATH (COMPLEMENT v)``, 2633 STRIP_TAC THEN 2634 REWRITE_TAC [IS_INFINITE_PROPER_PATH_def] THEN 2635 EQ_TAC THEN 2636 REPEAT STRIP_TAC THEN 2637 EXISTS_TAC ``COMPLEMENT_LETTER o (p :num -> 'a letter)`` 2638 THENL [ 2639 ALL_TAC, 2640 `v = COMPLEMENT (INFINITE p)` by PROVE_TAC[COMPLEMENT_COMPLEMENT] 2641 ] THEN 2642 FULL_SIMP_TAC list_ss [COMPLEMENT_def, COMPLEMENT_LETTER_Cases]); 2643 2644 2645val IS_INFINITE_PROPER_PATH_RESTN = 2646 store_thm 2647 ("IS_INFINITE_PROPER_PATH_RESTN", 2648 ``!v t. IS_INFINITE_PROPER_PATH v ==> IS_INFINITE_PROPER_PATH (RESTN v t)``, 2649 2650 REWRITE_TAC [IS_INFINITE_PROPER_PATH_def] THEN 2651 REPEAT STRIP_TAC THEN 2652 EXISTS_TAC ``(\n. p (n + t)):num -> 'a letter`` THEN 2653 ASM_SIMP_TAC arith_ss [RESTN_INFINITE, GSYM ADD_SUC]); 2654 2655 2656 2657 2658val IS_INFINITE_PROPER_PATH___CAT_SEL_TOP_OMEGA = 2659 store_thm 2660 ("IS_INFINITE_PROPER_PATH___CAT_SEL_TOP_OMEGA", 2661 ``!v j. (IS_INFINITE_PROPER_PATH v /\ ~(ELEM v j = BOTTOM)) ==> IS_INFINITE_PROPER_PATH (CAT (SEL v (0,j - 1),TOP_OMEGA))``, 2662 2663 REPEAT GEN_TAC THEN 2664 `? v'. (CAT (SEL v (0,j - 1),TOP_OMEGA)) = v'` by PROVE_TAC[] THEN 2665 REWRITE_TAC [IS_INFINITE_PROPER_PATH_def] THEN 2666 `IS_INFINITE v'` by PROVE_TAC[CAT_INFINITE, TOP_OMEGA_def] THEN 2667 `?q. INFINITE q = v'` by PROVE_TAC[IS_INFINITE_EXISTS] THEN 2668 REPEAT STRIP_TAC THEN 2669 EXISTS_TAC ``q:num -> 'a letter`` THEN 2670 REPEAT STRIP_TAC THENL [ 2671 PROVE_TAC[], 2672 2673 Cases_on `SUC n <= j-1` THENL [ 2674 `n <= j - 1` by DECIDE_TAC THEN 2675 `ELEM (INFINITE q) n = ELEM v n` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 2676 `ELEM (INFINITE q) (SUC n) = ELEM v (SUC n)` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 2677 `q n = p n` by PROVE_TAC[ELEM_INFINITE] THEN 2678 `q (SUC n) = p (SUC n)` by PROVE_TAC[ELEM_INFINITE] THEN 2679 `p n = TOP` by PROVE_TAC[] THEN 2680 `p (SUC n) = TOP` by PROVE_TAC[] THEN 2681 PROVE_TAC[], 2682 2683 `SUC n > j - 1` by DECIDE_TAC THEN 2684 `ELEM (INFINITE q) (SUC n) = ELEM TOP_OMEGA (SUC n - (SUC (j-1)))` by PROVE_TAC[ELEM_CAT_SEL___GREATER] THEN 2685 FULL_SIMP_TAC arith_ss [ELEM_INFINITE, TOP_OMEGA_def] 2686 ], 2687 2688 Cases_on `SUC n <= j-1` THENL [ 2689 `n <= j - 1` by DECIDE_TAC THEN 2690 `ELEM (INFINITE q) n = ELEM v n` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 2691 `ELEM (INFINITE q) (SUC n) = ELEM v (SUC n)` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 2692 `q n = p n` by PROVE_TAC[ELEM_INFINITE] THEN 2693 `q (SUC n) = p (SUC n)` by PROVE_TAC[ELEM_INFINITE] THEN 2694 `p n = BOTTOM` by PROVE_TAC[] THEN 2695 `p (SUC n) = BOTTOM` by PROVE_TAC[] THEN 2696 PROVE_TAC[], 2697 2698 Cases_on `n > j - 1` THENL [ 2699 `ELEM (INFINITE q) n = ELEM TOP_OMEGA (n - SUC (j-1))` by PROVE_TAC[ELEM_CAT_SEL___GREATER] THEN 2700 FULL_SIMP_TAC arith_ss [ELEM_INFINITE, TOP_OMEGA_def] THEN 2701 `~ (TOP = BOTTOM)` by EVAL_TAC, 2702 2703 `n <= j - 1` by DECIDE_TAC THEN 2704 `ELEM (INFINITE q) n = ELEM v n` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 2705 `q n = p n` by PROVE_TAC[ELEM_INFINITE] THEN 2706 `p n = BOTTOM` by PROVE_TAC[] THEN 2707 Cases_on `j = 0` THENL [ 2708 `n = j` by DECIDE_TAC THEN 2709 `p j = BOTTOM` by PROVE_TAC[], 2710 2711 `p (SUC n) = BOTTOM` by PROVE_TAC[] THEN 2712 `SUC n = j` by DECIDE_TAC 2713 ] THEN 2714 `p j = BOTTOM` by PROVE_TAC[] THEN 2715 PROVE_TAC [ELEM_INFINITE] 2716 ] 2717 ] 2718 ]); 2719 2720 2721 2722val PATH_PROP_FREE___CAT_SEL_INFINITE___IMPLIES = 2723 store_thm 2724 ("PATH_PROP_FREE___CAT_SEL_INFINITE___IMPLIES", 2725 ``!p a j. PATH_PROP_FREE a (INFINITE p) ==> PATH_PROP_FREE a (CAT (SEL (INFINITE p) (0,j - 1),TOP_OMEGA))``, 2726 2727 REWRITE_TAC [PATH_PROP_FREE_def, IN_DEF] THEN 2728 ASM_REWRITE_TAC [LENGTH_def, LS, ELEM_INFINITE] THEN 2729 REPEAT STRIP_TAC THEN 2730 Cases_on `n <= j - 1` THENL [ 2731 `ELEM (CAT (SEL (INFINITE p) (0,j - 1),TOP_OMEGA)) n = ELEM (INFINITE p) n` by PROVE_TAC[ELEM_CAT_SEL___LESS_EQ] THEN 2732 PROVE_TAC[ELEM_INFINITE], 2733 2734 `n > j - 1` by DECIDE_TAC THEN 2735 `~(STATE s = TOP)` by EVAL_TAC THEN 2736 `ELEM (CAT (SEL (INFINITE p) (0,j - 1),TOP_OMEGA)) n = ELEM TOP_OMEGA (n-SUC (j-1))` by PROVE_TAC[ELEM_CAT_SEL___GREATER] THEN 2737 FULL_SIMP_TAC arith_ss [TOP_OMEGA_def, ELEM_INFINITE] 2738 ]); 2739 2740 2741val IS_FINITE_PROPER_PATH___COMPLEMENT = 2742 store_thm 2743 ("IS_FINITE_PROPER_PATH___COMPLEMENT", 2744 2745 ``!v. IS_FINITE_PROPER_PATH v ==> ((COMPLEMENT v) = v)``, 2746 2747 REPEAT STRIP_TAC THEN 2748 FULL_SIMP_TAC std_ss [IS_FINITE_PROPER_PATH_def] THEN 2749 2750 REWRITE_TAC[COMPLEMENT_def, path_11] THEN 2751 `TOP_FREE p /\ BOTTOM_FREE p` by PROVE_TAC[PATH_TOP_FREE_def, PATH_BOTTOM_FREE_def] THEN 2752 UNDISCH_TAC ``TOP_FREE p`` THEN 2753 UNDISCH_TAC ``BOTTOM_FREE p`` THEN 2754 SPEC_TAC (``p:'a letter list``,``q:'a letter list``) THEN 2755 Induct_on `q` THENL [ 2756 SIMP_TAC list_ss [], 2757 Cases_on `h` THEN ASM_SIMP_TAC list_ss [TOP_FREE_def, BOTTOM_FREE_def, COMPLEMENT_LETTER_def] 2758 ]); 2759 2760 2761val IS_FINITE_PROPER_PATH___RESTN = 2762 store_thm 2763 ("IS_FINITE_PROPER_PATH___RESTN", 2764 2765 ``!v k. (IS_FINITE_PROPER_PATH v /\ k < LENGTH v) ==> IS_FINITE_PROPER_PATH (RESTN v k)``, 2766 2767 Induct_on `k` THENL [ 2768 SIMP_TAC list_ss [IS_FINITE_PROPER_PATH_def, PSLPathTheory.RESTN_def, FinitePSLPathTheory.RESTN_def], 2769 2770 FULL_SIMP_TAC list_ss [IS_FINITE_PROPER_PATH_def] THEN 2771 REPEAT STRIP_TAC THEN 2772 ASM_SIMP_TAC list_ss [PSLPathTheory.RESTN_def, FinitePSLPathTheory.RESTN_def] THEN 2773 2774 `?v'. v' = FINITE (REST p)` by PROVE_TAC[] THEN 2775 `SUC k < LENGTH p` by METIS_TAC[LENGTH_def, LS] THEN 2776 `0 < LENGTH p` by DECIDE_TAC THEN 2777 `REST v = v'` by ASM_SIMP_TAC list_ss [PSLPathTheory.REST_def, FinitePSLPathTheory.REST_def] THEN 2778 `LENGTH v' = LENGTH v - 1` by 2779 ASM_SIMP_TAC list_ss [LENGTH_def, SUB_xnum_num_def, xnum_11, FinitePSLPathTheory.REST_def, LENGTH_TL] THEN 2780 SUBGOAL_THEN ``PATH_TOP_FREE (v':'a letter path)`` ASSUME_TAC THEN1( 2781 FULL_SIMP_TAC std_ss [PATH_TOP_FREE_ELEM] THEN 2782 `!n. (n < LENGTH (FINITE p) - 1) = (n + 1 < LENGTH (FINITE p))` by 2783 SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, LS] THEN 2784 `FINITE (REST p) = RESTN (FINITE p) 1` by EVAL_TAC THEN 2785 ASM_SIMP_TAC arith_ss [ELEM_RESTN] THEN 2786 METIS_TAC[] 2787 ) THEN 2788 SUBGOAL_THEN ``PATH_BOTTOM_FREE (v':'a letter path)`` ASSUME_TAC THEN1( 2789 FULL_SIMP_TAC std_ss [PATH_BOTTOM_FREE_ELEM] THEN 2790 `!n. (n < LENGTH (FINITE p) - 1) = (n + 1 < LENGTH (FINITE p))` by 2791 SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, LS] THEN 2792 `FINITE (REST p) = RESTN (FINITE p) 1` by EVAL_TAC THEN 2793 ASM_SIMP_TAC arith_ss [ELEM_RESTN] THEN 2794 METIS_TAC[] 2795 ) THEN 2796 `k < LENGTH v'` by ASM_SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, LS] THEN 2797 METIS_TAC[] 2798 ]); 2799 2800 2801 2802 2803(**************************************************************************) 2804(* Lemmata *) 2805(**************************************************************************) 2806 2807 2808 2809 2810 2811 2812 2813 2814val INFINITE_PROPER_PATH___TOP_BOTTOM_FOLLOWING = 2815 store_thm 2816 ("INFINITE_PROPER_PATH___TOP_BOTTOM_FOLLOWING", 2817 2818 ``!v k l. (IS_INFINITE_PROPER_PATH v /\ l >= k) ==> ( 2819 ((ELEM v k = TOP) ==> (ELEM v l = TOP)) /\ 2820 ((ELEM v k = BOTTOM) ==> (ELEM v l = BOTTOM)))``, 2821 2822 Induct_on `(l-k):num` THENL [ 2823 SIMP_TAC arith_ss [] THEN 2824 REPEAT STRIP_TAC THEN 2825 `l = k` by DECIDE_TAC THEN 2826 PROVE_TAC[], 2827 2828 REPEAT STRIP_TAC THEN 2829 `~(l = 0)` by DECIDE_TAC THEN 2830 `?l'. l = SUC l'` by PROVE_TAC[num_CASES] THEN 2831 `v = l' - k` by DECIDE_TAC THEN 2832 `l' >= k` by DECIDE_TAC THENL [ 2833 `ELEM v' l' = TOP` by METIS_TAC[], 2834 `ELEM v' l' = BOTTOM` by METIS_TAC[] 2835 ] THEN 2836 METIS_TAC[ELEM_INFINITE, IS_INFINITE_PROPER_PATH_def] 2837 ]); 2838 2839 2840val IS_PROPER_PATH___COMPLEMENT = 2841 store_thm 2842 ("IS_PROPER_PATH___COMPLEMENT", 2843 ``!v. (IS_PROPER_PATH v) = (IS_PROPER_PATH (COMPLEMENT v))``, 2844 2845 REWRITE_TAC[IS_PROPER_PATH_def] THEN 2846 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2847 PROVE_TAC[IS_INFINITE_PROPER_PATH___COMPLEMENT], 2848 PROVE_TAC[IS_FINITE_PROPER_PATH___COMPLEMENT], 2849 PROVE_TAC[IS_INFINITE_PROPER_PATH___COMPLEMENT], 2850 PROVE_TAC[IS_FINITE_PROPER_PATH___COMPLEMENT, COMPLEMENT_COMPLEMENT] 2851 ]); 2852 2853 2854val IS_PATH_WITH_REPLACEMENTS___COMPLEMENT = 2855 store_thm 2856 ("IS_PATH_WITH_REPLACEMENTS___COMPLEMENT", 2857 ``!v w x. (IS_PATH_WITH_REPLACEMENTS v w x = IS_PATH_WITH_REPLACEMENTS (COMPLEMENT v) (COMPLEMENT w) (COMPLEMENT_LETTER x))``, 2858 2859 REWRITE_TAC [IS_PATH_WITH_REPLACEMENTS_def] THEN 2860 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2861 ASM_REWRITE_TAC[LENGTH_COMPLEMENT], 2862 2863 FULL_SIMP_TAC std_ss [LENGTH_COMPLEMENT] THEN 2864 `n < LENGTH w` by PROVE_TAC[] THEN 2865 ASM_SIMP_TAC std_ss [ELEM_COMPLEMENT] THEN 2866 PROVE_TAC[COMPLEMENT_LETTER_COMPLEMENT_LETTER], 2867 2868 PROVE_TAC[LENGTH_COMPLEMENT], 2869 2870 FULL_SIMP_TAC std_ss [LENGTH_COMPLEMENT] THEN 2871 `n < LENGTH w` by PROVE_TAC[] THEN 2872 METIS_TAC[ELEM_COMPLEMENT, COMPLEMENT_LETTER_COMPLEMENT_LETTER] 2873 ]); 2874 2875val IS_PATH_WITH_REPLACEMENTS___CAT_SEL = 2876 store_thm 2877 ("IS_PATH_WITH_REPLACEMENTS___CAT_SEL", 2878 ``!v w j x p. (IS_PATH_WITH_REPLACEMENTS v w x /\ j < LENGTH v) ==> 2879 IS_PATH_WITH_REPLACEMENTS (CAT (SEL v (0, j), p)) (CAT (SEL w (0, j), p)) x``, 2880 2881 SIMP_TAC std_ss [IS_PATH_WITH_REPLACEMENTS_def] THEN 2882 REPEAT STRIP_TAC THENL [ 2883 Cases_on `p` THEN SIMP_TAC std_ss [LENGTH_CAT, LENGTH_SEL], 2884 2885 Cases_on `n <= j` THENL [ 2886 SUBGOAL_TAC `n < LENGTH v` THEN1 ( 2887 Cases_on `v` THEN Cases_on `w` THEN 2888 FULL_SIMP_TAC arith_ss [LENGTH_def, xnum_11, LS, xnum_distinct] 2889 ) THEN 2890 ASM_SIMP_TAC std_ss [ELEM_CAT_SEL___LESS_EQ], 2891 2892 ASM_SIMP_TAC arith_ss [ELEM_CAT_SEL___GREATER] 2893 ] 2894 ]); 2895 2896 2897val IS_PATH_WITH_REPLACEMENTS___RESTN = 2898 store_thm 2899 ("IS_PATH_WITH_REPLACEMENTS___RESTN", 2900 ``!v w x n. (n <= LENGTH v /\ IS_PATH_WITH_REPLACEMENTS v w x) ==> IS_PATH_WITH_REPLACEMENTS (RESTN v n) (RESTN w n) x``, 2901 2902 SIMP_TAC std_ss [IS_PATH_WITH_REPLACEMENTS_def, LENGTH_RESTN_THM_LE] THEN 2903 REPEAT STRIP_TAC THENL [ 2904 PROVE_TAC[LENGTH_RESTN_THM_LE], 2905 2906 REWRITE_TAC[ELEM_RESTN] THEN 2907 SUBGOAL_TAC `n' + n < LENGTH v` THEN1 ( 2908 Cases_on `v` THEN Cases_on `w` THEN 2909 FULL_SIMP_TAC arith_ss [LENGTH_def, LS, xnum_11, LE_num_xnum_def, SUB_xnum_num_def] 2910 ) THEN 2911 PROVE_TAC[] 2912 ]); 2913 2914 2915val SEL_IS_PATH_WITH_REPLACEMENTS = 2916 store_thm 2917 ("SEL_IS_PATH_WITH_REPLACEMENTS", 2918 2919 ``!v w x n m. (IS_PATH_WITH_REPLACEMENTS v w x /\ n < LENGTH v /\ m < LENGTH v) ==> 2920 IS_LIST_WITH_REPLACEMENTS (SEL v (n, m)) (SEL w (n, m)) x``, 2921 2922 SIMP_TAC list_ss [LENGTH_SEL, IS_PATH_WITH_REPLACEMENTS_def, IS_LIST_WITH_REPLACEMENTS_def] THEN 2923 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN 2924 Cases_on `m <= n` THENL [ 2925 SIMP_TAC std_ss [SEL_def] THEN 2926 `(m - n + 1 = SUC 0) /\ (n' = 0)` by DECIDE_TAC THEN 2927 ASM_REWRITE_TAC[SEL_REC_SUC, SEL_REC_def, EL, HD] THEN 2928 PROVE_TAC[], 2929 2930 `?k. n' + n = k` by PROVE_TAC[] THEN 2931 `(n' = k - n) /\ (n <= k) /\ (k <= m)` by DECIDE_TAC THEN 2932 ASM_SIMP_TAC std_ss [EL_SEL] THEN 2933 SUBGOAL_TAC `k < LENGTH v`THEN1 ( 2934 Cases_on `v` THEN Cases_on `w` THEN 2935 FULL_SIMP_TAC arith_ss [LENGTH_def, LS, xnum_11, xnum_distinct] 2936 ) THEN 2937 PROVE_TAC[] 2938 ]); 2939 2940 2941val IS_LIST_WITH_REPLACEMENTS___SUC = 2942 store_thm 2943 ("IS_LIST_WITH_REPLACEMENTS___SUC", 2944 2945 ``!l1 l2 x1 x2 x. IS_LIST_WITH_REPLACEMENTS (x1::l1) (x2::l2) x = 2946 (IS_LIST_WITH_REPLACEMENTS l1 l2 x /\ ((x1 = x2) \/ (x1 = x)))``, 2947 2948 SIMP_TAC list_ss [IS_LIST_WITH_REPLACEMENTS_def] THEN 2949 REPEAT GEN_TAC THEN 2950 Cases_on `(LENGTH l1 = LENGTH l2)` THEN ASM_REWRITE_TAC[] THEN 2951 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2952 `SUC n < SUC (LENGTH l2)` by DECIDE_TAC THEN 2953 RES_TAC THEN 2954 FULL_SIMP_TAC list_ss [], 2955 2956 `0 < SUC (LENGTH l2)` by DECIDE_TAC THEN 2957 RES_TAC THEN 2958 FULL_SIMP_TAC list_ss [], 2959 2960 Cases_on `n` THEN ASM_SIMP_TAC list_ss [], 2961 Cases_on `n` THEN ASM_SIMP_TAC list_ss [] 2962 ]); 2963 2964 2965 2966 2967val IS_LIST_WITH_REPLACEMENTS___APPEND = 2968 store_thm 2969 ("IS_LIST_WITH_REPLACEMENTS___APPEND", 2970 2971 ``!l l1 l2 l' l1' l2' x. ((l = l1 <> l2) /\ (l' = l1' <> l2') /\ (LENGTH l1 = LENGTH l1')) ==> 2972 (IS_LIST_WITH_REPLACEMENTS l l' x = 2973 (IS_LIST_WITH_REPLACEMENTS l1 l1' x /\ IS_LIST_WITH_REPLACEMENTS l2 l2' x))``, 2974 2975 REWRITE_TAC[IS_LIST_WITH_REPLACEMENTS_def] THEN 2976 REPEAT STRIP_TAC THEN 2977 ASM_SIMP_TAC list_ss [] THEN 2978 Cases_on `LENGTH l2 = LENGTH l2'` THEN ASM_REWRITE_TAC[] THEN 2979 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2980 `n < LENGTH l1' + LENGTH l2'` by DECIDE_TAC THEN 2981 METIS_TAC[EL_APPEND1], 2982 2983 `?k. k = LENGTH l1' + n` by PROVE_TAC[] THEN 2984 `(k - LENGTH l1' = n) /\ (LENGTH l1' <= k) /\ (k < LENGTH l1' + LENGTH l2')` by DECIDE_TAC THEN 2985 METIS_TAC[EL_APPEND2], 2986 2987 Cases_on `n < LENGTH l1'` THENL [ 2988 METIS_TAC[EL_APPEND1], 2989 2990 `?k. k = n - LENGTH l1'` by PROVE_TAC[] THEN 2991 `(LENGTH l1' <= n) /\ (k < LENGTH l2')` by DECIDE_TAC THEN 2992 METIS_TAC[EL_APPEND2] 2993 ] 2994 ]); 2995 2996 2997val IS_LIST_WITH_REPLACEMENTS___SEG = 2998 store_thm 2999 ("IS_LIST_WITH_REPLACEMENTS___SEG", 3000 3001 ``!x l l' n m. (n + m <= LENGTH l /\ IS_LIST_WITH_REPLACEMENTS l l' x) ==> 3002 (IS_LIST_WITH_REPLACEMENTS (SEG n m l) (SEG n m l') x)``, 3003 3004 REWRITE_TAC[IS_LIST_WITH_REPLACEMENTS_def] THEN 3005 SIMP_TAC list_ss [LENGTH_SEG, SEG_EL]); 3006 3007 3008val F_CLOCK_SERE_FREE___IS_TOP_BOTTOM_WELL_BEHAVED = 3009 store_thm 3010 ("F_CLOCK_SERE_FREE___IS_TOP_BOTTOM_WELL_BEHAVED", 3011 ``!f. (F_CLOCK_SERE_FREE f) ==> (IS_TOP_BOTTOM_WELL_BEHAVED f)``, 3012 3013 INDUCT_THEN fl_induct ASSUME_TAC THEN 3014 FULL_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, IS_TOP_BOTTOM_WELL_BEHAVED_def, F_CLOCK_FREE_def, F_SERE_FREE_def]); 3015 3016 3017(*********************************************************** 3018 * Important Lemmata 3019 ***********************************************************) 3020 3021val UF_SEM___F_CLOCK_SERE_FREE___OMEGA_TOP_BOTTOM = 3022 store_thm 3023 ("UF_SEM___F_CLOCK_SERE_FREE___OMEGA_TOP_BOTTOM", 3024 ``!f. (F_CLOCK_SERE_FREE f) ==> (UF_SEM TOP_OMEGA f /\ ~UF_SEM BOTTOM_OMEGA f)``, 3025 REWRITE_TAC[TOP_OMEGA_def, BOTTOM_OMEGA_def] THEN 3026 INDUCT_THEN fl_induct ASSUME_TAC THEN 3027 ASM_SIMP_TAC (arith_ss++res_quanTools.resq_SS) [F_CLOCK_SERE_FREE_def, UF_SEM_def, COMPLEMENT_def, F_CLOCK_FREE_def, F_SERE_FREE_def, 3028 B_SEM_def, ELEM_INFINITE, LENGTH_def, GT, xnum_distinct, o_DEF, COMPLEMENT_LETTER_def, RESTN_INFINITE, IN_LESSX]); 3029 3030 3031val UF_SEM___DIRECT___F_F = 3032 store_thm 3033 ("UF_SEM___DIRECT___F_F", 3034 ``!v f. (IS_PROPER_PATH v) ==> (UF_SEM v (F_F f) = ?k. k IN LESS (LENGTH v) /\ UF_SEM (RESTN v k) f)``, 3035 3036 SIMP_TAC (std_ss++resq_SS) [F_F_def, UF_SEM_def] THEN 3037 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 3038 METIS_TAC[], 3039 3040 FULL_SIMP_TAC arith_ss [IN_LESSX_REWRITE] THEN 3041 SIMP_TAC std_ss [ELEM_RESTN, IN_LESS] THEN 3042 Cases_on `ELEM v k = BOTTOM` THENL [ 3043 SUBGOAL_TAC `?j. (ELEM v j = BOTTOM) /\ !j'. j' < j ==> ~(ELEM v j' = BOTTOM)` THEN1 ( 3044 ASSUME_TAC (EXISTS_LEAST_CONV ``?j. ELEM v j = BOTTOM``) THEN 3045 PROVE_TAC[] 3046 ) THEN 3047 EXISTS_TAC ``j:num`` THEN 3048 `~(k < j)` by PROVE_TAC[] THEN 3049 `j < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3050 `IS_INFINITE_PROPER_PATH v` by PROVE_TAC[PROPER_PATH___IS_INFINITE_TOP_BOTTOM] THEN 3051 `(RESTN v j = BOTTOM_OMEGA)` by PROVE_TAC[INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA, LESS_EQ_REFL] THEN 3052 `(RESTN v k = BOTTOM_OMEGA)` by PROVE_TAC[INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA, LESS_EQ_REFL] THEN 3053 ASM_REWRITE_TAC[] THEN 3054 REPEAT STRIP_TAC THENL [ 3055 PROVE_TAC[], 3056 3057 DISJ2_TAC THEN 3058 Cases_on `ELEM v j'` THEN REWRITE_TAC[B_SEM_def] THEN 3059 PROVE_TAC[] 3060 ], 3061 3062 3063 EXISTS_TAC ``k:num`` THEN 3064 ASM_REWRITE_TAC[] THEN 3065 REPEAT STRIP_TAC THEN 3066 DISJ2_TAC THEN 3067 Cases_on `ELEM v j` THEN REWRITE_TAC[B_SEM_def] THEN 3068 `j < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3069 `IS_INFINITE_PROPER_PATH v` by PROVE_TAC[PROPER_PATH___IS_INFINITE_TOP_BOTTOM] THEN 3070 `k >= j` by DECIDE_TAC THEN 3071 PROVE_TAC[INFINITE_PROPER_PATH___TOP_BOTTOM_FOLLOWING] 3072 ] 3073 ]); 3074 3075 3076val UF_SEM___DIRECT___F_G = 3077 store_thm 3078 ("UF_SEM___DIRECT___F_G", 3079 ``!v f. (IS_PROPER_PATH v) ==> (UF_SEM v (F_G f) = !k. k IN LESS (LENGTH v) ==> UF_SEM (RESTN v k) f)``, 3080 3081 REWRITE_TAC[F_G_def, UF_SEM_def] THEN 3082 REPEAT STRIP_TAC THEN 3083 `IS_PROPER_PATH (COMPLEMENT v)` by PROVE_TAC[IS_PROPER_PATH___COMPLEMENT] THEN 3084 ASM_SIMP_TAC std_ss [LENGTH_COMPLEMENT, UF_SEM___DIRECT___F_F, IN_LESSX_REWRITE, 3085 UF_SEM_def, IMP_DISJ_THM] THEN 3086 METIS_TAC [RESTN_COMPLEMENT, COMPLEMENT_COMPLEMENT]); 3087 3088 3089 3090val PSL_WEAK_UNTIL___ALTERNATIVE_DEF = 3091 store_thm 3092 ("PSL_WEAK_UNTIL___ALTERNATIVE_DEF", 3093 ``!v f1 f2. IS_PROPER_PATH v ==> 3094 (UF_SEM v (F_WEAK_UNTIL(f1,f2)) = 3095 UF_SEM v (F_NOT (F_UNTIL(F_NOT f2, F_AND(F_NOT f1, F_NOT f2)))))``, 3096 3097 3098 SIMP_TAC (std_ss++resq_SS) [F_WEAK_UNTIL_def, F_W_def, UF_SEM_F_OR, IN_LESS, 3099 UF_SEM___DIRECT___F_G, IN_LESSX_REWRITE, UF_SEM_def, LENGTH_COMPLEMENT] THEN 3100 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 3101 Cases_on `k' < LENGTH v` THEN ASM_SIMP_TAC std_ss [] THEN 3102 ASM_SIMP_TAC std_ss [RESTN_COMPLEMENT, COMPLEMENT_COMPLEMENT] THEN 3103 Cases_on `UF_SEM (RESTN v k') f1` THEN ASM_REWRITE_TAC[] THEN 3104 `~(k' < k)` by PROVE_TAC[] THEN 3105 Cases_on `k = k'` THEN1 PROVE_TAC[] THEN 3106 `k < k'` by DECIDE_TAC THEN 3107 Cases_on `UF_SEM (RESTN v k') f2` THEN ASM_SIMP_TAC std_ss [] THEN 3108 EXISTS_TAC ``k:num`` THEN 3109 ASM_SIMP_TAC std_ss [RESTN_COMPLEMENT, COMPLEMENT_COMPLEMENT], 3110 3111 Cases_on `k < LENGTH v` THEN ASM_REWRITE_TAC[] THEN 3112 ASM_SIMP_TAC std_ss [RESTN_COMPLEMENT, COMPLEMENT_COMPLEMENT], 3113 3114 Cases_on `!k. k < LENGTH v ==> UF_SEM (RESTN v k) f1` THEN ASM_SIMP_TAC std_ss [] THEN 3115 FULL_SIMP_TAC std_ss [] THEN 3116 SUBGOAL_TAC `?k. (~UF_SEM (RESTN v k) f1 /\ k < LENGTH v) /\ 3117 !k'. k' < k ==> ~(~UF_SEM (RESTN v k') f1 /\ k' < LENGTH v)` THEN1 ( 3118 3119 ASSUME_TAC (EXISTS_LEAST_CONV ``?k. ~(UF_SEM (RESTN v k) f1) /\ (k < LENGTH v)``) THEN 3120 RES_TAC THEN 3121 EXISTS_TAC ``k':num`` THEN 3122 ASM_REWRITE_TAC[] 3123 ) THEN 3124 `!k'':num. k'' < k' ==> k'' < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3125 FULL_SIMP_TAC std_ss [] THEN 3126 Cases_on `UF_SEM (RESTN v k') f2` THEN1 METIS_TAC[] THEN 3127 `?j. j < k' /\ UF_SEM (RESTN v j) f2` by METIS_TAC[RESTN_COMPLEMENT, COMPLEMENT_COMPLEMENT] THEN 3128 EXISTS_TAC ``j:num`` THEN 3129 ASM_SIMP_TAC arith_ss [] 3130 ]); 3131 3132 3133 3134val US_SEM___S_CLOCK_FREE___OMEGA_BOTTOM = 3135 store_thm 3136 ("US_SEM___S_CLOCK_FREE___OMEGA_BOTTOM", 3137 ``!r l ls. (S_CLOCK_FREE r /\ IS_LIST_WITH_REPLACEMENTS ls l BOTTOM) ==> ( 3138 (US_SEM ls r ==> US_SEM l r))``, 3139 3140 REPEAT STRIP_TAC THEN 3141 Tactical.REVERSE (SUBGOAL_THEN ``l:'a letter list = ls`` ASSUME_TAC) THEN1 ( 3142 ASM_REWRITE_TAC[] 3143 ) THEN 3144 `BOTTOM_FREE ls` by PROVE_TAC[Lemma5] THEN 3145 FULL_SIMP_TAC std_ss [IS_LIST_WITH_REPLACEMENTS_def, LIST_EQ_REWRITE] THEN 3146 PROVE_TAC[BOTTOM_FREE_EL] 3147 ); 3148 3149 3150val US_SEM___S_CLOCK_FREE___OMEGA_TOP = 3151 store_thm 3152 ("US_SEM___S_CLOCK_FREE___OMEGA_TOP", 3153 ``!r l lw. (S_CLOCK_FREE r /\ IS_LIST_WITH_REPLACEMENTS lw l TOP) ==> ( 3154 (US_SEM l r ==> US_SEM lw r))``, 3155 3156 INDUCT_THEN sere_induct ASSUME_TAC THENL [ (* 8 subgoals *) 3157 SIMP_TAC std_ss [IS_LIST_WITH_REPLACEMENTS_def, S_CLOCK_FREE_def, US_SEM_def] THEN 3158 REPEAT STRIP_TAC THEN 3159 `0 < LENGTH lw` by DECIDE_TAC THEN 3160 `(EL 0 lw = EL 0 l) \/ (EL 0 lw = TOP)` by PROVE_TAC[] THENL [ 3161 FULL_SIMP_TAC std_ss [ELEM_EL], 3162 ASM_SIMP_TAC std_ss [ELEM_EL, B_SEM_def] 3163 ], 3164 3165 3166 SIMP_TAC std_ss [S_CLOCK_FREE_def, US_SEM_def] THEN 3167 REPEAT STRIP_TAC THEN 3168 `?vw1. FIRSTN (LENGTH v1) lw = vw1` by PROVE_TAC[] THEN 3169 `?vw2. LASTN (LENGTH v2) lw = vw2` by PROVE_TAC[] THEN 3170 `LENGTH lw = LENGTH v1 + LENGTH v2` by PROVE_TAC[LENGTH_APPEND, IS_LIST_WITH_REPLACEMENTS_def] THEN 3171 `lw = vw1 <> vw2` by PROVE_TAC[APPEND_FIRSTN_LASTN, ADD_COMM] THEN 3172 EXISTS_TAC ``vw1:'a letter list`` THEN 3173 EXISTS_TAC ``vw2:'a letter list`` THEN 3174 ASM_REWRITE_TAC[] THEN 3175 `LENGTH v1 <= LENGTH lw` by DECIDE_TAC THEN 3176 `LENGTH v1 = LENGTH vw1` by PROVE_TAC[LENGTH_FIRSTN] THEN 3177 PROVE_TAC[IS_LIST_WITH_REPLACEMENTS___APPEND], 3178 3179 3180 SIMP_TAC list_ss [S_CLOCK_FREE_def, US_SEM_def] THEN 3181 REPEAT STRIP_TAC THEN 3182 `?vw1. vw1 = FIRSTN (LENGTH v1) lw` by PROVE_TAC[] THEN 3183 `?vw2. vw2 = LASTN (LENGTH v2) lw` by PROVE_TAC[] THEN 3184 `?lw'. lw' = EL (LENGTH v1) lw` by PROVE_TAC[] THEN 3185 EXISTS_TAC ``vw1:'a letter list`` THEN 3186 EXISTS_TAC ``vw2:'a letter list`` THEN 3187 EXISTS_TAC ``lw':'a letter`` THEN 3188 `?vw1'. vw1' = FIRSTN (SUC (LENGTH v1)) lw` by PROVE_TAC[] THEN 3189 `?v1'. v1' = v1 <> [l']` by PROVE_TAC[] THEN 3190 `LENGTH l = SUC (LENGTH v1) + LENGTH v2` by ASM_SIMP_TAC list_ss [] THEN 3191 `LENGTH lw = SUC (LENGTH v1) + LENGTH v2` by PROVE_TAC[IS_LIST_WITH_REPLACEMENTS_def] THEN 3192 SUBGOAL_THEN ``(vw1':'a letter list) = vw1 <> [lw']`` ASSUME_TAC THEN1( 3193 ASM_SIMP_TAC list_ss [FIRSTN_SEG, SEG_SPLIT, SUC_ONE_ADD] THEN 3194 `(1:num > 0:num) /\ (LENGTH v1 < LENGTH lw)` by DECIDE_TAC THEN 3195 `SEG 1 (LENGTH v1) lw = [HD (SEG 1 (LENGTH v1) lw)]` by PROVE_TAC[SEG_SING_LIST] THEN 3196 ONCE_ASM_REWRITE_TAC[] THEN 3197 ASM_SIMP_TAC list_ss [GSYM EL_SEG] 3198 ) THEN 3199 3200 `vw1' <> vw2 = lw` by PROVE_TAC[APPEND_FIRSTN_LASTN, ADD_COMM] THEN 3201 STRIP_TAC THENL [ 3202 PROVE_TAC[], 3203 3204 `LENGTH v1' = SUC (LENGTH v1)` by ASM_SIMP_TAC list_ss [] THEN 3205 `LENGTH v1' <= LENGTH lw` by DECIDE_TAC THEN 3206 `LENGTH v1' = LENGTH vw1'` by ASM_SIMP_TAC list_ss [LENGTH_FIRSTN] THEN 3207 `l = v1' <> v2` by PROVE_TAC[] THEN 3208 3209 `(IS_LIST_WITH_REPLACEMENTS vw1' v1' TOP /\ IS_LIST_WITH_REPLACEMENTS vw2 v2 TOP)` by 3210 PROVE_TAC[IS_LIST_WITH_REPLACEMENTS___APPEND] THEN 3211 REPEAT STRIP_TAC THENL [ 3212 PROVE_TAC[], 3213 3214 SUBGOAL_TAC `IS_LIST_WITH_REPLACEMENTS (lw'::vw2) (l'::v2) TOP` THEN1 ( 3215 ASM_SIMP_TAC list_ss [IS_LIST_WITH_REPLACEMENTS___SUC] THEN 3216 `l' = EL(LENGTH v1) l` by 3217 ASM_SIMP_TAC arith_ss [EL_APPEND2, GSYM APPEND_ASSOC, EL, HD, APPEND] THEN 3218 `LENGTH v1 < LENGTH lw` by DECIDE_TAC THEN 3219 PROVE_TAC [IS_LIST_WITH_REPLACEMENTS_def] 3220 ) THEN 3221 PROVE_TAC[] 3222 ] 3223 ], 3224 3225 3226 SIMP_TAC std_ss [S_CLOCK_FREE_def, US_SEM_def] THEN PROVE_TAC[], 3227 SIMP_TAC std_ss [S_CLOCK_FREE_def, US_SEM_def] THEN PROVE_TAC[], 3228 SIMP_TAC list_ss [IS_LIST_WITH_REPLACEMENTS_def, LENGTH_NIL, S_CLOCK_FREE_def, US_SEM_def], 3229 3230 SIMP_TAC list_ss [S_CLOCK_FREE_def, US_SEM_def] THEN 3231 REPEAT STRIP_TAC THEN 3232 NTAC 3 (fn (asm, g) => UNDISCH_TAC (hd asm) (asm, g)) THEN 3233 SPEC_TAC (``l:'a letter list``, ``l:'a letter list``) THEN 3234 SPEC_TAC (``lw:'a letter list``, ``lw:'a letter list``) THEN 3235 Induct_on `vlist` THENL [ 3236 SIMP_TAC list_ss [] THEN 3237 REPEAT STRIP_TAC THEN 3238 EXISTS_TAC ``[]:'a letter list list`` THEN 3239 FULL_SIMP_TAC list_ss [CONCAT_def, IS_LIST_WITH_REPLACEMENTS_def, LENGTH_NIL], 3240 3241 SIMP_TAC list_ss [CONCAT_def] THEN 3242 REPEAT STRIP_TAC THEN 3243 `?hw. FIRSTN (LENGTH h) lw = hw` by PROVE_TAC[] THEN 3244 `?lw'. BUTFIRSTN (LENGTH h) lw = lw'` by PROVE_TAC[] THEN 3245 `LENGTH lw = (LENGTH h + LENGTH (CONCAT vlist))` by FULL_SIMP_TAC list_ss [IS_LIST_WITH_REPLACEMENTS_def] THEN 3246 `LENGTH h <= LENGTH lw` by DECIDE_TAC THEN 3247 `hw <> lw' = lw` by PROVE_TAC[APPEND_FIRSTN_BUTFIRSTN] THEN 3248 `LENGTH hw = LENGTH h` by PROVE_TAC [LENGTH_FIRSTN] THEN 3249 `IS_LIST_WITH_REPLACEMENTS lw' (CONCAT vlist) TOP /\ 3250 IS_LIST_WITH_REPLACEMENTS hw h TOP` by 3251 PROVE_TAC [IS_LIST_WITH_REPLACEMENTS___APPEND] THEN 3252 `?vlist'. (lw' = CONCAT vlist') /\ ALL_EL (\v'. US_SEM v' r) vlist'` by 3253 PROVE_TAC[] THEN 3254 EXISTS_TAC ``(hw::vlist'):'a letter list list`` THEN 3255 ASM_SIMP_TAC list_ss [] THEN 3256 PROVE_TAC[CONCAT_def] 3257 ], 3258 3259 REWRITE_TAC[S_CLOCK_FREE_def] 3260 ]); 3261 3262 3263val UF_SEM___F_CLOCK_FREE___OMEGA_TOP_BOTTOM = 3264 store_thm 3265 ("UF_SEM___F_CLOCK_FREE___OMEGA_TOP_BOTTOM", 3266 ``!f v vw vs. 3267 ((F_CLOCK_FREE f /\ IS_PATH_WITH_REPLACEMENTS vw v TOP /\ UF_SEM v f) ==> UF_SEM vw f) /\ 3268 ((F_CLOCK_FREE f /\ IS_PATH_WITH_REPLACEMENTS vs v BOTTOM /\ UF_SEM vs f) ==> UF_SEM v f)``, 3269 3270 INDUCT_THEN fl_induct ASSUME_TAC THENL [ 3271 3272 ASM_SIMP_TAC list_ss [IS_PATH_WITH_REPLACEMENTS_def, F_CLOCK_FREE_def, UF_SEM_def] THEN 3273 REPEAT STRIP_TAC THENL [ 3274 Cases_on `(ELEM vw 0) = (ELEM v 0)` THEN ASM_REWRITE_TAC[] THEN 3275 `ELEM vw 0 = TOP` by PROVE_TAC[GT_LS] THEN 3276 ASM_SIMP_TAC std_ss [B_SEM_def], 3277 3278 PROVE_TAC[], 3279 3280 Cases_on `(ELEM v 0) = (ELEM vs 0)` THEN ASM_REWRITE_TAC[] THEN 3281 `ELEM vs 0 = BOTTOM` by PROVE_TAC[GT_LS] THEN 3282 PROVE_TAC [B_SEM_def] 3283 ], 3284 3285 ASM_SIMP_TAC std_ss [IS_PATH_WITH_REPLACEMENTS_def, F_CLOCK_FREE_def, UF_SEM_def] THEN 3286 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 3287 Cases_on `LENGTH v = XNUM 0` THEN ASM_REWRITE_TAC[] THEN 3288 `0 < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, xnum_11]) THENL [ 3289 Cases_on `(ELEM vw 0) = (ELEM v 0)` THEN ASM_REWRITE_TAC[] THEN 3290 `ELEM vw 0 = TOP` by PROVE_TAC[] THEN 3291 ASM_SIMP_TAC std_ss [B_SEM_def], 3292 3293 PROVE_TAC[], 3294 3295 Cases_on `(ELEM v 0) = (ELEM vs 0)` THEN ASM_REWRITE_TAC[] THEN 3296 `ELEM vs 0 = BOTTOM` by PROVE_TAC[] THEN 3297 PROVE_TAC [B_SEM_def] 3298 ], 3299 3300 3301 SIMP_TAC std_ss [F_CLOCK_FREE_def, UF_SEM_def] THEN 3302 ONCE_REWRITE_TAC[IS_PATH_WITH_REPLACEMENTS___COMPLEMENT] THEN 3303 SIMP_TAC std_ss [COMPLEMENT_LETTER_def] THEN 3304 PROVE_TAC[], 3305 3306 3307 SIMP_TAC std_ss [F_CLOCK_FREE_def, UF_SEM_def] THEN PROVE_TAC[], 3308 3309 3310 ASM_SIMP_TAC (list_ss++resq_SS) [IN_LESSX_REWRITE, F_CLOCK_FREE_def, UF_SEM_def] THEN 3311 REPEAT STRIP_TAC THENL [ 3312 EXISTS_TAC ``j:num`` THEN 3313 `?l. (SEL v (0,j)) = l` by PROVE_TAC[] THEN 3314 `?lw. (SEL vw (0,j)) = lw` by PROVE_TAC[] THEN 3315 `LENGTH vw = LENGTH v` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3316 ASM_REWRITE_TAC[] THEN 3317 `0 < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3318 `IS_LIST_WITH_REPLACEMENTS lw l TOP` by PROVE_TAC[SEL_IS_PATH_WITH_REPLACEMENTS] THEN 3319 PROVE_TAC[US_SEM___S_CLOCK_FREE___OMEGA_TOP], 3320 3321 EXISTS_TAC ``j:num`` THEN 3322 `?l. (SEL v (0,j)) = l` by PROVE_TAC[] THEN 3323 `?ls. (SEL vs (0,j)) = ls` by PROVE_TAC[] THEN 3324 `LENGTH v = LENGTH vs` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3325 ASM_REWRITE_TAC[] THEN 3326 `0 < LENGTH vs` by (Cases_on `vs` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3327 `IS_LIST_WITH_REPLACEMENTS ls l BOTTOM` by PROVE_TAC[SEL_IS_PATH_WITH_REPLACEMENTS] THEN 3328 PROVE_TAC[US_SEM___S_CLOCK_FREE___OMEGA_BOTTOM] 3329 ], 3330 3331 3332 ASM_SIMP_TAC (list_ss++resq_SS) [IN_LESSX_REWRITE, LENGTH_CAT, TOP_OMEGA_def, F_CLOCK_FREE_def, UF_SEM_def, LS] THEN 3333 REWRITE_TAC [GSYM TOP_OMEGA_def] THEN 3334 REPEAT STRIP_TAC THENL [ 3335 `LENGTH v = LENGTH vw` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3336 `?k. US_SEM (SEL (CAT (SEL v (0,j),TOP_OMEGA)) (0,k)) s` by PROVE_TAC[] THEN 3337 3338 `?vw'. CAT (SEL vw (0,j),TOP_OMEGA) = vw'` by PROVE_TAC[] THEN 3339 `?v'. CAT (SEL v (0,j),TOP_OMEGA) = v'` by PROVE_TAC[] THEN 3340 `IS_PATH_WITH_REPLACEMENTS vw' v' TOP` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___CAT_SEL] THEN 3341 3342 EXISTS_TAC ``k:num`` THEN 3343 `?l. (SEL v' (0,k)) = l` by PROVE_TAC[] THEN 3344 `?lw. (SEL vw' (0,k)) = lw` by PROVE_TAC[] THEN 3345 `0 < LENGTH v` by (Cases_on `v` THEN Cases_on `vw` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3346 `LENGTH vw' = INFINITY` by PROVE_TAC[LENGTH_CAT, TOP_OMEGA_def] THEN 3347 `IS_LIST_WITH_REPLACEMENTS lw l TOP` by METIS_TAC[SEL_IS_PATH_WITH_REPLACEMENTS, LS] THEN 3348 PROVE_TAC[US_SEM___S_CLOCK_FREE___OMEGA_TOP], 3349 3350 3351 `LENGTH vs = LENGTH v` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3352 `?k. US_SEM (SEL (CAT (SEL vs (0,j),TOP_OMEGA)) (0,k)) s` by PROVE_TAC[] THEN 3353 3354 `?vs'. CAT (SEL vs (0,j),TOP_OMEGA) = vs'` by PROVE_TAC[] THEN 3355 `?v'. CAT (SEL v (0,j),TOP_OMEGA) = v'` by PROVE_TAC[] THEN 3356 `IS_PATH_WITH_REPLACEMENTS vs' v' BOTTOM` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___CAT_SEL] THEN 3357 3358 EXISTS_TAC ``k:num`` THEN 3359 `?l. (SEL v' (0,k)) = l` by PROVE_TAC[] THEN 3360 `?ls. (SEL vs' (0,k)) = ls` by PROVE_TAC[] THEN 3361 `0 < LENGTH v` by (Cases_on `v` THEN Cases_on `vs` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3362 `LENGTH vs' = INFINITY` by PROVE_TAC[LENGTH_CAT, TOP_OMEGA_def] THEN 3363 `IS_LIST_WITH_REPLACEMENTS ls l BOTTOM` by METIS_TAC[SEL_IS_PATH_WITH_REPLACEMENTS, LS] THEN 3364 PROVE_TAC[US_SEM___S_CLOCK_FREE___OMEGA_BOTTOM] 3365 ], 3366 3367 3368 SIMP_TAC std_ss [F_CLOCK_FREE_def, UF_SEM_def] THEN 3369 REPEAT STRIP_TAC THENL [ 3370 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def], 3371 3372 `(LENGTH vw = LENGTH v)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3373 `1 <= LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, LE_num_xnum_def, GT]) THEN 3374 METIS_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN], 3375 3376 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def], 3377 3378 `(LENGTH vs = LENGTH v)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3379 `1 <= LENGTH vs` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, LE_num_xnum_def, GT]) THEN 3380 METIS_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN] 3381 ], 3382 3383 3384 SIMP_TAC (list_ss++resq_SS) [IN_LESSX_REWRITE, F_CLOCK_FREE_def, UF_SEM_def, IN_LESS] THEN 3385 REPEAT STRIP_TAC THENL [ 3386 3387 EXISTS_TAC ``k:num`` THEN 3388 `(LENGTH vw = LENGTH v)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3389 ASM_REWRITE_TAC [] THEN 3390 `k <= LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LE_num_xnum_def, LS]) THEN 3391 REPEAT STRIP_TAC THENL [ 3392 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN], 3393 3394 `j <= LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, LE_num_xnum_def]) THEN 3395 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN] 3396 ], 3397 3398 3399 EXISTS_TAC ``k:num`` THEN 3400 `(LENGTH v = LENGTH vs)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3401 `k <= LENGTH vs` by (Cases_on `vs` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, LE_num_xnum_def]) THEN 3402 ASM_REWRITE_TAC [] THEN 3403 REPEAT STRIP_TAC THENL [ 3404 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN], 3405 3406 `j <= LENGTH vs` by (Cases_on `vs` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, LE_num_xnum_def]) THEN 3407 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN] 3408 ] 3409 ], 3410 3411 3412 3413 SIMP_TAC (list_ss++resq_SS) [IN_LESSX_REWRITE, F_CLOCK_FREE_def, UF_SEM_def, IN_LESS] THEN 3414 REPEAT STRIP_TAC THENL [ 3415 PROVE_TAC[], 3416 3417 DISJ2_TAC THEN 3418 EXISTS_TAC ``j:num`` THEN 3419 `(LENGTH vw = LENGTH v)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3420 REPEAT STRIP_TAC THENL [ 3421 ASM_REWRITE_TAC[], 3422 3423 `(ELEM vw j = ELEM v j) \/ (ELEM vw j = TOP)` by 3424 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3425 ASM_REWRITE_TAC [B_SEM_def], 3426 3427 Cases_on `j = 0` THEN FULL_SIMP_TAC std_ss [] THEN 3428 `j - 1 < LENGTH vw` by (Cases_on `vw` THEN Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3429 METIS_TAC [IS_PATH_WITH_REPLACEMENTS___CAT_SEL] 3430 ], 3431 3432 PROVE_TAC[], 3433 3434 DISJ2_TAC THEN 3435 EXISTS_TAC ``j:num`` THEN 3436 `(LENGTH v = LENGTH vs)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3437 REPEAT STRIP_TAC THENL [ 3438 ASM_REWRITE_TAC[], 3439 3440 `(ELEM v j = ELEM vs j) \/ (ELEM vs j = BOTTOM)` by 3441 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3442 FULL_SIMP_TAC std_ss [B_SEM_def], 3443 3444 Cases_on `j = 0` THEN FULL_SIMP_TAC std_ss [] THEN 3445 `j - 1 < LENGTH vs` by (Cases_on `vs` THEN Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3446 METIS_TAC [IS_PATH_WITH_REPLACEMENTS___CAT_SEL] 3447 ] 3448 ], 3449 3450 3451 ASM_REWRITE_TAC[F_CLOCK_FREE_def], 3452 3453 3454 3455 3456 SIMP_TAC (list_ss++resq_SS) [IN_LESSX_REWRITE, F_CLOCK_FREE_def, UF_SEM_def, IN_LESS] THEN 3457 REPEAT STRIP_TAC THENL [ 3458 `(LENGTH vw = LENGTH v)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3459 `IS_PATH_WITH_REPLACEMENTS (COMPLEMENT vw) (COMPLEMENT v) BOTTOM` by 3460 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___COMPLEMENT, COMPLEMENT_LETTER_def] THEN 3461 `?l. (SEL (COMPLEMENT v) (0, j)) = l` by PROVE_TAC[] THEN 3462 `?ls. (SEL (COMPLEMENT vw) (0, j)) = ls` by PROVE_TAC[] THEN 3463 `0 < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LS, LENGTH_def]) THEN 3464 `IS_LIST_WITH_REPLACEMENTS ls l BOTTOM` by PROVE_TAC[SEL_IS_PATH_WITH_REPLACEMENTS, LENGTH_COMPLEMENT] THEN 3465 `US_SEM l p_1` by PROVE_TAC[US_SEM___S_CLOCK_FREE___OMEGA_BOTTOM] THEN 3466 `UF_SEM (RESTN v j) f` by PROVE_TAC[] THEN 3467 `j <= LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LS, LENGTH_def, LE_num_xnum_def]) THEN 3468 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN], 3469 3470 3471 `(LENGTH vs = LENGTH v)` by PROVE_TAC[IS_PATH_WITH_REPLACEMENTS_def] THEN 3472 `IS_PATH_WITH_REPLACEMENTS (COMPLEMENT vs) (COMPLEMENT v) TOP` by 3473 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___COMPLEMENT, COMPLEMENT_LETTER_def] THEN 3474 `?l. (SEL (COMPLEMENT v) (0, j)) = l` by PROVE_TAC[] THEN 3475 `?lw. (SEL (COMPLEMENT vs) (0, j)) = lw` by PROVE_TAC[] THEN 3476 `0 < LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS]) THEN 3477 `IS_LIST_WITH_REPLACEMENTS lw l TOP` by PROVE_TAC[SEL_IS_PATH_WITH_REPLACEMENTS, LENGTH_COMPLEMENT] THEN 3478 `US_SEM lw p_1` by PROVE_TAC[US_SEM___S_CLOCK_FREE___OMEGA_TOP] THEN 3479 `UF_SEM (RESTN vs j) f` by PROVE_TAC[] THEN 3480 `j <= LENGTH v` by (Cases_on `v` THEN FULL_SIMP_TAC arith_ss [LENGTH_def, LS, LE_num_xnum_def]) THEN 3481 PROVE_TAC[IS_PATH_WITH_REPLACEMENTS___RESTN] 3482 ] 3483 ]); 3484 3485 3486 3487val PSL_WITH_SERES___STRICTLY_MORE_EXPRESSIVE_THAN___LTL___EXAMPLE = 3488 store_thm 3489 ("PSL_WITH_SERES___STRICTLY_MORE_EXPRESSIVE_THAN___LTL___EXAMPLE", 3490 ``!v p q. (!n:num. (n < LENGTH v) ==> (?s. (ELEM v n) = STATE s)) ==> 3491 3492 ((UF_SEM v (F_AND(F_SUFFIX_IMP (S_REPEAT(S_CAT(S_BOOL p, S_BOOL q)), 3493 F_NEXT(F_AND(F_STRONG_BOOL p, F_NEXT (F_STRONG_BOOL q)))), 3494 3495 F_AND(F_STRONG_BOOL p, F_NEXT (F_STRONG_BOOL q))))) = 3496 (!n:num. (LENGTH v > 2*n+1 /\ US_SEM (SEL v (0, 2*n+1)) (S_REPEAT 3497 (S_CAT (S_BOOL p,S_BOOL q)))) /\ 3498 B_SEM (ELEM v (n+n)) p /\ B_SEM (ELEM v (n+n+1)) q))``, 3499 3500 REPEAT STRIP_TAC THEN 3501 SUBGOAL_THEN ``COMPLEMENT v = v`` ASSUME_TAC THEN1 ( 3502 Cases_on `v` THEN 3503 REWRITE_TAC [COMPLEMENT_def, path_11] THENL [ 3504 Induct_on `l` THENL [ 3505 REWRITE_TAC [MAP], 3506 3507 FULL_SIMP_TAC list_ss [LENGTH_def, LS] THEN 3508 REPEAT STRIP_TAC THENL [ 3509 `ELEM (FINITE (h::l)) 0 = h` by SIMP_TAC list_ss [ELEM_FINITE] THEN 3510 `0 < SUC (LENGTH l)` by DECIDE_TAC THEN 3511 `?s. h = STATE s` by METIS_TAC[] THEN 3512 ASM_REWRITE_TAC[COMPLEMENT_LETTER_def], 3513 3514 `!n. ELEM (FINITE l) n = (ELEM (FINITE (h::l)) (SUC n))` by SIMP_TAC list_ss [ELEM_FINITE] THEN 3515 `!n. n < LENGTH l ==> SUC n < SUC (LENGTH l)` by DECIDE_TAC THEN 3516 PROVE_TAC[] 3517 ] 3518 ], 3519 3520 FULL_SIMP_TAC list_ss [LENGTH_def, LS, ELEM_INFINITE, FUN_EQ_THM, COMPLEMENT_def, o_DEF, path_11] THEN 3521 PROVE_TAC[COMPLEMENT_LETTER_def] 3522 ] 3523 ) THEN 3524 3525 EQ_TAC THENL [ 3526 FULL_SIMP_TAC (list_ss++resq_SS) [US_SEM_def, RESTN_RESTN, UF_SEM_def] THEN 3527 DISCH_TAC THEN 3528 FULL_SIMP_TAC std_ss [] THEN 3529 Induct_on `n` THENL [ 3530 FULL_SIMP_TAC arith_ss [ELEM_RESTN] THEN 3531 3532 EXISTS_TAC ``[SEL v (0, 1)]:'a letter list list`` THEN 3533 SIMP_TAC arith_ss [CONCAT_def, APPEND_NIL, ALL_EL] THEN 3534 EXISTS_TAC ``[(ELEM v 0)]:'a letter list`` THEN 3535 EXISTS_TAC ``[(ELEM v 1)]:'a letter list`` THEN 3536 `(ELEM [ELEM v 0] 0) = ELEM v 0` by (EVAL_TAC THEN PROVE_TAC[]) THEN 3537 `(ELEM [ELEM v 1] 0) = ELEM v 1` by (EVAL_TAC THEN PROVE_TAC[]) THEN 3538 ASM_SIMP_TAC list_ss [SEL_def] THEN 3539 `(2 = SUC (SUC 0)) /\ (1 = SUC 0)` by DECIDE_TAC THEN 3540 ONCE_ASM_REWRITE_TAC[] THEN 3541 SIMP_TAC list_ss [SEL_REC_def, ELEM_def, RESTN_def], 3542 3543 3544 3545 FULL_SIMP_TAC std_ss [] THEN 3546 SUBGOAL_THEN ``((2*n + 1) IN LESS (LENGTH (v:'a letter path)))`` ASSUME_TAC THEN1 ( 3547 Cases_on `v` THENL [ 3548 FULL_SIMP_TAC arith_ss [LENGTH_def, IN_LESSX, GT], 3549 SIMP_TAC std_ss [IN_LESSX, LENGTH_def] 3550 ] 3551 ) THEN 3552 RES_TAC THEN 3553 FULL_SIMP_TAC arith_ss [ELEM_RESTN] THEN 3554 REPEAT STRIP_TAC THENL [ 3555 Cases_on `v` THENL [ 3556 SUBGOAL_THEN ``2 * n + 2 < LENGTH (FINITE l:'a letter path)`` ASSUME_TAC THEN1 ( 3557 `LENGTH (RESTN (FINITE l) (2 * n + 1)) = LENGTH (FINITE l) - (2 * n + 1)` by 3558 METIS_TAC[GT_LS, LENGTH_RESTN, IS_FINITE_def] THEN 3559 FULL_SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, GT, LS] 3560 ) THEN 3561 3562 `LENGTH (RESTN (FINITE l) (2 * n + 2)) = LENGTH (FINITE l) - (2 * n + 2)` by 3563 METIS_TAC[LENGTH_RESTN, IS_FINITE_def] THEN 3564 FULL_SIMP_TAC arith_ss [LENGTH_def, SUB_xnum_num_def, GT, LS] THEN 3565 DECIDE_TAC, 3566 3567 SIMP_TAC std_ss [GT, LENGTH_def] 3568 ], 3569 3570 EXISTS_TAC ``(vlist:'a letter list list)<>[SEL v (2*SUC n, 2*SUC n + 1)]`` THEN 3571 REPEAT STRIP_TAC THENL [ 3572 SIMP_TAC list_ss [CONCAT_APPEND, CONCAT_def] THEN 3573 `0 <= 2 * n + 1 /\ 2 * n + 1 < 2* (SUC n)+1` by DECIDE_TAC THEN 3574 `SEL v (0, 2* SUC n + 1) = SEL v (0, 2* n + 1) <> SEL v (2* n + 1 + 1, 2 * (SUC n)+1)` by 3575 METIS_TAC[SEL_SPLIT] THEN 3576 `2 * n + 1 + 1 = 2 * (SUC n)` by DECIDE_TAC THEN 3577 ASM_REWRITE_TAC[], 3578 3579 ASM_SIMP_TAC list_ss [] THEN 3580 EXISTS_TAC ``[(ELEM v (2*SUC n))]:'a letter list`` THEN 3581 EXISTS_TAC ``[(ELEM v (2*(SUC n) + 1))]:'a letter list`` THEN 3582 `(ELEM [ELEM v (2*SUC n)] 0) = ELEM v (2*SUC n)` by (EVAL_TAC THEN PROVE_TAC[]) THEN 3583 `(ELEM [ELEM v (2*SUC n+1)] 0) = ELEM v (2*SUC n+1)` by (EVAL_TAC THEN PROVE_TAC[]) THEN 3584 ASM_SIMP_TAC list_ss [SEL_def] THEN 3585 `(2*SUC n = 2*n + 2) /\ (2*SUC n +1 = 2*n + 3)` by DECIDE_TAC THEN 3586 ASM_REWRITE_TAC[] THEN 3587 `2 = SUC (SUC 0)` by DECIDE_TAC THEN 3588 ONCE_ASM_REWRITE_TAC[] THEN 3589 SIMP_TAC list_ss [SEL_REC_def, SEL_REC_SUC, ELEM_def] THEN 3590 `2 * n + 3 = SUC (2 * n + 2)` by DECIDE_TAC THEN 3591 ASM_REWRITE_TAC[RESTN_def] 3592 ], 3593 3594 `2*(SUC n) = 2*n+2` by DECIDE_TAC THEN 3595 ASM_REWRITE_TAC[], 3596 3597 `2*(SUC n)+1 = 2*n + 3` by DECIDE_TAC THEN 3598 ASM_REWRITE_TAC[] 3599 ] 3600 ], 3601 3602 SIMP_TAC std_ss [FORALL_AND_THM] THEN 3603 REPEAT STRIP_TAC THEN 3604 SUBGOAL_THEN ``?v'. (v:'a letter path) = INFINITE v'`` STRIP_ASSUME_TAC THEN1 ( 3605 Cases_on `v` THENL [ 3606 FULL_SIMP_TAC arith_ss [LENGTH_def, GT] THEN 3607 `LENGTH l > 2*(LENGTH l) + 1` by PROVE_TAC[] THEN 3608 FULL_SIMP_TAC arith_ss [], 3609 3610 PROVE_TAC[] 3611 ] 3612 ) THEN 3613 3614 FULL_SIMP_TAC (arith_ss++resq_SS) [UF_SEM_def, RESTN_INFINITE, LENGTH_def, GT, IN_LESSX, ELEM_INFINITE, 3615 US_SEM_def] THEN 3616 Tactical.REVERSE (STRIP_TAC) THEN1 ( 3617 `(2*0 = 0:num) /\ (2*0 + 1 = 1:num)` by SIMP_TAC arith_ss [] THEN 3618 METIS_TAC[] 3619 ) THEN 3620 3621 GEN_TAC THEN DISCH_TAC THEN 3622 FULL_SIMP_TAC std_ss [] THEN 3623 Tactical.REVERSE (SUBGOAL_THEN ``ODD j`` ASSUME_TAC) THEN1 ( 3624 FULL_SIMP_TAC arith_ss [ODD_EXISTS] THEN 3625 `(j + 1= 2 * (SUC m)) /\ (j + 2 = (2*SUC m) + 1)` by DECIDE_TAC THEN 3626 PROVE_TAC[] 3627 ) THEN 3628 3629 SUBGOAL_THEN ``LENGTH (CONCAT vlist) = 2 * LENGTH (vlist:'a letter list list)`` ASSUME_TAC THEN1 ( 3630 (fn (asm, g) => UNDISCH_TAC (hd asm) (asm, g)) THEN 3631 WEAKEN_TAC (fn f => true) THEN 3632 Induct_on `vlist` THENL [ 3633 SIMP_TAC list_ss [CONCAT_def], 3634 3635 SIMP_TAC list_ss [CONCAT_def] THEN 3636 REPEAT STRIP_TAC THEN 3637 RES_TAC THEN 3638 ASM_SIMP_TAC list_ss [] 3639 ] 3640 ) THEN 3641 3642 `LENGTH (SEL (INFINITE v') (0, j)) = 2* (LENGTH vlist)` by PROVE_TAC[] THEN 3643 FULL_SIMP_TAC list_ss [LENGTH_SEL] THEN 3644 3645 `?m:num. LENGTH vlist = m` by PROVE_TAC[] THEN 3646 `(m > 0) /\ (j = (2 * m) - 1)` by DECIDE_TAC THEN 3647 REWRITE_TAC [ODD_EXISTS] THEN 3648 EXISTS_TAC ``PRE (m:num)`` THEN 3649 ASM_SIMP_TAC arith_ss [] 3650 ]); 3651 3652 3653 3654val IS_TOP_BOTTOM_WELL_BEHAVED_THM = 3655 store_thm 3656 ("IS_TOP_BOTTOM_WELL_BEHAVED_THM", 3657 ``!f. (IS_TOP_BOTTOM_WELL_BEHAVED f /\ F_CLOCK_FREE f) ==> 3658 ((UF_SEM TOP_OMEGA f) /\ ~(UF_SEM BOTTOM_OMEGA f))``, 3659 3660 INDUCT_THEN fl_induct ASSUME_TAC THENL [ 3661 SIMP_TAC std_ss [TOP_OMEGA_def, BOTTOM_OMEGA_def, UF_SEM_def, ELEM_INFINITE, B_SEM_def, LENGTH_def, GT], 3662 SIMP_TAC std_ss [TOP_OMEGA_def, BOTTOM_OMEGA_def, UF_SEM_def, ELEM_INFINITE, B_SEM_def, LENGTH_def, xnum_distinct], 3663 ASM_SIMP_TAC std_ss [TOP_BOTTOM_OMEGA___COMPLEMENT, IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, F_CLOCK_FREE_def], 3664 ASM_SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, F_CLOCK_FREE_def], 3665 ASM_SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def], 3666 ASM_SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def], 3667 3668 FULL_SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, F_CLOCK_FREE_def, TOP_OMEGA_def, BOTTOM_OMEGA_def, 3669 LENGTH_def, RESTN_INFINITE, GT], 3670 FULL_SIMP_TAC (std_ss++resq_SS) [IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, F_CLOCK_FREE_def, TOP_OMEGA_def, BOTTOM_OMEGA_def, 3671 LENGTH_def, RESTN_INFINITE, GT, IN_LESSX], 3672 3673 ASM_SIMP_TAC (std_ss++resq_SS) [IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, F_CLOCK_FREE_def, BOTTOM_OMEGA_def, LENGTH_def, IN_LESSX, 3674 ELEM_INFINITE, B_SEM_def], 3675 3676 SIMP_TAC std_ss [F_CLOCK_FREE_def], 3677 3678 SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def] 3679 ]); 3680 3681 3682 3683 3684 3685val WEAK_STRONG_UF_SEM___INFINITE_PATHS = 3686 store_thm 3687 ("WEAK_STRONG_UF_SEM___INFINITE_PATHS", 3688 3689 ``!v f. (IS_INFINITE v) ==> ((WEAK_UF_SEM v f = UF_SEM v f) /\ 3690 (STRONG_UF_SEM v f = UF_SEM v f))``, 3691 3692 Cases_on `v` THEN 3693 REWRITE_TAC[IS_INFINITE_def, WEAK_UF_SEM_def, STRONG_UF_SEM_def, PATH_APPEND_def]); 3694 3695 3696 3697val WEAK_STRONG_UF_SEM___FINITE_PROPER_PATHS = 3698 store_thm 3699 ("WEAK_STRONG_UF_SEM___FINITE_PROPER_PATHS", 3700 3701 ``!f p. (F_CLOCK_FREE f /\ IS_FINITE_PROPER_PATH (FINITE p) /\ IS_TOP_BOTTOM_WELL_BEHAVED f) ==> ( 3702 (STRONG_UF_SEM (FINITE p) f ==> UF_SEM (FINITE p) f) /\ 3703 (UF_SEM (FINITE p) f ==> WEAK_UF_SEM (FINITE p) f))``, 3704 3705 3706 REWRITE_TAC [WEAK_UF_SEM_def, STRONG_UF_SEM_def, PATH_APPEND_def, TOP_OMEGA_def, BOTTOM_OMEGA_def] THEN 3707 REWRITE_TAC [GSYM TOP_OMEGA_def, GSYM BOTTOM_OMEGA_def] THEN 3708 INDUCT_THEN fl_induct ASSUME_TAC THENL [ 3709 SIMP_TAC arith_ss [BOTTOM_OMEGA_def, TOP_OMEGA_def, LENGTH_CAT, F_CLOCK_FREE_def, UF_SEM_def, GT] THEN 3710 REPEAT GEN_TAC THEN STRIP_TAC THEN 3711 Cases_on `p` THENL [ 3712 SIMP_TAC list_ss [CAT_def, ELEM_INFINITE, B_SEM_def], 3713 SIMP_TAC list_ss [CAT_def, ELEM_FINITE, ELEM_def, RESTN_def, HEAD_CONS, LENGTH_def, GT] 3714 ], 3715 3716 SIMP_TAC arith_ss [BOTTOM_OMEGA_def, TOP_OMEGA_def, LENGTH_CAT, F_CLOCK_FREE_def, UF_SEM_def, xnum_distinct] THEN 3717 REPEAT GEN_TAC THEN STRIP_TAC THEN 3718 Cases_on `p` THENL [ 3719 SIMP_TAC list_ss [CAT_def, ELEM_INFINITE, B_SEM_def], 3720 SIMP_TAC list_ss [CAT_def, ELEM_FINITE, ELEM_def, RESTN_def, HEAD_CONS, LENGTH_def, xnum_11] 3721 ], 3722 3723 3724 SIMP_TAC std_ss [UF_SEM_def, COMPLEMENT_def, COMPLEMENT_CAT, IS_TOP_BOTTOM_WELL_BEHAVED_def, F_CLOCK_FREE_def, 3725 TOP_BOTTOM_OMEGA___COMPLEMENT] THEN 3726 REPEAT GEN_TAC THEN STRIP_TAC THEN 3727 `MAP COMPLEMENT_LETTER p = p` by 3728 METIS_TAC[IS_FINITE_PROPER_PATH___COMPLEMENT, COMPLEMENT_def, path_11] THEN 3729 PROVE_TAC[], 3730 3731 3732 ASM_SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def, F_CLOCK_FREE_def, UF_SEM_def], 3733 3734 3735 ASM_SIMP_TAC (list_ss++resq_SS) [IN_LESSX_REWRITE, TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, 3736 F_CLOCK_FREE_def, UF_SEM_def, LENGTH_def, LS] THEN 3737 REPEAT STRIP_TAC THENL [ 3738 `?p'. (SEL (CAT (p,INFINITE (\n. BOTTOM))) (0,j)) = p'` by PROVE_TAC[] THEN 3739 `BOTTOM_FREE p'` by PROVE_TAC[Lemma5] THEN 3740 SUBGOAL_THEN ``j:num < LENGTH (p:'a letter list)`` ASSUME_TAC THEN1 ( 3741 CCONTR_TAC THEN 3742 `LENGTH p' = j -0 + 1` by PROVE_TAC[LENGTH_SEL] THEN 3743 `j < LENGTH p'` by DECIDE_TAC THEN 3744 `~(EL j p' = BOTTOM)` by PROVE_TAC[BOTTOM_FREE_EL] THEN 3745 `EL j p' = ELEM (CAT (p,INFINITE (\n. BOTTOM))) j` by PROVE_TAC[EL_SEL0, LESS_EQ_REFL] THEN 3746 `j >= LENGTH p` by DECIDE_TAC THEN 3747 FULL_SIMP_TAC arith_ss [ELEM_CAT___GREATER_EQ, ELEM_INFINITE] 3748 ) THEN 3749 `j + 0 < LENGTH p` by DECIDE_TAC THEN 3750 PROVE_TAC[SEL_CAT___LESS], 3751 3752 `j + 0 < LENGTH p` by DECIDE_TAC THEN 3753 PROVE_TAC[SEL_CAT___LESS] 3754 ], 3755 3756 3757 REPEAT GEN_TAC THEN 3758 Cases_on `p = []` THEN1 ( 3759 ASM_SIMP_TAC std_ss [IS_TOP_BOTTOM_WELL_BEHAVED_def, CAT_def] 3760 ) THEN 3761 ASM_SIMP_TAC (list_ss++resq_SS) [UF_SEM_def, IN_LESSX_REWRITE, TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, LS, LENGTH_def] THEN 3762 REPEAT STRIP_TAC THENL [ 3763 `?k. US_SEM (SEL (CAT (SEL (CAT (p,INFINITE (\n. BOTTOM))) (0,j), 3764 INFINITE (\n. TOP))) (0,k)) s` by PROVE_TAC[] THEN 3765 `j + 0 < LENGTH p` by DECIDE_TAC THEN 3766 FULL_SIMP_TAC arith_ss [SEL_CAT___LESS] THEN 3767 PROVE_TAC[], 3768 3769 3770 3771 Cases_on `j < LENGTH p` THENL [ 3772 REMAINS_TAC `!k. 3773 ((SEL (CAT (SEL (FINITE p) (0,j),INFINITE (\n. TOP))) (0,k)) = 3774 (SEL (CAT (SEL (CAT (p,INFINITE (\n. TOP))) (0,j),INFINITE (\n. TOP))) (0,k)))` THEN1 ( 3775 PROVE_TAC[] 3776 ) THEN 3777 SIMP_TAC arith_ss [LIST_EQ_REWRITE, LENGTH_SEL, EL_SEL_THM] THEN 3778 REPEAT STRIP_TAC THEN 3779 rename1 `n < k + 1` THEN 3780 Cases_on `n < j + 1` THENL [ 3781 ASM_SIMP_TAC list_ss [ELEM_CAT___LESS, LENGTH_SEL, EL_SEL_THM, ELEM_FINITE], 3782 ASM_SIMP_TAC list_ss [ELEM_CAT___GREATER_EQ, LENGTH_SEL] 3783 ], 3784 3785 3786 `~(LENGTH p = 0)` by (Cases_on `p` THEN FULL_SIMP_TAC list_ss []) THEN 3787 `?j'. SUC j' = (LENGTH p)` by PROVE_TAC[num_CASES] THEN 3788 `j' < LENGTH p` by DECIDE_TAC THEN 3789 Tactical.REVERSE (SUBGOAL_THEN ``!k. 3790 ((SEL (CAT (SEL (FINITE p) (0,j'),INFINITE (\n. TOP))) (0,k)) = 3791 (SEL (CAT (SEL (CAT (p,INFINITE (\n. TOP))) (0,j),INFINITE (\n. TOP))) (0,k)))`` ASSUME_TAC) THEN1 ( 3792 PROVE_TAC[] 3793 ) THEN 3794 SIMP_TAC arith_ss [LIST_EQ_REWRITE, LENGTH_SEL, EL_SEL_THM] THEN 3795 REPEAT STRIP_TAC THEN 3796 rename1 `n < k + 1` THEN 3797 Cases_on `n < j' + 1` THENL [ 3798 ASM_SIMP_TAC list_ss [ELEM_CAT___LESS, LENGTH_SEL, EL_SEL_THM, ELEM_FINITE], 3799 3800 3801 ASM_SIMP_TAC list_ss [ELEM_CAT___GREATER_EQ, LENGTH_SEL, ELEM_INFINITE] THEN 3802 Cases_on `n >= j + 1` THENL [ 3803 ASM_SIMP_TAC list_ss [ELEM_CAT___GREATER_EQ, LENGTH_SEL, ELEM_INFINITE], 3804 3805 `n >= LENGTH p` by DECIDE_TAC THEN 3806 ASM_SIMP_TAC list_ss [ELEM_CAT___LESS, LENGTH_SEL, EL_SEL_THM, ELEM_CAT___GREATER_EQ, ELEM_INFINITE] 3807 ] 3808 ] 3809 ] 3810 ], 3811 3812 3813 GEN_TAC THEN 3814 Cases_on `~(LENGTH p > 1)` THENL [ 3815 ASM_SIMP_TAC list_ss [TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, CAT_def, 3816 F_CLOCK_FREE_def, UF_SEM_def, GT, LENGTH_def] THEN 3817 SUBGOAL_TAC `(RESTN (CAT (p,INFINITE (\n. BOTTOM))) 1) = INFINITE (\n. BOTTOM)` THEN1 ( 3818 Cases_on `p` THEN 3819 SIMP_TAC list_ss [CAT_def, REST_CONS, GSYM REST_RESTN, REST_def] THEN 3820 Cases_on `t` THENL [ 3821 SIMP_TAC std_ss [CAT_def], 3822 FULL_SIMP_TAC list_ss [] 3823 ] 3824 ) THEN 3825 ASM_REWRITE_TAC[GSYM BOTTOM_OMEGA_def, IS_TOP_BOTTOM_WELL_BEHAVED_def] THEN 3826 PROVE_TAC[IS_TOP_BOTTOM_WELL_BEHAVED_THM], 3827 3828 FULL_SIMP_TAC std_ss [] THEN 3829 ASM_SIMP_TAC list_ss [TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, F_CLOCK_FREE_def, UF_SEM_def, 3830 GT, LENGTH_def] THEN 3831 Cases_on `p` THEN FULL_SIMP_TAC list_ss [] THEN 3832 ASM_SIMP_TAC list_ss [GSYM REST_RESTN, 3833 REST_def, CAT_def, REST_CONS, IS_TOP_BOTTOM_WELL_BEHAVED_def] THEN 3834 STRIP_TAC THEN 3835 REWRITE_TAC[GSYM TOP_OMEGA_def, GSYM BOTTOM_OMEGA_def] THEN 3836 SUBGOAL_THEN ``IS_FINITE_PROPER_PATH (FINITE t)`` ASSUME_TAC THEN1 ( 3837 FULL_SIMP_TAC arith_ss [IS_FINITE_PROPER_PATH_def, PATH_TOP_FREE_def, PATH_BOTTOM_FREE_def, path_11] THEN 3838 Cases_on `h` THEN FULL_SIMP_TAC std_ss [TOP_FREE_def, BOTTOM_FREE_def] 3839 ) THEN 3840 PROVE_TAC[] 3841 ], 3842 3843 3844 ASM_SIMP_TAC (list_ss++resq_SS) [TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, CAT_def, 3845 IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, LENGTH_def, IN_LESSX, F_CLOCK_FREE_def, IN_LESS] THEN 3846 REPEAT STRIP_TAC THENL [ 3847 Cases_on `k >= LENGTH p` THENL [ 3848 FULL_SIMP_TAC std_ss [RESTN_CAT___GREATER_EQ, RESTN_INFINITE] THEN 3849 PROVE_TAC[IS_TOP_BOTTOM_WELL_BEHAVED_THM, BOTTOM_OMEGA_def], 3850 3851 `k < LENGTH p` by DECIDE_TAC THEN 3852 EXISTS_TAC ``k:num`` THEN 3853 REPEAT STRIP_TAC THENL [ 3854 ASM_REWRITE_TAC[], 3855 3856 `k < LENGTH (FINITE p)` by ASM_SIMP_TAC std_ss [LENGTH_def, LS] THEN 3857 `IS_FINITE_PROPER_PATH (RESTN (FINITE p) k)` by PROVE_TAC[IS_FINITE_PROPER_PATH___RESTN] THEN 3858 FULL_SIMP_TAC arith_ss [RESTN_CAT___LESS, RESTN_FINITE] THEN 3859 PROVE_TAC[BOTTOM_OMEGA_def], 3860 3861 `j < LENGTH p` by DECIDE_TAC THEN 3862 `j < LENGTH (FINITE p)` by ASM_SIMP_TAC std_ss [LENGTH_def, LS] THEN 3863 `IS_FINITE_PROPER_PATH (RESTN (FINITE p) j)` by PROVE_TAC[IS_FINITE_PROPER_PATH___RESTN] THEN 3864 FULL_SIMP_TAC arith_ss [RESTN_CAT___LESS, RESTN_FINITE] THEN 3865 PROVE_TAC[BOTTOM_OMEGA_def] 3866 ] 3867 ], 3868 3869 EXISTS_TAC ``k:num`` THEN 3870 REPEAT STRIP_TAC THENL [ 3871 `k < LENGTH (FINITE p)` by ASM_SIMP_TAC std_ss [LENGTH_def, LS] THEN 3872 `IS_FINITE_PROPER_PATH (RESTN (FINITE p) k)` by PROVE_TAC[IS_FINITE_PROPER_PATH___RESTN] THEN 3873 FULL_SIMP_TAC arith_ss [RESTN_CAT___LESS, RESTN_FINITE] THEN 3874 PROVE_TAC[TOP_OMEGA_def], 3875 3876 `j < LENGTH p` by DECIDE_TAC THEN 3877 `j < LENGTH (FINITE p)` by ASM_SIMP_TAC std_ss [LENGTH_def, LS] THEN 3878 `IS_FINITE_PROPER_PATH (RESTN (FINITE p) j)` by PROVE_TAC[IS_FINITE_PROPER_PATH___RESTN] THEN 3879 FULL_SIMP_TAC arith_ss [RESTN_CAT___LESS, RESTN_FINITE] THEN 3880 PROVE_TAC[TOP_OMEGA_def] 3881 ] 3882 ], 3883 3884 3885 ASM_SIMP_TAC (list_ss++resq_SS) [TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, CAT_def, 3886 IS_TOP_BOTTOM_WELL_BEHAVED_def, UF_SEM_def, F_CLOCK_FREE_def, IN_LESSX, LENGTH_def] THEN 3887 REPEAT STRIP_TAC THENL [ 3888 DISJ1_TAC THEN PROVE_TAC[BOTTOM_OMEGA_def], 3889 3890 DISJ2_TAC THEN 3891 EXISTS_TAC ``j:num`` THEN 3892 Tactical.REVERSE (Cases_on `j < LENGTH p`) THEN1 ( 3893 FULL_SIMP_TAC list_ss [ELEM_CAT___GREATER_EQ, ELEM_INFINITE, B_SEM_def] 3894 ) THEN 3895 FULL_SIMP_TAC arith_ss [ELEM_CAT___LESS, ELEM_FINITE] THEN 3896 Cases_on `j` THEN FULL_SIMP_TAC arith_ss [] THEN 3897 `n + 0 < LENGTH p` by DECIDE_TAC THEN 3898 FULL_SIMP_TAC std_ss [SEL_CAT___LESS], 3899 3900 DISJ1_TAC THEN PROVE_TAC[TOP_OMEGA_def], 3901 3902 DISJ2_TAC THEN 3903 EXISTS_TAC ``j:num`` THEN 3904 FULL_SIMP_TAC arith_ss [ELEM_CAT___LESS, ELEM_FINITE] THEN 3905 Cases_on `j` THEN FULL_SIMP_TAC arith_ss [] THEN 3906 `n + 0 < LENGTH p` by DECIDE_TAC THEN 3907 FULL_SIMP_TAC std_ss [SEL_CAT___LESS] 3908 ], 3909 3910 3911 ASM_REWRITE_TAC[F_CLOCK_FREE_def], 3912 3913 3914 ASM_SIMP_TAC (list_ss++resq_SS) [TOP_OMEGA_def, BOTTOM_OMEGA_def, LENGTH_CAT, 3915 IS_TOP_BOTTOM_WELL_BEHAVED_def, COMPLEMENT_CAT, COMPLEMENT_def, F_CLOCK_FREE_def, UF_SEM_def, 3916 LENGTH_def, IN_LESSX, o_DEF, COMPLEMENT_LETTER_def, RESTN_INFINITE] THEN 3917 REPEAT STRIP_TAC THENL [ 3918 `US_SEM (SEL (CAT (MAP COMPLEMENT_LETTER p,INFINITE (\n. TOP))) (0,j')) p_1` by 3919 ASM_SIMP_TAC list_ss [SEL_CAT___LESS, LENGTH_MAP] THEN 3920 `UF_SEM ((CAT (RESTN p j',INFINITE (\n. BOTTOM)))) f` by PROVE_TAC[RESTN_CAT___LESS] THEN 3921 SIMP_TAC std_ss [RESTN_FINITE] THEN 3922 `IS_FINITE_PROPER_PATH (FINITE (RESTN p j'))` by 3923 PROVE_TAC[IS_FINITE_PROPER_PATH___RESTN, LS, LENGTH_def, RESTN_FINITE] THEN 3924 PROVE_TAC[BOTTOM_OMEGA_def], 3925 3926 `?v'. v' = (SEL (CAT (MAP COMPLEMENT_LETTER p,INFINITE (\n. BOTTOM)))) (0, j')` by PROVE_TAC[] THEN 3927 Cases_on `~(j' < LENGTH p)` THEN1 ( 3928 `BOTTOM_FREE v'` by PROVE_TAC[Lemma5] THEN 3929 `j' < LENGTH v'` by ASM_SIMP_TAC arith_ss [LENGTH_SEL] THEN 3930 `EL j' v' = BOTTOM` by ASM_SIMP_TAC arith_ss [EL_SEL_THM, ELEM_CAT___GREATER_EQ, 3931 LENGTH_MAP, ELEM_INFINITE] THEN 3932 PROVE_TAC[BOTTOM_FREE_EL] 3933 ) THEN 3934 3935 FULL_SIMP_TAC arith_ss [RESTN_CAT___LESS, SEL_CAT___LESS, LENGTH_MAP, RESTN_FINITE] THEN 3936 `UF_SEM (FINITE (RESTN p j')) f` by PROVE_TAC[] THEN 3937 `IS_FINITE_PROPER_PATH (FINITE (RESTN p j'))` by 3938 PROVE_TAC[IS_FINITE_PROPER_PATH___RESTN, LS, LENGTH_def, RESTN_FINITE] THEN 3939 PROVE_TAC[TOP_OMEGA_def] 3940 ] 3941 ]); 3942 3943 3944 3945 3946val WEAK_STRONG_UF_SEM_THM = 3947 store_thm 3948 ("WEAK_STRONG_UF_SEM_THM", 3949 3950 ``!f v. (F_CLOCK_FREE f /\ IS_PROPER_PATH v /\ IS_TOP_BOTTOM_WELL_BEHAVED f) ==> ( 3951 (STRONG_UF_SEM v f ==> UF_SEM v f) /\ (UF_SEM v f ==> WEAK_UF_SEM v f))``, 3952 3953 REWRITE_TAC [IS_PROPER_PATH_def] THEN 3954 REPEAT GEN_TAC THEN STRIP_TAC THENL [ 3955 FULL_SIMP_TAC std_ss [IS_INFINITE_PROPER_PATH_def] THEN 3956 PROVE_TAC[WEAK_STRONG_UF_SEM___INFINITE_PATHS, IS_INFINITE_def], 3957 3958 `?p. v = FINITE p` by PROVE_TAC[IS_FINITE_PROPER_PATH_def] THEN 3959 PROVE_TAC[WEAK_STRONG_UF_SEM___FINITE_PROPER_PATHS] 3960 ]); 3961 3962 3963val UF_EQUIVALENT_def = 3964 Define `UF_EQUIVALENT f1 f2 = 3965 !v. ((UF_SEM v f1 = UF_SEM v f2))` 3966 3967 3968val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def = 3969 Define `UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 = 3970 !v. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> ((UF_SEM v f1 = UF_SEM v f2))` 3971 3972val F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def = 3973 Define `F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 = 3974 !v c. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> ((F_SEM v c f1 = F_SEM v c f2))` 3975 3976val F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def = 3977 Define 3978 `F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE f = 3979 (!v c. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> ~(F_SEM v c f))`; 3980 3981val F_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE_def = 3982 Define 3983 `F_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE f = 3984 (!v c. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> F_SEM v c f)`; 3985 3986val UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def = 3987 Define 3988 `UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE f = 3989 (!v. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> ~(UF_SEM v f))`; 3990 3991val UF_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE_def = 3992 Define 3993 `UF_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE f = 3994 (!v. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> UF_SEM v f)`; 3995 3996 3997 3998val UF_IS_TAUTOLOGY_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE___DUAL = 3999 store_thm 4000 ("UF_IS_TAUTOLOGY_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE___DUAL", 4001 4002 ``(!f. UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE (F_NOT f) = UF_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE f) /\ 4003 (!f. UF_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE (F_NOT f) = UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE f)``, 4004 4005 REWRITE_TAC[UF_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE_def, 4006 UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def, 4007 UF_SEM_def] THEN 4008 PROVE_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT, COMPLEMENT_COMPLEMENT]); 4009 4010 4011 4012val F_IS_TAUTOLOGY_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE___DUAL = 4013 store_thm 4014 ("F_IS_TAUTOLOGY_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE___DUAL", 4015 4016 ``(!f. F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE (F_NOT f) = F_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE f) /\ 4017 (!f. F_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE (F_NOT f) = F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE f)``, 4018 4019 REWRITE_TAC[F_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE_def, 4020 F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def, 4021 F_SEM_def] THEN 4022 PROVE_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT, COMPLEMENT_COMPLEMENT]); 4023 4024 4025val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TO___CONTRADICTION = 4026 store_thm 4027 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TO___CONTRADICTION", 4028 4029 ``!f1 f2. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 = 4030 UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE (F_NOT(F_IFF(f1, f2)))``, 4031 4032 SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 4033 UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def, 4034 UF_SEM_def, F_IFF_def, F_IMPLIES_def, F_OR_def, 4035 COMPLEMENT_COMPLEMENT, 4036 IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT] THEN 4037 PROVE_TAC[]); 4038 4039 4040 4041val F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TO___CONTRADICTION = 4042 store_thm 4043 ("F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TO___CONTRADICTION", 4044 4045 ``!f1 f2. F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 = 4046 F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE (F_NOT(F_IFF(f1, f2)))``, 4047 4048 SIMP_TAC std_ss [F_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 4049 F_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def, 4050 F_SEM_def, F_IFF_def, F_IMPLIES_def, F_OR_def, 4051 COMPLEMENT_COMPLEMENT, 4052 IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT] THEN 4053 PROVE_TAC[]); 4054 4055 4056val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___REFL = 4057 store_thm 4058 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___REFL", 4059 ``!f. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f f``, 4060 SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def]); 4061 4062 4063val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TRANS = 4064 store_thm 4065 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TRANS", 4066 ``!f1 f2 f3. (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 /\ 4067 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f3) ==> 4068 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f3``, 4069 SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def]); 4070 4071 4072val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___TRUE = 4073 store_thm 4074 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___TRUE", 4075 4076``!f. (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_SUFFIX_IMP (S_BOOL B_TRUE, f)) f)``, 4077 4078SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, IN_LESSX_REWRITE, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 4079IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT, US_SEM_def] THEN 4080REPEAT STRIP_TAC THEN 4081FULL_SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, LENGTH_def, US_SEM_def, 4082ELEM_def, LS, GT, LENGTH_SEL, SEL_def, RESTN_def] THEN 4083REWRITE_TAC[prove (``1 = SUC 0``, DECIDE_TAC), SEL_REC_def, HEAD_def] THEN 4084SIMP_TAC list_ss [FinitePSLPathTheory.ELEM_def, FinitePSLPathTheory.RESTN_def, FinitePSLPathTheory.HEAD_def, ETA_THM] THEN 4085`?s. p 0 = STATE s` by METIS_TAC[] THEN 4086ASM_REWRITE_TAC[B_SEM_def]); 4087 4088 4089 4090val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL = 4091 store_thm 4092 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL", 4093 4094``!b f. (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_SUFFIX_IMP ((S_BOOL b), f)) 4095 (F_IMPLIES((F_STRONG_BOOL b), f)))``, 4096 4097SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, IN_LESSX_REWRITE, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 4098IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT, F_IMPLIES_def, F_OR_def] THEN 4099REPEAT STRIP_TAC THEN 4100FULL_SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, LENGTH_def, US_SEM_def, 4101ELEM_def, LS, GT, LENGTH_SEL, SEL_def] THEN 4102REWRITE_TAC[prove (``1 = SUC 0``, DECIDE_TAC), SEL_REC_def, HEAD_def] THEN 4103SIMP_TAC list_ss [RESTN_INFINITE, HEAD_def, FinitePSLPathTheory.ELEM_def, FinitePSLPathTheory.RESTN_def, FinitePSLPathTheory.HEAD_def, ETA_THM] THEN 4104METIS_TAC[]); 4105 4106 4107val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CAT = 4108 store_thm 4109 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CAT", 4110 4111``!s1 s2 f. (~(US_SEM [] s1) /\ ~(US_SEM [] s2)) ==> 4112 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 4113 (F_SUFFIX_IMP (S_CAT(s1, s2), f)) 4114 (F_SUFFIX_IMP (s1, (F_NEXT (F_SUFFIX_IMP (s2, f)))))``, 4115 4116SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, IN_LESSX_REWRITE, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 4117IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT] THEN 4118REPEAT STRIP_TAC THEN 4119FULL_SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, LENGTH_def, US_SEM_def, 4120ELEM_def, LS, GT, LENGTH_SEL, SEL_def, RESTN_INFINITE, 4121COMPLEMENT_def, combinTheory.o_DEF] THEN 4122SUBGOAL_TAC `!x. COMPLEMENT_LETTER (p x) = p x` THEN1 ( 4123 GEN_TAC THEN 4124 `?s. p x = STATE s` by METIS_TAC[] THEN 4125 ASM_REWRITE_TAC[COMPLEMENT_LETTER_def] 4126) THEN 4127ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 4128 4129EQ_TAC THEN REPEAT STRIP_TAC THENL [ 4130 Q_SPEC_NO_ASSUM 2 `j' + 1 + j` THEN 4131 PROVE_CONDITION_NO_ASSUM 0 THENL [ 4132 ALL_TAC, 4133 FULL_SIMP_TAC arith_ss [] 4134 ] THEN 4135 4136 Q_TAC EXISTS_TAC `SEL_REC (j + 1) 0 (INFINITE p)` THEN 4137 Q_TAC EXISTS_TAC `SEL_REC (j' + 1) 0 (INFINITE (\n. p (n + 1 + j)))` THEN 4138 ASM_REWRITE_TAC[] THEN 4139 4140 REPEAT WEAKEN_HD_TAC THEN 4141 SPEC_TAC (``p:num -> 'a letter``, ``p:num -> 'a letter``) THEN 4142 Induct_on `j` THENL [ 4143 SIMP_TAC arith_ss [] THEN 4144 REWRITE_TAC[prove (``(j' + 2 = SUC (SUC j')) /\ ((j' + 1) = SUC j') /\ (1 = SUC 0)``, DECIDE_TAC), SEL_REC_def] THEN 4145 SIMP_TAC list_ss [REST_INFINITE, HEAD_def] THEN 4146 GEN_TAC THEN AP_TERM_TAC THEN 4147 SIMP_TAC arith_ss [path_11, FUN_EQ_THM] THEN 4148 GEN_TAC THEN 4149 AP_TERM_TAC THEN 4150 DECIDE_TAC, 4151 4152 4153 FULL_SIMP_TAC arith_ss [] THEN 4154 GEN_TAC THEN 4155 `(j' + (SUC j + 2)) = SUC (j + (j' + 2))` by DECIDE_TAC THEN 4156 ASM_REWRITE_TAC[SEL_REC_def, REST_INFINITE] THEN 4157 WEAKEN_HD_TAC THEN 4158 `(SUC j + 1) = SUC (j + 1)` by DECIDE_TAC THEN 4159 ASM_REWRITE_TAC[SEL_REC_def, REST_INFINITE] THEN 4160 SIMP_TAC list_ss [] THEN 4161 AP_TERM_TAC THEN 4162 SIMP_TAC arith_ss [path_11, FUN_EQ_THM] THEN 4163 GEN_TAC THEN 4164 AP_TERM_TAC THEN 4165 DECIDE_TAC 4166 ], 4167 4168 4169 4170 4171 4172 4173 4174 `?k. k = PRE (LENGTH v1)` by METIS_TAC[] THEN 4175 `?k'. k' = PRE (LENGTH v2)` by METIS_TAC[] THEN 4176 4177 SUBGOAL_TAC `LENGTH v1 > 0` THEN1 ( 4178 Cases_on `v1` THENL [ 4179 PROVE_TAC[], 4180 SIMP_TAC list_ss [] 4181 ] 4182 ) THEN 4183 4184 SUBGOAL_TAC `LENGTH v2 > 0` THEN1 ( 4185 Cases_on `v2` THENL [ 4186 PROVE_TAC[], 4187 SIMP_TAC list_ss [] 4188 ] 4189 ) THEN 4190 4191 FULL_SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN 4192 Q_SPECL_NO_ASSUM 7 [`k`, `k'`] THEN 4193 `(?l. k + 1 = l) /\ (?l'. k' + 1 = l')` by METIS_TAC[] THEN 4194 4195 SUBGOAL_TAC `j + 1 = l' + l` THEN1 ( 4196 `j + 1 = LENGTH (v1 <> v2)` by METIS_TAC[LENGTH_SEL_REC] THEN 4197 ASM_SIMP_TAC std_ss [] THEN 4198 SIMP_TAC list_ss [] THEN 4199 DECIDE_TAC 4200 ) THEN 4201 FULL_SIMP_TAC std_ss [] THEN 4202 4203 `LENGTH v1 = l` by DECIDE_TAC THEN 4204 `LENGTH v2 = l'` by DECIDE_TAC THEN 4205 FULL_SIMP_TAC std_ss [SEL_REC_SPLIT, APPEND_LENGTH_EQ,LENGTH_SEL_REC] THEN 4206 4207 NTAC 2 (GSYM_NO_TAC 13) (*v1, v2*) THEN 4208 FULL_SIMP_TAC std_ss [LENGTH_SEL_REC] THEN 4209 CLEAN_ASSUMPTIONS_TAC THEN 4210 PROVE_CONDITION_NO_ASSUM 5 THEN1 ASM_REWRITE_TAC[] THEN 4211 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 4212 SUBGOAL_TAC `INFINITE (\n. p (n + 1 + k)) = 4213 RESTN (INFINITE p) l` THEN1 ( 4214 SIMP_TAC std_ss [RESTN_INFINITE, path_11, FUN_EQ_THM] THEN 4215 GEN_TAC THEN AP_TERM_TAC THEN DECIDE_TAC 4216 ) THEN 4217 ASM_SIMP_TAC std_ss [SEL_REC_RESTN] 4218 ) THEN 4219 4220 UNDISCH_HD_TAC THEN IMP_TO_EQ_TAC THEN 4221 AP_THM_TAC THEN AP_TERM_TAC THEN 4222 SIMP_TAC std_ss [path_11, FUN_EQ_THM] THEN 4223 GEN_TAC THEN AP_TERM_TAC THEN DECIDE_TAC 4224]); 4225 4226 4227val S_BOOL_BIGCAT_def = 4228 Define 4229 `(S_BOOL_BIGCAT [b1] = S_BOOL b1) /\ 4230 (S_BOOL_BIGCAT (b1::b2::l) = S_CAT (S_BOOL b1, S_BOOL_BIGCAT (b2::l)))` 4231 4232 4233 4234val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL_BIGCAT = 4235 store_thm 4236 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL_BIGCAT", 4237 4238``(!f:'a fl b. 4239 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 4240 (F_SUFFIX_IMP (S_BOOL_BIGCAT [b], f)) (F_IMPLIES((F_STRONG_BOOL b), f))) /\ 4241 (!f:'a fl b1 b2 l. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 4242 (F_SUFFIX_IMP (S_BOOL_BIGCAT (b1::b2::l), f)) 4243 (F_IMPLIES((F_STRONG_BOOL b1), F_NEXT (F_SUFFIX_IMP (S_BOOL_BIGCAT (b2::l), f)))))``, 4244 4245 REPEAT STRIP_TAC THENL [ 4246 SIMP_TAC std_ss [S_BOOL_BIGCAT_def, 4247 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL], 4248 4249 SIMP_TAC std_ss [S_BOOL_BIGCAT_def] THEN 4250 ASSUME_TAC UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CAT THEN 4251 Q_SPECL_NO_ASSUM 0 [`S_BOOL b1`, `S_BOOL_BIGCAT (b2::l)`, `f`] THEN 4252 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 4253 Cases_on `l` THEN SIMP_TAC list_ss [US_SEM_def, S_BOOL_BIGCAT_def] 4254 ) THEN 4255 ASSUME_TAC UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___BOOL THEN 4256 FULL_SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def] 4257 ]); 4258 4259 4260 4261 4262 4263 4264 4265 4266 4267 4268 4269 4270 4271 4272 4273 4274 4275 4276 4277 4278 4279 4280 4281 4282val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL = 4283 store_thm 4284 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL", 4285 4286``!b f c. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 4287 (F_CLOCK_COMP c (F_SUFFIX_IMP ((S_BOOL b), f))) 4288 (F_W_CLOCK c (F_IMPLIES((F_STRONG_BOOL b), F_CLOCK_COMP c f)))``, 4289 4290 4291SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, IN_LESSX_REWRITE, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 4292IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT, F_IMPLIES_def, F_OR_def, 4293F_CLOCK_COMP_def, F_W_CLOCK_def, S_CLOCK_COMP_def, US_SEM_def, 4294COMPLEMENT_COMPLEMENT, F_W_def, F_G_def, F_F_def 4295] THEN 4296REPEAT STRIP_TAC THEN 4297FULL_SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, LENGTH_def, ELEM_def, LS, GT, LENGTH_SEL, SEL_def, RESTN_INFINITE, IMP_DISJ_THM, 4298xnum_distinct, HEAD_def, LENGTH_COMPLEMENT, RESTN_COMPLEMENT, IN_LESS] THEN 4299 4300SUBGOAL_TAC `!k. (COMPLEMENT (INFINITE (\n. p (n + k)))) = 4301 (INFINITE (\n. p (n + k)))` THEN1 ( 4302 SIMP_TAC std_ss [COMPLEMENT_def, path_11, FUN_EQ_THM] THEN 4303 REPEAT GEN_TAC THEN 4304 `?s. p (n + k) = STATE s` by METIS_TAC[] THEN 4305 ASM_SIMP_TAC std_ss [COMPLEMENT_LETTER_def] 4306) THEN 4307ASM_SIMP_TAC std_ss [HEAD_def] THEN WEAKEN_HD_TAC THEN 4308`!j. B_SEM (p j) B_TRUE` by METIS_TAC[B_SEM_def] THEN 4309ASM_SIMP_TAC std_ss [HEAD_def] THEN WEAKEN_HD_TAC THEN 4310 4311`!j. B_SEM (p j) (B_NOT c) = ~(B_SEM (p j) c)` by METIS_TAC[B_SEM_def] THEN 4312ASM_SIMP_TAC std_ss [HEAD_def] THEN WEAKEN_HD_TAC THEN 4313 4314EQ_TAC THENL [ 4315 REPEAT STRIP_TAC THEN 4316 LEFT_DISJ_TAC THEN 4317 FULL_SIMP_TAC std_ss [] THEN 4318 Q_EXISTS_LEAST_TAC `?l:num. B_SEM (p l) c` THEN 4319 FULL_SIMP_TAC std_ss [] THEN 4320 Q_TAC EXISTS_TAC `l` THEN 4321 ASM_REWRITE_TAC[] THEN 4322 REPEAT STRIP_TAC THENL [ 4323 ALL_TAC, 4324 METIS_TAC[] 4325 ] THEN 4326 Q_SPEC_NO_ASSUM 3 `l` THEN 4327 FULL_SIMP_TAC std_ss [] THEN 4328 DISJ1_TAC THEN 4329 Q_SPECL_NO_ASSUM 0 [`SEL_REC l 0 (INFINITE p)`, 4330 `SEL_REC 1 l (INFINITE p)`] THEN 4331 FULL_SIMP_TAC std_ss [] THENL [ 4332 FULL_SIMP_TAC std_ss [prove (``l + (1:num) = 1 + l``, DECIDE_TAC)] THEN 4333 FULL_SIMP_TAC std_ss [SEL_REC_SPLIT], 4334 4335 CCONTR_TAC THEN WEAKEN_HD_TAC THEN 4336 UNDISCH_HD_TAC THEN 4337 SIMP_TAC std_ss [] THEN 4338 NTAC 2 (WEAKEN_NO_TAC 1) THEN 4339 Induct_on `l` THENL [ 4340 SIMP_TAC std_ss [SEL_REC_def] THEN 4341 EXISTS_TAC ``[]:'a letter list list`` THEN 4342 SIMP_TAC list_ss [CONCAT_def], 4343 4344 REPEAT STRIP_TAC THEN 4345 FULL_SIMP_TAC arith_ss [] THEN 4346 Q_TAC EXISTS_TAC `vlist <> [[p l]]` THEN 4347 ASM_SIMP_TAC list_ss [FinitePSLPathTheory.ELEM_def, 4348 FinitePSLPathTheory.RESTN_def, FinitePSLPathTheory.HEAD_def, 4349 CONCAT_APPEND, CONCAT_def] THEN 4350 REPEAT STRIP_TAC THENL [ 4351 REWRITE_TAC [prove (``SUC l = 1 + l``, DECIDE_TAC)] THEN 4352 ASM_SIMP_TAC list_ss [SEL_REC_SPLIT] THEN 4353 ONCE_REWRITE_TAC [prove (``1 = SUC 0``, DECIDE_TAC)] THEN 4354 SIMP_TAC std_ss [SEL_REC_SUC, ELEM_INFINITE, SEL_REC_def], 4355 4356 `l < SUC l` by DECIDE_TAC THEN 4357 METIS_TAC[B_SEM_def] 4358 ] 4359 ], 4360 4361 FULL_SIMP_TAC std_ss [LENGTH_SEL_REC], 4362 4363 UNDISCH_HD_TAC THEN 4364 ONCE_REWRITE_TAC [prove (``1 = SUC 0``, DECIDE_TAC)] THEN 4365 SIMP_TAC list_ss [SEL_REC_SUC, ELEM_INFINITE, SEL_REC_def, 4366 FinitePSLPathTheory.ELEM_def, FinitePSLPathTheory.RESTN_def, 4367 FinitePSLPathTheory.HEAD_def] THEN 4368 METIS_TAC[B_SEM_def] 4369 ], 4370 4371 4372 Q.ABBREV_TAC `XXX = (?k. 4373 (B_SEM (p k) c /\ 4374 (~B_SEM (p k) b \/ 4375 UF_SEM (INFINITE (\n. p (n + k))) (F_CLOCK_COMP c f))) /\ 4376 !j. ~(j < k) \/ ~B_SEM (p j) c) \/ !k. ~B_SEM (p k) c` THEN 4377 REPEAT STRIP_TAC THEN 4378 LEFT_DISJ_TAC THEN 4379 REPEAT STRIP_TAC THEN 4380 RIGHT_DISJ_TAC THEN 4381 LEFT_DISJ_TAC THEN 4382 SIMP_ALL_TAC std_ss [] THEN 4383 4384 SUBGOAL_TAC `(!vlist. 4385 ~(v1 = CONCAT vlist) \/ 4386 ~EVERY (\v'. (LENGTH v' = 1) /\ B_SEM (ELEM v' 0) (B_NOT c)) vlist) = 4387 ~(EVERY (\s. B_SEM s (B_NOT c)) v1)` THEN1 ( 4388 ONCE_REWRITE_TAC[prove (``(A = B) = (~A = ~B)``, PROVE_TAC[])] THEN 4389 EQ_TAC THEN SIMP_TAC std_ss [] THEN STRIP_TAC THENL [ 4390 ASM_REWRITE_TAC[] THEN 4391 WEAKEN_NO_TAC 1 (*Def v1*) THEN 4392 Induct_on `vlist` THENL [ 4393 SIMP_TAC list_ss [CONCAT_def], 4394 4395 SIMP_TAC list_ss [CONCAT_def] THEN 4396 Cases_on `h` THEN 4397 FULL_SIMP_TAC list_ss [LENGTH_NIL, ELEM_EL] 4398 ], 4399 4400 WEAKEN_NO_TAC 3 (*v1 <> v2 = SEL REC...*) THEN 4401 UNDISCH_HD_TAC THEN 4402 SPEC_TAC (``v1:'a letter list``, ``v1:'a letter list``) THEN 4403 INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 4404 REPEAT STRIP_TAC THEN 4405 EXISTS_TAC ``[]:'a letter list list`` THEN 4406 SIMP_TAC list_ss [CONCAT_def], 4407 4408 4409 SIMP_TAC list_ss [SNOC_APPEND] THEN 4410 REPEAT STRIP_TAC THEN 4411 FULL_SIMP_TAC std_ss [] THEN 4412 Q_TAC EXISTS_TAC `vlist <> [[x]]` THEN 4413 ASM_SIMP_TAC list_ss [CONCAT_APPEND, CONCAT_def, 4414 ELEM_EL] 4415 ] 4416 ] 4417 ) THEN 4418 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 4419 4420 4421 SUBGOAL_TAC `LENGTH v1 = j` THEN1 ( 4422 `LENGTH (v1 <> v2) = j + 1` by METIS_TAC[LENGTH_SEL_REC] THEN 4423 UNDISCH_HD_TAC THEN 4424 ASM_SIMP_TAC list_ss [] 4425 ) THEN 4426 UNDISCH_NO_TAC 3 (*v1 <> v2*) THEN 4427 REWRITE_TAC [prove (``l + (1:num) = 1 + l``, DECIDE_TAC)] THEN 4428 ASM_SIMP_TAC std_ss [SEL_REC_SPLIT, APPEND_LENGTH_EQ, LENGTH_SEL_REC] THEN 4429 ONCE_REWRITE_TAC [prove (``1 = SUC 0``, DECIDE_TAC)] THEN 4430 SIMP_TAC std_ss [SEL_REC_SUC, ELEM_INFINITE, SEL_REC_def] THEN 4431 REPEAT STRIP_TAC THEN 4432 GSYM_NO_TAC 1 THEN 4433 `?s. p j = STATE s` by METIS_TAC[] THEN 4434 `?P. P = \k. (B_SEM (p k) c /\ 4435 (~B_SEM (p k) b \/ 4436 UF_SEM (INFINITE (\n. p (k + n))) (F_CLOCK_COMP c f)) /\ 4437 !j. ~(j < k) \/ ~B_SEM (p j) c)` by METIS_TAC[] THEN 4438 SUBGOAL_TAC `?k. P k` THEN1 ( 4439 Q.UNABBREV_TAC `XXX` THEN 4440 FULL_SIMP_TAC list_ss [ELEM_EL, B_SEM_def] THENL [ 4441 METIS_TAC[], 4442 Q_TAC EXISTS_TAC `k` THEN FULL_SIMP_TAC arith_ss [], 4443 METIS_TAC[] 4444 ] 4445 ) THEN 4446 NTAC 2 (WEAKEN_NO_TAC 10) THEN GSYM_NO_TAC 1 THEN 4447 4448 FULL_SIMP_TAC list_ss [FinitePSLPathTheory.ELEM_def, 4449 FinitePSLPathTheory.RESTN_def, FinitePSLPathTheory.HEAD_def, 4450 B_SEM_def] THEN 4451 Q_EXISTS_LEAST_TAC `?l. P l` THEN 4452 SIMP_ALL_TAC std_ss [] THEN 4453 REMAINS_TAC `l = j` THEN1 METIS_TAC[] THEN 4454 REMAINS_TAC `~(l < j) /\ ~(j < l)` THEN1 DECIDE_TAC THEN 4455 STRIP_TAC THENL [ 4456 CCONTR_TAC THEN 4457 SIMP_ALL_TAC std_ss [] THEN 4458 REMAINS_TAC `MEM (p l) v1` THEN1 ( 4459 SIMP_ALL_TAC std_ss [listTheory.EVERY_MEM] THEN 4460 METIS_TAC[B_SEM_def] 4461 ) THEN 4462 GSYM_NO_TAC 8 (*v1 = SEL_REC ..*) THEN 4463 ASM_SIMP_TAC std_ss [MEM_SEL_REC, ELEM_INFINITE] THEN 4464 METIS_TAC[], 4465 4466 METIS_TAC[B_SEM_def] 4467 ] 4468]); 4469 4470 4471 4472val S_SEM___CLOCK_OCCURRENCE = 4473 store_thm 4474 ("S_SEM___CLOCK_OCCURRENCE", 4475 4476 ``!s v c. S_SEM v c s /\ ~(v = []) /\ S_CLOCK_FREE s ==> 4477 B_SEM (EL (LENGTH v - 1) v) c``, 4478 4479INDUCT_THEN sere_induct ASSUME_TAC THENL [ 4480 SIMP_TAC (list_ss++resq_SS) [S_SEM_def, CLOCK_TICK_def, IN_LESS, 4481 ELEM_EL], 4482 4483 SIMP_TAC (list_ss++resq_SS) [S_SEM_def, S_CLOCK_FREE_def] THEN 4484 REPEAT STRIP_TAC THEN 4485 Cases_on `v2 = []` THENL [ 4486 FULL_SIMP_TAC list_ss [], 4487 4488 `LENGTH v2 > 0` by (Cases_on `v2` THEN FULL_SIMP_TAC list_ss []) THEN 4489 ASM_SIMP_TAC list_ss [EL_APPEND2] 4490 ], 4491 4492 SIMP_TAC (list_ss++resq_SS) [S_SEM_def, S_CLOCK_FREE_def] THEN 4493 REPEAT STRIP_TAC THEN 4494 FULL_SIMP_TAC list_ss [] THEN 4495 ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC, EL_APPEND2] THEN 4496 `LENGTH (l::v2) - 1 = LENGTH v2` by SIMP_TAC list_ss [] THEN 4497 `~(l::v2 = [])` by SIMP_TAC list_ss [] THEN 4498 SIMP_TAC list_ss [] THEN 4499 METIS_TAC[], 4500 4501 4502 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN METIS_TAC[], 4503 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN METIS_TAC[], 4504 SIMP_TAC std_ss [S_SEM_def], 4505 4506 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4507 REPEAT STRIP_TAC THEN 4508 SUBGOAL_TAC `?vlist' x. (v = CONCAT vlist' <> x) /\ (~(x = [])) /\ 4509 S_SEM x c s` THEN1 ( 4510 UNDISCH_ALL_TAC THEN 4511 SPEC_TAC (``v:'a letter list``, ``v:'a letter list``) THEN 4512 SPEC_TAC (``vlist:'a letter list list``, ``vlist:'a letter list list``) THEN 4513 INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 4514 ASM_SIMP_TAC list_ss [CONCAT_def], 4515 4516 REPEAT STRIP_TAC THEN 4517 FULL_SIMP_TAC list_ss [SNOC_APPEND, CONCAT_APPEND, CONCAT_def] THEN 4518 Cases_on `x = []` THENL [ 4519 FULL_SIMP_TAC list_ss [] THEN 4520 METIS_TAC[], 4521 4522 METIS_TAC[] 4523 ] 4524 ] 4525 ) THEN 4526 4527 WEAKEN_NO_TAC 5 (*v = CONCAT vlist*) THEN 4528 `LENGTH x > 0` by (Cases_on `x` THEN ASM_SIMP_TAC list_ss [] THEN PROVE_TAC[]) THEN 4529 ASM_SIMP_TAC list_ss [EL_APPEND2], 4530 4531 4532 SIMP_TAC std_ss [S_CLOCK_FREE_def] 4533]); 4534 4535 4536 4537 4538 4539val S_SEM___EXTEND_NO_CLOCK_CYCLES = 4540 store_thm 4541 ("S_SEM___EXTEND_NO_CLOCK_CYCLES", 4542 4543``!s k m n0 c p. 4544((!l. (l < k) ==> B_SEM (ELEM p (n0 + l)) (B_NOT c)) /\ 4545 (S_SEM (SEL_REC m (n0+k) p) c s) /\ 4546 (m > 0) /\ 4547 (S_CLOCK_FREE s)) ==> 4548 (S_SEM (SEL_REC (m+k) n0 p) c s)``, 4549 4550 4551INDUCT_THEN sere_induct ASSUME_TAC THENL [ 4552 SIMP_TAC (std_ss++resq_SS) [S_SEM_def, CLOCK_TICK_def, IN_LESSX_REWRITE, 4553 LENGTH_SEL_REC, IN_LESS, ELEM_EL, S_CLOCK_FREE_def] THEN 4554 REPEAT STRIP_TAC THENL [ 4555 DECIDE_TAC, 4556 4557 UNDISCH_NO_TAC 2 THEN 4558 ASM_SIMP_TAC arith_ss [EL_SEL_REC], 4559 4560 FULL_SIMP_TAC arith_ss [EL_SEL_REC] THEN 4561 Cases_on `i < k` THENL [ 4562 PROVE_TAC[], 4563 4564 REMAINS_TAC `?i'. (i' < m - 1) /\ ((i' + (k + n0)) = (i + n0))` THEN1 PROVE_TAC[] THEN 4565 Q_TAC EXISTS_TAC `i - k` THEN 4566 ASM_SIMP_TAC arith_ss [] 4567 ], 4568 4569 UNDISCH_NO_TAC 0 THEN 4570 ASM_SIMP_TAC arith_ss [EL_SEL_REC] 4571 ], 4572 4573 4574 4575 4576 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4577 REPEAT STRIP_TAC THEN 4578 Cases_on `~(LENGTH v1 > 0)` THEN1 ( 4579 `LENGTH v1 = 0` by DECIDE_TAC THEN 4580 Q_TAC EXISTS_TAC `[]:'a letter list` THEN 4581 Q_TAC EXISTS_TAC `SEL_REC (k + m) n0 p` THEN 4582 FULL_SIMP_TAC list_ss [LENGTH_NIL] 4583 ) THEN 4584 4585 Q_TAC EXISTS_TAC `SEL_REC (LENGTH v1 + k) n0 p` THEN 4586 Q_TAC EXISTS_TAC `SEL_REC (LENGTH v2) (n0 + (LENGTH v1 + k)) p` THEN 4587 ASM_SIMP_TAC arith_ss [GSYM SEL_REC_SPLIT] THEN 4588 4589 4590 Q.ABBREV_TAC `m1 = LENGTH v1` THEN 4591 Q.ABBREV_TAC `m2 = LENGTH v2` THEN 4592 `m = m1 + m2` by METIS_TAC[LENGTH_SEL_REC, LENGTH_APPEND] THEN 4593 ASM_REWRITE_TAC[] THEN 4594 4595 UNDISCH_NO_TAC 9 (*SEL REC m (n0 + k) p = v1 <> v2*) THEN 4596 SUBGOAL_TAC `SEL_REC m (n0 + k) p = 4597 SEL_REC m1 (n0 + k) p <> SEL_REC m2 ((n0 + k) + m1) p` THEN1 ( 4598 METIS_TAC[SEL_REC_SPLIT, ADD_COMM] 4599 ) THEN 4600 4601 ASM_SIMP_TAC arith_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC] THEN 4602 METIS_TAC[ADD_COMM], 4603 4604 4605 4606 4607 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4608 REPEAT STRIP_TAC THEN 4609 4610 Q_TAC EXISTS_TAC `SEL_REC (LENGTH v1 + k) n0 p` THEN 4611 Q_TAC EXISTS_TAC `SEL_REC (LENGTH v2) (n0 + ((LENGTH v1 + 1) + k)) p` THEN 4612 Q_TAC EXISTS_TAC `l` THEN 4613 4614 Q.ABBREV_TAC `m1 = LENGTH v1` THEN 4615 Q.ABBREV_TAC `m2 = LENGTH v2` THEN 4616 SUBGOAL_TAC `m = (m1 + 1) + m2` THEN1 ( 4617 `LENGTH (SEL_REC m (n0 + k) p) = LENGTH (v1 <> [l] <> v2)` by METIS_TAC[] THEN 4618 UNDISCH_HD_TAC THEN 4619 ASM_SIMP_TAC list_ss [LENGTH_SEL_REC] 4620 ) THEN 4621 ASM_REWRITE_TAC[] THEN 4622 4623 SUBGOAL_TAC `[l] = SEL_REC (1:num) (n0 + (m1 + k)) p` THEN1 ( 4624 MATCH_RIGHT_EQ_MP_TAC LIST_EQ_REWRITE THEN 4625 SIMP_TAC list_ss [LENGTH_SEL_REC] THEN 4626 REPEAT STRIP_TAC THEN 4627 rename1 `EL n [l]` THEN 4628 `n = 0` by DECIDE_TAC THEN 4629 ASM_SIMP_TAC std_ss [EL_SEL_REC] THEN 4630 `EL m1 (SEL_REC m (n0 + k) p) = EL m1 (v1 <> [l] <> v2)` by METIS_TAC[] THEN 4631 UNDISCH_HD_TAC THEN 4632 ASM_SIMP_TAC list_ss [EL_SEL_REC, EL_APPEND1, EL_APPEND2] 4633 ) THEN 4634 4635 SUBGOAL_TAC `(v1 = SEL_REC m1 (n0 + k) p) /\ 4636 (v2 = SEL_REC m2 ((n0 + k) + m1 + 1) p)` THEN1 ( 4637 SUBGOAL_TAC `SEL_REC m (n0 + k) p = 4638 SEL_REC m1 (n0 + k) p <> [l] <> SEL_REC m2 ((n0 + k) + m1 + 1) p` THEN1 ( 4639 GSYM_NO_TAC 9 (*SEL_REC m (n0 + k) = ...*) THEN 4640 `m1 + 1 + m2 = m2 + 1 + m1` by DECIDE_TAC THEN 4641 ASM_REWRITE_TAC[] THEN 4642 ASM_REWRITE_TAC[SEL_REC_SPLIT] THEN 4643 SIMP_TAC list_ss [] 4644 ) THEN 4645 UNDISCH_NO_TAC 10 (*SEL_REC m (n0 + k) = ...*) THEN 4646 ASM_SIMP_TAC arith_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC, LENGTH_APPEND] 4647 ) THEN 4648 4649 REPEAT STRIP_TAC THENL [ 4650 `(n0 + (m1 + 1 + k)) = n0 + (1 + (m1 + k))` by DECIDE_TAC THEN 4651 ASM_REWRITE_TAC[GSYM SEL_REC_SPLIT] THEN 4652 SIMP_TAC arith_ss [], 4653 4654 4655 UNDISCH_NO_TAC 10 (*S_SEM v1 <> [l] *) THEN 4656 ASM_REWRITE_TAC [GSYM SEL_REC_SPLIT] THEN 4657 `(n0 + (m1 + k)) = (n0 + k) + m1` by DECIDE_TAC THEN 4658 ASM_REWRITE_TAC [GSYM SEL_REC_SPLIT] THEN 4659 `((1 + m1) > 0) /\ ((1 + (m1 + k)) = ((1 + m1) + k))` by DECIDE_TAC THEN 4660 METIS_TAC[], 4661 4662 FULL_SIMP_TAC arith_ss [] 4663 ], 4664 4665 4666 4667 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4668 METIS_TAC[], 4669 4670 4671 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4672 METIS_TAC[], 4673 4674 4675 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4676 REPEAT STRIP_TAC THEN 4677 `LENGTH (SEL_REC m (n0 + k) p) = LENGTH ([]:'a letter list)` by PROVE_TAC[] THEN 4678 FULL_SIMP_TAC list_ss [LENGTH_SEL_REC], 4679 4680 4681 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4682 REPEAT STRIP_TAC THEN 4683 SUBGOAL_TAC `?h l. (CONCAT vlist = CONCAT (h::l)) /\ (!e. MEM e (h::l) ==> MEM e vlist) /\ (LENGTH h > 0)` THEN1 ( 4684 Induct_on `vlist` THENL [ 4685 REPEAT STRIP_TAC THEN 4686 `LENGTH (SEL_REC m (n0 + k) p) = LENGTH (CONCAT ([]:'a letter list list))` by PROVE_TAC[] THEN 4687 FULL_SIMP_TAC list_ss [CONCAT_def, LENGTH_SEL_REC], 4688 4689 GEN_TAC THEN 4690 Cases_on `h = []` THENL [ 4691 FULL_SIMP_TAC list_ss [CONCAT_def] THEN 4692 METIS_TAC[], 4693 4694 FULL_SIMP_TAC list_ss [CONCAT_def] THEN 4695 REMAINS_TAC `LENGTH h > 0` THEN1 METIS_TAC[] THEN 4696 Cases_on `h` THEN FULL_SIMP_TAC list_ss [] 4697 ] 4698 ] 4699 ) THEN 4700 FULL_SIMP_TAC list_ss [listTheory.EVERY_MEM, CONCAT_def] THEN 4701 4702 4703 Q_TAC EXISTS_TAC `(SEL_REC (LENGTH h + k) n0 p)::l` THEN 4704 Q.ABBREV_TAC `m1 = LENGTH h` THEN 4705 Q.ABBREV_TAC `m2 = LENGTH (CONCAT l)` THEN 4706 `m = m1 + m2` by METIS_TAC[LENGTH_SEL_REC, LENGTH_APPEND] THEN 4707 ASM_SIMP_TAC list_ss [DISJ_IMP_THM, CONCAT_def] THEN 4708 4709 4710 GSYM_NO_TAC 9 (*SEL REC m (n0 + k) p = v1 <> v2*) THEN 4711 UNDISCH_HD_TAC THEN 4712 SUBGOAL_TAC `SEL_REC (m1 + m2) (k + n0) p = 4713 SEL_REC m1 (k + n0) p <> SEL_REC m2 ((k+ n0) + m1) p` THEN1 ( 4714 METIS_TAC[SEL_REC_SPLIT, ADD_COMM] 4715 ) THEN 4716 4717 ASM_SIMP_TAC list_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC, CONCAT_def] THEN 4718 REPEAT STRIP_TAC THEN 4719 `(k + (m1 + n0)) = (n0 + (k + m1))` by DECIDE_TAC THEN 4720 ASM_REWRITE_TAC[GSYM SEL_REC_SPLIT] THEN 4721 SIMP_TAC arith_ss [], 4722 4723 4724 SIMP_TAC std_ss [S_CLOCK_FREE_def] 4725]); 4726 4727 4728 4729 4730 4731val S_SEM___RESTRICT_NO_CLOCK_CYCLES = 4732 store_thm 4733 ("S_SEM___RESTRICT_NO_CLOCK_CYCLES", 4734 4735``!s k m n0 c p. 4736((!l. (l < k) ==> ((B_SEM (ELEM p (n0 + l)) (B_NOT c)) /\ ?s'. (ELEM p (n0 + l) = STATE s'))) /\ 4737 (S_SEM (SEL_REC (m+k) n0 p) c s) /\ 4738 (m > 0) /\ 4739 (S_CLOCK_FREE s)) ==> 4740 (S_SEM (SEL_REC m (n0+k) p) c s)``, 4741 4742 4743INDUCT_THEN sere_induct ASSUME_TAC THENL [ 4744 SIMP_TAC (std_ss++resq_SS) [S_SEM_def, CLOCK_TICK_def, IN_LESSX_REWRITE, 4745 LENGTH_SEL_REC, IN_LESS, ELEM_EL, S_CLOCK_FREE_def] THEN 4746 REPEAT STRIP_TAC THENL [ 4747 FULL_SIMP_TAC arith_ss [EL_SEL_REC], 4748 4749 FULL_SIMP_TAC arith_ss [EL_SEL_REC] THEN 4750 REMAINS_TAC `?i'. (i' < k + m - 1) /\ ((i' + n0) = (i + (k + n0)))` THEN1 PROVE_TAC[] THEN 4751 Q_TAC EXISTS_TAC `i + k` THEN 4752 ASM_SIMP_TAC arith_ss [], 4753 4754 FULL_SIMP_TAC arith_ss [EL_SEL_REC] 4755 ], 4756 4757 4758 4759 4760 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4761 REPEAT STRIP_TAC THEN 4762 Cases_on `~(LENGTH v1 > 0)` THEN1 ( 4763 `LENGTH v1 = 0` by DECIDE_TAC THEN 4764 Q_TAC EXISTS_TAC `[]:'a letter list` THEN 4765 Q_TAC EXISTS_TAC `SEL_REC m (n0 + k) p` THEN 4766 FULL_SIMP_TAC list_ss [LENGTH_NIL] 4767 ) THEN 4768 4769 Q.ABBREV_TAC `m1 = LENGTH v1` THEN 4770 Q.ABBREV_TAC `m2 = LENGTH v2` THEN 4771 `m + k = m1 + m2` by METIS_TAC[LENGTH_SEL_REC, LENGTH_APPEND] THEN 4772 4773 SUBGOAL_TAC `m1 > k` THEN1 ( 4774 ASSUME_TAC S_SEM___CLOCK_OCCURRENCE THEN 4775 Q_SPECL_NO_ASSUM 0 [`s`, `v1`, `c`] THEN 4776 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 4777 ASM_REWRITE_TAC[] THEN 4778 Cases_on `v1` THEN FULL_SIMP_TAC list_ss [] 4779 ) THEN 4780 UNDISCH_HD_TAC THEN 4781 4782 `EL (m1 - 1) v1 = EL (m1 - 1) (v1 <> v2)` by ASM_SIMP_TAC list_ss [EL_APPEND1] THEN 4783 ASM_SIMP_TAC std_ss [] THEN 4784 GSYM_NO_TAC 10 (* SEL REC = v1 <> v2*) THEN 4785 ASM_SIMP_TAC arith_ss [EL_SEL_REC] THEN 4786 4787 REPEAT STRIP_TAC THEN CCONTR_TAC THEN 4788 Q_SPEC_NO_ASSUM 13 `m1 - 1` THEN 4789 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 4790 CLEAN_ASSUMPTIONS_TAC THEN 4791 `m1 + n0 - 1 = (n0 + (m1 - 1))` by DECIDE_TAC THEN 4792 METIS_TAC[B_SEM_def] 4793 ) THEN 4794 4795 Q_TAC EXISTS_TAC `SEL_REC (m1 - k) (n0 + k) p` THEN 4796 Q_TAC EXISTS_TAC `SEL_REC m2 ((n0 + k) + (m1 - k)) p` THEN 4797 REWRITE_TAC [GSYM SEL_REC_SPLIT] THEN 4798 `(m2 + (m1 - k) = m) /\ ((n0 + k + (m1 - k)) = n0 + m1)` by DECIDE_TAC THEN 4799 ASM_REWRITE_TAC[] THEN 4800 4801 UNDISCH_NO_TAC 12 (*SEL REC (m + k) n0 p = v1 <> v2*) THEN 4802 SUBGOAL_TAC `SEL_REC (m+k) n0 p = 4803 SEL_REC m1 n0 p <> SEL_REC m2 (n0 + m1) p` THEN1 ( 4804 METIS_TAC[SEL_REC_SPLIT, ADD_COMM] 4805 ) THEN 4806 4807 ASM_SIMP_TAC arith_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC], 4808 4809 4810 4811 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4812 REPEAT STRIP_TAC THEN 4813 4814 Q.ABBREV_TAC `m1 = LENGTH v1` THEN 4815 Q.ABBREV_TAC `m2 = LENGTH v2` THEN 4816 SUBGOAL_TAC `m + k = (m1 + 1) + m2` THEN1 ( 4817 `LENGTH (SEL_REC (m + k) n0 p) = LENGTH (v1 <> [l] <> v2)` by PROVE_TAC[] THEN 4818 UNDISCH_HD_TAC THEN 4819 ASM_SIMP_TAC list_ss [LENGTH_SEL_REC] 4820 ) THEN 4821 SUBGOAL_TAC `m1 >= k` THEN1 ( 4822 ASSUME_TAC S_SEM___CLOCK_OCCURRENCE THEN 4823 Q_SPECL_NO_ASSUM 0 [`s`, `v1<>[l]`, `c`] THEN 4824 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 4825 ASM_SIMP_TAC list_ss [] 4826 ) THEN 4827 UNDISCH_HD_TAC THEN 4828 4829 4830 `EL m1 (v1 <> [l]) = EL m1 (v1 <> [l] <> v2)` by ASM_SIMP_TAC list_ss [EL_APPEND1] THEN 4831 ASM_SIMP_TAC list_ss [] THEN 4832 GSYM_NO_TAC 9 (* SEL REC = v1 <> [l] <> v2*) THEN 4833 ASM_SIMP_TAC arith_ss [EL_SEL_REC] THEN 4834 4835 REPEAT STRIP_TAC THEN CCONTR_TAC THEN 4836 Q_SPEC_NO_ASSUM 12 `m1` THEN 4837 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 4838 CLEAN_ASSUMPTIONS_TAC THEN 4839 METIS_TAC[B_SEM_def, ADD_COMM] 4840 ) THEN 4841 4842 Q_TAC EXISTS_TAC `SEL_REC (m1 - k) (n0 + k) p` THEN 4843 Q_TAC EXISTS_TAC `SEL_REC m2 ((n0 + k) + ((m1 - k)+ 1)) p` THEN 4844 Q_TAC EXISTS_TAC `l` THEN 4845 4846 SUBGOAL_TAC `[l] = SEL_REC (1:num) (n0 + m1) p` THEN1 ( 4847 MATCH_RIGHT_EQ_MP_TAC LIST_EQ_REWRITE THEN 4848 SIMP_TAC list_ss [LENGTH_SEL_REC] THEN 4849 REPEAT STRIP_TAC THEN 4850 rename1 `EL n [l]` THEN 4851 `n = 0` by DECIDE_TAC THEN 4852 ASM_SIMP_TAC list_ss [EL_SEL_REC] THEN 4853 `EL m1 (SEL_REC (m + k) n0 p) = EL m1 (v1 <> [l] <> v2)` by METIS_TAC[] THEN 4854 UNDISCH_HD_TAC THEN 4855 ASM_SIMP_TAC list_ss [EL_SEL_REC, EL_APPEND1, EL_APPEND2] 4856 ) THEN 4857 4858 SUBGOAL_TAC `(v1 = SEL_REC m1 n0 p) /\ 4859 (v2 = SEL_REC m2 (n0 + m1 + 1) p)` THEN1 ( 4860 SUBGOAL_TAC `SEL_REC (m+k) n0 p = 4861 SEL_REC m1 n0 p <> [l] <> SEL_REC m2 (n0 + m1 + 1) p` THEN1 ( 4862 GSYM_NO_TAC 10 (*SEL_REC (m+k) n0 = ...*) THEN 4863 `m1 + 1 + m2 = m2 + 1 + m1` by DECIDE_TAC THEN 4864 ASM_REWRITE_TAC[] THEN 4865 ASM_REWRITE_TAC[SEL_REC_SPLIT] THEN 4866 SIMP_TAC list_ss [] 4867 ) THEN 4868 UNDISCH_NO_TAC 11 (*SEL_REC (m+k) n0 = ...*) THEN 4869 ASM_SIMP_TAC arith_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC, LENGTH_APPEND] 4870 ) THEN 4871 4872 REPEAT STRIP_TAC THENL [ 4873 `(n0 + (m1 + 1 + k)) = n0 + (1 + (m1 + k))` by DECIDE_TAC THEN 4874 `(n0 + m1 = ((n0 + k) + (m1 - k))) /\ 4875 ((n0 + k + (m1 - k + 1)) = ((n0 + k) + (1 + (m1 - k))))` by 4876 ASM_SIMP_TAC arith_ss [] THEN 4877 ASM_REWRITE_TAC[GSYM SEL_REC_SPLIT] THEN 4878 NTAC 2 WEAKEN_HD_TAC THEN 4879 `(m2 + (1 + (m1 - k))) = m` by DECIDE_TAC THEN 4880 ASM_REWRITE_TAC[], 4881 4882 4883 UNDISCH_NO_TAC 11 (*S_SEM v1 <> [l] *) THEN 4884 ASM_REWRITE_TAC [GSYM SEL_REC_SPLIT] THEN 4885 `n0 + m1 = ((n0 + k) + (m1 - k))` by DECIDE_TAC THEN 4886 ASM_REWRITE_TAC [GSYM SEL_REC_SPLIT] THEN 4887 WEAKEN_HD_TAC THEN 4888 `((1 + (m1 - k)) > 0) /\ ((((1 + (m1 -k)) + k)) = (1 + m1))` by DECIDE_TAC THEN 4889 METIS_TAC[], 4890 4891 FULL_SIMP_TAC arith_ss [] 4892 ], 4893 4894 4895 4896 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4897 METIS_TAC[], 4898 4899 4900 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4901 METIS_TAC[], 4902 4903 4904 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4905 REPEAT STRIP_TAC THEN 4906 `LENGTH (SEL_REC (m + k) n0 p) = LENGTH ([]:'a letter list)` by PROVE_TAC[] THEN 4907 FULL_SIMP_TAC list_ss [LENGTH_SEL_REC], 4908 4909 4910 SIMP_TAC std_ss [S_SEM_def, S_CLOCK_FREE_def] THEN 4911 REPEAT STRIP_TAC THEN 4912 SUBGOAL_TAC `?h l. (CONCAT vlist = CONCAT (h::l)) /\ (!e. MEM e (h::l) ==> MEM e vlist) /\ (LENGTH h > 0)` THEN1 ( 4913 Induct_on `vlist` THENL [ 4914 REPEAT STRIP_TAC THEN 4915 `LENGTH (SEL_REC (m+k) n0 p) = LENGTH (CONCAT ([]:'a letter list list))` by PROVE_TAC[] THEN 4916 FULL_SIMP_TAC list_ss [CONCAT_def, LENGTH_SEL_REC], 4917 4918 GEN_TAC THEN 4919 Cases_on `h = []` THENL [ 4920 FULL_SIMP_TAC list_ss [CONCAT_def] THEN 4921 METIS_TAC[], 4922 4923 FULL_SIMP_TAC list_ss [CONCAT_def] THEN 4924 REMAINS_TAC `LENGTH h > 0` THEN1 METIS_TAC[] THEN 4925 Cases_on `h` THEN FULL_SIMP_TAC list_ss [] 4926 ] 4927 ] 4928 ) THEN 4929 FULL_SIMP_TAC list_ss [listTheory.EVERY_MEM, CONCAT_def] THEN 4930 4931 4932 Q.ABBREV_TAC `m1 = LENGTH h` THEN 4933 Q.ABBREV_TAC `m2 = LENGTH (CONCAT l)` THEN 4934 `k + m = m1 + m2` by METIS_TAC[LENGTH_SEL_REC, LENGTH_APPEND] THEN 4935 4936 4937 SUBGOAL_TAC `m1 > k` THEN1 ( 4938 ASSUME_TAC S_SEM___CLOCK_OCCURRENCE THEN 4939 Q_SPECL_NO_ASSUM 0 [`s`, `h`, `c`] THEN 4940 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 4941 REPEAT STRIP_TAC THENL [ 4942 PROVE_TAC[], 4943 Cases_on `h` THEN FULL_SIMP_TAC list_ss [], 4944 ASM_REWRITE_TAC[] 4945 ] 4946 ) THEN 4947 UNDISCH_HD_TAC THEN 4948 4949 `EL (m1 - 1) h = EL (m1 - 1) (h<>(CONCAT l))` by ASM_SIMP_TAC list_ss [EL_APPEND1] THEN 4950 ASM_SIMP_TAC std_ss [] THEN 4951 GSYM_NO_TAC 10 (* SEL REC = h <> concat l*) THEN 4952 ASM_SIMP_TAC arith_ss [EL_SEL_REC] THEN 4953 4954 REPEAT STRIP_TAC THEN CCONTR_TAC THEN 4955 Q_SPEC_NO_ASSUM 13 `m1 - 1` THEN 4956 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 4957 CLEAN_ASSUMPTIONS_TAC THEN 4958 `m1 - 1 + n0 = (m1 + n0 - 1)` by DECIDE_TAC THEN 4959 METIS_TAC[B_SEM_def] 4960 ) THEN 4961 4962 Q_TAC EXISTS_TAC `(SEL_REC (m1 - k) (k+n0) p)::l` THEN 4963 ASM_SIMP_TAC list_ss [DISJ_IMP_THM, CONCAT_def] THEN 4964 4965 GSYM_NO_TAC 10 (*SEL REC m (n0 + k) p = v1 <> v2*) THEN 4966 UNDISCH_HD_TAC THEN 4967 SUBGOAL_TAC `SEL_REC (m1 + m2) n0 p = 4968 SEL_REC m1 n0 p <> SEL_REC m2 (n0 + m1) p` THEN1 ( 4969 METIS_TAC[SEL_REC_SPLIT, ADD_COMM] 4970 ) THEN 4971 4972 ASM_SIMP_TAC list_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC, CONCAT_def] THEN 4973 REPEAT STRIP_TAC THEN 4974 `((m1 + n0) = ((k + n0) + (m1 - k))) /\ 4975 ((m2 + (m1 - k)) = m)` by DECIDE_TAC THEN 4976 ASM_REWRITE_TAC[GSYM SEL_REC_SPLIT], 4977 4978 4979 SIMP_TAC std_ss [S_CLOCK_FREE_def] 4980]); 4981 4982 4983 4984val S_SEM___EXTEND_RESTRICT_NO_CLOCK_CYCLES = 4985 store_thm 4986 ("S_SEM___EXTEND_RESTRICT_NO_CLOCK_CYCLES", 4987 4988``!s k m n0 c p. 4989((!l. (l < k) ==> ((B_SEM (ELEM p (n0 + l)) (B_NOT c)) /\ ?s'. (ELEM p (n0 + l) = STATE s'))) /\ 4990 (m > 0) /\ 4991 (S_CLOCK_FREE s)) ==> 4992 ((S_SEM (SEL_REC m (n0+k) p) c s) = (S_SEM (SEL_REC (m+k) n0 p) c s))``, 4993 4994 METIS_TAC[S_SEM___RESTRICT_NO_CLOCK_CYCLES, 4995 S_SEM___EXTEND_NO_CLOCK_CYCLES]); 4996 4997 4998 4999val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_CAT = 5000 store_thm 5001 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_CAT", 5002 5003``!s1 s2 f c. (S_CLOCK_FREE s1 /\ S_CLOCK_FREE s2 /\ 5004 (~(S_SEM [] c s1) /\ ~(S_SEM [] c s2))) ==> 5005 5006 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 5007 (F_CLOCK_COMP c (F_SUFFIX_IMP (S_CAT(s1, s2), f))) 5008 (F_CLOCK_COMP c (F_SUFFIX_IMP (s1, (F_WEAK_X (F_SUFFIX_IMP (s2, f))))))``, 5009 5010SIMP_TAC (std_ss++resq_SS) [UF_SEM_def, IN_LESSX_REWRITE, UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def, 5011IS_INFINITE_TOP_BOTTOM_FREE_PATH___COMPLEMENT, 5012F_CLOCK_COMP_def, S_CLOCK_COMP_def, F_U_CLOCK_def, 5013RESTN_RESTN, F_WEAK_X_def] THEN 5014REPEAT STRIP_TAC THEN 5015FULL_SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, LENGTH_def, US_SEM_def, 5016ELEM_def, LS, GT, LENGTH_SEL, SEL_def, RESTN_INFINITE, 5017COMPLEMENT_def, combinTheory.o_DEF, 5018GSYM S_CLOCK_COMP_CORRECT, 5019IN_LESSX_REWRITE, LS, xnum_distinct, 5020HEAD_def, IN_LESS] THEN 5021SUBGOAL_TAC `!x. COMPLEMENT_LETTER (p x) = p x` THEN1 ( 5022 GEN_TAC THEN 5023 `?s. p x = STATE s` by METIS_TAC[] THEN 5024 ASM_REWRITE_TAC[COMPLEMENT_LETTER_def] 5025) THEN 5026ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 5027 5028EQ_TAC THEN REPEAT STRIP_TAC THENL [ 5029 LEFT_DISJ_TAC THEN 5030 RIGHT_DISJ_TAC THEN 5031 GEN_TAC THEN 5032 LEFT_DISJ_TAC THEN 5033 RIGHT_DISJ_TAC THEN 5034 GEN_TAC THEN 5035 RIGHT_DISJ_TAC THEN 5036 FULL_SIMP_TAC std_ss [] THEN 5037 5038 Q_SPEC_NO_ASSUM 6 `j' + (k + (1 + k')) + j` THEN 5039 PROVE_CONDITION_NO_ASSUM 0 THENL [ 5040 ALL_TAC, 5041 FULL_SIMP_TAC arith_ss [] 5042 ] THEN 5043 5044 SUBGOAL_TAC `k = 0` THEN1 ( 5045 ASSUME_TAC S_SEM___CLOCK_OCCURRENCE THEN 5046 Q_SPECL_NO_ASSUM 0 [`s1`, `SEL_REC (j + 1) 0 (INFINITE p)`, `c`] THEN 5047 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 5048 ASM_SIMP_TAC list_ss [prove (``j + 1 = SUC j``, DECIDE_TAC), 5049 SEL_REC_def] 5050 ) THEN 5051 UNDISCH_HD_TAC THEN 5052 SIMP_TAC std_ss [LENGTH_SEL_REC, EL_SEL_REC, ELEM_INFINITE] THEN 5053 STRIP_TAC THEN 5054 CCONTR_TAC THEN 5055 `0 < k` by DECIDE_TAC THEN 5056 `B_SEM (p (0 + j)) (B_NOT c)` by METIS_TAC[] THEN 5057 SIMP_ALL_TAC std_ss [] THEN 5058 METIS_TAC[B_SEM_def] 5059 ) THEN 5060 FULL_SIMP_TAC std_ss [] THEN 5061 5062 Q_TAC EXISTS_TAC `SEL_REC (j + 1) 0 (INFINITE p)` THEN 5063 Q_TAC EXISTS_TAC `SEL_REC (k' + j' + 1) (0 + (j + 1)) (INFINITE p)` THEN 5064 REWRITE_TAC[GSYM SEL_REC_SPLIT] THEN 5065 SIMP_TAC arith_ss [] THEN 5066 5067 CONJ_TAC THENL [ 5068 METIS_TAC[], 5069 5070 5071 ASSUME_TAC S_SEM___EXTEND_NO_CLOCK_CYCLES THEN 5072 Q_SPECL_NO_ASSUM 0 [`s2`, `k'`, `j' + 1`, `j+1`, `c`, `INFINITE p`] THEN 5073 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 5074 ASM_SIMP_TAC arith_ss [ELEM_INFINITE] THEN 5075 REPEAT STRIP_TAC THENL [ 5076 `j + (l + 1) = 1 + l + j` by DECIDE_TAC THEN 5077 PROVE_TAC[], 5078 5079 `(j + (k' + 1)) = (0 + (j + (k' + 1)))` by DECIDE_TAC THEN 5080 ONCE_ASM_REWRITE_TAC[] THEN 5081 REWRITE_TAC[GSYM SEL_REC_RESTN] THEN 5082 WEAKEN_HD_TAC THEN 5083 FULL_SIMP_TAC arith_ss [RESTN_INFINITE] 5084 ] 5085 ) THEN 5086 FULL_SIMP_TAC arith_ss [] 5087 ], 5088 5089 5090 5091 `?k. k = PRE (LENGTH v1)` by METIS_TAC[] THEN 5092 `?k'. k' = PRE (LENGTH v2)` by METIS_TAC[] THEN 5093 5094 SUBGOAL_TAC `LENGTH v1 > 0` THEN1 ( 5095 Cases_on `v1` THENL [ 5096 PROVE_TAC[], 5097 SIMP_TAC list_ss [] 5098 ] 5099 ) THEN 5100 5101 SUBGOAL_TAC `LENGTH v2 > 0` THEN1 ( 5102 Cases_on `v2` THENL [ 5103 PROVE_TAC[], 5104 SIMP_TAC list_ss [] 5105 ] 5106 ) THEN 5107 5108 `(?l. k + 1 = l) /\ (?l'. k' + 1 = l')` by METIS_TAC[] THEN 5109 5110 SUBGOAL_TAC `j + 1 = l' + l` THEN1 ( 5111 `j + 1 = LENGTH (v1 <> v2)` by METIS_TAC[LENGTH_SEL_REC] THEN 5112 ASM_SIMP_TAC std_ss [] THEN 5113 SIMP_TAC list_ss [] THEN 5114 DECIDE_TAC 5115 ) THEN 5116 FULL_SIMP_TAC std_ss [] THEN 5117 5118 SUBGOAL_TAC `(v1 = SEL_REC l 0 (INFINITE p)) /\ 5119 (v2 = SEL_REC l' l (INFINITE p))` THEN1 ( 5120 `LENGTH v1 = l` by DECIDE_TAC THEN 5121 `LENGTH v2 = l'` by DECIDE_TAC THEN 5122 FULL_SIMP_TAC std_ss [SEL_REC_SPLIT, APPEND_LENGTH_EQ,LENGTH_SEL_REC] 5123 ) THEN 5124 NTAC 2 (WEAKEN_NO_TAC 7) (*Def k, k'*) THEN 5125 5126 Q_SPEC_NO_ASSUM 10 `k` THEN 5127 PROVE_CONDITION_NO_ASSUM 0 THEN1 (ASM_SIMP_TAC arith_ss [] THEN PROVE_TAC[]) THEN 5128 Q_SPEC_NO_ASSUM 0 `0:num` THEN 5129 FULL_SIMP_TAC std_ss [] THEN1 ( 5130 ASSUME_TAC S_SEM___CLOCK_OCCURRENCE THEN 5131 Q_SPECL_NO_ASSUM 0 [`s1`, `SEL_REC l 0 (INFINITE p)`, `c`] THEN 5132 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 5133 ASM_REWRITE_TAC[] THEN 5134 GSYM_NO_TAC 5 (*Def l*) THEN 5135 ASM_SIMP_TAC list_ss [SEL_REC_def, prove (``k + 1 = SUC k``, DECIDE_TAC)] 5136 ) THEN 5137 UNDISCH_HD_TAC THEN 5138 5139 ASM_SIMP_TAC arith_ss [LENGTH_SEL_REC, EL_SEL_REC, ELEM_INFINITE] THEN 5140 `l - 1 = k` by DECIDE_TAC THEN 5141 ASM_REWRITE_TAC[] 5142 ) THEN 5143 5144 SUBGOAL_TAC `B_SEM (p (1 + k' + k)) c` THEN1 ( 5145 ASSUME_TAC S_SEM___CLOCK_OCCURRENCE THEN 5146 Q_SPECL_NO_ASSUM 0 [`s2`, `SEL_REC l' l (INFINITE p)`, `c`] THEN 5147 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 5148 ASM_REWRITE_TAC[] THEN 5149 GSYM_NO_TAC 4 (*Def l'*) THEN 5150 ONCE_REWRITE_TAC[prove (``l:num = 0 + l``, DECIDE_TAC)] THEN 5151 REWRITE_TAC[GSYM SEL_REC_RESTN] THEN 5152 ASM_SIMP_TAC list_ss [SEL_REC_def, prove (``k' + 1 = SUC k'``, DECIDE_TAC)] 5153 ) THEN 5154 UNDISCH_HD_TAC THEN 5155 5156 ASM_SIMP_TAC arith_ss [LENGTH_SEL_REC, EL_SEL_REC, ELEM_INFINITE] THEN 5157 `l + l' - 1 = k + l'` by DECIDE_TAC THEN 5158 ASM_REWRITE_TAC[] 5159 ) THEN 5160 Q_EXISTS_LEAST_TAC `?m. B_SEM (p (1 + m + k)) c` THEN 5161 CLEAN_ASSUMPTIONS_TAC THEN 5162 5163 5164 Q_SPEC_NO_ASSUM 3 `m` THEN 5165 FULL_SIMP_TAC std_ss [] THENL [ 5166 PROVE_TAC[], 5167 ALL_TAC, 5168 METIS_TAC[B_SEM_def] 5169 ] THEN 5170 5171 SUBGOAL_TAC `?j'. m + j' = k'` THEN1 ( 5172 `~(k' < m)` by PROVE_TAC[] THEN 5173 Q_TAC EXISTS_TAC `k' - m` THEN 5174 DECIDE_TAC 5175 ) THEN 5176 5177 Q_SPEC_NO_ASSUM 1 `j'` THEN 5178 CLEAN_ASSUMPTIONS_TAC THENL [ 5179 ALL_TAC, 5180 5181 UNDISCH_HD_TAC THEN 5182 `!n:num. n + j' + (1 + m) + k = n + j` by DECIDE_TAC THEN 5183 ASM_SIMP_TAC std_ss [] 5184 ] THEN 5185 5186 ASSUME_TAC S_SEM___EXTEND_RESTRICT_NO_CLOCK_CYCLES THEN 5187 Q_SPECL_NO_ASSUM 0 [`s2`, `m`, `j'+1`, `1 + k`, `c`, `INFINITE p`] THEN 5188 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 5189 ASM_SIMP_TAC arith_ss [ELEM_INFINITE] THEN 5190 REPEAT STRIP_TAC THEN 5191 `(l + l'') = 1 + l'' + k` by DECIDE_TAC THEN 5192 METIS_TAC[B_SEM_def] 5193 ) THEN 5194 5195 SUBGOAL_TAC `SEL_REC (j' + 1) (1+k+m) (INFINITE p) = 5196 SEL_REC (j' + 1) 0 (INFINITE (\n. p (n + (1 + m) + k)))` THEN1 ( 5197 `(1 + k + m) = (0 + (1 + k + m))` by DECIDE_TAC THEN 5198 ONCE_ASM_REWRITE_TAC[] THEN 5199 REWRITE_TAC[GSYM SEL_REC_RESTN] THEN 5200 WEAKEN_HD_TAC THEN 5201 SIMP_TAC arith_ss [RESTN_INFINITE] 5202 ) THEN 5203 NTAC 2 (UNDISCH_NO_TAC 1) THEN 5204 `j' + (m + 1) = l'` by DECIDE_TAC THEN 5205 ASM_SIMP_TAC arith_ss [] 5206]); 5207 5208 5209 5210val UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL_BIGCAT = 5211 store_thm 5212 ("UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL_BIGCAT", 5213 5214``(!f:'a fl b c . 5215 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 5216 (F_CLOCK_COMP c (F_SUFFIX_IMP (S_BOOL_BIGCAT [b], f))) 5217 (F_W_CLOCK c (F_IMPLIES (F_STRONG_BOOL b,F_CLOCK_COMP c f))) 5218 ) /\ 5219 (!f:'a fl b1 b2 l c. UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE 5220 (F_CLOCK_COMP c (F_SUFFIX_IMP (S_BOOL_BIGCAT (b1::b2::l), f))) 5221 (F_CLOCK_COMP c (F_SUFFIX_IMP (S_BOOL b1, F_WEAK_X (F_SUFFIX_IMP (S_BOOL_BIGCAT (b2::l), f))))))``, 5222 5223 REPEAT STRIP_TAC THENL [ 5224 SIMP_TAC std_ss [S_BOOL_BIGCAT_def, 5225 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL], 5226 5227 SIMP_TAC std_ss [S_BOOL_BIGCAT_def] THEN 5228 ASSUME_TAC UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_CAT THEN 5229 Q_SPECL_NO_ASSUM 0 [`S_BOOL b1`, `S_BOOL_BIGCAT (b2::l)`, `f`, `c`] THEN 5230 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 5231 SIMP_TAC list_ss [S_SEM_def, S_CLOCK_FREE_def, CLOCK_TICK_def] THEN 5232 Induct_on `l` THENL [ 5233 SIMP_TAC list_ss [S_SEM_def, S_BOOL_BIGCAT_def, S_CLOCK_FREE_def, 5234 CLOCK_TICK_def], 5235 5236 Cases_on `l` THEN 5237 FULL_SIMP_TAC list_ss [S_SEM_def, S_BOOL_BIGCAT_def, S_CLOCK_FREE_def, 5238 CLOCK_TICK_def] 5239 ] 5240 ) THEN 5241 ASSUME_TAC UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___F_SUFFIX_IMP___CLOCK_BOOL THEN 5242 FULL_SIMP_TAC std_ss [UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE_def] 5243 ]); 5244 5245 5246 5247 5248val _ = export_theory(); 5249