1 2(*****************************************************************************) 3(* Some properties of the Sugar 2.0 semantics *) 4(* ------------------------------------------------------------------------- *) 5(* *) 6(* Started: Tue Dec 31 2002 *) 7(* Semantics changed (additional ``LENGTH w > 0`` added): Mon Feb 10 2003 *) 8(*****************************************************************************) 9 10(*****************************************************************************) 11(* START BOILERPLATE *) 12(*****************************************************************************) 13 14(****************************************************************************** 15* Load theories 16* (commented out for compilation) 17******************************************************************************) 18(* 19quietdec := true; 20loadPath := "../official-semantics" :: "../regexp" :: !loadPath; 21map load 22 ["bossLib", "KripkeTheory", "UnclockedSemanticsTheory", 23 "SyntacticSugarTheory", "ClockedSemanticsTheory", "RewritesTheory", 24 "rich_listTheory", "intLib", "res_quanLib", "res_quanTheory"]; 25open KripkeTheory FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 26 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 27 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory 28 ClockedSemanticsTheory; 29val _ = intLib.deprecate_int(); 30quietdec := false; 31*) 32 33(****************************************************************************** 34* Boilerplate needed for compilation 35******************************************************************************) 36open HolKernel Parse boolLib bossLib; 37 38(****************************************************************************** 39* Open theories 40******************************************************************************) 41open KripkeTheory FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 42 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 43 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory 44 ClockedSemanticsTheory; 45 46(*****************************************************************************) 47(* END BOILERPLATE *) 48(*****************************************************************************) 49 50(****************************************************************************** 51* Versions of simpsets that deal properly with theorems containing SUC 52******************************************************************************) 53val simp_arith_ss = simpLib.++ (arith_ss, numSimps.SUC_FILTER_ss); 54val simp_list_ss = simpLib.++ (list_ss, numSimps.SUC_FILTER_ss); 55 56(****************************************************************************** 57* Set default parsing to natural numbers rather than integers 58******************************************************************************) 59val _ = intLib.deprecate_int(); 60 61(****************************************************************************** 62* A simpset fragment to rewrite away quantifiers restricted with :: (a to b) 63******************************************************************************) 64val resq_SS = 65 simpLib.merge_ss 66 [res_quanTools.resq_SS, 67 rewrites 68 [num_to_def,xnum_to_def,IN_DEF,num_to_def,xnum_to_def,LENGTH_def]]; 69 70(****************************************************************************** 71* Start a new theory called Properties 72******************************************************************************) 73val _ = new_theory "Properties"; 74val _ = ParseExtras.temp_loose_equality() 75 76 77(****************************************************************************** 78* Set default path theory to FinitePSLPathTheory 79******************************************************************************) 80local open FinitePSLPathTheory in 81 82(****************************************************************************** 83* w |=T b is equivalent to ?l. (w =[l]) /\ l |= b 84******************************************************************************) 85val S_BOOL_TRUE = 86 store_thm 87 ("S_BOOL_TRUE", 88 ``S_SEM w B_TRUE (S_BOOL b) = ?l. (w =[l]) /\ B_SEM l b``, 89 RW_TAC (arith_ss ++ resq_SS) 90 [S_SEM_def,B_SEM,CONJ_ASSOC,LENGTH1,B_SEM_def, 91 Cooper.COOPER_PROVE``(n:num >= 1 /\ (!i:num. ~(i < n-1))) = (n = 1)``] 92 THEN EQ_TAC 93 THEN RW_TAC simp_list_ss [] 94 THEN FULL_SIMP_TAC simp_list_ss [LENGTH,ELEM_def,RESTN_def,HEAD_def]); 95 96(****************************************************************************** 97* Some lemmas about NEXT_RISE 98******************************************************************************) 99val S_REPEAT_BOOL_TRUE = 100 store_thm 101 ("S_REPEAT_BOOL_TRUE", 102 ``S_SEM w B_TRUE (S_REPEAT(S_BOOL b)) = 103 !i. i < LENGTH w ==> B_SEM (EL i w) b``, 104 RW_TAC (arith_ss ++ resq_SS) 105 [S_SEM_def,B_SEM,CONJ_ASSOC,LENGTH_CONS,LENGTH_NIL,ELEM_EL, 106 Cooper.COOPER_PROVE ``(n:num >= 1 /\ !i:num. ~(i < n-1)) = (n = 1)``] 107 THEN EQ_TAC 108 THEN RW_TAC std_ss [] 109 THENL 110 [IMP_RES_TAC 111 (SIMP_RULE std_ss [] (Q.ISPEC `\x. B_SEM x b` ALL_EL_CONCAT)) 112 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [EVERY_EL]) 113 THEN RES_TAC, 114 Q.EXISTS_TAC `MAP (\l. [l]) w` 115 THEN RW_TAC list_ss 116 [EVERY_EL,CONCAT_MAP_SINGLETON,LENGTH_EL_MAP_SINGLETON, 117 HD_EL_MAP]]); 118 119end; 120 121(****************************************************************************** 122* NEXT_RISE w c (i,j) = w^{i,j} |=T {(\neg c)[*];c} 123* (i is the first rising edge after j of clock c in word w) 124******************************************************************************) 125val NEXT_RISE_def = 126 Define 127 `NEXT_RISE w c (i,j) = 128 S_SEM 129 (SEL w (i,j)) 130 B_TRUE 131 (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c))`; 132 133val NEXT_RISE_IMP = 134 store_thm 135 ("NEXT_RISE_IMP", 136 ``NEXT_RISE p c (i,j) ==> 137 (!k. i <= k /\ k < j ==> ~B_SEM (ELEM p k) c) 138 /\ 139 (i <= j ==> B_SEM (ELEM p j) c)``, 140 REWRITE_TAC [NEXT_RISE_def,ELEM_EL] 141 THEN ONCE_REWRITE_TAC[S_SEM_def] 142 THEN SIMP_TAC list_ss 143 [S_REPEAT_BOOL_TRUE,S_BOOL_TRUE,B_SEM] 144 THEN ONCE_REWRITE_TAC [EQ_SINGLETON] 145 THEN RW_TAC std_ss [] 146 THENL 147 [ASSUM_LIST(fn thl => ASSUME_TAC(ONCE_REWRITE_RULE[el 4 thl](el 6 thl))) 148 THEN IMP_RES_TAC(DECIDE ``i <= k ==> k < j ==> k < j``) 149 THEN `j > i` by DECIDE_TAC 150 THEN IMP_RES_TAC SEL_APPEND_SINGLETON 151 THEN ASSUM_LIST(fn thl => ASSUME_TAC(Q.AP_TERM `EL (k-i)` (el 2 thl))) 152 THEN `k <= j-1` by DECIDE_TAC 153 THEN IMP_RES_TAC(Q.INST_TYPE[`:'a`|->`:'a->bool`]EL_SEL) 154 THEN `ELEM p k = EL (k - i) w1` by PROVE_TAC[] 155 THEN ASM_REWRITE_TAC [] 156 THEN ASSUM_LIST 157 (fn thl 158 => ASSUME_TAC 159 (Q.AP_TERM 160 `list$LENGTH` 161 (el 7 thl))) 162 THEN POP_ASSUM(ASSUME_TAC o REWRITE_RULE[LENGTH_SEL]) 163 THEN `k-i < LENGTH w1` by DECIDE_TAC 164 THEN PROVE_TAC[], 165 ASSUM_LIST(fn thl => ASSUME_TAC(ONCE_REWRITE_RULE[el 3 thl](el 5 thl))) 166 THEN ASSUM_LIST 167 (fn thl => 168 ASSUME_TAC 169 (SIMP_RULE arith_ss 170 [LENGTH_MAP,LENGTH_APPEND,LENGTH,SEL_def, 171 LENGTH_SEL_REC] 172 (Q.AP_TERM `list$LENGTH` (el 1 thl)))) 173 THEN Cases_on `i=j` 174 THENL 175 [`w1 = []` by PROVE_TAC [LENGTH_NIL, SUB_EQUAL_0] 176 THEN RW_TAC arith_ss [] 177 THEN FULL_SIMP_TAC list_ss [LENGTH,SEL_ELEM] 178 THEN PROVE_TAC[ELEM_EL], 179 `j > i` by DECIDE_TAC 180 THEN IMP_RES_TAC SEL_APPEND_SINGLETON 181 THEN PROVE_TAC[ELEM_EL]]]); 182 183val NEXT_RISE_REVIMP = 184 store_thm 185 ("NEXT_RISE_REVIMP", 186 ``i <= j /\ 187 (!k. i <= k /\ k < j ==> ~B_SEM (ELEM p k) c) /\ 188 B_SEM (ELEM p j) c 189 ==> 190 NEXT_RISE p c (i,j)``, 191 REWRITE_TAC [NEXT_RISE_def] 192 THEN ONCE_REWRITE_TAC[S_SEM_def] 193 THEN RW_TAC list_ss 194 [S_REPEAT_BOOL_TRUE,S_BOOL_TRUE,B_SEM] 195 THEN Cases_on `i=j` 196 THENL 197 [RW_TAC std_ss [] 198 THEN Q.EXISTS_TAC `[]` 199 THEN Q.EXISTS_TAC `SEL p (i,i)` 200 THEN RW_TAC list_ss [SEL_ELEM], 201 Q.EXISTS_TAC `SEL p (i,j-1)` 202 THEN Q.EXISTS_TAC `SEL p (j,j)` 203 THEN RW_TAC list_ss [] 204 THENL 205 [`i <= j-1 /\ j-1 < j /\ ((j-1)+1 = j)` by DECIDE_TAC 206 THEN PROVE_TAC[SEL_SPLIT], 207 POP_ASSUM 208 (ASSUME_TAC o 209 SIMP_RULE arith_ss 210 [SEL_def,SEL_REC_def,LENGTH_SEL_REC]) 211 THEN `i <= i+i' /\ i+i' < j` by DECIDE_TAC 212 THEN RES_TAC 213 THEN POP_ASSUM(K ALL_TAC) 214 THEN `(i+i') - i = i'` by DECIDE_TAC 215 THEN `i <= i+i' /\ i+i' <= j-1` by DECIDE_TAC 216 THEN IMP_RES_TAC(Q.INST_TYPE[`:'a`|->`:'a->bool`]EL_SEL) 217 THEN POP_ASSUM(K ALL_TAC) 218 THEN POP_ASSUM 219 (ASSUME_TAC o REWRITE_RULE[DECIDE``i + i' - i = i'``] o SPEC_ALL) 220 THEN RW_TAC std_ss [], 221 Q.EXISTS_TAC `ELEM p j` 222 THEN RW_TAC list_ss [SEL_ELEM]]]); 223 224val NEXT_RISE = 225 store_thm 226 ("NEXT_RISE", 227 ``i <= j 228 ==> 229 (NEXT_RISE p c (i,j) = 230 (!k. i <= k /\ k < j ==> ~B_SEM (ELEM p k) c) 231 /\ 232 B_SEM (ELEM p j) c)``, 233 PROVE_TAC[NEXT_RISE_IMP, NEXT_RISE_REVIMP]); 234 235val NEXT_RISE_TRUE = 236 store_thm 237 ("NEXT_RISE_TRUE", 238 ``i <= j ==> (NEXT_RISE p B_TRUE (i,j) = (i = j))``, 239 RW_TAC std_ss [NEXT_RISE,B_SEM] 240 THEN EQ_TAC 241 THENL 242 [RW_TAC arith_ss [] 243 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE arith_ss [] o SPEC ``i:num``) 244 THEN DECIDE_TAC, 245 intLib.COOPER_TAC]); 246 247val NEXT_RISE_TRUE_COR = 248 store_thm 249 ("NEXT_RISE_TRUE_COR", 250 ``i <= j /\ NEXT_RISE p B_TRUE (i,j) = (i = j)``, 251 EQ_TAC 252 THEN RW_TAC arith_ss [NEXT_RISE_TRUE] 253 THEN PROVE_TAC[NEXT_RISE_TRUE]); 254 255val NEXT_RISE_TRUE_EXISTS = 256 store_thm 257 ("NEXT_RISE_TRUE_EXISTS", 258 ``?k. NEXT_RISE p B_TRUE (j,k)``, 259 Q.EXISTS_TAC `j` 260 THEN RW_TAC std_ss 261 [SIMP_RULE arith_ss [] (Q.SPECL[`p`,`j`,`j`](GEN_ALL NEXT_RISE_TRUE))]); 262 263val NEXT_RISE_LEQ_TRUE_EXISTS = 264 store_thm 265 ("NEXT_RISE_LEQ_TRUE_EXISTS", 266 ``?k. j <= k /\ NEXT_RISE p B_TRUE (j,k)``, 267 Q.EXISTS_TAC `j` 268 THEN RW_TAC arith_ss 269 [SIMP_RULE arith_ss [] (Q.SPECL[`p`,`j`,`j`](GEN_ALL NEXT_RISE_TRUE))]); 270 271val NEXT_RISE_LESS = 272 store_thm 273 ("NEXT_RISE_LESS", 274 ``i <= j /\ NEXT_RISE p c (i,j) = 275 i <= j 276 /\ 277 (!k. i <= k /\ k < j ==> ~B_SEM (ELEM p k) c) 278 /\ 279 B_SEM (ELEM p j) c``, 280 PROVE_TAC[NEXT_RISE]); 281 282val NEXT_RISE_RESTN = 283 store_thm 284 ("NEXT_RISE_RESTN", 285 ``!i j p. NEXT_RISE (RESTN p i) c (j,k) = NEXT_RISE p c (i+j,i+k)``, 286 Induct 287 THEN RW_TAC arith_ss [NEXT_RISE, RESTN_def,ELEM_RESTN] 288 THEN RW_TAC arith_ss [NEXT_RISE_def] 289 THEN `SEL (REST p) (i + j,i + k) = SEL (RESTN p 1) (i + j,i + k)` 290 by PROVE_TAC[RESTN_def, DECIDE``SUC 0 = 1``] 291 THEN RW_TAC arith_ss [SEL_RESTN, DECIDE``i + (j + 1) = j + SUC i``]); 292 293val NEXT_TRUE_GE = 294 store_thm 295 ("NEXT_TRUE_GE", 296 ``x' >= x /\ NEXT_RISE p B_TRUE (x,x') = (x=x')``, 297 EQ_TAC 298 THEN RW_TAC arith_ss [NEXT_RISE_TRUE] 299 THEN IMP_RES_TAC(DECIDE``x':num >= x:num = x <= x'``) 300 THEN FULL_SIMP_TAC std_ss [NEXT_RISE_TRUE]); 301 302(****************************************************************************** 303* Structural induction rule for SEREs 304******************************************************************************) 305val sere_induct = save_thm 306 ("sere_induct", 307 Q.GEN 308 `P` 309 (MATCH_MP 310 (DECIDE ``(A ==> (B1 /\ B2 /\ B3)) ==> (A ==> B1)``) 311 (SIMP_RULE 312 std_ss 313 [pairTheory.FORALL_PROD, 314 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 315 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 316 (Q.SPECL 317 [`P`,`\ (r,b). P r`,`\ (r1,r2). P r1 /\ P r2`] 318 (TypeBase.induction_of ``:'a sere``))))); 319 320(****************************************************************************** 321* S_CLOCK_FREE r means r contains no clocking statements 322******************************************************************************) 323val S_CLOCK_FREE_def = 324 Define 325 `(S_CLOCK_FREE (S_BOOL b) = T) 326 /\ 327 (S_CLOCK_FREE (S_CAT(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 328 /\ 329 (S_CLOCK_FREE (S_FUSION(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 330 /\ 331 (S_CLOCK_FREE (S_OR(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 332 /\ 333 (S_CLOCK_FREE (S_AND(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 334 /\ 335 (S_CLOCK_FREE (S_REPEAT r) = S_CLOCK_FREE r) 336 /\ 337 (S_CLOCK_FREE (S_CLOCK v) = F)`; 338 339(****************************************************************************** 340* Proof that if S_CLOCK_FREE r then the unclocked semantics of 341* a SERE r is the same as the clocked semantics with clock equal to T 342******************************************************************************) 343 344val S_SEM_TRUE_LEMMA = 345 store_thm 346 ("S_SEM_TRUE_LEMMA", 347 ``!r w. 348 S_CLOCK_FREE r 349 ==> 350 (S_SEM w B_TRUE r = US_SEM w r)``, 351 INDUCT_THEN sere_induct ASSUME_TAC 352 THEN RW_TAC std_ss [S_SEM_def, US_SEM_def, S_CLOCK_FREE_def] 353 THEN RW_TAC (arith_ss ++ resq_SS) 354 [B_SEM,CONJ_ASSOC,LENGTH1, 355 Cooper.COOPER_PROVE``(n:num >= 1 /\ (!i:num. ~(i < n-1))) = (n = 1)``] 356 THEN EQ_TAC 357 THEN RW_TAC list_ss [LENGTH] 358 THEN FULL_SIMP_TAC list_ss [LENGTH]); 359 360val S_SEM_TRUE = 361 store_thm 362 ("S_SEM_TRUE", 363 ``S_CLOCK_FREE r ==> !w. S_SEM w B_TRUE r = US_SEM w r``, 364 Cases_on `r` 365 THEN RW_TAC std_ss [S_SEM_TRUE_LEMMA]); 366 367(****************************************************************************** 368* Structural induction rule for FL formulas 369******************************************************************************) 370val fl_induct = 371 save_thm 372 ("fl_induct", 373 Q.GEN 374 `P` 375 (MATCH_MP 376 (DECIDE ``(A ==> (B1 /\ B2 /\ B3)) ==> (A ==> B1)``) 377 (SIMP_RULE 378 std_ss 379 [pairTheory.FORALL_PROD, 380 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 381 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 382 (Q.SPECL 383 [`P`,`\ (r,f). P f`,`\ (f,b). P f`,`\ (f1,f2). P f1 /\ P f2`] 384 (TypeBase.induction_of ``:'a fl``))))); 385 386(****************************************************************************** 387* Negated clocking of f with T! equal to clocking with T of F_NOT f: 388* p |=T !f <==> ~(p |=T f) 389******************************************************************************) 390val F_SEM_TRUE_WEAK_NOT_EQ = 391 store_thm 392 ("F_SEM_TRUE_WEAK_NOT_EQ", 393 ``!f p. F_SEM p B_TRUE (F_NOT f) = ~(F_SEM p B_TRUE f)``, 394 INDUCT_THEN fl_induct ASSUME_TAC 395 THEN RW_TAC std_ss [F_SEM_def]); 396 397(****************************************************************************** 398* F_CLOCK_FREE f means f contains no clocking statements 399******************************************************************************) 400val F_CLOCK_FREE_def = 401 Define 402 `(F_CLOCK_FREE (F_BOOL b) = T) 403 /\ 404 (F_CLOCK_FREE (F_NOT f) = F_CLOCK_FREE f) 405 /\ 406 (F_CLOCK_FREE (F_AND(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2) 407 /\ 408 (F_CLOCK_FREE (F_NEXT f) = F_CLOCK_FREE f) 409 /\ 410 (F_CLOCK_FREE (F_UNTIL(f1,f2)) = F_CLOCK_FREE f1 /\ F_CLOCK_FREE f2) 411 /\ 412 (F_CLOCK_FREE (F_SUFFIX_IMP(r,f)) = F_CLOCK_FREE f /\ S_CLOCK_FREE r) 413 /\ 414 (F_CLOCK_FREE (F_STRONG_IMP(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 415 /\ 416 (F_CLOCK_FREE (F_WEAK_IMP(r1,r2)) = S_CLOCK_FREE r1 /\ S_CLOCK_FREE r2) 417 /\ 418 (F_CLOCK_FREE (F_ABORT (f,b)) = F_CLOCK_FREE f) 419 /\ 420 (F_CLOCK_FREE (F_STRONG_CLOCK v) = F)`; 421 422(****************************************************************************** 423* If F_CLOCK_FREE f then the unclocked semantics of an 424* FL formula f is the same as the clocked semantics with clock equal to T! 425* (i.e. strongly clocked) 426******************************************************************************) 427local 428val INIT_TAC = 429 RW_TAC (arith_ss ++ resq_SS) 430 [F_SEM_def,UF_SEM_def,F_CLOCK_FREE_def,RESTN_def,GSYM NEXT_RISE_def]; 431in 432val F_SEM_TRUE_LEMMA = 433 store_thm 434 ("F_SEM_TRUE_LEMMA", 435 ``!f p. F_CLOCK_FREE f ==> (F_SEM p B_TRUE f = UF_SEM p f)``, 436 INDUCT_THEN fl_induct ASSUME_TAC (* 10 subgoals *) 437 THENL 438 [(* 1. F_BOOL b *) 439 INIT_TAC, 440 (* 2. F_NOT b *) 441 INIT_TAC, 442 (* 3. F_AND (f1,f2) *) 443 INIT_TAC, 444 (* 4. F_NEXT f *) 445 Cases 446 THEN INIT_TAC 447 THEN EQ_TAC 448 THEN RW_TAC (arith_ss ++ resq_SS) [GT] 449 THEN IMP_RES_TAC NEXT_RISE_TRUE 450 THEN TRY DECIDE_TAC 451 THEN FULL_SIMP_TAC (std_ss++resq_SS) [num_to_def,xnum_to_def,NEXT_RISE_TRUE] 452 THEN TRY(PROVE_TAC[]) 453 THEN RW_TAC arith_ss [NEXT_RISE_TRUE] 454 THEN Q.EXISTS_TAC `1` 455 THEN RW_TAC arith_ss [NEXT_RISE_TRUE], 456 (* 5. F_UNTIL(f1,f2) f *) 457 Cases THEN INIT_TAC THEN RW_TAC std_ss [B_SEM], 458 (* 6. F_SUFFIX_IMP(s,f) *) 459 Cases_on `p` 460 THEN INIT_TAC 461 THEN RW_TAC (std_ss ++ resq_SS) [S_SEM_TRUE,B_SEM] 462 THEN EQ_TAC 463 THEN RW_TAC std_ss [] 464 THEN RES_TAC 465 THEN FULL_SIMP_TAC std_ss [NEXT_RISE_LESS,CONJ_ASSOC] 466 THEN IMP_RES_TAC NEXT_RISE 467 THEN FULL_SIMP_TAC std_ss [B_SEM] 468 THENL 469 [PROVE_TAC 470 [DECIDE ``m:num <= n:num /\ n <= m = (m = n)``, 471 Cooper.COOPER_PROVE ``(!k:num. k < j':num ==> ~(j:num <= k)) = j' <= j``], 472 Q.EXISTS_TAC `i` 473 THEN RW_TAC arith_ss [NEXT_RISE,B_SEM], 474 PROVE_TAC 475 [DECIDE ``m:num <= n:num /\ n <= m = (m = n)``, 476 Cooper.COOPER_PROVE ``(!k:num. k < j':num ==> ~(j:num <= k)) = j' <= j``], 477 Q.EXISTS_TAC `i` 478 THEN RW_TAC arith_ss [NEXT_RISE,B_SEM]], 479 (* 7. F_STRONG_IMP(s1,s2) *) 480 INIT_TAC 481 THEN RW_TAC std_ss [S_SEM_TRUE,NEXT_TRUE_GE,DECIDE``m:num <= n:num = n >= m``] 482 THEN EQ_TAC 483 THEN RW_TAC std_ss [] 484 THEN PROVE_TAC[], 485 (* 8. F_WEAK_IMP(s1,s2) *) 486 INIT_TAC 487 THEN RW_TAC std_ss [S_SEM_TRUE,NEXT_TRUE_GE,DECIDE``m:num <= n:num = n >= m``] 488 THEN EQ_TAC 489 THEN RW_TAC std_ss [], 490 (* 9. F_ABORT(f,b)) *) 491 INIT_TAC THEN RW_TAC std_ss [B_SEM,DECIDE``(A\/B=A\/C) = A \/ (B=C)``] 492 THEN Cases_on`UF_SEM p f \/ LENGTH p > 0 /\ B_SEM (ELEM p 0) p_2` 493 THEN RW_TAC std_ss [] 494 THEN RW_TAC std_ss [DISJ_ASSOC] 495 THEN FULL_SIMP_TAC std_ss [DE_MORGAN_THM] 496 THEN EQ_TAC 497 THEN RW_TAC arith_ss [ELEM_RESTN] 498 THENL 499 [Cases_on `p` 500 THEN FULL_SIMP_TAC arith_ss [xnum_to_def,LENGTH_def,GT_xnum_num_def], 501 Cases_on `p` 502 THEN FULL_SIMP_TAC arith_ss [xnum_to_def,LENGTH_def,GT_xnum_num_def], 503 Q.EXISTS_TAC `i` 504 THEN RW_TAC std_ss [] 505 THEN rename1 `UF_SEM (CAT (SEL p (0,i ��� 1),w'')) f` 506 THEN Q.EXISTS_TAC `w''` (* was: w' *) 507 THEN RW_TAC std_ss [] 508 THEN Cases_on `p` 509 THEN FULL_SIMP_TAC arith_ss 510 [xnum_to_def,LENGTH_def,GT_xnum_num_def,RESTN_FINITE,LENGTH_def, 511 FinitePSLPathTheory.LENGTH_RESTN,LENGTH_RESTN_INFINITE], 512 Q.EXISTS_TAC `j` 513 THEN RW_TAC std_ss [] 514 THEN PROVE_TAC []], 515 (* 10. F_STRONG_CLOCK(f,c) *) 516 INIT_TAC]); 517end; 518 519val F_SEM_TRUE = 520 store_thm 521 ("F_SEM_TRUE", 522 ``!f. F_CLOCK_FREE f ==> !w. F_SEM w B_TRUE f = UF_SEM w f``, 523 PROVE_TAC[F_SEM_TRUE_LEMMA]); 524 525(****************************************************************************** 526* Formula disjunction: f1 \/ f2 527******************************************************************************) 528val UF_SEM_F_OR = 529 store_thm 530 ("UF_SEM_F_OR", 531 ``UF_SEM p (F_OR(f1,f2)) = UF_SEM p f1 \/ UF_SEM p f2``, 532 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def,F_OR_def]); 533 534(****************************************************************************** 535* Formula implication: f1 --> f2 536******************************************************************************) 537val UF_SEM_F_IMPLIES = 538 store_thm 539 ("UF_SEM_F_IMPLIES", 540 ``UF_SEM p (F_IMPLIES (f1,f2)) = UF_SEM p f1 ==> UF_SEM p f2``, 541 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def,F_IMPLIES_def,UF_SEM_F_OR] 542 THEN PROVE_TAC[]); 543 544(****************************************************************************** 545* Eventually: F f 546******************************************************************************) 547val UF_SEM_F_F = 548 store_thm 549 ("UF_SEM_F_F", 550 ``UF_SEM p (F_F f) = ?i :: (0 to LENGTH p). UF_SEM (RESTN p i) f``, 551 RW_TAC (arith_ss ++ resq_SS) [UF_SEM_def,F_F_def,B_SEM] 552 THEN Cases_on `p` 553 THEN RW_TAC arith_ss 554 [xnum_to_def,LENGTH_def,GT_xnum_num_def,RESTN_FINITE,LENGTH_def, 555 FinitePSLPathTheory.LENGTH_RESTN,LENGTH_RESTN_INFINITE] 556 THEN EQ_TAC 557 THEN ZAP_TAC arith_ss [] 558 THEN Q.EXISTS_TAC `i` 559 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN]); 560 561(****************************************************************************** 562* Always: G f 563******************************************************************************) 564val UF_SEM_F_G = 565 store_thm 566 ("UF_SEM_F_G", 567 ``UF_SEM p (F_G f) = !i :: (0 to LENGTH p). UF_SEM (RESTN p i) f``, 568 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def,F_G_def,UF_SEM_F_F] 569 THEN PROVE_TAC[]); 570 571(****************************************************************************** 572* Weak until: [f1 W f2] 573******************************************************************************) 574val UF_SEM_F_W = 575 store_thm 576 ("UF_SEM_F_W", 577 ``UF_SEM p (F_W(f1,f2)) = UF_SEM p (F_UNTIL(f1,f2)) \/ UF_SEM p (F_G f1)``, 578 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def,F_W_def,UF_SEM_F_OR]); 579 580(****************************************************************************** 581* Strongly on first posedge. 582* Exists a posedge and true on it: [!c U (c /\ f)] 583******************************************************************************) 584val UF_SEM_F_U_CLOCK = 585 store_thm 586 ("UF_SEM_F_U_CLOCK", 587 ``UF_SEM p (F_U_CLOCK c f) = 588 ?i :: (0 to LENGTH p). NEXT_RISE p c (0,i) /\ UF_SEM (RESTN p i) f``, 589 RW_TAC (arith_ss ++ resq_SS) 590 [F_U_CLOCK_def,ELEM_RESTN,UF_SEM_def,B_SEM,NEXT_RISE] 591 THEN EQ_TAC 592 THEN RW_TAC std_ss [] 593 THENL 594 [Q.EXISTS_TAC `k` 595 THEN RW_TAC std_ss [], 596 Q.EXISTS_TAC `i` 597 THEN RW_TAC std_ss [] 598 THEN Cases_on `p` 599 THEN FULL_SIMP_TAC arith_ss 600 [xnum_to_def,LENGTH_def,GT_xnum_num_def,RESTN_FINITE,LENGTH_def, 601 FinitePSLPathTheory.LENGTH_RESTN,LENGTH_RESTN_INFINITE]]); 602 603(****************************************************************************** 604* Weakly on first posedge. 605* On first posedge, if there is a posedge: [!c U (c /\ f)] 606******************************************************************************) 607val UF_SEM_F_W_CLOCK = 608 store_thm 609 ("UF_SEM_F_W_CLOCK", 610 ``UF_SEM p (F_W_CLOCK c f) = 611 UF_SEM p (F_U_CLOCK c f) 612 \/ 613 !i :: (0 to LENGTH p).~UF_SEM (RESTN p i) (F_BOOL c)``, 614 RW_TAC (std_ss ++ resq_SS) 615 [F_U_CLOCK_def,F_W_CLOCK_def,UF_SEM_F_W,UF_SEM_F_G,B_SEM,UF_SEM_def] 616 THEN EQ_TAC 617 THEN RW_TAC std_ss [] 618 THEN Cases_on `p` 619 THEN FULL_SIMP_TAC arith_ss 620 [xnum_to_def,LENGTH_def,GT_xnum_num_def,RESTN_FINITE,LENGTH_def, 621 FinitePSLPathTheory.LENGTH_RESTN,LENGTH_RESTN_INFINITE] 622 THENL 623 [Cases_on `!i. i < LENGTH l ==> ~B_SEM (ELEM (FINITE (RESTN l i)) 0) c` 624 THEN RW_TAC std_ss [] 625 THEN FULL_SIMP_TAC std_ss [NOT_FORALL_THM] 626 THEN Q.EXISTS_TAC `k` 627 THEN RW_TAC std_ss [], 628 Cases_on `!i. ~B_SEM (ELEM (RESTN (INFINITE f') i) 0) c` 629 THEN RW_TAC std_ss [] 630 THEN FULL_SIMP_TAC std_ss [NOT_FORALL_THM] 631 THEN Q.EXISTS_TAC `k` 632 THEN RW_TAC std_ss [], 633 Cases_on `!i. i < LENGTH l ==> ~B_SEM (ELEM (FINITE (RESTN l i)) 0) c` 634 THEN RW_TAC std_ss [] 635 THEN FULL_SIMP_TAC std_ss [NOT_FORALL_THM] 636 THEN Q.EXISTS_TAC `k` 637 THEN RW_TAC std_ss [], 638 Cases_on `!i. ~B_SEM (ELEM (RESTN (INFINITE f') i) 0) c` 639 THEN RW_TAC std_ss [] 640 THEN FULL_SIMP_TAC std_ss [NOT_FORALL_THM] 641 THEN Q.EXISTS_TAC `k` 642 THEN RW_TAC std_ss []]); 643 644(****************************************************************************** 645* S_CLOCK_COMP c r contains no clocked SEREs 646******************************************************************************) 647val S_CLOCK_COMP_CLOCK_FREE = 648 store_thm 649 ("S_CLOCK_COMP_CLOCK_FREE", 650 ``!r c. S_CLOCK_FREE(S_CLOCK_COMP c r)``, 651 INDUCT_THEN sere_induct ASSUME_TAC 652 THEN RW_TAC std_ss [S_CLOCK_FREE_def,S_CLOCK_COMP_def]); 653 654(****************************************************************************** 655* F_CLOCK_COMP c f contains no clocked formulas 656******************************************************************************) 657val F_CLOCK_COMP_CLOCK_FREE_LEMMA = 658 store_thm 659 ("F_CLOCK_COMP_CLOCK_FREE_LEMMA", 660 ``!f c. F_CLOCK_FREE(F_CLOCK_COMP c f)``, 661 INDUCT_THEN fl_induct ASSUME_TAC 662 THEN RW_TAC std_ss 663 [F_CLOCK_FREE_def,F_CLOCK_COMP_def,F_U_CLOCK_def,F_IMPLIES_def, 664 F_OR_def,S_CLOCK_COMP_CLOCK_FREE]) 665 666val F_CLOCK_COMP_CLOCK_FREE = 667 store_thm 668 ("F_CLOCK_COMP_CLOCK_FREE", 669 ``!c f. F_CLOCK_FREE(F_CLOCK_COMP c f)``, 670 RW_TAC std_ss [F_CLOCK_COMP_CLOCK_FREE_LEMMA]); 671 672(****************************************************************************** 673* w |=c r <==> w |= (S_CLOCK_COMP c r) 674******************************************************************************) 675local open FinitePSLPathTheory 676 677val INIT_TAC0 = 678 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def]; 679 680val INIT_TAC1 = 681 INIT_TAC0 682 THEN RW_TAC list_ss [EVERY_EL] 683 THEN EQ_TAC 684 THEN RW_TAC list_ss [LENGTH_APPEND,ELEM_EL,LENGTH1]; 685 686val INIT_TAC2 = 687 `!n:num. n < LENGTH wlist ==> (?x. EL n wlist = [x])` by PROVE_TAC[] 688 THEN IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a->bool``]EVERY_EL_SINGLETON_LENGTH) 689 THEN IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a->bool``]EVERY_EL_SINGLETON) 690 THEN FULL_SIMP_TAC list_ss [LENGTH_APPEND] 691 THEN RW_TAC list_ss [EL_MAP,EL_APPEND1,EL_APPEND2]; 692 693in 694 695val S_CLOCK_COMP_ELIM = 696 store_thm 697 ("S_CLOCK_COMP_ELIM", 698 ``!r w c. S_SEM w c r = US_SEM w (S_CLOCK_COMP c r)``, 699 INDUCT_THEN sere_induct ASSUME_TAC 700 THENL 701 [(* S_BOOL b *) 702 INIT_TAC1 THEN TRY INIT_TAC2 703 THEN Q.EXISTS_TAC `BUTLAST w` 704 THEN Q.EXISTS_TAC `[LAST w]` 705 THEN RW_TAC list_ss [] 706 THEN RW_TAC list_ss [APPEND_BUTLAST_LAST,LENGTH_NIL_LEMMA] 707 THENL 708 [Q.EXISTS_TAC `MAP(\l.[l])(BUTLAST w)` 709 THEN RW_TAC list_ss [CONCAT_MAP_SINGLETON,EL_MAP] 710 THEN IMP_RES_TAC LENGTH_NIL_LEMMA 711 THEN IMP_RES_TAC LENGTH_BUTLAST 712 THEN `n:num < LENGTH w - 1` by DECIDE_TAC 713 THEN PROVE_TAC[EL_BUTLAST], 714 IMP_RES_TAC EL_PRE_LENGTH 715 THEN POP_ASSUM(fn th => RW_TAC list_ss [GSYM th])], 716 (* S_CAT(r,r') *) 717 INIT_TAC0, 718 (* S_FUSION (r,r') *) 719 INIT_TAC0, 720 (* S_OR (r,r') *) 721 INIT_TAC0, 722 (* S_AND (r,r') *) 723 INIT_TAC0, 724 (* S_REPEAT r *) 725 INIT_TAC0, 726 (* S_CLOCK (r,p_2) *) 727 INIT_TAC0 728 THEN EQ_TAC 729 THEN RW_TAC list_ss 730 [LENGTH_APPEND,LENGTH_NIL,ELEM_EL,EVERY_EL,LENGTH1, 731 APPEND_SINGLETON_EQ] 732 THEN FULL_SIMP_TAC list_ss [] 733 THENL 734 [Q.EXISTS_TAC `CONCAT wlist` 735 THEN Q.EXISTS_TAC `x :: RESTN w (i+1)` 736 THEN RW_TAC list_ss [] 737 THENL 738 [ONCE_REWRITE_TAC [APPEND_CONS] 739 THEN ASSUM_LIST(fn thl => REWRITE_TAC[SYM(el 4 thl)]) 740 THEN Cases_on `i:num = LENGTH w - 1` 741 THENL 742 [RW_TAC arith_ss [] 743 THEN `0 < LENGTH w` by DECIDE_TAC 744 THEN ASSUM_LIST(fn thl => SIMP_TAC std_ss (mapfilter SYM thl)) 745 THEN IMP_RES_TAC SEL_RESTN_EQ0 746 THEN POP_ASSUM(fn th => REWRITE_TAC[th,RESTN_LENGTH,APPEND_NIL]), 747 `i:num < LENGTH w - 1` by DECIDE_TAC 748 THEN IMP_RES_TAC(DECIDE``i:num < m:num-1 ==> i+1 < m``) 749 THEN IMP_RES_TAC SEL_RESTN_EQ 750 THEN ASSUM_LIST(fn thl => SIMP_TAC std_ss (mapfilter SYM thl)) 751 THEN POP_ASSUM(ASSUME_TAC o SYM) 752 THEN IMP_RES_TAC 753 (SIMP_RULE 754 arith_ss 755 [] 756 (GSYM(Q.SPECL[`w`,`i`,`0`,`list$LENGTH w - 1`]FinitePSLPathTheory.SEL_SPLIT))) 757 THEN POP_ASSUM(fn th => REWRITE_TAC[th]) 758 THEN PROVE_TAC[DECIDE``i:num < n:num-1 ==> 0 < n``,SEL_RESTN_EQ0]], 759 PROVE_TAC[], 760 `!n. n < LENGTH wlist ==> (?x. EL n wlist = [x])` by PROVE_TAC[] 761 THEN IMP_RES_TAC(INST_TYPE[``:'a``|->``:'a->bool``]EVERY_EL_SINGLETON_LENGTH) 762 THEN PROVE_TAC[RESTN_EL,LAST_SINGLETON,EL_LAST_SEL]], 763 Q.EXISTS_TAC `LENGTH(CONCAT wlist)` 764 THEN RW_TAC list_ss [RESTN_APPEND] 765 THEN Q.EXISTS_TAC `CONCAT wlist` 766 THEN Q.EXISTS_TAC `[l]` 767 THEN RW_TAC list_ss [] 768 THENL 769 [ONCE_REWRITE_TAC [APPEND_CONS] 770 THEN Cases_on `CONCAT wlist = []` 771 THEN RW_TAC list_ss [SEL_ELEM,ELEM_EL] 772 THEN POP_ASSUM(ASSUME_TAC o SIMP_RULE std_ss [GSYM LENGTH_NIL]) 773 THEN `0 < LENGTH(CONCAT wlist)` by DECIDE_TAC 774 THEN `1 <= LENGTH([l] <> w2')` by RW_TAC list_ss [] 775 THEN RW_TAC std_ss [SEL_APPEND_COR,GSYM APPEND_ASSOC,SEL_RESTN_EQ0] 776 THEN RW_TAC list_ss [], 777 PROVE_TAC[]]]]); 778 779end; 780 781(****************************************************************************** 782* Make theorems that apply to both finite and infinite paths 783* (maybe not needed) 784******************************************************************************) 785val HEAD_def = 786 LIST_CONJ[FinitePSLPathTheory.HEAD_def,PSLPathTheory.HEAD_def]; 787 788val REST_def = 789 LIST_CONJ[FinitePSLPathTheory.REST_def,PSLPathTheory.REST_def]; 790 791val RESTN_def = 792 LIST_CONJ[FinitePSLPathTheory.RESTN_def,PSLPathTheory.RESTN_def]; 793 794val ELEM_def = 795 LIST_CONJ[FinitePSLPathTheory.ELEM_def,PSLPathTheory.ELEM_def]; 796 797val LENGTH_REST = 798 LIST_CONJ[FinitePSLPathTheory.LENGTH_REST,PSLPathTheory.LENGTH_REST]; 799 800val LENGTH_RESTN = 801 LIST_CONJ[FinitePSLPathTheory.LENGTH_RESTN,PSLPathTheory.LENGTH_RESTN]; 802 803(****************************************************************************** 804* F_INIT_CLOCK_COMP_CORRECT f = (p |=T f <==> p |= (F_INIT_CLOCK_COMP T f)) 805******************************************************************************) 806val F_INIT_CLOCK_COMP_CORRECT_def = 807 Define 808 `F_INIT_CLOCK_COMP_CORRECT f = 809 !w c. (F_SEM w c f = UF_SEM w (F_INIT_CLOCK_COMP c f))`; 810 811val F_BOOL_INIT_CLOCK_COMP_ELIM = 812 store_thm 813 ("F_BOOL_INIT_CLOCK_COMP_ELIM", 814 ``!b. F_INIT_CLOCK_COMP_CORRECT (F_BOOL b)``, 815 RW_TAC (std_ss ++ resq_SS) 816 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def]); 817 818val F_NOT_INIT_CLOCK_COMP_ELIM = 819 store_thm 820 ("F_NOT_INIT_CLOCK_COMP_ELIM", 821 ``!f. F_INIT_CLOCK_COMP_CORRECT f ==> F_INIT_CLOCK_COMP_CORRECT (F_NOT f)``, 822 RW_TAC (std_ss ++ resq_SS) 823 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def]); 824 825val F_AND_INIT_CLOCK_COMP_ELIM = 826 store_thm 827 ("F_AND_INIT_CLOCK_COMP_ELIM", 828 ``!f1 f2. F_INIT_CLOCK_COMP_CORRECT f1 /\ F_INIT_CLOCK_COMP_CORRECT f2 829 ==> F_INIT_CLOCK_COMP_CORRECT (F_AND(f1,f2))``, 830 RW_TAC (std_ss ++ resq_SS) 831 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def]); 832 833val F_NEXT_INIT_CLOCK_COMP_ELIM = 834 store_thm 835 ("F_NEXT_INIT_CLOCK_COMP_ELIM", 836 ``!f. F_INIT_CLOCK_COMP_CORRECT f ==> F_INIT_CLOCK_COMP_CORRECT (F_NEXT f)``, 837 RW_TAC (std_ss ++ resq_SS) 838 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def] 839 THEN Cases_on `w` 840 THEN ONCE_REWRITE_TAC[ONE] 841 THENL 842 [RW_TAC (arith_ss ++ resq_SS) 843 [UF_SEM_F_U_CLOCK,GSYM NEXT_RISE_def,NEXT_RISE,LENGTH_def, 844 RESTN_def,xnum_to_def,GT_xnum_num_def,RESTN_FINITE] 845 THEN EQ_TAC 846 THEN RW_TAC std_ss [] 847 THENL 848 [DECIDE_TAC, 849 Q.EXISTS_TAC `i-1` 850 THEN IMP_RES_TAC NEXT_RISE 851 THEN RW_TAC arith_ss 852 [REST_def,LENGTH_def,xnum_to_def,RESTN_def,RESTN_FINITE,LENGTH_TL, 853 RESTN_TL,ELEM_FINITE_TL] 854 THEN `0 < i /\ k+1 < i /\ 1 <= k+1 /\ 0 < LENGTH l` by DECIDE_TAC 855 THEN RES_TAC 856 THEN RW_TAC arith_ss [ELEM_FINITE_TL_COR], 857 Q.EXISTS_TAC `i+1` 858 THEN ZAP_TAC arith_ss [RESTN_def,ADD1] 859 THENL 860 [`0 < LENGTH l` by DECIDE_TAC 861 THEN IMP_RES_TAC LENGTH_REST 862 THEN DECIDE_TAC, 863 RW_TAC arith_ss [NEXT_RISE] 864 THENL 865 [`k-1 < i /\ 0 < k /\ 0 < LENGTH l` by DECIDE_TAC 866 THEN PROVE_TAC[ELEM_FINITE_TL,REST_def], 867 `0 < LENGTH l` by DECIDE_TAC 868 THEN PROVE_TAC[ELEM_FINITE_TL_COR,REST_def]]]], 869 RW_TAC (arith_ss ++ resq_SS) 870 [LENGTH_def,xnum_to_def,GT_xnum_num_def, 871 UF_SEM_F_U_CLOCK,GSYM NEXT_RISE_def,NEXT_RISE, 872 RESTN_def,xnum_to_def,NEXT_RISE_LESS,REST_def,CONJ_ASSOC] 873 THEN RW_TAC std_ss [GSYM REST_def] 874 THEN EQ_TAC 875 THEN RW_TAC std_ss [] 876 THENL 877 [Q.EXISTS_TAC `i-1` 878 THEN RW_TAC arith_ss [ELEM_REST_INFINITE,RESTN_REST_INFINITE] 879 THEN `1 <= k+1 /\ k+1 < i` by DECIDE_TAC 880 THEN RES_TAC 881 THEN RW_TAC arith_ss [ELEM_REST_INFINITE_COR], 882 Q.EXISTS_TAC `i+1` 883 THEN RW_TAC arith_ss [RESTN_def,ADD1] 884 THENL 885 [`0 < k /\ k-1 < i` by DECIDE_TAC 886 THEN PROVE_TAC[ELEM_REST_INFINITE], 887 PROVE_TAC[ELEM_REST_INFINITE_COR], 888 PROVE_TAC[RESTN_REST_INFINITE_COR]]]]); 889 890val F_UNTIL_INIT_CLOCK_COMP_ELIM = 891 store_thm 892 ("F_UNTIL_INIT_CLOCK_COMP_ELIM", 893 ``!f1 f2. 894 F_INIT_CLOCK_COMP_CORRECT f1 /\ F_INIT_CLOCK_COMP_CORRECT f2 ==> 895 F_INIT_CLOCK_COMP_CORRECT (F_UNTIL(f1, f2))``, 896 RW_TAC (std_ss ++ resq_SS) 897 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def] 898 THEN Cases_on `w` 899 THEN RW_TAC (arith_ss ++ resq_SS) 900 [LENGTH_def,num_to_def,xnum_to_def,UF_SEM_def,UF_SEM_F_IMPLIES,ELEM_RESTN] 901 THEN PROVE_TAC[]); 902 903val F_SUFFIX_IMP_INIT_CLOCK_COMP_ELIM = 904 store_thm 905 ("F_SUFFIX_IMP_INIT_CLOCK_COMP_ELIM", 906 ``!r f. F_INIT_CLOCK_COMP_CORRECT f ==> F_INIT_CLOCK_COMP_CORRECT (F_SUFFIX_IMP(r,f))``, 907 RW_TAC (std_ss ++ resq_SS) 908 [F_INIT_CLOCK_COMP_CORRECT_def,F_INIT_CLOCK_COMP_def,S_CLOCK_COMP_ELIM, 909 F_SEM_def,NEXT_RISE,GSYM NEXT_RISE_def,UF_SEM_def,UF_SEM_F_U_CLOCK] 910 THEN Cases_on `w` 911 THEN RW_TAC (arith_ss ++ resq_SS) 912 [LENGTH_def,num_to_def,xnum_to_def,UF_SEM_def,UF_SEM_F_IMPLIES,LENGTH_RESTN, 913 LENGTH_RESTN_INFINITE,RESTN_FINITE,ELEM_RESTN,B_SEM,RESTN_RESTN] 914 THEN EQ_TAC 915 THEN RW_TAC std_ss [] 916 THEN RES_TAC 917 THEN IMP_RES_TAC NEXT_RISE 918 THENL 919 [Q.EXISTS_TAC `j'-j` 920 THEN RW_TAC arith_ss [] 921 THEN `0 <= j' - j` by DECIDE_TAC 922 THEN RW_TAC arith_ss [NEXT_RISE,ELEM_RESTN,GSYM RESTN_FINITE], 923 Q.EXISTS_TAC `i'+i` 924 THEN RW_TAC arith_ss [NEXT_RISE] 925 THEN `0 <= i'` by DECIDE_TAC 926 THEN POP_ASSUM 927 (fn th => FULL_SIMP_TAC std_ss 928 [ELEM_RESTN,GSYM RESTN_FINITE,MATCH_MP NEXT_RISE th]) 929 THEN `0 <= k-i /\ k-i < i' /\ (i+(k-i) = k)` by DECIDE_TAC 930 THEN PROVE_TAC[] (* PROVE_TAC[ADD_SYM] *), 931 Q.EXISTS_TAC `j'-j` 932 THEN RW_TAC arith_ss [] 933 THEN `0 <= j' - j` by DECIDE_TAC 934 THEN RW_TAC arith_ss [NEXT_RISE,ELEM_RESTN], 935 Q.EXISTS_TAC `i'+i` 936 THEN RW_TAC arith_ss [NEXT_RISE] 937 THEN `0 <= i'` by DECIDE_TAC 938 THEN POP_ASSUM 939 (fn th => FULL_SIMP_TAC std_ss 940 [ELEM_RESTN,GSYM RESTN_FINITE,MATCH_MP NEXT_RISE th]) 941 THEN `0 <= k-i /\ k-i < i' /\ (i+(k-i) = k)` by DECIDE_TAC 942 THEN PROVE_TAC[]]); 943 944val F_STRONG_IMP_INIT_CLOCK_COMP_ELIM = 945 store_thm 946 ("F_STRONG_IMP_INIT_CLOCK_COMP_ELIM", 947 ``!r1 r2. F_INIT_CLOCK_COMP_CORRECT(F_STRONG_IMP(r1,r2))``, 948 RW_TAC (std_ss ++ resq_SS) 949 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def,S_CLOCK_COMP_ELIM] 950 THEN Cases_on `w` 951 THEN RW_TAC (arith_ss ++ resq_SS) 952 [LENGTH_def,num_to_def,xnum_to_def,UF_SEM_def,UF_SEM_F_IMPLIES,ELEM_RESTN]); 953 954val F_WEAK_IMP_INIT_CLOCK_COMP_ELIM = 955 store_thm 956 ("F_WEAK_IMP_INIT_CLOCK_COMP_ELIM", 957 ``!r1 r2. F_INIT_CLOCK_COMP_CORRECT(F_WEAK_IMP(r1,r2))``, 958 RW_TAC (std_ss ++ resq_SS) 959 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def,S_CLOCK_COMP_ELIM] 960 THEN Cases_on `w` 961 THEN RW_TAC (arith_ss ++ resq_SS) 962 [LENGTH_def,num_to_def,xnum_to_def,UF_SEM_def,UF_SEM_F_IMPLIES,ELEM_RESTN]); 963 964val F_ABORT_INIT_CLOCK_COMP_ELIM = 965 store_thm 966 ("F_ABORT_INIT_CLOCK_COMP_ELIM", 967 ``!b f. F_INIT_CLOCK_COMP_CORRECT f ==> F_INIT_CLOCK_COMP_CORRECT (F_ABORT(f,b))``, 968 RW_TAC (std_ss ++ resq_SS) 969 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def] 970 THEN Cases_on `w` 971 THEN RW_TAC (arith_ss ++ resq_SS) 972 [LENGTH_def,num_to_def,xnum_to_def,UF_SEM_def, 973 UF_SEM_F_OR,UF_SEM_F_IMPLIES,ELEM_RESTN,B_SEM_def] 974 THEN PROVE_TAC[]); 975 976val F_STRONG_CLOCK_INIT_CLOCK_COMP_ELIM = 977 store_thm 978 ("F_STRONG_CLOCK_INIT_CLOCK_COMP_ELIM", 979 ``!f. F_INIT_CLOCK_COMP_CORRECT f ==> 980 !c1. F_INIT_CLOCK_COMP_CORRECT (F_STRONG_CLOCK(f,c1))``, 981 RW_TAC (std_ss ++ resq_SS) 982 [F_INIT_CLOCK_COMP_CORRECT_def,F_SEM,UF_SEM_def,F_INIT_CLOCK_COMP_def] 983 THEN Cases_on `w` 984 THEN RW_TAC (arith_ss ++ resq_SS) 985 [LENGTH_def,num_to_def,xnum_to_def,UF_SEM_def,UF_SEM_F_IMPLIES,ELEM_RESTN, 986 UF_SEM_F_U_CLOCK,GSYM NEXT_RISE_def,NEXT_RISE]); 987 988val F_INIT_CLOCK_COMP_ELIM = 989 store_thm 990 ("F_INIT_CLOCK_COMP_ELIM", 991 ``!f. F_INIT_CLOCK_COMP_CORRECT f``, 992 INDUCT_THEN fl_induct ASSUME_TAC 993 THEN RW_TAC std_ss 994 [F_BOOL_INIT_CLOCK_COMP_ELIM, 995 F_NOT_INIT_CLOCK_COMP_ELIM, 996 F_AND_INIT_CLOCK_COMP_ELIM, 997 F_SUFFIX_IMP_INIT_CLOCK_COMP_ELIM, 998 F_ABORT_INIT_CLOCK_COMP_ELIM, 999 F_WEAK_IMP_INIT_CLOCK_COMP_ELIM, 1000 F_STRONG_IMP_INIT_CLOCK_COMP_ELIM, 1001 F_STRONG_CLOCK_INIT_CLOCK_COMP_ELIM, 1002 F_NEXT_INIT_CLOCK_COMP_ELIM, 1003 F_UNTIL_INIT_CLOCK_COMP_ELIM]); 1004 1005(****************************************************************************** 1006* Proof that if the clock is initially true, then the two rewrites for 1007* abort (defined in F_CLOCK_COMP and F_INIT_CLOCK_COMP) are equivalent. 1008******************************************************************************) 1009local 1010val INIT_TAC = 1011 RW_TAC std_ss [F_CLOCK_COMP_def,F_INIT_CLOCK_COMP_def,UF_SEM_def,B_SEM]; 1012in 1013val INIT_CLOCK_COMP_EQUIV = 1014 store_thm 1015 ("INIT_CLOCK_COMP_EQUIV", 1016 ``!f w c. 1017 B_SEM (ELEM w 0) c 1018 ==> 1019 (UF_SEM w (F_CLOCK_COMP c f) = UF_SEM w (F_INIT_CLOCK_COMP c f))``, 1020 INDUCT_THEN fl_induct ASSUME_TAC 1021 THENL 1022 [(* F_BOOL b *) 1023 INIT_TAC, 1024 (* F_NOT b *) 1025 INIT_TAC, 1026 (* F_AND (f1,f2) *) 1027 INIT_TAC, 1028 (* F_NEXT f *) 1029 INIT_TAC 1030 THEN RW_TAC (arith_ss++resq_SS) [UF_SEM_F_U_CLOCK,RESTN_RESTN] 1031 THEN Cases_on `w` 1032 THEN RW_TAC arith_ss 1033 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE, 1034 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1035 THEN EQ_TAC 1036 THEN RW_TAC std_ss [] 1037 THEN Q.EXISTS_TAC `i` 1038 THEN PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`j`,`0`]ELEM_RESTN)], 1039 (* F_UNTIL(f1,f2) f *) 1040 INIT_TAC 1041 THEN RW_TAC (arith_ss++resq_SS) [ELEM_RESTN,UF_SEM_F_IMPLIES,UF_SEM_def] 1042 THEN Cases_on `w` 1043 THEN RW_TAC arith_ss 1044 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE, 1045 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1046 THEN EQ_TAC 1047 THEN RW_TAC std_ss [] 1048 THEN Q.EXISTS_TAC `k` 1049 THEN PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`j`,`0`]ELEM_RESTN)], 1050 (* F_SUFFIX_IMP(s,f) *) 1051 INIT_TAC 1052 THEN RW_TAC (arith_ss++resq_SS) [ELEM_RESTN,UF_SEM_F_IMPLIES,UF_SEM_def] 1053 THEN Cases_on `w` 1054 THEN RW_TAC (arith_ss ++resq_SS) 1055 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE,UF_SEM_F_U_CLOCK,LENGTH_RESTN, 1056 RESTN_FINITE,num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN,RESTN_RESTN] 1057 THEN EQ_TAC 1058 THEN RW_TAC std_ss [] 1059 THEN RES_TAC 1060 THEN Q.EXISTS_TAC `i` 1061 THEN RW_TAC arith_ss [] 1062 THEN FULL_SIMP_TAC std_ss [GSYM(SIMP_RULE arith_ss [] (Q.SPECL[`i+j`,`0`]ELEM_RESTN))] 1063 THEN PROVE_TAC[RESTN_FINITE], 1064 (* F_STRONG_IMP(s1,s2) *) 1065 INIT_TAC, 1066 (* F_WEAK_IMP(s1,s2) *) 1067 INIT_TAC, 1068 (* F_ABORT(f,b)) *) 1069 INIT_TAC 1070 THEN RW_TAC (arith_ss++resq_SS) [ELEM_RESTN,UF_SEM_F_OR,UF_SEM_def] 1071 THEN Cases_on `w` 1072 THEN RW_TAC arith_ss 1073 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE,B_SEM, 1074 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1075 THEN EQ_TAC 1076 THEN RW_TAC std_ss [] 1077 THEN RW_TAC std_ss [] 1078 THENL 1079 [ASSUM_LIST 1080 (fn thl => 1081 ASSUME_TAC 1082 (GEN_ALL 1083 (SIMP_RULE std_ss [ELEM_CAT_SEL] 1084 (Q.SPECL[`(CAT (SEL w (0,j - 1),w'))`,`c`] (el 8 thl))))) 1085 THEN PROVE_TAC[], 1086 ASSUM_LIST 1087 (fn thl => 1088 ASSUME_TAC 1089 (GEN_ALL 1090 (SIMP_RULE std_ss [ELEM_CAT_SEL] 1091 (Q.SPECL[`(CAT (SEL w (0,j - 1),w'))`,`c`] (el 8 thl))))) 1092 THEN PROVE_TAC[], 1093 ASSUM_LIST 1094 (fn thl => 1095 ASSUME_TAC 1096 (GEN_ALL 1097 (SIMP_RULE std_ss [ELEM_CAT_SEL] 1098 (Q.SPECL[`(CAT (SEL w (0,j - 1),w'))`,`c`] (el 6 thl))))) 1099 THEN PROVE_TAC[], 1100 ASSUM_LIST 1101 (fn thl => 1102 ASSUME_TAC 1103 (GEN_ALL 1104 (SIMP_RULE std_ss [ELEM_CAT_SEL] 1105 (Q.SPECL[`(CAT (SEL w (0,j - 1),w'))`,`c`] (el 6 thl))))) 1106 THEN PROVE_TAC[]], 1107 (* F_STRONG_CLOCK(f,c) *) 1108 INIT_TAC 1109 THEN RW_TAC (arith_ss++resq_SS) [UF_SEM_F_U_CLOCK,RESTN_RESTN] 1110 THEN Cases_on `w` 1111 THEN RW_TAC arith_ss 1112 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE, 1113 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1114 THEN EQ_TAC 1115 THEN RW_TAC std_ss [] 1116 THEN Q.EXISTS_TAC `i` 1117 THEN RW_TAC std_ss [] 1118 THEN PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`j`,`0`]ELEM_RESTN)]]); 1119end; 1120 1121val F_CLOCK_COMP_CORRECT = 1122 store_thm 1123 ("F_CLOCK_COMP_CORRECT", 1124 `` !f w c. 1125 B_SEM (ELEM w 0) c ==> 1126 (F_SEM w c f = UF_SEM w (F_CLOCK_COMP c f))``, 1127 PROVE_TAC[F_INIT_CLOCK_COMP_ELIM,F_INIT_CLOCK_COMP_CORRECT_def,INIT_CLOCK_COMP_EQUIV]); 1128 1129(****************************************************************************** 1130* w |=T f <==> w |= T^{T}(f) 1131******************************************************************************) 1132val F_TRUE_COMP_CORRECT_LEMMA = 1133 save_thm 1134 ("F_TRUE_COMP_CORRECT_LEMMA", 1135 SIMP_CONV std_ss [B_SEM] ``B_SEM (ELEM w 0) B_TRUE``); 1136 1137val F_TRUE_CLOCK_COMP_ELIM = 1138 store_thm 1139 ("F_TRUE_CLOCK_COMP_ELIM", 1140 ``F_SEM w B_TRUE f = UF_SEM w (F_CLOCK_COMP B_TRUE f)``, 1141 PROVE_TAC 1142 [F_CLOCK_COMP_CORRECT,F_TRUE_COMP_CORRECT_LEMMA]); 1143 1144local 1145val INIT_TAC = 1146 RW_TAC (arith_ss ++ resq_SS) 1147 [F_SEM_def,UF_SEM_def,OLD_F_SEM_def,OLD_UF_SEM_def, 1148 F_CLOCK_FREE_def,RESTN_def,GSYM NEXT_RISE_def,xnum_to_def,num_to_def]; 1149 1150fun FIN_TAC v = 1151 `LENGTH(RESTN l ^v) = LENGTH l - ^v` by PROVE_TAC[LENGTH_RESTN] 1152 THEN `0 < LENGTH(RESTN l ^v)` by DECIDE_TAC 1153 THEN `0 < LENGTH(FINITE(RESTN l ^v))` by PROVE_TAC[LENGTH_def,PSLPathTheory.LS,xnum_11] 1154 THEN PROVE_TAC[]; 1155 1156fun INF_TAC f v = 1157 `0 < LENGTH(RESTN(INFINITE ^f) ^v)` 1158 by PROVE_TAC[LENGTH_RESTN_INFINITE,LENGTH_def,PSLPathTheory.LS,xnum_11] 1159 THEN PROVE_TAC[]; 1160in 1161val OLD_UF_SEM_UF_SEM = 1162 store_thm 1163 ("OLD_UF_SEM_UF_SEM", 1164 ``!f w. LENGTH w > 0 /\ F_CLOCK_FREE f ==> (OLD_UF_SEM w f = UF_SEM w f)``, 1165 INDUCT_THEN fl_induct ASSUME_TAC (* 10 subgoals *) 1166 THENL 1167 [(* F_BOOL b *) 1168 INIT_TAC, 1169 (* F_NOT b *) 1170 INIT_TAC, 1171 (* F_AND (f1,f2) *) 1172 INIT_TAC, 1173 (* F_NEXT f *) 1174 INIT_TAC 1175 THEN EQ_TAC 1176 THEN RW_TAC std_ss [] 1177 THEN FULL_SIMP_TAC arith_ss [GT_LS] 1178 THEN IMP_RES_TAC LENGTH_RESTN_THM 1179 THEN Cases_on `w` 1180 THEN FULL_SIMP_TAC arith_ss [LENGTH_def,GT,LS,PSLPathTheory.SUB,RESTN_FINITE,xnum_11] 1181 THENL 1182 [FIN_TAC ``1``, 1183 INF_TAC ``f' :num -> 'a -> bool`` ``1``], 1184 (* F_UNTIL(f1,f2) f *) 1185 INIT_TAC 1186 THEN EQ_TAC 1187 THEN RW_TAC std_ss [] 1188 THEN FULL_SIMP_TAC arith_ss [GT_LS] 1189 THEN IMP_RES_TAC LENGTH_RESTN_THM 1190 THEN Cases_on `w` 1191 THEN FULL_SIMP_TAC arith_ss 1192 [LENGTH_def,GT,LS,PSLPathTheory.SUB,RESTN_FINITE,xnum_11,xnum_to_def] 1193 THEN Q.EXISTS_TAC `k` 1194 THEN RW_TAC std_ss [] 1195 THENL 1196 [FIN_TAC ``k:num``, 1197 `j < LENGTH l` by DECIDE_TAC THEN FIN_TAC ``j:num``, 1198 INF_TAC ``f'' :num -> 'a -> bool`` ``k:num``, 1199 INF_TAC ``f'' :num -> 'a -> bool`` ``j:num``, 1200 FIN_TAC ``k:num``, 1201 `j < LENGTH l` by DECIDE_TAC THEN FIN_TAC ``j:num``, 1202 INF_TAC ``f'' :num -> 'a -> bool`` ``k:num``, 1203 INF_TAC ``f'' :num -> 'a -> bool`` ``j:num``], 1204 (* F_SUFFIX_IMP(s,f) *) 1205 INIT_TAC 1206 THEN EQ_TAC 1207 THEN RW_TAC std_ss [] 1208 THEN Cases_on `w` 1209 THEN FULL_SIMP_TAC arith_ss 1210 [LENGTH_def,GT,LS,PSLPathTheory.SUB,RESTN_FINITE,xnum_11,xnum_to_def,GT_LS] 1211 THEN RES_TAC 1212 THENL 1213 [FIN_TAC ``j:num``, 1214 INF_TAC ``f' :num -> 'a -> bool`` ``j:num``, 1215 FIN_TAC ``j:num``, 1216 INF_TAC ``f' :num -> 'a -> bool`` ``j:num``], 1217 (* F_STRONG_IMP(s1,s2) *) 1218 INIT_TAC , 1219 (* F_WEAK_IMP(s1,s2) *) 1220 INIT_TAC , 1221 (* F_ABORT(f,b)) *) 1222 INIT_TAC 1223 THEN EQ_TAC 1224 THEN RW_TAC std_ss [] 1225 THEN FULL_SIMP_TAC arith_ss [GT_LS] 1226 THEN IMP_RES_TAC LENGTH_RESTN_THM 1227 THEN Cases_on `w` 1228 THEN FULL_SIMP_TAC arith_ss [xnum_to_def,LENGTH_def,GT,LS,PSLPathTheory.SUB,RESTN_FINITE,xnum_11] 1229 THENL (* 4 subgoals *) 1230 [REPEAT DISJ2_TAC 1231 THEN Q.EXISTS_TAC `j` 1232 THEN RW_TAC std_ss [] 1233 THEN rename1 `OLD_UF_SEM (CAT (SEL (FINITE l) (0,j ��� 1),w'')) f` 1234 THEN Q.EXISTS_TAC `w''` (* was: w' *) 1235 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 1236 THEN Cases_on `w''` 1237 THEN RW_TAC std_ss [] 1238 THENL 1239 [`LENGTH(CAT (SEL (FINITE l) (0,j - 1),FINITE l')) = XNUM(j + LENGTH l')` 1240 by RW_TAC arith_ss [LENGTH_CAT,LENGTH_SEL] 1241 THEN FULL_SIMP_TAC std_ss [CAT_FINITE_APPEND,CAT_FINITE_APPEND,LENGTH_def,xnum_11] 1242 THEN `0 < LENGTH (SEL (FINITE l) (0,j - 1) <> l')` by DECIDE_TAC 1243 THEN `0 < LENGTH (FINITE(SEL (FINITE l) (0,j - 1) <> l'))` 1244 by PROVE_TAC[LENGTH_def,PSLPathTheory.LS,xnum_11] 1245 THEN PROVE_TAC[], 1246 `LENGTH(CAT (SEL (FINITE l) (0,j - 1),INFINITE f')) = INFINITY` 1247 by RW_TAC arith_ss [LENGTH_CAT] 1248 THEN `0 < LENGTH (CAT (SEL (FINITE l) (0,j - 1),INFINITE f'))` 1249 by PROVE_TAC[LENGTH_RESTN_INFINITE,LENGTH_def,PSLPathTheory.LS,xnum_11] 1250 THEN PROVE_TAC[]], 1251 REPEAT DISJ2_TAC 1252 THEN Q.EXISTS_TAC `j` 1253 THEN RW_TAC std_ss [LENGTH_RESTN_INFINITE,LS] 1254 THEN rename1 `OLD_UF_SEM (CAT (SEL (INFINITE f') (0,j ��� 1),w'')) f` 1255 THEN Q.EXISTS_TAC `w''` 1256 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 1257 THEN Cases_on `w''` 1258 THEN RW_TAC std_ss [] 1259 THENL 1260 [`LENGTH(CAT (SEL (INFINITE f') (0,j - 1),FINITE l)) = XNUM(j + LENGTH l)` 1261 by RW_TAC arith_ss [LENGTH_CAT,LENGTH_SEL] 1262 THEN FULL_SIMP_TAC std_ss [CAT_FINITE_APPEND,CAT_FINITE_APPEND,LENGTH_def,xnum_11] 1263 THEN `0 < LENGTH (SEL (INFINITE f') (0,j - 1) <> l)` by DECIDE_TAC 1264 THEN `0 < LENGTH (FINITE(SEL (INFINITE f') (0,j - 1) <> l))` 1265 by PROVE_TAC[LENGTH_def,PSLPathTheory.LS,xnum_11] 1266 THEN PROVE_TAC[], 1267 `LENGTH(CAT (SEL (INFINITE f') (0,j - 1),INFINITE f'')) = INFINITY` 1268 by RW_TAC arith_ss [LENGTH_CAT] 1269 THEN `0 < LENGTH (CAT (SEL (INFINITE f') (0,j - 1),INFINITE f''))` 1270 by PROVE_TAC[LENGTH_RESTN_INFINITE,LENGTH_def,PSLPathTheory.LS,xnum_11] 1271 THEN PROVE_TAC[]], 1272 REPEAT DISJ2_TAC 1273 THEN Q.EXISTS_TAC `j` 1274 THEN RW_TAC std_ss [] 1275 THEN rename1 `UF_SEM (CAT (SEL (FINITE l) (0,j ��� 1),w'')) f` 1276 THEN Q.EXISTS_TAC `w''` 1277 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 1278 THEN Cases_on `w''` 1279 THEN RW_TAC std_ss [] 1280 THENL 1281 [`LENGTH(CAT (SEL (FINITE l) (0,j - 1),FINITE l')) = XNUM(j + LENGTH l')` 1282 by RW_TAC arith_ss [LENGTH_CAT,LENGTH_SEL] 1283 THEN FULL_SIMP_TAC std_ss [CAT_FINITE_APPEND,CAT_FINITE_APPEND,LENGTH_def,xnum_11] 1284 THEN `0 < LENGTH (SEL (FINITE l) (0,j - 1) <> l')` by DECIDE_TAC 1285 THEN `0 < LENGTH (FINITE(SEL (FINITE l) (0,j - 1) <> l'))` 1286 by PROVE_TAC[LENGTH_def,PSLPathTheory.LS,xnum_11] 1287 THEN PROVE_TAC[], 1288 `LENGTH(CAT (SEL (FINITE l) (0,j - 1),INFINITE f')) = INFINITY` 1289 by RW_TAC arith_ss [LENGTH_CAT] 1290 THEN `0 < LENGTH (CAT (SEL (FINITE l) (0,j - 1),INFINITE f'))` 1291 by PROVE_TAC[LENGTH_RESTN_INFINITE,LENGTH_def,PSLPathTheory.LS,xnum_11] 1292 THEN PROVE_TAC[]], 1293 REPEAT DISJ2_TAC 1294 THEN Q.EXISTS_TAC `j` 1295 THEN RW_TAC std_ss [LENGTH_RESTN_INFINITE,LS] 1296 THEN rename1 `UF_SEM (CAT (SEL (INFINITE f') (0,j ��� 1),w'')) f` 1297 THEN Q.EXISTS_TAC `w''` 1298 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN] 1299 THEN Cases_on `w''` 1300 THEN RW_TAC std_ss [] 1301 THENL 1302 [`LENGTH(CAT (SEL (INFINITE f') (0,j - 1),FINITE l)) = XNUM(j + LENGTH l)` 1303 by RW_TAC arith_ss [LENGTH_CAT,LENGTH_SEL] 1304 THEN FULL_SIMP_TAC std_ss [CAT_FINITE_APPEND,CAT_FINITE_APPEND,LENGTH_def,xnum_11] 1305 THEN `0 < LENGTH (SEL (INFINITE f') (0,j - 1) <> l)` by DECIDE_TAC 1306 THEN `0 < LENGTH (FINITE(SEL (INFINITE f') (0,j - 1) <> l))` 1307 by PROVE_TAC[LENGTH_def,PSLPathTheory.LS,xnum_11] 1308 THEN PROVE_TAC[], 1309 `LENGTH(CAT (SEL (INFINITE f') (0,j - 1),INFINITE f'')) = INFINITY` 1310 by RW_TAC arith_ss [LENGTH_CAT] 1311 THEN `0 < LENGTH (CAT (SEL (INFINITE f') (0,j - 1),INFINITE f''))` 1312 by PROVE_TAC[LENGTH_RESTN_INFINITE,LENGTH_def,PSLPathTheory.LS,xnum_11] 1313 THEN PROVE_TAC[]]], 1314 (* F_STRONG_CLOCK(f,c) *) 1315 INIT_TAC]); 1316end; 1317 1318(****************************************************************************** 1319* F_ABORT_FREE f means f contains no abort statements 1320******************************************************************************) 1321val F_ABORT_FREE_def = 1322 Define 1323 `(F_ABORT_FREE (F_BOOL b) = T) 1324 /\ 1325 (F_ABORT_FREE (F_NOT f) = F_ABORT_FREE f) 1326 /\ 1327 (F_ABORT_FREE (F_AND(f1,f2)) = F_ABORT_FREE f1 /\ F_ABORT_FREE f2) 1328 /\ 1329 (F_ABORT_FREE (F_NEXT f) = F_ABORT_FREE f) 1330 /\ 1331 (F_ABORT_FREE (F_UNTIL(f1,f2)) = F_ABORT_FREE f1 /\ F_ABORT_FREE f2) 1332 /\ 1333 (F_ABORT_FREE (F_SUFFIX_IMP(r,f)) = F_ABORT_FREE f) 1334 /\ 1335 (F_ABORT_FREE (F_STRONG_IMP(r1,r2)) = T) 1336 /\ 1337 (F_ABORT_FREE (F_WEAK_IMP(r1,r2)) = T) 1338 /\ 1339 (F_ABORT_FREE (F_ABORT (f,b)) = F) 1340 /\ 1341 (F_ABORT_FREE (F_STRONG_CLOCK(f,c)) = F_ABORT_FREE f)`; 1342 1343(****************************************************************************** 1344* Proof that if there are no aborts then 1345* F_CLOCK_COMP and F_INIT_CLOCK_COMP are equivalent. 1346******************************************************************************) 1347local 1348val INIT_TAC = 1349 RW_TAC std_ss 1350 [F_ABORT_FREE_def,F_CLOCK_COMP_def,F_INIT_CLOCK_COMP_def,UF_SEM_def,B_SEM]; 1351in 1352val ABORT_FREE_INIT_CLOCK_COMP_EQUIV = 1353 store_thm 1354 ("ABORT_FREE_INIT_CLOCK_COMP_EQUIV", 1355 ``!f. 1356 F_ABORT_FREE f 1357 ==> 1358 !w c. UF_SEM w (F_CLOCK_COMP c f) = UF_SEM w (F_INIT_CLOCK_COMP c f)``, 1359 INDUCT_THEN fl_induct ASSUME_TAC 1360 THENL 1361 [(* F_BOOL b *) 1362 INIT_TAC, 1363 (* F_NOT b *) 1364 INIT_TAC, 1365 (* F_AND (f1,f2) *) 1366 INIT_TAC, 1367 (* F_NEXT f *) 1368 INIT_TAC 1369 THEN RW_TAC (arith_ss++resq_SS) [UF_SEM_F_U_CLOCK,RESTN_RESTN] 1370 THEN Cases_on `w` 1371 THEN RW_TAC arith_ss 1372 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE, 1373 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1374 THEN EQ_TAC 1375 THEN RW_TAC std_ss [] 1376 THEN Q.EXISTS_TAC `i` 1377 THEN PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`j`,`0`]ELEM_RESTN)], 1378 (* F_UNTIL(f1,f2) f *) 1379 INIT_TAC 1380 THEN RW_TAC (arith_ss++resq_SS) [ELEM_RESTN,UF_SEM_F_IMPLIES,UF_SEM_def] 1381 THEN Cases_on `w` 1382 THEN RW_TAC arith_ss 1383 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE, 1384 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1385 THEN EQ_TAC 1386 THEN RW_TAC std_ss [] 1387 THEN Q.EXISTS_TAC `k` 1388 THEN PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`j`,`0`]ELEM_RESTN)], 1389 (* F_SUFFIX_IMP(s,f) *) 1390 INIT_TAC 1391 THEN RW_TAC (arith_ss++resq_SS) [ELEM_RESTN,UF_SEM_F_IMPLIES,UF_SEM_def] 1392 THEN Cases_on `w` 1393 THEN RW_TAC (arith_ss ++resq_SS) 1394 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE,UF_SEM_F_U_CLOCK,LENGTH_RESTN, 1395 RESTN_FINITE,num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN,RESTN_RESTN] 1396 THEN EQ_TAC 1397 THEN RW_TAC std_ss [] 1398 THEN RES_TAC 1399 THEN Q.EXISTS_TAC `i` 1400 THEN RW_TAC arith_ss [] 1401 THEN FULL_SIMP_TAC std_ss [GSYM(SIMP_RULE arith_ss [] (Q.SPECL[`i+j`,`0`]ELEM_RESTN))] 1402 THEN PROVE_TAC[RESTN_FINITE], 1403 (* F_STRONG_IMP(s1,s2) *) 1404 INIT_TAC, 1405 (* F_WEAK_IMP(s1,s2) *) 1406 INIT_TAC, 1407 (* F_ABORT(f,b)) *) 1408 INIT_TAC, 1409 (* F_STRONG_CLOCK(f,c) *) 1410 INIT_TAC 1411 THEN RW_TAC (arith_ss++resq_SS) [UF_SEM_F_U_CLOCK,RESTN_RESTN] 1412 THEN Cases_on `w` 1413 THEN RW_TAC arith_ss 1414 [LENGTH_def,GT_xnum_num_def,LENGTH_RESTN_INFINITE, 1415 num_to_def,xnum_to_def,NEXT_RISE,ELEM_RESTN] 1416 THEN EQ_TAC 1417 THEN RW_TAC std_ss [] 1418 THEN Q.EXISTS_TAC `i` 1419 THEN RW_TAC std_ss [] 1420 THEN PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`j`,`0`]ELEM_RESTN)]]); 1421end; 1422 1423val ABORT_FREE_F_CLOCK_COMP_CORRECT = 1424 store_thm 1425 ("ABORT_FREE_F_CLOCK_COMP_CORRECT", 1426 ``!f. F_ABORT_FREE f ==> 1427 !w c. F_SEM w c f = UF_SEM w (F_CLOCK_COMP c f)``, 1428 PROVE_TAC[F_INIT_CLOCK_COMP_ELIM,F_INIT_CLOCK_COMP_CORRECT_def, 1429 ABORT_FREE_INIT_CLOCK_COMP_EQUIV]); 1430 1431(****************************************************************************** 1432* Version of Define that doesn't add to the EVAL compset 1433******************************************************************************) 1434val pureDefine = with_flag (computeLib.auto_import_definitions, false) Define; 1435 1436(****************************************************************************** 1437* Joe Hurd hack: EVAL should never get hold of this definition 1438******************************************************************************) 1439val UNINT_def = pureDefine `UNINT x = x`; 1440 1441val F_CLOCK_COMP_ELIM = 1442 store_thm 1443 ("F_CLOCK_COMP_ELIM", 1444 ``F_SEM w c f = 1445 if B_SEM (ELEM w 0) c 1446 then UF_SEM w (F_CLOCK_COMP c f) 1447 else (UNINT F_SEM) w c f``, 1448 RW_TAC std_ss [UNINT_def,F_CLOCK_COMP_CORRECT]); 1449 1450val ABORT_FREE_F_CLOCK_COMP_CORRECT_COR = 1451 store_thm 1452 ("ABORT_FREE_F_CLOCK_COMP_CORRECT_COR", 1453 ``F_SEM w c f = 1454 if F_ABORT_FREE f 1455 then UF_SEM w (F_CLOCK_COMP c f) 1456 else (UNINT F_SEM) w c f``, 1457 RW_TAC std_ss [UNINT_def,ABORT_FREE_F_CLOCK_COMP_CORRECT]); 1458 1459(****************************************************************************** 1460* Associativity of SERE concantenation (;) 1461******************************************************************************) 1462 1463val S_CAT_ASSOC = 1464 store_thm 1465 ("S_CAT_ASSOC", 1466 ``!w r1 r2 r3. 1467 US_SEM w (S_CAT(S_CAT(r1,r2),r3)) = 1468 US_SEM w (S_CAT(r1, S_CAT(r2,r3)))``, 1469 RW_TAC simp_list_ss [US_SEM_def] 1470 THEN PROVE_TAC[APPEND_ASSOC]); 1471 1472val S_NONEMPTY_def = 1473 Define `S_NONEMPTY r = !w. US_SEM w r ==> ~(NULL w)`; 1474 1475val TL_APPEND = 1476 store_thm 1477 ("TL_APPEND", 1478 ``~(NULL l1) ==> (TL(l1 <> l2) = TL l1 <> l2)``, 1479 Induct_on `l1` 1480 THEN RW_TAC simp_list_ss []); 1481 1482(****************************************************************************** 1483* (r1:r2);r3 = r1:(r2;r3) 1484******************************************************************************) 1485 1486val S_CAT_FUSION_ASSOC = 1487 store_thm 1488 ("S_CAT_FUSION_ASSOC", 1489 ``!w r1 r2 r3. 1490 S_NONEMPTY r2 1491 ==> 1492 (US_SEM w (S_CAT(S_FUSION(r1,r2),r3)) = 1493 US_SEM w (S_FUSION(r1, S_CAT(r2,r3))))``, 1494 RW_TAC simp_list_ss [US_SEM_def] 1495 THEN EQ_TAC 1496 THEN RW_TAC simp_list_ss [APPEND_ASSOC] 1497 THEN FULL_SIMP_TAC simp_list_ss [S_NONEMPTY_def] 1498 THENL 1499 [Q.EXISTS_TAC `w1'` THEN Q.EXISTS_TAC `w2'<>w2` THEN Q.EXISTS_TAC `l` 1500 THEN RW_TAC std_ss [APPEND_ASSOC] 1501 THEN Q.EXISTS_TAC `l::w2'` THEN Q.EXISTS_TAC `w2` 1502 THEN RW_TAC simp_list_ss [APPEND_ASSOC], 1503 Q.EXISTS_TAC `w1<>[l]<>(TL w1')` THEN Q.EXISTS_TAC `w2'` 1504 THEN ASSUM_LIST 1505 (fn thl => 1506 ASSUME_TAC 1507 (SIMP_RULE simp_list_ss [](Q.AP_TERM `TL` (el 3 thl)))) 1508 THEN RW_TAC simp_list_ss [APPEND_ASSOC] 1509 THENL 1510 [PROVE_TAC[TL_APPEND,APPEND_ASSOC], 1511 Q.EXISTS_TAC `w1` THEN Q.EXISTS_TAC `TL w1'` THEN Q.EXISTS_TAC `l` 1512 THEN RW_TAC simp_list_ss [APPEND_ASSOC] 1513 THEN RES_TAC 1514 THEN IMP_RES_TAC TL_APPEND 1515 THEN POP_ASSUM(fn th => ASSUME_TAC(Q.SPEC `w2'` th)) 1516 THEN PROVE_TAC[APPEND_RIGHT_CANCEL,APPEND_ASSOC,APPEND]]]); 1517 1518val CONCAT_APPEND = 1519 store_thm 1520 ("CONCAT_APPEND", 1521 ``!ll1 ll2: 'a list list. CONCAT(ll1<>ll2) = (CONCAT ll1)<>(CONCAT ll2)``, 1522 Induct 1523 THEN RW_TAC simp_list_ss [CONCAT_def]); 1524 1525(****************************************************************************** 1526* Idempotency of r[*]: r[*];r[*] = [*] 1527******************************************************************************) 1528 1529val S_REPEAT_IDEMPOTENT = 1530 store_thm 1531 ("S_REPEAT_IDEMPOTENT", 1532 ``!w r. US_SEM w (S_CAT(S_REPEAT r,S_REPEAT r)) = US_SEM w (S_REPEAT r)``, 1533 RW_TAC simp_list_ss [US_SEM_def,B_SEM] 1534 THEN EQ_TAC 1535 THEN RW_TAC simp_list_ss [] 1536 THENL 1537 [Q.EXISTS_TAC `wlist<>wlist'` 1538 THEN RW_TAC simp_list_ss [ALL_EL_APPEND,CONCAT_APPEND], 1539 Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `CONCAT wlist` 1540 THEN RW_TAC simp_list_ss [] 1541 THENL 1542 [Q.EXISTS_TAC `[]` 1543 THEN RW_TAC simp_list_ss [CONCAT_def], 1544 PROVE_TAC[]]]); 1545 1546(****************************************************************************** 1547* Idempotency of r[*]: r[*];r[*] = r[*] 1548******************************************************************************) 1549 1550val S_REPEAT_IDEMPOTENT = 1551 store_thm 1552 ("S_REPEAT_IDEMPOTENT", 1553 ``!w r. US_SEM w (S_CAT(S_REPEAT r,S_REPEAT r)) = US_SEM w (S_REPEAT r)``, 1554 RW_TAC simp_list_ss [US_SEM_def,B_SEM] 1555 THEN EQ_TAC 1556 THEN RW_TAC simp_list_ss [] 1557 THENL 1558 [Q.EXISTS_TAC `wlist<>wlist'` 1559 THEN RW_TAC simp_list_ss [ALL_EL_APPEND,CONCAT_APPEND], 1560 Q.EXISTS_TAC `[]` THEN Q.EXISTS_TAC `CONCAT wlist` 1561 THEN RW_TAC simp_list_ss [] 1562 THENL 1563 [Q.EXISTS_TAC `[]` 1564 THEN RW_TAC simp_list_ss [CONCAT_def], 1565 PROVE_TAC[]]]); 1566 1567 1568val _ = export_theory(); 1569