1(*****************************************************************************) 2(* Create "ExecuteSemantics": a derived fixpoint-style executable semantics *) 3(* *) 4(* Created Wed Mar 19 19:01:20 GMT 2003 *) 5(*****************************************************************************) 6 7(*****************************************************************************) 8(* START BOILERPLATE *) 9(*****************************************************************************) 10 11(****************************************************************************** 12* Parent theories (comment out "load"s and "quietdec"s for compilation) 13******************************************************************************) 14 15(* 16*) 17quietdec := true; 18loadPath := ["../../path","../../regexp","../official-semantics"] @ !loadPath; 19app load ["bossLib","metisLib","intLib","res_quanTools","pred_setLib", 20 "rich_listTheory", "regexpLib", 21 "FinitePSLPathTheory","PSLPathTheory","SyntaxTheory", 22 "UnclockedSemanticsTheory","ClockedSemanticsTheory", 23 "SyntacticSugarTheory" 24 (*, "PropertiesTheory"*) 25 ]; 26 27open HolKernel Parse boolLib; 28open bossLib metisLib listTheory rich_listTheory pred_setLib intLib 29 arithmeticTheory; 30open regexpTheory matcherTheory; 31open FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 32 UnclockedSemanticsTheory ClockedSemanticsTheory 33 (* PropertiesTheory*); 34 35(* 36*) 37quietdec := false; 38 39(*****************************************************************************) 40(* END BOILERPLATE *) 41(*****************************************************************************) 42 43(****************************************************************************** 44* Start a new theory called "ExecuteSemantics" 45******************************************************************************) 46val _ = new_theory "ExecuteSemantics"; 47 48(****************************************************************************** 49* Set default parsing to natural numbers rather than integers 50******************************************************************************) 51val _ = intLib.deprecate_int(); 52 53(*---------------------------------------------------------------------------*) 54(* Symbolic tacticals. *) 55(*---------------------------------------------------------------------------*) 56 57infixr 0 ++ << || THENC ORELSEC ORELSER ##; 58infix 1 >>; 59 60val op ++ = op THEN; 61val op << = op THENL; 62val op >> = op THEN1; 63val op || = op ORELSE; 64val Know = Q_TAC KNOW_TAC; 65val Suff = Q_TAC SUFF_TAC; 66val REVERSE = Tactical.REVERSE; 67 68val pureDefine = with_flag (computeLib.auto_import_definitions,false) Define; 69 70(****************************************************************************** 71* A simpset fragment to rewrite away quantifiers restricted with :: (a to b) 72******************************************************************************) 73val resq_SS = 74 simpLib.merge_ss 75 [res_quanTools.resq_SS, 76 rewrites [IN_DEF,LESS_def,LESSX_def, 77 LS,GT,num_to_def,xnum_to_def,LENGTH_def]]; 78 79val std_resq_ss = simpLib.++ (std_ss, resq_SS); 80val arith_resq_ss = simpLib.++ (arith_ss, resq_SS); 81val list_resq_ss = simpLib.++ (list_ss, resq_SS); 82 83val arith_suc_ss = simpLib.++ (arith_ss, numSimps.SUC_FILTER_ss); 84 85(****************************************************************************** 86* Structural induction rule for SEREs (used to be in PropertiesTheory) 87******************************************************************************) 88val sere_induct = save_thm 89 ("sere_induct", 90 Q.GEN 91 `P` 92 (MATCH_MP 93 (DECIDE ``(A ==> (B1 /\ B2 /\ B3)) ==> (A ==> B1)``) 94 (SIMP_RULE 95 std_ss 96 [pairTheory.FORALL_PROD, 97 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 98 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 99 (Q.SPECL 100 [`P`,`\(r1,r2). P r1 /\ P r2`,`\(r,b). P r`] 101 (TypeBase.induction_of "sere"))))); 102 103(****************************************************************************** 104* S_CLOCK_FREE r means r contains no clocking statements 105* (used to be in PropertiesTheory) 106******************************************************************************) 107val S_CLOCK_FREE_def = 108 Define 109 `(S_CLOCK_FREE (S_BOOL b) = T) 110 /\ 111 (S_CLOCK_FREE (S_CAT(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 112 /\ 113 (S_CLOCK_FREE (S_FUSION(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 114 /\ 115 (S_CLOCK_FREE (S_OR(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 116 /\ 117 (S_CLOCK_FREE (S_AND(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 118 /\ 119 (S_CLOCK_FREE (S_REPEAT r) = S_CLOCK_FREE r) 120 /\ 121 (S_CLOCK_FREE (S_CLOCK v) = F)`; 122 123(****************************************************************************** 124* Neutrality 125******************************************************************************) 126 127(* 128 A list of letters is neutral iff it contains no occurrences of TOP or 129 BOTTOM 130*) 131 132val NEUTRAL_LIST_def = 133 Define 134 `(NEUTRAL_LIST[] = T) /\ 135 (NEUTRAL_LIST(TOP::p) = F) /\ 136 (NEUTRAL_LIST(BOTTOM::p) = F) /\ 137 (NEUTRAL_LIST(STATE f::p) = NEUTRAL_LIST p)`; 138 139val MAP_COMPLEMENT_LETTER_NEUTRAL_LIST = 140 store_thm 141 ("MAP_COMPLEMENT_LETTER_NEUTRAL_LIST", 142 ``!p. NEUTRAL_LIST p ==> (MAP COMPLEMENT_LETTER p = p)``, 143 Induct 144 THEN RW_TAC list_ss [COMPLEMENT_LETTER_def,NEUTRAL_LIST_def] 145 THEN Cases_on `h` 146 THEN FULL_SIMP_TAC list_ss [COMPLEMENT_LETTER_def,NEUTRAL_LIST_def]); 147 148val COMPLEMENT_FINITE_NEUTRAL_LIST = 149 store_thm 150 ("COMPLEMENT_FINITE_NEUTRAL_LIST", 151 ``!p. NEUTRAL_LIST p ==> (COMPLEMENT(FINITE p) = FINITE p)``, 152 Induct 153 THEN RW_TAC list_ss [COMPLEMENT_def,NEUTRAL_LIST_def] 154 THEN Cases_on `h` 155 THEN FULL_SIMP_TAC list_ss [COMPLEMENT_LETTER_def,NEUTRAL_LIST_def] 156 THEN RW_TAC std_ss [MAP_COMPLEMENT_LETTER_NEUTRAL_LIST]); 157 158(* A path is neutral iff it contains no occurrences of TOP or BOTTOM *) 159 160val NEUTRAL_PATH_def = 161 Define 162 `(NEUTRAL_PATH(FINITE p) = NEUTRAL_LIST p) /\ 163 (NEUTRAL_PATH(INFINITE f) = !n. ?s. f n = STATE s)`; 164 165val COMPLEMENT_NEUTRAL_PATH = 166 store_thm 167 ("COMPLEMENT_NEUTRAL_PATH", 168 ``NEUTRAL_PATH w ==> (COMPLEMENT w = w)``, 169 Cases_on `w` 170 THEN RW_TAC list_ss [NEUTRAL_PATH_def,COMPLEMENT_FINITE_NEUTRAL_LIST,COMPLEMENT_def] 171 THEN CONV_TAC FUN_EQ_CONV 172 THEN Induct 173 THEN RW_TAC std_ss [] 174 THEN PROVE_TAC[COMPLEMENT_LETTER_def]); 175 176(* Top-free and bottom-free *) 177val TOP_FREE_LIST_def = Define `TOP_FREE_LIST = EVERY (\x. ~(x = TOP))`; 178 179val BOTTOM_FREE_LIST_def = Define 180 `BOTTOM_FREE_LIST = EVERY (\x. ~(x = BOTTOM))`; 181 182val NEUTRAL_LIST = prove 183 (``!l. NEUTRAL_LIST l = TOP_FREE_LIST l /\ BOTTOM_FREE_LIST l``, 184 Induct 185 ++ RW_TAC std_ss 186 [NEUTRAL_LIST_def, TOP_FREE_LIST_def, BOTTOM_FREE_LIST_def, EVERY_DEF] 187 ++ Cases_on `h` 188 ++ RW_TAC std_ss 189 [NEUTRAL_LIST_def, TOP_FREE_LIST_def, BOTTOM_FREE_LIST_def, EVERY_DEF]); 190 191(****************************************************************************** 192* Evaluating boolean properties 193******************************************************************************) 194val B_SEMS_def = pureDefine `B_SEMS s b = B_SEM (STATE s) b`; 195 196val EVAL_B_SEMS = store_thm 197 ("EVAL_B_SEMS", 198 ``(B_SEMS l (B_PROP p) = p IN l) /\ 199 (B_SEMS l B_TRUE = T) /\ 200 (B_SEMS l B_FALSE = F) /\ 201 (B_SEMS l (B_NOT b) = ~(B_SEMS l b)) /\ 202 (B_SEMS l (B_AND (b1,b2)) = B_SEMS l b1 /\ B_SEMS l b2) /\ 203 (B_SEMS l (B_OR (b1,b2)) = B_SEMS l b1 \/ B_SEMS l b2) /\ 204 (B_SEMS l (B_IMP (b1,b2)) = (B_SEMS l b1 ==> B_SEMS l b2)) /\ 205 (B_SEMS l (B_IFF (b1,b2)) = (B_SEMS l b1 = B_SEMS l b2))``, 206 RW_TAC std_ss [B_SEMS_def,B_OR_def,B_IMP_def,B_IFF_def,B_SEM_def] 207 THEN PROVE_TAC []); 208 209val EVAL_B_SEM = store_thm 210 ("EVAL_B_SEM", 211 ``!l b. 212 B_SEM l b = 213 case l of TOP -> T || BOTTOM -> F || STATE s -> B_SEMS s b``, 214 Cases 215 ++ RW_TAC std_ss [B_SEM_def, B_SEMS_def]); 216 217(****************************************************************************** 218* Derived SEREs 219******************************************************************************) 220 221(* Empty only matches the empty string *) 222 223val S_EMPTY = store_thm 224 ("S_EMPTY", 225 ``!p. US_SEM p S_EMPTY = (p = [])``, 226 RW_TAC std_ss [US_SEM_def]); 227 228val S_EMPTY_CAT = store_thm 229 ("S_EMPTY_CAT", 230 ``!p a. US_SEM p (S_CAT (S_EMPTY, a)) = US_SEM p a``, 231 RW_TAC std_ss [US_SEM_def, S_EMPTY, APPEND]); 232 233(* Any matches any bottom-free string *) 234 235val S_ANY = store_thm 236 ("S_ANY", 237 ``!p. US_SEM p S_ANY = BOTTOM_FREE_LIST p``, 238 RW_TAC std_ss [S_ANY_def, BOTTOM_FREE_LIST_def] 239 ++ Induct_on `p` 240 ++ ONCE_REWRITE_TAC [US_SEM] 241 ++ RW_TAC std_ss [S_EMPTY, EVERY_DEF, LENGTH_NIL] 242 ++ RW_TAC std_ss [S_TRUE_def] 243 ++ Cases_on `p = []` >> RW_TAC std_ss [EVERY_DEF] 244 ++ RW_TAC std_ss [] 245 ++ REVERSE EQ_TAC 246 >> (RW_TAC std_ss [] 247 ++ Q.EXISTS_TAC `METIS_TAC [APPEND] 248 249 RW_TAC std_ss [S_ANY_def, BOTTOM_FREE_LIST_def] 250 ++ completeInduct_on `LENGTH p` 251 ++ ONCE_REWRITE_TAC [US_SEM] 252 ++ RW_TAC std_ss [S_EMPTY, EVERY_DEF, LENGTH_NIL] 253 ++ RW_TAC std_ss [S_TRUE_def] 254 ++ Cases_on `p = []` >> RW_TAC std_ss [EVERY_DEF] 255 ++ RW_TAC std_ss [] 256 ++ REVERSE EQ_TAC 257 >> (RW_TAC std_ss [] 258 ++ Q.EXISTS_TAC `METIS_TAC [APPEND] 259 260 ++ ONCE_REWRITE_TAC [US_SEM] 261 ++ RW_TAC std_ss [S_EMPTY, EVERY_DEF] 262 ++ Q.EXISTS_TAC `[h]` 263 ++ Q.EXISTS_TAC `p` 264 >> (RW_ 265 RW_TAC std_ss [S_ANY_def, US_SEM_def, B_SEM_def, S_TRUE_def] 266 ++ Q.EXISTS_TAC `MAP (\x. [x]) w` 267 ++ (RW_TAC std_ss [listTheory.EVERY_MAP, listTheory.LENGTH] 268 ++ RW_TAC std_ss [listTheory.EVERY_MEM]) 269 ++ Induct_on `w` 270 ++ RW_TAC std_ss [CONCAT_def, MAP, APPEND] 271 ++ PROVE_TAC []); 272 273val US_SEM_REPEAT_TRUE = store_thm 274 ("US_SEM_REPEAT_TRUE", 275 ``!w. US_SEM w (S_REPEAT S_TRUE)``, 276 RW_TAC std_ss [US_SEM_def, B_SEM, S_TRUE_def] 277 ++ Q.EXISTS_TAC `MAP (\x. [x]) w` 278 ++ (RW_TAC std_ss [listTheory.EVERY_MAP, listTheory.LENGTH] 279 ++ RW_TAC std_ss [listTheory.EVERY_MEM]) 280 ++ Induct_on `w` 281 ++ RW_TAC std_ss [CONCAT_def, MAP, APPEND] 282 ++ PROVE_TAC []); 283 284 285(****************************************************************************** 286* Executable semantics of [f1 U f2] 287* w |= [f1 U f2] 288* <==> 289* |w| > 0 And (w |= f2 Or (w |= f1 And w^1 |= [f1 U f2])) 290******************************************************************************) 291val UF_SEM_F_UNTIL_REC = 292 store_thm 293 ("UF_SEM_F_UNTIL_REC", 294 ``UF_SEM w (F_UNTIL(f1,f2)) = 295 LENGTH w > 0 296 /\ 297 (UF_SEM w f2 298 \/ 299 (UF_SEM w f1 /\ UF_SEM (RESTN w 1) (F_UNTIL(f1,f2))))``, 300 RW_TAC arith_resq_ss [UF_SEM_def] 301 THEN Cases_on `w` 302 THEN ONCE_REWRITE_TAC[arithmeticTheory.ONE] 303 THEN RW_TAC arith_resq_ss 304 [num_to_def,xnum_to_def,RESTN_def,REST_def,LENGTH_def] 305 THEN EQ_TAC 306 THEN RW_TAC arith_ss [] 307 THENL 308 [DECIDE_TAC, 309 Cases_on `UF_SEM (FINITE l) f2` 310 THEN RW_TAC std_ss [] 311 THEN Cases_on `k=0` 312 THEN RW_TAC arith_ss [] 313 THEN FULL_SIMP_TAC std_ss [RESTN_def] 314 THEN `0 < k` by DECIDE_TAC 315 THEN RES_TAC 316 THENL 317 [PROVE_TAC[RESTN_def], 318 `k - 1 < LENGTH l - 1` by DECIDE_TAC 319 THEN Q.EXISTS_TAC `k-1` 320 THEN RW_TAC arith_ss [LENGTH_TL] 321 THENL 322 [`k = SUC(k-1)` by DECIDE_TAC 323 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SUBS[el 1 thl] (el 8 thl))) 324 THEN FULL_SIMP_TAC std_ss [RESTN_def,REST_def], 325 `SUC j < k` by DECIDE_TAC 326 THEN RES_TAC 327 THEN FULL_SIMP_TAC std_ss [REST_def, RESTN_def]]], 328 Q.EXISTS_TAC `0` 329 THEN RW_TAC arith_ss [RESTN_def], 330 `LENGTH (TL l) = LENGTH l - 1` by RW_TAC arith_ss [LENGTH_TL] 331 THEN `SUC k < LENGTH l` by DECIDE_TAC 332 THEN Q.EXISTS_TAC `SUC k` 333 THEN RW_TAC std_ss [RESTN_def,REST_def] 334 THEN Cases_on `j=0` 335 THEN RW_TAC std_ss [RESTN_def] 336 THEN `j - 1 < k` by DECIDE_TAC 337 THEN RES_TAC 338 THEN `j = SUC(j-1)` by DECIDE_TAC 339 THEN POP_ASSUM(fn th => SUBST_TAC[th]) 340 THEN RW_TAC std_ss [RESTN_def,REST_def], 341 Cases_on `UF_SEM (INFINITE f) f2` 342 THEN RW_TAC std_ss [] 343 THEN Cases_on `k=0` 344 THEN RW_TAC arith_ss [] 345 THEN FULL_SIMP_TAC std_ss [RESTN_def] 346 THEN `0 < k` by DECIDE_TAC 347 THEN RES_TAC 348 THEN FULL_SIMP_TAC std_ss [RESTN_def,GSYM REST_def] 349 THEN `k = SUC(k-1)` by DECIDE_TAC 350 THEN ASSUM_LIST(fn thl => ASSUME_TAC(SUBS[el 1 thl] (el 7 thl))) 351 THEN FULL_SIMP_TAC std_ss [RESTN_def] 352 THEN Q.EXISTS_TAC `k-1` 353 THEN RW_TAC std_ss [] 354 THEN `SUC j < k` by DECIDE_TAC 355 THEN PROVE_TAC[RESTN_def], 356 Q.EXISTS_TAC `0` 357 THEN RW_TAC arith_ss [RESTN_def], 358 Q.EXISTS_TAC `SUC k` 359 THEN FULL_SIMP_TAC std_ss [GSYM REST_def] 360 THEN RW_TAC std_ss [RESTN_def] 361 THEN Cases_on `j=0` 362 THEN RW_TAC std_ss [RESTN_def] 363 THEN `j - 1 < k` by DECIDE_TAC 364 THEN RES_TAC 365 THEN `j = SUC(j-1)` by DECIDE_TAC 366 THEN POP_ASSUM(fn th => SUBST_TAC[th]) 367 THEN RW_TAC std_ss [RESTN_def]]); 368 369(****************************************************************************** 370* Executable semantics of {r}(f) on finite paths. 371* 372* First define w |=_n f 373* 374* w |=_0 {r}(f) 375* 376* w |=_{n+1} {r}(f) 377* <==> 378* w |=_n {r}(f) And (w^{0,n} |= r Implies w^n |= f) 379* 380* then 381* 382* w |= {r}(f) <==> w |=_|w| {r}(f) 383******************************************************************************) 384val UF_SEM_F_SUFFIX_IMP_FINITE_REC_def = 385 Define 386 `(UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) 0 = T) 387 /\ 388 (UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) (SUC n) = 389 UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) n 390 /\ 391 (US_SEM (SEL w (0, n)) r ==> UF_SEM (RESTN w n) f))`; 392 393(****************************************************************************** 394* Form needed for computeLib.EVAL 395******************************************************************************) 396val UF_SEM_F_SUFFIX_IMP_FINITE_REC_AUX = 397 store_thm 398 ("UF_SEM_F_SUFFIX_IMP_FINITE_REC_AUX", 399 ``UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) n = 400 (n = 0) \/ 401 (UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) (n-1) 402 /\ 403 (US_SEM (SEL w (0, (n-1))) r ==> UF_SEM (RESTN w (n-1)) f))``, 404 Cases_on `n` 405 THEN RW_TAC arith_ss [UF_SEM_F_SUFFIX_IMP_FINITE_REC_def]); 406 407(****************************************************************************** 408* UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL 409* 410* (All j < n: w^{0,j} |= r Implies w^j |= f) = w |=_n {r}(f) 411******************************************************************************) 412local 413val UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL1 = 414 prove 415 (``(!j. j < n ==> US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f) 416 ==> 417 UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) n``, 418 Induct_on `n` 419 THEN RW_TAC arith_ss [UF_SEM_F_SUFFIX_IMP_FINITE_REC_def]); 420 421val UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL2 = 422 prove 423 (``UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) n 424 ==> 425 (!j. j < n ==> US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f)``, 426 Induct_on `n` 427 THEN RW_TAC arith_ss [UF_SEM_F_SUFFIX_IMP_FINITE_REC_def] 428 THEN Cases_on `j=n` 429 THEN RW_TAC std_ss [] 430 THEN `j < n` by DECIDE_TAC 431 THEN PROVE_TAC[]); 432in 433val UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL = 434 store_thm 435 ("UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL", 436 ``(!j. j < n ==> US_SEM (SEL w (0,j)) r ==> UF_SEM (RESTN w j) f) 437 = 438 UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) n``, 439 PROVE_TAC[UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL1,UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL2]); 440end; 441 442(****************************************************************************** 443* w |= {r}(f) <==> w |=_|w| {r}(f) 444******************************************************************************) 445val UF_SEM_F_SUFFIX_IMP_FINITE_REC = 446 store_thm 447 ("UF_SEM_F_SUFFIX_IMP_FINITE_REC", 448 ``NEUTRAL_LIST w 449 ==> 450 (UF_SEM (FINITE w) (F_SUFFIX_IMP(r,f)) = 451 UF_SEM_F_SUFFIX_IMP_FINITE_REC (FINITE w) (r,f) (LENGTH w))``, 452 RW_TAC list_resq_ss [UF_SEM_def] 453 THEN PROVE_TAC 454 [UF_SEM_F_SUFFIX_IMP_FINITE_REC_FORALL,COMPLEMENT_FINITE_NEUTRAL_LIST]); 455 456(****************************************************************************** 457* Define w |=_x {r}(f) where x is an extended number (xnum) 458******************************************************************************) 459val UF_SEM_F_SUFFIX_IMP_REC_def = 460 Define 461 `(UF_SEM_F_SUFFIX_IMP_REC w (r,f) (XNUM n) = 462 UF_SEM_F_SUFFIX_IMP_FINITE_REC w (r,f) n) 463 /\ 464 (UF_SEM_F_SUFFIX_IMP_REC w (r,f) INFINITY = 465 !n. US_SEM (SEL w (0,n)) r ==> UF_SEM (RESTN w n) f)`; 466 467(****************************************************************************** 468* w |= {r}(f) <==> w |=_|w| {r}(f) (for finite and infinite paths w) 469******************************************************************************) 470val UF_SEM_F_SUFFIX_IMP_REC = 471 store_thm 472 ("UF_SEM_F_SUFFIX_IMP_REC", 473 ``NEUTRAL_PATH w 474 ==> 475 (UF_SEM w (F_SUFFIX_IMP(r,f)) = 476 UF_SEM_F_SUFFIX_IMP_REC w (r,f) (LENGTH w))``, 477 Cases_on `w` 478 THEN RW_TAC list_resq_ss 479 [UF_SEM_def,UF_SEM_F_SUFFIX_IMP_FINITE_REC,NEUTRAL_PATH_def, 480 UF_SEM_F_SUFFIX_IMP_REC_def,COMPLEMENT_NEUTRAL_PATH]); 481 482(*---------------------------------------------------------------------------*) 483(* Converting regexps from SyntaxTheory to regexpTheory. *) 484(*---------------------------------------------------------------------------*) 485 486val CONCAT_is_CONCAT = prove 487 (``FinitePSLPath$CONCAT = regexp$CONCAT``, 488 RW_TAC std_ss [FUN_EQ_THM] 489 ++ Induct_on `x` 490 ++ RW_TAC std_ss [FinitePSLPathTheory.CONCAT_def, regexpTheory.CONCAT_def]); 491 492val RESTN_is_BUTFIRSTN = prove 493 (``!n l. n <= LENGTH l ==> (RESTN l n = BUTFIRSTN n l)``, 494 Induct_on `l` 495 >> RW_TAC arith_ss [LENGTH, BUTFIRSTN, FinitePSLPathTheory.RESTN_def] 496 ++ GEN_TAC 497 ++ Cases >> RW_TAC arith_ss [LENGTH, BUTFIRSTN, FinitePSLPathTheory.RESTN_def] 498 ++ RW_TAC arith_ss 499 [LENGTH, BUTFIRSTN, FinitePSLPathTheory.RESTN_def, 500 FinitePSLPathTheory.REST_def, TL]); 501 502val SEL_FINITE_is_BUTFIRSTN_FIRSTN = prove 503 (``!j k l. 504 j <= k /\ k < LENGTH l ==> 505 (SEL (FINITE l) (j,k) = BUTFIRSTN j (FIRSTN (SUC k) l))``, 506 SIMP_TAC std_ss [SEL_def] 507 ++ Induct_on `l` >> RW_TAC arith_ss [LENGTH, FIRSTN] 508 ++ GEN_TAC 509 ++ GEN_TAC 510 ++ Cases 511 >> (ONCE_REWRITE_TAC [SEL_REC_AUX] 512 ++ RW_TAC arith_ss [LENGTH, FIRSTN, HEAD_def, HD] 513 ++ ONCE_REWRITE_TAC [SEL_REC_AUX] 514 ++ RW_TAC arith_ss [BUTFIRSTN]) 515 ++ FULL_SIMP_TAC arith_ss [LENGTH] 516 ++ ONCE_REWRITE_TAC [SEL_REC_AUX] 517 ++ RW_TAC arith_ss 518 [LENGTH, FIRSTN, arithmeticTheory.ADD1, HEAD_def, HD, REST_def, TL, 519 BUTFIRSTN] 520 << [Q.PAT_ASSUM `!j. P j` (MP_TAC o Q.SPECL [`0`, `n`]) 521 ++ RW_TAC arith_ss [BUTFIRSTN, arithmeticTheory.ADD1], 522 Q.PAT_ASSUM `!j. P j` (MP_TAC o Q.SPECL [`j - 1`, `n`]) 523 ++ RW_TAC arith_ss [BUTFIRSTN, arithmeticTheory.ADD1] 524 ++ Cases_on `j` 525 ++ RW_TAC arith_ss [BUTFIRSTN]]); 526 527val sere2regexp_def = Define 528 `(sere2regexp (S_BOOL b) = Atom (\l. B_SEM l b)) /\ 529 (sere2regexp (S_CAT (r1, r2)) = Cat (sere2regexp r1) (sere2regexp r2)) /\ 530 (sere2regexp (S_FUSION (r1, r2)) = Fuse (sere2regexp r1) (sere2regexp r2)) /\ 531 (sere2regexp (S_OR (r1, r2)) = Or (sere2regexp r1) (sere2regexp r2)) /\ 532 (sere2regexp (S_AND (r1, r2)) = And (sere2regexp r1) (sere2regexp r2)) /\ 533 (sere2regexp S_EMPTY = One) /\ 534 (sere2regexp (S_REPEAT r) = Repeat (sere2regexp r))`; 535 536val sere2regexp = prove 537 (``!r l. S_CLOCK_FREE r ==> (US_SEM l r = sem (sere2regexp r) l)``, 538 INDUCT_THEN sere_induct ASSUME_TAC 539 ++ RW_TAC std_ss 540 [US_SEM_def, sem_def, sere2regexp_def, sem_One, 541 ELEM_EL, EL, S_CLOCK_FREE_def] 542 ++ CONV_TAC (DEPTH_CONV ETA_CONV) 543 ++ RW_TAC std_ss [CONCAT_is_CONCAT]); 544 545val EVAL_US_SEM = store_thm 546 ("EVAL_US_SEM", 547 ``!l r. 548 US_SEM l r = 549 if S_CLOCK_FREE r then amatch (sere2regexp r) l else US_SEM l r``, 550 RW_TAC std_ss [GSYM sere2regexp, amatch]); 551 552(****************************************************************************** 553* Evaluating suffix implication of finite neutral paths with clockfree regexps 554******************************************************************************) 555val EVAL_UF_SEM_F_SUFFIX_IMP = store_thm 556 ("EVAL_UF_SEM_F_SUFFIX_IMP", 557 ``!w r f. 558 UF_SEM (FINITE w) (F_SUFFIX_IMP (r,f)) = 559 if S_CLOCK_FREE r /\ NEUTRAL_LIST w then 560 acheck (sere2regexp r) (\x. UF_SEM (FINITE x) f) w 561 else UF_SEM (FINITE w) (F_SUFFIX_IMP (r,f))``, 562 RW_TAC list_resq_ss [acheck, UF_SEM_def, sere2regexp, RESTN_FINITE] 563 ++ RW_TAC arith_ss 564 [RESTN_is_BUTFIRSTN, SEL_FINITE_is_BUTFIRSTN_FIRSTN, BUTFIRSTN, 565 COMPLEMENT_FINITE_NEUTRAL_LIST] 566 ++ METIS_TAC []); 567 568(****************************************************************************** 569* Strong seres 570******************************************************************************) 571val FINITE_UF_SEM_F_STRONG_SERE = store_thm 572 ("FINITE_UF_SEM_F_STRONG_SERE", 573 ``!w r. 574 UF_SEM (FINITE w) (F_STRONG_SERE r) = 575 US_SEM w (S_CAT (r,S_ANY))``, 576 577 if NEUTRAL_LIST w /\ CLOCK_FREE r then 578 US_SEM 579 UF_SEM (FINITE w) 580 (F_SUFFIX_IMP (r1, F_NOT (F_SUFFIX_IMP (r2, F_STRONG_BOOL B_FALSE)))))``, 581 NEUTRAL_LIST w 582 ==> 583 (UF_SEM (FINITE w) (F_STRONG_IMP (r1,r2)) = 584 UF_SEM (FINITE w) 585 (F_SUFFIX_IMP (r1, F_NOT (F_SUFFIX_IMP (r2, F_STRONG_BOOL B_FALSE)))))``, 586 RW_TAC list_resq_ss [UF_SEM_def, B_SEM_def, AND_IMP_INTRO] 587 ++ HO_MATCH_MP_TAC 588 (METIS_PROVE [] 589 ``(!j. P j ==> (Q j = R j)) ==> ((!j. P j ==> Q j) = !j. P j ==> R j)``) 590 ++ RW_TAC std_ss [] 591 ++ HO_MATCH_MP_TAC 592 (METIS_PROVE [] 593 ``!R. (!k. P k ==> (?k'. k = k' + j)) /\ (!k. P (k + j) = Q k) ==> 594 ((?j. P j) = ?j. Q j)``) 595 ++ CONJ_TAC 596 >> (RW_TAC std_ss [] 597 ++ Q.EXISTS_TAC `k - j` 598 ++ RW_TAC arith_ss []) 599 ++ RW_TAC arith_ss [] 600 ++ Know `(j,j+j') = (j+0,j+j')` >> RW_TAC arith_ss [] 601 ++ DISCH_THEN (fn th => REWRITE_TAC [th, GSYM SEL_RESTN]) 602 ++ MATCH_MP_TAC (PROVE [] ``(a ==> (b = c)) ==> (b /\ a = c /\ a)``) 603 ++ STRIP_TAC 604 ++ RW_TAC arith_ss [xnum_to_def, RESTN_FINITE, LENGTH_def] 605 ++ RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN]); 606 607val INFINITE_UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP = store_thm 608 ("INFINITE_UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP", 609 ``!p r1 r2. 610 UF_SEM (INFINITE p) (F_STRONG_IMP (r1,r2)) = 611 UF_SEM (INFINITE p) 612 (F_SUFFIX_IMP (r1, F_NOT (F_SUFFIX_IMP (r2, F_BOOL B_FALSE))))``, 613 RW_TAC list_resq_ss [UF_SEM_def, B_SEM, AND_IMP_INTRO] 614 THEN HO_MATCH_MP_TAC (* MJCG tried using ++, <<, but it wouldn't parse *) 615 (METIS_PROVE [] 616 ``(!j. P j ==> (Q j = R j)) ==> ((!j. P j ==> Q j) = !j. P j ==> R j)``) 617 THEN RW_TAC arith_ss [LENGTH_RESTN_INFINITE,xnum_to_def,SEL_RESTN] 618 THEN EQ_TAC 619 THEN RW_TAC std_ss [] 620 THENL[Q.EXISTS_TAC `k-j`, Q.EXISTS_TAC `j+j'`] 621 THEN RW_TAC arith_ss []); 622 623val UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP = store_thm 624 ("UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP", 625 ``!w r1 r2. 626 UF_SEM w (F_STRONG_IMP (r1,r2)) = 627 UF_SEM w 628 (F_SUFFIX_IMP (r1, F_NOT (F_SUFFIX_IMP (r2, F_BOOL B_FALSE))))``, 629 Cases_on `w` 630 THEN PROVE_TAC 631 [FINITE_UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP, 632 INFINITE_UF_SEM_F_STRONG_IMP_F_SUFFIX_IMP]); 633 634(****************************************************************************** 635* Weak implication 636******************************************************************************) 637val BUTFIRSTN_FIRSTN = prove 638 (``!n k l. 639 k + n <= LENGTH l ==> 640 (BUTFIRSTN n (FIRSTN (k + n) l) = FIRSTN k (BUTFIRSTN n l))``, 641 Induct 642 ++ GEN_TAC 643 ++ Cases 644 ++ RW_TAC arith_ss [BUTFIRSTN, FIRSTN, HD, TL, LENGTH, arithmeticTheory.ADD] 645 ++ Q.PAT_ASSUM `!x. P x` (MP_TAC o GSYM o Q.SPECL [`k`, `t`]) 646 ++ RW_TAC arith_ss [] 647 ++ RW_TAC arith_ss [BUTFIRSTN, FIRSTN, arithmeticTheory.ADD_CLAUSES]); 648 649val UF_SEM_F_WEAK_IMP_FINITE = prove 650 (``!w r1 r2. 651 UF_SEM (FINITE w) (F_WEAK_IMP (r1,r2)) = 652 !j :: (0 to LENGTH w). 653 US_SEM (SEL (FINITE w) (0,j)) r1 654 ==> 655 (?k :: (j to LENGTH w). US_SEM (SEL (FINITE w) (j,k)) r2) 656 \/ 657 ?w'. US_SEM (SEL (FINITE w) (j, LENGTH w - 1) <> w') r2``, 658 RW_TAC list_resq_ss [UF_SEM_def] 659 ++ ONCE_REWRITE_TAC [PROVE [] ``a \/ b = ~a ==> b``] 660 ++ REWRITE_TAC [AND_IMP_INTRO] 661 ++ HO_MATCH_MP_TAC 662 (METIS_PROVE [] 663 ``(!j. A j ==> (B j = C j)) ==> ((!j. A j ==> B j) = !j. A j ==> C j)``) 664 ++ RW_TAC std_ss [] 665 ++ EQ_TAC 666 >> (DISCH_THEN (MP_TAC o Q.SPEC `LENGTH (w : ('a -> bool) list) - 1`) 667 ++ RW_TAC arith_ss []) 668 ++ RW_TAC std_ss [] 669 ++ Cases_on `k = LENGTH w - 1` >> METIS_TAC [] 670 ++ Q.EXISTS_TAC `SEL (FINITE w) (k + 1, LENGTH w - 1) <> w'` 671 ++ RW_TAC arith_ss [APPEND_ASSOC, GSYM SEL_SPLIT]); 672 673val EVAL_UF_SEM_F_WEAK_IMP = store_thm 674 ("EVAL_UF_SEM_F_WEAK_IMP", 675 ``!w r1 r2. 676 UF_SEM (FINITE w) (F_WEAK_IMP (r1,r2)) = 677 if S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2 then 678 acheck (sere2regexp r1) 679 (\x. 680 UF_SEM (FINITE x) (F_NOT (F_SUFFIX_IMP (r2, F_BOOL B_FALSE))) \/ 681 amatch (Prefix (sere2regexp r2)) x) w 682 else UF_SEM (FINITE w) (F_WEAK_IMP (r1,r2))``, 683 RW_TAC list_resq_ss 684 [UF_SEM_F_WEAK_IMP_FINITE, acheck, amatch, sere2regexp] 685 ++ ONCE_REWRITE_TAC [UF_SEM_def] 686 ++ ONCE_REWRITE_TAC [EVAL_UF_SEM_F_SUFFIX_IMP] 687 ++ RW_TAC arith_ss 688 [acheck, RESTN_is_BUTFIRSTN, SEL_FINITE_is_BUTFIRSTN_FIRSTN, sem_def, 689 BUTFIRSTN] 690 ++ RW_TAC std_ss [AND_IMP_INTRO] 691 ++ HO_MATCH_MP_TAC 692 (METIS_PROVE [] 693 ``(!j. A j ==> (B j = C j)) ==> ((!j. A j ==> B j) = !j. A j ==> C j)``) 694 ++ RW_TAC std_ss [] 695 ++ MATCH_MP_TAC (PROVE [] ``(a = b) /\ (c = d) ==> (a \/ c = b \/ d)``) 696 ++ REVERSE CONJ_TAC 697 >> (Know `SUC (LENGTH w - 1) = LENGTH w` >> DECIDE_TAC 698 ++ RW_TAC std_ss [FIRSTN_LENGTH_ID]) 699 ++ RW_TAC arith_ss [UF_SEM_def, B_SEM] 700 ++ HO_MATCH_MP_TAC 701 (METIS_PROVE [] 702 ``!f. 703 (!j. A j ==> ?x. f x = j) /\ (!j. A (f j) = B j) ==> 704 ((?j. A j) = ?j. B j)``) 705 ++ Q.EXISTS_TAC `\k. k + n` 706 ++ RW_TAC arith_ss [] >> (Q.EXISTS_TAC `k - n` ++ RW_TAC arith_ss []) 707 ++ RW_TAC arith_ss [LENGTH_BUTFIRSTN] 708 ++ Cases_on `n + n' < LENGTH w` 709 ++ RW_TAC arith_ss [SEL_FINITE_is_BUTFIRSTN_FIRSTN] 710 ++ AP_TERM_TAC 711 ++ Know `SUC (n + n') <= LENGTH w` >> DECIDE_TAC 712 ++ POP_ASSUM_LIST (K ALL_TAC) 713 ++ Know `SUC (n + n') = SUC n' + n` >> DECIDE_TAC 714 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 715 ++ METIS_TAC [BUTFIRSTN_FIRSTN]); 716 717(****************************************************************************** 718* always{r} = {T[*]} |-> {r} 719******************************************************************************) 720val F_SERE_ALWAYS_def = Define 721 `F_SERE_ALWAYS r = F_WEAK_IMP(S_REPEAT S_TRUE, r)`; 722 723(****************************************************************************** 724* never{r} = {T[*];r} |-> {F} 725******************************************************************************) 726val F_SERE_NEVER_def = Define 727 `F_SERE_NEVER r = F_WEAK_IMP(S_CAT(S_REPEAT S_TRUE, r), S_FALSE)`; 728 729val F_SERE_NEVER_amatch = store_thm 730 ("F_SERE_NEVER_amatch", 731 ``!r w. 732 S_CLOCK_FREE r /\ IS_INFINITE w ==> 733 (UF_SEM w (F_SERE_NEVER r) = 734 !n. ~amatch (sere2regexp (S_CAT (S_REPEAT S_TRUE,r))) (SEL w (0,n)))``, 735 RW_TAC std_ss [F_SERE_NEVER_def] 736 ++ Know `LENGTH w = INFINITY` 737 >> PROVE_TAC [PSLPathTheory.IS_INFINITE_EXISTS, PSLPathTheory.LENGTH_def] 738 ++ RW_TAC list_resq_ss [UF_SEM_def, xnum_to_def] 739 ++ Know `!l. US_SEM l S_FALSE = F` 740 >> RW_TAC std_ss [US_SEM_def, S_FALSE_def, B_SEM] 741 ++ DISCH_THEN (fn th => RW_TAC std_ss [th]) 742 ++ ONCE_REWRITE_TAC [EVAL_US_SEM] 743 ++ RW_TAC std_ss [S_CLOCK_FREE_def, S_TRUE_def] 744 ++ Suff `!j : num. (!k : num. ~(j <= k)) = F` 745 >> DISCH_THEN (fn th => REWRITE_TAC [th]) 746 ++ RW_TAC std_ss [] 747 ++ PROVE_TAC [arithmeticTheory.LESS_EQ_REFL]); 748 749(****************************************************************************** 750* Generating FSA checkers for the simple subset of PSL. 751******************************************************************************) 752 753(* Lemmas *) 754 755val ELEM_SEL = store_thm 756 ("ELEM_SEL", 757 ``!w i. ELEM (SEL w (0,i)) 0 = ELEM w 0``, 758 Cases 759 ++ RW_TAC arith_ss 760 [FinitePSLPathTheory.ELEM_def, FinitePSLPathTheory.RESTN_def, 761 FinitePSLPathTheory.HEAD_def, ELEM_def, RESTN_def, SEL_def] 762 ++ REWRITE_TAC [GSYM arithmeticTheory.ADD1, SEL_REC_def, HEAD_def, HD]); 763 764val US_SEM_APPEND = store_thm 765 ("US_SEM_APPEND", 766 ``!r r' w w'. 767 US_SEM w r /\ US_SEM w' r' ==> US_SEM (APPEND w w') (S_CAT (r,r'))``, 768 RW_TAC std_ss [] 769 ++ ONCE_REWRITE_TAC [US_SEM_def] 770 ++ Q.EXISTS_TAC `w` 771 ++ Q.EXISTS_TAC `w'` 772 ++ RW_TAC std_ss []); 773 774val CONCAT_EMPTY = store_thm 775 ("CONCAT_EMPTY", 776 ``!l. (FinitePSLPath$CONCAT l = []) = EVERY (\x. x = []) l``, 777 Induct 778 ++ RW_TAC std_ss [CONCAT_def, listTheory.EVERY_DEF, 779 listTheory.APPEND_eq_NIL]); 780 781val EMPTY_CONCAT = store_thm 782 ("EMPTY_CONCAT", 783 ``!l. ([] = FinitePSLPath$CONCAT l) = EVERY (\x. x = []) l``, 784 PROVE_TAC [CONCAT_EMPTY]); 785 786val S_FLEX_AND_EMPTY = store_thm 787 ("S_FLEX_AND_EMPTY", 788 ``!f g. US_SEM [] (S_FLEX_AND (f,g)) = US_SEM [] f /\ US_SEM [] g``, 789 RW_TAC std_ss [US_SEM_def, S_FLEX_AND_def, S_TRUE_def, B_SEM, 790 listTheory.APPEND_eq_NIL, EMPTY_CONCAT, 791 GSYM listTheory.EVERY_CONJ] 792 ++ RW_TAC (simpLib.++ (arith_ss, boolSimps.CONJ_ss)) [LENGTH] 793 ++ RW_TAC std_ss [ALL_EL_F]); 794 795val SEL_NIL = store_thm 796 ("SEL_NIL", 797 ``!n p. ~(SEL p (0,n) = [])``, 798 RW_TAC arith_suc_ss [SEL_def, SEL_REC_def]); 799 800val SEL_INIT_APPEND = store_thm 801 ("SEL_INIT_APPEND", 802 ``!p w. 803 (?l n. SEL p (0,n) = APPEND w l) ==> 804 (w = []) \/ (SEL p (0, LENGTH w - 1) = w)``, 805 Induct_on `w` >> RW_TAC std_ss [] 806 ++ RW_TAC std_ss [] 807 ++ POP_ASSUM MP_TAC 808 ++ Cases_on `n` 809 >> RW_TAC arith_suc_ss [APPEND, LENGTH, arithmeticTheory.PRE_SUB1, 810 listTheory.APPEND_eq_NIL, SEL_def, SEL_REC_def] 811 ++ Know `!l. ~(l = []) ==> (l = HD l :: TL l)` 812 >> (Cases ++ RW_TAC std_ss [HD, TL]) 813 ++ DISCH_THEN (MP_TAC o Q.SPEC `SEL p (0,SUC n')`) 814 ++ SIMP_TAC std_ss [SEL_NIL] 815 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 816 ++ RW_TAC std_ss [TL_SEL0, HD_SEL0, APPEND] 817 ++ Know `!l. ~(l = []) ==> (l = HD l :: TL l)` 818 >> (Cases ++ RW_TAC std_ss [HD, TL]) 819 ++ DISCH_THEN (MP_TAC o Q.SPEC `SEL p (0, LENGTH (HEAD p :: w) - 1)`) 820 ++ SIMP_TAC std_ss [SEL_NIL] 821 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 822 ++ RW_TAC arith_ss [TL_SEL0, HD_SEL0, LENGTH] 823 ++ REPEAT (POP_ASSUM MP_TAC) 824 ++ Cases_on `LENGTH w` 825 >> (POP_ASSUM MP_TAC 826 ++ RW_TAC arith_suc_ss [LENGTH_NIL, SEL_def, SEL_REC_def, TL]) 827 ++ RW_TAC arith_ss [TL_SEL0] 828 ++ Know `~(w = [])` 829 >> (STRIP_TAC 830 ++ Q.PAT_ASSUM `LENGTH w = SUC n` MP_TAC 831 ++ RW_TAC std_ss [LENGTH]) 832 ++ REWRITE_TAC [IMP_DISJ_THM] 833 ++ FIRST_ASSUM MATCH_MP_TAC 834 ++ PROVE_TAC []); 835 836val CAT_APPEND = store_thm 837 ("CAT_APPEND", 838 ``!a b c. CAT (a, CAT (b,c)) = CAT (a <> b, c)``, 839 Induct ++ RW_TAC std_ss [APPEND, CAT_def]); 840 841val REST_CAT = store_thm 842 ("REST_CAT", 843 ``!l p. ~(l = []) ==> (REST (CAT (l,p)) = CAT (TL l, p))``, 844 Induct >> RW_TAC std_ss [] 845 ++ RW_TAC std_ss [CAT_def, REST_CONS, TL]); 846 847val S_OR_CAT = store_thm 848 ("S_OR_CAT", 849 ``!p a b c. 850 US_SEM p (S_CAT (S_OR (a,b), c)) = 851 US_SEM p (S_OR (S_CAT (a,c), S_CAT (b,c)))``, 852 RW_TAC std_ss [US_SEM_def] 853 ++ PROVE_TAC []); 854 855val S_REPEAT_UNWIND = store_thm 856 ("S_REPEAT_UNWIND", 857 ``!a p. 858 US_SEM p (S_OR (S_EMPTY, S_CAT (a, S_REPEAT a))) = 859 US_SEM p (S_REPEAT a)``, 860 RW_TAC std_ss [US_SEM_def, S_EMPTY] 861 ++ EQ_TAC 862 << [STRIP_TAC 863 >> (Q.EXISTS_TAC `[]` 864 ++ RW_TAC std_ss [CONCAT_def, listTheory.EVERY_DEF]) 865 ++ Q.EXISTS_TAC `w1 :: wlist` 866 ++ RW_TAC std_ss [CONCAT_def, listTheory.EVERY_DEF], 867 RW_TAC std_ss [] 868 ++ Cases_on `wlist` >> RW_TAC std_ss [CONCAT_def] 869 ++ DISJ2_TAC 870 ++ Q.EXISTS_TAC `h` 871 ++ Q.EXISTS_TAC `FinitePSLPath$CONCAT t` 872 ++ FULL_SIMP_TAC std_ss [CONCAT_def, listTheory.EVERY_DEF] 873 ++ PROVE_TAC []]); 874 875val S_REPEAT_CAT_UNWIND = store_thm 876 ("S_REPEAT_CAT_UNWIND", 877 ``!a b p. 878 US_SEM p (S_OR (b, S_CAT (a, S_CAT (S_REPEAT a, b)))) = 879 US_SEM p (S_CAT (S_REPEAT a, b))``, 880 RW_TAC std_ss [] 881 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_def])) 882 ++ CONV_TAC (LAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [GSYM S_EMPTY_CAT]))) 883 ++ RW_TAC std_ss [GSYM S_CAT_ASSOC] 884 ++ RW_TAC std_ss [GSYM US_SEM_def, GSYM S_OR_CAT] 885 ++ ONCE_REWRITE_TAC [US_SEM_def] 886 ++ RW_TAC std_ss [GSYM S_REPEAT_UNWIND]); 887 888val SEL_REC0 = store_thm 889 ("SEL_REC0", 890 ``!n p. SEL_REC (n + 1) 0 p = SEL p (0,n)``, 891 RW_TAC arith_ss [SEL_def]); 892 893val S_FLEX_AND_SEL_REC = store_thm 894 ("S_FLEX_AND_SEL_REC", 895 ``!p f g. 896 (?n. US_SEM (SEL_REC n 0 p) (S_FLEX_AND (f,g))) = 897 ?n. 898 US_SEM (SEL_REC n 0 p) 899 (S_AND (S_CAT (f, S_REPEAT S_TRUE), S_CAT (g, S_REPEAT S_TRUE)))``, 900 RW_TAC std_ss [S_FLEX_AND_def, GSYM S_TRUE_def] 901 ++ EQ_TAC 902 >> (CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_def])) 903 ++ RW_TAC std_ss [] 904 << [Q.EXISTS_TAC `n` 905 ++ POP_ASSUM MP_TAC 906 ++ ONCE_REWRITE_TAC [US_SEM_def] 907 ++ RW_TAC std_ss [] 908 ++ ONCE_REWRITE_TAC [US_SEM_def] 909 ++ RW_TAC std_ss [US_SEM_REPEAT_TRUE] 910 ++ PROVE_TAC [APPEND_NIL], 911 Q.EXISTS_TAC `n` 912 ++ POP_ASSUM MP_TAC 913 ++ ONCE_REWRITE_TAC [US_SEM_def] 914 ++ RW_TAC std_ss [] 915 ++ ONCE_REWRITE_TAC [US_SEM_def] 916 ++ RW_TAC std_ss [US_SEM_REPEAT_TRUE] 917 ++ PROVE_TAC [APPEND_NIL]]) 918 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_def])) 919 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_def])) 920 ++ RW_TAC std_ss [US_SEM_REPEAT_TRUE] 921 ++ Know `LENGTH w1 <= LENGTH w1' \/ LENGTH w1' <= LENGTH w1` 922 >> DECIDE_TAC 923 ++ REWRITE_TAC [LESS_EQ_EXISTS] 924 ++ DISCH_THEN (STRIP_ASSUME_TAC o GSYM) 925 << [Q.EXISTS_TAC `LENGTH w1'` 926 ++ ONCE_REWRITE_TAC [US_SEM_def] 927 ++ DISJ2_TAC 928 ++ Know `n = LENGTH w1' + LENGTH w2'` 929 >> METIS_TAC [LENGTH_APPEND, LENGTH_SEL_REC] 930 ++ RW_TAC std_ss [] 931 ++ ONCE_REWRITE_TAC [US_SEM_def] 932 ++ REVERSE CONJ_TAC 933 >> (Q.PAT_ASSUM `SEL_REC A B C = w1' <> w2'` MP_TAC 934 ++ ONCE_REWRITE_TAC [ADD_COMM] 935 ++ ONCE_REWRITE_TAC [SEL_REC_SPLIT] 936 ++ RW_TAC arith_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC]) 937 ++ Know `LENGTH w1' + LENGTH w2' = LENGTH w1 + LENGTH w2` 938 >> METIS_TAC [listTheory.LENGTH_APPEND, LENGTH_SEL_REC] 939 ++ STRIP_TAC 940 ++ Know `p' + LENGTH w2' = LENGTH w2` 941 >> DECIDE_TAC 942 ++ POP_ASSUM (K ALL_TAC) 943 ++ STRIP_TAC 944 ++ Q.PAT_ASSUM `SEL_REC A B C = D` (K ALL_TAC) 945 ++ Q.PAT_ASSUM `SEL_REC A B C = D` MP_TAC 946 ++ Q.PAT_ASSUM `A = LENGTH w1'`(fn th => REWRITE_TAC [GSYM th]) 947 ++ ASM_REWRITE_TAC [GSYM ADD_ASSOC] 948 ++ ONCE_REWRITE_TAC [ADD_COMM] 949 ++ ONCE_REWRITE_TAC [SEL_REC_SPLIT] 950 ++ ONCE_REWRITE_TAC [US_SEM_def] 951 ++ RW_TAC arith_ss 952 [US_SEM_REPEAT_TRUE, APPEND_LENGTH_EQ, LENGTH_SEL_REC] 953 ++ PROVE_TAC [], 954 Q.EXISTS_TAC `LENGTH w1` 955 ++ ONCE_REWRITE_TAC [US_SEM_def] 956 ++ DISJ1_TAC 957 ++ Know `n = LENGTH w1 + LENGTH w2` 958 >> METIS_TAC [LENGTH_APPEND, LENGTH_SEL_REC] 959 ++ RW_TAC std_ss [] 960 ++ ONCE_REWRITE_TAC [US_SEM_def] 961 ++ CONJ_TAC 962 >> (Q.PAT_ASSUM `SEL_REC A B C = w1 <> w2` MP_TAC 963 ++ ONCE_REWRITE_TAC [ADD_COMM] 964 ++ ONCE_REWRITE_TAC [SEL_REC_SPLIT] 965 ++ RW_TAC arith_ss [APPEND_LENGTH_EQ, LENGTH_SEL_REC]) 966 ++ Know `LENGTH w1' + LENGTH w2' = LENGTH w1 + LENGTH w2` 967 >> METIS_TAC [listTheory.LENGTH_APPEND, LENGTH_SEL_REC] 968 ++ STRIP_TAC 969 ++ Know `p' + LENGTH w2 = LENGTH w2'` 970 >> DECIDE_TAC 971 ++ POP_ASSUM (K ALL_TAC) 972 ++ STRIP_TAC 973 ++ Q.PAT_ASSUM `SEL_REC A B C = D` MP_TAC 974 ++ Q.PAT_ASSUM `SEL_REC A B C = D` (K ALL_TAC) 975 ++ Q.PAT_ASSUM `A = LENGTH w1`(fn th => REWRITE_TAC [GSYM th]) 976 ++ ASM_REWRITE_TAC [GSYM ADD_ASSOC] 977 ++ ONCE_REWRITE_TAC [ADD_COMM] 978 ++ ONCE_REWRITE_TAC [SEL_REC_SPLIT] 979 ++ ONCE_REWRITE_TAC [US_SEM_def] 980 ++ RW_TAC arith_ss 981 [US_SEM_REPEAT_TRUE, APPEND_LENGTH_EQ, LENGTH_SEL_REC] 982 ++ PROVE_TAC []]); 983 984val S_FLEX_AND_SEL = store_thm 985 ("S_FLEX_AND_SEL", 986 ``!p f g. 987 US_SEM [] (S_FLEX_AND (f,g)) \/ 988 (?n. US_SEM (SEL p (0,n)) (S_FLEX_AND (f,g))) = 989 ?n. 990 US_SEM (SEL p (0,n)) 991 (S_AND (S_CAT (f, S_REPEAT S_TRUE), S_CAT (g, S_REPEAT S_TRUE)))``, 992 RW_TAC std_ss [] 993 ++ MP_TAC (Q.SPECL [`p`, `f`, `g`] S_FLEX_AND_SEL_REC) 994 ++ Know `!P Q. 995 ((?n. P n) = ?n. Q n) = 996 (P 0 \/ (?n. P (SUC n)) = Q 0 \/ ?n. Q (SUC n))` 997 >> METIS_TAC [num_CASES] 998 ++ DISCH_THEN (fn th => SIMP_TAC std_ss [th]) 999 ++ MATCH_MP_TAC 1000 (PROVE [] 1001 ``(A = B) /\ (C = D) /\ (E = G) ==> ((A \/ C = E) ==> (B \/ D = G))``) 1002 ++ CONJ_TAC >> SIMP_TAC arith_ss [SEL_REC_def] 1003 ++ CONJ_TAC >> RW_TAC arith_ss [SEL_def, ADD1] 1004 ++ SIMP_TAC arith_ss [SEL_def, ADD1] 1005 ++ MATCH_MP_TAC (PROVE [] ``(B ==> A) ==> (B \/ A = A)``) 1006 ++ ONCE_REWRITE_TAC [US_SEM_def] 1007 ++ ONCE_REWRITE_TAC [US_SEM_def] 1008 ++ RW_TAC std_ss [SEL_REC_def, US_SEM_REPEAT_TRUE, APPEND_eq_NIL] 1009 ++ Q.EXISTS_TAC `0` 1010 ++ PROVE_TAC [APPEND]); 1011 1012val S_FLEX_AND = store_thm 1013 ("S_FLEX_AND", 1014 ``!p f g. 1015 (?n. US_SEM (SEL_REC n 0 p) (S_FLEX_AND (f,g))) = 1016 (?n. US_SEM (SEL_REC n 0 p) f) /\ (?n. US_SEM (SEL_REC n 0 p) g)``, 1017 RW_TAC std_ss [S_FLEX_AND_SEL_REC] 1018 ++ ONCE_REWRITE_TAC [US_SEM_def] 1019 ++ ONCE_REWRITE_TAC [US_SEM_def] 1020 ++ RW_TAC std_ss [US_SEM_REPEAT_TRUE] 1021 ++ EQ_TAC 1022 << [RW_TAC std_ss [] 1023 << [Know `n = LENGTH w2 + LENGTH w1` 1024 >> PROVE_TAC [LENGTH_APPEND, LENGTH_SEL_REC, ADD_COMM] 1025 ++ RW_TAC std_ss [] 1026 ++ Q.PAT_ASSUM `X = Y` (K ALL_TAC) 1027 ++ Q.PAT_ASSUM `X = Y` MP_TAC 1028 ++ RW_TAC arith_ss [SEL_REC_SPLIT, APPEND_LENGTH_EQ, LENGTH_SEL_REC] 1029 ++ PROVE_TAC [], 1030 Know `n = LENGTH w2' + LENGTH w1'` 1031 >> PROVE_TAC [LENGTH_APPEND, LENGTH_SEL_REC, ADD_COMM] 1032 ++ RW_TAC std_ss [] 1033 ++ Q.PAT_ASSUM `X = Y` MP_TAC 1034 ++ Q.PAT_ASSUM `X = Y` (K ALL_TAC) 1035 ++ RW_TAC arith_ss [SEL_REC_SPLIT, APPEND_LENGTH_EQ, LENGTH_SEL_REC] 1036 ++ PROVE_TAC []], 1037 RW_TAC std_ss [] 1038 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1039 ++ REWRITE_TAC [LESS_EQ_EXISTS] 1040 ++ DISCH_THEN (STRIP_ASSUME_TAC o GSYM) 1041 << [Q.EXISTS_TAC `n'` 1042 ++ REVERSE CONJ_TAC >> PROVE_TAC [APPEND_NIL] 1043 ++ RW_TAC std_ss [] 1044 ++ ONCE_REWRITE_TAC [ADD_COMM] 1045 ++ RW_TAC arith_ss [SEL_REC_SPLIT] 1046 ++ PROVE_TAC [APPEND_LENGTH_EQ, LENGTH_SEL_REC], 1047 Q.EXISTS_TAC `n` 1048 ++ CONJ_TAC >> PROVE_TAC [APPEND_NIL] 1049 ++ RW_TAC std_ss [] 1050 ++ ONCE_REWRITE_TAC [ADD_COMM] 1051 ++ RW_TAC arith_ss [SEL_REC_SPLIT] 1052 ++ PROVE_TAC [APPEND_LENGTH_EQ, LENGTH_SEL_REC]]]); 1053 1054val S_CAT_SEL_REC = store_thm 1055 ("S_CAT_SEL_REC", 1056 ``!p s t. 1057 (?n. US_SEM (SEL_REC n 0 p) (S_CAT (s,t))) = 1058 (?m. US_SEM (SEL_REC m 0 p) s /\ 1059 ?n. US_SEM (SEL_REC n 0 (RESTN p m)) t)``, 1060 RW_TAC std_ss [US_SEM_def] 1061 ++ EQ_TAC 1062 << [RW_TAC std_ss [] 1063 ++ Know `n = LENGTH w2 + LENGTH w1` 1064 >> PROVE_TAC [LENGTH_SEL_REC, LENGTH_APPEND, ADD_COMM] 1065 ++ RW_TAC std_ss [] 1066 ++ FULL_SIMP_TAC arith_ss 1067 [SEL_REC_SPLIT, APPEND_LENGTH_EQ, LENGTH_SEL_REC] 1068 ++ Q.EXISTS_TAC `LENGTH w1` 1069 ++ RW_TAC std_ss [] 1070 ++ Q.EXISTS_TAC `LENGTH w2` 1071 ++ RW_TAC arith_ss [SEL_REC_RESTN], 1072 RW_TAC std_ss [] 1073 ++ Q.EXISTS_TAC `n + m` 1074 ++ Q.EXISTS_TAC `SEL_REC m 0 p` 1075 ++ Q.EXISTS_TAC `SEL_REC n 0 (RESTN p m)` 1076 ++ RW_TAC arith_ss [SEL_REC_SPLIT, SEL_REC_RESTN]]); 1077 1078val S_FUSION_SEL_REC = store_thm 1079 ("S_FUSION_SEL_REC", 1080 ``!p s t. 1081 (?n. US_SEM (SEL_REC n 0 p) (S_FUSION (s,t))) = 1082 (?m. US_SEM (SEL_REC (m + 1) 0 p) s /\ 1083 ?n. US_SEM (SEL_REC (n + 1) 0 (RESTN p m)) t)``, 1084 RW_TAC std_ss [US_SEM_def] 1085 ++ EQ_TAC 1086 << [RW_TAC std_ss [] 1087 ++ Know `n = LENGTH w2 + LENGTH [l] + LENGTH w1` 1088 >> METIS_TAC [LENGTH_SEL_REC, LENGTH_APPEND, ADD_COMM, ADD_ASSOC] 1089 ++ RW_TAC std_ss [] 1090 ++ Q.PAT_ASSUM `X = Y` 1091 (MP_TAC o SIMP_RULE arith_ss 1092 [SEL_REC_SPLIT, APPEND_LENGTH_EQ, LENGTH_SEL_REC, APPEND_ASSOC, 1093 LENGTH_APPEND]) 1094 ++ RW_TAC std_ss [LENGTH] 1095 ++ Q.EXISTS_TAC `LENGTH w1` 1096 ++ CONJ_TAC 1097 >> (ONCE_REWRITE_TAC [ADD_COMM] 1098 ++ RW_TAC arith_ss [SEL_REC_SPLIT]) 1099 ++ Q.EXISTS_TAC `LENGTH w2` 1100 ++ RW_TAC arith_ss [SEL_REC_RESTN] 1101 ++ RW_TAC arith_ss [SEL_REC_SPLIT], 1102 RW_TAC std_ss [] 1103 ++ Q.EXISTS_TAC `n + 1 + m` 1104 ++ Q.EXISTS_TAC `SEL_REC m 0 p` 1105 ++ Q.EXISTS_TAC `SEL_REC n 0 (RESTN p (m + 1))` 1106 ++ Q.EXISTS_TAC `ELEM p m` 1107 ++ ASM_SIMP_TAC arith_ss [APPEND_11, SEL_REC_SPLIT, GSYM APPEND_ASSOC] 1108 ++ Know `[ELEM p m] = SEL_REC 1 0 (RESTN p m)` 1109 >> RW_TAC bool_ss [ELEM_def, SEL_REC_def, ONE] 1110 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 1111 ++ CONJ_TAC >> RW_TAC arith_ss [SEL_REC_RESTN] 1112 ++ CONJ_TAC 1113 >> (Q.PAT_ASSUM `US_SEM X s` MP_TAC 1114 ++ ONCE_REWRITE_TAC [ADD_COMM] 1115 ++ RW_TAC arith_ss [SEL_REC_RESTN, SEL_REC_SPLIT]) 1116 ++ POP_ASSUM MP_TAC 1117 ++ SIMP_TAC arith_ss [SEL_REC_SPLIT] 1118 ++ RW_TAC arith_ss [SEL_REC_RESTN]]); 1119 1120val S_CAT_SEL_REC0 = store_thm 1121 ("S_CAT_SEL_REC0", 1122 ``!p s t n. 1123 US_SEM (SEL_REC n 0 p) (S_CAT (s,t)) = 1124 (?m. 1125 m <= n /\ 1126 US_SEM (SEL_REC m 0 p) s /\ 1127 US_SEM (SEL_REC (n - m) 0 (RESTN p m)) t)``, 1128 RW_TAC std_ss [US_SEM_def] 1129 ++ EQ_TAC 1130 << [RW_TAC std_ss [] 1131 ++ Know `n = LENGTH w2 + LENGTH w1` 1132 >> PROVE_TAC [LENGTH_SEL_REC, LENGTH_APPEND, ADD_COMM] 1133 ++ RW_TAC std_ss [] 1134 ++ FULL_SIMP_TAC arith_ss 1135 [SEL_REC_SPLIT, APPEND_LENGTH_EQ, LENGTH_SEL_REC] 1136 ++ Q.EXISTS_TAC `LENGTH w1` 1137 ++ RW_TAC arith_ss [] 1138 ++ RW_TAC arith_ss [SEL_REC_RESTN], 1139 RW_TAC std_ss [] 1140 ++ Q.EXISTS_TAC `SEL_REC m 0 p` 1141 ++ Q.EXISTS_TAC `SEL_REC (n - m) 0 (RESTN p m)` 1142 ++ RW_TAC arith_ss [SEL_REC_RESTN] 1143 ++ MP_TAC (Q.SPECL [`p`, `n - m`, `m`, `0`] 1144 (GEN_ALL (INST_TYPE [alpha |-> ``:'a -> bool``] 1145 (GSYM SEL_REC_SPLIT)))) 1146 ++ RW_TAC arith_ss []]); 1147 1148val RESTN_CAT = store_thm 1149 ("RESTN_CAT", 1150 ``!l p n. (LENGTH l = n) ==> (RESTN (CAT (l,p)) n = p)``, 1151 Induct 1152 ++ RW_TAC std_ss [CAT_def, LENGTH] 1153 ++ RW_TAC std_ss [RESTN_def, REST_CONS]); 1154 1155val CONS_HEAD_REST = store_thm 1156 ("CONS_HEAD_REST", 1157 ``!p. LENGTH p > 0 ==> (CONS (HEAD p, REST p) = p)``, 1158 Cases 1159 ++ RW_TAC arith_ss [LENGTH_def, GT, REST_def, CONS_def, HEAD_def, FUN_EQ_THM] 1160 ++ PROVE_TAC [CONS, LENGTH_NOT_NULL, GREATER_DEF]); 1161 1162val CAT_SEL_REC_RESTN = store_thm 1163 ("CAT_SEL_REC_RESTN", 1164 ``!n p. IS_INFINITE p ==> (CAT (SEL_REC n 0 p, RESTN p n) = p)``, 1165 Induct 1166 ++ RW_TAC std_ss [CAT_def, SEL_REC_def, RESTN_def, IS_INFINITE_REST] 1167 ++ PROVE_TAC [CONS_HEAD_REST, GT, LENGTH_def, IS_INFINITE_EXISTS]); 1168 1169val SEL_REC_CAT_0 = store_thm 1170 ("SEL_REC_CAT_0", 1171 ``!n l p. (LENGTH l = n) ==> (SEL_REC n 0 (CAT (l,p)) = l)``, 1172 Induct_on `l` 1173 ++ RW_TAC std_ss [LENGTH] 1174 ++ RW_TAC std_ss [SEL_REC_def, CAT_def, HEAD_CONS, REST_CONS]); 1175 1176val SEL_REC_CAT = store_thm 1177 ("SEL_REC_CAT", 1178 ``!n m l p. (LENGTH l = n) ==> (SEL_REC m n (CAT (l,p)) = SEL_REC m 0 p)``, 1179 Induct_on `l` 1180 ++ RW_TAC std_ss [LENGTH] 1181 ++ Cases_on `m` 1182 ++ RW_TAC std_ss [SEL_REC_def, CAT_def, HEAD_CONS, REST_CONS]); 1183 1184val UF_SEM_F_W_ALT = store_thm 1185 ("UF_SEM_F_W_ALT", 1186 ``!f g w. 1187 UF_SEM w (F_W (f,g)) = 1188 !j :: 0 to LENGTH w. 1189 ~UF_SEM (RESTN w j) f ==> ?k :: 0 to SUC j. UF_SEM (RESTN w k) g``, 1190 RW_TAC std_ss [] 1191 ++ (Cases_on `w` 1192 ++ RW_TAC arith_resq_ss 1193 [UF_SEM_F_W, UF_SEM_def, UF_SEM_F_G, xnum_to_def] 1194 ++ Know `!m n. (m:num) < SUC n = m <= n` >> DECIDE_TAC 1195 ++ DISCH_THEN (fn th => REWRITE_TAC [th])) 1196 << [REVERSE EQ_TAC 1197 >> (RW_TAC std_ss [] 1198 ++ MATCH_MP_TAC (PROVE [] ``(~b ==> a) ==> a \/ b``) 1199 ++ SIMP_TAC std_ss [] 1200 ++ DISCH_THEN (MP_TAC o HO_MATCH_MP LEAST_EXISTS_IMP) 1201 ++ Q.SPEC_TAC 1202 (`LEAST i. i < LENGTH l /\ ~UF_SEM (RESTN (FINITE l) i) f`,`i`) 1203 ++ RW_TAC arith_ss [GSYM AND_IMP_INTRO] 1204 ++ Q.PAT_ASSUM `!j. P j ==> Q j ==> R j` (MP_TAC o Q.SPEC `i`) 1205 ++ RW_TAC arith_ss [] 1206 ++ Q.EXISTS_TAC `k` 1207 ++ RW_TAC arith_ss []) 1208 ++ RW_TAC std_ss [] 1209 >> (Q.EXISTS_TAC `k` 1210 ++ RW_TAC arith_ss [] 1211 ++ Know `!m n. (m:num) <= (n:num) \/ n < m` >> DECIDE_TAC 1212 ++ METIS_TAC []) 1213 ++ METIS_TAC [], 1214 REVERSE EQ_TAC 1215 >> (RW_TAC std_ss [] 1216 ++ MATCH_MP_TAC (PROVE [] ``(~b ==> a) ==> a \/ b``) 1217 ++ SIMP_TAC std_ss [] 1218 ++ DISCH_THEN (MP_TAC o HO_MATCH_MP LEAST_EXISTS_IMP) 1219 ++ Q.SPEC_TAC (`LEAST i. ~UF_SEM (RESTN (INFINITE f') i) f`,`i`) 1220 ++ RW_TAC arith_ss [] 1221 ++ Q.PAT_ASSUM `!j. P j ==> ?k. Q j k` (MP_TAC o Q.SPEC `i`) 1222 ++ RW_TAC arith_ss [] 1223 ++ Q.EXISTS_TAC `k` 1224 ++ RW_TAC arith_ss []) 1225 ++ RW_TAC std_ss [] 1226 >> (Q.EXISTS_TAC `k` 1227 ++ RW_TAC arith_ss [] 1228 ++ Know `!m n. (m:num) <= (n:num) \/ n < m` >> DECIDE_TAC 1229 ++ METIS_TAC []) 1230 ++ METIS_TAC []]); 1231 1232val UF_SEM_WEAK_UNTIL = store_thm 1233 ("UF_SEM_WEAK_UNTIL", 1234 ``!p f g. 1235 UF_SEM p 1236 (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)),F_UNTIL (F_BOOL B_TRUE,F_NOT f)))) = 1237 UF_SEM p (F_W (f,g))``, 1238 RW_TAC std_ss [UF_SEM_def, F_W_def, F_OR_def, F_G_def, F_F_def]); 1239 1240val LENGTH_IS_INFINITE = store_thm 1241 ("LENGTH_IS_INFINITE", 1242 ``!p. IS_INFINITE p ==> (LENGTH p = INFINITY)``, 1243 METIS_TAC [LENGTH_def, IS_INFINITE_EXISTS]); 1244 1245val CAT_SEL_REC_RESTN = store_thm 1246 ("CAT_SEL_REC_RESTN", 1247 ``!n p. IS_INFINITE p ==> (CAT (SEL_REC n 0 p, RESTN p n) = p)``, 1248 Induct 1249 ++ RW_TAC std_ss [SEL_REC_def, RESTN_def, CAT_def, IS_INFINITE_REST] 1250 ++ PROVE_TAC [CONS_HEAD_REST, LENGTH_IS_INFINITE, GT]); 1251 1252(* Safety violations *) 1253 1254val safety_violation_def = Define 1255 `safety_violation p (f : 'a fl) = 1256 ?n. !q. IS_INFINITE q ==> ~UF_SEM (CAT (SEL_REC n 0 p, q)) f`; 1257 1258val safety_violation_alt = store_thm 1259 ("safety_violation_alt", 1260 ``!p f. 1261 safety_violation p f = 1262 ?n. !w. ~UF_SEM (CAT (SEL_REC n 0 p, INFINITE w)) f``, 1263 REPEAT STRIP_TAC 1264 ++ REWRITE_TAC [safety_violation_def] 1265 ++ PROVE_TAC [IS_INFINITE_EXISTS, path_nchotomy, IS_INFINITE_def]); 1266 1267val safety_violation = store_thm 1268 ("safety_violation", 1269 ``!p f. 1270 safety_violation p f = 1271 ?n. !q. IS_INFINITE q ==> ~UF_SEM (CAT (SEL p (0,n), q)) f``, 1272 REPEAT STRIP_TAC 1273 ++ SIMP_TAC arith_ss [safety_violation_def, SEL_def] 1274 ++ REVERSE EQ_TAC >> PROVE_TAC [] 1275 ++ STRIP_TAC 1276 ++ POP_ASSUM MP_TAC 1277 ++ REVERSE (Cases_on `n`) >> PROVE_TAC [ADD1] 1278 ++ SIMP_TAC std_ss [SEL_REC_def, CAT_def] 1279 ++ PROVE_TAC [IS_INFINITE_CAT]); 1280 1281val safety_violation_aux = store_thm 1282 ("safety_violation_aux", 1283 ``!p f. 1284 safety_violation p f = 1285 ?n. !w. ~UF_SEM (CAT (SEL p (0,n), INFINITE w)) f``, 1286 REPEAT STRIP_TAC 1287 ++ REWRITE_TAC [safety_violation] 1288 ++ PROVE_TAC [IS_INFINITE_EXISTS, path_nchotomy, IS_INFINITE_def]); 1289 1290val safety_violation_refl = store_thm 1291 ("safety_violation_refl", 1292 ``!p f. IS_INFINITE p /\ safety_violation p f ==> ~UF_SEM p f``, 1293 RW_TAC std_ss [safety_violation_alt] 1294 ++ MP_TAC (Q.SPECL [`n`, `p`] 1295 (INST_TYPE [alpha |-> ``:'a->bool``] CAT_SEL_REC_RESTN)) 1296 ++ ASM_REWRITE_TAC [] 1297 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 1298 ++ PROVE_TAC [IS_INFINITE_EXISTS, IS_INFINITE_RESTN]); 1299 1300val safety_violation_NOT_NOT = store_thm 1301 ("safety_violation_NOT_NOT", 1302 ``!f p. safety_violation p (F_NOT (F_NOT f)) = safety_violation p f``, 1303 RW_TAC std_ss [safety_violation_def, UF_SEM_def]); 1304 1305val safety_violation_WEAK_UNTIL = store_thm 1306 ("safety_violation_WEAK_UNTIL", 1307 ``!p f g. 1308 safety_violation p 1309 (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)),F_UNTIL (F_BOOL B_TRUE,F_NOT f)))) = 1310 safety_violation p (F_W (f,g))``, 1311 RW_TAC std_ss [safety_violation_def, UF_SEM_WEAK_UNTIL]); 1312 1313(* The simple subset *) 1314 1315val boolean_def = Define 1316 `(boolean (F_BOOL _) = T) /\ 1317 (boolean (F_NOT f) = boolean f) /\ 1318 (boolean (F_AND (f,g)) = boolean f /\ boolean g) /\ 1319 (boolean _ = F)`; 1320 1321(* 1322 Cannot allow F_STRONG_IMP as simple formulas, because 1323 1324 F_STRONG_IMP (S_TRUE, S_CAT (S_REPEAT (S_BOOL P), S_FALSE)) 1325 1326 doesn't have a finite bad prefix on P P P P P P P ..., and also 1327 1328 F_AND (F_STRONG_IMP (S_TRUE, S_CAT (S_REPEAT (S_BOOL P), S_BOOL Q)), 1329 F_STRONG_IMP (S_TRUE, S_CAT (S_REPEAT (S_BOOL P), S_BOOL (B_NOT Q)))) 1330 1331 is "pathologically safe" [Kuperferman & Vardi 1999], meaning that the path 1332 1333 P P P P P P P P ... 1334 1335 has a bad prefix [] for the property, but there are no bad prefixes for 1336 either of the conjuncts. 1337*) 1338 1339val simple_def = Define 1340 `(simple (F_BOOL b) = boolean (F_BOOL b)) /\ 1341 (simple (F_NOT (F_NOT f)) = simple f) /\ 1342 (simple (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)), h))) = 1343 simple f /\ boolean g /\ (h = F_UNTIL (F_BOOL B_TRUE, F_NOT f))) /\ 1344 (simple (F_NOT (F_AND (f,g))) = simple (F_NOT f) /\ simple (F_NOT g)) /\ 1345 (simple (F_NOT f) = boolean f) /\ 1346 (simple (F_AND (f,g)) = simple f /\ simple g) /\ 1347 (simple (F_NEXT f) = simple f) /\ 1348 (simple (F_UNTIL _) = F) /\ 1349 (simple (F_SUFFIX_IMP (r,f)) = S_CLOCK_FREE r /\ simple f) /\ 1350 (simple (F_STRONG_IMP _) = F) /\ 1351 (simple (F_WEAK_IMP _) = F) /\ 1352 (simple (F_ABORT _) = F) /\ 1353 (simple (F_STRONG_CLOCK _) = F)`; 1354 1355val simple_ind = theorem "simple_ind"; 1356 1357val boolean_simple = store_thm 1358 ("boolean_simple", 1359 ``!f. boolean f ==> simple f /\ simple (F_NOT f)``, 1360 (INDUCT_THEN fl_induct ASSUME_TAC 1361 ++ RW_TAC std_ss [boolean_def, simple_def]) 1362 ++ (Cases_on `f` ++ RW_TAC std_ss [simple_def]) 1363 ++ (Cases_on `f''` ++ RW_TAC std_ss [simple_def]) 1364 ++ FULL_SIMP_TAC std_ss [boolean_def]); 1365 1366val UF_SEM_boolean = store_thm 1367 ("UF_SEM_boolean", 1368 ``!f p. 1369 boolean f /\ LENGTH p > 0 ==> 1370 (UF_SEM (FINITE [ELEM p 0]) f = UF_SEM p f)``, 1371 INDUCT_THEN fl_induct ASSUME_TAC 1372 ++ RW_TAC std_ss 1373 [boolean_def, UF_SEM_def, LENGTH, ELEM_def, 1374 RESTN_def, GT, LENGTH_SEL, LENGTH_def, HEAD_def, HD]); 1375 1376val boolean_safety_violation = store_thm 1377 ("boolean_safety_violation", 1378 ``!p f. 1379 boolean f /\ IS_INFINITE p ==> 1380 (safety_violation p f = ~UF_SEM (FINITE [ELEM p 0]) f)``, 1381 GEN_TAC 1382 ++ Know `!P : num -> (num -> 'a -> bool) -> ('a -> bool) path. 1383 (!n w. LENGTH (P n w) > 0) ==> 1384 !f. boolean f ==> 1385 !n w. ~UF_SEM (P n w) f = ~UF_SEM (FINITE [ELEM (P n w) 0]) f` 1386 >> (RW_TAC std_ss [] ++ PROVE_TAC [UF_SEM_boolean]) 1387 ++ DISCH_THEN (MP_TAC o Q.SPEC `\n w. CAT (SEL p (0,n), INFINITE w)`) 1388 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> (a ==> b) ==> c``) 1389 ++ CONJ_TAC >> RW_TAC std_ss [LENGTH_def, LENGTH_CAT, GT] 1390 ++ BETA_TAC 1391 ++ STRIP_TAC 1392 ++ INDUCT_THEN fl_induct (K ALL_TAC) 1393 ++ RW_TAC std_ss [boolean_def, safety_violation_aux, ELEM_CAT_SEL]); 1394 1395(* The basic constraint on simple formulas *) 1396 1397val simple_safety = store_thm 1398 ("simple_safety", 1399 ``!f p. simple f /\ IS_INFINITE p ==> (safety_violation p f = ~UF_SEM p f)``, 1400 RW_TAC std_ss [] 1401 ++ EQ_TAC >> METIS_TAC [safety_violation_refl] 1402 ++ REPEAT (POP_ASSUM MP_TAC) 1403 ++ SIMP_TAC std_ss [AND_IMP_INTRO, GSYM CONJ_ASSOC] 1404 ++ Q.SPEC_TAC (`p`,`p`) 1405 ++ Q.SPEC_TAC (`f`,`f`) 1406 ++ recInduct simple_ind 1407 ++ (REPEAT CONJ_TAC 1408 ++ TRY (ASM_SIMP_TAC std_ss [simple_def, boolean_def] ++ NO_TAC) 1409 ++ SIMP_TAC std_ss [boolean_def] 1410 ++ RW_TAC std_ss [] 1411 ++ Q.PAT_ASSUM `simple X` MP_TAC 1412 ++ ONCE_REWRITE_TAC [simple_def] 1413 ++ RW_TAC std_ss [boolean_def]) 1414 << [(* F_BOOL *) 1415 Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1416 ++ RW_TAC std_ss [simple_def, safety_violation_alt, UF_SEM_def] 1417 >> METIS_TAC [LENGTH_def, IS_INFINITE_EXISTS, GT] 1418 ++ Q.EXISTS_TAC `1` 1419 ++ RW_TAC bool_ss 1420 [ONE, SEL_REC_def, CAT_def, ELEM_def, RESTN_def, HEAD_CONS] 1421 ++ PROVE_TAC [ELEM_def, RESTN_def], 1422 1423 (* F_NOT (F_NOT f) *) 1424 FULL_SIMP_TAC std_ss [safety_violation_NOT_NOT, UF_SEM_def], 1425 1426 (* F_NOT (F_AND (F_NOT (F_UNTIL (f,g)), _)) *) 1427 Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1428 ++ ASM_SIMP_TAC arith_resq_ss 1429 [safety_violation_alt, UF_SEM_WEAK_UNTIL, UF_SEM_F_W_ALT, 1430 xnum_to_def, LENGTH_CAT, LENGTH_IS_INFINITE] 1431 ++ Know `!m n. (m:num) < SUC n = m <= n` >> DECIDE_TAC 1432 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 1433 ++ SIMP_TAC arith_ss [GSYM IMP_DISJ_THM] 1434 ++ RW_TAC std_ss [] 1435 ++ Q.PAT_ASSUM `!p. X p /\ Y p ==> Z p` (MP_TAC o Q.SPEC `RESTN p j`) 1436 ++ RW_TAC arith_ss 1437 [IS_INFINITE_RESTN, safety_violation_alt, SEL_REC_RESTN] 1438 ++ Q.EXISTS_TAC `SUC n + j` 1439 ++ RW_TAC std_ss [] 1440 ++ Q.EXISTS_TAC `j` 1441 ++ CONJ_TAC 1442 >> (RW_TAC arith_ss 1443 [SEL_REC_SPLIT, GSYM CAT_APPEND, RESTN_CAT, LENGTH_SEL_REC] 1444 ++ RW_TAC bool_ss [ADD1] 1445 ++ ONCE_REWRITE_TAC [ADD_COMM] 1446 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1447 ++ METIS_TAC [IS_INFINITE_EXISTS, IS_INFINITE_def, IS_INFINITE_CAT]) 1448 ++ RW_TAC std_ss [] 1449 ++ MP_TAC 1450 (Q.SPECL [`g`,`RESTN (CAT (SEL_REC (SUC n + j) 0 p,INFINITE w)) k`] 1451 (GSYM UF_SEM_boolean)) 1452 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 1453 ++ CONJ_TAC 1454 >> (RW_TAC std_ss [] 1455 ++ PROVE_TAC [LENGTH_IS_INFINITE, IS_INFINITE_def, 1456 IS_INFINITE_RESTN, IS_INFINITE_CAT, GT]) 1457 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 1458 ++ Q.PAT_ASSUM `!w. P w` (K ALL_TAC) 1459 ++ Q.PAT_ASSUM `!w. P w` (MP_TAC o Q.SPEC `k`) 1460 ++ ASM_SIMP_TAC std_ss [] 1461 ++ MP_TAC (Q.SPECL [`g`,`RESTN p k`] (GSYM UF_SEM_boolean)) 1462 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 1463 ++ CONJ_TAC 1464 >> (RW_TAC std_ss [] 1465 ++ PROVE_TAC [LENGTH_IS_INFINITE, IS_INFINITE_def, 1466 IS_INFINITE_RESTN, IS_INFINITE_CAT, GT]) 1467 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 1468 ++ MATCH_MP_TAC (PROVE [] ``(a = b) ==> (a ==> b)``) 1469 ++ NTAC 6 (AP_TERM_TAC || AP_THM_TAC) 1470 ++ RW_TAC arith_ss [ELEM_RESTN] 1471 ++ RW_TAC arith_ss [ELEM_def] 1472 ++ Know `k <= j + SUC n` >> DECIDE_TAC 1473 ++ RW_TAC bool_ss [LESS_EQ_EXISTS] 1474 ++ RW_TAC std_ss [] 1475 ++ ONCE_REWRITE_TAC [ADD_COMM] 1476 ++ RW_TAC std_ss 1477 [SEL_REC_SPLIT, GSYM CAT_APPEND, RESTN_CAT, LENGTH_SEL_REC] 1478 ++ RW_TAC arith_ss [] 1479 ++ Cases_on `p'` >> FULL_SIMP_TAC arith_ss [] 1480 ++ RW_TAC std_ss [SEL_REC_SUC, CAT_def, HEAD_CONS, ELEM_def], 1481 1482 (* F_NOT (F_AND (f,g)) *) 1483 RW_TAC std_ss [safety_violation_def] 1484 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1485 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1486 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1487 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1488 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1489 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1490 ++ STRIP_TAC 1491 ++ HO_MATCH_MP_TAC 1492 (METIS_PROVE [] 1493 ``!P Q R. 1494 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1495 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1496 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1497 ++ RW_TAC std_ss [safety_violation_def] 1498 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1499 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1500 << [Q.EXISTS_TAC `n + p'` 1501 ++ RW_TAC std_ss [] 1502 ++ ONCE_REWRITE_TAC [ADD_COMM] 1503 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1504 ++ METIS_TAC [IS_INFINITE_CAT], 1505 Q.EXISTS_TAC `n' + p'` 1506 ++ RW_TAC std_ss [] 1507 ++ ONCE_REWRITE_TAC [ADD_COMM] 1508 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1509 ++ METIS_TAC [IS_INFINITE_CAT]], 1510 RW_TAC std_ss [safety_violation_def] 1511 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1512 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1513 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1514 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1515 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1516 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1517 ++ STRIP_TAC 1518 ++ HO_MATCH_MP_TAC 1519 (METIS_PROVE [] 1520 ``!P Q R. 1521 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1522 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1523 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1524 ++ RW_TAC std_ss [safety_violation_def] 1525 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1526 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1527 << [Q.EXISTS_TAC `n + p'` 1528 ++ RW_TAC std_ss [] 1529 ++ ONCE_REWRITE_TAC [ADD_COMM] 1530 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1531 ++ METIS_TAC [IS_INFINITE_CAT], 1532 Q.EXISTS_TAC `n' + p'` 1533 ++ RW_TAC std_ss [] 1534 ++ ONCE_REWRITE_TAC [ADD_COMM] 1535 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1536 ++ METIS_TAC [IS_INFINITE_CAT]], 1537 RW_TAC std_ss [safety_violation_def] 1538 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1539 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1540 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1541 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1542 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1543 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1544 ++ STRIP_TAC 1545 ++ HO_MATCH_MP_TAC 1546 (METIS_PROVE [] 1547 ``!P Q R. 1548 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1549 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1550 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1551 ++ RW_TAC std_ss [safety_violation_def] 1552 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1553 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1554 << [Q.EXISTS_TAC `n + p'` 1555 ++ RW_TAC std_ss [] 1556 ++ ONCE_REWRITE_TAC [ADD_COMM] 1557 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1558 ++ METIS_TAC [IS_INFINITE_CAT], 1559 Q.EXISTS_TAC `n' + p'` 1560 ++ RW_TAC std_ss [] 1561 ++ ONCE_REWRITE_TAC [ADD_COMM] 1562 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1563 ++ METIS_TAC [IS_INFINITE_CAT]], 1564 RW_TAC std_ss [safety_violation_def] 1565 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1566 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1567 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1568 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1569 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1570 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1571 ++ STRIP_TAC 1572 ++ HO_MATCH_MP_TAC 1573 (METIS_PROVE [] 1574 ``!P Q R. 1575 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1576 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1577 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1578 ++ RW_TAC std_ss [safety_violation_def] 1579 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1580 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1581 << [Q.EXISTS_TAC `n + p'` 1582 ++ RW_TAC std_ss [] 1583 ++ ONCE_REWRITE_TAC [ADD_COMM] 1584 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1585 ++ METIS_TAC [IS_INFINITE_CAT], 1586 Q.EXISTS_TAC `n' + p'` 1587 ++ RW_TAC std_ss [] 1588 ++ ONCE_REWRITE_TAC [ADD_COMM] 1589 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1590 ++ METIS_TAC [IS_INFINITE_CAT]], 1591 RW_TAC std_ss [safety_violation_def] 1592 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1593 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1594 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1595 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1596 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1597 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1598 ++ STRIP_TAC 1599 ++ HO_MATCH_MP_TAC 1600 (METIS_PROVE [] 1601 ``!P Q R. 1602 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1603 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1604 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1605 ++ RW_TAC std_ss [safety_violation_def] 1606 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1607 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1608 << [Q.EXISTS_TAC `n + p'` 1609 ++ RW_TAC std_ss [] 1610 ++ ONCE_REWRITE_TAC [ADD_COMM] 1611 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1612 ++ METIS_TAC [IS_INFINITE_CAT], 1613 Q.EXISTS_TAC `n' + p'` 1614 ++ RW_TAC std_ss [] 1615 ++ ONCE_REWRITE_TAC [ADD_COMM] 1616 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1617 ++ METIS_TAC [IS_INFINITE_CAT]], 1618 RW_TAC std_ss [safety_violation_def] 1619 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1620 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1621 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1622 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1623 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1624 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1625 ++ STRIP_TAC 1626 ++ HO_MATCH_MP_TAC 1627 (METIS_PROVE [] 1628 ``!P Q R. 1629 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1630 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1631 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1632 ++ RW_TAC std_ss [safety_violation_def] 1633 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1634 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1635 << [Q.EXISTS_TAC `n + p'` 1636 ++ RW_TAC std_ss [] 1637 ++ ONCE_REWRITE_TAC [ADD_COMM] 1638 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1639 ++ METIS_TAC [IS_INFINITE_CAT], 1640 Q.EXISTS_TAC `n' + p'` 1641 ++ RW_TAC std_ss [] 1642 ++ ONCE_REWRITE_TAC [ADD_COMM] 1643 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1644 ++ METIS_TAC [IS_INFINITE_CAT]], 1645 RW_TAC std_ss [safety_violation_def] 1646 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1647 ++ ONCE_REWRITE_TAC [UF_SEM_def] 1648 ++ PURE_ONCE_REWRITE_TAC [UF_SEM_def] 1649 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1650 ++ ONCE_REWRITE_TAC [GSYM UF_SEM_def] 1651 ++ PURE_ONCE_REWRITE_TAC [DE_MORGAN_THM] 1652 ++ STRIP_TAC 1653 ++ HO_MATCH_MP_TAC 1654 (METIS_PROVE [] 1655 ``!P Q R. 1656 (?n. (!q. P n q ==> Q n q) /\ (!q. P n q ==> R n q)) ==> 1657 ?n. (!q. P n q ==> Q n q /\ R n q)``) 1658 ++ REPEAT (Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`)) 1659 ++ RW_TAC std_ss [safety_violation_def] 1660 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1661 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1662 << [Q.EXISTS_TAC `n + p'` 1663 ++ RW_TAC std_ss [] 1664 ++ ONCE_REWRITE_TAC [ADD_COMM] 1665 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1666 ++ METIS_TAC [IS_INFINITE_CAT], 1667 Q.EXISTS_TAC `n' + p'` 1668 ++ RW_TAC std_ss [] 1669 ++ ONCE_REWRITE_TAC [ADD_COMM] 1670 ++ RW_TAC std_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1671 ++ METIS_TAC [IS_INFINITE_CAT]], 1672 1673 (* F_NOT (F_BOOL b) *) 1674 RW_TAC std_ss [safety_violation_alt] 1675 ++ Q.EXISTS_TAC `1` 1676 ++ POP_ASSUM MP_TAC 1677 ++ RW_TAC bool_ss [ONE, SEL_REC_def, CAT_def, UF_SEM_def] 1678 >> RW_TAC std_ss [LENGTH_def, CONS_def, GT] 1679 ++ POP_ASSUM MP_TAC 1680 ++ RW_TAC std_ss [ELEM_def, RESTN_def, HEAD_CONS], 1681 1682 (* F_AND (f,g) *) 1683 RW_TAC std_ss [safety_violation_alt] 1684 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1685 ++ RW_TAC std_ss [UF_SEM_def] 1686 << [Q.PAT_ASSUM `!p. P p` (K ALL_TAC) 1687 ++ Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`) 1688 ++ RW_TAC std_ss [safety_violation_alt] 1689 ++ METIS_TAC [], 1690 Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `p`) 1691 ++ RW_TAC std_ss [safety_violation_alt] 1692 ++ METIS_TAC []], 1693 1694 (* F_NEXT f *) 1695 RW_TAC std_ss [safety_violation_alt] 1696 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1697 ++ RW_TAC std_ss [UF_SEM_def] 1698 >> PROVE_TAC [LENGTH_IS_INFINITE, GT] 1699 ++ Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `RESTN p 1`) 1700 ++ RW_TAC std_ss [safety_violation_alt, IS_INFINITE_RESTN] 1701 ++ Q.EXISTS_TAC `SUC n` 1702 ++ RW_TAC std_ss [] 1703 ++ DISJ2_TAC 1704 ++ RW_TAC bool_ss [ONE, SEL_REC_def, CAT_def, RESTN_def, REST_CONS] 1705 ++ METIS_TAC [RESTN_def, ONE], 1706 1707 (* F_SUFFIX_IMP (r,f) *) 1708 RW_TAC std_ss [safety_violation_alt] 1709 ++ Q.PAT_ASSUM `~UF_SEM X Y` MP_TAC 1710 ++ RW_TAC arith_resq_ss 1711 [UF_SEM_def, xnum_to_def, LENGTH_CAT, LENGTH_IS_INFINITE, SEL_def] 1712 ++ Q.PAT_ASSUM `!p. P p` (MP_TAC o Q.SPEC `RESTN p j`) 1713 ++ RW_TAC std_ss [safety_violation_alt, IS_INFINITE_RESTN] 1714 ++ Q.EXISTS_TAC `SUC n + j` 1715 ++ RW_TAC std_ss [] 1716 ++ Q.EXISTS_TAC `j` 1717 ++ REVERSE CONJ_TAC 1718 >> (Q.PAT_ASSUM `!w. P w` MP_TAC 1719 ++ RW_TAC arith_ss 1720 [SEL_REC_SPLIT, RESTN_CAT, LENGTH_SEL_REC, GSYM CAT_APPEND, 1721 SEL_REC_RESTN] 1722 ++ RW_TAC std_ss [ADD1] 1723 ++ ONCE_REWRITE_TAC [ADD_COMM] 1724 ++ RW_TAC arith_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1725 ++ METIS_TAC [IS_INFINITE_def, IS_INFINITE_CAT, IS_INFINITE_EXISTS]) 1726 ++ Q.PAT_ASSUM `US_SEM X Y` MP_TAC 1727 ++ MATCH_MP_TAC (PROVE [] ``(a = b) ==> (a ==> b)``) 1728 ++ AP_THM_TAC 1729 ++ AP_TERM_TAC 1730 ++ Know `SUC n + j = n + (j + 1)` >> DECIDE_TAC 1731 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 1732 ++ CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV [SEL_REC_SPLIT]))) 1733 ++ RW_TAC arith_ss [GSYM CAT_APPEND] 1734 ++ Q.SPEC_TAC (`CAT (SEL_REC n (j + 1) p,INFINITE w)`,`q`) 1735 ++ Q.SPEC_TAC (`p`,`p`) 1736 ++ Q.SPEC_TAC (`j + 1`,`j`) 1737 ++ Induct 1738 ++ RW_TAC std_ss [SEL_REC_def, CAT_def, HEAD_CONS, REST_CONS] 1739 ++ PROVE_TAC []]); 1740 1741(* The regexp checker *) 1742 1743val bool_checker_def = Define 1744 `(bool_checker (F_BOOL b) = b) /\ 1745 (bool_checker (F_NOT f) = B_NOT (bool_checker f)) /\ 1746 (bool_checker (F_AND (f,g)) = B_AND (bool_checker f, bool_checker g))`; 1747 1748val boolean_checker_def = Define 1749 `boolean_checker f = S_BOOL (bool_checker (F_NOT f))`; 1750 1751val checker_def = Define 1752 `(checker (F_BOOL b) = boolean_checker (F_BOOL b)) /\ 1753 (checker (F_NOT (F_NOT f)) = checker f) /\ 1754 (checker (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)), _))) = 1755 S_CAT 1756 (S_REPEAT (boolean_checker g), 1757 S_FLEX_AND (checker f, boolean_checker g))) /\ 1758 (checker (F_NOT (F_AND (f,g))) = 1759 S_FLEX_AND (checker (F_NOT f), checker (F_NOT g))) /\ 1760 (checker (F_NOT f) = boolean_checker (F_NOT f)) /\ 1761 (checker (F_AND (f,g)) = S_OR (checker f, checker g)) /\ 1762 (checker (F_NEXT f) = S_CAT (S_TRUE, checker f)) /\ 1763 (checker (F_SUFFIX_IMP (r,f)) = S_FUSION (r, checker f))`; 1764 1765val boolean_checker_CLOCK_FREE = store_thm 1766 ("boolean_checker_CLOCK_FREE", 1767 ``!f. boolean f ==> S_CLOCK_FREE (boolean_checker f)``, 1768 Induct 1769 ++ RW_TAC std_ss [simple_def, S_CLOCK_FREE_def, boolean_checker_def]); 1770 1771val boolean_checker_initially_ok = store_thm 1772 ("boolean_checker_initially_ok", 1773 ``!f. boolean f ==> ~US_SEM [] (boolean_checker f)``, 1774 recInduct simple_ind 1775 ++ REPEAT CONJ_TAC 1776 ++ RW_TAC arith_ss [boolean_def, boolean_checker_def, bool_checker_def] 1777 ++ ONCE_REWRITE_TAC [US_SEM_def] 1778 ++ RW_TAC arith_ss [listTheory.LENGTH]); 1779 1780val boolean_checker = store_thm 1781 ("boolean_checker", 1782 ``!f p. 1783 boolean f /\ IS_INFINITE p ==> 1784 (safety_violation p f = 1785 ?n. amatch (sere2regexp (boolean_checker f)) (SEL p (0,n)))``, 1786 SIMP_TAC arith_ss 1787 [amatch, GSYM sere2regexp, boolean_checker_CLOCK_FREE, 1788 boolean_safety_violation, boolean_checker_def, bool_checker_def, 1789 US_SEM_def, B_SEM, UF_SEM_def, LENGTH_SEL, ELEM_SEL] 1790 ++ INDUCT_THEN fl_induct ASSUME_TAC 1791 ++ REPEAT (POP_ASSUM MP_TAC) 1792 ++ SIMP_TAC arith_ss 1793 [boolean_def, bool_checker_def, UF_SEM_def, LENGTH_def, HD, 1794 ELEM_def, GT, B_SEM_def, RESTN_def, HEAD_def, listTheory.LENGTH]); 1795 1796val boolean_checker_SEL_REC = store_thm 1797 ("boolean_checker_SEL_REC", 1798 ``!f p. 1799 boolean f /\ IS_INFINITE p ==> 1800 (safety_violation p f = 1801 ?n. amatch (sere2regexp (boolean_checker f)) (SEL_REC n 0 p))``, 1802 RW_TAC arith_ss 1803 [boolean_checker, SEL_def, amatch, GSYM sere2regexp, 1804 boolean_checker_CLOCK_FREE] 1805 ++ EQ_TAC >> PROVE_TAC [] 1806 ++ STRIP_TAC 1807 ++ POP_ASSUM MP_TAC 1808 ++ REVERSE (Cases_on `n`) >> PROVE_TAC [ADD1] 1809 ++ RW_TAC std_ss [SEL_REC_def, boolean_checker_initially_ok]); 1810 1811val boolean_checker_US_SEM = store_thm 1812 ("boolean_checker_US_SEM", 1813 ``!f p. 1814 boolean f /\ IS_INFINITE p ==> 1815 (safety_violation p f = 1816 ?n. US_SEM (SEL_REC n 0 p) (boolean_checker f))``, 1817 SIMP_TAC std_ss 1818 [boolean_checker_SEL_REC, amatch, GSYM sere2regexp, 1819 boolean_checker_CLOCK_FREE]); 1820 1821val US_SEM_boolean_checker = store_thm 1822 ("US_SEM_boolean_checker", 1823 ``!f w. 1824 US_SEM w (boolean_checker f) = 1825 (?x. (w = [x]) /\ US_SEM [x] (boolean_checker f))``, 1826 RW_TAC std_ss [US_SEM_def, boolean_checker_def] 1827 ++ Cases_on `w` >> RW_TAC std_ss [LENGTH] 1828 ++ REVERSE (Cases_on `t`) >> RW_TAC bool_ss [LENGTH, ONE] 1829 ++ RW_TAC std_ss []); 1830 1831val US_SEM_boolean_checker_SEL_REC = store_thm 1832 ("US_SEM_boolean_checker_SEL_REC", 1833 ``!f n m p. 1834 US_SEM (SEL_REC n m p) (boolean_checker f) = 1835 (n = 1) /\ US_SEM (SEL_REC 1 m p) (boolean_checker f)``, 1836 RW_TAC std_ss [] 1837 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_boolean_checker])) 1838 ++ Cases_on `n` >> RW_TAC std_ss [SEL_REC_def] 1839 ++ EQ_TAC 1840 << [STRIP_TAC 1841 ++ MATCH_MP_TAC (PROVE [] ``(a ==> b) /\ a ==> a /\ b``) 1842 ++ CONJ_TAC >> PROVE_TAC [] 1843 ++ METIS_TAC [LENGTH_SEL_REC, ONE, LENGTH], 1844 RW_TAC bool_ss [ONE] 1845 ++ Cases_on `SEL_REC (SUC 0) m p` 1846 >> PROVE_TAC [LENGTH_SEL_REC, LENGTH, numTheory.NOT_SUC] 1847 ++ Suff `t = []` >> PROVE_TAC [] 1848 ++ Cases_on `t` >> RW_TAC std_ss [] 1849 ++ PROVE_TAC [LENGTH_SEL_REC, LENGTH, numTheory.NOT_SUC, 1850 prim_recTheory.INV_SUC_EQ]]); 1851 1852val US_SEM_boolean_checker_CONJ = store_thm 1853 ("US_SEM_boolean_checker_CONJ", 1854 ``!f p. 1855 (?w. US_SEM w (boolean_checker f) /\ p w f) = 1856 (?x. US_SEM [x] (boolean_checker f) /\ p [x] f)``, 1857 RW_TAC std_ss [US_SEM_def, boolean_checker_def] 1858 ++ MATCH_MP_TAC EQ_SYM 1859 ++ MP_TAC 1860 (PROVE [list_CASES] 1861 ``!p q. (q = p [] \/ ?t (h : 'a -> bool). p (h::t)) ==> (q = ?l. p l)``) 1862 ++ DISCH_THEN (fn th => HO_MATCH_MP_TAC th ++ ASSUME_TAC th) 1863 ++ SIMP_TAC std_ss [LENGTH] 1864 ++ POP_ASSUM HO_MATCH_MP_TAC 1865 ++ RW_TAC arith_ss [LENGTH]); 1866 1867val boolean_checker_US_SEM1 = store_thm 1868 ("boolean_checker_US_SEM1", 1869 ``!f p. 1870 boolean f /\ IS_INFINITE p ==> 1871 (US_SEM (SEL_REC 1 0 p) (boolean_checker f) = ~UF_SEM p f)``, 1872 RW_TAC std_ss [] 1873 ++ MP_TAC (Q.SPECL [`f`, `p`] (GSYM boolean_checker_US_SEM)) 1874 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [US_SEM_boolean_checker_SEL_REC])) 1875 ++ RW_TAC std_ss [] 1876 ++ RW_TAC std_ss [simple_safety, boolean_simple]); 1877 1878val checker_initially_ok = store_thm 1879 ("checker_initially_ok", 1880 ``!f. simple f ==> ~US_SEM [] (checker f)``, 1881 recInduct simple_ind 1882 ++ REPEAT CONJ_TAC 1883 ++ RW_TAC arith_ss [simple_def, checker_def, boolean_checker_def, 1884 bool_checker_def] 1885 ++ ONCE_REWRITE_TAC [US_SEM_def] 1886 ++ ONCE_REWRITE_TAC [US_SEM_def] 1887 ++ RW_TAC arith_ss [listTheory.LENGTH, US_SEM_REPEAT_TRUE, 1888 listTheory.APPEND_eq_NIL, S_FLEX_AND_EMPTY] 1889 ++ RW_TAC std_ss [US_SEM_def, S_TRUE_def, LENGTH]); 1890 1891val checker_CLOCK_FREE = store_thm 1892 ("checker_CLOCK_FREE", 1893 ``!f. simple f ==> S_CLOCK_FREE (checker f)``, 1894 recInduct simple_ind 1895 ++ REPEAT CONJ_TAC 1896 ++ RW_TAC std_ss [simple_def, S_CLOCK_FREE_def, checker_def, S_TRUE_def, 1897 boolean_checker_CLOCK_FREE, S_FLEX_AND_def, S_FALSE_def] 1898 ++ PROVE_TAC [boolean_def, boolean_checker_CLOCK_FREE]); 1899 1900val checker_NOT_AND = store_thm 1901 ("checker_NOT_AND", 1902 ``!f g. 1903 (!p. 1904 simple (F_NOT f) /\ IS_INFINITE p ==> 1905 (safety_violation p (F_NOT f) = 1906 ?n. US_SEM (SEL_REC n 0 p) (checker (F_NOT f)))) /\ 1907 (!p. 1908 simple (F_NOT g) /\ IS_INFINITE p ==> 1909 (safety_violation p (F_NOT g) = 1910 ?n. US_SEM (SEL_REC n 0 p) (checker (F_NOT g)))) ==> 1911 !p. 1912 (simple (F_NOT f) /\ simple (F_NOT g)) /\ IS_INFINITE p ==> 1913 (safety_violation p (F_NOT (F_AND (f,g))) = 1914 ?n. 1915 US_SEM (SEL_REC n 0 p) 1916 (S_FLEX_AND (checker (F_NOT f),checker (F_NOT g))))``, 1917 RW_TAC std_ss [safety_violation_alt, UF_SEM_def, S_FLEX_AND] 1918 ++ REPEAT (Q.PAT_ASSUM `!x. P x` (fn th => RW_TAC std_ss [GSYM th])) 1919 ++ EQ_TAC >> PROVE_TAC [] 1920 ++ RW_TAC std_ss [] 1921 ++ Know `n <= n' \/ n' <= n` >> DECIDE_TAC 1922 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 1923 << [Q.EXISTS_TAC `n + p'` 1924 ++ RW_TAC std_ss [] 1925 ++ ONCE_REWRITE_TAC [ADD_COMM] 1926 ++ RW_TAC arith_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1927 ++ PROVE_TAC [IS_INFINITE_CAT, IS_INFINITE_EXISTS], 1928 Q.EXISTS_TAC `n' + p'` 1929 ++ RW_TAC std_ss [] 1930 ++ ONCE_REWRITE_TAC [ADD_COMM] 1931 ++ RW_TAC arith_ss [SEL_REC_SPLIT, GSYM CAT_APPEND] 1932 ++ PROVE_TAC [IS_INFINITE_CAT, IS_INFINITE_EXISTS]]); 1933 1934val checker_AND = store_thm 1935 ("checker_AND", 1936 ``!f g. 1937 (!p. 1938 simple f /\ IS_INFINITE p ==> 1939 (safety_violation p f = 1940 ?n. US_SEM (SEL_REC n 0 p) (checker f))) /\ 1941 (!p. 1942 simple g /\ IS_INFINITE p ==> 1943 (safety_violation p g = 1944 ?n. US_SEM (SEL_REC n 0 p) (checker g))) ==> 1945 !p. 1946 (simple f /\ simple g) /\ IS_INFINITE p ==> 1947 (safety_violation p (F_AND (f,g)) = 1948 ?n. US_SEM (SEL_REC n 0 p) (S_OR (checker f,checker g)))``, 1949 RW_TAC std_ss [simple_safety, simple_def, UF_SEM_def, US_SEM_def] 1950 ++ METIS_TAC []); 1951 1952val checker_NEXT = store_thm 1953 ("checker_NEXT", 1954 ``!f. 1955 (!p. 1956 simple f /\ IS_INFINITE p ==> 1957 (safety_violation p f = 1958 ?n. US_SEM (SEL_REC n 0 p) (checker f))) ==> 1959 !p. 1960 simple f /\ IS_INFINITE p ==> 1961 (safety_violation p (F_NEXT f) = 1962 ?n. US_SEM (SEL_REC n 0 p) (S_CAT (S_TRUE,checker f)))``, 1963 RW_TAC std_ss [] 1964 ++ RW_TAC arith_suc_ss 1965 [safety_violation_alt, UF_SEM_def, US_SEM_def, LENGTH_CAT, 1966 S_TRUE_def, GT, B_SEM, RESTN_def, REST_CAT, SEL_NIL] 1967 ++ Know `!P Q. (P 0 \/ (?n. P (SUC n)) = Q) ==> ((?n. P n) = Q)` 1968 >> PROVE_TAC [arithmeticTheory.num_CASES] 1969 ++ DISCH_THEN HO_MATCH_MP_TAC 1970 ++ RW_TAC std_ss [SEL_REC_def, CAT_def, REST_CONS] 1971 ++ MATCH_MP_TAC (PROVE [] ``(a ==> b) /\ (b = c) ==> (a \/ b = c)``) 1972 ++ CONJ_TAC 1973 >> (RW_TAC std_ss [] 1974 ++ Q.EXISTS_TAC `0` 1975 ++ RW_TAC std_ss [SEL_REC_def, CAT_def] 1976 ++ Know `!q. IS_INFINITE q ==> ~UF_SEM (REST q) f` 1977 >> PROVE_TAC [IS_INFINITE_def, path_nchotomy] 1978 ++ DISCH_THEN (MP_TAC o Q.SPEC `CONS (x, INFINITE w)`) 1979 ++ RW_TAC std_ss [REST_CONS, IS_INFINITE_CONS, IS_INFINITE_def]) 1980 ++ RW_TAC std_ss [GSYM safety_violation_alt, IS_INFINITE_REST] 1981 ++ Know `!P Q. (P = (?n. Q n []) \/ (?n h. Q n [h]) \/ 1982 (?h1 h2 t n. Q n (h1 :: h2 :: t))) ==> 1983 (P = ?n w1. Q (n : num) (w1 : ('a -> bool) list))` 1984 >> metisLib.METIS_TAC [list_CASES] 1985 ++ DISCH_THEN HO_MATCH_MP_TAC 1986 ++ RW_TAC arith_suc_ss [LENGTH, APPEND] 1987 ++ Know `!P Q. (?h w2. P h (w2 : ('a -> bool) list) /\ Q w2) = 1988 ?w2. (?h : 'a -> bool. P h w2) /\ Q w2` 1989 >> PROVE_TAC [] 1990 ++ DISCH_THEN (fn th => SIMP_TAC std_ss [th]) 1991 ++ Know `!P Q. (Q = P 0 \/ ?n. P (SUC n)) ==> (Q = ?n. P n)` 1992 >> PROVE_TAC [arithmeticTheory.num_CASES] 1993 ++ DISCH_THEN HO_MATCH_MP_TAC 1994 ++ RW_TAC arith_suc_ss [SEL_REC_def, TL, checker_initially_ok]); 1995 1996val checker_UNTIL = store_thm 1997 ("checker_UNTIL", 1998 ``!f g h. 1999 (!p. 2000 simple f /\ IS_INFINITE p ==> 2001 (safety_violation p f = 2002 ?n. US_SEM (SEL_REC n 0 p) (checker f))) ==> 2003 !p. 2004 (simple f /\ boolean g /\ 2005 (h = F_UNTIL (F_BOOL B_TRUE,F_NOT f))) /\ IS_INFINITE p ==> 2006 (safety_violation p (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)),h))) = 2007 ?n. 2008 US_SEM (SEL_REC n 0 p) 2009 (S_CAT 2010 (S_REPEAT (boolean_checker g), 2011 S_FLEX_AND (checker f,boolean_checker g))))``, 2012 RW_TAC std_ss [] 2013 ++ Know 2014 `safety_violation p 2015 (F_NOT (F_AND (F_NOT (F_UNTIL (f,g)),F_UNTIL (F_BOOL B_TRUE,F_NOT f)))) = 2016 safety_violation p (F_W (f,g))` 2017 >> (RW_TAC std_ss 2018 [safety_violation_def, UF_SEM_def, F_W_def, F_OR_def, F_G_def, F_F_def]) 2019 ++ DISCH_THEN (fn th => SIMP_TAC std_ss [th]) 2020 ++ RW_TAC arith_resq_ss 2021 [safety_violation_alt, UF_SEM_F_W_ALT, LENGTH_CAT, S_TRUE_def] 2022 ++ Know `!m n. (m:num) < SUC n = m <= n` >> DECIDE_TAC 2023 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 2024 ++ SIMP_TAC arith_ss [GSYM IMP_DISJ_THM] 2025 ++ REVERSE EQ_TAC 2026 >> (RW_TAC std_ss [S_CAT_SEL_REC, S_FLEX_AND] 2027 ++ Q.EXISTS_TAC `m + n` 2028 ++ POP_ASSUM MP_TAC 2029 ++ ONCE_REWRITE_TAC [US_SEM_boolean_checker_SEL_REC] 2030 ++ RW_TAC std_ss [RESTN_RESTN] 2031 ++ Q.EXISTS_TAC `m` 2032 ++ CONJ_TAC 2033 >> (ONCE_REWRITE_TAC [ADD_COMM] 2034 ++ RW_TAC arith_ss 2035 [SEL_REC_SPLIT, LENGTH_SEL_REC, RESTN_CAT, GSYM CAT_APPEND] 2036 ++ Know `m = 0 + m` >> DECIDE_TAC 2037 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 2038 ++ RW_TAC std_ss [GSYM SEL_REC_RESTN] 2039 ++ MATCH_MP_TAC safety_violation_refl 2040 ++ RW_TAC std_ss 2041 [IS_INFINITE_CAT, IS_INFINITE_def, IS_INFINITE_RESTN] 2042 ++ Q.EXISTS_TAC `n` 2043 ++ RW_TAC std_ss [SEL_REC_CAT_0, LENGTH_SEL_REC]) 2044 ++ RW_TAC std_ss [] 2045 ++ STRIP_TAC 2046 ++ Q.PAT_ASSUM `k <= m` MP_TAC 2047 ++ Suff `~(k = m) /\ m <= k` >> DECIDE_TAC 2048 ++ CONJ_TAC 2049 >> (STRIP_TAC 2050 ++ RW_TAC arith_ss [] 2051 ++ POP_ASSUM MP_TAC 2052 ++ RW_TAC std_ss [] 2053 ++ MATCH_MP_TAC safety_violation_refl 2054 ++ RW_TAC std_ss 2055 [IS_INFINITE_RESTN, IS_INFINITE_CAT, IS_INFINITE_def, 2056 boolean_checker_US_SEM] 2057 ++ Q.EXISTS_TAC `1` 2058 ++ POP_ASSUM MP_TAC 2059 ++ MATCH_MP_TAC (PROVE [] ``(a = b) ==> (a ==> b)``) 2060 ++ AP_THM_TAC 2061 ++ AP_TERM_TAC 2062 ++ RW_TAC arith_ss [SEL_REC_RESTN] 2063 ++ ONCE_REWRITE_TAC [ADD_COMM] 2064 ++ RW_TAC arith_ss 2065 [SEL_REC_SPLIT, GSYM CAT_APPEND, SEL_REC_CAT, LENGTH_SEL_REC] 2066 ++ Know `~(n = 0)` >> PROVE_TAC [checker_initially_ok, SEL_REC_def] 2067 ++ STRIP_TAC 2068 ++ Know `1 <= n` >> DECIDE_TAC 2069 ++ RW_TAC std_ss [LESS_EQ_EXISTS] 2070 ++ RW_TAC std_ss [] 2071 ++ ONCE_REWRITE_TAC [ADD_COMM] 2072 ++ RW_TAC std_ss 2073 [SEL_REC_SPLIT, GSYM CAT_APPEND, SEL_REC_CAT_0, LENGTH_SEL_REC]) 2074 ++ Q.PAT_ASSUM `UF_SEM X Y` MP_TAC 2075 ++ Q.PAT_ASSUM `US_SEM X (S_REPEAT Y)` MP_TAC 2076 ++ Q.PAT_ASSUM `IS_INFINITE p` MP_TAC 2077 ++ Q.SPEC_TAC (`p`,`p`) 2078 ++ Q.SPEC_TAC (`k`,`k`) 2079 ++ Q.SPEC_TAC (`m`,`m`) 2080 ++ Q.PAT_ASSUM `boolean g` MP_TAC 2081 ++ POP_ASSUM_LIST (K ALL_TAC) 2082 ++ STRIP_TAC 2083 ++ SIMP_TAC std_ss [AND_IMP_INTRO] 2084 ++ Induct 2085 ++ RW_TAC arith_ss [] 2086 ++ Q.PAT_ASSUM `US_SEM X Y` MP_TAC 2087 ++ ONCE_REWRITE_TAC [GSYM S_REPEAT_UNWIND] 2088 ++ ONCE_REWRITE_TAC [US_SEM_def] 2089 ++ SIMP_TAC std_ss [S_EMPTY, S_CAT_SEL_REC0] 2090 ++ STRIP_TAC >> PROVE_TAC [LENGTH_SEL_REC, LENGTH, numTheory.NOT_SUC] 2091 ++ REPEAT (Q.PAT_ASSUM `US_SEM X Y` MP_TAC) 2092 ++ ONCE_REWRITE_TAC [US_SEM_boolean_checker_SEL_REC] 2093 ++ RW_TAC arith_ss [] 2094 ++ Cases_on `k` 2095 >> (RW_TAC arith_ss [] 2096 ++ Q.PAT_ASSUM `!k. P k` (K ALL_TAC) 2097 ++ Q.PAT_ASSUM `UF_SEM X Y` MP_TAC 2098 ++ RW_TAC std_ss [RESTN_def] 2099 ++ MATCH_MP_TAC safety_violation_refl 2100 ++ RW_TAC std_ss 2101 [IS_INFINITE_RESTN, IS_INFINITE_CAT, IS_INFINITE_def, 2102 boolean_checker_US_SEM] 2103 ++ Q.EXISTS_TAC `1` 2104 ++ Know `n + SUC m = (n + m) + 1` >> DECIDE_TAC 2105 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 2106 ++ ONCE_REWRITE_TAC [SEL_REC_SPLIT] 2107 ++ RW_TAC std_ss [GSYM CAT_APPEND, SEL_REC_CAT_0, LENGTH_SEL_REC]) 2108 ++ RW_TAC arith_ss [] 2109 ++ FIRST_ASSUM MATCH_MP_TAC 2110 ++ Q.EXISTS_TAC `REST p` 2111 ++ POP_ASSUM MP_TAC 2112 ++ RW_TAC bool_ss [IS_INFINITE_REST, ONE, RESTN_def] 2113 ++ Q.PAT_ASSUM `UF_SEM X Y` MP_TAC 2114 ++ MATCH_MP_TAC (PROVE [] ``(a = b) ==> (a ==> b)``) 2115 ++ AP_THM_TAC 2116 ++ AP_TERM_TAC 2117 ++ RW_TAC std_ss [RESTN_def, ADD_CLAUSES, SEL_REC_def, REST_CAT, TL] 2118 ++ PROVE_TAC [ADD_COMM]) 2119 ++ STRIP_TAC 2120 ++ RW_TAC std_ss [S_CAT_SEL_REC, S_FLEX_AND] 2121 ++ ONCE_REWRITE_TAC [US_SEM_boolean_checker_SEL_REC] 2122 ++ RW_TAC std_ss [] 2123 ++ Know `?w. INFINITE w = RESTN p n` 2124 >> METIS_TAC [IS_INFINITE_EXISTS, IS_INFINITE_RESTN] 2125 ++ STRIP_TAC 2126 ++ Q.PAT_ASSUM `!w. P w` (MP_TAC o Q.SPEC `w`) 2127 ++ RW_TAC std_ss [CAT_SEL_REC_RESTN] 2128 ++ Q.PAT_ASSUM `INFINITE w = x` (K ALL_TAC) 2129 ++ Q.PAT_ASSUM `!p : ('a -> bool) path. P p` (MP_TAC o Q.SPEC `RESTN p j`) 2130 ++ RW_TAC std_ss [IS_INFINITE_RESTN, simple_safety] 2131 ++ Q.EXISTS_TAC `j` 2132 ++ REVERSE CONJ_TAC 2133 >> (CONJ_TAC >> METIS_TAC [] 2134 ++ RW_TAC std_ss [boolean_checker_US_SEM1, IS_INFINITE_RESTN] 2135 ++ PROVE_TAC [LESS_EQ_REFL]) 2136 ++ Know `j = j + 0` >> DECIDE_TAC 2137 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 2138 ++ Know `p = RESTN p (j - (j + 0))` >> RW_TAC arith_ss [RESTN_def] 2139 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 2140 ++ Know `j + 0 <= j` >> DECIDE_TAC 2141 ++ Q.SPEC_TAC (`j + 0`, `k`) 2142 ++ Induct 2143 >> (RW_TAC std_ss [SEL_REC_def, US_SEM_def] 2144 ++ METIS_TAC [CONCAT_def, EVERY_DEF]) 2145 ++ ONCE_REWRITE_TAC [GSYM S_REPEAT_UNWIND] 2146 ++ ONCE_REWRITE_TAC [US_SEM_def] 2147 ++ ONCE_REWRITE_TAC [US_SEM_def] 2148 ++ RW_TAC std_ss [] 2149 ++ DISJ2_TAC 2150 ++ RW_TAC std_ss [ADD1, SEL_REC_SPLIT] 2151 ++ Q.PAT_ASSUM `X ==> Y` MP_TAC 2152 ++ (MP_TAC o Q.SPEC `k` o GENL [``m:num``,``n:num``,``r:num``] o 2153 INST_TYPE [alpha |-> ``:'a -> bool``]) SEL_REC_RESTN 2154 ++ RW_TAC arith_ss [] 2155 ++ Q.EXISTS_TAC `SEL_REC 1 0 (RESTN p (j - (k + 1)))` 2156 ++ Q.EXISTS_TAC `SEL_REC k (j - k) p` 2157 ++ RW_TAC std_ss [] 2158 ++ RW_TAC std_ss [boolean_checker_US_SEM1, IS_INFINITE_RESTN] 2159 ++ FIRST_ASSUM MATCH_MP_TAC 2160 ++ DECIDE_TAC); 2161 2162val checker_SEL_REC = store_thm 2163 ("checker_SEL_REC", 2164 ``!f p. 2165 simple f /\ IS_INFINITE p ==> 2166 (safety_violation p f = 2167 ?n. amatch (sere2regexp (checker f)) (SEL_REC n 0 p))``, 2168 SIMP_TAC std_ss [amatch, GSYM sere2regexp, checker_CLOCK_FREE] 2169 ++ recInduct simple_ind 2170 ++ (REPEAT CONJ_TAC 2171 ++ TRY (ASM_SIMP_TAC std_ss [simple_def, boolean_def] ++ NO_TAC) 2172 ++ SIMP_TAC std_ss [boolean_def]) 2173 << [(* F_BOOL *) 2174 RW_TAC std_ss [boolean_checker_US_SEM, boolean_def, checker_def], 2175 2176 (* F_NOT (F_NOT f) *) 2177 RW_TAC std_ss [safety_violation_def, UF_SEM_def, simple_def, checker_def] 2178 ++ RW_TAC std_ss [GSYM safety_violation_def], 2179 2180 (* F_NOT (F_AND (F_NOT (F_UNTIL (f,g)), _)) *) 2181 ONCE_REWRITE_TAC [simple_def, checker_def] 2182 ++ METIS_TAC [checker_UNTIL], 2183 2184 (* F_NOT (F_AND (f,g)) *) 2185 RW_TAC std_ss [] 2186 ++ Q.PAT_ASSUM `simple X` MP_TAC 2187 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2188 ++ RW_TAC std_ss [boolean_def] 2189 ++ METIS_TAC [checker_NOT_AND], 2190 RW_TAC std_ss [] 2191 ++ Q.PAT_ASSUM `simple X` MP_TAC 2192 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2193 ++ RW_TAC std_ss [boolean_def] 2194 ++ METIS_TAC [checker_NOT_AND], 2195 RW_TAC std_ss [] 2196 ++ Q.PAT_ASSUM `simple X` MP_TAC 2197 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2198 ++ RW_TAC std_ss [boolean_def] 2199 ++ METIS_TAC [checker_NOT_AND], 2200 RW_TAC std_ss [] 2201 ++ Q.PAT_ASSUM `simple X` MP_TAC 2202 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2203 ++ RW_TAC std_ss [boolean_def] 2204 ++ METIS_TAC [checker_NOT_AND], 2205 RW_TAC std_ss [] 2206 ++ Q.PAT_ASSUM `simple X` MP_TAC 2207 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2208 ++ RW_TAC std_ss [boolean_def] 2209 ++ METIS_TAC [checker_NOT_AND], 2210 RW_TAC std_ss [] 2211 ++ Q.PAT_ASSUM `simple X` MP_TAC 2212 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2213 ++ RW_TAC std_ss [boolean_def] 2214 ++ METIS_TAC [checker_NOT_AND], 2215 RW_TAC std_ss [] 2216 ++ Q.PAT_ASSUM `simple X` MP_TAC 2217 ++ ONCE_REWRITE_TAC [simple_def, checker_def] 2218 ++ RW_TAC std_ss [boolean_def] 2219 ++ METIS_TAC [checker_NOT_AND], 2220 2221 (* F_NOT (F_BOOL b) *) 2222 RW_TAC std_ss 2223 [boolean_checker_US_SEM, boolean_def, simple_def, checker_def], 2224 2225 (* F_AND (f,g) *) 2226 ONCE_REWRITE_TAC [simple_def, checker_def] 2227 ++ METIS_TAC [checker_AND], 2228 2229 (* F_NEXT f *) 2230 ONCE_REWRITE_TAC [simple_def, checker_def] 2231 ++ METIS_TAC [checker_NEXT], 2232 2233 (* F_SUFFIX_IMP (r,f) *) 2234 RW_TAC arith_resq_ss 2235 [simple_def, checker_def, simple_safety, UF_SEM_def, 2236 LENGTH_IS_INFINITE, SEL_def, IS_INFINITE_RESTN, S_FUSION_SEL_REC] 2237 ++ REVERSE EQ_TAC >> METIS_TAC [] 2238 ++ RW_TAC std_ss [] 2239 ++ REVERSE (Cases_on `n`) >> METIS_TAC [ADD1] 2240 ++ METIS_TAC [SEL_REC_def, checker_initially_ok]]); 2241 2242val checker = store_thm 2243 ("checker", 2244 ``!f p. 2245 simple f /\ IS_INFINITE p ==> 2246 (safety_violation p f = 2247 ?n. amatch (sere2regexp (checker f)) (SEL p (0,n)))``, 2248 RW_TAC arith_ss [checker_SEL_REC, SEL_def] 2249 ++ REVERSE EQ_TAC >> METIS_TAC [] 2250 ++ RW_TAC std_ss [amatch, GSYM sere2regexp, checker_CLOCK_FREE] 2251 ++ REVERSE (Cases_on `n`) >> METIS_TAC [ADD1] 2252 ++ METIS_TAC [SEL_REC_def, checker_initially_ok]); 2253 2254(****************************************************************************** 2255* Beginning of some stuff that turned out to be useless for execution. 2256* Leaving it here as just conceivably a future use might appear! 2257******************************************************************************) 2258 2259(****************************************************************************** 2260* Formula version of an operator due to Dana Fisman 2261******************************************************************************) 2262val F_PREF_def = 2263 pureDefine `F_PREF w f = ?w'. UF_SEM (CAT(w,w')) f`; 2264 2265val EXISTS_RES_to = 2266 store_thm 2267 ("EXISTS_RES_to", 2268 ``!m n P. 2269 (?j :: (m to n). P j n) = (m < n) /\ (P m n \/ ?j :: ((m+1) to n). P j n)``, 2270 Cases_on `n` 2271 THEN RW_TAC std_resq_ss [num_to_def,xnum_to_def,LS] 2272 THENL 2273 [PROVE_TAC[DECIDE ``m <= j = (m=j) \/ m+1 <= j``], 2274 EQ_TAC 2275 THEN RW_TAC std_ss [] 2276 THEN TRY(PROVE_TAC[DECIDE ``m <= j = (m=j) \/ m+1 <= j``]) 2277 THEN DECIDE_TAC]); 2278 2279val ABORT_AUX_def = 2280 pureDefine 2281 `ABORT_AUX w f b n = 2282 ?(j::n to LENGTH w). 2283 UF_SEM (RESTN w j) (F_BOOL b) /\ F_PREF (SEL w (0,j - 1)) f`; 2284 2285val EXISTS_RES_to_COR = 2286 SIMP_RULE std_ss [] 2287 (Q.SPECL 2288 [`n`,`LENGTH(w :('a -> bool) path)`, 2289 `\j n. UF_SEM (RESTN w j) (F_BOOL b) /\ F_PREF (SEL w (0,j - 1)) f`] 2290 EXISTS_RES_to); 2291 2292val ABORT_AUX_REC = 2293 store_thm 2294 ("ABORT_AUX_REC", 2295 ``ABORT_AUX w f b n 2296 = n < LENGTH w /\ 2297 (UF_SEM (RESTN w n) (F_BOOL b) /\ F_PREF (SEL w (0,n - 1)) f 2298 \/ 2299 ABORT_AUX w f b (n+1))``, 2300 RW_TAC std_ss [ABORT_AUX_def] 2301 THEN ACCEPT_TAC EXISTS_RES_to_COR); 2302 2303val UF_ABORT_REC = 2304 store_thm 2305 ("UF_ABORT_REC", 2306 ``UF_SEM w (F_ABORT (f,b)) = 2307 UF_SEM w f \/ UF_SEM w (F_BOOL b) \/ ABORT_AUX w f b 1``, 2308 RW_TAC std_resq_ss [UF_SEM_def,F_PREF_def,ABORT_AUX_def] 2309 THEN PROVE_TAC[]); 2310 2311(****************************************************************************** 2312* End of useless stuff. 2313******************************************************************************) 2314 2315 2316val _ = export_theory(); 2317