1 2(*****************************************************************************) 3(* Simple example encoding part of Johan's April 15, 2004 message *) 4(* (with changes for fusion from later messages, and proof hints from Johan) *) 5(* *) 6(* UPDATES: *) 7(* END changed by Johan Martensson Mon Apr 26 2004 *) 8(*****************************************************************************) 9 10(*****************************************************************************) 11(* Load in useful stuff *) 12(*****************************************************************************) 13quietdec := true; (* Switch off output *) 14map load 15 ["intLib", "Cooper","rich_listTheory"]; (* Load useful theories *) 16intLib.deprecate_int(); (* Set num as default numbers type *) 17open rich_listTheory; (* Open theories *) 18quietdec := false; (* Restore output *) 19 20(*****************************************************************************) 21(* N^f = { w | w is a finite list of states/letters } (the set of neutral *) 22(* finite words) *) 23(* *) 24(* we let \epsilon be the empty (neutral) word *) 25(* *) 26(* W = { W(w) | w \in N^f } (the set of weak finite words) *) 27(* *) 28(* Let A = N^f U W *) 29(*****************************************************************************) 30 31(*****************************************************************************) 32(* Here is a datatype definition of a type A (hopefully self-explanatory). *) 33(* It creates a tagged disjoint union with elements ``N l`` and ``W l``, *) 34(* where l is a HOL list (a pre-defined datatype). *) 35(*****************************************************************************) 36val A_def = 37 Hol_datatype 38 `A = N of 'a list 39 | W of 'a list`; 40 41(*****************************************************************************) 42(* Retrieve from data-base (DB) automatically proved theorems about A *) 43(*****************************************************************************) 44val A_11 = assoc "A_11" (DB.theorems "-") 45and A_distinct = assoc "A_distinct" (DB.theorems "-"); 46 47val ELEM_def = 48 Define 49 `(ELEM (N l) n = EL n l) 50 /\ 51 (ELEM (W l) n = EL n l) `; 52 53(*****************************************************************************) 54(* We define concatenation ( * ) on A: if v,w \in N then v*w is just the *) 55(* list concatenation of v and w (remember v,w finite) v*W(w) = W(v*w) *) 56(* and for v\in W and w\in A v*w = v *) 57(*****************************************************************************) 58 59(*****************************************************************************) 60(* For readability overload "++" onto HOL's list append constant APPEND, *) 61(* and make it a left associative infix with precedence 500. *) 62(*****************************************************************************) 63set_fixity "++" (Infixl 500); 64overload_on("++", ``APPEND``); 65 66(*****************************************************************************) 67(* Define ``CONC`` for concatenation on values of type A. *) 68(*****************************************************************************) 69set_fixity "CONC" (Infixl 500); 70 71val CONC_def = 72 Define 73 `(N v CONC N w = N(v++w)) 74 /\ 75 (N v CONC W w = W(v++w)) 76 /\ 77 (W v CONC a = W v)`; 78 79(*****************************************************************************) 80(* Overload "*" on to "CONC" for readability. *) 81(*****************************************************************************) 82overload_on("*", ``$CONC``); 83 84(*****************************************************************************) 85(* We want to show that A is closed under *, that * is associative on A and *) 86(* that \epsilon is the identity for this operation. *) 87(*****************************************************************************) 88val CONC_identity = 89 prove 90 (``(N[] * a = a) /\ (a * N[] = a)``, 91 Cases_on `a` 92 THEN RW_TAC list_ss [CONC_def]); 93 94val CONC_assoc = 95 prove 96 (``a * (b * c) = (a * b) * c``, 97 Cases_on `a` THEN Cases_on `b` THEN Cases_on `c` 98 THEN RW_TAC list_ss [CONC_def]); 99 100val ASSOC_CONC = 101 prove 102 (``ASSOC $*``, 103 RW_TAC std_ss [operatorTheory.ASSOC_DEF,CONC_assoc]); 104 105(*****************************************************************************) 106(* for w \in N |w| is the number of elements in w, and |W(w)| = |w| *) 107(*****************************************************************************) 108 109(*****************************************************************************) 110(* Represent |w| by LEN w. HOL's built-in length function on lists *) 111(* is LENGTH. *) 112(*****************************************************************************) 113val LEN_def = 114 Define 115 `(LEN(N w) = LENGTH w) 116 /\ 117 (LEN(W w) = LENGTH w)`; 118 119(*****************************************************************************) 120(* we want to show that if w \in N then *) 121(* |w*v| = |w|+|v| and *) 122(* |W(w)*v| = |w| *) 123(*****************************************************************************) 124val LEN = 125 prove 126 (``(LEN(N w * a) = LEN(N w) + LEN a) 127 /\ 128 (LEN(W w * a) = LEN(W w))``, 129 Cases_on `a` 130 THEN RW_TAC list_ss [LEN_def,CONC_def]); 131 132(*****************************************************************************) 133(* We define (on A) w<=v (prefix) if there is u \in A such that w*u=v *) 134(*****************************************************************************) 135val PREFIX_def = Define `PREFIX w v = ?u. w*u = v`; 136 137val STRICT_PREFIX_def = Define `STRICT_PREFIX w v = PREFIX w v /\ ~(w = v)`; 138 139(*****************************************************************************) 140(* u<w is u is prefix of w and u/=w *) 141(* One could try to prove that if u<w u is neutral *) 142(*****************************************************************************) 143 144val STRICT_PREFIX_NEUTRAL = 145 prove 146 (``STRICT_PREFIX u w ==> ?l. u = N l``, 147 Cases_on `u` THEN Cases_on `w` 148 THEN RW_TAC list_ss [STRICT_PREFIX_def,PREFIX_def,CONC_def]); 149 150(*****************************************************************************) 151(* We also define W(w)^k = w^k *) 152(*****************************************************************************) 153val ELEM_def = 154 Define 155 `(ELEM (N l) n = EL n l) 156 /\ 157 (ELEM (W l) n = EL n l) `; 158 159(*****************************************************************************) 160(* The problem with fusion is that if w is a weak word that matches *) 161(* the beginning (but not the whole of) r1, then w should match r1:r2, so *) 162(* we need to see to it that the definition doesn't require that l matches *) 163(* the beginning of r2 in this case. *) 164(* *) 165(* This is the point of the end operator. We define for w \in N *) 166(* *) 167(* end(w) = \epsilon *) 168(* end(W(w)) = W(\epsilon) *) 169(*****************************************************************************) 170val END_def = 171 Define 172 `(END(N w) = N[]) 173 /\ 174 (END(W w) = W[])`; 175 176(*****************************************************************************) 177(* Now we can use it to turn on/turn off words because *) 178(* *) 179(* end(v)*w = w but *) 180(* end(W(v))*w = W(\epsilon) *) 181(*****************************************************************************) 182val END = 183 prove 184 (``!v w. (END(N v) * w = w) /\ (END(W v) * w = W[])``, 185 GEN_TAC 186 THEN Cases_on `w` 187 THEN RW_TAC list_ss [LEN_def,CONC_def,END_def]); 188 189(*****************************************************************************) 190(* We can now define tight satisfaction: *) 191(* w,v and u are finite neutral or weak words. *) 192(* (definition below incorporates fusion from later message) *) 193(* *) 194(* w|==. b <=> w=\epsilon^- or (w \in N and |w|=1 and w^0||=b) *) 195(* w|==. r1;r2 <=> *) 196(* there exist v,u s.t. v*u=w and v|==. r1 and u|==. r2 *) 197(* w|==. r1:r2 <=> *) 198(* there exist v,u \in A and l s.t. v*l*u=w and v*l|==. r1 *) 199(* and end(v)*l*u|==. r2 *) 200(* w|==. r1&r2 <=> w|==. r1 and w|==. r2 *) 201(* w|==. r1|r2 <=> w|==. r1 or w|==. r2 *) 202(* w|==. r* <=> either w=\epsilon or there exists w1,w2,..wn such that *) 203(* w=*(w1w2..wn)=w1*w2*..*wn *) 204(* and forall 1<=k<=n wk|==. r *) 205(*****************************************************************************) 206 207(*****************************************************************************) 208(* Boolean expressions *) 209(*****************************************************************************) 210val bexp_def = 211 Hol_datatype 212 `bexp = B_PROP of 'a (* atomic proposition *) 213 | B_NOT of bexp (* negation *) 214 | B_AND of bexp # bexp`; (* conjunction *) 215 216(*****************************************************************************) 217(* B_SEM l b means "l |= b" where l is a letter, i.e. l : 'prop -> bool *) 218(*****************************************************************************) 219val B_SEM_def = 220 Define 221 `(B_SEM l (B_PROP(p:'prop)) = p IN l) 222 /\ 223 (B_SEM l (B_NOT b) = ~(B_SEM l b)) 224 /\ 225 (B_SEM l (B_AND(b1,b2)) = B_SEM l b1 /\ B_SEM l b2)`; 226 227(*****************************************************************************) 228(* Syntax of Sequential Extended Regular Expressions (SEREs) *) 229(*****************************************************************************) 230val sere_def = 231 Hol_datatype 232 `sere = S_BOOL of 'a bexp (* boolean expression *) 233 | S_CAT of sere # sere (* r1 ; r2 *) 234 | S_FUSION of sere # sere (* r1 : r2 *) 235 | S_OR of sere # sere (* r1 | r2 *) 236 | S_AND of sere # sere (* r1 && r2 *) 237 | S_REPEAT of sere`; (* r[*] *) 238 239(*****************************************************************************) 240(* Structural induction rule for SEREs *) 241(*****************************************************************************) 242val sere_induct = save_thm 243 ("sere_induct", 244 Q.GEN 245 `P` 246 (MATCH_MP 247 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 248 (SIMP_RULE 249 std_ss 250 [pairTheory.FORALL_PROD, 251 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 252 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 253 (Q.SPECL 254 [`P`,`\(r1,r2). P r1 /\ P r2`] 255 (TypeBase.induction_of "sere"))))); 256 257(*****************************************************************************) 258(* Some auxiliary definitions *) 259(*****************************************************************************) 260val IS_WEAK_def = Define `(IS_WEAK (W w) = T) /\ (IS_WEAK (N w) = F)` 261and IS_NEUTRAL_def = Define `(IS_NEUTRAL (W w) = F) /\ (IS_NEUTRAL (N w) = T)`; 262 263val IS_LETTER_def = 264 Define 265 `(IS_LETTER(N w) = ?l. w = [l]) 266 /\ 267 (IS_LETTER(W w) = ?l. w = [l])`; 268 269(*****************************************************************************) 270(* Semantics of SEREs *) 271(*****************************************************************************) 272val US_SEM_def = 273 Define 274 `(US_SEM v (S_BOOL b) = (IS_WEAK v /\ (LEN v = 0)) 275 \/ 276 (IS_NEUTRAL v /\ (LEN v = 1) /\ B_SEM (ELEM v 0) b)) 277 /\ 278 (US_SEM v (S_CAT(r1,r2)) = 279 ?v1 v2. (v = v1 * v2) /\ US_SEM v1 r1 /\ US_SEM v2 r2) 280 /\ 281 (US_SEM v (S_FUSION(r1,r2)) = 282 ?v1 v2 l. IS_LETTER l /\ (v = v1*l*v2) 283 /\ 284 US_SEM (v1*l) r1 /\ US_SEM (END(v1)*l*v2) r2) 285 /\ 286 (US_SEM v (S_OR(r1,r2)) = 287 US_SEM v r1 \/ US_SEM v r2) 288 /\ 289 (US_SEM v (S_AND(r1,r2)) = 290 US_SEM v r1 /\ US_SEM v r2) 291 /\ 292 (US_SEM v (S_REPEAT r) = 293 ?vlist. (v = FOLDL $* (N[]) vlist) /\ EVERY (\v. US_SEM v r) vlist)`; 294 295(*****************************************************************************) 296(* We can now prove with fusion in the language *) 297(* for all r: W(\espilon)|==.r *) 298(*****************************************************************************) 299local 300val S_SEM_SIMP_TAC = 301 RW_TAC list_ss [US_SEM_def,IS_WEAK_def,IS_NEUTRAL_def,LEN_def,ELEM_def] 302in 303val TightTrueEmpty = 304 prove 305 (``!r. US_SEM (W[]) r``, 306 INDUCT_THEN sere_induct ASSUME_TAC 307 THENL 308 [(* S_BOOL b *) 309 S_SEM_SIMP_TAC, 310 (* S_CAT (r,r') *) 311 S_SEM_SIMP_TAC 312 THEN Q.EXISTS_TAC `W []` 313 THEN Q.EXISTS_TAC `W []` 314 THEN RW_TAC list_ss [CONC_def], 315 (* S_FUSION (r,r') *) 316 S_SEM_SIMP_TAC 317 THEN Q.EXISTS_TAC `W []` 318 THEN Q.EXISTS_TAC `W []` 319 THEN Q.EXISTS_TAC `W [b]` 320 THEN RW_TAC list_ss [CONC_def,END,IS_LETTER_def], 321 (* S_OR (r,r') *) 322 S_SEM_SIMP_TAC, 323 (* S_AND (r,r') *) 324 S_SEM_SIMP_TAC, 325 (* S_REPEAT (r,r') *) 326 S_SEM_SIMP_TAC 327 THEN Q.EXISTS_TAC `[W []]` 328 THEN RW_TAC list_ss [CONC_def]]) 329end; 330 331(*****************************************************************************) 332(* Weaken a word *) 333(*****************************************************************************) 334val WEAKEN_def = Define `(WEAKEN(N l) = W l) /\ (WEAKEN(W l) = W l)`; 335 336val WEAKEN = 337 prove 338 (``(IS_WEAK(WEAKEN w) = T) /\ (IS_NEUTRAL(WEAKEN w) = F)``, 339 Cases_on `w` 340 THEN RW_TAC list_ss [IS_WEAK_def,IS_NEUTRAL_def,WEAKEN_def]); 341 342val LEN_WEAKEN = 343 prove 344 (``LEN(WEAKEN w) = LEN w``, 345 Cases_on `w` 346 THEN RW_TAC list_ss [WEAKEN_def,LEN_def]); 347 348(*****************************************************************************) 349(* Tight prefix theorem *) 350(* w|==.r and u<w => W(u)|==.r *) 351(*****************************************************************************) 352val APPEND_EQ_NIL = 353 prove 354 (``!l1 l2. (LENGTH(l1++l2) = 0) ==> (l1 = []) /\ (l2 = [])``, 355 Induct 356 THEN RW_TAC list_ss [] 357 THEN `LENGTH l2 = 0` by DECIDE_TAC 358 THEN PROVE_TAC[LENGTH_NIL]); 359 360val APPEND_EQ_SINGLETON = 361 prove 362 (``!l1 l2. (LENGTH(l1++l2) = 1) ==> (l1 = []) \/ (l2 = [])``, 363 Induct 364 THEN RW_TAC list_ss [] 365 THEN `LENGTH l2 = 0` by DECIDE_TAC 366 THEN PROVE_TAC[LENGTH_NIL]); 367 368val APPEND_NIL_CANCEL = 369 prove 370 (``!l1 l2. (l1++l2 = l1) ==> (l2 = [])``, 371 Induct 372 THEN RW_TAC list_ss []); 373 374val PREFIX_CONC = 375 prove 376 (``PREFIX u v1 ==> !v2. PREFIX u (v1 * v2)``, 377 Cases_on `u` THEN Cases_on `v1` 378 THEN RW_TAC list_ss [PREFIX_def,CONC_def] 379 THEN Cases_on `u` THEN Cases_on `v2` 380 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct] 381 THENL 382 [Q.EXISTS_TAC `N(l''++l''')` 383 THEN RW_TAC list_ss [CONC_def], 384 Q.EXISTS_TAC `W(l''++l''')` 385 THEN RW_TAC list_ss [CONC_def]]); 386 387(*****************************************************************************) 388(* Not sure if this is needed *) 389(*****************************************************************************) 390val STRICT_PREFIX_CONC = 391 prove 392 (``STRICT_PREFIX u v1 ==> !v2. STRICT_PREFIX u (v1 * v2)``, 393 Cases_on `u` THEN Cases_on `v1` 394 THEN RW_TAC list_ss [STRICT_PREFIX_def,PREFIX_def,CONC_def] 395 THEN Cases_on `u` THEN Cases_on `v2` 396 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct] 397 THENL 398 [Q.EXISTS_TAC `N(l''++l''')` 399 THEN RW_TAC list_ss [CONC_def], 400 Q.EXISTS_TAC `W(l''++l''')` 401 THEN RW_TAC list_ss [CONC_def], 402 Cases_on `l = l' ++ l'''` 403 THEN RW_TAC list_ss [] 404 THEN `l''' ++ l'' = []` by PROVE_TAC[APPEND_ASSOC,APPEND_NIL_CANCEL] 405 THEN `(l''' = []) /\ (l'' = [])` by PROVE_TAC[APPEND_EQ_NIL,LENGTH_NIL] 406 THEN RW_TAC list_ss [] 407 THEN FULL_SIMP_TAC list_ss []]); 408 409val HD_APPEND = 410 prove 411 (``!v1 v2. ~(v1 = []) ==> (HD(APPEND v1 v2) = HD v1)``, 412 Induct 413 THEN RW_TAC list_ss []); 414 415val TL_APPEND = 416 prove 417 (``!v1 v2. ~(v1 = []) ==> (TL(APPEND v1 v2) = APPEND (TL v1) v2)``, 418 Induct 419 THEN RW_TAC list_ss []); 420 421val LIST_TRICHOTOMY_LEMMA1 = 422 prove 423 (``~(v = []) ==> (h::u ++ u' = v ++ v') ==> (h = HD v) /\ (u ++ u' = TL v ++ v')``, 424 RW_TAC list_ss [] 425 THEN PROVE_TAC[HD,HD_APPEND,TL,TL_APPEND]); 426 427val LIST_TRICHOTOMY_LEMMA2 = 428 prove 429 (``~(v = []) ==> (!w. ~(HD v::u ++ w = v)) ==> !w. ~(u ++ w = TL v)``, 430 RW_TAC list_ss [] 431 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 432 THEN Cases_on `~(u ++ w = TL v)` 433 THEN FULL_SIMP_TAC list_ss [] 434 THEN `HD v :: u ++ w = HD v :: TL v` by PROVE_TAC[] 435 THEN `~(NULL v)` by PROVE_TAC[NULL_EQ_NIL] 436 THEN FULL_SIMP_TAC std_ss [CONS] 437 THEN RES_TAC); 438 439val LIST_TRICHOTOMY_LEMMA3 = 440 prove 441 (``!u v. 442 (u ++ u' = v ++ v') /\ (!w. ~(u ++ w = v)) 443 ==> 444 ?w. v ++ w = u``, 445 Induct 446 THEN RW_TAC list_ss [] 447 THEN Cases_on `v=[]` 448 THEN RW_TAC list_ss [] 449 THEN IMP_RES_TAC LIST_TRICHOTOMY_LEMMA1 450 THEN RW_TAC list_ss [] 451 THEN `TL(HD v::u ++ u') = TL(v ++ v')` by PROVE_TAC[] 452 THEN FULL_SIMP_TAC list_ss [] 453 THEN IMP_RES_TAC LIST_TRICHOTOMY_LEMMA2 454 THEN RES_TAC 455 THEN `HD v :: TL v ++ w = HD v :: u` by PROVE_TAC[] 456 THEN PROVE_TAC[APPEND,CONS,NULL_EQ_NIL]); 457 458val LIST_TRICHOTOMY = 459 prove 460 (``!u v. 461 (?u' v'. u ++ u' = v ++ v') 462 ==> 463 (?w. u ++ w = v) \/ (?w. v ++ w = u)``, 464 RW_TAC list_ss [] 465 THEN Cases_on `(?w. u ++ w = v)` (* u<=v *) 466 THEN RW_TAC list_ss [] 467 THEN FULL_SIMP_TAC list_ss [] 468 THEN Induct_on `u` 469 THEN RW_TAC list_ss [] 470 THEN PROVE_TAC[LIST_TRICHOTOMY_LEMMA3,APPEND]); 471 472val PREFIX_TRICHOTOMY = 473 prove 474 (``!v1 v2 w. 475 PREFIX v1 w /\ PREFIX v2 w ==> STRICT_PREFIX v1 v2 \/ PREFIX v2 v1``, 476 REPEAT GEN_TAC 477 THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `w` 478 THEN RW_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def] 479 THEN Cases_on `u` THEN Cases_on `u'` 480 THEN FULL_SIMP_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def,A_11,A_distinct] 481 THEN Cases_on `?u. l' ++ u = l` 482 THEN FULL_SIMP_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def,A_11,A_distinct] 483 THEN ZAP_TAC list_ss [CONC_def,A_11] 484 THEN Cases_on `?u. l++u = l'` 485 THEN ZAP_TAC list_ss [CONC_def,A_11] 486 THEN FULL_SIMP_TAC list_ss [] 487 THEN IMP_RES_TAC LIST_TRICHOTOMY 488 THEN RES_TAC); 489 490val PREFIX_REFL = 491 prove 492 (``!v. PREFIX v v``, 493 Induct 494 THEN RW_TAC list_ss [PREFIX_def,CONC_def] 495 THEN Q.EXISTS_TAC `N[]` 496 THEN RW_TAC list_ss [CONC_def]); 497 498val APPEND_LEFT_CANCEL = 499 store_thm 500 ("APPEND_LEFT_CANCEL", 501 ``(APPEND l l1 = APPEND l l2) = (l1 = l2)``, 502 Induct_on `l` 503 THEN ZAP_TAC list_ss []); 504 505val PREFIX_CANCEL = 506 prove 507 (``(PREFIX (N(u ++ v1)) (N(u ++ v2)) ==> PREFIX (N v1) (N v2)) /\ 508 (PREFIX (W(u ++ v1)) (N(u ++ v2)) ==> PREFIX (W v1) (N v2)) /\ 509 (PREFIX (N(u ++ v1)) (W(u ++ v2)) ==> PREFIX (N v1) (W v2)) /\ 510 (PREFIX (W(u ++ v1)) (W(u ++ v2)) ==> PREFIX (W v1) (W v2))``, 511 RW_TAC list_ss [PREFIX_def,CONC_def] 512 THEN Cases_on `u'` 513 THEN FULL_SIMP_TAC std_ss 514 [GSYM APPEND_ASSOC,CONC_def,A_11,A_distinct,APPEND_LEFT_CANCEL] 515 THEN PROVE_TAC[CONC_def]); 516 517val STRICT_PREFIX_CANCEL = 518 prove 519 (``(STRICT_PREFIX (N(u ++ v1)) (N(u ++ v2)) ==> STRICT_PREFIX (N v1) (N v2)) /\ 520 (STRICT_PREFIX (W(u ++ v1)) (N(u ++ v2)) ==> STRICT_PREFIX (W v1) (N v2)) /\ 521 (STRICT_PREFIX (N(u ++ v1)) (W(u ++ v2)) ==> STRICT_PREFIX (N v1) (W v2)) /\ 522 (STRICT_PREFIX (W(u ++ v1)) (W(u ++ v2)) ==> STRICT_PREFIX (W v1) (W v2))``, 523 RW_TAC list_ss [STRICT_PREFIX_def] 524 THEN PROVE_TAC[PREFIX_CANCEL]); 525 526val B_FALSE_def = 527 Define `B_FALSE = B_AND(B_PROP ARB, B_NOT(B_PROP ARB))`; 528 529val B_FALSE = 530 prove 531 (``B_SEM v B_FALSE = F``, 532 RW_TAC list_ss [B_FALSE_def,B_SEM_def]); 533 534val IS_WEAK_LEN_0 = 535 prove 536 (``!v. IS_WEAK v /\ (LEN v = 0) = (v = W[])``, 537 Induct 538 THEN RW_TAC list_ss [IS_WEAK_def,LEN_def,LENGTH_NIL]); 539 540val FOLDL_W_NIL = 541 prove 542 (``!l. ALL_EL (\v. v = W []) l ==> (FOLDL $* (W []) l = W[])``, 543 Induct 544 THEN RW_TAC list_ss [CONC_def]); 545 546val FOLDL_N_NIL = 547 prove 548 (``!l. ~(l = []) ==> ALL_EL (\v. v = W []) l ==> (FOLDL $* (N []) l = W[])``, 549 Induct 550 THEN RW_TAC list_ss [CONC_def,FOLDL_W_NIL]); 551 552val S_CATN_def = 553 Define 554 `(S_CATN 0 r = r) /\ (S_CATN (SUC n) r = S_CAT(r, S_CATN n r))`; 555 556val ASSOC_FOLDL = 557 prove 558 (``!l x y. ASSOC f ==> (FOLDL f (f x y) l = f x (FOLDL f y l))``, 559 Induct 560 THEN RW_TAC list_ss [operatorTheory.ASSOC_DEF]); 561 562val FOLDL_CONCAT_N = 563 prove 564 (``!vlist v. FOLDL $* v vlist = v * FOLDL $* (N []) vlist``, 565 PROVE_TAC[ASSOC_FOLDL,ASSOC_CONC,CONC_identity]); 566 567 val US_SEM_CAT_REPEAT_CATN = 568 store_thm 569 ("US_SEM_CAT_REPEAT_CATN", 570 ``!v r. US_SEM v (S_CAT(S_REPEAT r, r)) = ?n. US_SEM v (S_CATN n r)``, 571 RW_TAC list_ss [US_SEM_def] 572 THEN EQ_TAC 573 THEN RW_TAC list_ss [] 574 THENL 575 [Induct_on `vlist` 576 THEN RW_TAC list_ss [CONC_identity,S_CATN_def,US_SEM_def] 577 THEN ZAP_TAC std_ss [S_CATN_def] 578 THEN RW_TAC std_ss [] 579 THEN RES_TAC 580 THEN Q.EXISTS_TAC `SUC n` 581 THEN RW_TAC list_ss [S_CATN_def,US_SEM_def] 582 THEN Q.EXISTS_TAC `h` THEN Q.EXISTS_TAC `FOLDL $* (N []) vlist * v2` 583 THEN RW_TAC std_ss [] 584 THEN PROVE_TAC[FOLDL_CONCAT_N,CONC_assoc], 585 Q.UNDISCH_TAC `US_SEM v (S_CATN n r)` 586 THEN Q.SPEC_TAC(`v`,`v`) 587 THEN Q.SPEC_TAC(`r`,`r`) 588 THEN Q.SPEC_TAC(`n`,`n`) 589 THEN Induct 590 THEN RW_TAC list_ss [S_CATN_def] 591 THENL 592 [Q.EXISTS_TAC `N[]` THEN Q.EXISTS_TAC `v` 593 THEN RW_TAC list_ss [CONC_identity] 594 THEN Q.EXISTS_TAC `[]` 595 THEN RW_TAC list_ss [], 596 FULL_SIMP_TAC list_ss [US_SEM_def] 597 THEN RES_TAC 598 THEN RW_TAC std_ss [] 599 THEN Q.EXISTS_TAC `v1 * FOLDL $* (N []) vlist` THEN Q.EXISTS_TAC `v2'` 600 THEN RW_TAC std_ss [CONC_assoc] 601 THEN Q.EXISTS_TAC `v1::vlist` 602 THEN RW_TAC list_ss [CONC_identity] 603 THEN PROVE_TAC[FOLDL_CONCAT_N]]]); 604 605val FOLDLN_def = 606 Define 607 `(FOLDLN 0 f e l = e) /\ 608 (FOLDLN (SUC n) f e l = FOLDLN n f (f e (HD l)) (TL l))`; 609 610val FOLDLN_LENGTH = 611 prove 612 (``!l f e. FOLDLN (LENGTH l) f e l = FOLDL f e l``, 613 Induct 614 THEN RW_TAC list_ss [FOLDLN_def]); 615 616val FOLDLN_ASSOC = 617 prove 618 (``!n v1 v2 l. FOLDLN n $* (v1 * v2) l = v1 * FOLDLN n $* v2 l``, 619 Induct 620 THEN RW_TAC list_ss [FOLDLN_def,CONC_assoc]); 621 622val FOLDLN_CATN = 623 prove 624 (``!l v0 r. 625 ALL_EL (\v. US_SEM v r) l /\ US_SEM v0 r 626 ==> 627 !n. n <= LENGTH l ==> US_SEM (FOLDLN n $* v0 l) (S_CATN n r)``, 628 Induct 629 THEN RW_TAC list_ss [FOLDLN_def,S_CATN_def] 630 THEN Cases_on `n = 0` 631 THEN RW_TAC list_ss [FOLDLN_def,S_CATN_def] 632 THEN `?m. n = SUC m` by Cooper.COOPER_TAC 633 THEN RW_TAC list_ss [FOLDLN_def,S_CATN_def] 634 THEN FULL_SIMP_TAC arith_ss [US_SEM_def] 635 THEN RES_TAC 636 THEN Q.EXISTS_TAC `v0` 637 THEN Q.EXISTS_TAC `FOLDLN m $* h l` 638 THEN RW_TAC list_ss [FOLDLN_ASSOC]); 639 640 val US_SEM_REPEAT_CATN = 641 store_thm 642 ("US_SEM_REPEAT_CATN", 643 ``!v r. US_SEM v (S_REPEAT r) = (v = N[]) \/ ?n. US_SEM v (S_CATN n r)``, 644 RW_TAC list_ss [] 645 THEN EQ_TAC 646 THENL 647 [SIMP_TAC list_ss[US_SEM_def] 648 THEN REPEAT STRIP_TAC 649 THEN Cases_on `v = N[]` 650 THEN ASM_REWRITE_TAC[] 651 THEN Cases_on `vlist` 652 THEN FULL_SIMP_TAC list_ss [CONC_identity] 653 THEN RES_TAC 654 THEN `LENGTH t <= LENGTH t` by DECIDE_TAC 655 THEN IMP_RES_TAC FOLDLN_CATN 656 THEN Q.EXISTS_TAC `LENGTH t` 657 THEN FULL_SIMP_TAC list_ss [FOLDLN_LENGTH], 658 RW_TAC list_ss [US_SEM_def] 659 THENL 660 [Q.EXISTS_TAC `[]` 661 THEN RW_TAC list_ss [], 662 Q.UNDISCH_TAC `US_SEM v (S_CATN n r)` 663 THEN Q.SPEC_TAC(`v`,`v`) 664 THEN Q.SPEC_TAC(`r`,`r`) 665 THEN Q.SPEC_TAC(`n`,`n`) 666 THEN Induct 667 THEN RW_TAC list_ss [S_CATN_def] 668 THENL 669 [Q.EXISTS_TAC `[v]` 670 THEN RW_TAC list_ss [CONC_identity], 671 FULL_SIMP_TAC list_ss [US_SEM_def] 672 THEN RES_TAC 673 THEN Q.EXISTS_TAC `v1::vlist` 674 THEN RW_TAC list_ss [CONC_identity] 675 THEN PROVE_TAC[FOLDL_CONCAT_N]]]]); 676 677val WEAKEN_CONC = 678 prove 679 (``!v w. WEAKEN v * w = WEAKEN v``, 680 Induct 681 THEN RW_TAC list_ss [CONC_def,WEAKEN_def]); 682 683val END_WEAKEN = 684 prove 685 (``!v. END(WEAKEN v) = W[]``, 686 Induct 687 THEN RW_TAC list_ss [CONC_def,WEAKEN_def,END_def]); 688 689val NN_APPEND_PREFIX = 690 prove 691 (``!u v. PREFIX (N u) (N v) ==> PREFIX (N(w ++ u)) (N(w ++ v))``, 692 RW_TAC list_ss [PREFIX_def,CONC_def] 693 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 694 THEN FULL_SIMP_TAC list_ss 695 [CONC_def,CONC_identity,A_11,A_distinct] 696 THENL 697 [PROVE_TAC[CONC_identity], 698 Q.EXISTS_TAC `N(h::t)` 699 THEN RW_TAC list_ss [CONC_def], 700 Q.EXISTS_TAC `N l` 701 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND], 702 Q.EXISTS_TAC `N l` 703 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND]]); 704 705val WN_APPEND_PREFIX = 706 prove 707 (``!u v. PREFIX (W u) (N v) ==> PREFIX (W(w ++ u)) (N(w ++ v))``, 708 RW_TAC list_ss [PREFIX_def,CONC_def] 709 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 710 THEN FULL_SIMP_TAC list_ss 711 [CONC_def,CONC_identity,A_11,A_distinct]); 712 713val NW_APPEND_PREFIX = 714 prove 715 (``!u v. PREFIX (N u) (W v) ==> PREFIX (N(w ++ u)) (W(w ++ v))``, 716 RW_TAC list_ss [PREFIX_def,CONC_def] 717 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 718 THEN FULL_SIMP_TAC list_ss 719 [CONC_def,CONC_identity,A_11,A_distinct] 720 THENL 721 [Q.EXISTS_TAC `W[]` 722 THEN RW_TAC list_ss [CONC_def], 723 Q.EXISTS_TAC `W(h::t)` 724 THEN RW_TAC list_ss [CONC_def], 725 Q.EXISTS_TAC `W l` 726 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND], 727 Q.EXISTS_TAC `W l` 728 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND]]); 729 730val WW_APPEND_PREFIX = 731 prove 732 (``!u v. PREFIX (W u) (W v) ==> PREFIX (W(w ++ u)) (W(w ++ v))``, 733 RW_TAC list_ss [PREFIX_def,CONC_def] 734 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 735 THEN FULL_SIMP_TAC list_ss 736 [CONC_def,CONC_identity,A_11,A_distinct]); 737 738val APPEND_STRICT_PREFIX = 739 prove 740 (``!u v. 741 (STRICT_PREFIX (N u) (N v) ==> STRICT_PREFIX (N(w ++ u)) (N(w ++ v))) /\ 742 (STRICT_PREFIX (W u) (N v) ==> STRICT_PREFIX (W(w ++ u)) (N(w ++ v))) /\ 743 (STRICT_PREFIX (N u) (W v) ==> STRICT_PREFIX (N(w ++ u)) (W(w ++ v))) /\ 744 (STRICT_PREFIX (W u) (W v) ==> STRICT_PREFIX (W(w ++ u)) (W(w ++ v)))``, 745 RW_TAC list_ss 746 [STRICT_PREFIX_def, 747 NN_APPEND_PREFIX,WN_APPEND_PREFIX,NW_APPEND_PREFIX,WW_APPEND_PREFIX]); 748 749val NOT_STRICT_PREFIX_N = 750 prove 751 (``!u. ~STRICT_PREFIX u (N [])``, 752 GEN_TAC 753 THEN Cases_on `u` 754 THEN RW_TAC list_ss [CONC_def,STRICT_PREFIX_def,PREFIX_def] 755 THEN Cases_on `l = []` 756 THEN RW_TAC list_ss [CONC_def] 757 THEN Cases_on `u` 758 THEN RW_TAC list_ss [CONC_def,STRICT_PREFIX_def,PREFIX_def]); 759 760local 761val S_SEM_SIMPS = 762 [US_SEM_def,IS_WEAK_def,IS_NEUTRAL_def,LEN_def,ELEM_def, 763 WEAKEN_def,WEAKEN,LEN_WEAKEN,PREFIX_def,STRICT_PREFIX_def,CONC_def]; 764in 765val TightPrefix_S_BOOL = 766 prove 767 (``!b w. 768 US_SEM w (S_BOOL b) 769 ==> 770 !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_BOOL b)``, 771 RW_TAC list_ss S_SEM_SIMPS 772 THEN Cases_on `u` THEN Cases_on `u'` 773 THEN FULL_SIMP_TAC list_ss (S_SEM_SIMPS@[CONC_def,A_11,A_distinct]) 774 THEN `(LENGTH l = 0) \/ (LENGTH l' = 0)` by DECIDE_TAC 775 THEN `l' = []` by PROVE_TAC[LENGTH_NIL] 776 THEN FULL_SIMP_TAC list_ss []) 777end; 778 779val TightPrefix_S_CAT = 780 prove 781 (``(!w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r) /\ 782 (!w. US_SEM w r' ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r') 783 ==> 784 !w. US_SEM w (S_CAT (r,r')) 785 ==> 786 !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_CAT (r,r'))``, 787 RW_TAC list_ss [US_SEM_def] 788 THEN Cases_on `STRICT_PREFIX u v1` 789 THENL 790 [RES_TAC 791 THEN Q.EXISTS_TAC `WEAKEN u` THEN Q.EXISTS_TAC `v2` 792 THEN RW_TAC list_ss [] 793 THEN Cases_on `u` THEN Cases_on `v2` 794 THEN RW_TAC list_ss [WEAKEN_def,CONC_def], 795 `PREFIX v1 u` by PROVE_TAC[PREFIX_TRICHOTOMY,STRICT_PREFIX_def,PREFIX_CONC,PREFIX_REFL] 796 THEN FULL_SIMP_TAC list_ss [PREFIX_def] 797 THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `u` THEN Cases_on `u'` 798 THEN FULL_SIMP_TAC list_ss [WEAKEN_def,CONC_def,A_11,A_distinct] 799 THEN Q.EXISTS_TAC`N l` THEN Q.EXISTS_TAC `W l'''` 800 THEN RW_TAC list_ss [CONC_def] 801 THEN IMP_RES_TAC STRICT_PREFIX_CANCEL 802 THEN RES_TAC 803 THEN FULL_SIMP_TAC list_ss [WEAKEN_def]]); 804 805val TightPrefix_S_FUSION = 806 prove 807 (``(!w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r) /\ 808 (!w. US_SEM w r' ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r') 809 ==> 810 !w. US_SEM w (S_FUSION (r,r')) 811 ==> 812 !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_FUSION (r,r'))``, 813 RW_TAC list_ss [US_SEM_def] 814 THEN Cases_on `STRICT_PREFIX u (v1 * l)` 815 THENL 816 [`US_SEM (WEAKEN u) r` by PROVE_TAC[] 817 THEN `US_SEM (WEAKEN u * l) r` by PROVE_TAC[WEAKEN_CONC] 818 THEN `US_SEM (W[]) r'` by PROVE_TAC[TightTrueEmpty] 819 THEN `US_SEM (END(WEAKEN u) * (l * v2)) r'` by RW_TAC list_ss [END_WEAKEN,CONC_def] 820 THEN Q.EXISTS_TAC `WEAKEN u` THEN Q.EXISTS_TAC `v2` THEN Q.EXISTS_TAC `l` 821 THEN RW_TAC list_ss [] 822 THEN Cases_on `u` 823 THEN RW_TAC list_ss [WEAKEN_def,CONC_def] 824 THEN FULL_SIMP_TAC std_ss [CONC_assoc,WEAKEN_def], 825 `PREFIX (v1 * l) u` by PROVE_TAC[PREFIX_TRICHOTOMY,STRICT_PREFIX_def,PREFIX_CONC,PREFIX_REFL] 826 THEN FULL_SIMP_TAC list_ss [PREFIX_def] 827 THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `l` 828 THEN FULL_SIMP_TAC list_ss [WEAKEN_def,CONC_def,A_11,A_distinct] 829 THEN Q.EXISTS_TAC`N l'` THEN Q.EXISTS_TAC `W l''''` THEN Q.EXISTS_TAC `N l'''''` 830 THEN RW_TAC list_ss [CONC_def,END_def] 831 THEN FULL_SIMP_TAC list_ss [CONC_def,END_def] 832 THEN IMP_RES_TAC STRICT_PREFIX_CANCEL 833 THEN PROVE_TAC[APPEND_STRICT_PREFIX,WEAKEN_def]]); 834 835val TightPrefix_S_CATN = 836 prove 837 (``(!w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r) 838 ==> 839 !n w. 840 US_SEM w (S_CATN n r) 841 ==> 842 !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) (S_CATN n r)``, 843 DISCH_TAC 844 THEN Induct 845 THEN RW_TAC list_ss [S_CATN_def] 846 THEN RES_TAC 847 THEN IMP_RES_TAC TightPrefix_S_CAT); 848 849val TightPrefix = 850 prove 851 (``!r w. US_SEM w r ==> !u. STRICT_PREFIX u w ==> US_SEM (WEAKEN u) r``, 852 INDUCT_THEN sere_induct ASSUME_TAC 853 THENL 854 [(* S_BOOL b *) 855 PROVE_TAC[TightPrefix_S_BOOL], 856 (* S_CAT (r,r') *) 857 RW_TAC std_ss [] 858 THEN IMP_RES_TAC TightPrefix_S_CAT, 859 (* S_FUSION (r,r') *) 860 RW_TAC std_ss [] 861 THEN IMP_RES_TAC TightPrefix_S_FUSION, 862 (* S_OR (r,r') *) 863 RW_TAC std_ss [US_SEM_def] 864 THEN PROVE_TAC[], 865 (* S_AND (r,r') *) 866 RW_TAC std_ss [US_SEM_def] 867 THEN PROVE_TAC[], 868 (* S_REPEAT (r,r') *) 869 PROVE_TAC[US_SEM_REPEAT_CATN,NOT_STRICT_PREFIX_N,TightPrefix_S_CATN]]); 870 871 872