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