1 2(*****************************************************************************) 3(* Create "FinitePSLPathTheory", a theory of finite paths represented as *) 4(* lists. Note that finite paths can be empty in the "SEM_1" semantics. *) 5(* *) 6(* The theory "PSLPathTheory" defines a type ``:'a path`` of finite and *) 7(* infinite paths, and extends the path operators to work on these. *) 8(* *) 9(* Created Wed Dec 27 2002 *) 10(*****************************************************************************) 11 12(*****************************************************************************) 13(* START BOILERPLATE *) 14(*****************************************************************************) 15 16(****************************************************************************** 17* Load theories 18* (commented out for compilation) 19******************************************************************************) 20(* 21quietdec := true; 22app load ["bossLib", "rich_listTheory", "intLib", "arithmeticTheory"]; 23open listTheory rich_listTheory arithmeticTheory intLib; 24val _ = intLib.deprecate_int(); 25quietdec := false; 26*) 27 28(****************************************************************************** 29* Boilerplate needed for compilation 30******************************************************************************) 31open HolKernel Parse boolLib bossLib; 32 33(****************************************************************************** 34* Open theories 35******************************************************************************) 36open listTheory rich_listTheory arithmeticTheory intLib; 37 38(****************************************************************************** 39* Set default parsing to natural numbers rather than integers 40******************************************************************************) 41val _ = intLib.deprecate_int(); 42 43(*****************************************************************************) 44(* END BOILERPLATE *) 45(*****************************************************************************) 46 47(****************************************************************************** 48* Versions of simpsets that deal properly with theorems containing SUC 49******************************************************************************) 50val simp_arith_ss = simpLib.++ (arith_ss, numSimps.SUC_FILTER_ss); 51val simp_list_ss = simpLib.++ (list_ss, numSimps.SUC_FILTER_ss); 52 53(****************************************************************************** 54* Simpsets to deal properly with theorems containing SUC 55******************************************************************************) 56val simp_arith_ss = simpLib.++ (arith_ss, numSimps.SUC_FILTER_ss); 57 58(****************************************************************************** 59* Set default parsing to natural numbers rather than integers 60******************************************************************************) 61val _ = intLib.deprecate_int(); 62 63(****************************************************************************** 64* Start a new theory called FinitePath 65******************************************************************************) 66val _ = new_theory "FinitePSLPath"; 67 68(****************************************************************************** 69* Infix list concatenation 70******************************************************************************) 71val _ = set_fixity "<>" (Infixl 500); 72val _ = overload_on ("<>", Term`APPEND`); 73 74(****************************************************************************** 75* Concatenate a list of lists 76******************************************************************************) 77val CONCAT_def = 78 Define `(CONCAT [] = []) /\ (CONCAT(l::ll) = l <> CONCAT ll)`; 79 80(****************************************************************************** 81* HEAD (p0 p1 p2 p3 ...) = p0 82******************************************************************************) 83val HEAD_def = Define `HEAD = list$HD`; 84 85(****************************************************************************** 86* REST (p0 p1 p2 p3 ...) = (p1 p2 p3 ...) 87******************************************************************************) 88val REST_def = Define `REST = list$TL`; 89 90(****************************************************************************** 91* RESTN (p0 p1 p2 p3 ...) n = (pn p(n+1) p(n+2) ...) 92******************************************************************************) 93val RESTN_def = 94 Define `(RESTN p 0 = p) /\ (RESTN p (SUC n) = RESTN (REST p) n)`; 95 96(****************************************************************************** 97* ELEM (p0 p1 p2 p3 ...) n = pn 98******************************************************************************) 99val ELEM_def = Define `ELEM p n = HEAD(RESTN p n)`; 100 101val LENGTH_REST = 102 store_thm 103 ("LENGTH_REST", 104 ``!p. 0 < LENGTH p ==> (LENGTH(REST p) = LENGTH p - 1)``, 105 Cases 106 THEN RW_TAC list_ss [LENGTH,REST_def,LENGTH_CONS, 107 Cooper.COOPER_PROVE``0 < n = ?m. n = SUC m``]); 108 109val LENGTH_TL = 110 store_thm 111 ("LENGTH_TL", 112 ``!l. 0 < LENGTH l ==> (LENGTH(TL l) = LENGTH l - 1)``, 113 Induct 114 THEN RW_TAC list_ss []); 115 116(****************************************************************************** 117* HD(RESTN p i) = EL i p for finite paths 118******************************************************************************) 119val HD_RESTN = 120 store_thm 121 ("HD_RESTN", 122 ``!p. HD(RESTN p i) = EL i p``, 123 Induct_on `i` 124 THEN ASM_SIMP_TAC list_ss [HEAD_def,REST_def,RESTN_def, EL]); 125 126(****************************************************************************** 127* ELEM p i = EL i p for finite paths 128******************************************************************************) 129val ELEM_EL = 130 store_thm 131 ("ELEM_EL", 132 ``!p. ELEM p i = EL i p``, 133 RW_TAC list_ss [ELEM_def,HEAD_def,REST_def,RESTN_def,HD_RESTN]); 134 135val LENGTH_RESTN = 136 store_thm 137 ("LENGTH_RESTN", 138 ``!n p. n < LENGTH p ==> (LENGTH(RESTN p n) = LENGTH p - n)``, 139 Induct 140 THEN RW_TAC arith_ss [LENGTH,RESTN_def,LENGTH_REST]); 141 142val RESTN_TL = 143 store_thm 144 ("RESTN_TL", 145 ``!l i. 0 < i /\ i < LENGTH l ==> (RESTN (TL l) (i-1) = RESTN l i)``, 146 Induct_on `i` 147 THEN RW_TAC list_ss [REST_def,RESTN_def]); 148 149(****************************************************************************** 150* Form needeed for computeLib 151******************************************************************************) 152val RESTN_AUX = 153 store_thm 154 ("RESTN_AUX", 155 ``RESTN p n = if n=0 then p else RESTN (REST p) (n-1)``, 156 Cases_on `n` THEN RW_TAC arith_ss [RESTN_def]); 157 158val _ = computeLib.add_funs[RESTN_AUX]; 159 160(****************************************************************************** 161* SEL_REC m n p = [p(n); p(n+1); ... ; p(n+m)] 162* (Recursive form for easy definition using Define) 163* 164* SEL_REC defined here is a fully specified version of SEG from 165* rich_listTheory. SEG is only partially specified using 166* new_specification. 167******************************************************************************) 168val SEL_REC_def = 169 Define 170 `(SEL_REC 0 n p = []) 171 /\ 172 (SEL_REC (SUC m) 0 p = (HEAD p)::SEL_REC m 0 (REST p)) 173 /\ 174 (SEL_REC (SUC m) (SUC n) p = SEL_REC (SUC m) n (REST p))`; 175 176(****************************************************************************** 177* SEL_REC m n p = [p(n); p(n+1); ... ; p(n+m-1)] 178* (Version for computeLib) 179******************************************************************************) 180val SEL_REC_AUX = 181 store_thm 182 ("SEL_REC_AUX", 183 ``SEL_REC m n p = 184 if m = 0 then [] else 185 if (n = 0) then (HEAD p)::SEL_REC (m-1) 0 (REST p) 186 else SEL_REC m (n-1) (REST p)``, 187 Cases_on `m` THEN Cases_on `n` THEN RW_TAC arith_ss [SEL_REC_def]); 188 189val _ = computeLib.add_funs[SEL_REC_AUX]; 190 191val SEL_REC_SUC = 192 store_thm 193 ("SEL_REC_SUC", 194 ``!p. SEL_REC (SUC m) n p = ELEM p n :: SEL_REC m (SUC n) p``, 195 Induct_on `n` 196 THEN RW_TAC arith_ss [SEL_REC_def,ELEM_def,RESTN_def] 197 THEN Induct_on `m` 198 THEN RW_TAC simp_arith_ss [SEL_REC_def,ELEM_def,RESTN_def]); 199 200(****************************************************************************** 201* SEL p (m,n) = [p m; ... ; p n] 202******************************************************************************) 203val SEL_def = Define `SEL p (m,n) = SEL_REC (n-m+1) m p`; 204 205(****************************************************************************** 206* RESTN (RESTN p m) n = RESTN p (m+n) 207******************************************************************************) 208val RESTN_RESTN = 209 store_thm 210 ("RESTN_RESTN", 211 ``!m n p. RESTN (RESTN p m) n = RESTN p (m+n)``, 212 Induct 213 THEN RW_TAC arith_ss [RESTN_def,arithmeticTheory.ADD_CLAUSES]); 214 215(****************************************************************************** 216* ELEM (RESTN p m) n = ELEM p (m+n) 217******************************************************************************) 218val ELEM_RESTN = 219 store_thm 220 ("ELEM_RESTN", 221 ``!m n p. ELEM (RESTN p m) n = ELEM p (n+m)``, 222 Induct 223 THEN RW_TAC arith_ss [RESTN_def,ELEM_def,RESTN_RESTN]); 224 225(****************************************************************************** 226* CAT(w,p) creates a new path by concatenating w in front of p 227******************************************************************************) 228val CAT_def = 229 Define 230 `(CAT([], p) = p) 231 /\ 232 (CAT((x::w), p) = x :: CAT(w,p))`; 233 234val ALL_EL_F = 235 store_thm 236 ("ALL_EL_F", 237 ``ALL_EL (\x. F) l = (l = [])``, 238 Cases_on `l` 239 THEN RW_TAC list_ss []); 240 241val ALL_EL_CONCAT = 242 store_thm 243 ("ALL_EL_CONCAT", 244 ``!P. ALL_EL (\l. (LENGTH l = 1) /\ P(EL(LENGTH l - 1)l)) ll 245 ==> ALL_EL P (CONCAT ll)``, 246 Induct_on `ll` 247 THEN RW_TAC list_ss [CONCAT_def] 248 THEN RW_TAC list_ss [EVERY_EL,DECIDE``n<1 ==> (n=0)``] 249 THEN ASSUM_LIST(fn thl => ACCEPT_TAC(SIMP_RULE arith_ss [el 4 thl,EL] (el 3 thl)))); 250 251val CONCAT_MAP_SINGLETON = 252 store_thm 253 ("CONCAT_MAP_SINGLETON", 254 ``!ll. CONCAT (MAP (\l. [l]) ll) = ll``, 255 Induct 256 THEN RW_TAC list_ss [CONCAT_def,MAP]); 257 258val LENGTH_EL_MAP_SINGLETON = 259 store_thm 260 ("LENGTH_EL_MAP_SINGLETON", 261 ``!ll n. n < LENGTH ll ==> (LENGTH (EL n (MAP (\l. [l]) ll)) = 1)``, 262 Induct 263 THEN RW_TAC list_ss [MAP] 264 THEN Cases_on `n` 265 THEN RW_TAC list_ss [EL]); 266 267val HD_EL_MAP = 268 store_thm 269 ("HD_EL_MAP", 270 ``!ll n. n < LENGTH ll ==> ((HD (EL n (MAP (\l. [l]) ll))) = EL n ll)``, 271 Induct 272 THEN RW_TAC list_ss [MAP] 273 THEN Cases_on `n` 274 THEN RW_TAC list_ss [EL]); 275 276val EQ_SINGLETON = 277 store_thm 278 ("EQ_SINGLETON", 279 ``(l = [x]) = (x = HD l) /\ (l = [HD l])``, 280 Induct_on `l` 281 THEN ZAP_TAC list_ss []); 282 283val SEL_REC_SPLIT = 284 store_thm 285 ("SEL_REC_SPLIT", 286 ``!n. SEL_REC (m+k) n p = 287 APPEND (SEL_REC k n p) (SEL_REC m (n+k) p)``, 288 Induct_on `k` 289 THEN RW_TAC list_ss [SEL_def,SEL_REC_def,arithmeticTheory.ONE] 290 THEN RW_TAC std_ss [DECIDE ``m + SUC k = SUC(m+k)``, 291 SEL_REC_SUC,APPEND,arithmeticTheory.ADD]); 292 293val SEL_SPLIT = 294 store_thm 295 ("SEL_SPLIT", 296 ``!p k m n. 297 m <= k /\ k < n 298 ==> 299 (SEL p (m,n) = APPEND (SEL p (m,k)) (SEL p (k+1,n)))``, 300 RW_TAC list_ss [SEL_def] 301 THEN IMP_RES_TAC 302 (DECIDE ``m <= k ==> k < n ==> (n + 1 - m = (n-k) + (k+1-m))``) 303 THEN IMP_RES_TAC(DECIDE ``m <= k ==> (k+ 1 = m + (k + 1 - m))``) 304 THEN ASSUM_LIST(fn thl => CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[el 2 thl]))) 305 THEN ASSUM_LIST(fn thl => CONV_TAC(RHS_CONV(RAND_CONV(ONCE_REWRITE_CONV[el 1 thl])))) 306 THEN REWRITE_TAC[SEL_REC_SPLIT]); 307 308val SEL_ELEM = 309 store_thm 310 ("SEL_ELEM", 311 ``!p m. SEL p (m,m) = [ELEM p m]``, 312 Induct_on `m` 313 THEN RW_TAC simp_arith_ss [SEL_def,SEL_REC_def,ELEM_def, 314 RESTN_def, SEL_REC_SUC]); 315 316val APPEND_LAST_CANCEL = 317 store_thm 318 ("APPEND_LAST_CANCEL", 319 ``(APPEND l1 [x1] = APPEND l2 [x2]) = (l1 = l2) /\ (x1 = x2)``, 320 ZAP_TAC list_ss [GSYM SNOC_APPEND,SNOC_11]); 321 322val APPEND_RIGHT_CANCEL = 323 store_thm 324 ("APPEND_RIGHT_CANCEL", 325 ``(APPEND l1 l = APPEND l2 l) = (l1 = l2)``, 326 Induct_on `l` 327 THEN ZAP_TAC list_ss [GSYM SNOC_APPEND,SNOC_11]); 328 329val APPEND_LEFT_CANCEL = 330 store_thm 331 ("APPEND_LEFT_CANCEL", 332 ``(APPEND l l1 = APPEND l l2) = (l1 = l2)``, 333 Induct_on `l` 334 THEN ZAP_TAC list_ss []); 335 336val SEL_APPEND_SINGLETON_IMP = 337 store_thm 338 ("SEL_APPEND_SINGLETON_IMP", 339 ``j > i 340 ==> 341 (SEL p (i,j) = APPEND w [l]) ==> (SEL p (i,j-1) = w) /\ (ELEM p j = l)``, 342 REPEAT DISCH_TAC 343 THEN IMP_RES_TAC(DECIDE ``j > i ==> (i <= (j-1) /\ (j-1) < j)``) 344 THEN IMP_RES_TAC(DECIDE``j:num > i:num ==> (j - 1 + 1 = j)``) 345 THEN IMP_RES_TAC(ISPEC ``p :'a list`` SEL_SPLIT) 346 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 347 THEN ASSUM_LIST(fn thl => ASSUME_TAC(TRANS (GSYM(el 5 thl)) (el 1 thl))) 348 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss [SEL_ELEM,el 3 thl] (el 1 thl))) 349 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [APPEND_LAST_CANCEL]) 350 THEN RW_TAC std_ss []); 351 352val SEL_APPEND_SINGLETON = 353 store_thm 354 ("SEL_APPEND_SINGLETON", 355 ``j > i 356 ==> 357 ((SEL p (i,j) = APPEND w [l]) 358 = 359 (SEL p (i,j-1) = w) /\ (ELEM p j = l))``, 360 REPEAT STRIP_TAC 361 THEN EQ_TAC 362 THEN ZAP_TAC std_ss [SEL_APPEND_SINGLETON_IMP] 363 THEN IMP_RES_TAC(DECIDE ``j > i ==> i <= j - 1 /\ j - 1 < j``) 364 THEN IMP_RES_TAC 365 (ISPECL [``p :'a list``,``j:num-1``,``i:num``,``j:num``] SEL_SPLIT) 366 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 367 THEN IMP_RES_TAC(DECIDE``j:num > i:num ==> (j - 1 + 1 = j)``) 368 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE std_ss [SEL_ELEM,el 1 thl] (el 2 thl))) 369 THEN ZAP_TAC arith_ss [APPEND_LAST_CANCEL,SEL_ELEM]); 370 371val LENGTH_SEL_REC = 372 store_thm 373 ("LENGTH_SEL_REC", 374 ``!m n p. LENGTH(SEL_REC m n p) = m``, 375 Induct_on `m`THEN Induct_on `n` 376 THEN RW_TAC list_ss [SEL_REC_def]); 377 378val LENGTH_SEL = 379 store_thm 380 ("LENGTH_SEL", 381 ``!m n p. LENGTH(SEL p (m,n)) = n-m+1``, 382 RW_TAC arith_ss [SEL_def,SEL_REC_def,LENGTH_SEL_REC]); 383 384val HD_SEL = 385 store_thm 386 ("HD_SEL", 387 ``!i j p. i <= j ==> (HD(SEL p (i,j)) = ELEM p i)``, 388 Induct 389 THEN RW_TAC list_ss 390 [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1, 391 ELEM_def,RESTN_def] 392 THEN IMP_RES_TAC(DECIDE ``SUC i <= j ==> ((SUC (j - SUC i)) = (j-i))``) 393 THEN RW_TAC arith_ss [] 394 THEN ASSUM_LIST 395 (fn thl => 396 ASSUME_TAC 397 (GSYM 398 (Q.GEN `p` 399 (SIMP_RULE arith_ss thl (Q.SPECL [`p`,`i`,`j-1`] SEL_def))))) 400 THEN RW_TAC arith_ss [ELEM_def]); 401 402val HD_SEL0 = 403 store_thm 404 ("HD_SEL0", 405 ``HD(SEL p (0,i)) = HEAD p``, 406 RW_TAC list_ss [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1]); 407 408val TL_SEL_SUC = 409 store_thm 410 ("TL_SEL_SUC", 411 ``!i j p. i <= j ==> (TL(SEL p (i,SUC j)) = SEL (REST p) (i,j))``, 412 Induct 413 THEN RW_TAC list_ss 414 [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1, 415 ELEM_def,RESTN_def] 416 THEN IMP_RES_TAC(DECIDE ``SUC i <= j ==> ((SUC (j - SUC i)) = (j-i))``) 417 THEN RW_TAC arith_ss [] 418 THEN ASSUM_LIST 419 (fn thl => 420 ASSUME_TAC 421 (GSYM 422 (Q.GEN `p` 423 (SIMP_RULE arith_ss thl (Q.SPECL [`p`,`i`,`j`] SEL_def))))) 424 THEN IMP_RES_TAC(DECIDE ``SUC i <= j ==> (SUC (j - i) = j + 1 - i)``) 425 THEN RW_TAC arith_ss [] 426 THEN IMP_RES_TAC(DECIDE ``SUC i <= j ==> i <= j-1``) 427 THEN RES_TAC 428 THEN IMP_RES_TAC(DECIDE ``SUC i <= j ==> (SUC(j-1)=j)``) 429 THEN ASSUM_LIST 430 (fn thl => ASSUME_TAC(SIMP_RULE std_ss [el 1 thl] (el 2 thl))) 431 THEN RW_TAC arith_ss [SEL_def]); 432 433val TL_SEL = 434 store_thm 435 ("TL_SEL", 436 ``!i j p. i < j ==> (TL(SEL p (i,j)) = SEL (REST p) (i,j-1))``, 437 RW_TAC std_ss [] 438 THEN IMP_RES_TAC(DECIDE ``i < j ==> i <= j-1``) 439 THEN IMP_RES_TAC TL_SEL_SUC 440 THEN IMP_RES_TAC(DECIDE ``i < j ==> (SUC(j-1)=j)``) 441 THEN ASSUM_LIST 442 (fn thl => ASSUME_TAC(SIMP_RULE std_ss [el 1 thl] (el 2 thl))) 443 THEN RW_TAC arith_ss []); 444 445val TL_SEL0 = 446 store_thm 447 ("TL_SEL0", 448 ``TL(SEL p (0,SUC i)) = SEL (REST p) (0,i)``, 449 RW_TAC list_ss [SEL_def,SEL_REC_def,GSYM arithmeticTheory.ADD1]); 450 451val EL_SEL_LEMMA = 452 prove 453 (``!m i j p. 454 i <= j /\ m <= j-i ==> (EL m (SEL p (i,j)) = ELEM p (i+m))``, 455 Induct 456 THEN RW_TAC list_ss 457 [SEL_REC_def,ELEM_def,RESTN_def, EL, 458 HD_SEL,TL_SEL,RESTN_def,DECIDE``i + SUC m = SUC(i+m)``]); 459 460val EL_SEL = 461 store_thm 462 ("EL_SEL", 463 ``!i k j p. 464 i <= k ==> k <= j ==> (EL (k-i) (SEL p (i,j)) = ELEM p k)``, 465 RW_TAC arith_ss [EL_SEL_LEMMA]); 466 467val EL_SEL0 = 468 store_thm 469 ("EL_SEL0", 470 ``!j i p. j <= i ==> (EL j (SEL p (0,i)) = ELEM p j)``, 471 Induct 472 THEN RW_TAC list_ss [SEL_REC_def,ELEM_def,RESTN_def,HD_SEL0,EL] 473 THEN Induct_on `i` 474 THEN RW_TAC list_ss [SEL_REC_def,ELEM_def,RESTN_def,TL_SEL0,EL]); 475 476val SEL_REC_REST = 477 store_thm 478 ("SEL_REC_REST", 479 ``!p. SEL_REC m n (REST p) = SEL_REC m (SUC n) p``, 480 Induct_on `m` 481 THEN RW_TAC arith_ss [SEL_REC_def]); 482 483val SEL_REC_RESTN = 484 store_thm 485 ("SEL_REC_RESTN", 486 ``!p. SEL_REC m n (RESTN p r) = SEL_REC m (n + r) p``, 487 Induct_on `r` 488 THEN RW_TAC arith_ss [SEL_REC_def,RESTN_def,arithmeticTheory.ADD_CLAUSES] 489 THEN PROVE_TAC[SEL_REC_REST]); 490 491val SEL_RESTN = 492 store_thm 493 ("SEL_RESTN", 494 ``!p. SEL (RESTN p r) (n,m) = SEL p (r + n, r + m)``, 495 RW_TAC arith_ss [SEL_def,SEL_REC_RESTN]); 496 497val LENGTH1 = 498 store_thm 499 ("LENGTH1", 500 ``(LENGTH l = 1) = ?x. l=[x]``, 501 REWRITE_TAC [arithmeticTheory.ONE] 502 THEN EQ_TAC 503 THEN RW_TAC list_ss [LENGTH,LENGTH_NIL,LENGTH_CONS]); 504 505(****************************************************************************** 506* Some ad hoc lemmas for the rather gross proof that S_CLOCK_COMP works 507******************************************************************************) 508val LENGTH_NIL_LEMMA = 509 store_thm 510 ("LENGTH_NIL_LEMMA", 511 ``LENGTH l >= 1 ==> ~(l = [])``, 512 RW_TAC list_ss [DECIDE``m>=1 = ~(m=0)``,LENGTH_NIL]); 513 514val EL_BUTLAST = 515 store_thm 516 ("EL_BUTLAST", 517 ``!w n. n < PRE(LENGTH w) ==> (EL n (BUTLAST w) = EL n w)``, 518 Induct 519 THEN RW_TAC list_ss [FRONT_DEF] 520 THEN Cases_on `n` 521 THEN RW_TAC list_ss [EL]); 522 523val EL_PRE_LENGTH = 524 store_thm 525 ("EL_PRE_LENGTH", 526 ``!w. LENGTH w >= 1 ==> (EL (LENGTH w - 1) w = LAST w)``, 527 Induct 528 THEN RW_TAC list_ss [] 529 THEN Cases_on `LENGTH w` 530 THEN RW_TAC list_ss [EL,LAST_DEF] 531 THEN IMP_RES_TAC LENGTH_NIL 532 THEN IMP_RES_TAC(SIMP_CONV list_ss [] ``LENGTH [] = SUC n``) 533 THEN RES_TAC 534 THEN FULL_SIMP_TAC arith_ss []); 535 536val EVERY_EL_SINGLETON_LENGTH = 537 store_thm 538 ("EVERY_EL_SINGLETON_LENGTH", 539 ``!wlist P. 540 (!n. n < LENGTH wlist ==> ?l. EL n wlist = [l]) 541 ==> 542 (LENGTH(CONCAT wlist) = LENGTH wlist)``, 543 Induct 544 THEN RW_TAC list_ss [CONCAT_def] 545 THEN ASSUM_LIST 546 (fn thl => 547 ASSUME_TAC(Q.GEN `n` (SIMP_RULE list_ss [EL] (Q.SPEC `SUC n` (el 1 thl))))) 548 THEN ASSUM_LIST 549 (fn thl => 550 STRIP_ASSUME_TAC(SIMP_RULE list_ss [EL] (Q.SPEC `0` (el 2 thl)))) 551 THEN RES_TAC 552 THEN RW_TAC list_ss []); 553 554val EVERY_EL_SINGLETON = 555 store_thm 556 ("EVERY_EL_SINGLETON", 557 ``!wlist P. 558 (!n. n < LENGTH wlist ==> ?l. EL n wlist = [l]) 559 ==> 560 (CONCAT wlist = MAP HD wlist)``, 561 Induct 562 THEN RW_TAC list_ss [CONCAT_def] 563 THEN ASSUM_LIST 564 (fn thl => 565 ASSUME_TAC(Q.GEN `n` (SIMP_RULE list_ss [EL] (Q.SPEC `SUC n` (el 1 thl))))) 566 THEN ASSUM_LIST 567 (fn thl => 568 STRIP_ASSUME_TAC(SIMP_RULE list_ss [EL] (Q.SPEC `0` (el 2 thl)))) 569 THEN RES_TAC 570 THEN RW_TAC list_ss []); 571 572val APPEND_SINGLETON_EQ = 573 store_thm 574 ("APPEND_SINGLETON_EQ", 575 ``(l <> [x] = [y]) = (l = []) /\ (x = y)``, 576 EQ_TAC 577 THEN RW_TAC list_ss [] 578 THEN Cases_on `l` 579 THEN FULL_SIMP_TAC list_ss []); 580 581val APPEND_CONS = 582 store_thm 583 ("APPEND_CONS", 584 ``l1 <> (x :: l2) = (l1 <> [x]) <> l2``, 585 Induct_on `l1` 586 THEN RW_TAC list_ss []); 587 588val SEL_RESTN_EQ0 = 589 store_thm 590 ("SEL_RESTN_EQ0", 591 ``0 < LENGTH w ==> (SEL w (0, LENGTH w - 1) = w)``, 592 RW_TAC list_ss [SEL_def] 593 THEN Induct_on `w` 594 THEN RW_TAC list_ss [SEL_REC_def,HEAD_def,REST_def] 595 THEN Cases_on `w` 596 THEN RW_TAC list_ss [SEL_REC_def]); 597 598val SEL_RESTN_EQ = 599 store_thm 600 ("SEL_RESTN_EQ", 601 ``!w. i < LENGTH w ==> (SEL w (i, LENGTH w - 1) = RESTN w i)``, 602 Induct_on `i` 603 THEN SIMP_TAC std_ss [SEL_RESTN_EQ0,RESTN_def] 604 THEN FULL_SIMP_TAC std_ss [SEL_def] 605 THEN Induct 606 THEN RW_TAC list_ss [SEL_REC_def,HEAD_def,REST_def] 607 THEN Cases_on `w` 608 THEN RW_TAC list_ss [SEL_REC_def] 609 THEN FULL_SIMP_TAC list_ss [DECIDE``(i < 1) = (i = 0)``] 610 THEN RW_TAC simp_list_ss [SEL_REC_def,RESTN_def,HEAD_def] 611 THEN FULL_SIMP_TAC list_ss [DECIDE ``n + 1 - SUC i = n - i``,REST_def] 612 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SIMP_RULE list_ss [] (Q.SPEC `h'::t` (el 3 thl)))) 613 THEN PROVE_TAC[]); 614 615val RESTN_EL = 616 store_thm 617 ("RESTN_EL", 618 ``!i w. i < LENGTH w ==> (RESTN w i = EL i w :: RESTN w (i + 1))``, 619 Induct 620 THEN RW_TAC simp_list_ss [RESTN_def,REST_def,LENGTH_NIL_LEMMA,EL,DECIDE``0 < n = n >= 1``] 621 THENL 622 [PROVE_TAC[LENGTH_NIL_LEMMA,CONS,NULL_EQ_NIL], 623 FULL_SIMP_TAC std_ss 624 [DECIDE``PRE (PRE (SUC i + 1)) = i``, DECIDE ``i+1 = SUC i``, 625 GSYM HEAD_def, GSYM REST_def,GSYM ELEM_EL] 626 THEN FULL_SIMP_TAC std_ss [RESTN_def] 627 THEN ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `REST w` (el 2 thl))) 628 THEN PROVE_TAC[DECIDE``SUC m < n = m < n - 1``, DECIDE``SUC m < n ==> 0 < n``, 629 LENGTH_REST]]); 630 631val LAST_SINGLETON = 632 store_thm 633 ("LAST_SINGLETON", 634 ``!l x. LAST(l <> [x]) = x``, 635 Induct 636 THEN RW_TAC list_ss [LAST_DEF]); 637 638val EL_LAST_SEL = 639 store_thm 640 ("EL_LAST_SEL", 641 ``LAST(SEL w (0,i)) = EL i w``, 642 Cases_on `0 < i` 643 THEN RW_TAC std_ss 644 [SIMP_RULE arith_ss [SEL_ELEM,ELEM_EL] (Q.SPECL[`w`,`n-1`,`0`,`n`]SEL_SPLIT)] 645 THEN RW_TAC std_ss [LAST_SINGLETON] 646 THEN `i=0` by DECIDE_TAC 647 THEN RW_TAC list_ss [SEL_ELEM,ELEM_EL]); 648 649val RESTN_APPEND = 650 store_thm 651 ("RESTN_APPEND", 652 ``!w1 w2. RESTN (w1 <> w2) (LENGTH w1) = w2``, 653 Induct 654 THEN RW_TAC list_ss [RESTN_def,REST_def]); 655 656val FINITE_SEL_REC = 657 store_thm 658 ("FINITE_SEL_REC", 659 ``(SEL_REC 0 n l = []) /\ 660 (SEL_REC (SUC m) 0 (x::l) = x::SEL_REC m 0 l) /\ 661 (SEL_REC (SUC m) (SUC n) (x::l) = SEL_REC (SUC m) n l)``, 662 RW_TAC list_ss [SEL_REC_def,HEAD_def,REST_def]); 663 664(****************************************************************************** 665* SEL_REC on lists is a totally specified extension of SEG. 666* Proofs below extracts theorems about SEG for SEL_REC 667* from rich_listScript.sml sources 668******************************************************************************) 669local open prim_recTheory 670 671val ADD_SUC_lem = 672 let val l = CONJUNCTS ADD_CLAUSES 673 in 674 GEN_ALL (TRANS (el 4 l) (SYM (el 3 l))) 675 end ; 676 677in 678 679val FINITE_SEL_REC_SEL_REC = store_thm("FINITE_SEL_REC_SEL_REC", 680 (``!n1 m1 n2 m2 (l:'a list). 681 (((n1 + m1) <= (LENGTH l)) /\ ((n2 + m2) <= n1)) ==> 682 (SEL_REC n2 m2 (SEL_REC n1 m1 l) = SEL_REC n2 (m1 + m2) l)``), 683 REPEAT numLib.INDUCT_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC 684 THEN REWRITE_TAC[LENGTH,FINITE_SEL_REC,NOT_LESS_0,NOT_SUC_LESS_EQ_0,ADD,ADD_0] 685 THENL[ 686 GEN_TAC THEN REWRITE_TAC[LESS_EQ_MONO,CONS_11] 687 THEN STRIP_TAC THEN SUBST_OCCS_TAC[([3],SYM(SPEC(``0``)ADD_0))] 688 THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[ADD_0], 689 690 REWRITE_TAC[LESS_EQ_MONO,ADD_SUC_lem] THEN STRIP_TAC 691 THEN SUBST_OCCS_TAC[([2],SYM(SPEC(``m2:num``)(CONJUNCT1 ADD)))] 692 THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[ADD_0], 693 694 REWRITE_TAC[LESS_EQ_MONO,ADD_SUC_lem] THEN STRIP_TAC 695 THEN SUBST_OCCS_TAC[([2],SYM(SPEC(``m1:num``)ADD_0))] 696 THEN FIRST_ASSUM MATCH_MP_TAC 697 THEN ASM_REWRITE_TAC[LESS_EQ_MONO,ADD_0], 698 699 PURE_ONCE_REWRITE_TAC[LESS_EQ_MONO] THEN STRIP_TAC 700 THEN FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL[ 701 PURE_ONCE_REWRITE_TAC[GSYM ADD_SUC_lem] 702 THEN FIRST_ASSUM ACCEPT_TAC, 703 ASM_REWRITE_TAC[ADD,LESS_EQ_MONO]]]); 704 705val FINITE_SEL_REC_SUC_CONS = store_thm("FINITE_SEL_REC_SUC_CONS", 706 (``!m n l (x:'a). (SEL_REC m (SUC n) (CONS x l) = SEL_REC m n l)``), 707 numLib.INDUCT_TAC THEN REWRITE_TAC[FINITE_SEL_REC]); 708 709val FINITE_SEL_REC_APPEND = store_thm("FINITE_SEL_REC_APPEND", 710 (``!m (l1:'a list) n l2. (m < LENGTH l1) /\ ((LENGTH l1) <= (n + m)) /\ 711 ((n + m) <= ((LENGTH l1) + (LENGTH l2))) ==> 712 (SEL_REC n m (APPEND l1 l2) = 713 APPEND (SEL_REC ((LENGTH l1) - m) m l1) (SEL_REC ((n + m)-(LENGTH l1)) 0 l2))``), 714 numLib.INDUCT_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC 715 THEN REPEAT (FILTER_GEN_TAC (``n:num``)) 716 THEN numLib.INDUCT_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC 717 THEN REPEAT GEN_TAC 718 THEN REWRITE_TAC[LENGTH,FINITE_SEL_REC,NOT_LESS_0,NOT_SUC_LESS_EQ_0,ADD,ADD_0,SUB_0] 719 THEN REWRITE_TAC 720 [LESS_EQ_MONO,SUB_0,SUB_MONO_EQ,APPEND,FINITE_SEL_REC,NOT_SUC_LESS_EQ_0,CONS_11] 721 THEN RULE_ASSUM_TAC (REWRITE_RULE[ADD_0,SUB_0]) 722 THENL[ 723 DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) 724 THEN POP_ASSUM (SUBST1_TAC o (MATCH_MP LESS_EQUAL_ANTISYM)) 725 THEN REWRITE_TAC[FINITE_SEL_REC,APPEND_NIL,SUB_EQUAL_0], 726 STRIP_TAC THEN DISJ_CASES_TAC (SPEC (``LENGTH (l1:'a list)``)LESS_0_CASES) 727 THENL[ 728 POP_ASSUM (ASSUME_TAC o SYM) THEN IMP_RES_TAC LENGTH_NIL 729 THEN ASM_REWRITE_TAC[APPEND,FINITE_SEL_REC,SUB_0], 730 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[LENGTH]], 731 DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) 732 THEN POP_ASSUM (SUBST1_TAC o (MATCH_MP LESS_EQUAL_ANTISYM)) 733 THEN REWRITE_TAC[FINITE_SEL_REC,APPEND_NIL,SUB_EQUAL_0], 734 REWRITE_TAC[LESS_MONO_EQ,GSYM NOT_LESS] THEN STRIP_TAC THEN RES_TAC, 735 DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) 736 THEN POP_ASSUM (SUBST1_TAC o (MATCH_MP LESS_EQUAL_ANTISYM)) 737 THEN REWRITE_TAC[FINITE_SEL_REC,APPEND_NIL,SUB_EQUAL_0] 738 THEN REWRITE_TAC[ADD_SUC_lem,ADD_SUB,FINITE_SEL_REC], 739 REWRITE_TAC[LESS_MONO_EQ,FINITE_SEL_REC_SUC_CONS] THEN STRIP_TAC 740 THEN PURE_ONCE_REWRITE_TAC[ADD_SUC_lem] 741 THEN FIRST_ASSUM MATCH_MP_TAC 742 THEN ASM_REWRITE_TAC[GSYM ADD_SUC_lem,LENGTH]]); 743 744end; 745 746val SEL_APPEND = 747 store_thm 748 ("SEL_APPEND", 749 ``!m n w1 w2. 750 m < LENGTH w1 /\ LENGTH w1 <= n /\ 751 n + 1 <= LENGTH w1 + LENGTH w2 ==> 752 (SEL (w1 <> w2) (m,n) = 753 SEL w1 (m, LENGTH w1 - 1) <> SEL w2 (0, n - LENGTH w1))``, 754 RW_TAC list_ss 755 [SEL_def,DISCH_ALL 756 (SIMP_RULE arith_ss 757 [ASSUME``m<=n``] (Q.SPECL[`m`,`w1`,`n-m+1`,`w2`]FINITE_SEL_REC_APPEND))]); 758 759val SEL_APPEND_COR = 760 save_thm 761 ("SEL_APPEND_COR", 762 SIMP_RULE arith_ss [SEL_ELEM,ELEM_EL] (Q.SPECL[`0`,`list$LENGTH w1`,`w1`,`w2`]SEL_APPEND)); 763 764val RESTN_LENGTH = 765 store_thm 766 ("RESTN_LENGTH", 767 ``!w. RESTN w (LENGTH w) = []``, 768 Induct 769 THEN RW_TAC list_ss [RESTN_def,REST_def]); 770 771val _ = export_theory(); 772