1 2 3(*****************************************************************************) 4(* Definition and validation of the "projection view" of clocked semantics *) 5(* ------------------------------------------------------------------------- *) 6(* *) 7(* Started: Tue Mar 9, 2004 *) 8(*****************************************************************************) 9 10(*****************************************************************************) 11(* START BOILERPLATE *) 12(*****************************************************************************) 13 14(****************************************************************************** 15* Load theories 16* (commented out for compilation) 17******************************************************************************) 18(* 19quietdec := true; 20loadPath 21 := 22 "../official-semantics" :: "../../regexp" :: "../../path" :: !loadPath; 23map load 24 ["UnclockedSemanticsTheory", 25 "SyntacticSugarTheory", "ClockedSemanticsTheory", "RewritesTheory", "whileTheory", 26 "rich_listTheory", "intLib", "res_quanLib", "res_quanTheory", 27 "LemmasTheory","RewritesPropertiesTheory"]; 28open FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 29 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 30 arithmeticTheory whileTheory listTheory rich_listTheory 31 res_quanLib res_quanTheory 32 arithmeticTheory listTheory whileTheory rich_listTheory res_quanLib res_quanTheory 33 ClockedSemanticsTheory LemmasTheory RewritesPropertiesTheory; 34val _ = intLib.deprecate_int(); 35quietdec := false; 36*) 37 38 39(****************************************************************************** 40* Boilerplate needed for compilation 41******************************************************************************) 42open HolKernel Parse boolLib bossLib; 43 44(****************************************************************************** 45* Open theories 46******************************************************************************) 47open FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 48 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 49 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory 50 whileTheory ClockedSemanticsTheory LemmasTheory RewritesPropertiesTheory 51 arithmeticTheory listTheory whileTheory rich_listTheory res_quanLib 52 res_quanTheory ClockedSemanticsTheory LemmasTheory 53 RewritesPropertiesTheory; 54 55(****************************************************************************** 56* Set default parsing to natural numbers rather than integers 57******************************************************************************) 58val _ = intLib.deprecate_int(); 59 60(*****************************************************************************) 61(* END BOILERPLATE *) 62(*****************************************************************************) 63 64(****************************************************************************** 65* Start a new theory called Project 66******************************************************************************) 67val _ = new_theory "Projection"; 68val _ = ParseExtras.temp_loose_equality() 69 70(****************************************************************************** 71* A simpset fragment to rewrite away quantifiers restricted with :: (a to b) 72******************************************************************************) 73val resq_SS = 74 simpLib.merge_ss 75 [res_quanTools.resq_SS, 76 rewrites 77 [IN_DEF,LESS_def,LESSX_def,LENGTH_def]]; 78 79(****************************************************************************** 80* CLOCK c s is true is clock c is true in state s 81******************************************************************************) 82 83val CLOCK_def = Define `CLOCK c s = B_SEM s c`; 84 85open FinitePSLPathTheory; 86 87val LIST_PROJ_def = 88 Define `LIST_PROJ l c = FILTER (CLOCK c) l`; 89 90val LENGTH_FILTER_NON_EMPTY = 91 store_thm 92 ("LENGTH_FILTER_NON_EMPTY", 93 ``!l P. (LENGTH(FILTER P l) > 0) ==> LENGTH l > 0``, 94 Induct 95 THEN RW_TAC list_ss []); 96 97val LENGTH_FILTER_1_NON_EMPTY = 98 store_thm 99 ("LENGTH_FILTER_1_NON_EMPTY", 100 ``!l P. (LENGTH(FILTER P l) = 1) ==> LENGTH l > 0``, 101 Induct 102 THEN RW_TAC list_ss []); 103 104val FILTER_NON_EMPTY = 105 store_thm 106 ("FILTER_NON_EMPTY", 107 ``!l P. LENGTH l > 0 /\ (?n. n < LENGTH l /\ P(EL n l)) ==> ~(FILTER P l = [])``, 108 Induct 109 THEN RW_TAC list_ss [] 110 THEN Cases_on `n` 111 THEN RW_TAC list_ss [] 112 THEN FULL_SIMP_TAC list_ss [] 113 THEN PROVE_TAC[]); 114 115val LAST_FILTER_NON_EMPTY = 116 store_thm 117 ("LAST_FILTER_NON_EMPTY", 118 ``!l P. LENGTH l > 0 /\ P(LAST l) ==> ~(FILTER P l = [])``, 119 Induct 120 THEN RW_TAC list_ss [] 121 THEN Cases_on `l` 122 THEN RW_TAC list_ss [] 123 THEN FULL_SIMP_TAC list_ss [LAST_CONS] 124 THEN PROVE_TAC[]); 125 126val LENGTH_APPEND_GREATER_1 = 127 store_thm 128 ("LENGTH_APPEND_GREATER_1", 129 ``LENGTH(l1 <> [x] <> l2 <> [y]) > 1``, 130 RW_TAC list_ss []); 131 132val FIRSTN_SUC_EL = 133 store_thm 134 ("FIRSTN_SUC_EL", 135 ``!l n. n < LENGTH l ==> (FIRSTN (SUC n) l = FIRSTN n l <> [EL n l])``, 136 Induct 137 THEN Cases_on `n` 138 THEN RW_TAC list_ss [FIRSTN]); 139 140val FIRSTN_LASTN_SPLIT = 141 store_thm 142 ("FIRSTN_LASTN_SPLIT", 143 ``!n l. n < LENGTH l 144 ==> 145 (l = FIRSTN n l <> [EL n l] <> BUTFIRSTN (SUC n) l)``, 146 RW_TAC list_ss [GSYM FIRSTN_SUC_EL,APPEND_FIRSTN_BUTFIRSTN]); 147 148val LENGTH_FILTER_1_NOT = 149 store_thm 150 ("LENGTH_FILTER_1_NOT", 151 ``!l P. P(LAST l) /\ (LENGTH(FILTER P l) = 1) 152 ==> !i. i < LENGTH l - 1 ==> ~P(EL i l)``, 153 RW_TAC list_ss [] 154 THEN Cases_on `P (EL i l)` 155 THEN RW_TAC list_ss [] 156 THEN IMP_RES_TAC LENGTH_FILTER_1_NON_EMPTY 157 THEN `~(l=[])` by PROVE_TAC[LENGTH_NIL,DECIDE``n>0 ==> ~(n=0)``] 158 THEN `i <= LENGTH l` by DECIDE_TAC 159 THEN IMP_RES_TAC APPEND_FRONT_LAST 160 THEN IMP_RES_TAC LENGTH_BUTLAST 161 THEN `i < LENGTH(BUTLAST l)` by DECIDE_TAC 162 THEN IMP_RES_TAC FIRSTN_LASTN_SPLIT 163 THEN `i < PRE(LENGTH l)` by DECIDE_TAC 164 THEN IMP_RES_TAC EL_BUTLAST 165 THEN `l = (FIRSTN i (BUTLAST l) <> [EL i l] <> 166 BUTFIRSTN (SUC i) (BUTLAST l)) <> [LAST l]` 167 by PROVE_TAC[] 168 THEN ASSUM_LIST 169 (fn thl => 170 ASSUME_TAC 171 (SIMP_RULE list_ss [el 11 thl,el 14 thl,FILTER_APPEND] 172 (Q.AP_TERM `FILTER P` (el 1 thl)))) 173 THEN `LENGTH(FILTER P l) > 1` by PROVE_TAC[LENGTH_APPEND_GREATER_1] 174 THEN DECIDE_TAC); 175 176val TOP_FREE_def = 177 Define 178 `(TOP_FREE[] = T) /\ 179 (TOP_FREE(TOP::v) = F) /\ 180 (TOP_FREE(BOTTOM::v) = TOP_FREE v) /\ 181 (TOP_FREE((STATE s)::v) = TOP_FREE v)`; 182 183val TOP_FREE_APPEND = 184 store_thm 185 ("TOP_FREE_APPEND", 186 ``!v1 v2. TOP_FREE (v1 <> v2) = TOP_FREE v1 /\ TOP_FREE v2``, 187 Induct 188 THEN RW_TAC list_ss [TOP_FREE_def] 189 THEN Cases_on `h` 190 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def]); 191 192val TOP_FREE_EL = 193 store_thm 194 ("TOP_FREE_EL", 195 ``!l. TOP_FREE l = !i. i < LENGTH l ==> ~(EL i l = TOP)``, 196 Induct 197 THEN RW_TAC list_ss [TOP_FREE_def] 198 THEN EQ_TAC 199 THEN RW_TAC list_ss [TOP_FREE_def] 200 THENL 201 [Cases_on `i` 202 THEN Cases_on `h` 203 THEN RW_TAC list_ss [] 204 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def], 205 Cases_on `h` 206 THEN RW_TAC list_ss [] 207 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def] 208 THENL 209 [POP_ASSUM 210 (fn th => 211 STRIP_ASSUME_TAC(SIMP_RULE list_ss [] (SPEC ``0`` th))), 212 POP_ASSUM 213 (fn th => 214 STRIP_ASSUME_TAC(GEN_ALL(SIMP_RULE list_ss [] (SPEC ``SUC i`` th)))), 215 POP_ASSUM 216 (fn th => 217 STRIP_ASSUME_TAC(GEN_ALL(SIMP_RULE list_ss [] (SPEC ``SUC i`` th))))]]); 218 219 220val BOTTOM_FREE_EL = 221 store_thm 222 ("BOTTOM_FREE_EL", 223 ``!l. BOTTOM_FREE l = !i. i < LENGTH l ==> ~(EL i l = BOTTOM)``, 224 Induct 225 THEN RW_TAC list_ss [BOTTOM_FREE_def] 226 THEN EQ_TAC 227 THEN RW_TAC list_ss [BOTTOM_FREE_def] 228 THENL 229 [Cases_on `i` 230 THEN Cases_on `h` 231 THEN RW_TAC list_ss [] 232 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def], 233 Cases_on `h` 234 THEN RW_TAC list_ss [] 235 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def] 236 THENL 237 [POP_ASSUM 238 (fn th => 239 STRIP_ASSUME_TAC(GEN_ALL(SIMP_RULE list_ss [] (SPEC ``SUC i`` th)))), 240 POP_ASSUM 241 (fn th => 242 STRIP_ASSUME_TAC(SIMP_RULE list_ss [] (SPEC ``0`` th))), 243 POP_ASSUM 244 (fn th => 245 STRIP_ASSUME_TAC(GEN_ALL(SIMP_RULE list_ss [] (SPEC ``SUC i`` th))))]]); 246 247val CLOCK_TICK_LENGTH_1 = 248 store_thm 249 ("CLOCK_TICK_LENGTH_1", 250 ``!l c. TOP_FREE l /\ CLOCK_TICK l c 251 ==> 252 (LENGTH (FILTER (CLOCK c) l) = 1)``, 253 RW_TAC (list_ss++resq_SS) [CLOCK_TICK_def,CLOCK_def,ELEM_EL] 254 THEN `~(LENGTH l = 0)` by DECIDE_TAC 255 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 256 THEN IMP_RES_TAC APPEND_FRONT_LAST 257 THEN POP_ASSUM(fn th => ONCE_REWRITE_TAC[GSYM th]) 258 THEN `LENGTH l >= 1` by DECIDE_TAC 259 THEN RW_TAC list_ss [GSYM EL_PRE_LENGTH,FILTER_APPEND,LENGTH_APPEND,CLOCK_def] 260 THEN Induct_on `l` 261 THEN RW_TAC list_ss [] 262 THEN Cases_on `l = []` 263 THEN RW_TAC list_ss [] 264 THEN ASM_REWRITE_TAC [FRONT_DEF] 265 THEN `~(LENGTH l = 0)` by PROVE_TAC[LENGTH_NIL] 266 THEN `0 < LENGTH l` by DECIDE_TAC 267 THEN RES_TAC 268 THEN FULL_SIMP_TAC list_ss [CLOCK_def] 269 THEN Cases_on `h` 270 THEN FULL_SIMP_TAC list_ss [B_SEM_def,TOP_FREE_def,EL_CONS,DECIDE``PRE n = n-1``] 271 THEN ASSUM_LIST 272 (fn thl => 273 ASSUME_TAC 274 (Q.GEN `i` 275 (SIMP_RULE list_ss 276 [DECIDE ``SUC n < m:num = n < m-1``] (Q.SPEC `SUC i` (el 5 thl))))) 277 THEN PROVE_TAC[]); 278 279val S_CLOCK_LAST = 280 store_thm 281 ("S_CLOCK_LAST", 282 ``!r. S_CLOCK_FREE r 283 ==> 284 !v c. S_SEM v c r /\ LENGTH v > 0 ==> CLOCK c (LAST v)``, 285 RW_TAC std_ss [CLOCK_def] 286 THEN `LENGTH v >= 1` by DECIDE_TAC 287 THEN PROVE_TAC[Lemma2,ELEM_EL,EL_PRE_LENGTH]); 288 289val LENGTH_FILTER_1_LAST = 290 store_thm 291 ("LENGTH_FILTER_1_LAST", 292 ``!l P. P(LAST l) /\ (LENGTH(FILTER P l) = 1) 293 ==> (HD(FILTER P l) = LAST l)``, 294 RW_TAC std_ss [] 295 THEN IMP_RES_TAC LENGTH_FILTER_1_NOT 296 THEN Induct_on `l` 297 THEN RW_TAC list_ss [FILTER] 298 THENL 299 [Cases_on `l` 300 THEN FULL_SIMP_TAC list_ss [] 301 THEN `0 < SUC (LENGTH t)` by DECIDE_TAC 302 THEN RES_TAC 303 THEN FULL_SIMP_TAC list_ss [], 304 IMP_RES_TAC LENGTH_FILTER_1_NON_EMPTY 305 THEN `~(LENGTH l = 0)` by DECIDE_TAC 306 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 307 THEN FULL_SIMP_TAC list_ss [LAST_DEF] 308 THEN ASSUM_LIST 309 (fn thl => 310 ASSUME_TAC 311 (GEN_ALL 312 (SIMP_RULE list_ss 313 [EL,DECIDE ``(SUC i < n:num ) = (i < n - 1)``] 314 (Q.SPEC `SUC i` (el 4 thl))))) 315 THEN RES_TAC]); 316 317val CONCAT_NIL = 318 store_thm 319 ("CONCAT_NIL", 320 ``!l. (CONCAT l = []) = ALL_EL (\x. x=[]) l``, 321 Induct 322 THEN RW_TAC list_ss [CONCAT_def]); 323 324val S_PROJ_EMPTY = 325 store_thm 326 ("S_PROJ_EMPTY", 327 ``!r c. S_CLOCK_FREE r ==> (US_SEM [] r = S_SEM [] c r)``, 328 INDUCT_THEN sere_induct ASSUME_TAC 329 THENL 330 [(* S_BOOL b *) 331 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def] 332 THEN RW_TAC list_ss [CLOCK_TICK_def,ELEM_EL], 333 (* S_CAT(r,r') *) 334 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 335 THEN PROVE_TAC[], 336 (* S_FUSION (r,r') *) 337 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 338 THEN PROVE_TAC[], 339 (* S_OR (r,r') *) 340 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 341 THEN PROVE_TAC[], 342 (* S_AND (r,r') *) 343 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 344 THEN PROVE_TAC[], 345 (* S_EMPTY *) 346 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 347 THEN PROVE_TAC[], 348 (* S_REPEAT r *) 349 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def,CONCAT_NIL] 350 THEN EQ_TAC 351 THEN RW_TAC list_ss [] 352 THEN Q.EXISTS_TAC `[]` 353 THEN RW_TAC list_ss [], 354 (* S_CLOCK (r,p_2) *) 355 RW_TAC list_ss [S_CLOCK_FREE_def]]); 356 357 358(****************************************************************************** 359* Make FIRSTN executable (for testing) 360******************************************************************************) 361 362val FIRSTN_AUX = 363 store_thm 364 ("FIRSTN_AUX", 365 ``FIRSTN n l = 366 if n=0 then [] 367 else (if NULL l then FIRSTN n [] 368 else HD l :: FIRSTN (n-1) (TL l))``, 369 Cases_on `n` THEN Cases_on `l` 370 THEN RW_TAC list_ss [FIRSTN]); 371 372val _ = computeLib.add_funs[FIRSTN_AUX] 373 374val TAKE_FIRST_def = 375 Define 376 `(TAKE_FIRST P [] = []) 377 /\ 378 (TAKE_FIRST P (x::l) = 379 if P x then [x] else x :: TAKE_FIRST P l)`; 380 381val TAKE_FIRSTN_def = 382 Define 383 `(TAKE_FIRSTN P 0 l = []) 384 /\ 385 (TAKE_FIRSTN P (SUC n) l = 386 TAKE_FIRST P l <> TAKE_FIRSTN P n (BUTFIRSTN (LENGTH(TAKE_FIRST P l)) l))`; 387 388(****************************************************************************** 389* Make BUTFIRSTN executable for testing (not sure is this is needed) 390******************************************************************************) 391 392val BUTFIRSTN_AUX = 393 store_thm 394 ("BUTFIRSTN_AUX", 395 ``BUTFIRSTN n l = 396 if n=0 then l 397 else (if NULL l then BUTFIRSTN n [] 398 else BUTFIRSTN (n-1) (TL l))``, 399 Cases_on `n` THEN Cases_on `l` 400 THEN RW_TAC list_ss [BUTFIRSTN]); 401 402val _ = computeLib.add_funs[BUTFIRSTN_AUX]; 403 404val TAKE_FIRST_NIL = 405 store_thm 406 ("TAKE_FIRST_NIL", 407 ``!l. (TAKE_FIRST P l = []) ==> (l = [])``, 408 Induct 409 THEN RW_TAC list_ss [TAKE_FIRST_def,FILTER_APPEND]); 410 411val TAKE_FIRSTN_NIL = 412 store_thm 413 ("TAKE_FIRSTN_NIL", 414 ``!P n l. 0 < n ==> (TAKE_FIRSTN P n l = []) ==> (l = [])``, 415 GEN_TAC 416 THEN Induct 417 THEN RW_TAC list_ss [] 418 THEN FULL_SIMP_TAC list_ss [TAKE_FIRSTN_def] 419 THEN PROVE_TAC[TAKE_FIRST_NIL]); 420 421val HD_TAKE_FIRST = 422 store_thm 423 ("HD_TAKE_FIRST", 424 ``!l. (?n. n < LENGTH l /\ P(EL n l)) 425 ==> 426 (HD(FILTER P l) = LAST(TAKE_FIRST P l))``, 427 Induct 428 THEN RW_TAC list_ss [TAKE_FIRST_def,FILTER_APPEND] 429 THEN Cases_on `n` 430 THEN RW_TAC list_ss [] 431 THEN FULL_SIMP_TAC list_ss [] 432 THEN RES_TAC 433 THEN RW_TAC list_ss [] 434 THEN `LENGTH l > 0` by DECIDE_TAC 435 THEN IMP_RES_TAC FILTER_NON_EMPTY 436 THEN `~(LENGTH l = 0)` by DECIDE_TAC 437 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 438 THEN `~(TAKE_FIRST P l = [])` by PROVE_TAC[TAKE_FIRST_NIL] 439 THEN RW_TAC list_ss [LAST_DEF]); 440 441val BUTFIRSTN_ONE = 442 store_thm 443 ("BUTFIRSTN_ONE", 444 ``BUTFIRSTN 1 (h::l) = l``, 445 PROVE_TAC[ONE,BUTFIRSTN]); 446 447val FIRSTN_TAKE_FIRSTN = 448 store_thm 449 ("FIRSTN_TAKE_FIRSTN", 450 ``!P n l. FIRSTN (LENGTH(TAKE_FIRSTN P n l)) l = TAKE_FIRSTN P n l``, 451 GEN_TAC 452 THEN Induct 453 THEN RW_TAC list_ss 454 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN] 455 THEN Induct_on `l` 456 THEN RW_TAC list_ss 457 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN,GSYM COND_RAND] 458 THEN FULL_SIMP_TAC list_ss [BUTFIRSTN_ONE,BUTFIRSTN] 459 THENL 460 [FIRST_ASSUM (fn th => ONCE_REWRITE_TAC[GSYM th]) 461 THEN SIMP_TAC list_ss [], 462 RW_TAC list_ss [FIRSTN,DECIDE``m + SUC n = SUC(m + n)``]]); 463 464val FIRSTN_FILTER_TAKE_FIRSTN = 465 store_thm 466 ("FIRSTN_FILTER_TAKE_FIRSTN", 467 ``!P n l. n <= LENGTH(FILTER P l) 468 ==> 469 (FIRSTN n (FILTER P l) = FILTER P (TAKE_FIRSTN P n l))``, 470 GEN_TAC 471 THEN Induct 472 THEN RW_TAC list_ss 473 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN] 474 THEN Induct_on `l` 475 THEN RW_TAC list_ss 476 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN] 477 THEN FULL_SIMP_TAC list_ss []); 478 479val REVERSE_REVERSE_EQ = 480 store_thm 481 ("REVERSE_REVERSE_EQ", 482 ``!l1 l2. (l1 = l2) = (REVERSE l1 = REVERSE l2)``, 483 PROVE_TAC[REVERSE_REVERSE]); 484 485val EQ_APPEND_IMP = 486 store_thm 487 ("EQ_APPEND_IMP", 488 ``(l = v1 <> v2) ==> (l = FIRSTN (LENGTH v1) l <> LASTN (LENGTH v2) l)``, 489 RW_TAC std_ss [] 490 THEN PROVE_TAC 491 [LENGTH_APPEND, 492 APPEND_FIRSTN_LASTN,FIRSTN_LENGTH_APPEND,LASTN_LENGTH_APPEND]); 493 494val APPEND_NIL_NIL = 495 store_thm 496 ("APPEND_NIL_NIL", 497 ``!l1 l2. (l1 <> l2 = []) = (l1 = []) /\ (l2 = [])``, 498 Induct 499 THEN RW_TAC list_ss []); 500 501val HOLDS_LAST_def = 502 Define 503 `HOLDS_LAST P l = (?n. n < LENGTH l /\ P(EL n l)) /\ P(LAST l)`; 504 505val LENGTH_TAKE_FIRST = 506 store_thm 507 ("LENGTH_TAKE_FIRST", 508 ``!P l. LENGTH (TAKE_FIRST P l) <= LENGTH l``, 509 GEN_TAC 510 THEN Induct 511 THEN RW_TAC list_ss [TAKE_FIRST_def]); 512 513val HOLDS_LAST_BUTFIRSTN = 514 store_thm 515 ("HOLDS_LAST_BUTFIRSTN", 516 ``!P l. LENGTH(FILTER P l) > 1 /\ HOLDS_LAST P l 517 ==> 518 HOLDS_LAST P (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)``, 519 GEN_TAC 520 THEN Induct 521 THEN RW_TAC list_ss [HOLDS_LAST_def,TAKE_FIRST_def,BUTFIRSTN_ONE] 522 THENL 523 [Cases_on `0 < LENGTH l` 524 THEN RW_TAC list_ss [] 525 THENL 526 [`LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 527 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 528 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF] 529 THEN PROVE_TAC[EL_PRE_LENGTH], 530 `LENGTH l = 0` by DECIDE_TAC 531 THEN `n = 0` by DECIDE_TAC 532 THEN RW_TAC list_ss [] 533 THEN `LENGTH (FILTER P l) > 0` by DECIDE_TAC 534 THEN IMP_RES_TAC LENGTH_FILTER_NON_EMPTY 535 THEN DECIDE_TAC], 536 Cases_on `0 < LENGTH l` 537 THEN RW_TAC list_ss [] 538 THENL 539 [`LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 540 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 541 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF], 542 `LENGTH l = 0` by DECIDE_TAC 543 THEN `n = 0` by DECIDE_TAC 544 THEN `l = []` by PROVE_TAC[LENGTH_NIL] 545 THEN RW_TAC list_ss [] 546 THEN FULL_SIMP_TAC list_ss []], 547 RES_TAC 548 THEN `n <= LENGTH l` by DECIDE_TAC 549 THEN RW_TAC list_ss [BUTFIRSTN,LENGTH_BUTFIRSTN,LENGTH_TAKE_FIRST] 550 THEN Cases_on `n = 0` 551 THEN RW_TAC list_ss [] 552 THEN FULL_SIMP_TAC list_ss [] 553 THEN `n-1 < LENGTH l` by DECIDE_TAC 554 THEN `LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 555 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 556 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF] 557 THEN `n = SUC(n-1)` by DECIDE_TAC 558 THEN `P(EL (n-1) l)` by PROVE_TAC[TL,EL] 559 THEN `HOLDS_LAST P l` by PROVE_TAC[HOLDS_LAST_def] 560 THEN RES_TAC 561 THEN POP_ASSUM(STRIP_ASSUME_TAC o SIMP_RULE list_ss [HOLDS_LAST_def]) 562 THEN PROVE_TAC[BUTFIRSTN,LENGTH_BUTFIRSTN,LENGTH_TAKE_FIRST], 563 RES_TAC 564 THEN `n <= LENGTH l` by DECIDE_TAC 565 THEN RW_TAC list_ss [BUTFIRSTN,LENGTH_BUTFIRSTN,LENGTH_TAKE_FIRST] 566 THEN Cases_on `n = 0` 567 THEN RW_TAC list_ss [] 568 THEN FULL_SIMP_TAC list_ss [] 569 THEN `n-1 < LENGTH l` by DECIDE_TAC 570 THEN `LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 571 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 572 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF] 573 THEN `n = SUC(n-1)` by DECIDE_TAC 574 THEN `P(EL (n-1) l)` by PROVE_TAC[TL,EL] 575 THEN `HOLDS_LAST P l` by PROVE_TAC[HOLDS_LAST_def] 576 THEN RES_TAC 577 THEN POP_ASSUM(STRIP_ASSUME_TAC o SIMP_RULE list_ss [HOLDS_LAST_def])]); 578 579val LENGTH_FILTER_BUTFIRSTN = 580 store_thm 581 ("LENGTH_FILTER_BUTFIRSTN", 582 ``!P l. LENGTH(FILTER P (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) = 583 LENGTH(FILTER P l) - 1``, 584 GEN_TAC 585 THEN Induct 586 THEN RW_TAC list_ss [TAKE_FIRST_def,BUTFIRSTN,BUTFIRSTN_ONE,GSYM COND_RAND]); 587 588val LENGTH_1_BUTFIRSTN = 589 store_thm 590 ("LENGTH_1_BUTFIRSTN", 591 ``!P l. HOLDS_LAST P l /\ (LENGTH (FILTER P l) = 1) 592 ==> 593 (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l = [])``, 594 GEN_TAC 595 THEN Induct 596 THEN RW_TAC list_ss [TAKE_FIRST_def,BUTFIRSTN,BUTFIRSTN_ONE,HOLDS_LAST_def,GSYM COND_RAND] 597 THENL 598 [Cases_on `l = []` 599 THEN RW_TAC list_ss [] 600 THEN `~(LENGTH l = 0)` by PROVE_TAC[LENGTH_NIL] 601 THEN `LENGTH l > 0` by DECIDE_TAC 602 THEN PROVE_TAC[LAST_FILTER_NON_EMPTY,LENGTH_NIL,LAST_DEF], 603 Cases_on `n = 0` 604 THEN RW_TAC list_ss [] 605 THEN FULL_SIMP_TAC list_ss [] 606 THEN `n-1 < LENGTH l` by DECIDE_TAC 607 THEN `LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 608 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 609 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF] 610 THEN `n = SUC(n-1)` by DECIDE_TAC 611 THEN `P(EL (n-1) l)` by PROVE_TAC[TL,EL] 612 THEN `HOLDS_LAST P l` by PROVE_TAC[HOLDS_LAST_def] 613 THEN RES_TAC]); 614 615val HOLDS_LAST_1_TAKE_FIRST = 616 store_thm 617 ("HOLDS_LAST_1_TAKE_FIRST", 618 ``!P l. HOLDS_LAST P l /\ (LENGTH(FILTER P l) = 1) ==> (TAKE_FIRST P l = l)``, 619 GEN_TAC 620 THEN Induct 621 THEN RW_TAC list_ss [HOLDS_LAST_def,TAKE_FIRST_def] 622 THENL 623 [Cases_on `l = []` 624 THEN RW_TAC list_ss [] 625 THEN `~(LENGTH l = 0)` by PROVE_TAC[LENGTH_NIL] 626 THEN `LENGTH l > 0` by DECIDE_TAC 627 THEN PROVE_TAC[LAST_FILTER_NON_EMPTY,LENGTH_NIL,LAST_DEF], 628 Cases_on `n = 0` 629 THEN RW_TAC list_ss [] 630 THEN FULL_SIMP_TAC list_ss [] 631 THEN `n-1 < LENGTH l` by DECIDE_TAC 632 THEN `LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 633 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 634 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF] 635 THEN `n = SUC(n-1)` by DECIDE_TAC 636 THEN `P(EL (n-1) l)` by PROVE_TAC[TL,EL] 637 THEN `HOLDS_LAST P l` by PROVE_TAC[HOLDS_LAST_def] 638 THEN RES_TAC]); 639 640val TAKE_FIRST_APPEND = 641 store_thm 642 ("TAKE_FIRST_APPEND", 643 ``!P l. TAKE_FIRST P l <> BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l = l``, 644 GEN_TAC 645 THEN Induct 646 THEN RW_TAC list_ss [HOLDS_LAST_def,TAKE_FIRST_def,BUTFIRSTN_ONE,BUTFIRSTN] 647 THEN Cases_on `n = 0` 648 THEN RW_TAC list_ss [] 649 THEN FULL_SIMP_TAC list_ss [] 650 THEN `n-1 < LENGTH l` by DECIDE_TAC 651 THEN `LENGTH l >= 1 /\ LENGTH l - 1 < LENGTH l /\ ~(LENGTH l = 0)` by DECIDE_TAC 652 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 653 THEN `P(LAST l)` by PROVE_TAC[LAST_DEF] 654 THEN `n = SUC(n-1)` by DECIDE_TAC 655 THEN `P(EL (n-1) l)` by PROVE_TAC[TL,EL] 656 THEN `HOLDS_LAST P l` by PROVE_TAC[HOLDS_LAST_def] 657 THEN RES_TAC); 658 659val HOLDS_LAST_TAKE_FIRSTN = 660 store_thm 661 ("HOLDS_LAST_TAKE_FIRSTN", 662 ``!P l. HOLDS_LAST P l ==> (TAKE_FIRSTN P (LENGTH(FILTER P l)) l = l)``, 663 Induct_on `LENGTH(FILTER P l)` 664 THEN RW_TAC list_ss [] 665 THENL 666 [FULL_SIMP_TAC list_ss [HOLDS_LAST_def] 667 THEN `LENGTH l > 0` by DECIDE_TAC 668 THEN IMP_RES_TAC FILTER_NON_EMPTY 669 THEN PROVE_TAC[LENGTH_NIL], 670 `v = LENGTH (FILTER P l) - 1` by DECIDE_TAC 671 THEN RW_TAC list_ss [] 672 THEN ASSUM_LIST(fn thl => ONCE_REWRITE_TAC[GSYM(el 2 thl)]) 673 THEN REWRITE_TAC[TAKE_FIRSTN_def] 674 THEN ASSUM_LIST 675 (fn thl => 676 ASSUME_TAC(Q.SPECL[`P`,`BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l`](el 3 thl))) 677 THEN `LENGTH(FILTER P l) > 0` by DECIDE_TAC 678 THEN Cases_on `LENGTH (FILTER P l) = 1` 679 THEN RW_TAC list_ss [LENGTH_1_BUTFIRSTN,TAKE_FIRSTN_def,HOLDS_LAST_1_TAKE_FIRST] 680 THEN `LENGTH(FILTER P l) > 1` by DECIDE_TAC 681 THEN IMP_RES_TAC HOLDS_LAST_BUTFIRSTN 682 THEN `TAKE_FIRSTN P 683 (LENGTH (FILTER P l) - 1) 684 (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) = 685 BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l` by PROVE_TAC[LENGTH_FILTER_BUTFIRSTN] 686 THEN RW_TAC list_ss [TAKE_FIRST_APPEND]]); 687 688val LENGTH_TAKE_FIRSTN = 689 store_thm 690 ("LENGTH_TAKE_FIRSTN", 691 ``!P n l. LENGTH(TAKE_FIRSTN P n l) <= LENGTH l``, 692 GEN_TAC 693 THEN Induct 694 THEN RW_TAC list_ss [TAKE_FIRST_def] 695 THEN Induct_on `l` 696 THEN RW_TAC list_ss 697 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN,BUTFIRSTN,BUTFIRSTN_ONE] 698 THEN FULL_SIMP_TAC list_ss [] 699 THENL 700 [POP_ASSUM 701 (ACCEPT_TAC o SIMP_RULE list_ss [TAKE_FIRSTN_def] o Q.SPEC `[]`), 702 RW_TAC list_ss [DECIDE ``m+1 <= SUC n = m <= n``], 703 RW_TAC list_ss [DECIDE ``m + SUC n <= SUC p = m + n <= p``] 704 THEN RW_TAC std_ss [GSYM LENGTH_APPEND,GSYM TAKE_FIRSTN_def]]); 705 706val LENGTH_LESS_TAKE_FIRSTN = 707 store_thm 708 ("LENGTH_LESS_TAKE_FIRSTN", 709 ``!P n l. 0 < n /\ n < LENGTH(FILTER P l) ==> LENGTH(TAKE_FIRSTN P n l) < LENGTH l``, 710 GEN_TAC 711 THEN Induct 712 THEN RW_TAC list_ss [TAKE_FIRST_def] 713 THEN Induct_on `l` 714 THEN RW_TAC list_ss 715 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN,BUTFIRSTN,BUTFIRSTN_ONE] 716 THEN FULL_SIMP_TAC list_ss [] 717 THENL 718 [Cases_on `n=0` 719 THEN RW_TAC list_ss [TAKE_FIRSTN_def] 720 THENL 721 [`LENGTH (FILTER P l) > 0` by DECIDE_TAC 722 THEN IMP_RES_TAC LENGTH_FILTER_NON_EMPTY 723 THEN DECIDE_TAC, 724 `0 < n` by DECIDE_TAC 725 THEN RES_TAC 726 THEN DECIDE_TAC], 727 RW_TAC list_ss [DECIDE ``m + SUC n < SUC p = m + n < p``] 728 THEN RW_TAC std_ss (map GSYM [LENGTH_APPEND,TAKE_FIRSTN_def])]); 729 730 731val TOP_FREE_FIRSTN = 732 store_thm 733 ("TOP_FREE_FIRSTN", 734 ``!l n. n <= LENGTH l /\ TOP_FREE l ==> TOP_FREE(FIRSTN n l)``, 735 Induct 736 THEN RW_TAC list_ss [TOP_FREE_def,FIRSTN] 737 THEN Induct_on `n` 738 THEN RW_TAC list_ss 739 [FIRSTN,BUTFIRSTN,BUTFIRSTN_ONE] 740 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def] 741 THEN Cases_on `h` 742 THEN FULL_SIMP_TAC list_ss 743 [B_SEM_def,TOP_FREE_def,EL_CONS,DECIDE``PRE n = n-1``]); 744 745val BOTTOM_FREE_FIRSTN = 746 store_thm 747 ("BOTTOM_FREE_FIRSTN", 748 ``!l n. n <= LENGTH l /\ BOTTOM_FREE l ==> BOTTOM_FREE(FIRSTN n l)``, 749 Induct 750 THEN RW_TAC list_ss [BOTTOM_FREE_def,FIRSTN] 751 THEN Induct_on `n` 752 THEN RW_TAC list_ss 753 [FIRSTN,BUTFIRSTN,BUTFIRSTN_ONE] 754 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def] 755 THEN Cases_on `h` 756 THEN FULL_SIMP_TAC list_ss 757 [B_SEM_def,BOTTOM_FREE_def,EL_CONS,DECIDE``PRE n = n-1``]); 758 759val TOP_FREE_TAKE_FIRSTN = 760 store_thm 761 ("TOP_FREE_TAKE_FIRSTN", 762 ``!l P n. TOP_FREE l ==> TOP_FREE(TAKE_FIRSTN P n l)``, 763 Induct 764 THEN RW_TAC list_ss [TOP_FREE_def,TAKE_FIRST_def] 765 THEN Induct_on `n` 766 THEN RW_TAC list_ss 767 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN,BUTFIRSTN,BUTFIRSTN_ONE] 768 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def] 769 THEN Cases_on `h` 770 THEN FULL_SIMP_TAC list_ss 771 [B_SEM_def,TOP_FREE_def,EL_CONS,DECIDE``PRE n = n-1``] 772 THEN RW_TAC list_ss [GSYM TAKE_FIRSTN_def]); 773 774val BOTTOM_FREE_TAKE_FIRSTN = 775 store_thm 776 ("BOTTOM_FREE_TAKE_FIRSTN", 777 ``!l P n. BOTTOM_FREE l ==> BOTTOM_FREE(TAKE_FIRSTN P n l)``, 778 Induct 779 THEN RW_TAC list_ss [BOTTOM_FREE_def,TAKE_FIRST_def] 780 THEN Induct_on `n` 781 THEN RW_TAC list_ss 782 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN,BUTFIRSTN,BUTFIRSTN_ONE] 783 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def] 784 THEN Cases_on `h` 785 THEN FULL_SIMP_TAC list_ss 786 [B_SEM_def,BOTTOM_FREE_def,EL_CONS,DECIDE``PRE n = n-1``] 787 THEN RW_TAC list_ss [GSYM TAKE_FIRSTN_def]); 788 789val TOP_FREE_REVERSE = 790 store_thm 791 ("TOP_FREE_REVERSE", 792 ``!l. TOP_FREE(REVERSE l) = TOP_FREE l``, 793 Induct 794 THEN RW_TAC list_ss [TOP_FREE_def] 795 THEN Cases_on `h` 796 THEN FULL_SIMP_TAC list_ss 797 [B_SEM_def,TOP_FREE_def,EL_CONS, 798 DECIDE``PRE n = n-1``,TOP_FREE_APPEND]); 799 800val BOTTOM_FREE_REVERSE = 801 store_thm 802 ("BOTTOM_FREE_REVERSE", 803 ``!l. BOTTOM_FREE(REVERSE l) = BOTTOM_FREE l``, 804 Induct 805 THEN RW_TAC list_ss [BOTTOM_FREE_def] 806 THEN Cases_on `h` 807 THEN FULL_SIMP_TAC list_ss 808 [B_SEM_def,BOTTOM_FREE_def,EL_CONS, 809 DECIDE``PRE n = n-1``,BOTTOM_FREE_APPEND]); 810 811val LASTN_REVERSE_FIRSTN = 812 store_thm 813 ("LASTN_REVERSE_FIRSTN", 814 ``!n l. n <= LENGTH l ==> (LASTN n l = REVERSE(FIRSTN n (REVERSE l)))``, 815 PROVE_TAC[REVERSE_REVERSE,FIRSTN_REVERSE]); 816 817val TOP_FREE_LAST = 818 store_thm 819 ("TOP_FREE_LAST", 820 ``!l. 0 < LENGTH l /\ TOP_FREE l ==> TOP_FREE[LAST l]``, 821 Induct 822 THEN RW_TAC list_ss [TOP_FREE_def] 823 THEN Cases_on `h` 824 THEN FULL_SIMP_TAC list_ss [B_SEM_def,TOP_FREE_def] 825 THEN Cases_on `l` 826 THEN RW_TAC list_ss [TOP_FREE_def]); 827 828val TOP_FREE_LASTN = 829 store_thm 830 ("TOP_FREE_LASTN", 831 ``!l n. n <= LENGTH l /\ TOP_FREE l ==> TOP_FREE(LASTN n l)``, 832 SIMP_TAC list_ss [LASTN_REVERSE_FIRSTN] 833 THEN Induct_on `l` 834 THEN RW_TAC list_ss [TOP_FREE_def,FIRSTN] 835 THEN Induct_on `n` 836 THEN RW_TAC list_ss 837 [FIRSTN,TOP_FREE_def] 838 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def] 839 THEN Cases_on `h` 840 THEN FULL_SIMP_TAC list_ss 841 [B_SEM_def,TOP_FREE_def,EL_CONS, 842 DECIDE``PRE n = n-1``,TOP_FREE_REVERSE] 843 THEN RES_TAC 844 THEN Cases_on `n = LENGTH l` 845 THEN RW_TAC list_ss [] 846 THENL 847 [`LENGTH(REVERSE l <> [BOTTOM]) = SUC(LENGTH l)` 848 by RW_TAC list_ss [LENGTH_REVERSE] 849 THEN `LENGTH l < LENGTH(REVERSE l <> [BOTTOM])` by DECIDE_TAC 850 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 851 THEN `~NULL[BOTTOM]` by RW_TAC list_ss [] 852 THEN `EL (LENGTH l) (REVERSE l <> [BOTTOM]) = BOTTOM` by PROVE_TAC[EL_LENGTH_APPEND,HD] 853 THEN RW_TAC list_ss [FIRSTN_SUC_EL,TOP_FREE_APPEND,TOP_FREE_def], 854 `SUC n <= LENGTH l` by DECIDE_TAC 855 THEN RES_TAC 856 THEN `LENGTH l < LENGTH(REVERSE l <> [BOTTOM])` 857 by RW_TAC list_ss [LENGTH_APPEND,LENGTH_REVERSE] 858 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 859 THEN `~NULL[BOTTOM]` by RW_TAC list_ss [] 860 THEN `EL (LENGTH l) (REVERSE l <> [BOTTOM]) = BOTTOM` by PROVE_TAC[EL_LENGTH_APPEND,HD] 861 THEN `n < LENGTH l` by DECIDE_TAC 862 THEN RW_TAC list_ss [EL_APPEND1,FIRSTN_SUC_EL,TOP_FREE_APPEND,TOP_FREE_def] 863 THEN RW_TAC list_ss [TOP_FREE_EL] 864 THEN `i = 0` by DECIDE_TAC 865 THEN RW_TAC list_ss [] 866 THEN `TOP_FREE(REVERSE l)` by PROVE_TAC[TOP_FREE_REVERSE] 867 THEN FULL_SIMP_TAC list_ss [TOP_FREE_EL], 868 `LENGTH(REVERSE l <> [STATE f]) = SUC(LENGTH l)` 869 by RW_TAC list_ss [LENGTH_REVERSE] 870 THEN `LENGTH l < LENGTH(REVERSE l <> [STATE f])` by DECIDE_TAC 871 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 872 THEN `~NULL[STATE f]` by RW_TAC list_ss [] 873 THEN `EL (LENGTH l) (REVERSE l <> [STATE f]) = STATE f` by PROVE_TAC[EL_LENGTH_APPEND,HD] 874 THEN RW_TAC list_ss [FIRSTN_SUC_EL,TOP_FREE_APPEND,TOP_FREE_def], 875 `SUC n <= LENGTH l` by DECIDE_TAC 876 THEN RES_TAC 877 THEN `LENGTH l < LENGTH(REVERSE l <> [STATE f])` 878 by RW_TAC list_ss [LENGTH_APPEND,LENGTH_REVERSE] 879 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 880 THEN `~NULL[STATE f]` by RW_TAC list_ss [] 881 THEN `EL (LENGTH l) (REVERSE l <> [STATE f]) = STATE f` by PROVE_TAC[EL_LENGTH_APPEND,HD] 882 THEN `n < LENGTH l` by DECIDE_TAC 883 THEN RW_TAC list_ss [EL_APPEND1,FIRSTN_SUC_EL,TOP_FREE_APPEND,TOP_FREE_def] 884 THEN RW_TAC list_ss [TOP_FREE_EL] 885 THEN `i = 0` by DECIDE_TAC 886 THEN RW_TAC list_ss [] 887 THEN `TOP_FREE(REVERSE l)` by PROVE_TAC[TOP_FREE_REVERSE] 888 THEN FULL_SIMP_TAC list_ss [TOP_FREE_EL]]); 889 890val BOTTOM_FREE_LAST = 891 store_thm 892 ("BOTTOM_FREE_LAST", 893 ``!l. 0 < LENGTH l /\ BOTTOM_FREE l ==> BOTTOM_FREE[LAST l]``, 894 Induct 895 THEN RW_TAC list_ss [BOTTOM_FREE_def] 896 THEN Cases_on `h` 897 THEN FULL_SIMP_TAC list_ss [B_SEM_def,BOTTOM_FREE_def] 898 THEN Cases_on `l` 899 THEN RW_TAC list_ss [BOTTOM_FREE_def]); 900 901val BOTTOM_FREE_LASTN = 902 store_thm 903 ("BOTTOM_FREE_LASTN", 904 ``!l n. n <= LENGTH l /\ BOTTOM_FREE l ==> BOTTOM_FREE(LASTN n l)``, 905 SIMP_TAC list_ss [LASTN_REVERSE_FIRSTN] 906 THEN Induct_on `l` 907 THEN RW_TAC list_ss [BOTTOM_FREE_def,FIRSTN] 908 THEN Induct_on `n` 909 THEN RW_TAC list_ss 910 [FIRSTN,BOTTOM_FREE_def] 911 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def] 912 THEN Cases_on `h` 913 THEN FULL_SIMP_TAC list_ss 914 [B_SEM_def,BOTTOM_FREE_def,EL_CONS, 915 DECIDE``PRE n = n-1``,BOTTOM_FREE_REVERSE] 916 THEN RES_TAC 917 THEN Cases_on `n = LENGTH l` 918 THEN RW_TAC list_ss [] 919 THENL 920 [`LENGTH(REVERSE l <> [TOP]) = SUC(LENGTH l)` 921 by RW_TAC list_ss [LENGTH_REVERSE] 922 THEN `LENGTH l < LENGTH(REVERSE l <> [TOP])` by DECIDE_TAC 923 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 924 THEN `~NULL[TOP]` by RW_TAC list_ss [] 925 THEN `EL (LENGTH l) (REVERSE l <> [TOP]) = TOP` by PROVE_TAC[EL_LENGTH_APPEND,HD] 926 THEN RW_TAC list_ss [FIRSTN_SUC_EL,BOTTOM_FREE_APPEND,BOTTOM_FREE_def], 927 `SUC n <= LENGTH l` by DECIDE_TAC 928 THEN RES_TAC 929 THEN `LENGTH l < LENGTH(REVERSE l <> [TOP])` 930 by RW_TAC list_ss [LENGTH_APPEND,LENGTH_REVERSE] 931 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 932 THEN `~NULL[TOP]` by RW_TAC list_ss [] 933 THEN `EL (LENGTH l) (REVERSE l <> [TOP]) = TOP` by PROVE_TAC[EL_LENGTH_APPEND,HD] 934 THEN `n < LENGTH l` by DECIDE_TAC 935 THEN RW_TAC list_ss [EL_APPEND1,FIRSTN_SUC_EL,BOTTOM_FREE_APPEND,BOTTOM_FREE_def] 936 THEN RW_TAC list_ss [BOTTOM_FREE_EL] 937 THEN `i = 0` by DECIDE_TAC 938 THEN RW_TAC list_ss [] 939 THEN `BOTTOM_FREE(REVERSE l)` by PROVE_TAC[BOTTOM_FREE_REVERSE] 940 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_EL], 941 `LENGTH(REVERSE l <> [STATE f]) = SUC(LENGTH l)` 942 by RW_TAC list_ss [LENGTH_REVERSE] 943 THEN `LENGTH l < LENGTH(REVERSE l <> [STATE f])` by DECIDE_TAC 944 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 945 THEN `~NULL[STATE f]` by RW_TAC list_ss [] 946 THEN `EL (LENGTH l) (REVERSE l <> [STATE f]) = STATE f` by PROVE_TAC[EL_LENGTH_APPEND,HD] 947 THEN RW_TAC list_ss [FIRSTN_SUC_EL,BOTTOM_FREE_APPEND,BOTTOM_FREE_def], 948 `SUC n <= LENGTH l` by DECIDE_TAC 949 THEN RES_TAC 950 THEN `LENGTH l < LENGTH(REVERSE l <> [STATE f])` 951 by RW_TAC list_ss [LENGTH_APPEND,LENGTH_REVERSE] 952 THEN `LENGTH(REVERSE l) = LENGTH l` by RW_TAC list_ss [LENGTH_REVERSE] 953 THEN `~NULL[STATE f]` by RW_TAC list_ss [] 954 THEN `EL (LENGTH l) (REVERSE l <> [STATE f]) = STATE f` by PROVE_TAC[EL_LENGTH_APPEND,HD] 955 THEN `n < LENGTH l` by DECIDE_TAC 956 THEN RW_TAC list_ss [EL_APPEND1,FIRSTN_SUC_EL,BOTTOM_FREE_APPEND,BOTTOM_FREE_def] 957 THEN RW_TAC list_ss [BOTTOM_FREE_EL] 958 THEN `i = 0` by DECIDE_TAC 959 THEN RW_TAC list_ss [] 960 THEN `BOTTOM_FREE(REVERSE l)` by PROVE_TAC[BOTTOM_FREE_REVERSE] 961 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_EL]]); 962 963val LAST_TAKE_FIRST = 964 store_thm 965 ("LAST_TAKE_FIRST", 966 ``!P l. 0 < LENGTH(FILTER P l) ==> P(LAST(TAKE_FIRST P l))``, 967 GEN_TAC 968 THEN Induct 969 THEN RW_TAC list_ss 970 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN,LAST_DEF] 971 THEN RES_TAC 972 THEN Cases_on `TAKE_FIRST P l = []` 973 THEN RW_TAC std_ss [] 974 THEN IMP_RES_TAC TAKE_FIRST_NIL 975 THEN RW_TAC list_ss [] 976 THEN FULL_SIMP_TAC list_ss []); 977 978val LAST_TAKE_FIRSTN = 979 store_thm 980 ("LAST_TAKE_FIRSTN", 981 ``!P l n. 0 < n /\ n <= LENGTH(FILTER P l) ==> P(LAST(TAKE_FIRSTN P n l))``, 982 GEN_TAC 983 THEN Induct 984 THEN Induct_on `n` 985 THEN RW_TAC list_ss 986 [TAKE_FIRST_def,TAKE_FIRSTN_def,FIRSTN] 987 THEN FULL_SIMP_TAC list_ss [BUTFIRSTN,BUTFIRSTN_ONE] 988 THENL 989 [Cases_on `n = 0` 990 THEN RW_TAC list_ss [TAKE_FIRSTN_def] 991 THEN `0 < n` by DECIDE_TAC 992 THEN RES_TAC 993 THEN RW_TAC list_ss [LAST_DEF], 994 Cases_on `n = 0` 995 THEN RW_TAC list_ss [TAKE_FIRSTN_def] 996 THENL 997 [`0 < 1 /\ 1 <= LENGTH (FILTER P l) /\ 0 < SUC 0` by DECIDE_TAC 998 THEN RES_TAC 999 THEN RW_TAC list_ss [LAST_DEF] 1000 THEN FULL_SIMP_TAC list_ss [TAKE_FIRSTN_def] 1001 THEN IMP_RES_TAC TAKE_FIRST_NIL 1002 THEN RW_TAC list_ss [] 1003 THEN FULL_SIMP_TAC list_ss [], 1004 `0 < SUC n` by DECIDE_TAC 1005 THEN RES_TAC 1006 THEN RW_TAC list_ss [GSYM TAKE_FIRSTN_def] 1007 THEN RW_TAC list_ss [LAST_DEF] 1008 THEN FULL_SIMP_TAC list_ss [TAKE_FIRSTN_def] 1009 THEN IMP_RES_TAC TAKE_FIRST_NIL 1010 THEN RW_TAC list_ss [] 1011 THEN FULL_SIMP_TAC list_ss []]]); 1012 1013val LENGTH_FILTER_FIRSTN = 1014 store_thm 1015 ("LENGTH_FILTER_FIRSTN", 1016 ``!P n l. 1017 n <= LENGTH (FILTER P l) 1018 ==> 1019 (LENGTH(FILTER P (FIRSTN (LENGTH (TAKE_FIRSTN P n l)) l)) = n)``, 1020 RW_TAC list_ss [FIRSTN_TAKE_FIRSTN,GSYM FIRSTN_FILTER_TAKE_FIRSTN,LENGTH_FIRSTN]); 1021 1022val SPLIT_APPEND = store_thm 1023 ("SPLIT_APPEND", 1024 ``!u1 u2 v1 v2:'a list. 1025 (u1 <> u2 = v1 <> v2) /\ (LENGTH u1 = LENGTH v1) ==> (u2 = v2)``, 1026 Induct 1027 >> RW_TAC list_ss [] 1028 >> Cases_on `v1` 1029 >> RW_TAC list_ss [] 1030 >> FULL_SIMP_TAC list_ss []); 1031 1032val S_PROJ_S_BOOL = 1033 store_thm 1034 ("S_PROJ_S_BOOL", 1035 ``!b l c. 1036 S_CLOCK_FREE (S_BOOL b) /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1037 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) (S_BOOL b) = 1038 S_SEM l c (S_BOOL b))``, 1039 RW_TAC list_ss [LIST_PROJ_def,S_SEM_def,US_SEM_def,CLOCK_def] 1040 THEN RW_TAC list_ss [CLOCK_TICK_def,ELEM_EL] 1041 THEN RW_TAC (list_ss++resq_SS) [] 1042 THEN EQ_TAC 1043 THEN RW_TAC list_ss [] 1044 THEN IMP_RES_TAC LENGTH_FILTER_1_NON_EMPTY 1045 THEN `LENGTH l >= 1` by DECIDE_TAC 1046 THEN ZAP_TAC std_ss [EL_PRE_LENGTH] 1047 THENL 1048 [FULL_SIMP_TAC std_ss [GSYM CLOCK_def] 1049 THEN IMP_RES_TAC 1050 (ISPECL [``l :'a letter list``,``CLOCK c``] LENGTH_FILTER_1_NOT) 1051 THEN Cases_on `EL i l` 1052 THEN FULL_SIMP_TAC std_ss [CLOCK_def,B_SEM_def] 1053 THEN `i < LENGTH l` by DECIDE_TAC 1054 THEN IMP_RES_TAC BOTTOM_FREE_EL, 1055 IMP_RES_TAC 1056 (SIMP_RULE std_ss [CLOCK_def] 1057 (ISPECL[``l :'a letter list``,``CLOCK c``] LENGTH_FILTER_1_LAST)) 1058 THEN IMP_RES_TAC EL_PRE_LENGTH 1059 THEN PROVE_TAC[], 1060 `CLOCK_TICK l c` 1061 by PROVE_TAC[SIMP_RULE (list_ss++resq_SS) [ELEM_EL] CLOCK_TICK_def] 1062 THEN IMP_RES_TAC CLOCK_TICK_LENGTH_1, 1063 `CLOCK_TICK l c` 1064 by PROVE_TAC[SIMP_RULE (list_ss++resq_SS) [ELEM_EL] CLOCK_TICK_def] 1065 THEN IMP_RES_TAC EL_PRE_LENGTH 1066 THEN PROVE_TAC 1067 [SIMP_RULE std_ss [CLOCK_def] 1068 (ISPECL[``l :'a letter list``,``CLOCK c``] LENGTH_FILTER_1_LAST), 1069 CLOCK_TICK_LENGTH_1]]); 1070 1071val S_PROJ_S_CAT_LEMMA1 = 1072 store_thm 1073 ("S_PROJ_S_CAT_LEMMA1", 1074 ``LENGTH (TAKE_FIRSTN (CLOCK(c:'a bexp)) (LENGTH(v1:'a letter list)) l) <= LENGTH l 1075 ==> 1076 ((FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l 1077 <> 1078 LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l) = l)``, 1079 RW_TAC std_ss [] 1080 THEN `(LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) + 1081 (LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) = LENGTH l` 1082 by DECIDE_TAC 1083 THEN IMP_RES_TAC APPEND_FIRSTN_LASTN); 1084 1085val S_PROJ_S_CAT_LEMMA2 = 1086 store_thm 1087 ("S_PROJ_S_CAT_LEMMA2", 1088 ``LENGTH 1089 (TAKE_FIRSTN (CLOCK (c :'a bexp)) (LENGTH (v1 :'a letter list)) 1090 (l :'a letter list)) <= LENGTH l ==> 1091 ((FILTER (CLOCK c) (FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l) <> 1092 FILTER (CLOCK c) (LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l)) = 1093 (FILTER (CLOCK c) l))``, 1094 RW_TAC std_ss [GSYM FILTER_APPEND] 1095 THEN IMP_RES_TAC S_PROJ_S_CAT_LEMMA1 1096 THEN RW_TAC std_ss []); 1097 1098val S_PROJ_S_CAT_LEMMA3 = 1099 store_thm 1100 ("S_PROJ_S_CAT_LEMMA3", 1101 ``(FILTER (CLOCK c) l = v1 <> v2) 1102 ==> 1103 (FILTER 1104 (CLOCK c) 1105 (LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l) = 1106 v2)``, 1107 RW_TAC list_ss [] 1108 THEN `LENGTH(TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) <= LENGTH l` 1109 by PROVE_TAC[LENGTH_TAKE_FIRSTN] 1110 THEN `LENGTH(FILTER (CLOCK c) l) = LENGTH(v1 <> v2)` by PROVE_TAC[] 1111 THEN FULL_SIMP_TAC list_ss [LENGTH_APPEND] 1112 THEN `LENGTH v1 <= LENGTH (FILTER (CLOCK c) l)` by DECIDE_TAC 1113 THEN PROVE_TAC[SPLIT_APPEND,LENGTH_FILTER_FIRSTN,S_PROJ_S_CAT_LEMMA2]); 1114 1115val S_PROJ_S_CAT = 1116 store_thm 1117 ("S_PROJ_S_CAT", 1118 ``(!l c. S_CLOCK_FREE r /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1119 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r = S_SEM l c r)) 1120 /\ 1121 (!l c. S_CLOCK_FREE r' /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1122 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r' = S_SEM l c r')) 1123 ==> 1124 !l c. S_CLOCK_FREE (S_CAT (r,r')) /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1125 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) (S_CAT (r,r')) = 1126 S_SEM l c (S_CAT (r,r')))``, 1127 RW_TAC list_ss [LIST_PROJ_def,S_SEM_def,US_SEM_def,S_CLOCK_FREE_def] 1128 THEN RW_TAC list_ss [CLOCK_TICK_def,ELEM_EL] 1129 THEN RW_TAC (list_ss++resq_SS) [] 1130 THEN EQ_TAC 1131 THEN RW_TAC list_ss [FILTER_APPEND] 1132 THENL 1133 [Cases_on `v1=[]` THEN Cases_on `v2=[]` (* Case split may be overkill *) 1134 THEN RW_TAC list_ss [] 1135 THEN FULL_SIMP_TAC list_ss [] 1136 THENL 1137 [Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `[]` 1138 THEN RW_TAC list_ss [GSYM S_PROJ_EMPTY] 1139 THEN Cases_on `LENGTH l > 0` 1140 THEN IMP_RES_TAC 1141 (ISPECL 1142 [``l :'a letter list``,``CLOCK(c :'a bexp)``]LAST_FILTER_NON_EMPTY) 1143 THEN ZAP_TAC list_ss [CLOCK_def,LENGTH_NIL,DECIDE``~(n > 0) = (n = 0)``], 1144 Q.EXISTS_TAC `[]` 1145 THEN RW_TAC list_ss [GSYM S_PROJ_EMPTY] 1146 THEN ASSUM_LIST 1147 (fn thl => 1148 ACCEPT_TAC 1149 (SIMP_RULE list_ss [el 2 thl,el 4 thl,el 5 thl,el 6 thl,CLOCK_def] 1150 (Q.SPECL[`l`,`c`](el 9 thl)))), 1151 Q.EXISTS_TAC `l` THEN Q.EXISTS_TAC `[]` 1152 THEN RW_TAC list_ss [GSYM S_PROJ_EMPTY] 1153 THEN ASSUM_LIST 1154 (fn thl => 1155 ACCEPT_TAC 1156 (SIMP_RULE list_ss [el 3 thl,el 4 thl,el 5 thl,el 6 thl,CLOCK_def] 1157 (Q.SPECL[`l`,`c`](el 10 thl)))), 1158 `LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) <= LENGTH l` 1159 by PROVE_TAC[LENGTH_TAKE_FIRSTN] 1160 THEN `(LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) 1161 + (LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) = 1162 LENGTH l` by DECIDE_TAC 1163 THEN Q.EXISTS_TAC `TAKE_FIRSTN (CLOCK c) (LENGTH v1) l` 1164 THEN Q.EXISTS_TAC `LASTN (LENGTH l - LENGTH(TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l` 1165 THEN ONCE_REWRITE_TAC[GSYM FIRSTN_TAKE_FIRSTN] 1166 THEN RW_TAC list_ss 1167 [AP_TERM ``LENGTH:'a list->num`` (SPEC_ALL FIRSTN_TAKE_FIRSTN)] 1168 THEN RW_TAC list_ss [APPEND_FIRSTN_LASTN] 1169 THEN `~(LENGTH v1 = 0) /\ ~(LENGTH v2 = 0)` by PROVE_TAC[LENGTH_NIL] 1170 THEN ASSUM_LIST 1171 (fn thl => 1172 ASSUME_TAC 1173 (SIMP_RULE std_ss 1174 [LENGTH_APPEND] (AP_TERM ``LENGTH:'a letter list->num`` (el 9 thl)))) 1175 THENL 1176 [`LENGTH v1 <= LENGTH(FILTER (CLOCK c) l)` by DECIDE_TAC 1177 THEN RW_TAC list_ss [FIRSTN_TAKE_FIRSTN] 1178 THEN `TOP_FREE (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)` 1179 by PROVE_TAC[TOP_FREE_TAKE_FIRSTN] 1180 THEN `BOTTOM_FREE (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)` 1181 by PROVE_TAC[BOTTOM_FREE_TAKE_FIRSTN] 1182 THEN IMP_RES_TAC 1183 (GSYM 1184 (ISPECL[``CLOCK c``,``LENGTH(v1:'a letter list)``] 1185 FIRSTN_FILTER_TAKE_FIRSTN)) 1186 THEN ASSUM_LIST 1187 (fn thl => 1188 (ASSUME_TAC o GSYM) 1189 (SIMP_RULE std_ss 1190 [FIRSTN_LENGTH_APPEND, 1191 el 1 thl,el 2 thl,el 3 thl,el 4 thl,el 13 thl,el 14 thl] 1192 (Q.SPECL 1193 [`TAKE_FIRSTN (CLOCK c) (LENGTH(v1:'a letter list)) l`,`c`] 1194 (el 21 thl)))) 1195 THEN RW_TAC std_ss [] 1196 THEN `0 < LENGTH v1` by DECIDE_TAC 1197 THEN PROVE_TAC[LAST_TAKE_FIRSTN], 1198 `LENGTH v2 <= LENGTH(FILTER (CLOCK c) l)` by DECIDE_TAC 1199 THEN `LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) <= LENGTH l` 1200 by DECIDE_TAC 1201 THEN IMP_RES_TAC S_PROJ_S_CAT_LEMMA3 1202 THEN `LENGTH v2 > 0` by DECIDE_TAC 1203 THEN `LENGTH 1204 (FILTER (CLOCK c) 1205 (LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l)) > 0` 1206 by PROVE_TAC[] 1207 THEN IMP_RES_TAC LENGTH_FILTER_NON_EMPTY 1208 THEN ASSUM_LIST 1209 (fn thl => 1210 (ASSUME_TAC o GSYM) 1211 (SIMP_RULE list_ss 1212 [TOP_FREE_LASTN,BOTTOM_FREE_LASTN,LAST_LASTN_LAST, 1213 el 1 thl,el 5 thl,el 18 thl,el 19 thl,el 20 thl] 1214 (Q.SPECL 1215 [`LASTN 1216 (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH(v1:'a letter list)) l)) 1217 l`, 1218 `c`] 1219 (el 22 thl)))) 1220 THEN IMP_RES_TAC(DECIDE ``~(n = 0) ==> 0 < n``) 1221 THEN IMP_RES_TAC(DECIDE ``(n = n1+n2) ==> 0<n1 ==> 0<n2 ==> n1<n``) 1222 THEN IMP_RES_TAC LAST_LASTN_LAST 1223 THEN `LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) < LENGTH l` 1224 by PROVE_TAC[LENGTH_LESS_TAKE_FIRSTN] 1225 THEN IMP_RES_TAC 1226 (DECIDE ``(LENGTH l1):num < (LENGTH l2):num ==> 0 < LENGTH l2 - LENGTH l1``) 1227 THEN IMP_RES_TAC LAST_LASTN_LAST 1228 THEN ASSUM_LIST 1229 (fn thl => 1230 ASSUME_TAC(SIMP_RULE list_ss [el 1 thl,el 15 thl] (el 11 thl))) 1231 THEN RW_TAC std_ss [] 1232 THEN Cases_on `LENGTH l > 0` 1233 THEN RW_TAC std_ss [] 1234 THEN IMP_RES_TAC(DECIDE``~(LENGTH l:num > 0) ==> (LENGTH l = 0)``) 1235 THEN `l = []` by PROVE_TAC[LENGTH_NIL] 1236 THEN RW_TAC list_ss []]], 1237 Cases_on `v2` 1238 THEN RW_TAC list_ss [LAST_APPEND_CONS] 1239 THEN FULL_SIMP_TAC list_ss [TOP_FREE_APPEND,BOTTOM_FREE_APPEND] 1240 THEN RES_TAC 1241 THEN FULL_SIMP_TAC list_ss [], 1242 Q.EXISTS_TAC `FILTER (CLOCK c) v1` THEN Q.EXISTS_TAC `FILTER (CLOCK c) v2` 1243 THEN RW_TAC list_ss [FILTER_APPEND] 1244 THEN PROVE_TAC[TOP_FREE_APPEND,BOTTOM_FREE_APPEND]]); 1245 1246val LENGTH_TAKE_FIRST_SUC = 1247 store_thm 1248 ("LENGTH_TAKE_FIRST_SUC", 1249 ``!n P l. LENGTH(TAKE_FIRSTN P n l) <= LENGTH(TAKE_FIRSTN P (SUC n) l)``, 1250 Induct 1251 THEN RW_TAC list_ss [TAKE_FIRSTN_def] 1252 THEN Induct_on `l` 1253 THEN RW_TAC list_ss [TAKE_FIRST_def,TAKE_FIRSTN_def,BUTFIRSTN_ONE,BUTFIRSTN] 1254 THEN ASM_REWRITE_TAC[GSYM LENGTH_APPEND, GSYM TAKE_FIRSTN_def]); 1255 1256val LENGTH_TAKE_FIRST_MONO = 1257 store_thm 1258 ("LENGTH_TAKE_FIRST_MONO", 1259 ``!n m P l. m <= n ==> LENGTH(TAKE_FIRSTN P m l) <= LENGTH(TAKE_FIRSTN P n l)``, 1260 Induct 1261 THEN RW_TAC list_ss [] 1262 THEN Cases_on `m = SUC n` 1263 THEN RW_TAC list_ss [] 1264 THEN `m <= n` by DECIDE_TAC 1265 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 1266 THEN PROVE_TAC 1267 [LENGTH_TAKE_FIRST_SUC,DECIDE``(m:num) <= (n:num) /\ n <= (p:num) ==> m <= p``]); 1268 1269val LENGTH_TAKE_FIRST_GREATER = 1270 store_thm 1271 ("LENGTH_TAKE_FIRST_GREATER", 1272 ``!n P l. n <= LENGTH l ==> n <= LENGTH(TAKE_FIRSTN P n l)``, 1273 Induct 1274 THEN RW_TAC list_ss [TAKE_FIRSTN_def] 1275 THEN Induct_on `l` 1276 THEN RW_TAC list_ss [TAKE_FIRST_def,TAKE_FIRSTN_def,BUTFIRSTN_ONE,GSYM COND_RAND] 1277 THEN RES_TAC 1278 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 1279 THEN RW_TAC list_ss [DECIDE ``SUC n <= m + SUC p = n <= m + p``] 1280 THEN IMP_RES_TAC LENGTH_BUTFIRSTN 1281 THEN RW_TAC list_ss [BUTFIRSTN] 1282 THEN REWRITE_TAC[GSYM LENGTH_APPEND, GSYM TAKE_FIRSTN_def] 1283 THEN `LENGTH(TAKE_FIRSTN P n l) <= LENGTH(TAKE_FIRSTN P (SUC n) l)` 1284 by PROVE_TAC[LENGTH_TAKE_FIRST_SUC] 1285 THEN DECIDE_TAC); 1286 1287val S_PROJ_S_FUSION_TOP_LEMMA = 1288 store_thm 1289 ("S_PROJ_S_FUSION_TOP_LEMMA", 1290 ``0 < LENGTH l /\ TOP_FREE l 1291 ==> 1292 TOP_FREE 1293 (LAST(FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l) 1294 :: 1295 LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l)``, 1296 RW_TAC list_ss [] 1297 THEN `(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) <= LENGTH l` 1298 by PROVE_TAC[LENGTH_TAKE_FIRSTN] 1299 THEN `TOP_FREE(FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l)` 1300 by PROVE_TAC[TOP_FREE_FIRSTN] 1301 THEN `1 <= LENGTH l` by DECIDE_TAC 1302 THEN `1 <= LENGTH (TAKE_FIRSTN (CLOCK c) 1 l)` 1303 by PROVE_TAC[LENGTH_TAKE_FIRST_GREATER] 1304 THEN `1 <= SUC(LENGTH v1)` by DECIDE_TAC 1305 THEN `LENGTH (TAKE_FIRSTN (CLOCK c) 1 l) <= LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)` 1306 by PROVE_TAC[LENGTH_TAKE_FIRST_MONO] 1307 THEN `0 < LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)` 1308 by DECIDE_TAC 1309 THEN `TOP_FREE[LAST(TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)]` 1310 by PROVE_TAC[TOP_FREE_LAST,TOP_FREE_TAKE_FIRSTN] 1311 THEN `TOP_FREE[LAST(FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l)]` 1312 by PROVE_TAC[FIRSTN_TAKE_FIRSTN] 1313 THEN ONCE_REWRITE_TAC[GSYM(SIMP_CONV list_ss [] ``[x]<>l``)] 1314 THEN RW_TAC list_ss [TOP_FREE_APPEND,TOP_FREE_LASTN]); 1315 1316val S_PROJ_S_FUSION_BOTTOM_LEMMA = 1317 store_thm 1318 ("S_PROJ_S_FUSION_BOTTOM_LEMMA", 1319 ``0 < LENGTH l /\ BOTTOM_FREE l 1320 ==> 1321 BOTTOM_FREE 1322 (LAST(FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l) 1323 :: 1324 LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l)``, 1325 RW_TAC list_ss [] 1326 THEN `(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) <= LENGTH l` 1327 by PROVE_TAC[LENGTH_TAKE_FIRSTN] 1328 THEN `BOTTOM_FREE(FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l)` 1329 by PROVE_TAC[BOTTOM_FREE_FIRSTN] 1330 THEN `1 <= LENGTH l` by DECIDE_TAC 1331 THEN `1 <= LENGTH (TAKE_FIRSTN (CLOCK c) 1 l)` 1332 by PROVE_TAC[LENGTH_TAKE_FIRST_GREATER] 1333 THEN `1 <= SUC(LENGTH v1)` by DECIDE_TAC 1334 THEN `LENGTH (TAKE_FIRSTN (CLOCK c) 1 l) <= LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)` 1335 by PROVE_TAC[LENGTH_TAKE_FIRST_MONO] 1336 THEN `0 < LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)` 1337 by DECIDE_TAC 1338 THEN `BOTTOM_FREE[LAST(TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)]` 1339 by PROVE_TAC[BOTTOM_FREE_LAST,BOTTOM_FREE_TAKE_FIRSTN] 1340 THEN `BOTTOM_FREE[LAST(FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l)]` 1341 by PROVE_TAC[FIRSTN_TAKE_FIRSTN] 1342 THEN ONCE_REWRITE_TAC[GSYM(SIMP_CONV list_ss [] ``[x]<>l``)] 1343 THEN RW_TAC list_ss [BOTTOM_FREE_APPEND,BOTTOM_FREE_LASTN]); 1344 1345val S_PROJ_S_CAT_LEMMA4 = 1346 store_thm 1347 ("S_PROJ_S_CAT_LEMMA4", 1348 ``!v1 v2 l c. 1349 (FILTER (CLOCK c) l = v1 <> v2) 1350 ==> 1351 (FILTER 1352 (CLOCK c) 1353 (FIRSTN (LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l)) l) = 1354 v1)``, 1355 RW_TAC list_ss [] 1356 THEN `LENGTH(FILTER (CLOCK c) l) = LENGTH(v1 <> v2)` by PROVE_TAC[] 1357 THEN FULL_SIMP_TAC list_ss [LENGTH_APPEND] 1358 THEN `LENGTH v1 <= LENGTH (FILTER (CLOCK c) l)` by DECIDE_TAC 1359 THEN `LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 1360 THEN `LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) + 1361 LENGTH (TAKE_FIRSTN (CLOCK c) (LENGTH v1) l) = 1362 LENGTH l` by DECIDE_TAC 1363 THEN IMP_RES_TAC 1364 (Q.ISPECL 1365 [`LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK(c:'a bexp)) (LENGTH(v1:'a letter list)) l)`, 1366 `LENGTH (TAKE_FIRSTN (CLOCK(c:'a bexp)) (LENGTH(v1:'a letter list)) l)`, 1367 `l:'a letter list`] 1368 APPEND_FIRSTN_LASTN) 1369 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE list_ss [FILTER_APPEND] 1370 o AP_TERM ``FILTER (CLOCK c):'a letter list->'a letter list``) 1371 THEN IMP_RES_TAC S_PROJ_S_CAT_LEMMA3 1372 THEN PROVE_TAC[APPEND_RIGHT_CANCEL]); 1373 1374val S_PROJ_S_FUSION_LEMMA1 = 1375 store_thm 1376 ("S_PROJ_S_FUSION_LEMMA1", 1377 ``(FILTER (CLOCK c) l = v1 <> [l'] <> v2) 1378 ==> 1379 (FILTER (CLOCK c) 1380 (LASTN (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) l) 1381 = v2)``, 1382 ACCEPT_TAC 1383 (REWRITE_RULE 1384 [GSYM ADD1,LENGTH_TAKE_FIRSTN] 1385 (SIMP_RULE list_ss [] 1386 (Q.SPECL [`v2`,`v1<>[l']`,`l`,`c`](GEN_ALL S_PROJ_S_CAT_LEMMA3))))); 1387 1388val S_PROJ_S_FUSION_LEMMA2 = 1389 store_thm 1390 ("S_PROJ_S_FUSION_LEMMA2", 1391 ``(FILTER (CLOCK c) l = v1 <> [l'] <> v2) 1392 ==> 1393 (FILTER (CLOCK c) (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l) = v1 <> [l'])``, 1394 PROVE_TAC 1395 [LENGTH_TAKE_FIRSTN, FIRSTN_TAKE_FIRSTN, LENGTH_APPEND, 1396 (SIMP_RULE 1397 list_ss 1398 [LENGTH_APPEND,GSYM ADD1] 1399 (ISPECL 1400 [``(v1<>[l']) :'a letter list``, ``v2 :'a letter list``, ``l :'a letter list``, ``c :'a bexp``] 1401 S_PROJ_S_CAT_LEMMA4))]); 1402 1403val LAST_FILTER = (* Must be a nicer proof than this! *) 1404 store_thm 1405 ("LAST_FILTER", 1406 ``!P l. P(LAST l) ==> (LAST(FILTER P l) = LAST l)``, 1407 GEN_TAC 1408 THEN Induct 1409 THEN RW_TAC list_ss [] 1410 THEN Cases_on `l` 1411 THEN RW_TAC list_ss [] 1412 THEN FULL_SIMP_TAC list_ss [] 1413 THEN Cases_on `h=h'` 1414 THEN RW_TAC list_ss [] 1415 THEN RES_TAC 1416 THEN Cases_on `t = []` 1417 THEN RW_TAC list_ss [] 1418 THEN FULL_SIMP_TAC list_ss [] 1419 THEN `?x l'. t = x::l'` by PROVE_TAC[NULL_EQ_NIL,CONS] 1420 THEN ASM_REWRITE_TAC[LAST_CONS] 1421 THEN POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [GSYM th]) 1422 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE list_ss [el 1 thl,LAST_DEF] (el 4 thl))) 1423 THEN `~(LENGTH t = 0)` by PROVE_TAC[LENGTH_NIL] 1424 THEN `LENGTH t >= 1` by DECIDE_TAC 1425 THEN IMP_RES_TAC EL_PRE_LENGTH 1426 THEN `LENGTH t - 1 < LENGTH t` by DECIDE_TAC 1427 THEN `LENGTH t > 0` by DECIDE_TAC 1428 THEN `~(FILTER P t = [])` by PROVE_TAC[FILTER_NON_EMPTY] 1429 THEN PROVE_TAC[LAST_DEF]); 1430 1431val S_PROJ_S_FUSION_LEMMA3 = 1432 store_thm 1433 ("S_PROJ_S_FUSION_LEMMA3", 1434 ``!v1 l' v2. 1435 (FILTER (CLOCK c) l = v1 <> [l'] <> v2) 1436 ==> 1437 (LAST (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l) = l')``, 1438 RW_TAC list_ss [] 1439 THEN IMP_RES_TAC S_PROJ_S_FUSION_LEMMA2 1440 THEN `LAST(FILTER (CLOCK c) (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) = l'` 1441 by PROVE_TAC[LAST_SINGLETON] 1442 THEN `LENGTH(FILTER (CLOCK c) l) = LENGTH(v1 <> [l'] <> v2)` 1443 by PROVE_TAC[] 1444 THEN FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH] 1445 THEN `0 < SUC (LENGTH v1)` by DECIDE_TAC 1446 THEN `SUC (LENGTH v1) <= LENGTH(FILTER (CLOCK c) l)` 1447 by DECIDE_TAC 1448 THEN `CLOCK c (LAST (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l))` 1449 by PROVE_TAC[LAST_TAKE_FIRSTN] 1450 THEN PROVE_TAC[LAST_FILTER]); 1451 1452val FILTER_LAST = 1453 store_thm 1454 ("FILTER_LAST", 1455 ``!P l l' x. (FILTER P l = l' <> [x]) ==> P x``, 1456 GEN_TAC 1457 THEN Induct 1458 THEN RW_TAC list_ss [] 1459 THEN `TL(h::FILTER P l) = TL(l' <> [x])` by PROVE_TAC[] 1460 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE list_ss []) 1461 THEN Cases_on `l'` 1462 THEN RW_TAC list_ss [] 1463 THEN FULL_SIMP_TAC list_ss []); 1464 1465val S_PROJ_S_FUSION = 1466 store_thm 1467 ("S_PROJ_S_FUSION", 1468 ``(!l c. S_CLOCK_FREE r /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1469 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r = S_SEM l c r)) 1470 /\ 1471 (!l c. S_CLOCK_FREE r' /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1472 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r' = S_SEM l c r')) 1473 ==> 1474 !l c. S_CLOCK_FREE (S_FUSION (r,r')) /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1475 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) (S_FUSION (r,r')) = 1476 S_SEM l c (S_FUSION (r,r')))``, 1477 RW_TAC list_ss [LIST_PROJ_def,S_SEM_def,US_SEM_def,S_CLOCK_FREE_def] 1478 THEN RW_TAC list_ss [CLOCK_TICK_def,ELEM_EL] 1479 THEN RW_TAC (list_ss++resq_SS) [] 1480 THEN EQ_TAC 1481 THEN RW_TAC list_ss [FILTER_APPEND] 1482 THENL 1483 [Cases_on `l = []` 1484 THEN RW_TAC list_ss [] 1485 THEN FULL_SIMP_TAC list_ss [] 1486 THEN `0 < SUC(LENGTH v1)` by DECIDE_TAC 1487 THEN `~(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l = [])` by PROVE_TAC[TAKE_FIRSTN_NIL] 1488 THEN Q.EXISTS_TAC `BUTLAST(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)` 1489 THEN Q.EXISTS_TAC `LASTN (LENGTH l - LENGTH(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)) l` 1490 THEN Q.EXISTS_TAC `LAST(TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)` 1491 THEN RW_TAC list_ss [APPEND_FRONT_LAST] 1492 THEN ONCE_REWRITE_TAC[GSYM FIRSTN_TAKE_FIRSTN] 1493 THEN RW_TAC list_ss 1494 [AP_TERM ``LENGTH:'a list->num`` (SPEC_ALL FIRSTN_TAKE_FIRSTN)] 1495 THENL 1496 [`LENGTH (TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l) <= LENGTH l` 1497 by PROVE_TAC[LENGTH_TAKE_FIRSTN] 1498 THEN `(LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)) 1499 + (LENGTH (TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)) = 1500 LENGTH l` by DECIDE_TAC 1501 THEN RW_TAC list_ss [APPEND_FIRSTN_LASTN], 1502 RW_TAC list_ss [FIRSTN_TAKE_FIRSTN] 1503 THEN `TOP_FREE (TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)` 1504 by PROVE_TAC[TOP_FREE_TAKE_FIRSTN] 1505 THEN `BOTTOM_FREE (TAKE_FIRSTN (CLOCK c) (SUC(LENGTH v1)) l)` 1506 by PROVE_TAC[BOTTOM_FREE_TAKE_FIRSTN] 1507 THEN ASSUM_LIST 1508 (fn thl => 1509 ASSUME_TAC 1510 (SIMP_RULE list_ss 1511 [LENGTH_APPEND] (AP_TERM ``LENGTH:'a letter list->num`` (el 8 thl)))) 1512 THEN `SUC (LENGTH v1) <= LENGTH (FILTER (CLOCK c) l)` by DECIDE_TAC 1513 THEN IMP_RES_TAC 1514 (GSYM 1515 (ISPECL[``CLOCK c``,``SUC(LENGTH(v1:'a letter list))``] 1516 FIRSTN_FILTER_TAKE_FIRSTN)) 1517 THEN `SUC(LENGTH v1) = LENGTH(v1 <> [l'])` by RW_TAC list_ss [] 1518 THEN ASSUM_LIST 1519 (fn thl => 1520 (ASSUME_TAC o GSYM) 1521 (SIMP_RULE std_ss 1522 [FIRSTN_LENGTH_APPEND, 1523 el 1 thl,el 2 thl,el 4 thl,el 5 thl,el 6 thl,el 11 thl,el 12 thl] 1524 (Q.SPECL 1525 [`TAKE_FIRSTN (CLOCK c) (SUC(LENGTH(v1:'a letter list))) l`,`c`] 1526 (el 19 thl)))) 1527 THEN RW_TAC std_ss [] 1528 THEN `0 < LENGTH(v1 <> [l'])` by RW_TAC list_ss [] 1529 THEN `LENGTH(v1 <> [l']) <= LENGTH (FILTER (CLOCK c) l)` by RW_TAC list_ss [] 1530 THEN PROVE_TAC[LAST_TAKE_FIRSTN], 1531 `~(LENGTH l = 0)` by PROVE_TAC[LENGTH_NIL] 1532 THEN `0 < LENGTH l` by DECIDE_TAC 1533 THEN ASSUM_LIST 1534 (fn thl => 1535 (ASSUME_TAC o GSYM) 1536 (SIMP_RULE std_ss 1537 [S_PROJ_S_FUSION_TOP_LEMMA,S_PROJ_S_FUSION_BOTTOM_LEMMA,FIRSTN_TAKE_FIRSTN, 1538 el 1 thl,el 10 thl,el 11 thl] 1539 (Q.SPECL 1540 [`(LAST 1541 (FIRSTN 1542 (LENGTH 1543 (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH(v1:'a letter list))) l)) l) 1544 :: 1545 LASTN 1546 (LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l)) 1547 l)`, 1548 `c`] 1549 (el 14 thl)))) 1550 THEN ASM_REWRITE_TAC[FIRSTN_TAKE_FIRSTN] 1551 THEN POP_ASSUM(K ALL_TAC) 1552 THEN ASSUM_LIST 1553 (fn thl => 1554 ASSUME_TAC 1555 (SIMP_RULE list_ss 1556 [LENGTH_APPEND] (AP_TERM ``LENGTH:'a letter list->num`` (el 8 thl)))) 1557 THEN `SUC (LENGTH v1) <= LENGTH(FILTER (CLOCK c) l)` by DECIDE_TAC 1558 THEN RW_TAC std_ss [] 1559 THENL 1560 [Cases_on `(LENGTH l - LENGTH (TAKE_FIRSTN (CLOCK c) (SUC (LENGTH v1)) l))` 1561 THEN RW_TAC list_ss [LASTN,LAST_TAKE_FIRSTN] 1562 THEN `SUC n <= LENGTH l` by DECIDE_TAC 1563 THEN Cases_on `LASTN (SUC n) l = []` 1564 THEN RW_TAC list_ss [LAST_LASTN_LAST,LAST_TAKE_FIRSTN] 1565 THEN `?x l'. LASTN (SUC n) l = x::l'` by PROVE_TAC[NULL_EQ_NIL,CONS] 1566 THEN RW_TAC list_ss [LAST_CONS] 1567 THEN POP_ASSUM(fn th => REWRITE_TAC[GSYM th]) 1568 THEN RW_TAC list_ss [LAST_LASTN_LAST], 1569 IMP_RES_TAC S_PROJ_S_FUSION_LEMMA3 1570 THEN ASM_REWRITE_TAC [] 1571 THEN IMP_RES_TAC S_PROJ_S_FUSION_LEMMA1 1572 THEN IMP_RES_TAC S_PROJ_S_FUSION_LEMMA2 1573 THEN ONCE_REWRITE_TAC[GSYM(SIMP_CONV list_ss [] ``[x]<>l``)] 1574 THEN ASM_REWRITE_TAC[FILTER_APPEND] 1575 THEN IMP_RES_TAC FILTER_LAST 1576 THEN RW_TAC list_ss []]], 1577 Cases_on `v2` 1578 THEN RW_TAC list_ss [LAST_APPEND_CONS] 1579 THEN IMP_RES_TAC S_CLOCK_LAST 1580 THEN FULL_SIMP_TAC list_ss [TOP_FREE_APPEND,BOTTOM_FREE_APPEND,LAST_SINGLETON], 1581 Q.EXISTS_TAC `FILTER (CLOCK c) v1` 1582 THEN Q.EXISTS_TAC `FILTER (CLOCK c) v2` 1583 THEN Q.EXISTS_TAC `l'` 1584 THEN RW_TAC list_ss [FILTER_APPEND] 1585 THENL 1586 [IMP_RES_TAC S_CLOCK_LAST 1587 THEN FULL_SIMP_TAC list_ss [LAST_SINGLETON], 1588 `TOP_FREE(v1 <> [l'])` by PROVE_TAC[TOP_FREE_APPEND] 1589 THEN `BOTTOM_FREE(v1 <> [l'])` by PROVE_TAC[BOTTOM_FREE_APPEND] 1590 THEN `US_SEM (FILTER (CLOCK c)(v1 <> [l'])) r` by PROVE_TAC[] 1591 THEN IMP_RES_TAC S_CLOCK_LAST 1592 THEN FULL_SIMP_TAC list_ss [FILTER_APPEND,LAST_SINGLETON], 1593 `TOP_FREE([l'] <> v2)` by PROVE_TAC[TOP_FREE_APPEND] 1594 THEN `BOTTOM_FREE([l'] <> v2)` by PROVE_TAC[BOTTOM_FREE_APPEND] 1595 THEN FULL_SIMP_TAC list_ss [] 1596 THEN `US_SEM (FILTER (CLOCK c)(l' :: v2)) r'` by PROVE_TAC[] 1597 THEN IMP_RES_TAC S_CLOCK_LAST 1598 THEN FULL_SIMP_TAC list_ss [FILTER_APPEND,LAST_SINGLETON]]]); 1599 1600val US_SEM_S_EMPTY = 1601 store_thm 1602 ("US_SEM_S_EMPTY", 1603 ``US_SEM l S_EMPTY = (l = [])``, 1604 RW_TAC std_ss [US_SEM_def]); 1605 1606val S_SEM_S_EMPTY = 1607 store_thm 1608 ("S_SEM_S_EMPTY", 1609 ``S_SEM l c S_EMPTY = (l = [])``, 1610 RW_TAC std_ss [S_SEM_def]); 1611 1612val S_PROJ_S_EMPTY = 1613 store_thm 1614 ("S_PROJ_S_EMPTY", 1615 ``!l c. 1616 TOP_FREE l /\ BOTTOM_FREE l ==> 1617 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ 1618 US_SEM (LIST_PROJ l c) S_EMPTY = 1619 S_SEM l c S_EMPTY)``, 1620 RW_TAC list_ss [S_SEM_def,US_SEM_def] 1621 THEN EQ_TAC 1622 THEN RW_TAC list_ss [CLOCK_def,BOTTOM_FREE_def] 1623 THEN FULL_SIMP_TAC list_ss [LIST_PROJ_def,GSYM CLOCK_def] 1624 THEN IMP_RES_TAC LAST_FILTER_NON_EMPTY 1625 THEN Cases_on `l = []` 1626 THEN RW_TAC list_ss [] 1627 THEN `~(LENGTH l = 0)` by PROVE_TAC[LENGTH_NIL] 1628 THEN `LENGTH l > 0` by DECIDE_TAC 1629 THEN PROVE_TAC[LAST_FILTER_NON_EMPTY]); 1630 1631val S_CATN_def = 1632 Define 1633 `(S_CATN 0 r = S_EMPTY) /\ (S_CATN (SUC n) r = S_CAT(r, S_CATN n r))`; 1634 1635val US_SEM_REPEAT_CATN = 1636 store_thm 1637 ("US_SEM_REPEAT_CATN", 1638 ``!v r. US_SEM v (S_REPEAT r) = ?n. US_SEM v (S_CATN n r)``, 1639 RW_TAC list_ss [US_SEM_def] 1640 THEN EQ_TAC 1641 THEN RW_TAC std_ss [] 1642 THENL 1643 [Induct_on `vlist` 1644 THEN RW_TAC list_ss [CONCAT_def] 1645 THENL 1646 [Q.EXISTS_TAC `0` 1647 THEN RW_TAC list_ss [S_CATN_def,US_SEM_S_EMPTY], 1648 RES_TAC 1649 THEN Q.EXISTS_TAC `SUC n` 1650 THEN RW_TAC list_ss [S_CATN_def,US_SEM_def] 1651 THEN Q.EXISTS_TAC `h` 1652 THEN Q.EXISTS_TAC `CONCAT vlist` 1653 THEN RW_TAC list_ss []], 1654 Q.UNDISCH_TAC `US_SEM v (S_CATN n r)` 1655 THEN Q.SPEC_TAC(`v`,`v`) 1656 THEN Q.SPEC_TAC(`r`,`r`) 1657 THEN Q.SPEC_TAC(`n`,`n`) 1658 THEN Induct 1659 THEN RW_TAC list_ss [S_CATN_def,US_SEM_S_EMPTY] 1660 THENL 1661 [Q.EXISTS_TAC `[]` 1662 THEN RW_TAC list_ss [CONCAT_def], 1663 FULL_SIMP_TAC list_ss [US_SEM_def] 1664 THEN RES_TAC 1665 THEN RW_TAC std_ss [] 1666 THEN Q.EXISTS_TAC `v1::vlist` 1667 THEN RW_TAC list_ss [CONCAT_def]]]); 1668 1669 1670val S_SEM_REPEAT_CATN = 1671 store_thm 1672 ("S_SEM_REPEAT_CATN", 1673 ``!v r c. S_SEM v c (S_REPEAT r) = ?n. S_SEM v c (S_CATN n r)``, 1674 RW_TAC list_ss [S_SEM_def] 1675 THEN EQ_TAC 1676 THEN RW_TAC std_ss [] 1677 THENL 1678 [Induct_on `vlist` 1679 THEN RW_TAC list_ss [CONCAT_def] 1680 THENL 1681 [Q.EXISTS_TAC `0` 1682 THEN RW_TAC list_ss [S_CATN_def,S_SEM_S_EMPTY], 1683 RES_TAC 1684 THEN Q.EXISTS_TAC `SUC n` 1685 THEN RW_TAC list_ss [S_CATN_def,S_SEM_def] 1686 THEN Q.EXISTS_TAC `h` 1687 THEN Q.EXISTS_TAC `CONCAT vlist` 1688 THEN RW_TAC list_ss []], 1689 Q.UNDISCH_TAC `S_SEM v c (S_CATN n r)` 1690 THEN Q.SPEC_TAC(`v`,`v`) 1691 THEN Q.SPEC_TAC(`r`,`r`) 1692 THEN Q.SPEC_TAC(`n`,`n`) 1693 THEN Induct 1694 THEN RW_TAC list_ss [S_CATN_def,S_SEM_S_EMPTY] 1695 THENL 1696 [Q.EXISTS_TAC `[]` 1697 THEN RW_TAC list_ss [CONCAT_def], 1698 FULL_SIMP_TAC list_ss [S_SEM_def] 1699 THEN RES_TAC 1700 THEN RW_TAC std_ss [] 1701 THEN Q.EXISTS_TAC `v1::vlist` 1702 THEN RW_TAC list_ss [CONCAT_def]]]); 1703 1704val S_PROJ_CORRECT_def = 1705 Define 1706 `S_PROJ_CORRECT r = 1707 !l c. 1708 S_CLOCK_FREE r /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1709 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r = S_SEM l c r)`; 1710 1711val S_PROJ_CORRECT_EMPTY = 1712 store_thm 1713 ("S_PROJ_CORRECT_EMPTY", 1714 ``S_PROJ_CORRECT S_EMPTY``, 1715 RW_TAC std_ss [S_PROJ_CORRECT_def,S_PROJ_S_EMPTY]); 1716 1717val S_PROJ_CORRECT_CAT = 1718 store_thm 1719 ("S_PROJ_CORRECT_CAT", 1720 ``!r1 r2. S_PROJ_CORRECT r1 /\ S_PROJ_CORRECT r2 1721 ==> 1722 S_PROJ_CORRECT(S_CAT(r1,r2))``, 1723 RW_TAC std_ss [S_PROJ_CORRECT_def,S_PROJ_S_CAT]); 1724 1725val S_PROJ_CORRECT_CATN = 1726 store_thm 1727 ("S_PROJ_CORRECT_CATN", 1728 ``!r. S_PROJ_CORRECT r ==> !n. S_PROJ_CORRECT(S_CATN n r)``, 1729 GEN_TAC THEN DISCH_TAC 1730 THEN Induct 1731 THEN RW_TAC std_ss [S_CATN_def,S_PROJ_CORRECT_EMPTY,S_PROJ_CORRECT_CAT]); 1732 1733val S_CLOCK_FREE_CATN = 1734 store_thm 1735 ("S_CLOCK_FREE_CATN", 1736 ``!r. S_CLOCK_FREE r ==> !n. S_CLOCK_FREE(S_CATN n r)``, 1737 GEN_TAC THEN DISCH_TAC 1738 THEN Induct 1739 THEN RW_TAC list_ss [S_CATN_def,S_CLOCK_FREE_def]); 1740 1741val S_PROJ_S_REPEAT = 1742 store_thm 1743 ("S_PROJ_S_REPEAT", 1744 ``(!l c. 1745 S_CLOCK_FREE r /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1746 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r = S_SEM l c r)) 1747 ==> 1748 !l c. 1749 S_CLOCK_FREE (S_REPEAT r) /\ TOP_FREE l /\ BOTTOM_FREE l ==> 1750 ((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ 1751 US_SEM (LIST_PROJ l c) (S_REPEAT r) = 1752 S_SEM l c (S_REPEAT r))``, 1753 RW_TAC std_ss [US_SEM_REPEAT_CATN,S_SEM_REPEAT_CATN,S_CLOCK_FREE_def] 1754 THEN EQ_TAC 1755 THEN RW_TAC list_ss [] 1756 THEN FULL_SIMP_TAC std_ss [GSYM S_PROJ_CORRECT_def] 1757 THEN `S_CLOCK_FREE(S_CATN n r)` by PROVE_TAC[S_CLOCK_FREE_CATN] 1758 THEN IMP_RES_TAC S_PROJ_CORRECT_CATN 1759 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [S_PROJ_CORRECT_def] o SPEC_ALL) 1760 THEN PROVE_TAC[]); 1761 1762val S_PROJ = 1763 store_thm 1764 ("S_PROJ", 1765 ``!r. 1766 S_CLOCK_FREE r 1767 ==> 1768 !l. TOP_FREE l /\ BOTTOM_FREE l 1769 ==> 1770 !c. S_SEM l c r = (LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r``, 1771 INDUCT_THEN sere_induct ASSUME_TAC 1772 THENL 1773 [(* S_BOOL b *) 1774 RW_TAC std_ss [S_PROJ_S_BOOL], 1775 (* S_CAT(r,r') *) 1776 RW_TAC std_ss [S_PROJ_S_CAT], 1777 (* S_FUSION (r,r') *) 1778 RW_TAC std_ss [S_PROJ_S_FUSION], 1779 (* S_OR (r,r') *) 1780 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 1781 THEN EQ_TAC 1782 THEN ZAP_TAC list_ss [CLOCK_def], 1783 (* S_AND (r,r') *) 1784 RW_TAC list_ss [S_SEM_def,US_SEM_def,CLOCK_def,S_CLOCK_FREE_def] 1785 THEN EQ_TAC 1786 THEN ZAP_TAC list_ss [CLOCK_def], 1787 (* S_EMPTY *) 1788 PROVE_TAC[S_PROJ_S_EMPTY], (* for some reason RW_TAC std_ss [S_PROJ_S_EMPTY] fails *) 1789 (* S_REPEAT r *) 1790 RW_TAC std_ss [S_PROJ_S_REPEAT], 1791 (* S_CLOCK (r,p_2) *) 1792 RW_TAC list_ss [S_CLOCK_FREE_def]]); 1793 1794val S_PROJ_COR = 1795 store_thm 1796 ("S_PROJ_COR", 1797 ``!r l c. 1798 S_CLOCK_FREE r 1799 ==> 1800 TOP_FREE l /\ BOTTOM_FREE l 1801 ==> 1802 (S_SEM l c r = 1803 (LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r)``, 1804 PROVE_TAC[S_PROJ]); 1805 1806(*****************************************************************************) 1807(* Start developing projection view for formulas *) 1808(*****************************************************************************) 1809 1810(*****************************************************************************) 1811(* Switch default to general (i.e. finite or infinite) paths *) 1812(*****************************************************************************) 1813open PSLPathTheory; 1814 1815(****************************************************************************** 1816* FUN_FILTER_COUNT P f m n = P is true for the mth time in f at position n 1817******************************************************************************) 1818val FUN_FILTER_COUNT_def = 1819 Define 1820 `(FUN_FILTER_COUNT P f 0 n = P(f n) /\ !i :: LESS n. ~P(f i)) 1821 /\ 1822 (FUN_FILTER_COUNT P f (SUC m) n = 1823 ?n' :: LESS n. 1824 FUN_FILTER_COUNT P f m n' /\ P(f n) /\ !i :: LESS n. n' < i ==> ~P(f i))`; 1825 1826val PATH_FILTER_def = 1827 Define 1828 `(PATH_FILTER P (FINITE l) = FINITE(FILTER P l)) 1829 /\ 1830 (PATH_FILTER P (INFINITE f) = 1831 if (!m:num. ?n. m <= n /\ P(f n)) 1832 then INFINITE(f o (\m. LEAST n. FUN_FILTER_COUNT P f m n)) 1833 else FINITE(FILTER P (GENLIST f (LEAST i. !j. i <= j ==> ~P(f j)))))`; 1834 1835val PROJ_def = Define `PROJ p c = PATH_FILTER (CLOCK c) p`; 1836 1837val FUN_FILTER_COUNT_UNIQUE = 1838 store_thm 1839 ("FUN_FILTER_COUNT_UNIQUE", 1840 ``!P f m n1 n2. 1841 FUN_FILTER_COUNT P f m n1 /\ FUN_FILTER_COUNT P f m n2 ==> (n1 = n2)``, 1842 GEN_TAC THEN GEN_TAC 1843 THEN Induct 1844 THEN RW_TAC (list_ss++resq_SS) [FUN_FILTER_COUNT_def] 1845 THENL 1846 [Cases_on `n1 < n2` 1847 THEN RES_TAC 1848 THEN Cases_on `n2 < n1` 1849 THEN RES_TAC 1850 THEN DECIDE_TAC, 1851 `n' = n''` by PROVE_TAC[] 1852 THEN Cases_on `n1 < n2` 1853 THEN RW_TAC std_ss [] 1854 THEN RES_TAC 1855 THEN Cases_on `n2 < n1` 1856 THEN RES_TAC 1857 THEN DECIDE_TAC]); 1858 1859(* 1860val PROJ_def = 1861 Define 1862 `(PROJ (FINITE l) c = FINITE(LIST_PROJ l c)) 1863 /\ 1864 (PROJ (INFINITE f) c = 1865 if !m. ?n. FUN_FILTER_COUNT (CLOCK c) f m n 1866 then INFINITE(\m. f(@n. FUN_FILTER_COUNT (CLOCK c) f m n)) 1867 else FINITE 1868 (FILTER 1869 (CLOCK c) 1870 (GENLIST f (LEAST i. !j. j > i ==> ~CLOCK c (f j)))))`; 1871*) 1872 1873(****************************************************************************** 1874* F_CLOCK_FREE f means f contains no clocking statements 1875******************************************************************************) 1876val F_CLOCK_FREE_def = 1877 Define 1878 `(F_CLOCK_FREE (F_STRONG_BOOL b) = T) 1879 /\ 1880 (F_CLOCK_FREE (F_WEAK_BOOL b) = T) 1881 /\ 1882 (F_CLOCK_FREE (F_NOT f) = F_CLOCK_FREE f) 1883 /\ 1884 (F_CLOCK_FREE (F_AND(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2) 1885 /\ 1886 (F_CLOCK_FREE (F_STRONG_SERE r) = S_CLOCK_FREE r) 1887 /\ 1888 (F_CLOCK_FREE (F_WEAK_SERE r) = S_CLOCK_FREE r) 1889 /\ 1890 (F_CLOCK_FREE (F_NEXT f) = F_CLOCK_FREE f) 1891 /\ 1892 (F_CLOCK_FREE (F_UNTIL(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2) 1893 /\ 1894 (F_CLOCK_FREE (F_ABORT (f,b)) = F_CLOCK_FREE f) 1895 /\ 1896 (F_CLOCK_FREE (F_SUFFIX_IMP(r,f)) = F_CLOCK_FREE f /\ S_CLOCK_FREE r) 1897 /\ 1898 (F_CLOCK_FREE (F_CLOCK v) = F)`; 1899 1900val PATH_TOP_FREE_def = 1901 Define 1902 `(PATH_TOP_FREE(FINITE l) = TOP_FREE l) 1903 /\ 1904 (PATH_TOP_FREE(INFINITE f) = !n. ~(f n = TOP))`; 1905 1906val PATH_BOTTOM_FREE_def = 1907 Define 1908 `(PATH_BOTTOM_FREE(FINITE l) = BOTTOM_FREE l) 1909 /\ 1910 (PATH_BOTTOM_FREE(INFINITE f) = !n. ~(f n = BOTTOM))`; 1911 1912val HD_RESTN_TL = 1913 store_thm 1914 ("HD_RESTN_TL", 1915 ``!n l. HD (RESTN (TL l) n) = EL n (TL l)``, 1916 Induct 1917 THEN RW_TAC list_ss 1918 [FinitePSLPathTheory.RESTN_def,FinitePSLPathTheory.REST_def,EL]); 1919 1920val ELEM_FINITE = 1921 store_thm 1922 ("ELEM_FINITE", 1923 ``!n l. ELEM (FINITE l) n = EL n l``, 1924 Induct 1925 THEN RW_TAC list_ss 1926 [ELEM_def,HEAD_def,RESTN_def, 1927 FinitePSLPathTheory.RESTN_def,FinitePSLPathTheory.REST_def, 1928 REST_def,RESTN_FINITE,HD_RESTN_TL,EL]); 1929 1930val ELEM_INFINITE = 1931 store_thm 1932 ("ELEM_INFINITE", 1933 ``!n f. ELEM (INFINITE f) n = f n``, 1934 Induct 1935 THEN RW_TAC list_ss 1936 [ELEM_def,HEAD_def,RESTN_INFINITE]); 1937 1938val LENGTH_FILTER_NON_ZERO_EXISTS = 1939 store_thm 1940 ("LENGTH_FILTER_NON_ZERO_EXISTS", 1941 ``!P l. LENGTH (FILTER P l) > 0 ==> ?n. n < LENGTH l /\ P (EL n l)``, 1942 GEN_TAC 1943 THEN Induct 1944 THEN RW_TAC list_ss [] 1945 THENL 1946 [Q.EXISTS_TAC `0` 1947 THEN RW_TAC list_ss [], 1948 RES_TAC 1949 THEN Q.EXISTS_TAC `SUC n` 1950 THEN RW_TAC list_ss []]); 1951 1952val NON_ZERO_EXISTS_LENGTH_FILTER = 1953 store_thm 1954 ("NON_ZERO_EXISTS_LENGTH_FILTER", 1955 ``!P l n. n < LENGTH l /\ P (EL n l) ==> LENGTH (FILTER P l) > 0``, 1956 GEN_TAC 1957 THEN Induct 1958 THEN RW_TAC list_ss [] 1959 THEN Cases_on `n` 1960 THEN RW_TAC list_ss [] 1961 THEN FULL_SIMP_TAC list_ss [] 1962 THEN RES_TAC); 1963 1964 1965(* 1966val FUN_FILTER_COUNT = 1967 store_thm 1968 ("FUN_FILTER_COUNT", 1969 ``!P f. 1970 (!m. ?n. FUN_FILTER_COUNT P f m n) 1971 ==> 1972 !m. 1973 FUN_FILTER_COUNT P f m ((\m. @n. FUN_FILTER_COUNT P f m n)m)``, 1974 RW_TAC std_ss [] 1975 THEN POP_ASSUM(STRIP_ASSUME_TAC o SPEC_ALL) 1976 THEN IMP_RES_TAC SELECT_AX 1977 THEN CONV_TAC(DEPTH_CONV ETA_CONV) 1978 THEN RW_TAC std_ss []); 1979*) 1980 1981val FUN_FILTER_COUNT = 1982 store_thm 1983 ("FUN_FILTER_COUNT", 1984 ``!P f. 1985 (!m. ?n. FUN_FILTER_COUNT P f m n) 1986 ==> 1987 !m. 1988 FUN_FILTER_COUNT P f m (@n. FUN_FILTER_COUNT P f m n)``, 1989 RW_TAC std_ss [] 1990 THEN POP_ASSUM(STRIP_ASSUME_TAC o SPEC_ALL) 1991 THEN IMP_RES_TAC SELECT_AX 1992 THEN CONV_TAC(DEPTH_CONV ETA_CONV) 1993 THEN RW_TAC std_ss []); 1994 1995val FUN_FILTER_COUNT_EXISTS = 1996 store_thm 1997 ("FUN_FILTER_COUNT_EXISTS", 1998 ``!P f. 1999 (!n:num. ?n'. n <= n' /\ P(f n')) 2000 ==> 2001 !m. ?n. FUN_FILTER_COUNT P f m n``, 2002 RW_TAC std_ss [] 2003 THEN Induct_on `m` 2004 THEN RW_TAC (list_ss++resq_SS) [FUN_FILTER_COUNT_def] 2005 THENL 2006 [POP_ASSUM(STRIP_ASSUME_TAC o SPEC ``0``) 2007 THEN FULL_SIMP_TAC arith_ss [] 2008 THEN IMP_RES_TAC 2009 (SIMP_RULE std_ss [] 2010 (ISPEC ``(P :'a -> bool) o (f :num -> 'a)`` LEAST_EXISTS)) 2011 THEN Q.EXISTS_TAC `$LEAST (P o f)` 2012 THEN RW_TAC arith_ss [], 2013 ASSUM_LIST(fn thl => STRIP_ASSUME_TAC(Q.SPEC `SUC n` (el 2 thl))) 2014 THEN IMP_RES_TAC 2015 (SIMP_RULE std_ss [] 2016 (ISPEC ``\n':num. (P :'a -> bool)(f n') /\ SUC n <= n'`` LEAST_EXISTS)) 2017 THEN Q.EXISTS_TAC `LEAST n'. P (f n') /\ SUC n <= n'` 2018 THEN Q.EXISTS_TAC `n` 2019 THEN RW_TAC arith_ss [] 2020 THEN `SUC n <= i` by DECIDE_TAC 2021 THEN Cases_on `P (f i)` 2022 THEN RW_TAC arith_ss [] 2023 THEN IMP_RES_TAC LESS_LEAST 2024 THEN POP_ASSUM(STRIP_ASSUME_TAC o REWRITE_RULE[GSYM NOT_LESS] o SIMP_RULE std_ss [])]); 2025 2026val NOT_FUN_FILTER_COUNT = 2027 store_thm 2028 ("NOT_FUN_FILTER_COUNT", 2029 ``!P f. 2030 ~(!m. ?n. FUN_FILTER_COUNT P f m n) 2031 ==> 2032 ?n:num. !n'. n <= n' ==> ~P(f n')``, 2033 PROVE_TAC[FUN_FILTER_COUNT_EXISTS]); 2034 2035val LEAST0 = 2036 store_thm 2037 ("LEAST0", 2038 ``!P. (?i. P i) /\ ((LEAST i. P i) = 0) = P 0``, 2039 GEN_TAC 2040 THEN EQ_TAC 2041 THEN ZAP_TAC list_ss [LESS_LEAST] 2042 THEN IMP_RES_TAC FULL_LEAST_INTRO 2043 THENL 2044 [ASSUM_LIST 2045 (fn thl => ASSUME_TAC(GSYM(CONV_RULE(DEPTH_CONV ETA_CONV)(el 5 thl)))) 2046 THEN RW_TAC arith_ss [], 2047 CONV_TAC(DEPTH_CONV ETA_CONV) 2048 THEN DECIDE_TAC]); 2049 2050val IS_LEAST_def = 2051 Define 2052 `IS_LEAST P n = P n /\ !m:num. m < n ==> ~P m`; 2053 2054val IS_LEAST_UNIQUE = 2055 store_thm 2056 ("IS_LEAST_UNIQUE", 2057 ``!P m n. IS_LEAST P m /\ IS_LEAST P n ==> (m = n)``, 2058 RW_TAC arith_ss [IS_LEAST_def] 2059 THEN Cases_on `m < n` 2060 THEN RES_TAC 2061 THEN Cases_on `n < m` 2062 THEN RES_TAC 2063 THEN DECIDE_TAC); 2064 2065val IS_LEAST_SUC = 2066 store_thm 2067 ("IS_LEAST_SUC", 2068 ``!P n. ~(P 0) ==> (IS_LEAST P (SUC n) = IS_LEAST (P o SUC) n)``, 2069 RW_TAC arith_ss [IS_LEAST_def] 2070 THEN EQ_TAC 2071 THEN RW_TAC arith_ss [] 2072 THEN Cases_on `m = 0` 2073 THEN RW_TAC arith_ss [] 2074 THEN `PRE m < n` by DECIDE_TAC 2075 THEN `SUC(PRE m) = m` by DECIDE_TAC 2076 THEN PROVE_TAC[]); 2077 2078val IS_LEAST_LEAST = 2079 store_thm 2080 ("IS_LEAST_LEAST", 2081 ``!P n. P n ==> IS_LEAST P (LEAST n. P n)``, 2082 CONV_TAC(DEPTH_CONV ETA_CONV) 2083 THEN RW_TAC std_ss [IS_LEAST_def] 2084 THEN IMP_RES_TAC LEAST_INTRO 2085 THEN IMP_RES_TAC LESS_LEAST); 2086 2087val IS_LEAST_EQ_IMP = 2088 store_thm 2089 ("IS_LEAST_EQ_IMP", 2090 ``!P m. IS_LEAST P m ==> (m = $LEAST P)``, 2091 RW_TAC std_ss [] 2092 THEN IMP_RES_TAC IS_LEAST_def 2093 THEN IMP_RES_TAC IS_LEAST_LEAST 2094 THEN IMP_RES_TAC IS_LEAST_UNIQUE 2095 THEN RW_TAC std_ss [] 2096 THEN CONV_TAC(DEPTH_CONV ETA_CONV) 2097 THEN RW_TAC std_ss []); 2098 2099val IS_LEAST_EQ = 2100 store_thm 2101 ("IS_LEAST_EQ", 2102 ``!P n. IS_LEAST P n = (?n. P n) /\ (n = $LEAST P)``, 2103 RW_TAC std_ss [] 2104 THEN EQ_TAC 2105 THEN RW_TAC std_ss [] 2106 THENL 2107 [IMP_RES_TAC IS_LEAST_def 2108 THEN PROVE_TAC[], 2109 IMP_RES_TAC IS_LEAST_EQ_IMP, 2110 IMP_RES_TAC IS_LEAST_LEAST 2111 THEN POP_ASSUM(ASSUME_TAC o CONV_RULE(DEPTH_CONV ETA_CONV)) 2112 THEN PROVE_TAC[]]); 2113 2114val LEAST_SUC = 2115 store_thm 2116 ("LEAST_SUC", 2117 ``!P i. ~(P 0) /\ P i ==> ((LEAST i. P i) = SUC(LEAST i. P(SUC i)))``, 2118 RW_TAC list_ss [] 2119 THEN IMP_RES_TAC IS_LEAST_SUC 2120 THEN POP_ASSUM(K ALL_TAC) THEN POP_ASSUM(K ALL_TAC) 2121 THEN FULL_SIMP_TAC list_ss [IS_LEAST_EQ] 2122 THEN Cases_on `i = 0` 2123 THEN RW_TAC std_ss [] 2124 THEN RES_TAC 2125 THEN `?j. i = SUC j` by Cooper.COOPER_TAC 2126 THEN RW_TAC list_ss [] 2127 THEN `(P o SUC) j` by RW_TAC std_ss [] 2128 THEN CONV_TAC(RHS_CONV(REWRITE_CONV[GSYM(SIMP_CONV std_ss [] ``(P o SUC) j:bool``)])) 2129 THEN CONV_TAC(DEPTH_CONV ETA_CONV) 2130 THEN `!n. (SUC n = $LEAST P) = (n = $LEAST (P o SUC))` by PROVE_TAC[] 2131 THEN PROVE_TAC[]); 2132 2133val LENGTH_PATH_FILTER_NON_ZERO_EXISTS = 2134 store_thm 2135 ("LENGTH_PATH_FILTER_NON_ZERO_EXISTS", 2136 ``!v. LENGTH(PATH_FILTER P v) > 0 ==> ?n. n < LENGTH v /\ P(ELEM v n)``, 2137 GEN_TAC 2138 THEN Cases_on `v` 2139 THEN RW_TAC list_ss 2140 [PATH_FILTER_def,LENGTH_def,GT,ELEM_FINITE, 2141 LENGTH_FILTER_NON_ZERO_EXISTS,LS] 2142 THENL 2143 [POP_ASSUM(STRIP_ASSUME_TAC o 2144 SIMP_RULE list_ss [FUN_FILTER_COUNT_def] o 2145 Q.SPEC `0`) 2146 THEN Q.EXISTS_TAC `n` 2147 THEN RW_TAC list_ss [ELEM_INFINITE], 2148 RW_TAC std_ss [ELEM_INFINITE] 2149 THEN FULL_SIMP_TAC list_ss [] 2150 THEN `!n. m <= n ==> ~P (f n)` by PROVE_TAC[] 2151 THEN Cases_on `(LEAST i. !j. i <= j ==> ~P (f j)) = 0` 2152 THENL 2153 [ASSUM_LIST 2154 (fn thl => STRIP_ASSUME_TAC(SIMP_RULE list_ss [el 1 thl,GENLIST] (el 3 thl))), 2155 Cases_on `!j. 0 <= j ==> ~P (f j)` 2156 THENL 2157 [POP_ASSUM 2158 (STRIP_ASSUME_TAC o 2159 ONCE_REWRITE_RULE 2160 [SIMP_RULE std_ss [] 2161 (GSYM(ISPEC ``\i:num. !j. i <= j ==> ~(P:'a->bool) ((f:num->'a) j)`` LEAST0))] o 2162 REWRITE_RULE[ZERO_LESS_EQ]), 2163 FULL_SIMP_TAC std_ss [] 2164 THEN PROVE_TAC[]]]]); 2165 2166val LE_LS_TRANS_X = 2167 store_thm 2168 ("LE_LS_TRANS_X", 2169 ``m:num <= n ==> n:num < p:xnum ==> m < p``, 2170 Cases_on `p` 2171 THEN RW_TAC arith_ss [LS,LE]); 2172 2173val LEAST_TAKE_FIRST = 2174 store_thm 2175 ("LEAST_TAKE_FIRST", 2176 ``!l. (?n. n < LENGTH l /\ P(EL n l)) 2177 ==> 2178 (EL (LEAST n. P(EL n l)) l = LAST(TAKE_FIRST P l))``, 2179 Induct 2180 THEN RW_TAC list_ss [TAKE_FIRST_def,FILTER_APPEND] 2181 THEN Induct_on `n` 2182 THEN RW_TAC list_ss [] 2183 THEN FULL_SIMP_TAC list_ss [] 2184 THEN RES_TAC 2185 THEN RW_TAC list_ss [] 2186 THENL 2187 [`(\n. P(EL n (h::l))) 0` by RW_TAC list_ss [] 2188 THEN IMP_RES_TAC(GSYM LEAST0) 2189 THEN FULL_SIMP_TAC list_ss [], 2190 `(\n. P(EL n (h::l))) 0` by RW_TAC list_ss [] 2191 THEN IMP_RES_TAC(GSYM LEAST0) 2192 THEN FULL_SIMP_TAC list_ss [], 2193 Cases_on `TAKE_FIRST P l = []` 2194 THEN IMP_RES_TAC TAKE_FIRST_NIL 2195 THEN RW_TAC list_ss [] 2196 THEN FULL_SIMP_TAC list_ss [] 2197 THEN RW_TAC list_ss [LAST_DEF] 2198 THEN IMP_RES_TAC 2199 (SIMP_RULE list_ss [] 2200 (ISPECL 2201 [``\n. (P :'a -> bool) (EL n ((h :'a)::(l :'a list)))``,``SUC n``] 2202 LEAST_SUC)) 2203 THEN RW_TAC list_ss []]); 2204 2205val HD_FILTER_LEAST = 2206 store_thm 2207 ("HD_FILTER_LEAST", 2208 ``!P l. (?n. n < LENGTH l /\ P(EL n l)) 2209 ==> 2210 (HD (FILTER P l) = EL (LEAST n. P (EL n l)) l)``, 2211 RW_TAC std_ss [] 2212 THEN IMP_RES_TAC HD_TAKE_FIRST 2213 THEN IMP_RES_TAC LEAST_TAKE_FIRST 2214 THEN RW_TAC list_ss []); 2215 2216val HD_FILTER_LEAST = 2217 store_thm 2218 ("HD_FILTER_LEAST", 2219 ``!P l n. n < LENGTH l /\ P(EL n l) 2220 ==> 2221 (HD (FILTER P l) = EL (LEAST n. P (EL n l)) l)``, 2222 RW_TAC std_ss [] 2223 THEN IMP_RES_TAC HD_TAKE_FIRST 2224 THEN IMP_RES_TAC LEAST_TAKE_FIRST 2225 THEN RW_TAC list_ss []); 2226 2227val IS_LEAST_MIN = 2228 store_thm 2229 ("IS_LEAST_MIN", 2230 ``!P. IS_LEAST P = IS_LEAST (\n. P n /\ !m. m < n ==> ~(P m))``, 2231 CONV_TAC(DEPTH_CONV FUN_EQ_CONV) 2232 THEN RW_TAC list_ss [IS_LEAST_def] 2233 THEN EQ_TAC 2234 THEN RW_TAC list_ss []); 2235 2236val LEAST_MIN = 2237 store_thm 2238 ("LEAST_MIN", 2239 ``!P n. P n ==> ((LEAST n. P n) = LEAST n. P n /\ !m. m < n ==> ~(P m))``, 2240 RW_TAC list_ss [] 2241 THEN IMP_RES_TAC LEAST_EXISTS_IMP 2242 THEN IMP_RES_TAC IS_LEAST_LEAST 2243 THEN `?n. P n /\ !m. m < n ==> ~(P m)` by PROVE_TAC[] 2244 THEN ASSUM_LIST(fn thl => ASSUME_TAC(ONCE_REWRITE_RULE[IS_LEAST_MIN](el 3 thl))) 2245 THEN IMP_RES_TAC 2246 (SIMP_RULE list_ss [] 2247 (ISPEC ``\(n :num). (P :num -> bool) n /\ !(m :num). m < n ==> ~P m`` 2248 IS_LEAST_LEAST)) 2249 THEN IMP_RES_TAC IS_LEAST_UNIQUE); 2250 2251val HD_APPEND = 2252 store_thm 2253 ("HD_APPEND", 2254 ``!l1 l2. ~(l1 = []) ==> (HD(l1 <> l2) = HD l1)``, 2255 Induct 2256 THEN RW_TAC list_ss [GENLIST]); 2257 2258val HD_GENLIST_APPEND = 2259 store_thm 2260 ("HD_GENLIST_APPEND", 2261 ``!n l. 0 < n ==> (HD(GENLIST f n <> l) = HD(GENLIST f n))``, 2262 RW_TAC list_ss [] 2263 THEN Cases_on `GENLIST f n` 2264 THEN RW_TAC list_ss [] 2265 THEN POP_ASSUM(ASSUME_TAC o AP_TERM ``LENGTH:'a list->num``) 2266 THEN FULL_SIMP_TAC list_ss [LENGTH_GENLIST]); 2267 2268val TL_APPEND = 2269 store_thm 2270 ("TL_APPEND", 2271 ``!l1 l2. ~(l1 = []) ==> (TL(l1 <> l2) = TL l1 <> l2)``, 2272 Induct 2273 THEN RW_TAC list_ss [GENLIST]); 2274 2275val EL_GENLIST = 2276 store_thm 2277 ("EL_GENLIST", 2278 ``!f m n. m < n ==> (EL m (GENLIST f n) = f m)``, 2279 GEN_TAC 2280 THEN Induct 2281 THEN Induct 2282 THEN RW_TAC list_ss [GENLIST,SNOC_APPEND] 2283 THENL 2284 [Cases_on `0 < n` 2285 THEN RW_TAC list_ss [] 2286 THEN RES_TAC 2287 THEN FULL_SIMP_TAC list_ss [HD_GENLIST_APPEND] 2288 THEN `n = 0` by DECIDE_TAC 2289 THEN RW_TAC list_ss [GENLIST], 2290 FULL_SIMP_TAC list_ss [] 2291 THEN Cases_on `GENLIST f n` 2292 THEN RW_TAC list_ss [TL_APPEND] 2293 THEN POP_ASSUM(ASSUME_TAC o AP_TERM ``LENGTH:'a list->num``) 2294 THEN FULL_SIMP_TAC list_ss [LENGTH_GENLIST] 2295 THEN Cases_on `m = LENGTH t` 2296 THEN RW_TAC list_ss [EL_APPEND2] 2297 THEN `m < LENGTH t` by DECIDE_TAC 2298 THEN RES_TAC 2299 THEN RW_TAC list_ss [EL_APPEND1]]); 2300 2301val LESS_IS_LEAST_EQ = 2302 store_thm 2303 ("LESS_IS_LEAST_EQ", 2304 ``!P Q n. P n /\ (!m. m <= n ==> (P m = Q m)) 2305 ==> 2306 !n. IS_LEAST P n = IS_LEAST Q n``, 2307 RW_TAC list_ss [IS_LEAST_def] 2308 THEN EQ_TAC 2309 THEN RW_TAC list_ss [] 2310 THEN RES_TAC 2311 THENL 2312 [Cases_on `n' <= n` 2313 THEN RES_TAC 2314 THEN RW_TAC list_ss [] 2315 THEN `n < n'` by DECIDE_TAC 2316 THEN RES_TAC, 2317 Cases_on `m <= n` 2318 THEN RES_TAC 2319 THEN ZAP_TAC list_ss [] 2320 THEN `n < n'` by DECIDE_TAC 2321 THEN RES_TAC, 2322 Cases_on `n' <= n` 2323 THEN RES_TAC 2324 THEN RW_TAC list_ss [] 2325 THEN `n < n'` by DECIDE_TAC 2326 THEN `n <= n` by DECIDE_TAC 2327 THEN RES_TAC, 2328 Cases_on `m <= n` 2329 THEN RES_TAC 2330 THEN ZAP_TAC list_ss [] 2331 THEN `n < n'` by DECIDE_TAC 2332 THEN `n <= n` by DECIDE_TAC 2333 THEN RES_TAC]); 2334 2335val LESS_LEAST_EQ = 2336 store_thm 2337 ("LESS_LEAST_EQ", 2338 ``!P Q n. P n /\ (!m. m <= n ==> (P m = Q m)) 2339 ==> 2340 ((LEAST n. P n) = (LEAST n. Q n))``, 2341 RW_TAC std_ss [] 2342 THEN IMP_RES_TAC LESS_IS_LEAST_EQ 2343 THEN IMP_RES_TAC IS_LEAST_LEAST 2344 THEN RES_TAC 2345 THEN IMP_RES_TAC IS_LEAST_EQ_IMP 2346 THEN CONV_TAC(DEPTH_CONV ETA_CONV) 2347 THEN PROVE_TAC[]); 2348 2349val PATH_FILTER_LEAST = 2350 store_thm 2351 ("PATH_FILTER_LEAST", 2352 ``!P v. 2353 (?n. n < LENGTH v /\ P(ELEM v n)) 2354 ==> 2355 (ELEM (PATH_FILTER P v) 0 = ELEM v LEAST n. P (ELEM v n))``, 2356 Cases_on `v` 2357 THEN RW_TAC std_ss [PATH_FILTER_def] 2358 THEN FULL_SIMP_TAC (list_ss++resq_SS) [ELEM_FINITE,ELEM_INFINITE,FUN_FILTER_COUNT_def,LS,HD] 2359 THENL 2360 [IMP_RES_TAC HD_FILTER_LEAST, 2361 IMP_RES_TAC(SIMP_RULE list_ss [] (ISPEC ``(P:'a->bool) o (f:num->'a)`` LEAST_MIN)) 2362 THEN RW_TAC std_ss [], 2363 `!n. m <= n ==> ~(P(f n))` by PROVE_TAC[] 2364 THEN Cases_on `n < LEAST i. !j. i <= j ==> ~P (f j)` 2365 THENL 2366 [ASSUM_LIST 2367 (fn thl => 2368 ASSUME_TAC 2369 (SIMP_RULE list_ss [el 1 thl,EL_GENLIST] 2370 (SIMP_RULE 2371 list_ss [LENGTH_GENLIST] 2372 (ISPECL 2373 [``P :'a -> bool``, 2374 ``GENLIST (f :num -> 'a) LEAST (i :num). !(j :num). i <= j ==> ~P (f j)``, 2375 ``n:num``] 2376 HD_FILTER_LEAST)))) 2377 THEN RW_TAC list_ss [] 2378 THEN `(\n. P (EL n (GENLIST f LEAST i. !j. i <= j ==> ~P (f j)))) n` 2379 by RW_TAC list_ss [EL_GENLIST] 2380 THEN IMP_RES_TAC FULL_LEAST_INTRO 2381 THEN `(LEAST n. P (EL n (GENLIST f LEAST i. !j. i <= j ==> ~P (f j)))) 2382 < LEAST i. !j. i <= j ==> ~P (f j)` by DECIDE_TAC 2383 THEN RW_TAC list_ss [EL_GENLIST] 2384 THEN `!m. m <= n 2385 ==> 2386 ((\n. P (EL n (GENLIST f LEAST i. !j. i <= j ==> ~P (f j)))) m = 2387 (\n. P(f n)) m)` 2388 by RW_TAC list_ss [EL_GENLIST] 2389 THEN POP_ASSUM(ASSUME_TAC o GSYM) 2390 THEN `(\n. P (f n)) n` by RW_TAC std_ss [] 2391 THEN IMP_RES_TAC LESS_LEAST_EQ 2392 THEN FULL_SIMP_TAC std_ss [], 2393 `(LEAST i. !j. i <= j ==> ~P (f j)) <= n` by DECIDE_TAC 2394 THEN `(\i. !j. i <= j ==> ~P (f j)) m` by PROVE_TAC[] 2395 THEN IMP_RES_TAC 2396 (ISPEC 2397 ``(\(i :num). !(j :num). i <= j ==> ~(P :'a -> bool) ((f :num -> 'a) j))`` 2398 LEAST_INTRO) 2399 THEN FULL_SIMP_TAC std_ss []]]); 2400 2401val PATH_FILTER_LEAST_COR = 2402 store_thm 2403 ("PATH_FILTER_LEAST_COR", 2404 ``!P1 P2 v. 2405 LENGTH(PATH_FILTER P1 v) > 0 2406 ==> 2407 P2 (ELEM (PATH_FILTER P1 v) 0) 2408 ==> 2409 ?n. n < LENGTH v /\ P1(ELEM v n) /\ (!m. m < n ==> ~P1(ELEM v m)) /\ P2(ELEM v n)``, 2410 RW_TAC std_ss [] 2411 THEN IMP_RES_TAC LENGTH_PATH_FILTER_NON_ZERO_EXISTS 2412 THEN IMP_RES_TAC 2413 (SIMP_RULE std_ss [] 2414 (ISPECL[``\n:num. (P1:'a -> bool) (ELEM v n)``, ``n:num``] 2415 (GEN_ALL FULL_LEAST_INTRO))) 2416 THEN Q.EXISTS_TAC `LEAST n. P1 (ELEM v n)` 2417 THEN RW_TAC std_ss [] 2418 THEN IMP_RES_TAC LESS_LEAST 2419 THEN FULL_SIMP_TAC std_ss [] 2420 THENL 2421 [IMP_RES_TAC FULL_LEAST_INTRO 2422 THEN IMP_RES_TAC LE_LS_TRANS_X, 2423 IMP_RES_TAC(GSYM PATH_FILTER_LEAST) 2424 THEN RW_TAC std_ss []]); 2425 2426val PATH_TOP_FREE_ELEM = 2427 store_thm 2428 ("PATH_TOP_FREE_ELEM", 2429 ``!v. PATH_TOP_FREE v = !i. i < LENGTH v ==> ~(ELEM v i = TOP)``, 2430 GEN_TAC 2431 THEN Cases_on `v` 2432 THEN RW_TAC list_ss 2433 [PATH_TOP_FREE_def,TOP_FREE_EL,ELEM_EL, 2434 ELEM_FINITE,ELEM_INFINITE,LENGTH_def,LS]); 2435 2436val PATH_BOTTOM_FREE_ELEM = 2437 store_thm 2438 ("PATH_BOTTOM_FREE_ELEM", 2439 ``!v. PATH_BOTTOM_FREE v = !i. i < LENGTH v ==> ~(ELEM v i = BOTTOM)``, 2440 GEN_TAC 2441 THEN Cases_on `v` 2442 THEN RW_TAC list_ss 2443 [PATH_BOTTOM_FREE_def,BOTTOM_FREE_EL,ELEM_EL, 2444 ELEM_FINITE,ELEM_INFINITE,LENGTH_def,LS]); 2445 2446val LENGTH_PATH_FILTER_NON_ZERO = 2447 store_thm 2448 ("LENGTH_PATH_FILTER_NON_ZERO", 2449 ``!P n v. n < LENGTH v /\ P(ELEM v n) ==> LENGTH (PATH_FILTER P v) > 0``, 2450 RW_TAC list_ss [] 2451 THEN Cases_on `v` 2452 THEN FULL_SIMP_TAC list_ss 2453 [PATH_FILTER_def,LENGTH_def,GT,ELEM_def,LS, 2454 RESTN_FINITE,RESTN_INFINITE,HEAD_def,HD_RESTN] 2455 THEN IMP_RES_TAC NON_ZERO_EXISTS_LENGTH_FILTER 2456 THEN Cases_on `!m. ?n. m <= n /\ P (f n)` 2457 THEN RW_TAC list_ss [GT,LENGTH_def] 2458 THEN FULL_SIMP_TAC list_ss [] 2459 THENL 2460 [ASSUM_LIST(fn thl => STRIP_ASSUME_TAC(SPEC ``XNUM m`` (el 2 thl))) 2461 THEN PROVE_TAC[LE], 2462 Cases_on `(LEAST i. !j. i <= j ==> ~P (f j)) = 0` 2463 THEN RW_TAC list_ss [GENLIST] 2464 THENL 2465 [`(\m. !n. m <= n ==> ~P(f n)) m'` by PROVE_TAC[] 2466 THEN IMP_RES_TAC LEAST_INTRO 2467 THEN FULL_SIMP_TAC list_ss [], 2468 Cases_on `n < LEAST i. !j. i <= j ==> ~P (f j)` 2469 THENL 2470 [`n < LENGTH(GENLIST f LEAST i. !j. i <= j ==> ~P (f j))` 2471 by RW_TAC list_ss [LENGTH_GENLIST] 2472 THEN `P(EL n (GENLIST f LEAST i. !j. i <= j ==> ~P (f j)))` 2473 by RW_TAC list_ss [EL_GENLIST] 2474 THEN IMP_RES_TAC NON_ZERO_EXISTS_LENGTH_FILTER, 2475 `(LEAST i. !j. i <= j ==> ~P (f j)) <= n` by DECIDE_TAC 2476 THEN `(\m. !n. m <= n ==> ~P(f n)) m'` by PROVE_TAC[] 2477 THEN IMP_RES_TAC LEAST_INTRO 2478 THEN FULL_SIMP_TAC list_ss []]]]); 2479 2480(* 2481val ELEM_LEAST = 2482 store_thm 2483 ("ELEM_LEAST", 2484 ``!P v j. j < LENGTH v /\ P(ELEM v j) ==> P(ELEM v LEAST n. P(ELEM v n))``, 2485 REPEAT GEN_TAC 2486 THEN Cases_on `v` 2487 THEN RW_TAC list_ss [ELEM_FINITE,ELEM_INFINITE,LENGTH_def,LS] 2488 THENL 2489 [`(\n. P(EL n l)) j` by PROVE_TAC[] 2490 THEN IMP_RES_TAC FULL_LEAST_INTRO 2491 THEN FULL_SIMP_TAC list_ss [], 2492 `(\n. P(f n)) j` by PROVE_TAC[] 2493 THEN IMP_RES_TAC FULL_LEAST_INTRO 2494 THEN FULL_SIMP_TAC list_ss []]); 2495*) 2496 2497val ELEM_LEAST = 2498 store_thm 2499 ("ELEM_LEAST", 2500 ``!P1 P2 v j. 2501 j < LENGTH v /\ P1(ELEM v j) /\ P2(ELEM v j) /\ (!i. i < j ==> ~(P2(ELEM v i))) 2502 ==> P1(ELEM v LEAST n. P2(ELEM v n))``, 2503 REPEAT GEN_TAC 2504 THEN Cases_on `v` 2505 THEN RW_TAC list_ss [ELEM_FINITE,ELEM_INFINITE,LENGTH_def,LS] 2506 THENL 2507 [`(\n. P2(EL n l)) j` by PROVE_TAC[] 2508 THEN IMP_RES_TAC FULL_LEAST_INTRO 2509 THEN FULL_SIMP_TAC list_ss [] 2510 THEN Cases_on `j = LEAST n. P2 (EL n l)` 2511 THEN RW_TAC list_ss [] 2512 THEN `(LEAST n. P2 (EL n l)) < j` by DECIDE_TAC 2513 THEN RES_TAC, 2514 `(\n. P2(f n)) j` by PROVE_TAC[] 2515 THEN IMP_RES_TAC FULL_LEAST_INTRO 2516 THEN FULL_SIMP_TAC list_ss [] 2517 THEN Cases_on `j = LEAST n. P2 (f n)` 2518 THEN RW_TAC list_ss [] 2519 THEN `(LEAST n. P2 (f n)) < j` by DECIDE_TAC 2520 THEN RES_TAC]); 2521 2522val CLOCK_NOT_LEMMA = 2523 store_thm 2524 ("CLOCK_NOT_LEMMA", 2525 ``PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v 2526 ==> 2527 !i. i < LENGTH v ==> (CLOCK (B_NOT c) (ELEM v i) = ~(CLOCK c (ELEM v i)))``, 2528 RW_TAC list_ss [] 2529 THEN Cases_on `(ELEM v i)` 2530 THEN RW_TAC list_ss [CLOCK_def,B_SEM_def] 2531 THEN IMP_RES_TAC PATH_TOP_FREE_ELEM 2532 THEN IMP_RES_TAC PATH_BOTTOM_FREE_ELEM); 2533 2534val CLOCK_NOT_LEMMA_COR = 2535 prove 2536 (``!j:num. 2537 PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v /\ j < LENGTH v 2538 ==> 2539 ((!i:num. i < j ==> ~(CLOCK c (ELEM v i))) 2540 = 2541 (!i:num. i < j ==> CLOCK (B_NOT c) (ELEM v i))) ``, 2542 RW_TAC list_ss [] 2543 THEN EQ_TAC 2544 THEN RW_TAC list_ss [] 2545 THEN RES_TAC 2546 THEN IMP_RES_TAC LS_TRANS_X 2547 THEN PROVE_TAC[CLOCK_NOT_LEMMA]); 2548 2549val F_PROJ_F_STRONG_BOOL = 2550 store_thm 2551 ("F_PROJ_F_STRONG_BOOL", 2552 ``!b. F_CLOCK_FREE (F_STRONG_BOOL b) ==> 2553 !v. PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2554 !c. UF_SEM (PROJ v c) (F_STRONG_BOOL b) = 2555 F_SEM v c (F_STRONG_BOOL b)``, 2556 RW_TAC (list_ss++resq_SS) [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def] 2557 THEN EQ_TAC 2558 THEN RW_TAC std_ss [] 2559 THENL 2560 [IMP_RES_TAC 2561 (ISPECL[``CLOCK(c :'a bexp)``,``CLOCK(b :'a bexp)``]PATH_FILTER_LEAST_COR) 2562 THEN Q.EXISTS_TAC `n` 2563 THEN RW_TAC (list_ss++resq_SS) [CLOCK_TICK_def,LENGTH_SEL] 2564 THEN RES_TAC 2565 THEN FULL_SIMP_TAC list_ss [CLOCK_def,ELEM_EL,EL_SEL0,B_SEM_def] 2566 THEN Cases_on `(ELEM v i)` 2567 THEN RW_TAC std_ss [B_SEM_def] 2568 THEN IMP_RES_TAC LS_TRANS_X 2569 THEN IMP_RES_TAC PATH_BOTTOM_FREE_ELEM, 2570 FULL_SIMP_TAC (list_ss++resq_SS) [CLOCK_TICK_def,LENGTH_SEL,ELEM_EL,EL_SEL0] 2571 THEN FULL_SIMP_TAC list_ss [GSYM CLOCK_def] 2572 THEN IMP_RES_TAC LENGTH_PATH_FILTER_NON_ZERO, 2573 FULL_SIMP_TAC (list_ss++resq_SS) [CLOCK_TICK_def,LENGTH_SEL,ELEM_EL,EL_SEL0] 2574 THEN FULL_SIMP_TAC list_ss [GSYM CLOCK_def] 2575 THEN IMP_RES_TAC PATH_FILTER_LEAST 2576 THEN RW_TAC std_ss [] 2577 THEN IMP_RES_TAC CLOCK_NOT_LEMMA_COR 2578 THEN IMP_RES_TAC(ISPECL[``CLOCK (b :'a bexp)``,``CLOCK (c :'a bexp)``]ELEM_LEAST)]); 2579 2580val NEUTRAL_COMPLEMENT = 2581 store_thm 2582 ("NEUTRAL_COMPLEMENT", 2583 ``!v. PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> (COMPLEMENT v = v)``, 2584 GEN_TAC 2585 THEN Cases_on `v` 2586 THEN RW_TAC list_ss [PATH_TOP_FREE_def,PATH_BOTTOM_FREE_def,COMPLEMENT_def] 2587 THENL 2588 [Induct_on `l` 2589 THEN RW_TAC list_ss [] 2590 THEN Cases_on `h` 2591 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def,BOTTOM_FREE_def,COMPLEMENT_LETTER_def], 2592 CONV_TAC FUN_EQ_CONV 2593 THEN Induct 2594 THEN RW_TAC list_ss [] 2595 THENL 2596 [Cases_on `f 0` 2597 THEN FULL_SIMP_TAC list_ss [COMPLEMENT_LETTER_def] 2598 THEN RES_TAC, 2599 Cases_on `f(SUC n)` 2600 THEN FULL_SIMP_TAC list_ss [COMPLEMENT_LETTER_def] 2601 THEN RES_TAC]]); 2602 2603val NOT_XNUM_0 = 2604 store_thm 2605 ("NOT_XNUM_0", 2606 ``!v. ~(v = XNUM 0) = v > 0``, 2607 GEN_TAC 2608 THEN Cases_on `v` 2609 THEN RW_TAC list_ss [xnum_11,GT]); 2610 2611val F_PROJ_F_WEAK_BOOL = 2612 store_thm 2613 ("F_PROJ_F_WEAK_BOOL", 2614 ``!b. F_CLOCK_FREE (F_WEAK_BOOL b) ==> 2615 !v. PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2616 !c. UF_SEM (PROJ v c) (F_WEAK_BOOL b) = 2617 F_SEM v c (F_WEAK_BOOL b)``, 2618 RW_TAC (list_ss++resq_SS) [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def] 2619 THEN EQ_TAC 2620 THEN RW_TAC std_ss [] 2621 THENL 2622 [Cases_on `PATH_FILTER (CLOCK c) v` 2623 THEN FULL_SIMP_TAC (list_ss++resq_SS) 2624 [LENGTH_def,xnum_11,xnum_distinct,LENGTH_NIL,CLOCK_TICK_def,LENGTH_SEL, 2625 ELEM_EL,EL_SEL0] 2626 THEN RW_TAC list_ss [] 2627 THEN FULL_SIMP_TAC std_ss [GSYM CLOCK_def,ELEM_COMPLEMENT] 2628 THEN POP_ASSUM(ASSUME_TAC o Q.AP_TERM `LENGTH`) 2629 THEN FULL_SIMP_TAC list_ss [LENGTH_def] 2630 THEN Cases_on `LENGTH (PATH_FILTER (CLOCK c) v) > 0` 2631 THENL 2632 [`XNUM 0 > 0` by PROVE_TAC[] 2633 THEN FULL_SIMP_TAC list_ss [GT], 2634 `~(?n. n < LENGTH v /\ CLOCK c (ELEM v n))` by PROVE_TAC[LENGTH_PATH_FILTER_NON_ZERO] 2635 THEN FULL_SIMP_TAC list_ss [] 2636 THEN `!n. n < LENGTH v ==> ~CLOCK c (ELEM v n)` by PROVE_TAC[] 2637 THEN RES_TAC 2638 THEN Cases_on `(ELEM v j)` 2639 THEN IMP_RES_TAC PATH_TOP_FREE_ELEM 2640 THEN IMP_RES_TAC PATH_BOTTOM_FREE_ELEM 2641 THEN IMP_RES_TAC ELEM_COMPLEMENT 2642 THEN PROVE_TAC[COMPLEMENT_LETTER_def]], 2643 IMP_RES_TAC NEUTRAL_COMPLEMENT 2644 THEN POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [th]) 2645 THEN FULL_SIMP_TAC (list_ss++resq_SS) 2646 [GSYM CLOCK_def,CLOCK_TICK_def,LENGTH_SEL,ELEM_EL,EL_SEL0] 2647 THEN IMP_RES_TAC PATH_FILTER_LEAST 2648 THEN `CLOCK b (ELEM v LEAST n. CLOCK c (ELEM v n))` by PROVE_TAC[] 2649 THEN IMP_RES_TAC CLOCK_NOT_LEMMA_COR 2650 THEN `IS_LEAST (\j. CLOCK c (ELEM v j)) j` 2651 by RW_TAC list_ss 2652 [SIMP_RULE list_ss [] 2653 (ISPECL[``(\j. CLOCK c (ELEM v j))``,``j:num``]IS_LEAST_def)] 2654 THEN IMP_RES_TAC IS_LEAST_EQ_IMP 2655 THEN RW_TAC list_ss [], 2656 Cases_on `LENGTH (PATH_FILTER (CLOCK c) v) = XNUM 0` 2657 THEN RW_TAC list_ss [] 2658 THEN FULL_SIMP_TAC list_ss [NOT_XNUM_0] 2659 THEN IMP_RES_TAC LENGTH_PATH_FILTER_NON_ZERO_EXISTS 2660 THEN IMP_RES_TAC PATH_FILTER_LEAST 2661 THEN RW_TAC list_ss [] 2662 THEN IMP_RES_TAC NEUTRAL_COMPLEMENT 2663 THEN POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [th]) 2664 THEN IMP_RES_TAC 2665 (SIMP_RULE list_ss [] 2666 (ISPEC ``(\n. CLOCK c (ELEM v n))``(GEN_ALL FULL_LEAST_INTRO))) 2667 THEN IMP_RES_TAC LE_LS_TRANS_X 2668 THEN FULL_SIMP_TAC (list_ss++resq_SS) 2669 [GSYM CLOCK_def,CLOCK_TICK_def,LENGTH_SEL,ELEM_EL,EL_SEL0] 2670 THEN ASSUM_LIST 2671 (fn thl => 2672 ASSUME_TAC 2673 (SIMP_RULE list_ss [el 1 thl,el 3 thl] 2674 (Q.SPEC `LEAST n. CLOCK c (ELEM v n)` (el 8 thl)))) 2675 THEN `(!i. i < (LEAST n. CLOCK c (ELEM v n)) ==> CLOCK (B_NOT c) (ELEM v i)) 2676 = 2677 (!i. i < (LEAST n. CLOCK c (ELEM v n)) ==> ~(CLOCK c (ELEM v i)))` 2678 by PROVE_TAC[CLOCK_NOT_LEMMA_COR] 2679 THEN POP_ASSUM(fn th => FULL_SIMP_TAC list_ss [th]) 2680 THEN FULL_SIMP_TAC list_ss 2681 [SIMP_RULE std_ss [] (ISPEC ``\n. CLOCK c (ELEM v n)`` LESS_LEAST)]]); 2682 2683val COMPLEMENT_LETTER_FILTER = 2684 store_thm 2685 ("COMPLEMENT_LETTER_FILTER", 2686 ``!f. (COMPLEMENT_LETTER o f = f) 2687 ==> 2688 !n. MAP COMPLEMENT_LETTER (FILTER P (GENLIST f n)) = FILTER P (GENLIST f n)``, 2689 RW_TAC list_ss [] 2690 THEN Induct_on `n` 2691 THEN RW_TAC list_ss [GENLIST,FILTER,SNOC_APPEND,FILTER_APPEND] 2692 THEN ASSUM_LIST(fn thl => ASSUME_TAC(CONV_RULE FUN_EQ_CONV (el 3 thl))) 2693 THEN FULL_SIMP_TAC list_ss []); 2694 2695val COMPLEMENT_PATH_FILTER = 2696 store_thm 2697 ("COMPLEMENT_PATH_FILTER", 2698 ``!v. (COMPLEMENT v = v) 2699 ==> 2700 (COMPLEMENT(PATH_FILTER P v) = PATH_FILTER P v)``, 2701 GEN_TAC 2702 THEN Cases_on `v` 2703 THEN RW_TAC list_ss 2704 [PATH_TOP_FREE_def,PATH_BOTTOM_FREE_def,COMPLEMENT_def,PATH_FILTER_def] 2705 THENL 2706 [Induct_on `l` 2707 THEN RW_TAC list_ss [PATH_FILTER_def,COMPLEMENT_def] 2708 THEN Cases_on `h` 2709 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def,BOTTOM_FREE_def,COMPLEMENT_LETTER_def], 2710 ASM_REWRITE_TAC [GSYM(SIMP_CONV std_ss [] ``(f o g) o h``)], 2711 IMP_RES_TAC COMPLEMENT_LETTER_FILTER 2712 THEN RW_TAC list_ss []]); 2713 2714val F_PROJ_F_NOT_BOOL = 2715 store_thm 2716 ("F_PROJ_F_NOT_BOOL", 2717 ``(F_CLOCK_FREE f ==> 2718 !v. PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2719 !c. UF_SEM (PROJ v c) f = F_SEM v c f) 2720 ==> 2721 F_CLOCK_FREE (F_NOT f) ==> 2722 !v. PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2723 !c. UF_SEM (PROJ v c) (F_NOT f) = F_SEM v c (F_NOT f)``, 2724 RW_TAC (list_ss++resq_SS) [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def] 2725 THEN RES_TAC 2726 THEN IMP_RES_TAC NEUTRAL_COMPLEMENT 2727 THEN RW_TAC std_ss [COMPLEMENT_PATH_FILTER]); 2728 2729val F_PROJ_F_NOT_BOOL_FINITE = 2730 store_thm 2731 ("F_PROJ_F_NOT_BOOL_FINITE", 2732 ``(F_CLOCK_FREE f ==> 2733 !l. 2734 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 2735 !c. UF_SEM (PROJ (FINITE l) c) f = F_SEM (FINITE l) c f) ==> 2736 F_CLOCK_FREE (F_NOT f) ==> 2737 !l. 2738 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 2739 !c. 2740 UF_SEM (PROJ (FINITE l) c) (F_NOT f) = 2741 F_SEM (FINITE l) c (F_NOT f)``, 2742 RW_TAC (list_ss++resq_SS) [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def] 2743 THEN RES_TAC 2744 THEN IMP_RES_TAC NEUTRAL_COMPLEMENT 2745 THEN RW_TAC std_ss [COMPLEMENT_PATH_FILTER]); 2746 2747val F_PROJ_F_AND_BOOL = 2748 store_thm 2749 ("F_PROJ_F_AND_BOOL", 2750 ``(F_CLOCK_FREE f ==> 2751 !v. 2752 PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2753 !c. UF_SEM (PROJ v c) f = F_SEM v c f) 2754 /\ 2755 (F_CLOCK_FREE f' ==> 2756 !v. 2757 PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2758 !c. UF_SEM (PROJ v c) f' = F_SEM v c f') 2759 ==> 2760 F_CLOCK_FREE (F_AND (f,f')) ==> 2761 !v. 2762 PATH_TOP_FREE v /\ PATH_BOTTOM_FREE v ==> 2763 !c. UF_SEM (PROJ v c) (F_AND (f,f')) = F_SEM v c (F_AND (f,f'))``, 2764 RW_TAC (list_ss++resq_SS) [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def]); 2765 2766val F_PROJ_F_AND_BOOL_FINITE = 2767 store_thm 2768 ("F_PROJ_F_AND_BOOL_FINITE", 2769 ``(F_CLOCK_FREE f ==> 2770 !l. 2771 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 2772 !c. UF_SEM (PROJ (FINITE l) c) f = F_SEM (FINITE l) c f) /\ 2773 (F_CLOCK_FREE f' ==> 2774 !l. 2775 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 2776 !c. UF_SEM (PROJ (FINITE l) c) f' = F_SEM (FINITE l) c f') ==> 2777 F_CLOCK_FREE (F_AND (f,f')) ==> 2778 !l. 2779 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 2780 !c. 2781 UF_SEM (PROJ (FINITE l) c) (F_AND (f,f')) = 2782 F_SEM (FINITE l) c (F_AND (f,f'))``, 2783 RW_TAC (list_ss++resq_SS) [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def]); 2784 2785val PATH_TOP_FREE_SEL = 2786 store_thm 2787 ("PATH_TOP_FREE_SEL", 2788 ``!v. PATH_TOP_FREE v ==> !j. j < LENGTH v ==> TOP_FREE (SEL v (0,j))``, 2789 Induct 2790 THEN RW_TAC list_ss 2791 [PATH_TOP_FREE_def,TOP_FREE_EL,LENGTH_SEL,LENGTH_def,LS,EL_SEL0, 2792 ELEM_FINITE,ELEM_INFINITE]); 2793 2794val PATH_BOTTOM_FREE_SEL = 2795 store_thm 2796 ("PATH_BOTTOM_FREE_SEL", 2797 ``!v. PATH_BOTTOM_FREE v ==> !j. j < LENGTH v ==> BOTTOM_FREE (SEL v (0,j))``, 2798 Induct 2799 THEN RW_TAC list_ss 2800 [PATH_BOTTOM_FREE_def,BOTTOM_FREE_EL,LENGTH_SEL,LENGTH_def,LS,EL_SEL0, 2801 ELEM_FINITE,ELEM_INFINITE]); 2802 2803val LENGTH_FILTER = 2804 store_thm 2805 ("LENGTH_FILTER", 2806 ``!l. LENGTH(FILTER P l) <= LENGTH l``, 2807 Induct 2808 THEN RW_TAC list_ss []); 2809 2810val LENGTH_PATH_FILTER = 2811 store_thm 2812 ("LENGTH_PATH_FILTER", 2813 ``!v. LENGTH(PATH_FILTER P v) <= LENGTH v``, 2814 Induct 2815 THEN RW_TAC list_ss [LENGTH_FILTER,PATH_FILTER_def,LENGTH_def,LE]); 2816 2817val LS_LE_TRANS_X = 2818 store_thm 2819 ("LS_LE_TRANS_X", 2820 ``m:num < n:xnum ==> n <= p:xnum ==> m < p``, 2821 Cases_on `n` THEN Cases_on `p` 2822 THEN RW_TAC arith_ss [LS,LE]); 2823 2824val PATH_TAKE_FIRST_def = 2825 Define 2826 `(PATH_TAKE_FIRST P (FINITE l) = TAKE_FIRST P l) 2827 /\ 2828 (PATH_TAKE_FIRST P (INFINITE f) = GENLIST f (SUC(LEAST n. P(f n))))`; 2829 2830val PATH_TAKE_FIRSTN_def = 2831 Define 2832 `(PATH_TAKE_FIRSTN P n (FINITE l) = TAKE_FIRSTN P n l) 2833 /\ 2834 (PATH_TAKE_FIRSTN P 0 (INFINITE f) = []) 2835 /\ 2836 (PATH_TAKE_FIRSTN P (SUC n) (INFINITE f) = 2837 PATH_TAKE_FIRST P (INFINITE f) 2838 <> 2839 PATH_TAKE_FIRSTN P n 2840 (INFINITE(\n. f(n + LENGTH(PATH_TAKE_FIRST P (INFINITE f))))))`; 2841 2842val TAKE_FIRSTN_1 = 2843 store_thm 2844 ("TAKE_FIRSTN_1", 2845 ``!P l. TAKE_FIRSTN P 1 l = TAKE_FIRST P l``, 2846 PROVE_TAC[ONE,TAKE_FIRSTN_def,APPEND_NIL]); 2847 2848val SEL_REC_FINITE = 2849 store_thm 2850 ("SEL_REC_FINITE", 2851 ``!m n l. SEL_REC m n (FINITE l) = SEL_REC m n l``, 2852 Induct THEN Induct THEN Induct 2853 THEN RW_TAC list_ss 2854 [HEAD_def,REST_def,SEL_def,SEL_REC_def, 2855 FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 2856 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def]); 2857 2858val SEL_FINITE = 2859 store_thm 2860 ("SEL_FINITE", 2861 ``!l m n. SEL (FINITE l) (m,n) = SEL l (m,n)``, 2862 RW_TAC list_ss 2863 [SEL_def,FinitePSLPathTheory.SEL_def,SEL_REC_FINITE]); 2864 2865val LENGTH_TAKE_FIRST_NON_EMPTY = 2866 store_thm 2867 ("LENGTH_TAKE_FIRST_NON_EMPTY", 2868 ``!P l. LENGTH l > 0 ==> LENGTH(TAKE_FIRST P l) > 0``, 2869 GEN_TAC 2870 THEN Induct 2871 THEN RW_TAC list_ss [TAKE_FIRST_def]); 2872 2873val FILTER_TAKE_FIRST = 2874 store_thm 2875 ("FILTER_TAKE_FIRST", 2876 ``!l. (?n. n < LENGTH l /\ P (EL n l)) 2877 ==> (FILTER P (TAKE_FIRST P l) = [HD (FILTER P l)])``, 2878 Induct 2879 THEN RW_TAC list_ss [TAKE_FIRST_def,FILTER_APPEND] 2880 THEN Cases_on `n` 2881 THEN RW_TAC list_ss [] 2882 THEN FULL_SIMP_TAC list_ss [] 2883 THEN RES_TAC 2884 THEN RW_TAC list_ss []); 2885 2886val TAKE_FIRSTN_NIL = 2887 store_thm 2888 ("TAKE_FIRSTN_NIL", 2889 ``!P n. TAKE_FIRSTN P n [] = []``, 2890 Induct_on `n` 2891 THEN RW_TAC list_ss [TAKE_FIRSTN_def,TAKE_FIRST_def,BUTFIRSTN]); 2892 2893val LENGTH_TAKE_FIRST_TAKE_FIRSTN = 2894 store_thm 2895 ("LENGTH_TAKE_FIRST_TAKE_FIRSTN", 2896 ``LENGTH (TAKE_FIRST P l) <= LENGTH (TAKE_FIRSTN P (SUC n) l)``, 2897 RW_TAC list_ss [GSYM TAKE_FIRSTN_1,LENGTH_TAKE_FIRST_MONO]); 2898 2899val LENGTH_TAKE_FIRSTN_LEMMA = 2900 prove 2901 (``LENGTH (TAKE_FIRST P l) 2902 + 2903 LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) = 2904 LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l)``, 2905 RW_TAC std_ss [GSYM LENGTH_APPEND,GSYM TAKE_FIRSTN_def]); 2906 2907val SEL_TAKE_FIRST = 2908 store_thm 2909 ("SEL_TAKE_FIRST", 2910 ``LENGTH l > 0 ==> (SEL l (0, LENGTH(TAKE_FIRST P l)-1) = TAKE_FIRST P l)``, 2911 RW_TAC std_ss [] 2912 THEN `LENGTH (TAKE_FIRST P l) > 0` by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY] 2913 THEN CONV_TAC(LHS_CONV(RATOR_CONV(ONCE_REWRITE_CONV[GSYM TAKE_FIRST_APPEND]))) 2914 THEN RW_TAC list_ss [SEL_APPEND1,SEL_RESTN_EQ0]); 2915 2916val SEL_BUTFIRSTN = 2917 store_thm 2918 ("SEL_BUTFIRSTN", 2919 ``!l m n. 2920 LENGTH l > m+n /\ n > 0 2921 ==> 2922 (SEL l (0, m+n) = SEL l (0,m) <> SEL (BUTFIRSTN (SUC m) l) (0,n-1))``, 2923 SIMP_TAC list_ss [FinitePSLPathTheory.SEL_def] 2924 THEN Induct_on `m` 2925 THEN RW_TAC list_ss [FinitePSLPathTheory.SEL_REC_def,ADD_CLAUSES,FinitePSLPathTheory.REST_def] 2926 THEN `BUTFIRSTN (SUC m) l = BUTFIRSTN m (TL l)` 2927 by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS,BUTFIRSTN] 2928 THEN RW_TAC list_ss [] 2929 THENL 2930 [`(HD l::TL l) = l` 2931 by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS] 2932 THEN ONCE_REWRITE_TAC[ONE,GSYM ADD1] 2933 THEN `BUTFIRSTN (SUC 0) l = TL l` by PROVE_TAC[BUTFIRSTN] 2934 THEN ASM_REWRITE_TAC 2935 [FinitePSLPathTheory.SEL_REC_def,FinitePSLPathTheory.HEAD_def, 2936 FinitePSLPathTheory.REST_def,APPEND,TWO,ADD_CLAUSES,CONS_11], 2937 Cases_on `m = 0` 2938 THEN RW_TAC list_ss [BUTFIRSTN] 2939 THEN ONCE_REWRITE_TAC[ONE,GSYM ADD1] 2940 THEN REWRITE_TAC 2941 [FinitePSLPathTheory.SEL_REC_def,FinitePSLPathTheory.HEAD_def, 2942 FinitePSLPathTheory.REST_def,APPEND,TWO,ADD_CLAUSES] 2943 THEN FULL_SIMP_TAC list_ss [] 2944 THENL 2945 [`LENGTH l > SUC(SUC 0)` by DECIDE_TAC 2946 THEN `(HD l::TL l) = l` 2947 by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS] 2948 THEN `0 < LENGTH l` by DECIDE_TAC 2949 THEN `LENGTH (TL l) = LENGTH l - 1` by PROVE_TAC[LENGTH_TL] 2950 THEN `LENGTH (TL l) > 0` by DECIDE_TAC 2951 THEN ONCE_REWRITE_TAC[TWO] 2952 THEN ONCE_REWRITE_TAC[ONE] 2953 THEN `(HD(TL l)::TL(TL l)) = TL l` 2954 by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS] 2955 THEN `BUTFIRSTN (SUC(SUC 0)) l = TL(TL l)` by PROVE_TAC[BUTFIRSTN] 2956 THEN RW_TAC list_ss [], 2957 `0 < LENGTH l` by DECIDE_TAC 2958 THEN `LENGTH (TL l) = LENGTH l - 1` by PROVE_TAC[LENGTH_TL] 2959 THEN `LENGTH (TL l) > m + n` by DECIDE_TAC 2960 THEN RES_TAC 2961 THEN FULL_SIMP_TAC std_ss [DECIDE``m + (n + 1) = SUC(m + n)``,GSYM ADD1] 2962 THEN `LENGTH (TL l) > 0` by DECIDE_TAC 2963 THEN `(HD(TL l)::TL(TL l)) = TL l` 2964 by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS] 2965 THEN FULL_SIMP_TAC std_ss 2966 [FinitePSLPathTheory.SEL_REC_def,FinitePSLPathTheory.HEAD_def, 2967 FinitePSLPathTheory.REST_def] 2968 THEN `HD (TL l)::SEL_REC (m + n) 0 (TL (TL l)) = 2969 (HD (TL l)::SEL_REC m 0 (TL (TL l))) <> 2970 SEL_REC n 0 (BUTFIRSTN m (TL(TL l)))` 2971 by PROVE_TAC[BUTFIRSTN] 2972 THEN FULL_SIMP_TAC std_ss [APPEND,CONS_11] 2973 THEN `(HD l::TL l) = l` 2974 by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``n>(p:num) ==> ~(n=0)``,CONS] 2975 THEN PROVE_TAC[BUTFIRSTN]]]); 2976 2977val SEL_TAKE_FIRSTN = 2978 store_thm 2979 ("SEL_TAKE_FIRSTN", 2980 ``!P n l. 2981 LENGTH l > 0 2982 ==> 2983 (SEL l (0, LENGTH(TAKE_FIRSTN P (SUC n) l)-1) = TAKE_FIRSTN P (SUC n) l)``, 2984 GEN_TAC 2985 THEN Induct 2986 THEN RW_TAC list_ss [REWRITE_RULE[ONE]TAKE_FIRSTN_1,SEL_TAKE_FIRST] 2987 THEN ONCE_REWRITE_TAC[TAKE_FIRSTN_def] 2988 THEN RW_TAC list_ss [] 2989 THEN `LENGTH (TAKE_FIRST P l) > 0` by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY] 2990 THEN Cases_on `BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l = []` 2991 THEN RW_TAC list_ss [TAKE_FIRSTN_NIL,SEL_TAKE_FIRST] 2992 THEN `~(LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)=0)` by PROVE_TAC[LENGTH_NIL] 2993 THEN `LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) > 0` by DECIDE_TAC 2994 THEN `LENGTH(TAKE_FIRST P (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0` 2995 by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY] 2996 THEN `LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0` 2997 by PROVE_TAC 2998 [LENGTH_TAKE_FIRST_TAKE_FIRSTN,DECIDE``m:num > 0 /\ m <= n:num ==> n > 0``] 2999 THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) > 0` 3000 by PROVE_TAC 3001 [LENGTH_TAKE_FIRST_TAKE_FIRSTN,LENGTH_TAKE_FIRST_SUC, 3002 DECIDE``m:num > 0 /\ m <= n:num /\ n <= p:num ==> p > 0``] 3003 THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 3004 THEN `LENGTH l > LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) - 1` by DECIDE_TAC 3005 THEN `LENGTH l > LENGTH (TAKE_FIRST P l) 3006 + 3007 LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1` 3008 by PROVE_TAC[LENGTH_TAKE_FIRSTN_LEMMA] 3009 THEN `LENGTH l > (LENGTH (TAKE_FIRST P l) - 1) 3010 + 3011 LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l))` 3012 by DECIDE_TAC 3013 THEN RW_TAC std_ss [DECIDE ``m > 0 ==> (m + n - 1 = (m - 1) + n)``] 3014 THEN RW_TAC list_ss [SEL_BUTFIRSTN,SEL_TAKE_FIRST] 3015 THEN `SEL (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) 3016 (0,LENGTH (TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1) = 3017 TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)` 3018 by PROVE_TAC[] 3019 THEN `SUC(LENGTH (TAKE_FIRST P l) - 1) = LENGTH(TAKE_FIRST P l)` by DECIDE_TAC 3020 THEN RW_TAC list_ss []); 3021 3022val FIRSTN_SEL = 3023 store_thm 3024 ("FIRSTN_SEL", 3025 ``!n l. n < LENGTH l ==> (FIRSTN (SUC n) l = SEL l (0,n))``, 3026 Induct 3027 THEN RW_TAC list_ss 3028 [FIRSTN,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3029 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def,ADD_CLAUSES] 3030 THEN REWRITE_TAC 3031 [ONE,GSYM ADD1,FIRSTN,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3032 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def,ADD_CLAUSES] 3033 THEN `(HD l::TL l) = l` by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``p:num<n ==> ~(n=0)``,CONS] 3034 THEN ZAP_TAC list_ss [FIRSTN,ONE] 3035 THEN `0 < LENGTH l` by DECIDE_TAC 3036 THEN IMP_RES_TAC LENGTH_TL 3037 THEN `0 < LENGTH(TL l)` by DECIDE_TAC 3038 THEN `(HD(TL l)::TL(TL l)) = TL l` by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``p:num<n ==> ~(n=0)``,CONS] 3039 THEN ASSUM_LIST(fn thl => ONCE_REWRITE_TAC[GSYM(el 5 thl)]) 3040 THEN ASSUM_LIST(fn thl => ONCE_REWRITE_TAC[GSYM(el 1 thl)]) 3041 THEN REWRITE_TAC 3042 [FIRSTN,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3043 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def] 3044 THEN RW_TAC list_ss [] 3045 THEN `n < LENGTH(TL l)` by DECIDE_TAC 3046 THEN FULL_SIMP_TAC list_ss 3047 [FIRSTN,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3048 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def] 3049 THEN `FIRSTN (SUC n) (HD (TL l)::TL (TL l)) = SEL_REC (SUC n) 0 (HD (TL l)::TL (TL l))` 3050 by PROVE_TAC[ADD1] 3051 THEN FULL_SIMP_TAC list_ss 3052 [FIRSTN,ADD1,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3053 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def]); 3054 3055 3056val SEL_TAKE_FIRSTN = 3057 store_thm 3058 ("SEL_TAKE_FIRSTN", 3059 ``!P n l. 3060 LENGTH l > 0 3061 ==> 3062 (SEL l (0, LENGTH(TAKE_FIRSTN P (SUC n) l)-1) = TAKE_FIRSTN P (SUC n) l)``, 3063 GEN_TAC 3064 THEN Induct 3065 THEN RW_TAC list_ss [REWRITE_RULE[ONE]TAKE_FIRSTN_1,SEL_TAKE_FIRST] 3066 THEN ONCE_REWRITE_TAC[TAKE_FIRSTN_def] 3067 THEN RW_TAC list_ss [] 3068 THEN `LENGTH (TAKE_FIRST P l) > 0` by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY] 3069 THEN Cases_on `BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l = []` 3070 THEN RW_TAC list_ss [TAKE_FIRSTN_NIL,SEL_TAKE_FIRST] 3071 THEN `~(LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)=0)` by PROVE_TAC[LENGTH_NIL] 3072 THEN `LENGTH(BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) > 0` by DECIDE_TAC 3073 THEN `LENGTH(TAKE_FIRST P (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0` 3074 by PROVE_TAC[LENGTH_TAKE_FIRST_NON_EMPTY] 3075 THEN `LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) > 0` 3076 by PROVE_TAC 3077 [LENGTH_TAKE_FIRST_TAKE_FIRSTN,DECIDE``m:num > 0 /\ m <= n:num ==> n > 0``] 3078 THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) > 0` 3079 by PROVE_TAC 3080 [LENGTH_TAKE_FIRST_TAKE_FIRSTN,LENGTH_TAKE_FIRST_SUC, 3081 DECIDE``m:num > 0 /\ m <= n:num /\ n <= p:num ==> p > 0``] 3082 THEN `LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 3083 THEN `LENGTH l > LENGTH(TAKE_FIRSTN P (SUC(SUC n)) l) - 1` by DECIDE_TAC 3084 THEN `LENGTH l > LENGTH (TAKE_FIRST P l) 3085 + 3086 LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1` 3087 by PROVE_TAC[LENGTH_TAKE_FIRSTN_LEMMA] 3088 THEN `LENGTH l > (LENGTH (TAKE_FIRST P l) - 1) 3089 + 3090 LENGTH(TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l))` 3091 by DECIDE_TAC 3092 THEN RW_TAC std_ss [DECIDE ``m > 0 ==> (m + n - 1 = (m - 1) + n)``] 3093 THEN RW_TAC list_ss [SEL_BUTFIRSTN,SEL_TAKE_FIRST] 3094 THEN `SEL (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l) 3095 (0,LENGTH (TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)) - 1) = 3096 TAKE_FIRSTN P (SUC n) (BUTFIRSTN (LENGTH (TAKE_FIRST P l)) l)` 3097 by PROVE_TAC[] 3098 THEN `SUC(LENGTH (TAKE_FIRST P l) - 1) = LENGTH(TAKE_FIRST P l)` by DECIDE_TAC 3099 THEN RW_TAC list_ss []); 3100 3101val FILTER_SEL = 3102 store_thm 3103 ("FILTER_SEL", 3104 ``!P n l. 3105 n < LENGTH (FILTER P l) 3106 ==> 3107 (FILTER P (SEL l (0,LENGTH (TAKE_FIRSTN P (SUC n) l) - 1)) = 3108 SEL (FILTER P l) (0,n))``, 3109 RW_TAC list_ss [] 3110 THEN `LENGTH (FILTER P l) > 0` by DECIDE_TAC 3111 THEN IMP_RES_TAC LENGTH_FILTER_NON_EMPTY 3112 THEN RW_TAC list_ss [SEL_TAKE_FIRSTN, GSYM FIRSTN_FILTER_TAKE_FIRSTN] 3113 THEN `LENGTH (FILTER P l) <= LENGTH l` by PROVE_TAC[LENGTH_FILTER] 3114 THEN `n < LENGTH l` by DECIDE_TAC 3115 THEN RW_TAC list_ss [FIRSTN_SEL]); 3116 3117val FILTER_SEL_PATH_FILTER_FINITE = 3118 store_thm 3119 ("FILTER_SEL_PATH_FILTER_FINITE", 3120 ``!P n l. 3121 n < LENGTH (PATH_FILTER P (FINITE l)) 3122 ==> 3123 (FILTER P (SEL (FINITE l) (0, LENGTH (PATH_TAKE_FIRSTN P (SUC n) (FINITE l)) - 1)) 3124 = 3125 SEL (PATH_FILTER P (FINITE l)) (0, n))``, 3126 REPEAT GEN_TAC 3127 THEN RW_TAC list_ss 3128 [PATH_FILTER_def,LENGTH_def,SEL_FINITE,LS,FILTER_SEL,PATH_TAKE_FIRSTN_def]); 3129 3130 3131(* 3132val FILTER_SEL_PATH_FILTER = 3133 store_thm 3134 ("FILTER_SEL_PATH_FILTER", 3135 ``!P n v. 3136 n < LENGTH (PATH_FILTER P v) 3137 ==> 3138 (FILTER P (SEL v (0, LENGTH (PATH_TAKE_FIRSTN P (SUC n) v) - 1)) 3139 = 3140 SEL (PATH_FILTER P v) (0, n))``, 3141 GEN_TAC THEN GEN_TAC 3142 THEN Cases 3143 THEN RW_TAC list_ss [FILTER_SEL_PATH_FILTER_FINITE] 3144 THEN RW_TAC list_ss [PATH_FILTER_def] 3145 THEN FULL_SIMP_TAC list_ss [] 3146*) 3147 3148val TOP_FREE_CONS = 3149 store_thm 3150 ("TOP_FREE_CONS", 3151 ``!x l. TOP_FREE(x::l) = TOP_FREE[x] /\ TOP_FREE l``, 3152 GEN_TAC 3153 THEN Induct_on `l` 3154 THEN Cases_on `x` 3155 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def]); 3156 3157val BOTTOM_FREE_CONS = 3158 store_thm 3159 ("BOTTOM_FREE_CONS", 3160 ``!x l. BOTTOM_FREE(x::l) = BOTTOM_FREE[x] /\ BOTTOM_FREE l``, 3161 GEN_TAC 3162 THEN Induct_on `l` 3163 THEN Cases_on `x` 3164 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def]); 3165 3166(*****************************************************************************) 3167(* Proofs of TOP_FREE_SEL and BOTTOM_FREE_SEL that follow can probably be *) 3168(* simplified. *) 3169(*****************************************************************************) 3170val TOP_FREE_SEL = 3171 store_thm 3172 ("TOP_FREE_SEL", 3173 ``!l n. TOP_FREE l /\ n < LENGTH l ==> TOP_FREE(SEL l (0,n))``, 3174 SIMP_TAC list_ss 3175 [GSYM ADD1,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3176 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def] 3177 THEN Induct_on `n` 3178 THEN RW_TAC std_ss [FinitePSLPathTheory.SEL_REC_def] 3179 THEN `(HD l::TL l) = l` by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``p:num<n ==> ~(n=0)``,CONS] 3180 THEN Cases_on `HD l` 3181 THEN FULL_SIMP_TAC list_ss [TOP_FREE_def] 3182 THENL 3183 [PROVE_TAC[TOP_FREE_CONS,TOP_FREE_def], 3184 PROVE_TAC[TOP_FREE_CONS,TOP_FREE_def], 3185 `0 < LENGTH l` by DECIDE_TAC 3186 THEN IMP_RES_TAC LENGTH_TL 3187 THEN `n < LENGTH(TL l)` by DECIDE_TAC 3188 THEN `TOP_FREE(TL l)` by PROVE_TAC[TOP_FREE_CONS] 3189 THEN `n < LENGTH l` by DECIDE_TAC 3190 THEN `TOP_FREE (HD l::SEL_REC n 0 (TL l))` by PROVE_TAC[] 3191 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def], 3192 `0 < LENGTH l` by DECIDE_TAC 3193 THEN IMP_RES_TAC LENGTH_TL 3194 THEN `n < LENGTH(TL l)` by DECIDE_TAC 3195 THEN `TOP_FREE(TL l)` by PROVE_TAC[TOP_FREE_CONS] 3196 THEN `n < LENGTH l` by DECIDE_TAC 3197 THEN `TOP_FREE (HD l::SEL_REC n 0 (TL l))` by PROVE_TAC[] 3198 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def]]); 3199 3200val BOTTOM_FREE_SEL = 3201 store_thm 3202 ("BOTTOM_FREE_SEL", 3203 ``!l n. BOTTOM_FREE l /\ n < LENGTH l ==> BOTTOM_FREE(SEL l (0,n))``, 3204 SIMP_TAC list_ss 3205 [GSYM ADD1,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3206 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def] 3207 THEN Induct_on `n` 3208 THEN RW_TAC std_ss [FinitePSLPathTheory.SEL_REC_def] 3209 THEN `(HD l::TL l) = l` by PROVE_TAC[NULL_EQ_NIL,LENGTH_NIL,DECIDE``p:num<n ==> ~(n=0)``,CONS] 3210 THEN Cases_on `HD l` 3211 THEN FULL_SIMP_TAC list_ss [BOTTOM_FREE_def] 3212 THENL 3213 [PROVE_TAC[BOTTOM_FREE_CONS,BOTTOM_FREE_def], 3214 `0 < LENGTH l` by DECIDE_TAC 3215 THEN IMP_RES_TAC LENGTH_TL 3216 THEN `n < LENGTH(TL l)` by DECIDE_TAC 3217 THEN `BOTTOM_FREE(TL l)` by PROVE_TAC[BOTTOM_FREE_CONS] 3218 THEN `n < LENGTH l` by DECIDE_TAC 3219 THEN `BOTTOM_FREE (HD l::SEL_REC n 0 (TL l))` by PROVE_TAC[] 3220 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def], 3221 PROVE_TAC[BOTTOM_FREE_CONS,BOTTOM_FREE_def], 3222 `0 < LENGTH l` by DECIDE_TAC 3223 THEN IMP_RES_TAC LENGTH_TL 3224 THEN `n < LENGTH(TL l)` by DECIDE_TAC 3225 THEN `BOTTOM_FREE(TL l)` by PROVE_TAC[BOTTOM_FREE_CONS] 3226 THEN `n < LENGTH l` by DECIDE_TAC 3227 THEN `BOTTOM_FREE (HD l::SEL_REC n 0 (TL l))` by PROVE_TAC[] 3228 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def]]); 3229 3230(*****************************************************************************) 3231(* |- !p. EL n (SEL p (0,n)) = EL n p *) 3232(*****************************************************************************) 3233val EL_SEL0_LEMMA = 3234 SIMP_RULE arith_ss 3235 [FinitePSLPathTheory.ELEM_def,FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def, 3236 FinitePSLPathTheory.HD_RESTN] 3237 (Q.SPECL[`n`,`n`]FinitePSLPathTheory.EL_SEL0); 3238 3239(*****************************************************************************) 3240(* |- !p. LENGTH (SEL p (0,n)) = n + 1 *) 3241(*****************************************************************************) 3242val LENGTH_SEL0 = 3243 SIMP_RULE arith_ss [] (Q.SPECL[`0`,`n`]FinitePSLPathTheory.LENGTH_SEL); 3244 3245val LENGTH_TAKE_FIRSTN_SEL_LEMMA = 3246 store_thm 3247 ("LENGTH_TAKE_FIRSTN_SEL_LEMMA", 3248 ``P(EL n l) /\ n < LENGTH l 3249 ==> 3250 (LENGTH(TAKE_FIRSTN P (SUC (LENGTH (FILTER P (SEL l (0,n))) - 1)) (SEL l (0,n))) - 1 = n)``, 3251 RW_TAC list_ss [] 3252 THEN `LENGTH(SEL l (0,n)) = n+1` by PROVE_TAC[LENGTH_SEL0] 3253 THEN `P(EL n (SEL l (0,n)))` by PROVE_TAC[EL_SEL0_LEMMA] 3254 THEN `n < LENGTH (SEL l (0,n))` by DECIDE_TAC 3255 THEN `LENGTH (FILTER P (SEL l (0,n))) > 0` by PROVE_TAC[NON_ZERO_EXISTS_LENGTH_FILTER] 3256 THEN `SUC (LENGTH (FILTER P (SEL l (0,n))) - 1) = LENGTH (FILTER P (SEL l (0,n)))` by DECIDE_TAC 3257 THEN RW_TAC list_ss [] 3258 THEN `P(LAST (SEL l (0,n)))` by PROVE_TAC[EL_LAST_SEL] 3259 THEN `HOLDS_LAST P (SEL l (0,n))` by PROVE_TAC[HOLDS_LAST_def] 3260 THEN IMP_RES_TAC HOLDS_LAST_TAKE_FIRSTN 3261 THEN RW_TAC list_ss []); 3262 3263(* 3264val LENGTH_TAKE_FIRSTN_SEL_LEMMA = 3265 store_thm 3266 ("LENGTH_TAKE_FIRSTN_SEL_LEMMA", 3267 ``P(EL n l) /\ n < LENGTH l 3268 ==> 3269 (LENGTH(TAKE_FIRSTN P (SUC (LENGTH (FILTER P (SEL l (0,n))) - 1)) l) - 1 = n)``, 3270 RW_TAC list_ss [] 3271 THEN `LENGTH(SEL l (0,n)) = n+1` by PROVE_TAC[LENGTH_SEL0] 3272 THEN `P(EL n (SEL l (0,n)))` by PROVE_TAC[EL_SEL0_LEMMA] 3273 THEN `n < LENGTH (SEL l (0,n))` by DECIDE_TAC 3274 THEN `LENGTH (FILTER P (SEL l (0,n))) > 0` by PROVE_TAC[NON_ZERO_EXISTS_LENGTH_FILTER] 3275 THEN `SUC (LENGTH (FILTER P (SEL l (0,n))) - 1) = LENGTH (FILTER P (SEL l (0,n)))` by DECIDE_TAC 3276 THEN RW_TAC list_ss [] 3277 THEN `P(LAST (SEL l (0,n)))` by PROVE_TAC[EL_LAST_SEL] 3278 THEN `HOLDS_LAST P (SEL l (0,n))` by PROVE_TAC[HOLDS_LAST_def] 3279 THEN RW_TAC list_ss [GSYM FIRSTN_SEL] 3280 3281Want 3282LENGTH (TAKE_FIRSTN P (LENGTH (FILTER P (FIRSTN n l))) l) = n 3283reduce using 3284LENGTH_FILTER_FIRSTN 3285to 3286TAKE_FIRSTN P (LENGTH (FILTER P (FIRSTN n l))) l = FILTER P (FIRSTN (LENGTH (TAKE_FIRSTN P n l)) l 3287reduce using 3288FIRSTN_TAKE_FIRSTN 3289to 3290TAKE_FIRSTN P (LENGTH (FILTER P (FIRSTN n l))) l = FILTER P (TAKE_FIRSTN P n l) 3291reduce using 3292FIRSTN_FILTER_TAKE_FIRSTN 3293to 3294TAKE_FIRSTN P (LENGTH (FILTER P (FIRSTN n l))) l = FIRSTN n (FILTER P l) 3295 3296 3297 THEN IMP_RES_TAC HOLDS_LAST_TAKE_FIRSTN 3298 THEN RW_TAC list_ss []); 3299*) 3300 3301val SEL_SEL = 3302 store_thm 3303 ("SEL_SEL", 3304 ``!(l:'a list) n. SEL (SEL l (0,n)) (0,n) = SEL l (0,n)``, 3305 SIMP_TAC list_ss 3306 [FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 3307 FinitePSLPathTheory.HEAD_def,FinitePSLPathTheory.REST_def] 3308 THEN REWRITE_TAC[GSYM ADD1] 3309 THEN Induct_on `n` 3310 THEN FULL_SIMP_TAC list_ss 3311 [FinitePSLPathTheory.SEL_REC_def,FinitePSLPathTheory.HEAD_def, 3312 FinitePSLPathTheory.REST_def]); 3313 3314(*****************************************************************************) 3315(* |- !n l P. *) 3316(* P (EL n l) /\ n < LENGTH l ==> *) 3317(* 0 < LENGTH (FILTER P (SEL l (0,n))) ==> *) 3318(* (FILTER P (SEL l (0,n)) = *) 3319(* SEL (FILTER P (SEL l (0,n))) *) 3320(* (0,LENGTH (FILTER P (SEL l (0,n))) - 1)) *) 3321(*****************************************************************************) 3322val FILTER_SEL_COR = 3323 GEN_ALL 3324 (DISCH_ALL 3325 (SIMP_RULE 3326 list_ss 3327 [SEL_SEL,ASSUME``P(EL n l) /\ n < LENGTH(l:'a letter list)``, 3328 LENGTH_TAKE_FIRSTN_SEL_LEMMA] 3329 (Q.ISPECL 3330 [`P:'a letter -> bool`,`LENGTH(FILTER P (SEL (l:'a letter list) (0,n))) - 1`,`SEL (l:'a letter list) (0,n)`] 3331 FILTER_SEL))); 3332 3333(*****************************************************************************) 3334(* |- j < LENGTH l - 1 ==> (l = SEL l (0,j) <> SEL l (j + 1,LENGTH l - 1)) *) 3335(*****************************************************************************) 3336val SEL_SPLIT_LEMMA = 3337 SIMP_RULE 3338 list_ss 3339 [SEL_LENGTH] 3340 (SPECL 3341 [``l:'a list``,``j:num``,``0``,``LENGTH(l:'a list)-1``] 3342 FinitePSLPathTheory.SEL_SPLIT); 3343 3344val SEL_CHOP = 3345 store_thm 3346 ("SEL_CHOP", 3347 ``j < LENGTH l ==> ?l'. l = SEL l (0,j) <> l'``, 3348 Cases_on `j = LENGTH l - 1` 3349 THEN RW_TAC list_ss [SEL_LENGTH] 3350 THENL 3351 [Q.EXISTS_TAC `[]` 3352 THEN RW_TAC list_ss [], 3353 `j < LENGTH l - 1` by DECIDE_TAC 3354 THEN PROVE_TAC[SEL_SPLIT_LEMMA]]); 3355 3356local 3357open FinitePSLPathTheory 3358in 3359val F_PROJ_F_STRONG_SERE_FINITE_LEMMA1 = 3360 SIMP_RULE 3361 list_ss 3362 [ELEM_EL,EL_SEL0,LENGTH_SEL] 3363 (ISPECL 3364 [``CLOCK c``,``SEL (l :'a letter list) (0,j)``,``j:num``] 3365 NON_ZERO_EXISTS_LENGTH_FILTER) 3366val F_PROJ_F_STRONG_SERE_FINITE_LEMMA2 = 3367 SIMP_RULE 3368 list_ss 3369 [] 3370 (ISPECL 3371 [``FILTER (CLOCK c) (SEL (l :'a letter list) (0,j))``, 3372 ``l' :'a letter list``, 3373 ``LENGTH (FILTER (CLOCK c) (SEL (l :'a letter list) (0,j))) - 1``] 3374 SEL_APPEND1) 3375end; 3376 3377val F_PROJ_F_STRONG_SERE_FINITE = 3378 store_thm 3379 ("F_PROJ_F_STRONG_SERE_FINITE", 3380 ``!r. 3381 F_CLOCK_FREE (F_STRONG_SERE r) ==> 3382 !l. 3383 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 3384 !c. 3385 UF_SEM (PROJ (FINITE l) c) (F_STRONG_SERE r) = 3386 F_SEM (FINITE l) c (F_STRONG_SERE r)``, 3387 RW_TAC (list_ss++resq_SS) 3388 [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def,LS,PATH_FILTER_def, 3389 PATH_TOP_FREE_def,PATH_BOTTOM_FREE_def,SEL_FINITE,LIST_PROJ_def] 3390 THEN EQ_TAC 3391 THEN RW_TAC list_ss [] 3392 THENL 3393 [`LENGTH (FILTER (CLOCK c) l) <= LENGTH l` by PROVE_TAC[LENGTH_FILTER] 3394 THEN `j < LENGTH l` by DECIDE_TAC 3395 THEN Q.EXISTS_TAC `LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1` 3396 THEN RW_TAC list_ss [LIST_PROJ_def,FILTER_SEL] 3397 THENL 3398 [`LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 3399 THEN DECIDE_TAC, 3400 `LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 3401 THEN `LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1 < LENGTH l` by DECIDE_TAC 3402 THEN `S_SEM (SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))) c r = 3403 (LENGTH(SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))) > 0 3404 ==> CLOCK c (LAST(SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))))) 3405 /\ 3406 US_SEM (LIST_PROJ (SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))) c) r` 3407 by PROVE_TAC[S_PROJ,TOP_FREE_SEL,BOTTOM_FREE_SEL] 3408 THEN RW_TAC list_ss [LIST_PROJ_def,FILTER_SEL,SEL_TAKE_FIRSTN,LAST_TAKE_FIRSTN]], 3409 `(LENGTH (SEL l (0,j)) > 0 3410 ==> 3411 CLOCK c (LAST (SEL l (0,j)))) /\ US_SEM (FILTER (CLOCK c) (SEL l (0,j))) r` 3412 by PROVE_TAC[S_PROJ,TOP_FREE_SEL,BOTTOM_FREE_SEL,LIST_PROJ_def] 3413 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.LENGTH_SEL,FinitePSLPathTheory.EL_LAST_SEL] 3414 THEN Q.EXISTS_TAC `LENGTH (FILTER (CLOCK c) (SEL l (0,j))) - 1` 3415 THEN IMP_RES_TAC NON_ZERO_EXISTS_LENGTH_FILTER 3416 THEN RW_TAC list_ss [] 3417 THEN IMP_RES_TAC SEL_CHOP 3418 THENL 3419 [POP_ASSUM(fn th => CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[th]))) 3420 THEN RW_TAC list_ss [FILTER_APPEND], 3421 POP_ASSUM(fn th => CONV_TAC((RATOR_CONV o RAND_CONV o RATOR_CONV) (ONCE_REWRITE_CONV[th]))) 3422 THEN IMP_RES_TAC F_PROJ_F_STRONG_SERE_FINITE_LEMMA1 3423 THEN `LENGTH (FILTER (CLOCK c) (SEL l (0,j))) - 1 < LENGTH(FILTER (CLOCK c) (SEL l (0,j)))` 3424 by DECIDE_TAC 3425 THEN `0 < LENGTH (FILTER (CLOCK c) (SEL l (0,j)))` by DECIDE_TAC 3426 THEN RW_TAC std_ss [F_PROJ_F_STRONG_SERE_FINITE_LEMMA2,FILTER_APPEND,SEL_LENGTH]]]); 3427 3428(* 3429 3430val F_PROJ_F_WEAK_SERE_FINITE = 3431 store_thm 3432 ("F_PROJ_F_WEAK_SERE_FINITE", 3433 ``!r. 3434 F_CLOCK_FREE (F_WEAK_SERE r) ==> 3435 !l. 3436 PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 3437 !c. 3438 UF_SEM (PROJ (FINITE l) c) (F_WEAK_SERE r) = 3439 F_SEM (FINITE l) c (F_WEAK_SERE r)``, 3440 RW_TAC (list_ss++resq_SS) 3441 [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def,LS,PATH_FILTER_def, 3442 PATH_TOP_FREE_def,PATH_BOTTOM_FREE_def,SEL_FINITE,LIST_PROJ_def] 3443 THEN EQ_TAC 3444 THEN RW_TAC list_ss [TOP_OMEGA_def,LENGTH_def,LS,LENGTH_CAT] 3445 THENL 3446 [`LENGTH (FILTER (CLOCK c) l) <= LENGTH l` by PROVE_TAC[LENGTH_FILTER] 3447 THEN `j < LENGTH l` by DECIDE_TAC 3448 THEN Q.EXISTS_TAC `LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1` 3449 THEN RW_TAC list_ss [LIST_PROJ_def,FILTER_SEL] 3450 THENL 3451 [`LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 3452 THEN DECIDE_TAC, 3453 `LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) <= LENGTH l` by PROVE_TAC[LENGTH_TAKE_FIRSTN] 3454 THEN `LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1 < LENGTH l` by DECIDE_TAC 3455 THEN `S_SEM (SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))) c r = 3456 (LENGTH(SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))) > 0 3457 ==> CLOCK c (LAST(SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))))) 3458 /\ 3459 US_SEM (LIST_PROJ (SEL l (0,(LENGTH (TAKE_FIRSTN (CLOCK c) (SUC j) l) - 1))) c) r` 3460 by PROVE_TAC[S_PROJ,TOP_FREE_SEL,BOTTOM_FREE_SEL] 3461 THEN RW_TAC list_ss [LIST_PROJ_def,FILTER_SEL,SEL_TAKE_FIRSTN,LAST_TAKE_FIRSTN]], 3462 `(LENGTH (SEL l (0,j)) > 0 3463 ==> 3464 CLOCK c (LAST (SEL l (0,j)))) /\ US_SEM (FILTER (CLOCK c) (SEL l (0,j))) r` 3465 by PROVE_TAC[S_PROJ,TOP_FREE_SEL,BOTTOM_FREE_SEL,LIST_PROJ_def] 3466 THEN FULL_SIMP_TAC list_ss [FinitePSLPathTheory.LENGTH_SEL,FinitePSLPathTheory.EL_LAST_SEL] 3467 THEN Q.EXISTS_TAC `LENGTH (FILTER (CLOCK c) (SEL l (0,j))) - 1` 3468 THEN IMP_RES_TAC NON_ZERO_EXISTS_LENGTH_FILTER 3469 THEN RW_TAC list_ss [] 3470 THEN IMP_RES_TAC SEL_CHOP 3471 THENL 3472 [POP_ASSUM(fn th => CONV_TAC(RAND_CONV(ONCE_REWRITE_CONV[th]))) 3473 THEN RW_TAC list_ss [FILTER_APPEND], 3474 POP_ASSUM(fn th => CONV_TAC((RATOR_CONV o RAND_CONV o RATOR_CONV) (ONCE_REWRITE_CONV[th]))) 3475 THEN IMP_RES_TAC F_PROJ_F_STRONG_SERE_FINITE_LEMMA1 3476 THEN `LENGTH (FILTER (CLOCK c) (SEL l (0,j))) - 1 < LENGTH(FILTER (CLOCK c) (SEL l (0,j)))` 3477 by DECIDE_TAC 3478 THEN `0 < LENGTH (FILTER (CLOCK c) (SEL l (0,j)))` by DECIDE_TAC 3479 THEN RW_TAC std_ss [F_PROJ_F_STRONG_SERE_FINITE_LEMMA2,FILTER_APPEND,SEL_LENGTH]]]); 3480 3481 3482val F_PROJ_F_NEXT_FINITE = 3483 store_thm 3484 ("F_PROJ_F_NEXT_FINITE", 3485 ``!f. 3486 (F_CLOCK_FREE f ==> 3487 !l. PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 3488 !c. UF_SEM (PROJ (FINITE l) c) f = F_SEM (FINITE l) c f) 3489 ==> 3490 F_CLOCK_FREE (F_NEXT f) ==> 3491 !l. PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) ==> 3492 !c. UF_SEM (PROJ (FINITE l) c) (F_NEXT f) = 3493 F_SEM (FINITE l) c (F_NEXT f)``, 3494 RW_TAC (list_ss++resq_SS) 3495 [UF_SEM,F_SEM,GSYM CLOCK_def,PROJ_def,F_CLOCK_FREE_def,LS,PATH_FILTER_def, 3496 PATH_TOP_FREE_def,PATH_BOTTOM_FREE_def,SEL_FINITE,LIST_PROJ_def] 3497 THEN EQ_TAC 3498 THEN RW_TAC list_ss [] 3499 3500val F_PROJ_FINITE = 3501 store_thm 3502 ("F_PROJ_FINITE", 3503 ``!f. 3504 F_CLOCK_FREE f 3505 ==> 3506 !l. PATH_TOP_FREE (FINITE l) /\ PATH_BOTTOM_FREE (FINITE l) 3507 ==> 3508 !c. UF_SEM (PROJ (FINITE l) c) f = F_SEM (FINITE l) c f``, 3509 INDUCT_THEN fl_induct ASSUME_TAC 3510 THENL 3511 [(* F_STRONG_BOOL b *) 3512 RW_TAC std_ss [F_PROJ_F_STRONG_BOOL], 3513 (* F_WEAK_BOOL b *) 3514 RW_TAC std_ss [F_PROJ_F_WEAK_BOOL], 3515 (* F_NOT_BOOL b *) 3516 RW_TAC std_ss [F_PROJ_F_NOT_BOOL_FINITE], 3517 (* F_AND_BOOL b *) 3518 RW_TAC std_ss [F_PROJ_F_AND_BOOL_FINITE], 3519 (* F_STRONG_SERE b *) 3520 RW_TAC std_ss [F_PROJ_F_STRONG_SERE_FINITE], 3521 3522*) 3523 3524val _ = export_theory(); 3525