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