1(*****************************************************************************) 2(* Create "WeakPSLUnclockedSemanticsTheory" *) 3(*****************************************************************************) 4 5(****************************************************************************** 6* Load theory of syntax, paths and models 7* (commented out for compilation) 8******************************************************************************) 9(* 10quietdec := true; (* Switch off output *) 11loadPath (* Add official-semantics to path *) 12 := 13 "../1.1/official-semantics" :: "../path" :: !loadPath; 14map load 15 ["intLib", "Cooper","rich_listTheory", (* Load useful theories *) 16 "FinitePathTheory", "PathTheory", 17 "res_quanLib", "res_quanTheory", 18 "SyntaxTheory","SyntacticSugarTheory", 19 "LemmasTheory","ProjectionTheory", 20 "UnclockedSemanticsTheory"]; 21open FinitePathTheory PathTheory (* Open theories *) 22 SyntaxTheory SyntacticSugarTheory 23 UnclockedSemanticsTheory 24 LemmasTheory ProjectionTheory 25 arithmeticTheory listTheory 26 rich_listTheory 27 res_quanLib res_quanTheory; 28intLib.deprecate_int(); (* Set num as default numbers type *) 29quietdec := false; (* Restore output *) 30*) 31 32(****************************************************************************** 33* Boilerplate needed for compilation 34******************************************************************************) 35open HolKernel Parse boolLib bossLib; 36 37(****************************************************************************** 38* Open theories 39******************************************************************************) 40open FinitePathTheory PathTheory SyntaxTheory SyntacticSugarTheory 41 UnclockedSemanticsTheory LemmasTheory ProjectionTheory 42 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory; 43 44(****************************************************************************** 45* Set default parsing to natural numbers rather than integers 46******************************************************************************) 47val _ = intLib.deprecate_int(); 48 49(*****************************************************************************) 50(* END BOILERPLATE *) 51(*****************************************************************************) 52 53(*****************************************************************************) 54(* Start a new theory called WeakPSLUnclockedSemanticsTheory *) 55(*****************************************************************************) 56 57val _ = new_theory "WeakPSLUnclockedSemantics"; 58 59(*****************************************************************************) 60(* N^f = { w | w is a finite list of states/letters } (the set of neutral *) 61(* finite words) *) 62(* *) 63(* we let \epsilon be the empty (neutral) word *) 64(* *) 65(* W = { W(w) | w \in N^f } (the set of weak finite words) *) 66(* *) 67(* Let A = N^f U W *) 68(*****************************************************************************) 69 70(*****************************************************************************) 71(* Definition of a datatypetype A. It creates a tagged disjoint union with *) 72(* elements ``N l``, ``W l`` and ``S l``, where l is a HOL list. *) 73(*****************************************************************************) 74val A_def = 75 Hol_datatype 76 `A = N of 'a list 77 | W of 'a list 78 | S of 'a list`; 79 80(*****************************************************************************) 81(* Retrieve from data-base (DB) automatically proved theorems about A *) 82(*****************************************************************************) 83val A_11 = assoc "A_11" (DB.theorems "-") 84and A_distinct = assoc "A_distinct" (DB.theorems "-"); 85 86val A_ELEM_def = 87 Define 88 `(A_ELEM (N l) n = EL n l) 89 /\ 90 (A_ELEM (W l) n = EL n l) 91 /\ 92 (A_ELEM (S l) n = EL n l)`; 93 94(*****************************************************************************) 95(* We define concatenation ( * ) on A: if v,w \in N then v*w is just the *) 96(* list concatenation of v and w (remember v,w finite) v*W(w) = W(v*w) *) 97(* and for v\in W and w\in A v*w = v *) 98(*****************************************************************************) 99 100(*****************************************************************************) 101(* For readability overload "++" onto HOL's list append constant APPEND, *) 102(* and make it a left associative infix with precedence 500. *) 103(*****************************************************************************) 104val _ = set_fixity "++" (Infixl 500); 105val _ = overload_on("++", ``APPEND``); 106 107(*****************************************************************************) 108(* Define ``CONC`` for concatenation on values of type A. *) 109(*****************************************************************************) 110val _ = set_fixity "CONC" (Infixl 500); 111 112val CONC_def = 113 Define 114 `(N v CONC N w = N(v++w)) 115 /\ 116 (N v CONC W w = W(v++w)) 117 /\ 118 (N v CONC S w = S(v++w)) 119 /\ 120 (W v CONC a = W v) 121 /\ 122 (S v CONC a = S v)`; 123 124(*****************************************************************************) 125(* Overload "*" on to "CONC" for readability. *) 126(*****************************************************************************) 127val _ = overload_on("*", ``$CONC``); 128 129(*****************************************************************************) 130(* We want to show that A is closed under *, that * is associative on A and *) 131(* that \epsilon is the identity for this operation. *) 132(*****************************************************************************) 133val CONC_IDENTITY = 134 prove 135 (``(N[] * a = a) /\ (a * N[] = a)``, 136 Cases_on `a` 137 THEN RW_TAC list_ss [CONC_def]); 138 139val CONC_ASSOC = 140 prove 141 (``a * (b * c) = (a * b) * c``, 142 Cases_on `a` THEN Cases_on `b` THEN Cases_on `c` 143 THEN RW_TAC list_ss [CONC_def]); 144 145val ASSOC_CONC = 146 prove 147 (``ASSOC $*``, 148 RW_TAC std_ss [operatorTheory.ASSOC_DEF,CONC_ASSOC]); 149 150(*****************************************************************************) 151(* for w \in N |w| is the number of elements in w, and |W(w)| = |w| *) 152(*****************************************************************************) 153 154(*****************************************************************************) 155(* Represent |w| by LEN w. HOL's built-in length function on lists *) 156(* is LENGTH. *) 157(*****************************************************************************) 158val LEN_def = 159 Define 160 `(LEN(N w) = LENGTH w) 161 /\ 162 (LEN(W w) = LENGTH w) 163 /\ 164 (LEN(S w) = LENGTH w)`; 165 166(*****************************************************************************) 167(* we want to show that if w \in N then *) 168(* |w*v| = |w|+|v|, |W(w)*v| = |w| and |S(w)*v| = |w| *) 169(*****************************************************************************) 170val LEN = 171 prove 172 (``(LEN(N w * a) = LEN(N w) + LEN a) 173 /\ 174 (LEN(W w * a) = LEN(W w)) 175 /\ 176 (LEN(S w * a) = LEN(S w))``, 177 Cases_on `a` 178 THEN RW_TAC list_ss [LEN_def,CONC_def]); 179 180(*****************************************************************************) 181(* We define (on A) w<=v (prefix) if there is u \in A such that w*u=v *) 182(*****************************************************************************) 183val PREFIX_def = Define `PREFIX w v = ?u. w*u = v`; 184 185val STRICT_PREFIX_def = Define `STRICT_PREFIX w v = PREFIX w v /\ ~(w = v)`; 186 187(*****************************************************************************) 188(* u<w is u is prefix of w and u/=w *) 189(* One could try to prove that if u<w u is neutral *) 190(*****************************************************************************) 191 192val STRICT_PREFIX_NEUTRAL = 193 prove 194 (``STRICT_PREFIX u w ==> ?l. u = N l``, 195 Cases_on `u` THEN Cases_on `w` 196 THEN RW_TAC list_ss [STRICT_PREFIX_def,PREFIX_def,CONC_def]); 197 198val IS_WEAK_def = 199 Define 200 `(IS_WEAK(W w) = T) /\ (IS_WEAK(N w) = F) /\ (IS_WEAK(S w) = F)` 201and IS_NEUTRAL_def = 202 Define 203 `(IS_NEUTRAL(W w) = F) /\ (IS_NEUTRAL(N w) = T) /\ (IS_NEUTRAL(S w) = F)` 204and IS_STRONG_def = 205 Define 206 `(IS_STRONG(W w) = F) /\ (IS_STRONG(N w) = F) /\ (IS_STRONG(S w) = T)`; 207 208val IS_LETTER_def = 209 Define 210 `(IS_LETTER(N w) = ?l. w = [l]) 211 /\ 212 (IS_LETTER(W w) = ?l. w = [l]) 213 /\ 214 (IS_LETTER(S w) = ?l. w = [l])`; 215 216(*****************************************************************************) 217(* WeakPSL Semantics of SEREs *) 218(*****************************************************************************) 219 220(*###################################################################### 221# 222# [Notation: w^- = W(w) and w^+ = S(w)] 223# 224# Weak/neutral word definition 225# ---------------------------- 226# for finite w \in W U N U S 227# 228# we define (let l be a letter or \epsilon^-) 229# 230# w|==wns b <=> either w=\epsilon^- or (w not \in S and |w|=1 and w^0||-b) 231# w|==wns r1;r2 <=> there exist u,v s.t. uv=w and u|==wns r1 and v|==wns r2 232# w|==wns r1:r2 <=> there exist u,v,l s.t. ulv=w and ul|==wns r1 and lv|==wns r2 233# w|==wns r1&r2 <=> w|==wns r1 and w|==wns r2 234# w|==wns r1|r2 <=> w|==wns r1 or w|==wns r2 235# w|==wns r* <=> either w=\epsilon 236# or there exist w_1,..w_j 237# s.t. w=w_1w_2...w_j and for 1<=i<=j w_i|==wns r 238######################################################################*) 239 240val WUS_SEM_def = 241 Define 242 `(WUS_SEM v (S_BOOL b) = 243 (v = W[]) \/ (~(IS_STRONG v) /\ (LEN v = 1) /\ B_SEM (A_ELEM v 0) b)) 244 /\ 245 (WUS_SEM v (S_CAT(r1,r2)) = 246 ?v1 v2. (v = v1 * v2) /\ WUS_SEM v1 r1 /\ WUS_SEM v2 r2) 247 /\ 248 (WUS_SEM v (S_FUSION(r1,r2)) = 249 ?v1 v2 l. (IS_LETTER l \/ (l = W[])) /\ (v = v1*l*v2) 250 /\ 251 WUS_SEM (v1*l) r1 /\ WUS_SEM (l*v2) r2) 252 /\ 253 (WUS_SEM v (S_AND(r1,r2)) = 254 WUS_SEM v r1 /\ WUS_SEM v r2) 255 /\ 256 (WUS_SEM v (S_OR(r1,r2)) = 257 WUS_SEM v r1 \/ WUS_SEM v r2) 258 /\ 259 (WUS_SEM v S_EMPTY = (v = N[]) \/ (v = W[])) 260 /\ 261 (WUS_SEM v (S_REPEAT r) = 262 ?vlist. (v = FOLDL $* (N[]) vlist) /\ EVERY (\v. WUS_SEM v r) vlist)`; 263 264(*****************************************************************************) 265(* We can now prove with fusion in the language *) 266(* for all unclocked r: W(\espilon) |==wns r *) 267(*****************************************************************************) 268local 269val WUS_SEM_SIMP_TAC = 270 RW_TAC list_ss 271 [S_CLOCK_FREE_def,WUS_SEM_def,IS_WEAK_def,IS_NEUTRAL_def,LEN_def,A_ELEM_def] 272in 273val TightTrueEmpty = 274 prove 275 (``!r. S_CLOCK_FREE r ==> WUS_SEM (W[]) r``, 276 INDUCT_THEN sere_induct ASSUME_TAC 277 THENL 278 [(* S_BOOL b *) 279 WUS_SEM_SIMP_TAC, 280 (* S_CAT (r,r') *) 281 WUS_SEM_SIMP_TAC 282 THEN Q.EXISTS_TAC `W []` 283 THEN Q.EXISTS_TAC `W []` 284 THEN RW_TAC list_ss [CONC_def], 285 (* S_FUSION (r,r') *) 286 WUS_SEM_SIMP_TAC 287 THEN Q.EXISTS_TAC `W []` 288 THEN Q.EXISTS_TAC `W []` 289 THEN Q.EXISTS_TAC `W []` 290 THEN RW_TAC list_ss [CONC_def,IS_LETTER_def], 291 (* S_OR (r,r') *) 292 WUS_SEM_SIMP_TAC, 293 (* S_AND (r,r') *) 294 WUS_SEM_SIMP_TAC, 295 (* S_EMPTY *) 296 WUS_SEM_SIMP_TAC 297 THEN Q.EXISTS_TAC `[W []]` 298 THEN RW_TAC list_ss [CONC_def], 299 (* S_REPEAT (r,r') *) 300 WUS_SEM_SIMP_TAC 301 THEN Q.EXISTS_TAC `[W []]` 302 THEN RW_TAC list_ss [CONC_def], 303 (* S_REPEAT (r,r') *) 304 WUS_SEM_SIMP_TAC]) 305end; 306 307(*****************************************************************************) 308(* Weaken a word *) 309(*****************************************************************************) 310val WEAKEN_def = 311 Define `(WEAKEN(N l) = W l) /\ (WEAKEN(W l) = W l) /\ (WEAKEN(S l) = S l)`; 312 313val LEN_WEAKEN = 314 prove 315 (``LEN(WEAKEN w) = LEN w``, 316 Cases_on `w` 317 THEN RW_TAC list_ss [WEAKEN_def,LEN_def]); 318 319(*****************************************************************************) 320(* Tight prefix theorem *) 321(* w |==wns r and u <= w => W(u) |==wns r *) 322(*****************************************************************************) 323val APPEND_EQ_NIL = 324 prove 325 (``!l1 l2. (LENGTH(l1++l2) = 0) ==> (l1 = []) /\ (l2 = [])``, 326 Induct 327 THEN RW_TAC list_ss [] 328 THEN `LENGTH l2 = 0` by DECIDE_TAC 329 THEN PROVE_TAC[LENGTH_NIL]); 330 331val APPEND_EQ_SINGLETON = 332 prove 333 (``!l1 l2. (LENGTH(l1++l2) = 1) ==> (l1 = []) \/ (l2 = [])``, 334 Induct 335 THEN RW_TAC list_ss [] 336 THEN `LENGTH l2 = 0` by DECIDE_TAC 337 THEN PROVE_TAC[LENGTH_NIL]); 338 339val APPEND_NIL_CANCEL = 340 prove 341 (``!l1 l2. (l1++l2 = l1) ==> (l2 = [])``, 342 Induct 343 THEN RW_TAC list_ss []); 344 345val PREFIX_CONC = 346 prove 347 (``PREFIX u v1 ==> !v2. PREFIX u (v1 * v2)``, 348 Cases_on `u` THEN Cases_on `v1` 349 THEN RW_TAC list_ss [PREFIX_def,CONC_def] 350 THEN Cases_on `u` THEN Cases_on `v2` 351 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct] 352 THENL 353 [Q.EXISTS_TAC `N(l''++l''')` THEN RW_TAC list_ss [CONC_def], 354 Q.EXISTS_TAC `W(l''++l''')` THEN RW_TAC list_ss [CONC_def], 355 Q.EXISTS_TAC `S(l''++l''')` THEN RW_TAC list_ss [CONC_def]]); 356 357val HD_APPEND = 358 prove 359 (``!v1 v2. ~(v1 = []) ==> (HD(APPEND v1 v2) = HD v1)``, 360 Induct 361 THEN RW_TAC list_ss []); 362 363val TL_APPEND = 364 prove 365 (``!v1 v2. ~(v1 = []) ==> (TL(APPEND v1 v2) = APPEND (TL v1) v2)``, 366 Induct 367 THEN RW_TAC list_ss []); 368 369val LIST_TRICHOTOMY_LEMMA1 = 370 prove 371 (``~(v = []) ==> (h::u ++ u' = v ++ v') ==> (h = HD v) /\ (u ++ u' = TL v ++ v')``, 372 RW_TAC list_ss [] 373 THEN PROVE_TAC[HD,HD_APPEND,TL,TL_APPEND]); 374 375val LIST_TRICHOTOMY_LEMMA2 = 376 prove 377 (``~(v = []) ==> (!w. ~(HD v::u ++ w = v)) ==> !w. ~(u ++ w = TL v)``, 378 RW_TAC list_ss [] 379 THEN POP_ASSUM(ASSUME_TAC o SPEC_ALL) 380 THEN Cases_on `~(u ++ w = TL v)` 381 THEN FULL_SIMP_TAC list_ss [] 382 THEN `HD v :: u ++ w = HD v :: TL v` by PROVE_TAC[] 383 THEN `~(NULL v)` by PROVE_TAC[NULL_EQ_NIL] 384 THEN FULL_SIMP_TAC std_ss [CONS] 385 THEN RES_TAC); 386 387val LIST_TRICHOTOMY_LEMMA3 = 388 prove 389 (``!u v. 390 (u ++ u' = v ++ v') /\ (!w. ~(u ++ w = v)) 391 ==> 392 ?w. v ++ w = u``, 393 Induct 394 THEN RW_TAC list_ss [] 395 THEN Cases_on `v=[]` 396 THEN RW_TAC list_ss [] 397 THEN IMP_RES_TAC LIST_TRICHOTOMY_LEMMA1 398 THEN RW_TAC list_ss [] 399 THEN `TL(HD v::u ++ u') = TL(v ++ v')` by PROVE_TAC[] 400 THEN FULL_SIMP_TAC list_ss [] 401 THEN IMP_RES_TAC LIST_TRICHOTOMY_LEMMA2 402 THEN RES_TAC 403 THEN `HD v :: TL v ++ w = HD v :: u` by PROVE_TAC[] 404 THEN PROVE_TAC[APPEND,CONS,NULL_EQ_NIL]); 405 406val LIST_TRICHOTOMY = 407 prove 408 (``!u v. 409 (?u' v'. u ++ u' = v ++ v') 410 ==> 411 (?w. u ++ w = v) \/ (?w. v ++ w = u)``, 412 RW_TAC list_ss [] 413 THEN Cases_on `(?w. u ++ w = v)` (* u<=v *) 414 THEN RW_TAC list_ss [] 415 THEN FULL_SIMP_TAC list_ss [] 416 THEN Induct_on `u` 417 THEN RW_TAC list_ss [] 418 THEN PROVE_TAC[LIST_TRICHOTOMY_LEMMA3,APPEND]); 419 420val PREFIX_TRICHOTOMY = 421 prove 422 (``!v1 v2 w. 423 PREFIX v1 w /\ PREFIX v2 w ==> STRICT_PREFIX v1 v2 \/ PREFIX v2 v1``, 424 REPEAT GEN_TAC 425 THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `w` 426 THEN RW_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def] 427 THEN Cases_on `u` THEN Cases_on `u'` 428 THEN FULL_SIMP_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def,A_11,A_distinct] 429 THEN Cases_on `?u. l' ++ u = l` 430 THEN FULL_SIMP_TAC list_ss [PREFIX_def,STRICT_PREFIX_def,CONC_def,A_11,A_distinct] 431 THEN ZAP_TAC list_ss [CONC_def,A_11] 432 THEN Cases_on `?u. l++u = l'` 433 THEN ZAP_TAC list_ss [CONC_def,A_11] 434 THEN FULL_SIMP_TAC list_ss [] 435 THEN IMP_RES_TAC LIST_TRICHOTOMY 436 THEN RES_TAC); 437 438val PREFIX_REFL = 439 prove 440 (``!v. PREFIX v v``, 441 Induct 442 THEN RW_TAC list_ss [PREFIX_def,CONC_def] 443 THEN Q.EXISTS_TAC `N[]` 444 THEN RW_TAC list_ss [CONC_def]); 445 446val APPEND_LEFT_CANCEL = 447 store_thm 448 ("APPEND_LEFT_CANCEL", 449 ``(APPEND l l1 = APPEND l l2) = (l1 = l2)``, 450 Induct_on `l` 451 THEN ZAP_TAC list_ss []); 452 453val PREFIX_CANCEL = 454 prove 455 (``(PREFIX (N(u ++ v1)) (N(u ++ v2)) ==> PREFIX (N v1) (N v2)) /\ 456 (PREFIX (W(u ++ v1)) (N(u ++ v2)) ==> PREFIX (W v1) (N v2)) /\ 457 (PREFIX (S(u ++ v1)) (N(u ++ v2)) ==> PREFIX (S v1) (N v2)) /\ 458 (PREFIX (N(u ++ v1)) (W(u ++ v2)) ==> PREFIX (N v1) (W v2)) /\ 459 (PREFIX (W(u ++ v1)) (W(u ++ v2)) ==> PREFIX (W v1) (W v2)) /\ 460 (PREFIX (S(u ++ v1)) (W(u ++ v2)) ==> PREFIX (S v1) (W v2)) /\ 461 (PREFIX (N(u ++ v1)) (S(u ++ v2)) ==> PREFIX (N v1) (S v2)) /\ 462 (PREFIX (W(u ++ v1)) (S(u ++ v2)) ==> PREFIX (W v1) (S v2)) /\ 463 (PREFIX (S(u ++ v1)) (S(u ++ v2)) ==> PREFIX (S v1) (S v2))``, 464 RW_TAC list_ss [PREFIX_def,CONC_def] 465 THEN Cases_on `u'` 466 THEN FULL_SIMP_TAC std_ss 467 [GSYM APPEND_ASSOC,CONC_def,A_11,A_distinct,APPEND_LEFT_CANCEL] 468 THEN PROVE_TAC[CONC_def]); 469 470val B_FALSE = 471 prove 472 (``B_SEM (STATE s) B_FALSE = F``, 473 RW_TAC list_ss [B_SEM_def]); 474 475val IS_WEAK_LEN_0 = 476 prove 477 (``!v. IS_WEAK v /\ (LEN v = 0) = (v = W[])``, 478 Induct 479 THEN RW_TAC list_ss [IS_WEAK_def,LEN_def,LENGTH_NIL]); 480 481val FOLDL_W_NIL = 482 prove 483 (``!l. ALL_EL (\v. v = W []) l ==> (FOLDL $* (W []) l = W[])``, 484 Induct 485 THEN RW_TAC list_ss [CONC_def]); 486 487val FOLDL_N_NIL = 488 prove 489 (``!l. ~(l = []) ==> ALL_EL (\v. v = W []) l ==> (FOLDL $* (N []) l = W[])``, 490 Induct 491 THEN RW_TAC list_ss [CONC_def,FOLDL_W_NIL]); 492 493(*****************************************************************************) 494(* Not sure why I defined WS_CATN here and S_CATN in ProjectionTheory. *) 495(* Probably could get away with just the latter, but I'm too lazy to redo *) 496(* the proofs! *) 497(*****************************************************************************) 498val WS_CATN_def = 499 Define 500 `(WS_CATN 0 r = r) /\ (WS_CATN (SUC n) r = S_CAT(r, WS_CATN n r))`; 501 502(*****************************************************************************) 503(* Theorem to connect WS_CATN and S_CATN in the LRM 1.1 semantics *) 504(*****************************************************************************) 505val US_SEM_WS_CATN = 506 store_thm 507 ("US_SEM_WS_CATN", 508 ``!n w r. US_SEM w (WS_CATN n r) = US_SEM w (S_CATN (SUC n) r)``, 509 Induct 510 THEN RW_TAC list_ss [US_SEM,WS_CATN_def,S_CATN_def]); 511 512val ASSOC_FOLDL = 513 prove 514 (``!l x y. ASSOC f ==> (FOLDL f (f x y) l = f x (FOLDL f y l))``, 515 Induct 516 THEN RW_TAC list_ss [operatorTheory.ASSOC_DEF]); 517 518val FOLDL_CONCAT_N = 519 prove 520 (``!vlist v. FOLDL $* v vlist = v * FOLDL $* (N []) vlist``, 521 PROVE_TAC[ASSOC_FOLDL,ASSOC_CONC,CONC_IDENTITY]); 522 523val WUS_SEM_CAT_REPEAT_CATN = 524 store_thm 525 ("WUS_SEM_CAT_REPEAT_CATN", 526 ``!v r. WUS_SEM v (S_CAT(S_REPEAT r, r)) = ?n. WUS_SEM v (WS_CATN n r)``, 527 RW_TAC list_ss [WUS_SEM_def] 528 THEN EQ_TAC 529 THEN RW_TAC list_ss [] 530 THENL 531 [Induct_on `vlist` 532 THEN RW_TAC list_ss [CONC_IDENTITY,WS_CATN_def,WUS_SEM_def] 533 THEN ZAP_TAC std_ss [WS_CATN_def] 534 THEN RW_TAC std_ss [] 535 THEN RES_TAC 536 THEN Q.EXISTS_TAC `SUC n` 537 THEN RW_TAC list_ss [WS_CATN_def,WUS_SEM_def] 538 THEN Q.EXISTS_TAC `h` THEN Q.EXISTS_TAC `FOLDL $* (N []) vlist * v2` 539 THEN RW_TAC std_ss [] 540 THEN PROVE_TAC[FOLDL_CONCAT_N,CONC_ASSOC], 541 Q.UNDISCH_TAC `WUS_SEM v (WS_CATN n r)` 542 THEN Q.SPEC_TAC(`v`,`v`) 543 THEN Q.SPEC_TAC(`r`,`r`) 544 THEN Q.SPEC_TAC(`n`,`n`) 545 THEN Induct 546 THEN RW_TAC list_ss [WS_CATN_def] 547 THENL 548 [Q.EXISTS_TAC `N[]` THEN Q.EXISTS_TAC `v` 549 THEN RW_TAC list_ss [CONC_IDENTITY] 550 THEN Q.EXISTS_TAC `[]` 551 THEN RW_TAC list_ss [], 552 FULL_SIMP_TAC list_ss [WUS_SEM_def] 553 THEN RES_TAC 554 THEN RW_TAC std_ss [] 555 THEN Q.EXISTS_TAC `v1 * FOLDL $* (N []) vlist` 556 THEN Q.EXISTS_TAC `v2'` 557 THEN RW_TAC std_ss [CONC_ASSOC] 558 THEN Q.EXISTS_TAC `v1::vlist` 559 THEN RW_TAC list_ss [CONC_IDENTITY] 560 THEN PROVE_TAC[FOLDL_CONCAT_N]]]); 561 562val FOLDLN_def = 563 Define 564 `(FOLDLN 0 f e l = e) /\ 565 (FOLDLN (SUC n) f e l = FOLDLN n f (f e (HD l)) (TL l))`; 566 567val FOLDLN_LENGTH = 568 prove 569 (``!l f e. FOLDLN (LENGTH l) f e l = FOLDL f e l``, 570 Induct 571 THEN RW_TAC list_ss [FOLDLN_def]); 572 573val FOLDLN_ASSOC = 574 prove 575 (``!n v1 v2 l. FOLDLN n $* (v1 * v2) l = v1 * FOLDLN n $* v2 l``, 576 Induct 577 THEN RW_TAC list_ss [FOLDLN_def,CONC_ASSOC]); 578 579val FOLDLN_CATN = 580 prove 581 (``!l v0 r. 582 ALL_EL (\v. WUS_SEM v r) l /\ WUS_SEM v0 r 583 ==> 584 !n. n <= LENGTH l ==> WUS_SEM (FOLDLN n $* v0 l) (WS_CATN n r)``, 585 Induct 586 THEN RW_TAC list_ss [FOLDLN_def,WS_CATN_def] 587 THEN Cases_on `n = 0` 588 THEN RW_TAC list_ss [FOLDLN_def,WS_CATN_def] 589 THEN `?m. n = SUC m` by Cooper.COOPER_TAC 590 THEN RW_TAC list_ss [FOLDLN_def,WS_CATN_def] 591 THEN FULL_SIMP_TAC arith_ss [WUS_SEM_def] 592 THEN RES_TAC 593 THEN Q.EXISTS_TAC `v0` 594 THEN Q.EXISTS_TAC `FOLDLN m $* h l` 595 THEN RW_TAC list_ss [FOLDLN_ASSOC]); 596 597val WUS_SEM_REPEAT_WS_CATN = 598 store_thm 599 ("WUS_SEM_REPEAT_WS_CATN", 600 ``!v r. WUS_SEM v (S_REPEAT r) = (v = N[]) 601 \/ 602 ?n. WUS_SEM v (WS_CATN n r)``, 603 RW_TAC list_ss [] 604 THEN EQ_TAC 605 THENL 606 [SIMP_TAC list_ss[WUS_SEM_def] 607 THEN REPEAT STRIP_TAC 608 THEN Cases_on `v = N[]` 609 THEN ASM_REWRITE_TAC[] 610 THEN Cases_on `vlist` 611 THEN FULL_SIMP_TAC list_ss [CONC_IDENTITY] 612 THEN RES_TAC 613 THEN `LENGTH t <= LENGTH t` by DECIDE_TAC 614 THEN IMP_RES_TAC FOLDLN_CATN 615 THEN Q.EXISTS_TAC `LENGTH t` 616 THEN FULL_SIMP_TAC list_ss [FOLDLN_LENGTH], 617 RW_TAC list_ss [WUS_SEM_def] 618 THENL 619 [Q.EXISTS_TAC `[]` 620 THEN RW_TAC list_ss [], 621 Q.UNDISCH_TAC `WUS_SEM v (WS_CATN n r)` 622 THEN Q.SPEC_TAC(`v`,`v`) 623 THEN Q.SPEC_TAC(`r`,`r`) 624 THEN Q.SPEC_TAC(`n`,`n`) 625 THEN Induct 626 THEN RW_TAC list_ss [WS_CATN_def] 627 THENL 628 [Q.EXISTS_TAC `[v]` 629 THEN RW_TAC list_ss [CONC_IDENTITY], 630 FULL_SIMP_TAC list_ss [WUS_SEM_def] 631 THEN RES_TAC 632 THEN Q.EXISTS_TAC `v1::vlist` 633 THEN RW_TAC list_ss [CONC_IDENTITY] 634 THEN PROVE_TAC[FOLDL_CONCAT_N]]]]); 635 636val NN_APPEND_PREFIX = 637 prove 638 (``!u v. PREFIX (N u) (N v) ==> PREFIX (N(w ++ u)) (N(w ++ v))``, 639 RW_TAC list_ss [PREFIX_def,CONC_def] 640 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 641 THEN FULL_SIMP_TAC list_ss 642 [CONC_def,CONC_IDENTITY,A_11,A_distinct] 643 THENL 644 [PROVE_TAC[CONC_IDENTITY], 645 Q.EXISTS_TAC `N(h::t)` 646 THEN RW_TAC list_ss [CONC_def], 647 Q.EXISTS_TAC `N l` 648 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND], 649 Q.EXISTS_TAC `N l` 650 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND]]); 651 652val WN_APPEND_PREFIX = 653 prove 654 (``!u v. PREFIX (W u) (N v) ==> PREFIX (W(w ++ u)) (N(w ++ v))``, 655 RW_TAC list_ss [PREFIX_def,CONC_def] 656 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 657 THEN FULL_SIMP_TAC list_ss 658 [CONC_def,CONC_IDENTITY,A_11,A_distinct]); 659 660val NW_APPEND_PREFIX = 661 prove 662 (``!u v. PREFIX (N u) (W v) ==> PREFIX (N(w ++ u)) (W(w ++ v))``, 663 RW_TAC list_ss [PREFIX_def,CONC_def] 664 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 665 THEN FULL_SIMP_TAC list_ss 666 [CONC_def,CONC_IDENTITY,A_11,A_distinct] 667 THENL 668 [Q.EXISTS_TAC `W[]` 669 THEN RW_TAC list_ss [CONC_def], 670 Q.EXISTS_TAC `W(h::t)` 671 THEN RW_TAC list_ss [CONC_def], 672 Q.EXISTS_TAC `W l` 673 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND], 674 Q.EXISTS_TAC `W l` 675 THEN RW_TAC std_ss [CONC_def,GSYM APPEND_ASSOC,APPEND]]); 676 677val WW_APPEND_PREFIX = 678 prove 679 (``!u v. PREFIX (W u) (W v) ==> PREFIX (W(w ++ u)) (W(w ++ v))``, 680 RW_TAC list_ss [PREFIX_def,CONC_def] 681 THEN Cases_on `u` THEN Cases_on `u'` THEN Cases_on `v` THEN Cases_on `w` 682 THEN FULL_SIMP_TAC list_ss 683 [CONC_def,CONC_IDENTITY,A_11,A_distinct]); 684 685local 686val WUS_SEM_SIMPS = 687 [WUS_SEM_def,IS_WEAK_def,IS_NEUTRAL_def,LEN_def,A_ELEM_def, 688 WEAKEN_def,(*WEAKEN,*)LEN_WEAKEN,PREFIX_def,PREFIX_def,CONC_def] 689in 690val TightPrefix_S_BOOL = 691 prove 692 (``!b w. 693 WUS_SEM w (S_BOOL b) 694 ==> 695 !u. PREFIX u w ==> WUS_SEM (WEAKEN u) (S_BOOL b)``, 696 RW_TAC list_ss WUS_SEM_SIMPS 697 THEN Cases_on `u` THEN Cases_on `u'` 698 THEN FULL_SIMP_TAC list_ss 699 (WUS_SEM_SIMPS@[IS_STRONG_def,CONC_def,A_11,A_distinct]) 700 THEN `(LENGTH l = 0) \/ (LENGTH l' = 0)` by DECIDE_TAC 701 THEN (`l = []` by PROVE_TAC[LENGTH_NIL] ORELSE 702 `l' = []` by PROVE_TAC[LENGTH_NIL]) 703 THEN FULL_SIMP_TAC list_ss []) 704end; 705 706val TightPrefix_S_CAT = 707 prove 708 (``(!w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r) /\ 709 (!w. WUS_SEM w r' ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r') 710 ==> 711 !w. WUS_SEM w (S_CAT (r,r')) 712 ==> 713 !u. PREFIX u w ==> WUS_SEM (WEAKEN u) (S_CAT (r,r'))``, 714 RW_TAC list_ss [WUS_SEM_def] 715 THEN Cases_on `PREFIX u v1` 716 THENL 717 [RES_TAC 718 THEN Q.EXISTS_TAC `WEAKEN u` THEN Q.EXISTS_TAC `v2` 719 THEN RW_TAC list_ss [] 720 THEN Cases_on `u` THEN Cases_on `v2` 721 THEN RW_TAC list_ss [WEAKEN_def,CONC_def], 722 `STRICT_PREFIX v1 u` 723 by PROVE_TAC[PREFIX_TRICHOTOMY,PREFIX_def,PREFIX_CONC,PREFIX_REFL] 724 THEN FULL_SIMP_TAC list_ss [STRICT_PREFIX_def,PREFIX_def] 725 THEN Q.EXISTS_TAC `v1` THEN Q.EXISTS_TAC `WEAKEN u''` 726 THEN RW_TAC list_ss [CONC_def] 727 THENL 728 [Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `u''` 729 THEN FULL_SIMP_TAC list_ss [WEAKEN_def,CONC_def,A_11,A_distinct], 730 FULL_SIMP_TAC list_ss [GSYM CONC_ASSOC] 731 THEN Cases_on `v1` THEN Cases_on `v2` THEN Cases_on `u'' * u'` 732 THEN FULL_SIMP_TAC list_ss [WEAKEN_def,CONC_def,A_11,A_distinct] 733 THEN RW_TAC std_ss [] 734 THEN RES_TAC]]); 735 736val CONC_WEAKEN = 737 store_thm 738 ("CONC_WEAKEN", 739 ``!u v. WEAKEN u * v = WEAKEN u``, 740 Cases_on `u` 741 THEN RW_TAC list_ss [CONC_def,WEAKEN_def]); 742 743val WEAKEN_CONC = 744 store_thm 745 ("WEAKEN_CONC", 746 ``!v1 v2. WEAKEN(v1 * v2) = v1 * WEAKEN v2``, 747 REPEAT GEN_TAC 748 THEN Cases_on `v1` THEN Cases_on `v2` 749 THEN RW_TAC list_ss [] 750 THEN FULL_SIMP_TAC list_ss [WEAKEN_def] 751 THEN RW_TAC list_ss [CONC_def,WEAKEN_def]); 752 753val APPEND_NIL_CANCEL = 754 store_thm 755 ("APPEND_NIL_CANCEL", 756 ``!l1 l2. (l1 = l1 ++ l2 ) = (l2 = [])``, 757 RW_TAC list_ss [] 758 THEN EQ_TAC 759 THEN RW_TAC list_ss [] 760 THEN `LENGTH l1 = LENGTH(l1 ++ l2)` by PROVE_TAC[] 761 THEN FULL_SIMP_TAC list_ss [] 762 THEN `LENGTH l2 = 0` by DECIDE_TAC 763 THEN PROVE_TAC[LENGTH_NIL]); 764 765(*********************************************************************** 766* if w\in N and w finite and for some u,u', w*u=w*u' then u=u' 767************************************************************************ 768** 769** Assume w \in N and w finite 770** if B is W, N or S then w*u \in B iff u \in B 771** Assume that w*u=w*u' 772** then u \in B iff u' \in B. 773** and also |u|=|u'| since |w|+|u|=|w*u|=|w*u|=|w|+|u'| 774** Now assume for contradiction that u/=u' 775** then there is k such that u^k/=u'^k. 776** but then (w*u)^(|w|+k)/=(w*u')^(|w|+k) contradicting the 777** assumption. 778** 779************************************************************************) 780val CONC_CANCEL = 781 store_thm 782 ("CONC_CANCEL", 783 ``!w u u'. IS_NEUTRAL w ==> ((w * u = w * u') = (u = u'))``, 784 Cases_on `w` THEN Cases_on `u` THEN Cases_on `u'` 785 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct,IS_NEUTRAL_def]); 786 787(*********************************************************************** 788* For v,w in A if v<=w and w<=v then w=v (antisymmetry) 789************************************************************************ 790** 791** Assume that v,w in A and v<=w and w<=v th 792** then there is u1 and u2 such that 793** v*u1=w and w*u2=v 794** if v \in N then w also \in N (because w*u2=w) 795** and v=w (antisymmetry of <= on neutral words) 796** if v \in W (\in S) 797** then v*u1=v so v=w. 798***********************************************************************) 799val PREFIX_ANTISYM = 800 store_thm 801 ("PREFIX_ANTISYM", 802 ``!v w. PREFIX v w /\ PREFIX w v ==> (w = v)``, 803 RW_TAC list_ss [PREFIX_def] 804 THEN Cases_on `w` THEN Cases_on `u` THEN Cases_on `u'` 805 THEN FULL_SIMP_TAC list_ss [CONC_def,A_distinct,A_11] 806 THEN `l'' ++ l' = []` by PROVE_TAC[APPEND_NIL_CANCEL,APPEND_ASSOC] 807 THEN FULL_SIMP_TAC list_ss [APPEND_eq_NIL]); 808 809(*********************************************************************** 810* if l is a letter or \epsilon^- and v1*l*v2 \in A then 811* 812* if v1*l<=u<=v1*l*v2 then there is v2' s.t. v1*l*v2'=u and l*v2'<=l*v2 813************************************************************************ 814** 815** Assume that l is a letter or \epsilon^- [MJCG: this is not needed] 816** and v1*l*v2 \in A 817** and that u is such that v1*l<=u<=v1*l*v2 818** 819** Either v1 \in N or not 820** Assume v1 \in N. 821** let v2' be such that v1*l*v2'=u, so v1*l*v2'<=v1*l*v2 822** let x be such that (v1*l*v2')*x=v1*l*v2. 823** By associativity v1*((l*v2')*x)=v1*(l*v2). 824** so by the previous lemma (l*v2')*x=l*v2 so l*v2'<=l*v2 825** Assume v1 \in W U S. 826** If v1 \in S U W. then v1*l=v1*l*v2=v1, by antisymmetry also u=v1 827** let v2'=\epsilon then v1*l*v2'=u and l*v2'=l<=l*v2. 828***********************************************************************) 829val PREFIX_FUSION_LEMMA = 830 store_thm 831 ("PREFIX_FUSION_LEMMA", 832 ``!v1 v2 l. 833 PREFIX (v1 * l) u /\ PREFIX u (v1 * l * v2) 834 ==> 835 ?v2'. (v1 * l * v2' = u) /\ PREFIX (l * v2') (l * v2)``, 836 RW_TAC list_ss [] 837 THEN Cases_on `IS_NEUTRAL v1` 838 THEN FULL_SIMP_TAC list_ss [GSYM CONC_ASSOC,CONC_def] 839 THENL 840 [PROVE_TAC[CONC_CANCEL,CONC_ASSOC,PREFIX_def], 841 Cases_on `v1` 842 THEN FULL_SIMP_TAC list_ss [CONC_def,IS_NEUTRAL_def] 843 THEN IMP_RES_TAC PREFIX_ANTISYM 844 THEN RW_TAC list_ss [] 845 THEN Q.EXISTS_TAC `v2` 846 THEN RW_TAC list_ss [PREFIX_def] 847 THEN Cases_on `l` 848 THEN RW_TAC list_ss 849 [CONC_def,GSYM CONC_ASSOC,CONC_CANCEL,IS_NEUTRAL_def] 850 THEN Cases_on `v2` 851 THEN RW_TAC list_ss [CONC_def,CONC_CANCEL,IS_NEUTRAL_def] 852 THEN Q.EXISTS_TAC `N[]` 853 THEN RW_TAC list_ss [CONC_def,CONC_CANCEL,IS_NEUTRAL_def]]); 854 855val TightPrefix_S_FUSION = 856 prove 857 (``(!w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r) /\ 858 (!w. WUS_SEM w r' ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r') 859 ==> 860 !w. WUS_SEM w (S_FUSION (r,r')) 861 ==> 862 !u. PREFIX u w ==> WUS_SEM (WEAKEN u) (S_FUSION (r,r'))``, 863 RW_TAC list_ss [WUS_SEM_def] 864 THEN Cases_on `STRICT_PREFIX u (v1 * l)` 865 THEN FULL_SIMP_TAC list_ss [CONC_def,GSYM CONC_ASSOC] 866 THENL 867 [FULL_SIMP_TAC list_ss [STRICT_PREFIX_def] 868 THEN RES_TAC 869 THEN Q.EXISTS_TAC `WEAKEN u` 870 THEN Q.EXISTS_TAC `v2` 871 THEN Q.EXISTS_TAC `l` 872 THEN RW_TAC list_ss [WEAKEN_def,CONC_def,CONC_WEAKEN], 873 `PREFIX (v1 * l) u` 874 by PROVE_TAC 875 [CONC_ASSOC,PREFIX_TRICHOTOMY,PREFIX_def,PREFIX_CONC,PREFIX_REFL] 876 THEN FULL_SIMP_TAC std_ss [CONC_ASSOC] 877 THEN `?v2'. (v1 * l * v2' = u) /\ PREFIX (l * v2') (l * v2)` 878 by PROVE_TAC[PREFIX_FUSION_LEMMA] 879 THEN `WUS_SEM (WEAKEN(l * v2')) r'` by PROVE_TAC[] 880 THEN `WUS_SEM (l * WEAKEN v2') r'` by PROVE_TAC[WEAKEN_CONC] 881 THEN Q.EXISTS_TAC `v1` 882 THEN Q.EXISTS_TAC `WEAKEN v2'` 883 THEN Q.EXISTS_TAC `l` 884 THEN `l * WEAKEN v2' = WEAKEN(l * v2')` by PROVE_TAC[WEAKEN_CONC] 885 THEN RW_TAC std_ss [GSYM CONC_ASSOC] 886 THEN REWRITE_TAC[WEAKEN_CONC], 887 FULL_SIMP_TAC list_ss [STRICT_PREFIX_def] 888 THEN RES_TAC 889 THEN Q.EXISTS_TAC `WEAKEN u` 890 THEN Q.EXISTS_TAC `v2` 891 THEN Q.EXISTS_TAC `W[]` 892 THEN RW_TAC list_ss [WEAKEN_def,CONC_def,CONC_WEAKEN], 893 RES_TAC 894 THEN Q.EXISTS_TAC `WEAKEN u` 895 THEN Q.EXISTS_TAC `v2` 896 THEN Q.EXISTS_TAC `W[]` 897 THEN RW_TAC list_ss [WEAKEN_def,CONC_def,CONC_WEAKEN]]); 898 899val TightPrefix_WS_CATN = 900 prove 901 (``(!w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r) 902 ==> 903 !n w. 904 WUS_SEM w (WS_CATN n r) 905 ==> 906 !u. PREFIX u w ==> WUS_SEM (WEAKEN u) (WS_CATN n r)``, 907 DISCH_TAC 908 THEN Induct 909 THEN RW_TAC list_ss [WS_CATN_def] 910 THEN RES_TAC 911 THEN IMP_RES_TAC TightPrefix_S_CAT); 912 913val PREFIX_N_EMPTY = 914 store_thm 915 ("PREFIX_N_EMPTY", 916 ``!w. PREFIX w (N[]) = (w = N[])``, 917 Cases_on `w` 918 THEN RW_TAC list_ss [CONC_def,WEAKEN_def,PREFIX_def] 919 THEN EQ_TAC 920 THEN RW_TAC list_ss [] 921 THENL 922 [Cases_on `u` 923 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct], 924 Q.EXISTS_TAC `N[]` 925 THEN RW_TAC list_ss [CONC_def]]); 926 927val PREFIX_W_EMPTY = 928 store_thm 929 ("PREFIX_W_EMPTY", 930 ``!w. PREFIX w (W[]) ==> (WEAKEN w = W[])``, 931 Cases_on `w` 932 THEN RW_TAC list_ss [CONC_def,WEAKEN_def,PREFIX_def] 933 THEN Cases_on `u` 934 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct]); 935 936val TightPrefix_S_REPEAT = 937 prove 938 (``!r. 939 (!w. S_CLOCK_FREE r /\ WUS_SEM w r ==> 940 !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r) ==> 941 !w. S_CLOCK_FREE (S_REPEAT r) /\ WUS_SEM w (S_REPEAT r) ==> 942 !u. PREFIX u w ==> WUS_SEM (WEAKEN u) (S_REPEAT r)``, 943 RW_TAC std_ss [S_CLOCK_FREE_def] 944 THEN `!w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r` 945 by PROVE_TAC[] 946 THEN IMP_RES_TAC TightPrefix_WS_CATN 947 THEN FULL_SIMP_TAC list_ss [WUS_SEM_REPEAT_WS_CATN] 948 THEN RW_TAC list_ss [] 949 THEN RES_TAC 950 THEN ZAP_TAC std_ss [PREFIX_N_EMPTY] 951 THEN FULL_SIMP_TAC list_ss [PREFIX_N_EMPTY,WEAKEN_def,A_distinct] 952 THEN Q.EXISTS_TAC `0` 953 THEN RW_TAC list_ss [WS_CATN_def,TightTrueEmpty]); 954 955val TightPrefix = 956 prove 957 (``!r. S_CLOCK_FREE r 958 ==> 959 !w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r``, 960 INDUCT_THEN sere_induct ASSUME_TAC 961 THENL 962 [(* S_BOOL b *) 963 PROVE_TAC[TightPrefix_S_BOOL], 964 (* S_CAT (r,r') *) 965 RW_TAC std_ss [S_CLOCK_FREE_def] 966 THEN `!w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r` 967 by PROVE_TAC[] 968 THEN `!w. WUS_SEM w r' ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r'` 969 by PROVE_TAC[] 970 THEN IMP_RES_TAC TightPrefix_S_CAT, 971 (* S_FUSION (r,r') *) 972 RW_TAC std_ss [S_CLOCK_FREE_def] 973 THEN `!w. WUS_SEM w r ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r` 974 by PROVE_TAC[] 975 THEN `!w. WUS_SEM w r' ==> !u. PREFIX u w ==> WUS_SEM (WEAKEN u) r'` 976 by PROVE_TAC[] 977 THEN IMP_RES_TAC TightPrefix_S_FUSION, 978 (* S_OR (r,r') *) 979 RW_TAC std_ss [WUS_SEM_def,S_CLOCK_FREE_def] 980 THEN PROVE_TAC[], 981 (* S_AND (r,r') *) 982 RW_TAC std_ss [WUS_SEM_def,S_CLOCK_FREE_def] 983 THEN PROVE_TAC[], 984 (* S_EMPTY *) 985 RW_TAC std_ss [WUS_SEM_def,S_CLOCK_FREE_def] 986 THEN Cases_on `u` 987 THEN FULL_SIMP_TAC list_ss [PREFIX_def,CONC_def,WEAKEN_def,A_distinct] 988 THEN Cases_on `u` 989 THEN FULL_SIMP_TAC list_ss 990 [PREFIX_def,CONC_def,WEAKEN_def,A_distinct,A_11], 991 (* S_REPEAT r *) 992 PROVE_TAC[TightPrefix_S_REPEAT], 993 (* S_CLOCK (r,c) *) 994 RW_TAC std_ss [S_CLOCK_FREE_def]]); 995 996val NEUTRAL_CONC_EQ = 997 store_thm 998 ("NEUTRAL_CONC_EQ", 999 ``!w v1 v2. (N w = v1 * v2) ==> ?w1 w2. (v1 = N w1) /\ (v2 = N w2)``, 1000 Cases_on `v1` THEN Cases_on `v2` 1001 THEN RW_TAC list_ss [CONC_def]); 1002 1003 1004val FOLDL_NW_FALSE = 1005 prove 1006 (``~(N w = FOLDL $* (W l) vlist)``, 1007 Induct_on `vlist` 1008 THEN RW_TAC list_ss [CONC_def]); 1009 1010val FOLDL_NS_FALSE = 1011 prove 1012 (``~(N w = FOLDL $* (S l) vlist)``, 1013 Induct_on `vlist` 1014 THEN RW_TAC list_ss [CONC_def]); 1015 1016val US_SEM_WUS_SEM_CATN = 1017 store_thm 1018 ("US_SEM_WUS_SEM_CATN", 1019 ``(!w. US_SEM w r = WUS_SEM (N w) r) 1020 ==> 1021 !n w. US_SEM w (WS_CATN n r) = WUS_SEM (N w) (WS_CATN n r)``, 1022 DISCH_TAC 1023 THEN Induct 1024 THEN RW_TAC list_ss [WS_CATN_def,US_SEM,WUS_SEM_def] 1025 THEN EQ_TAC 1026 THEN RW_TAC list_ss [] 1027 THENL 1028 [Q.EXISTS_TAC `N v1` THEN Q.EXISTS_TAC `N v2` 1029 THEN PROVE_TAC[CONC_def], 1030 Cases_on `v1` THEN Cases_on `v2` 1031 THEN FULL_SIMP_TAC list_ss [CONC_def,A_11,A_distinct,TOP_FREE_APPEND] 1032 THEN PROVE_TAC[]]); 1033 1034(*****************************************************************************) 1035(* Because this proof is tweaked from one for an earlier version with a *) 1036(* ``TOP_FREE w`` hypothesis, it is likely that it is more complicated *) 1037(* than needed. *) 1038(*****************************************************************************) 1039local 1040open FinitePathTheory; 1041val SIMP = 1042 RW_TAC list_ss 1043 [S_CLOCK_FREE_def,US_SEM_def,WUS_SEM_def,IS_STRONG_def,LEN_def,A_ELEM_def, 1044 ELEM_def,HEAD_def,RESTN_def]; 1045in 1046val TightNeutralEquiv = 1047 prove 1048 (``!r. S_CLOCK_FREE r ==> !w. US_SEM w r = WUS_SEM (N w) r``, 1049 INDUCT_THEN sere_induct ASSUME_TAC 1050 THENL 1051 [(* S_BOOL b *) 1052 SIMP, 1053 (* S_CAT (r,r') *) 1054 SIMP 1055 THEN EQ_TAC 1056 THEN RW_TAC list_ss [] 1057 THENL 1058 [Q.EXISTS_TAC `N v1` THEN Q.EXISTS_TAC `N v2` 1059 THEN RW_TAC list_ss [CONC_def], 1060 IMP_RES_TAC NEUTRAL_CONC_EQ 1061 THEN RW_TAC list_ss [] 1062 THEN FULL_SIMP_TAC list_ss [A_11,CONC_def] 1063 THEN Q.EXISTS_TAC `w1` THEN Q.EXISTS_TAC `w2` 1064 THEN RW_TAC list_ss []] 1065 THEN PROVE_TAC[TOP_FREE_APPEND], 1066 (* S_FUSION (r,r') *) 1067 SIMP 1068 THEN EQ_TAC 1069 THEN RW_TAC list_ss [] 1070 THEN FULL_SIMP_TAC list_ss [TOP_FREE_APPEND] 1071 THENL 1072 [Q.EXISTS_TAC `N v1` THEN Q.EXISTS_TAC `N v2` THEN Q.EXISTS_TAC `N[l]` 1073 THEN ZAP_TAC list_ss [CONC_def,IS_LETTER_def,TOP_FREE_APPEND] 1074 THEN RW_TAC list_ss [CONC_def] 1075 THEN `TOP_FREE([l]++v2)` by PROVE_TAC[TOP_FREE_APPEND] 1076 THEN FULL_SIMP_TAC list_ss [] 1077 THEN PROVE_TAC[], 1078 IMP_RES_TAC NEUTRAL_CONC_EQ 1079 THEN IMP_RES_TAC(GSYM NEUTRAL_CONC_EQ) 1080 THEN RW_TAC list_ss [] 1081 THEN FULL_SIMP_TAC list_ss [A_11,CONC_def,IS_LETTER_def] 1082 THEN RW_TAC list_ss [] 1083 THEN Q.EXISTS_TAC `w1'` THEN Q.EXISTS_TAC `w2` THEN Q.EXISTS_TAC `l` 1084 THEN FULL_SIMP_TAC list_ss [TOP_FREE_APPEND] 1085 THEN `TOP_FREE([l]++w2)` by PROVE_TAC[TOP_FREE_APPEND] 1086 THEN FULL_SIMP_TAC list_ss [] 1087 THEN PROVE_TAC[], 1088 IMP_RES_TAC NEUTRAL_CONC_EQ 1089 THEN IMP_RES_TAC(GSYM NEUTRAL_CONC_EQ) 1090 THEN RW_TAC list_ss [] 1091 THEN FULL_SIMP_TAC list_ss [A_distinct]], 1092 (* S_OR (r,r') *) 1093 SIMP, 1094 (* S_AND (r,r') *) 1095 SIMP, 1096 (* S_EMPTY *) 1097 SIMP, 1098 (* S_REPEAT r *) 1099 RW_TAC list_ss 1100 [WUS_SEM_REPEAT_WS_CATN,S_CLOCK_FREE_def,US_SEM_REPEAT_CATN] 1101 THEN EQ_TAC 1102 THEN RW_TAC list_ss [] 1103 THENL 1104 [`!w. US_SEM w r = WUS_SEM (N w) r` by PROVE_TAC[] 1105 THEN POP_ASSUM 1106 (fn th => ASSUME_TAC(GSYM(MATCH_MP US_SEM_WUS_SEM_CATN th))) 1107 THEN RW_TAC list_ss [US_SEM_WS_CATN] 1108 THEN Cases_on `n=0` 1109 THEN RW_TAC list_ss [] 1110 THEN FULL_SIMP_TAC list_ss [S_CATN_def,US_SEM] 1111 THEN `?m. n = SUC m` by Cooper.COOPER_TAC 1112 THEN DISJ2_TAC 1113 THEN Q.EXISTS_TAC `m` 1114 THEN RW_TAC list_ss [] 1115 THEN FULL_SIMP_TAC list_ss [S_CATN_def,US_SEM] 1116 THEN PROVE_TAC[], 1117 Q.EXISTS_TAC `0` 1118 THEN RW_TAC list_ss [S_CATN_def,US_SEM], 1119 `!w. US_SEM w r = WUS_SEM (N w) r` by PROVE_TAC[] 1120 THEN POP_ASSUM 1121 (fn th => ASSUME_TAC(GSYM(MATCH_MP US_SEM_WUS_SEM_CATN th))) 1122 THEN `US_SEM w (WS_CATN n r)` by PROVE_TAC[] 1123 THEN FULL_SIMP_TAC list_ss [US_SEM_WS_CATN] 1124 THEN PROVE_TAC[]], 1125 (* S_CLOCK (r,c) *) 1126 RW_TAC std_ss [S_CLOCK_FREE_def]]); 1127end; 1128 1129val _ = export_theory(); 1130 1131