1(*****************************************************************************) 2(* Create "PSLPathTheory", the theory of (finite and infinite) sequences. *) 3(* Note that finite paths can be empty. *) 4(*****************************************************************************) 5 6(*****************************************************************************) 7(* START BOILERPLATE *) 8(*****************************************************************************) 9 10(****************************************************************************** 11* Load theories 12* (commented out for compilation) 13******************************************************************************) 14(* 15quietdec := true; 16map load ["intLib","FinitePSLPathTheory"]; 17open intLib rich_listTheory FinitePSLPathTheory; 18val _ = intLib.deprecate_int(); 19quietdec := false; 20*) 21 22(****************************************************************************** 23* Boilerplate needed for compilation 24******************************************************************************) 25open HolKernel Parse boolLib bossLib; 26 27(****************************************************************************** 28* Open theories 29******************************************************************************) 30open intLib rich_listTheory FinitePSLPathTheory; 31 32(****************************************************************************** 33* Set default parsing to natural numbers rather than integers 34******************************************************************************) 35val _ = intLib.deprecate_int(); 36 37(*****************************************************************************) 38(* END BOILERPLATE *) 39(*****************************************************************************) 40 41(****************************************************************************** 42* Simpsets to deal properly with theorems containing SUC 43******************************************************************************) 44val simp_arith_ss = simpLib.++ (arith_ss, numSimps.SUC_FILTER_ss); 45 46(****************************************************************************** 47* Start a new theory called PSLPath 48******************************************************************************) 49val _ = new_theory "PSLPath"; 50val _ = ParseExtras.temp_loose_equality() 51 52(****************************************************************************** 53* A path is finite or infinite 54******************************************************************************) 55val path_def = 56 Hol_datatype 57 `path = FINITE of ('s list) 58 | INFINITE of (num -> 's)`; 59 60(****************************************************************************** 61* Tests 62******************************************************************************) 63val IS_FINITE_def = 64 Define `(IS_FINITE(FINITE p) = T) 65 /\ 66 (IS_FINITE(INFINITE f) = F)`; 67 68val IS_INFINITE_def = 69 Define `(IS_INFINITE(FINITE p) = F) 70 /\ 71 (IS_INFINITE(INFINITE f) = T)`; 72 73(****************************************************************************** 74* HEAD (p0 p1 p2 p3 ...) = p0 75******************************************************************************) 76val HEAD_def = 77 Define `(HEAD (FINITE p) = HD p) 78 /\ 79 (HEAD (INFINITE f) = f 0)`; 80 81(****************************************************************************** 82* REST (p0 p1 p2 p3 ...) = (p1 p2 p3 ...) 83******************************************************************************) 84val REST_def = 85 Define `(REST (FINITE p) = FINITE(TL p)) 86 /\ 87 (REST (INFINITE f) = INFINITE(\n. f(n+1)))`; 88 89(****************************************************************************** 90* RESTN (p0 p1 p2 p3 ...) n = (pn p(n+1) p(n+2) ...) 91******************************************************************************) 92val RESTN_def = 93 Define `(RESTN p 0 = p) /\ (RESTN p (SUC n) = RESTN (REST p) n)`; 94 95(****************************************************************************** 96* Simple properties 97******************************************************************************) 98val NOT_IS_INFINITE = 99 store_thm 100 ("NOT_IS_INFINITE", 101 ``IS_INFINITE p = ~(IS_FINITE p)``, 102 Cases_on `p` 103 THEN RW_TAC std_ss [IS_INFINITE_def,IS_FINITE_def]); 104 105val NOT_IS_FINITE = 106 store_thm 107 ("NOT_IS_FINITE", 108 ``IS_FINITE p = ~(IS_INFINITE p)``, 109 Cases_on `p` 110 THEN RW_TAC std_ss [IS_INFINITE_def,IS_FINITE_def]); 111 112val IS_INFINITE_REST = 113 store_thm 114 ("IS_INFINITE_REST", 115 ``!p. IS_INFINITE(REST p) = IS_INFINITE p``, 116 Induct 117 THEN RW_TAC list_ss [REST_def,IS_INFINITE_def,IS_FINITE_def]); 118 119val IS_INFINITE_RESTN = 120 store_thm 121 ("IS_INFINITE_RESTN", 122 ``!n p. IS_INFINITE(RESTN p n) = IS_INFINITE p``, 123 Induct 124 THEN RW_TAC list_ss [RESTN_def,IS_INFINITE_REST]); 125 126val IS_FINITE_REST = 127 store_thm 128 ("IS_FINITE_REST", 129 ``!p. IS_FINITE(REST p) = IS_FINITE p``, 130 Induct 131 THEN RW_TAC list_ss [REST_def,IS_INFINITE_def,IS_FINITE_def]); 132 133val IS_FINITE_RESTN = 134 store_thm 135 ("IS_FINITE_RESTN", 136 ``!n p. IS_FINITE(RESTN p n) = IS_FINITE p``, 137 Induct 138 THEN RW_TAC list_ss [RESTN_def,IS_FINITE_REST]); 139 140val RESTN_FINITE = 141 store_thm 142 ("RESTN_FINITE", 143 ``!l n. RESTN (FINITE l) n = FINITE(RESTN l n)``, 144 Induct_on `n` 145 THEN RW_TAC std_ss 146 [RESTN_def,FinitePSLPathTheory.RESTN_def, 147 REST_def,FinitePSLPathTheory.REST_def]); 148 149val FINITE_TL = 150 store_thm 151 ("FINITE_TL", 152 ``!l. 0 < LENGTH l ==> (FINITE(TL l) = REST(FINITE l))``, 153 Induct 154 THEN RW_TAC list_ss [REST_def]); 155 156(****************************************************************************** 157* Extended numbers. 158******************************************************************************) 159val xnum_def = 160 Hol_datatype 161 `xnum = INFINITY (* length of an infinite path *) 162 | XNUM of num`; (* length of a finite path *) 163 164(****************************************************************************** 165* The constant ``to`` is a left associative infix with precedence 500. 166* It is overloaded so that 167* (m to n) i means m <= i /\ i < n (num_to_def) 168* (m to XNUM n) i means m <= i /\ i < n (xnum_to_def) 169* (m to INFINITY) i means m <= i (xnum_to_def) 170******************************************************************************) 171val num_to_def = 172 Define `$num_to m n i = m <= i /\ i < n`; 173 174val xnum_to_def = 175 Define 176 `($xnum_to m (XNUM n) i = m <= i /\ i < n) 177 /\ 178 ($xnum_to m INFINITY i = m <= i)`; 179 180val _ = overload_on("to", ``num_to``); 181val _ = overload_on("to", ``xnum_to``); 182 183val _ = set_fixity "to" (Infixl 500); 184 185(****************************************************************************** 186* Extend subtraction (-) to extended numbers 187******************************************************************************) 188val SUB_num_xnum_def = 189 Define 190 `($SUB_num_xnum (m:num) (XNUM (n:num)) = XNUM((m:num) - (n:num))) 191 /\ 192 ($SUB_num_xnum (m:num) INFINITY = INFINITY)`; 193 194val SUB_xnum_num_def = 195 Define 196 `($SUB_xnum_num (XNUM (m:num)) (n:num) = XNUM((m:num) - (n:num))) 197 /\ 198 ($SUB_xnum_num INFINITY (n:num) = INFINITY)`; 199 200val SUB_xnum_xnum_def = 201 Define 202 `($SUB_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = XNUM((m:num) - (n:num))) 203 /\ 204 ($SUB_xnum_xnum (XNUM (m:num)) INFINITY = XNUM 0) 205 /\ 206 ($SUB_xnum_xnum INFINITY (XNUM (n:num)) = INFINITY)`; 207 208val SUB = 209 save_thm 210 ("SUB", LIST_CONJ[SUB_num_xnum_def,SUB_xnum_num_def,SUB_xnum_xnum_def]); 211 212val _ = overload_on("-", ``SUB_num_xnum``); 213val _ = overload_on("-", ``SUB_xnum_num``); 214val _ = overload_on("-", ``SUB_xnum_xnum``); 215 216(****************************************************************************** 217* Extend less-than predicate (<) to extended numbers 218******************************************************************************) 219val LS_num_xnum_def = 220 Define 221 `($LS_num_xnum (m:num) (XNUM (n:num)) = (m:num) < (n:num)) 222 /\ 223 ($LS_num_xnum (m:num) INFINITY = T)`; 224 225val LS_xnum_num_def = 226 Define 227 `($LS_xnum_num (XNUM (m:num)) (n:num) = (m:num) < (n:num)) 228 /\ 229 ($LS_xnum_num INFINITY (n:num) = F)`; 230 231val LS_xnum_xnum_def = 232 Define 233 `($LS_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = (m:num) < (n:num)) 234 /\ 235 ($LS_xnum_xnum (XNUM (m:num)) INFINITY = T) 236 /\ 237 ($LS_xnum_xnum INFINITY (XNUM (n:num)) = F)`; 238 239val LS = 240 save_thm 241 ("LS", LIST_CONJ[LS_num_xnum_def,LS_xnum_num_def,LS_xnum_xnum_def]); 242 243val _ = overload_on("<", ``LS_num_xnum``); 244val _ = overload_on("<", ``LS_xnum_num``); 245val _ = overload_on("<", ``LS_xnum_xnum``); 246 247(****************************************************************************** 248* Extend less-than-or-equal predicate (<=) to extended numbers 249******************************************************************************) 250val LE_num_xnum_def = 251 Define 252 `($LE_num_xnum (m:num) (XNUM (n:num)) = (m:num) <= (n:num)) 253 /\ 254 ($LE_num_xnum (m:num) INFINITY = T)`; 255 256val LE_xnum_num_def = 257 Define 258 `($LE_xnum_num (XNUM (m:num)) (n:num) = (m:num) <= (n:num)) 259 /\ 260 ($LE_xnum_num INFINITY (n:num) = F)`; 261 262val LE_xnum_xnum_def = 263 Define 264 `($LE_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = (m:num) <= (n:num)) 265 /\ 266 ($LE_xnum_xnum (XNUM (m:num)) INFINITY = T) 267 /\ 268 ($LE_xnum_xnum INFINITY (XNUM (n:num)) = F) 269 /\ 270 ($LE_xnum_xnum INFINITY INFINITY = T)`; 271 272val LE = 273 save_thm("LE",LIST_CONJ[LE_num_xnum_def,LE_xnum_num_def,LE_xnum_xnum_def]); 274 275val _ = overload_on("<=", ``LE_num_xnum``); 276val _ = overload_on("<=", ``LE_xnum_num``); 277val _ = overload_on("<=", ``LE_xnum_xnum``); 278 279(****************************************************************************** 280* Extend greater-than predicate (>) to extended numbers 281******************************************************************************) 282val GT_num_xnum_def = 283 Define `$GT_num_xnum (m:num) (XNUM (n:num)) = (m:num) > (n:num)`; 284 285val GT_num_xnum_def = 286 Define 287 `($GT_num_xnum (m:num) (XNUM (n:num)) = (m:num) > (n:num)) 288 /\ 289 ($GT_num_xnum (m:num) INFINITY = F)`; 290 291val GT_xnum_num_def = 292 Define 293 `($GT_xnum_num (XNUM (m:num)) (n:num) = (m:num) > (n:num)) 294 /\ 295 ($GT_xnum_num INFINITY (n:num) = T)`; 296 297val GT_xnum_xnum_def = 298 Define 299 `($GT_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = (m:num) > (n:num)) 300 /\ 301 ($GT_xnum_xnum (XNUM (m:num)) INFINITY = F) 302 /\ 303 ($GT_xnum_xnum INFINITY (XNUM (n:num)) = T)`; 304 305val GT = 306 save_thm("GT",LIST_CONJ[GT_num_xnum_def,GT_xnum_num_def,GT_xnum_xnum_def]); 307 308val _ = overload_on(">", ``GT_num_xnum``); 309val _ = overload_on(">", ``GT_xnum_num``); 310val _ = overload_on(">", ``GT_xnum_xnum``); 311 312(****************************************************************************** 313* Extend greater-than-or-equal predicate (>=) to extended numbers 314******************************************************************************) 315val GE_num_xnum_def = 316 Define `$GE_num_xnum (m:num) (XNUM (n:num)) = (m:num) >= (n:num)`; 317 318val GE_num_xnum_def = 319 Define 320 `($GE_num_xnum (m:num) (XNUM (n:num)) = (m:num) >= (n:num)) 321 /\ 322 ($GE_num_xnum (m:num) INFINITY = F)`; 323 324val GE_xnum_num_def = 325 Define 326 `($GE_xnum_num (XNUM (m:num)) (n:num) = (m:num) >= (n:num)) 327 /\ 328 ($GE_xnum_num INFINITY (n:num) = T)`; 329 330val GE_xnum_xnum_def = 331 Define 332 `($GE_xnum_xnum (XNUM (m:num)) (XNUM (n:num)) = (m:num) >= (n:num)) 333 /\ 334 ($GE_xnum_xnum (XNUM (m:num)) INFINITY = F) 335 /\ 336 ($GE_xnum_xnum INFINITY (XNUM (n:num)) = T)`; 337 338val GE = 339 save_thm("GE",LIST_CONJ[GE_num_xnum_def,GE_xnum_num_def,GE_xnum_xnum_def]); 340 341val _ = overload_on(">=", ``GE_num_xnum``); 342val _ = overload_on(">=", ``GE_xnum_num``); 343val _ = overload_on(">=", ``GE_xnum_xnum``); 344 345val GT_LS = 346 store_thm 347 ("GT_LS", 348 ``!x:xnum n:num. (x > n) = (n < x)``, 349 Cases_on `x` 350 THEN RW_TAC arith_ss [GT_xnum_num_def,LS_num_xnum_def]); 351 352(****************************************************************************** 353* LESS m is predicate to test if a number is less than m 354* LESS : num -> num -> bool 355******************************************************************************) 356val LESS_def = 357 Define `LESS (m:num) (n:num) = n < m`; 358 359(****************************************************************************** 360* LESSX m is predicate to test if a number is less than extended number m 361* LESSX : xnum -> num -> bool 362******************************************************************************) 363val LESSX_def = 364 Define `LESSX (m:xnum) (n:num) = n < m`; 365 366val _ = overload_on ("LESS", Term`LESSX`); 367 368val IN_LESS = 369 store_thm 370 ("IN_LESS", 371 ``!m n:num. m IN LESS n = m < n``, 372 RW_TAC arith_ss [IN_DEF,LESS_def]); 373 374val IN_LESSX = 375 store_thm 376 ("IN_LESSX", 377 ``!m:num. (m IN LESSX INFINITY) /\ !n:num. m IN LESSX (XNUM n) = m < n``, 378 RW_TAC arith_ss [IN_DEF,LESSX_def,LS]); 379 380(****************************************************************************** 381* LENGTH(FINITE l) = XNUM(LENGTH l) 382* LENGTH(INFINITE l) = INFINITY 383******************************************************************************) 384val LENGTH_def = 385 Define `(LENGTH(FINITE l) = XNUM(list$LENGTH l)) 386 /\ 387 (LENGTH(INFINITE p) = INFINITY)`; 388 389(****************************************************************************** 390* ELEM (p0 p1 p2 p3 ...) n = pn 391******************************************************************************) 392val ELEM_def = Define `ELEM p n = HEAD(RESTN p n)`; 393 394val LENGTH_REST = 395 store_thm 396 ("LENGTH_REST", 397 ``!p. IS_FINITE p /\ 0 < LENGTH p 398 ==> (LENGTH(REST p) = LENGTH p - 1)``, 399 Cases 400 THEN RW_TAC std_ss 401 [LENGTH_def,REST_def,IS_FINITE_def,LENGTH_CONS,SUB,LS,IS_FINITE_def, 402 Cooper.COOPER_PROVE``0 < n = ?m. n = SUC m``] 403 THEN RW_TAC list_ss []); 404 405val LENGTH_REST_COR = 406 store_thm 407 ("LENGTH_REST_COR", 408 ``!l. 0 < LENGTH(FINITE l) ==> (LENGTH(REST(FINITE l)) = LENGTH(FINITE l) - 1)``, 409 PROVE_TAC[LENGTH_REST,IS_FINITE_def]); 410 411val LENGTH_RESTN = 412 store_thm 413 ("LENGTH_RESTN", 414 ``!n p. IS_FINITE p /\ n < LENGTH p 415 ==> (LENGTH(RESTN p n) = LENGTH p - n)``, 416 Induct 417 THEN Cases 418 THEN RW_TAC list_ss 419 [LENGTH_def,RESTN_def,IS_FINITE_REST,SUB, 420 IS_FINITE_def,REST_def,LENGTH_RESTN,LS,EL] 421 THEN `PSLPath$LENGTH(FINITE(TL l)) = XNUM(list$LENGTH(TL l))` by RW_TAC std_ss [LENGTH_def] 422 THEN Cases_on `l` 423 THEN FULL_SIMP_TAC list_ss [DECIDE ``~(SUC n < 0)``] 424 THEN ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `FINITE t` (el 3 thl))) 425 THEN FULL_SIMP_TAC std_ss [IS_FINITE_def,LENGTH_def,LS,SUB,EL]); 426 427val LENGTH_RESTN_COR = 428 store_thm 429 ("LENGTH_RESTN_COR", 430 ``!n l. n < LENGTH(FINITE l) 431 ==> 432 (LENGTH(RESTN(FINITE l) n) = LENGTH(FINITE l) - n)``, 433 PROVE_TAC[LENGTH_RESTN,IS_FINITE_def]); 434 435(****************************************************************************** 436* 0 < i ==> (RESTN (REST(INFINITE f)) (i-1) = RESTN (INFINITE f) i) 437******************************************************************************) 438val RESTN_REST_INFINITE = 439 store_thm 440 ("RESTN_REST_INFINITE", 441 ``!f i. 0 < i ==> (RESTN (REST(INFINITE f)) (i-1) = RESTN (INFINITE f) i)``, 442 Induct_on `i` 443 THEN RW_TAC list_ss [RESTN_def]); 444 445(****************************************************************************** 446* RESTN (REST (INFINITE f)) k = RESTN (INFINITE f) (k + 1) 447******************************************************************************) 448val RESTN_REST_INFINITE_COR = 449 save_thm 450 ("RESTN_REST_INFINITE_COR", 451 SIMP_RULE arith_ss 452 [DECIDE``(k+1)-1=k``](Q.SPECL[`f`,`k+1`]RESTN_REST_INFINITE)); 453 454(****************************************************************************** 455* Form needeed for computeLib 456******************************************************************************) 457val RESTN_AUX = 458 store_thm 459 ("RESTN_AUX", 460 ``RESTN p n = if n=0 then p else RESTN (REST p) (n-1)``, 461 Cases_on `n` THEN RW_TAC arith_ss [RESTN_def]); 462 463val _ = computeLib.add_funs[RESTN_AUX]; 464 465(****************************************************************************** 466* SEL_REC m n p = [p(n); p(n+1); ... ; p(n+m)] 467* (Recursive form for easy definition using Define) 468******************************************************************************) 469val SEL_REC_def = 470 Define 471 `(SEL_REC 0 n p = []) 472 /\ 473 (SEL_REC (SUC m) 0 p = (HEAD p)::SEL_REC m 0 (REST p)) 474 /\ 475 (SEL_REC (SUC m) (SUC n) p = SEL_REC (SUC m) n (REST p))`; 476 477(****************************************************************************** 478* SEL_REC m n p = [p(n); p(n+1); ... ; p(n+m-1)] 479* (Version for computeLib) 480******************************************************************************) 481val SEL_REC_AUX = 482 store_thm 483 ("SEL_REC_AUX", 484 ``SEL_REC m n p = 485 if m = 0 then [] else 486 if (n = 0) then (HEAD p)::SEL_REC (m-1) 0 (REST p) 487 else SEL_REC m (n-1) (REST p)``, 488 Cases_on `m` THEN Cases_on `n` THEN RW_TAC arith_ss [SEL_REC_def]); 489 490val _ = computeLib.add_funs[SEL_REC_AUX]; 491 492val SEL_REC_SUC = 493 store_thm 494 ("SEL_REC_SUC", 495 ``!p. SEL_REC (SUC m) n p = ELEM p n :: SEL_REC m (SUC n) p``, 496 Induct_on `n` 497 THEN RW_TAC arith_ss [SEL_REC_def,ELEM_def,RESTN_def] 498 THEN Induct_on `m` 499 THEN RW_TAC simp_arith_ss [SEL_REC_def,ELEM_def,RESTN_def]); 500 501(****************************************************************************** 502* SEL p (m,n) = [p m; ... ; p n] 503******************************************************************************) 504val SEL_def = Define `SEL p (m,n) = SEL_REC (n-m+1) m p`; 505 506(****************************************************************************** 507* CONS(x,p) add x to the front of p 508******************************************************************************) 509val CONS_def = 510 Define 511 `(CONS(x, FINITE l) = FINITE(list$CONS x l)) 512 /\ 513 (CONS(x, INFINITE f) = 514 INFINITE(\n. if n=0 then x else f(n-1)))`; 515 516val IS_INFINITE_CONS = 517 store_thm 518 ("IS_INFINITE_CONS", 519 ``!p x. IS_INFINITE(CONS(x,p)) = IS_INFINITE p``, 520 Induct 521 THEN RW_TAC list_ss [IS_INFINITE_def,CONS_def]); 522 523val IS_FINITE_CONS = 524 store_thm 525 ("IS_FINITE_CONS", 526 ``!p x. IS_FINITE(CONS(x,p)) = IS_FINITE p``, 527 Induct 528 THEN RW_TAC list_ss [IS_FINITE_def,CONS_def]); 529 530val HEAD_CONS = 531 store_thm 532 ("HEAD_CONS", 533 ``!x p. HEAD(CONS(x,p)) = x``, 534 REPEAT GEN_TAC 535 THEN Cases_on `p` 536 THEN RW_TAC list_ss [HEAD_def,CONS_def]); 537 538val REST_CONS = 539 store_thm 540 ("REST_CONS", 541 ``!x p. REST(CONS(x,p)) = p``, 542 REPEAT GEN_TAC 543 THEN Cases_on `p` 544 THEN RW_TAC list_ss [REST_def,CONS_def,ETA_AX]); 545 546(****************************************************************************** 547* RESTN (RESTN p m) n = RESTN p (m+n) 548******************************************************************************) 549val RESTN_RESTN = 550 store_thm 551 ("RESTN_RESTN", 552 ``!m n p. RESTN (RESTN p m) n = RESTN p (m+n)``, 553 Induct 554 THEN RW_TAC arith_ss [RESTN_def,arithmeticTheory.ADD_CLAUSES]); 555 556(****************************************************************************** 557* ELEM (RESTN p m) n = ELEM p (m+n) 558******************************************************************************) 559val ELEM_RESTN = 560 store_thm 561 ("ELEM_RESTN", 562 ``!m n p. ELEM (RESTN p m) n = ELEM p (n+m)``, 563 Induct 564 THEN RW_TAC arith_ss [RESTN_def,ELEM_def,RESTN_RESTN]); 565 566(****************************************************************************** 567* 0 < i /\ 0 < LENGTH l ==> (ELEM (FINITE(TL l)) (i-1) = ELEM (FINITE l) i) 568******************************************************************************) 569val ELEM_FINITE_TL = 570 store_thm 571 ("ELEM_FINITE_TL", 572 ``!l i. 0 < i /\ 0 < LENGTH l 573 ==> 574 (ELEM (FINITE(TL l)) (i-1) = ELEM (FINITE l) i)``, 575 Induct_on `i` 576 THEN RW_TAC list_ss [ELEM_def,REST_def,RESTN_def]); 577 578(****************************************************************************** 579* 0 < LENGTH l ==> (ELEM (FINITE (TL l)) k = ELEM (FINITE l) (k + 1)) 580******************************************************************************) 581val ELEM_FINITE_TL_COR = 582 save_thm 583 ("ELEM_FINITE_TL_COR", 584 SIMP_RULE arith_ss [DECIDE``(k+1)-1=k``](Q.SPECL[`l`,`k+1`]ELEM_FINITE_TL)); 585 586(****************************************************************************** 587* REST(INFINITE f) = INFINITE(\n. f(n+1)) 588******************************************************************************) 589val REST_INFINITE = 590 store_thm 591 ("REST_INFINITE", 592 ``!f. REST (INFINITE f) = INFINITE(\n. f(n+1))``, 593 RW_TAC list_ss [REST_def]); 594 595(****************************************************************************** 596* RESTN (INFINITE f) i = INFINITE(\n. f(n+i)) 597******************************************************************************) 598val RESTN_INFINITE = 599 store_thm 600 ("RESTN_INFINITE", 601 ``!f i. RESTN (INFINITE f) i = INFINITE(\n. f(n+i))``, 602 Induct_on `i` 603 THEN RW_TAC list_ss 604 [REST_INFINITE,ETA_AX,RESTN_def, 605 DECIDE``i + (n + 1) = n + SUC i``]); 606 607(****************************************************************************** 608* LENGTH (RESTN (INFINITE p) n) = INFINITY 609******************************************************************************) 610val LENGTH_RESTN_INFINITE = 611 store_thm 612 ("LENGTH_RESTN_INFINITE", 613 ``!p n. LENGTH (RESTN (INFINITE p) n) = INFINITY``, 614 RW_TAC std_ss [RESTN_INFINITE,LENGTH_def]); 615 616val LENGTH_RESTN_THM = 617 store_thm 618 ("LENGTH_RESTN_THM", 619 ``n < LENGTH p ==> (LENGTH (RESTN p n) = LENGTH p - n)``, 620 Cases_on `p` 621 THEN RW_TAC std_ss 622 [LS_num_xnum_def,LENGTH_RESTN,LENGTH_RESTN_INFINITE,RESTN_FINITE, 623 LENGTH_def,SUB,FinitePSLPathTheory.LENGTH_RESTN]); 624 625(****************************************************************************** 626* 0 < i ==> (ELEM (FINITE(TL l)) (i-1) = ELEM (FINITE l) i) 627******************************************************************************) 628val ELEM_REST_INFINITE = 629 store_thm 630 ("ELEM_REST_INFINITE", 631 ``!f i. 0 < i ==> (ELEM (REST(INFINITE f)) (i-1) = ELEM (INFINITE f) i)``, 632 Induct_on `i` 633 THEN RW_TAC list_ss [ELEM_def,RESTN_def]); 634 635(****************************************************************************** 636* ELEM (REST (INFINITE l)) k = ELEM (INFINITE l) (k + 1) 637******************************************************************************) 638val ELEM_REST_INFINITE_COR = 639 save_thm 640 ("ELEM_REST_INFINITE_COR", 641 SIMP_RULE arith_ss [DECIDE``(k+1)-1=k``](Q.SPECL[`l`,`k+1`]ELEM_REST_INFINITE)); 642 643(****************************************************************************** 644* CAT(w,p) creates a new path by concatenating w in front of p 645******************************************************************************) 646val CAT_def = 647 Define 648 `(CAT([], p) = p) 649 /\ 650 (CAT((x::w), p) = CONS(x, CAT(w,p)))`; 651 652val CAT_FINITE_APPEND = 653 store_thm 654 ("CAT_FINITE_APPEND", 655 ``!l p. CAT(l, FINITE p) = FINITE(APPEND l p)``, 656 Induct 657 THEN RW_TAC list_ss [CAT_def,CONS_def]); 658 659val LENGTH_CAT_FINITE = 660 store_thm 661 ("LENGTH_CAT_FINITE", 662 ``!l1 l2. LENGTH(CAT(l1, FINITE l2)) = XNUM(LENGTH l1 + LENGTH l2)``, 663 Induct 664 THEN RW_TAC list_ss 665 [CAT_def,LENGTH_def,CAT_FINITE_APPEND,CONS_def]); 666 667val IS_INFINITE_EXISTS = 668 store_thm 669 ("IS_INFINITE_EXISTS", 670 ``!w. IS_INFINITE w = ?p. w = INFINITE p``, 671 Induct 672 THEN RW_TAC list_ss [IS_INFINITE_def]); 673 674val CAT_INFINITE = 675 store_thm 676 ("CAT_INFINITE", 677 ``!l p. IS_INFINITE(CAT(l, INFINITE p))``, 678 Induct 679 THEN RW_TAC list_ss [CAT_def,CONS_def,IS_INFINITE_def] 680 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 681 THEN IMP_RES_TAC IS_INFINITE_EXISTS 682 THEN RW_TAC std_ss [CONS_def,IS_INFINITE_def]); 683 684val LENGTH_CAT_INFINITE = 685 store_thm 686 ("LENGTH_CAT_INFINITE", 687 ``!l p. LENGTH(CAT(l, INFINITE p)) = INFINITY``, 688 Induct 689 THEN RW_TAC list_ss 690 [CAT_def,LENGTH_def,CONS_def] 691 THEN `IS_INFINITE(CAT (l,INFINITE p))` by PROVE_TAC[CAT_INFINITE] 692 THEN IMP_RES_TAC IS_INFINITE_EXISTS 693 THEN RW_TAC std_ss [CONS_def,LENGTH_def]); 694 695val LENGTH_CAT = 696 save_thm("LENGTH_CAT",CONJ LENGTH_CAT_FINITE LENGTH_CAT_INFINITE); 697 698 699(****************************************************************************** 700* Append paths 701******************************************************************************) 702val PATH_APPEND_def = 703 Define 704 `(PATH_APPEND (FINITE l1) (FINITE l2) = FINITE(APPEND l1 l2)) 705 /\ 706 (PATH_APPEND (FINITE l) p = CAT(l, p)) 707 /\ 708 (PATH_APPEND (INFINITE f) _ = INFINITE f)`; 709 710(****************************************************************************** 711* Infix list concatenation 712******************************************************************************) 713val _ = set_fixity "<>" (Infixl 500); 714val _ = overload_on ("<>", Term`APPEND`); 715val _ = overload_on ("<>", Term`PATH_APPEND`); 716 717val IS_INFINITE_CAT = 718 store_thm 719 ("IS_INFINITE_CAT", 720 ``!p l. IS_INFINITE(CAT(l,p)) = IS_INFINITE p``, 721 Induct_on `l` 722 THEN RW_TAC list_ss [IS_INFINITE_def,CAT_def,IS_INFINITE_CONS]); 723 724val IS_FINITE_CAT = 725 store_thm 726 ("IS_FINITE_CAT", 727 ``!p l. IS_FINITE(CAT(l,p)) = IS_FINITE p``, 728 Induct_on `l` 729 THEN RW_TAC list_ss [IS_FINITE_def,CAT_def,IS_FINITE_CONS]); 730 731val ELEM_CAT_SEL = 732 store_thm 733 ("ELEM_CAT_SEL", 734 ``!(w:'a path) i (w':'a path). ELEM (CAT (SEL w (0,i),w')) 0 = ELEM w 0``, 735 Induct_on `i` 736 THEN RW_TAC simp_arith_ss 737 [SEL_ELEM,CAT_def,ELEM_def,HEAD_def,RESTN_def,REST_def,HEAD_CONS, 738 SEL_def,SEL_REC_def,FinitePSLPathTheory.SEL_def,FinitePSLPathTheory.SEL_REC_def, 739 CAT_def,DECIDE``SUC i + 1= SUC(i+1)``]); 740 741val SEL_REC_SPLIT = 742 store_thm 743 ("SEL_REC_SPLIT", 744 ``!n. SEL_REC (m+k) n p = 745 APPEND (SEL_REC k n p) (SEL_REC m (n+k) p)``, 746 Induct_on `k` 747 THEN RW_TAC list_ss [SEL_def,SEL_REC_def,arithmeticTheory.ONE] 748 THEN RW_TAC std_ss [DECIDE ``m + SUC k = SUC(m+k)``, 749 SEL_REC_SUC,APPEND,arithmeticTheory.ADD]); 750 751val SEL_SPLIT = 752 store_thm 753 ("SEL_SPLIT", 754 ``!p k m n. 755 m <= k /\ k < n 756 ==> 757 (SEL p (m,n) = APPEND (SEL p (m,k)) (SEL p (k+1,n)))``, 758 RW_TAC list_ss [SEL_def] 759 THEN IMP_RES_TAC 760 (DECIDE ``m <= k ==> k < n ==> (n + 1 - m = (n-k) + (k+1-m))``) 761 THEN IMP_RES_TAC(DECIDE ``m <= k ==> (k+ 1 = m + (k + 1 - m))``) 762 THEN ASSUM_LIST(fn thl => CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[el 2 thl]))) 763 THEN ASSUM_LIST(fn thl => CONV_TAC(RHS_CONV(RAND_CONV(ONCE_REWRITE_CONV[el 1 thl])))) 764 THEN REWRITE_TAC[SEL_REC_SPLIT]); 765 766val SEL_ELEM = 767 store_thm 768 ("SEL_ELEM", 769 ``!p m. SEL p (m,m) = [ELEM p m]``, 770 Induct_on `m` 771 THEN RW_TAC simp_arith_ss [SEL_def,SEL_REC_def,ELEM_def, 772 RESTN_def, SEL_REC_SUC]); 773 774val SEL_APPEND_SINGLETON_IMP = 775 store_thm 776 ("SEL_APPEND_SINGLETON_IMP", 777 ``j > i 778 ==> 779 (SEL p (i,j) = APPEND w [l]) ==> (SEL p (i,j-1) = w) /\ (ELEM p j = l)``, 780 REPEAT DISCH_TAC 781 THEN IMP_RES_TAC(DECIDE ``j:num > i:num ==> (i <= (j-1) /\ (j-1) < j)``) 782 THEN IMP_RES_TAC(DECIDE``j:num > i:num ==> (j - 1 + 1 = j)``) 783 THEN IMP_RES_TAC(ISPEC ``p :'a path`` SEL_SPLIT) 784 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 785 THEN ASSUM_LIST(fn thl => ASSUME_TAC(TRANS (GSYM(el 5 thl)) (el 1 thl))) 786 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss [SEL_ELEM,el 3 thl] (el 1 thl))) 787 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [APPEND_LAST_CANCEL]) 788 THEN RW_TAC std_ss []); 789 790val SEL_APPEND_SINGLETON = 791 store_thm 792 ("SEL_APPEND_SINGLETON", 793 ``j > i 794 ==> 795 ((SEL p (i,j) = APPEND w [l]) 796 = 797 (SEL p (i,j-1) = w) /\ (ELEM p j = l))``, 798 REPEAT STRIP_TAC 799 THEN EQ_TAC 800 THEN ZAP_TAC std_ss [SEL_APPEND_SINGLETON_IMP] 801 THEN IMP_RES_TAC(DECIDE ``j:num > i:num ==> i <= j - 1 /\ j - 1 < j``) 802 THEN IMP_RES_TAC 803 (ISPECL [``p :'a path``,``j:num-1``,``i:num``,``j:num``] SEL_SPLIT) 804 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 805 THEN IMP_RES_TAC(DECIDE``j:num > i:num ==> (j - 1 + 1 = j)``) 806 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss [SEL_ELEM,el 1 thl] (el 2 thl))) 807 THEN ZAP_TAC arith_ss [APPEND_LAST_CANCEL,SEL_ELEM]); 808 809val LENGTH_SEL_REC = 810 store_thm 811 ("LENGTH_SEL_REC", 812 ``!m n p. LENGTH(SEL_REC m n p) = m``, 813 Induct_on `m`THEN Induct_on `n` 814 THEN RW_TAC list_ss [SEL_REC_def]); 815 816val LENGTH_SEL = 817 store_thm 818 ("LENGTH_SEL", 819 ``!m n p. LENGTH(SEL p (m,n)) = n-m+1``, 820 RW_TAC arith_ss [SEL_def,SEL_REC_def,LENGTH_SEL_REC]); 821 822val HD_SEL = 823 store_thm 824 ("HD_SEL", 825 ``!i j p. i <= j ==> (HD(SEL p (i,j)) = ELEM p i)``, 826 Induct 827 THEN RW_TAC list_ss 828 [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1, 829 ELEM_def,RESTN_def] 830 THEN IMP_RES_TAC(DECIDE ``SUC i <= j ==> ((SUC (j - SUC i)) = (j-i))``) 831 THEN RW_TAC arith_ss [] 832 THEN ASSUM_LIST 833 (fn thl => 834 ASSUME_TAC 835 (GSYM 836 (Q.GEN `p` 837 (SIMP_RULE arith_ss thl (Q.SPECL [`p`,`i`,`j-1`] SEL_def))))) 838 THEN RW_TAC arith_ss [ELEM_def]); 839 840val HD_SEL0 = 841 store_thm 842 ("HD_SEL0", 843 ``HD(SEL p (0,i)) = HEAD p``, 844 RW_TAC list_ss [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1]); 845 846val TL_SEL_SUC = 847 store_thm 848 ("TL_SEL_SUC", 849 ``!i j p. i <= j ==> (TL(SEL p (i,SUC j)) = SEL (REST p) (i,j))``, 850 Induct 851 THEN RW_TAC list_ss 852 [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1, 853 ELEM_def,RESTN_def] 854 THEN IMP_RES_TAC(DECIDE ``SUC i:num <= j:num ==> ((SUC (j - SUC i)) = (j-i))``) 855 THEN RW_TAC arith_ss [] 856 THEN ASSUM_LIST 857 (fn thl => 858 ASSUME_TAC 859 (GSYM 860 (Q.GEN `p` 861 (SIMP_RULE arith_ss thl (Q.SPECL [`p`,`i`,`j`] SEL_def))))) 862 THEN IMP_RES_TAC(DECIDE ``SUC i:num <= j:num ==> (SUC (j - i) = j + 1 - i)``) 863 THEN RW_TAC arith_ss [] 864 THEN IMP_RES_TAC(DECIDE ``SUC i:num <= j:num ==> i <= j-1``) 865 THEN RES_TAC 866 THEN IMP_RES_TAC(DECIDE ``SUC i:num <= j:num ==> (SUC(j-1)=j)``) 867 THEN ASSUM_LIST 868 (fn thl => ASSUME_TAC(SIMP_RULE std_ss [el 1 thl] (el 2 thl))) 869 THEN RW_TAC arith_ss [SEL_def]); 870 871val TL_SEL = 872 store_thm 873 ("TL_SEL", 874 ``!i j p. i < j ==> (TL(SEL p (i,j)) = SEL (REST p) (i,j-1))``, 875 RW_TAC std_ss [] 876 THEN IMP_RES_TAC(DECIDE ``i:num < j:num ==> i <= j-1``) 877 THEN IMP_RES_TAC TL_SEL_SUC 878 THEN IMP_RES_TAC(DECIDE ``i:num < j:num ==> (SUC(j-1)=j)``) 879 THEN ASSUM_LIST 880 (fn thl => ASSUME_TAC(SIMP_RULE std_ss [el 1 thl] (el 2 thl))) 881 THEN RW_TAC arith_ss []); 882 883val TL_SEL0 = 884 store_thm 885 ("TL_SEL0", 886 ``TL(SEL p (0,SUC i)) = SEL (REST p) (0,i)``, 887 RW_TAC list_ss [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1]); 888 889val EL_SEL_LEMMA = 890 prove 891 (``!m i j p. 892 i <= j /\ m <= j-i ==> (EL m (SEL p (i,j)) = ELEM p (i+m))``, 893 Induct 894 THEN RW_TAC list_ss 895 [SEL_REC_def,ELEM_def,RESTN_def,EL, 896 HD_SEL,TL_SEL,RESTN_def,DECIDE``i + SUC m = SUC(i+m)``]); 897 898val EL_SEL = 899 store_thm 900 ("EL_SEL", 901 ``!i k j p. 902 i <= k ==> k <= j ==> (EL (k-i) (SEL p (i,j)) = ELEM p k)``, 903 RW_TAC arith_ss [EL_SEL_LEMMA]); 904 905val EL_SEL0 = 906 store_thm 907 ("EL_SEL0", 908 ``!j i p. j <= i ==> (EL j (SEL p (0,i)) = ELEM p j)``, 909 Induct 910 THEN RW_TAC list_ss [SEL_REC_def,ELEM_def,RESTN_def,HD_SEL0,EL] 911 THEN Induct_on `i` 912 THEN RW_TAC list_ss [SEL_REC_def,ELEM_def,RESTN_def,TL_SEL0,EL]); 913 914val SEL_REC_REST = 915 store_thm 916 ("SEL_REC_REST", 917 ``!p. SEL_REC m n (REST p) = SEL_REC m (SUC n) p``, 918 Induct_on `m` 919 THEN RW_TAC arith_ss [SEL_REC_def]); 920 921val SEL_REC_RESTN = 922 store_thm 923 ("SEL_REC_RESTN", 924 ``!p. SEL_REC m n (RESTN p r) = SEL_REC m (n + r) p``, 925 Induct_on `r` 926 THEN RW_TAC arith_ss [SEL_REC_def,RESTN_def,arithmeticTheory.ADD_CLAUSES] 927 THEN PROVE_TAC[SEL_REC_REST]); 928 929val SEL_RESTN = 930 store_thm 931 ("SEL_RESTN", 932 ``!p. SEL (RESTN p r) (n,m) = SEL p (r + n, r + m)``, 933 RW_TAC arith_ss [SEL_def,SEL_REC_RESTN]); 934 935val _ = export_theory(); 936