1 2(*****************************************************************************) 3(* Correctness of the PSL 1.1 rewrites *) 4(* (guided in some places by hand proofs due to Dana Fisman) *) 5(* ------------------------------------------------------------------------- *) 6(* *) 7(* Started: Wed Feb 25, 2004 *) 8(* Completed: Sat Mar 06, 2004 *) 9(*****************************************************************************) 10 11(*****************************************************************************) 12(* START BOILERPLATE *) 13(*****************************************************************************) 14 15(****************************************************************************** 16* Load theories 17* (commented out for compilation) 18******************************************************************************) 19(* 20quietdec := true; 21loadPath 22 := 23 "../official-semantics" :: "../../regexp" :: "../../path" :: !loadPath; 24map load 25 ["UnclockedSemanticsTheory", 26 "SyntacticSugarTheory", "ClockedSemanticsTheory", "RewritesTheory", 27 "rich_listTheory", "intLib", "res_quanLib", "res_quanTheory","LemmasTheory"]; 28open FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 29 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 30 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory 31 ClockedSemanticsTheory LemmasTheory; 32val _ = intLib.deprecate_int(); 33quietdec := false; 34*) 35 36(****************************************************************************** 37* Boilerplate needed for compilation 38******************************************************************************) 39open HolKernel Parse boolLib bossLib; 40 41(****************************************************************************** 42* Open theories 43******************************************************************************) 44open FinitePSLPathTheory PSLPathTheory SyntaxTheory SyntacticSugarTheory 45 UnclockedSemanticsTheory ClockedSemanticsTheory RewritesTheory 46 arithmeticTheory listTheory rich_listTheory res_quanLib res_quanTheory 47 ClockedSemanticsTheory LemmasTheory; 48 49(****************************************************************************** 50* Set default parsing to natural numbers rather than integers 51******************************************************************************) 52val _ = intLib.deprecate_int(); 53 54(*****************************************************************************) 55(* END BOILERPLATE *) 56(*****************************************************************************) 57 58(****************************************************************************** 59* Start a new theory called RewritesProperties 60******************************************************************************) 61val _ = new_theory "RewritesProperties"; 62val _ = ParseExtras.temp_loose_equality() 63 64local 65 val th = prove (``!a b. a /\ (a ==> b) ==> a /\ b``, PROVE_TAC []) 66in 67 val STRONG_CONJ_TAC :tactic = MATCH_MP_TAC th >> CONJ_TAC 68end; 69 70(****************************************************************************** 71* A simpset fragment to rewrite away quantifiers restricted with :: (a to b) 72******************************************************************************) 73val resq_SS = 74 simpLib.merge_ss 75 [res_quanTools.resq_SS, 76 rewrites 77 [IN_DEF,LESS_def,LESSX_def,LENGTH_def]]; 78 79(****************************************************************************** 80* SEREs only need finite paths 81******************************************************************************) 82open FinitePSLPathTheory; 83 84val US_SEM_BOOL_REWRITE_LEMMA = 85 store_thm 86 ("US_SEM_BOOL_REWRITE_LEMMA", 87 ``US_SEM v (S_CAT (S_REPEAT (S_BOOL (B_NOT c)),S_BOOL (B_AND (c,b)))) = 88 LENGTH v > 0 /\ 89 B_SEM (ELEM v (LENGTH v - 1)) b /\ 90 B_SEM (ELEM v (LENGTH v - 1)) c /\ 91 !i. i < LENGTH v - 1 ==> B_SEM (ELEM v i) (B_NOT c)``, 92 RW_TAC (std_ss++resq_SS) [US_SEM_def,LENGTH1] 93 THEN EQ_TAC 94 THEN RW_TAC list_ss [LENGTH_APPEND] 95 THEN FULL_SIMP_TAC list_ss 96 [ELEM_def,RESTN_def,HEAD_def,B_SEM_def,LENGTH_APPEND,RESTN_APPEND] 97 THENL 98 [Cases_on `x` 99 THEN FULL_SIMP_TAC list_ss [B_SEM_def], 100 Cases_on `x` 101 THEN FULL_SIMP_TAC list_ss [B_SEM_def], 102 FULL_SIMP_TAC list_ss [EVERY_EL,EL_APPEND1,HD_RESTN] 103 THEN `(LENGTH (CONCAT vlist) = LENGTH vlist) /\ i < LENGTH vlist` 104 by PROVE_TAC[EVERY_EL_SINGLETON_LENGTH] 105 THEN `CONCAT vlist = MAP HD vlist` by PROVE_TAC[EVERY_EL_SINGLETON] 106 THEN RW_TAC list_ss [EL_MAP] 107 THEN PROVE_TAC[HD], 108 FULL_SIMP_TAC list_ss [EVERY_EL,EL_APPEND1,HD_RESTN] 109 THEN Q.EXISTS_TAC `BUTLAST v` 110 THEN Q.EXISTS_TAC `[LAST v]` 111 THEN RW_TAC list_ss [] 112 THEN RW_TAC list_ss [APPEND_BUTLAST_LAST,LENGTH_NIL_LEMMA] 113 THEN `LENGTH v >= 1` by DECIDE_TAC 114 THENL 115 [Q.EXISTS_TAC `MAP(\l.[l])(BUTLAST v)` 116 THEN RW_TAC list_ss [CONCAT_MAP_SINGLETON,EL_MAP] 117 THEN IMP_RES_TAC LENGTH_NIL_LEMMA 118 THEN IMP_RES_TAC LENGTH_BUTLAST 119 THEN `n:num < LENGTH v - 1` by DECIDE_TAC 120 THEN PROVE_TAC[EL_BUTLAST], 121 IMP_RES_TAC EL_PRE_LENGTH 122 THEN POP_ASSUM(fn th => RW_TAC list_ss [GSYM th]) 123 THEN Cases_on `EL (LENGTH v - 1) v` 124 THEN FULL_SIMP_TAC std_ss [B_SEM_def]]]); 125 126(****************************************************************************** 127* v |=c r <==> v |= (S_CLOCK_COMP c r) 128******************************************************************************) 129 130val S_CLOCK_COMP_CORRECT = 131 store_thm 132 ("S_CLOCK_COMP_CORRECT", 133 ``!r v c. S_SEM v c r = US_SEM v (S_CLOCK_COMP c r)``, 134 INDUCT_THEN sere_induct ASSUME_TAC 135 THENL 136 [(* S_BOOL b *) 137 RW_TAC std_ss [S_SEM_def, US_SEM_def] 138 THEN RW_TAC std_ss [CLOCK_TICK_def] 139 THEN RW_TAC (std_ss++resq_SS) [] 140 THEN RW_TAC (std_ss++resq_SS) [S_CLOCK_COMP_def] 141 THEN PROVE_TAC[US_SEM_BOOL_REWRITE_LEMMA], 142 (* S_CAT(r,r') *) 143 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def], 144 (* S_FUSION (r,r') *) 145 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def], 146 (* S_OR (r,r') *) 147 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def], 148 (* S_AND (r,r') *) 149 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def], 150 (* S_EMPTY *) 151 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def], 152 (* S_REPEAT r *) 153 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def], 154 (* S_CLOCK (r,p_2) *) 155 RW_TAC (std_ss ++ resq_SS) [S_SEM_def, US_SEM_def, S_CLOCK_COMP_def]]); 156 157(****************************************************************************** 158* Formulas need infinite paths 159******************************************************************************) 160open PSLPathTheory; 161 162(****************************************************************************** 163* Structural induction rule for FL formulas 164******************************************************************************) 165val fl_induct = 166 save_thm 167 ("fl_induct", 168 Q.GEN 169 `P` 170 (MATCH_MP 171 (DECIDE ``(A ==> (B1 /\ B2 /\ B3)) ==> (A ==> B1)``) 172 (SIMP_RULE 173 std_ss 174 [pairTheory.FORALL_PROD, 175 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 176 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 177 (Q.SPECL 178 [`P`,`\ (f,b). P f`,`\ (r,f). P f`,`\ (f1,f2). P f1 /\ P f2`] 179 (TypeBase.induction_of ``:'a fl``))))); 180 181val LS_LE_X = 182 store_thm 183 ("LS_LE_X", 184 ``m:num < n:xnum ==> m <= n``, 185 Cases_on `n` 186 THEN RW_TAC arith_ss [LS,LE]); 187 188val LS_TRANS_X = 189 store_thm 190 ("LS_TRANS_X", 191 ``m:num < n:num ==> n < p:xnum ==> m < p``, 192 Cases_on `p` 193 THEN RW_TAC arith_ss [LS]); 194 195local 196open FinitePSLPathTheory 197in 198val RESTN_NIL_LENGTH = 199 store_thm 200 ("RESTN_NIL_LENGTH", 201 ``!k v. k <= LENGTH v ==> ((RESTN v k = []) = (LENGTH v = k))``, 202 Induct 203 THEN RW_TAC list_ss [FinitePSLPathTheory.RESTN_def,LENGTH_NIL,REST_def] 204 THEN ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `TL v` (el 2 thl))) 205 THEN `0 < LENGTH v` by DECIDE_TAC 206 THEN `LENGTH(TL v) = LENGTH v - 1` by PROVE_TAC[LENGTH_TL] 207 THEN `k <= LENGTH(TL v)` by DECIDE_TAC 208 THEN RES_TAC 209 THEN RW_TAC list_ss []); 210end; 211 212val PATH_LENGTH_RESTN_0 = 213 store_thm 214 ("PATH_LENGTH_RESTN_0", 215 ``!k v. 216 k <= LENGTH v 217 ==> 218 ((LENGTH(RESTN v k) = XNUM 0) = (LENGTH v = XNUM k))``, 219 REPEAT GEN_TAC 220 THEN Cases_on `v` 221 THEN RW_TAC list_ss [LENGTH_RESTN_INFINITE,LENGTH_def,LE] 222 THEN RW_TAC list_ss 223 [xnum_11,LENGTH_NIL,RESTN_def,LENGTH_def, 224 RESTN_FINITE,RESTN_NIL_LENGTH]); 225 226val PATH_FINITE_LENGTH_RESTN_0 = 227 store_thm 228 ("PATH_FINITE_LENGTH_RESTN_0", 229 ``!k v. 230 k <= LENGTH v 231 ==> 232 ((LENGTH(RESTN v k) = XNUM 0) = 233 ?l. (LENGTH l = k) /\ (v = FINITE l))``, 234 REPEAT GEN_TAC 235 THEN Cases_on `v` 236 THEN RW_TAC list_ss [LENGTH_RESTN_INFINITE,LENGTH_def,LE] 237 THEN RW_TAC list_ss 238 [xnum_11,LENGTH_NIL,RESTN_def,LENGTH_def, 239 RESTN_FINITE,RESTN_NIL_LENGTH]); 240 241val LIST_LENGTH_RESTN_0 = 242 store_thm 243 ("LIST_LENGTH_RESTN_0", 244 ``!k l. 245 k <= LENGTH l 246 ==> 247 ((LENGTH(RESTN l k) = 0) = (LENGTH l = k))``, 248 RW_TAC list_ss [LENGTH_RESTN_INFINITE,LENGTH_def,LE] 249 THEN RW_TAC list_ss 250 [LENGTH_NIL,RESTN_def,LENGTH_def, 251 RESTN_FINITE,RESTN_NIL_LENGTH]); 252 253val PATH_FINITE_LENGTH_RESTN_0_COR = 254 store_thm 255 ("PATH_FINITE_LENGTH_RESTN_0_COR", 256 ``!k v. 257 k < LENGTH v 258 ==> 259 ((LENGTH(RESTN v k) = XNUM 0) = 260 ?l. (LENGTH l = k) /\ (v = FINITE l))``, 261 PROVE_TAC[LS_LE_X,PATH_FINITE_LENGTH_RESTN_0]); 262 263(****************************************************************************** 264* Unclocked semantics of [!c U (c /\ f)] 265******************************************************************************) 266val UF_SEM_F_U_CLOCK = 267 store_thm 268 ("UF_SEM_F_U_CLOCK", 269 ``UF_SEM v (F_U_CLOCK c f) = 270 ?j :: LESS(LENGTH v). 271 UF_SEM (RESTN v j) (F_AND(F_WEAK_BOOL c,f)) /\ 272 !i. i < j ==> B_SEM (ELEM v i) (B_NOT c)``, 273 RW_TAC (arith_ss ++ resq_SS) 274 [F_U_CLOCK_def,ELEM_RESTN,UF_SEM_def,CLOCK_TICK_def,LENGTH_SEL] 275 THEN EQ_TAC 276 THEN RW_TAC std_ss [] 277 THENL 278 [Q.EXISTS_TAC `k` 279 THEN RW_TAC std_ss [] 280 THEN RES_TAC 281 THEN IMP_RES_TAC LS_TRANS_X 282 THEN IMP_RES_TAC LS_LE_X 283 THEN IMP_RES_TAC PATH_FINITE_LENGTH_RESTN_0 284 THEN `~(i=k)` by DECIDE_TAC 285 THEN RW_TAC std_ss [], 286 Q.EXISTS_TAC `k` 287 THEN RW_TAC std_ss [] 288 THEN RES_TAC 289 THEN IMP_RES_TAC LS_TRANS_X 290 THEN IMP_RES_TAC LS_LE_X 291 THEN IMP_RES_TAC PATH_FINITE_LENGTH_RESTN_0 292 THEN RW_TAC std_ss [] 293 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS], 294 Q.EXISTS_TAC `j` 295 THEN RW_TAC std_ss [], 296 Q.EXISTS_TAC `j` 297 THEN RW_TAC std_ss []]); 298 299val COMPLEMENT_LETTER_COMPLEMENT_LETTER = 300 store_thm 301 ("COMPLEMENT_LETTER_COMPLEMENT_LETTER", 302 ``COMPLEMENT_LETTER(COMPLEMENT_LETTER l) = l``, 303 Cases_on `l` 304 THEN RW_TAC std_ss [COMPLEMENT_LETTER_def]); 305 306val COMPLEMENT_LETTER_COMPLEMENT_LETTER_o = 307 store_thm 308 ("COMPLEMENT_LETTER_COMPLEMENT_LETTER_o", 309 ``COMPLEMENT_LETTER o COMPLEMENT_LETTER = I``, 310 CONV_TAC FUN_EQ_CONV 311 THEN RW_TAC std_ss [COMPLEMENT_LETTER_COMPLEMENT_LETTER]); 312 313val MAP_I = 314 store_thm 315 ("MAP_I", 316 ``!l. MAP I l = l``, 317 Induct 318 THEN RW_TAC list_ss []); 319 320val COMPLEMENT_COMPLEMENT = 321 store_thm 322 ("COMPLEMENT_COMPLEMENT", 323 ``COMPLEMENT(COMPLEMENT l) = l``, 324 Cases_on `l` 325 THEN RW_TAC std_ss 326 [COMPLEMENT_def,MAP_I,MAP_MAP_o, 327 COMPLEMENT_LETTER_COMPLEMENT_LETTER_o] 328 THEN ONCE_REWRITE_TAC[combinTheory.o_ASSOC] 329 THEN REWRITE_TAC 330 [COMPLEMENT_LETTER_COMPLEMENT_LETTER_o,combinTheory.I_o_ID]); 331 332val LENGTH_COMPLEMENT = 333 store_thm 334 ("LENGTH_COMPLEMENT", 335 ``LENGTH(COMPLEMENT v) = LENGTH v``, 336 Cases_on `v` 337 THEN RW_TAC std_ss 338 [COMPLEMENT_def,LENGTH_def,LENGTH_MAP]); 339 340val HD_MAP = 341 store_thm 342 ("HD_MAP", 343 ``!f l. ~(l=[]) ==> (HD(MAP f l) = f(HD l))``, 344 GEN_TAC 345 THEN Induct 346 THEN RW_TAC list_ss []); 347 348val TL_MAP = 349 store_thm 350 ("TL_MAP", 351 ``!f l. ~(l=[]) ==> (TL(MAP f l) = MAP f (TL l))``, 352 GEN_TAC 353 THEN Induct 354 THEN RW_TAC list_ss []); 355 356val RESTN_COMPLEMENT = (* Harder to prove than expected *) 357 store_thm 358 ("RESTN_COMPLEMENT", 359 ``!n v. n < LENGTH v ==> (RESTN (COMPLEMENT v) n = COMPLEMENT(RESTN v n))``, 360 Induct 361 THEN Induct 362 THEN RW_TAC list_ss [RESTN_def,COMPLEMENT_def,REST_def] 363 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS] 364 THENL 365 [`0 < LENGTH l` by DECIDE_TAC 366 THEN IMP_RES_TAC LENGTH_TL 367 THEN `n < LENGTH(TL l)` by DECIDE_TAC 368 THEN ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `FINITE(TL l)` (el 5 thl))) 369 THEN `~(LENGTH l = 0)` by DECIDE_TAC 370 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 371 THEN IMP_RES_TAC(Q.ISPEC `COMPLEMENT_LETTER` TL_MAP) 372 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS,COMPLEMENT_def] 373 THEN RES_TAC 374 THEN RW_TAC list_ss [], 375 ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `REST(INFINITE f)` (el 2 thl))) 376 THEN FULL_SIMP_TAC list_ss 377 [LENGTH_def,LS,COMPLEMENT_def,REST_def,combinTheory.o_DEF]]); 378 379val RESTN_COMPLEMENT_COR = 380 save_thm 381 ("RESTN_COMPLEMENT_COR", 382 SIMP_RULE 383 std_ss 384 [LENGTH_def,LS] 385 (ISPECL[``n:num``,``FINITE(l:'a letter list)``]RESTN_COMPLEMENT)); 386 387val ELEM_COMPLEMENT = 388 store_thm 389 ("ELEM_COMPLEMENT", 390 ``!n v. n < LENGTH v ==> (ELEM (COMPLEMENT v) n = COMPLEMENT_LETTER(ELEM v n))``, 391 Induct 392 THEN Induct 393 THEN RW_TAC list_ss [RESTN_def,COMPLEMENT_def,REST_def,ELEM_def,HEAD_def] 394 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS] 395 THENL 396 [Cases_on `l` 397 THEN RW_TAC list_ss [] 398 THEN FULL_SIMP_TAC list_ss [], 399 ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `FINITE(TL l)` (el 2 thl))) 400 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS] 401 THEN `0 < LENGTH l` by DECIDE_TAC 402 THEN `LENGTH(TL l) = LENGTH l - 1` by PROVE_TAC[LENGTH_TL] 403 THEN `n < LENGTH(TL l)` by DECIDE_TAC 404 THEN RES_TAC 405 THEN FULL_SIMP_TAC list_ss [RESTN_def,COMPLEMENT_def,REST_def,ELEM_def,HEAD_def] 406 THEN `~(LENGTH l = 0)` by DECIDE_TAC 407 THEN `~(l = [])` by PROVE_TAC[LENGTH_NIL] 408 THEN IMP_RES_TAC(Q.ISPEC `COMPLEMENT_LETTER` TL_MAP) 409 THEN RW_TAC std_ss [], 410 ASSUM_LIST(fn thl => ASSUME_TAC(Q.SPEC `REST(INFINITE f)` (el 2 thl))) 411 THEN FULL_SIMP_TAC list_ss 412 [LENGTH_def,LS,COMPLEMENT_def,REST_def,combinTheory.o_DEF, 413 RESTN_def,COMPLEMENT_def,REST_def,ELEM_def,HEAD_def]]); 414 415val ELEM_COMPLEMENT_COR = 416 save_thm 417 ("ELEM_COMPLEMENT_COR", 418 SIMP_RULE 419 std_ss 420 [LENGTH_def,LS] 421 (ISPECL[``n:num``,``FINITE(l:'a letter list)``]ELEM_COMPLEMENT)); 422 423(****************************************************************************** 424* Formula disjunction: f1 \/ f2 425******************************************************************************) 426val UF_SEM_F_OR = 427 store_thm 428 ("UF_SEM_F_OR", 429 ``UF_SEM v (F_OR(f1,f2)) = UF_SEM v f1 \/ UF_SEM v f2``, 430 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def,F_OR_def,COMPLEMENT_COMPLEMENT]); 431 432(****************************************************************************** 433* Formula conjunction: f1 /\ f2 434******************************************************************************) 435val UF_SEM_F_AND = 436 store_thm 437 ("UF_SEM_F_AND", 438 ``UF_SEM v (F_AND(f1,f2)) = UF_SEM v f1 /\ UF_SEM v f2``, 439 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def]); 440 441(****************************************************************************** 442* Formula implication: f1 --> f2 443******************************************************************************) 444val UF_SEM_F_IMPLIES = 445 store_thm 446 ("UF_SEM_F_IMPLIES", 447 ``UF_SEM v (F_IMPLIES (f1,f2)) = UF_SEM (COMPLEMENT v) f1 ==> UF_SEM v f2``, 448 RW_TAC (std_ss ++ resq_SS) [UF_SEM_def,F_IMPLIES_def,UF_SEM_F_OR] 449 THEN PROVE_TAC[]); 450 451val UF_SEM_RESTN_F_WEAK_BOOL = 452 store_thm 453 ("UF_SEM_RESTN_F_WEAK_BOOL", 454 ``!j v. 455 j < LENGTH v 456 ==> 457 (UF_SEM (RESTN v j) (F_WEAK_BOOL b) = B_SEM (ELEM v j) b)``, 458 RW_TAC list_ss [UF_SEM_def,ELEM_RESTN] 459 THEN EQ_TAC 460 THEN RW_TAC list_ss [] 461 THEN IMP_RES_TAC LS_LE_X 462 THEN IMP_RES_TAC PATH_LENGTH_RESTN_0 463 THEN `j < XNUM j` by PROVE_TAC[] 464 THEN FULL_SIMP_TAC list_ss [LS]); 465 466val UF_SEM_RESTN_F_WEAK_BOOL_COR = 467 store_thm 468 ("UF_SEM_RESTN_F_WEAK_BOOL_COR", 469 ``!j v. 470 j < LENGTH v /\ UF_SEM (RESTN v j) (F_WEAK_BOOL b) = 471 j < LENGTH v /\ B_SEM (ELEM v j) b``, 472 PROVE_TAC[UF_SEM_RESTN_F_WEAK_BOOL]); 473 474(****************************************************************************** 475* Eventually: F f (implication) 476******************************************************************************) 477val UF_SEM_F_F_IMP = 478 store_thm 479 ("UF_SEM_F_F_IMP", 480 ``UF_SEM v (F_F f) ==> ?i :: LESS(LENGTH v). UF_SEM (RESTN v i) f``, 481 RW_TAC (arith_ss ++ resq_SS) [UF_SEM_def,F_F_def,B_SEM_def] 482 THEN Cases_on `v` 483 THEN RW_TAC arith_ss 484 [xnum_to_def,LENGTH_def,GT_xnum_num_def,RESTN_FINITE,LENGTH_def, 485 FinitePSLPathTheory.LENGTH_RESTN,LENGTH_RESTN_INFINITE,LS] 486 THEN Q.EXISTS_TAC `k` 487 THEN RW_TAC arith_ss [FinitePSLPathTheory.LENGTH_RESTN,GSYM RESTN_FINITE] 488 THEN PROVE_TAC[LENGTH_def,LS]); 489 490(****************************************************************************** 491* Eventually: F f (equation) 492* N.B. Probably can simplify proof to avoid cases on v, as in UF_SEM_F_G 493******************************************************************************) 494val UF_SEM_F_F = 495 store_thm 496 ("UF_SEM_F_F", 497 ``UF_SEM v (F_F f) = 498 ?i :: LESS(LENGTH v). 499 UF_SEM (RESTN v i) f 500 /\ 501 !j :: LESS i. (ELEM v j = BOTTOM) ==> (LENGTH v = XNUM j)``, 502 RW_TAC (arith_ss ++ resq_SS) [UF_SEM_def,F_F_def,B_SEM_def] 503 THEN Cases_on `v` 504 THEN RW_TAC arith_ss 505 [xnum_to_def,LENGTH_def,GT_xnum_num_def,RESTN_FINITE,LENGTH_def, 506 FinitePSLPathTheory.LENGTH_RESTN,LENGTH_RESTN_INFINITE] 507 THEN EQ_TAC 508 THEN RW_TAC arith_ss [] 509 THENL 510 [Q.EXISTS_TAC `k` 511 THEN RW_TAC arith_ss [] 512 THEN RES_TAC 513 THEN FULL_SIMP_TAC list_ss [LS,GSYM RESTN_FINITE,ELEM_RESTN] 514 THEN `j <= LENGTH l` by DECIDE_TAC 515 THEN IMP_RES_TAC LIST_LENGTH_RESTN_0 516 THEN TRY DECIDE_TAC >- fs [] 517 THEN PROVE_TAC[B_SEM_def], 518 Q.EXISTS_TAC `i` 519 THEN RW_TAC arith_ss [] 520 THEN RES_TAC 521 THEN FULL_SIMP_TAC list_ss [LS,GSYM RESTN_FINITE,ELEM_RESTN] 522 THEN `j <= LENGTH l` by DECIDE_TAC 523 THEN IMP_RES_TAC LIST_LENGTH_RESTN_0 524 THEN RW_TAC std_ss [] 525 THEN Cases_on `LENGTH l = j` (* 2 subgoals *) 526 THEN RW_TAC std_ss [] >- fs [] 527 THEN `~(ELEM (FINITE l) j = BOTTOM)` by PROVE_TAC[] 528 THEN Cases_on `ELEM (FINITE l) j` 529 THEN RW_TAC std_ss [B_SEM_def], 530 Q.EXISTS_TAC `k` 531 THEN RW_TAC arith_ss [] 532 THEN RES_TAC 533 THEN FULL_SIMP_TAC list_ss [ELEM_RESTN] 534 THEN Cases_on `ELEM (INFINITE f') j` 535 THEN RW_TAC std_ss [B_SEM_def] 536 THEN FULL_SIMP_TAC list_ss [B_SEM_def], 537 Q.EXISTS_TAC `i` 538 THEN RW_TAC arith_ss [] 539 THEN RES_TAC 540 THEN FULL_SIMP_TAC list_ss [ELEM_RESTN] 541 THEN Cases_on `ELEM (INFINITE f') j` 542 THEN RW_TAC std_ss [B_SEM_def]]); 543 544(****************************************************************************** 545* Globally: G f 546******************************************************************************) 547val UF_SEM_F_G_LEMMA = 548 SIMP_CONV (arith_ss ++ resq_SS) 549 [F_G_def,UF_SEM_def,UF_SEM_F_F,LENGTH_COMPLEMENT, 550 DECIDE ``~A \/ B \/ C = A ==> (B \/ C)``] 551 ``UF_SEM v (F_G f)``; 552 553val UF_SEM_F_G = 554 store_thm 555 ("UF_SEM_F_G", 556 ``UF_SEM v (F_G f) = 557 !i :: LESS(LENGTH v). 558 UF_SEM (RESTN v i) f 559 \/ 560 ?j :: LESS i. (ELEM v j = TOP) /\ ~(LENGTH v = XNUM j)``, 561 RW_TAC (arith_ss ++ resq_SS) [UF_SEM_F_G_LEMMA] 562 THEN EQ_TAC 563 THEN RW_TAC arith_ss [] 564 THEN RES_TAC 565 THENL 566 [IMP_RES_TAC RESTN_COMPLEMENT 567 THEN PROVE_TAC[COMPLEMENT_COMPLEMENT], 568 DISJ2_TAC 569 THEN Q.EXISTS_TAC `j` 570 THEN RW_TAC arith_ss [] 571 THEN `j < LENGTH v` by PROVE_TAC[LS_TRANS_X] 572 THEN IMP_RES_TAC ELEM_COMPLEMENT 573 THEN `COMPLEMENT_LETTER (ELEM v j) = BOTTOM` by PROVE_TAC[] 574 THEN POP_ASSUM(fn th => ASSUME_TAC(AP_TERM ``COMPLEMENT_LETTER`` th)) 575 THEN FULL_SIMP_TAC std_ss 576 [COMPLEMENT_LETTER_COMPLEMENT_LETTER,COMPLEMENT_LETTER_def], 577 IMP_RES_TAC RESTN_COMPLEMENT 578 THEN PROVE_TAC[COMPLEMENT_COMPLEMENT], 579 DISJ2_TAC 580 THEN Q.EXISTS_TAC `j` 581 THEN RW_TAC arith_ss [] 582 THEN `j < LENGTH v` by PROVE_TAC[LS_TRANS_X] 583 THEN IMP_RES_TAC ELEM_COMPLEMENT 584 THEN RW_TAC std_ss [COMPLEMENT_LETTER_def]]); 585 586(****************************************************************************** 587* Unclocked semantics of [!c W (c /\ f)] 588******************************************************************************) 589val UF_SEM_F_W_CLOCK_LEMMA = 590 SIMP_CONV (arith_ss ++ resq_SS) 591 [UF_SEM_F_G,UF_SEM_def,F_W_CLOCK_def,F_W_def,GSYM F_U_CLOCK_def, 592 UF_SEM_F_OR,ELEM_RESTN] 593 ``UF_SEM v (F_W_CLOCK c f)``; 594 595val UF_SEM_F_W_CLOCK = 596 store_thm 597 ("UF_SEM_F_W_CLOCK", 598 ``UF_SEM v (F_W_CLOCK c f) = 599 UF_SEM v (F_U_CLOCK c f) 600 \/ 601 !i :: LESS(LENGTH v). 602 B_SEM (ELEM v i) (B_NOT c) \/ ?j :: LESS i. ELEM v j = TOP``, 603 RW_TAC (arith_ss ++ resq_SS) 604 [F_W_CLOCK_def,UF_SEM_def,UF_SEM_F_W_CLOCK_LEMMA] 605 THEN EQ_TAC 606 THEN ZAP_TAC std_ss [] 607 THEN RW_TAC std_ss [] 608 THEN DISJ2_TAC 609 THEN RW_TAC std_ss [] 610 THEN RES_TAC 611 THEN ZAP_TAC std_ss [] 612 THENL 613 [IMP_RES_TAC LS_LE_X 614 THEN IMP_RES_TAC PATH_LENGTH_RESTN_0 615 THEN RW_TAC std_ss [] 616 THEN FULL_SIMP_TAC list_ss [LS], 617 DISJ2_TAC 618 THEN Q.EXISTS_TAC `j` 619 THEN RW_TAC std_ss [] 620 THEN Cases_on `LENGTH v = XNUM j` 621 THEN RW_TAC std_ss [] 622 THEN IMP_RES_TAC LS_TRANS_X 623 THEN `j < XNUM j` by PROVE_TAC[] 624 THEN FULL_SIMP_TAC list_ss [LS]]); 625 626local 627 628val AUX_TAC1 = 629 Q.EXISTS_TAC `j` 630 THEN RW_TAC arith_ss [ELEM_RESTN] 631 THEN IMP_RES_TAC LS_LE_X 632 THEN IMP_RES_TAC PATH_FINITE_LENGTH_RESTN_0 633 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS] 634 635in 636 637val F_STRONG_BOOL_CLOCK_COMP = 638 store_thm 639 ("F_STRONG_BOOL_CLOCK_COMP", 640 ``!b v c. F_SEM v c (F_STRONG_BOOL b) = 641 UF_SEM v (F_CLOCK_COMP c (F_STRONG_BOOL b))``, 642 RW_TAC (arith_ss ++ resq_SS) 643 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,UF_SEM_F_U_CLOCK, 644 CLOCK_TICK_def,LENGTH_SEL,ELEM_EL] 645 THEN EQ_TAC 646 THEN RW_TAC std_ss [] 647 THENL 648 [Q.EXISTS_TAC `j` 649 THEN RW_TAC arith_ss [ELEM_RESTN] 650 THENL 651 [`0 <= j /\ j <= j` by DECIDE_TAC 652 THEN IMP_RES_TAC 653 (INST_TYPE[{redex=``:'a``, residue=``:'a letter``}]EL_SEL) 654 THEN FULL_SIMP_TAC arith_ss [], 655 RES_TAC 656 THEN `0 <= i /\ i <= j` by DECIDE_TAC 657 THEN IMP_RES_TAC 658 (INST_TYPE[{redex=``:'a``, residue=``:'a letter``}]EL_SEL) 659 THEN FULL_SIMP_TAC arith_ss []], 660 AUX_TAC1, 661 AUX_TAC1, 662 AUX_TAC1, 663 Q.EXISTS_TAC `j` 664 THEN FULL_SIMP_TAC arith_ss [ELEM_RESTN] 665 THEN `0 <= j /\ j <= j` by DECIDE_TAC 666 THEN IMP_RES_TAC 667 (INST_TYPE[{redex=``:'a``, residue=``:'a letter``}]EL_SEL) 668 THEN FULL_SIMP_TAC arith_ss [ELEM_EL] 669 THEN RW_TAC std_ss [] 670 THEN `0 <= i /\ i <= j` by DECIDE_TAC 671 THEN IMP_RES_TAC 672 (INST_TYPE[{redex=``:'a``, residue=``:'a letter``}]EL_SEL) 673 THEN FULL_SIMP_TAC arith_ss [ELEM_EL]]) 674 675end; 676 677(* 678val th = 679 SIMP_CONV 680 (list_ss ++ resq_SS) 681 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,UF_SEM_F_U_CLOCK,CLOCK_TICK_def, 682 F_W_CLOCK_def,ELEM_RESTN,UF_SEM_def,CLOCK_TICK_def,LENGTH_SEL, 683 F_W_def,F_F_def,F_G_def,UF_SEM_F_OR,UF_SEM_F_U_CLOCK,LENGTH_COMPLEMENT, 684 ELEM_EL,RESTN_def,RESTN_FINITE,ELEM_def,COMPLEMENT_def,LS, 685 DECIDE ``m < 1 = (m=0)``, DECIDE ``m < 2 = (m=0) \/ (m=1)``, 686 COMPLEMENT_LETTER_def,FinitePSLPathTheory.RESTN_def, 687 HEAD_def,B_SEM_def,xnum_11,HD_SEL] 688 ``F_SEM (FINITE[BOTTOM]) c (F_WEAK_BOOL b) = 689 UF_SEM (FINITE[BOTTOM]) (F_CLOCK_COMP c (F_WEAK_BOOL b))``; 690*) 691 692val WOP_EQ = 693 prove 694 (``!P. (?n:num. P n) = ?n. P n /\ !m. m < n ==> ~P m``, 695 PROVE_TAC[WOP]); 696 697val WOP_IMP = 698 prove 699 (``!P n. P(n:num) ==> ?n. P n /\ !m. m < n ==> ~P m``, 700 PROVE_TAC[WOP]); 701 702 703(* 704Lemma below is one of the most messy proofs I've ever done! There is 705a frequented repeated well-foundedness argument, that occurrs several 706times inlined, which needs to be extracted into a lemma. 707*) 708 709val EL_SEL_LEMMA1 = 710 SIMP_RULE arith_ss [] (SPECL[``0``,``j:num``, ``j:num``]EL_SEL); 711 712val EL_SEL_LEMMA2 = 713 SIMP_RULE arith_ss [] (SPECL[``0``,``i:num``, ``j:num``]EL_SEL); 714 715val F_WEAK_BOOL_CLOCK_COMP_IMP1 = 716 store_thm 717 ("F_WEAK_BOOL_CLOCK_COMP_IMP1", 718 ``!b v c. F_SEM v c (F_WEAK_BOOL b) ==> 719 UF_SEM v (F_CLOCK_COMP c (F_WEAK_BOOL b))``, 720 SIMP_TAC (arith_ss ++ resq_SS) [F_SEM_def] 721 THEN SIMP_TAC (list_ss ++ resq_SS) 722 [CLOCK_TICK_def,LENGTH_SEL,ELEM_EL, 723 EL_SEL_LEMMA1,EL_SEL_LEMMA2] 724 THEN SIMP_TAC (list_ss ++ resq_SS) 725 [F_CLOCK_COMP_def,UF_SEM_F_W_CLOCK,UF_SEM_F_U_CLOCK,UF_SEM_F_AND] 726 THEN ONCE_REWRITE_TAC 727 [DECIDE ``A /\ (B /\ C) /\ D = A /\ ((A /\ B) /\ (A /\ C)) /\ D``] 728 THEN SIMP_TAC (list_ss ++ resq_SS) 729 [UF_SEM_RESTN_F_WEAK_BOOL_COR] 730 THEN ONCE_REWRITE_TAC 731 [DECIDE ``A /\ ((A /\ B) /\ (A /\ C)) /\ D = A /\ B /\ C /\ D``] 732 THEN RW_TAC std_ss [] 733 THEN Cases_on 734 `?j. j < LENGTH v /\ 735 B_SEM (ELEM (COMPLEMENT v) j) c /\ 736 (!i. i < j ==> B_SEM (ELEM (COMPLEMENT v) i) (B_NOT c))` 737 THENL 738 [POP_ASSUM STRIP_ASSUME_TAC 739 THEN RES_TAC 740 THEN Cases_on 741 `!i. i < LENGTH v ==> 742 B_SEM (ELEM v i) (B_NOT c) \/ ?j. j < i /\ (ELEM v j = TOP)` 743 THEN RW_TAC std_ss [] 744 THEN FULL_SIMP_TAC std_ss [NOT_FORALL_THM,DECIDE``~A \/ B = A ==> B``] 745 THEN Q.EXISTS_TAC `j` 746 THEN RW_TAC std_ss [] 747 THENL 748 [Cases_on `ELEM v j` 749 THEN FULL_SIMP_TAC std_ss [B_SEM_def,COMPLEMENT_LETTER_def] 750 THEN IMP_RES_TAC ELEM_COMPLEMENT 751 THEN PROVE_TAC[COMPLEMENT_LETTER_def], 752 `i' < LENGTH v` by PROVE_TAC[LS_TRANS_X] 753 THEN RES_TAC 754 THEN Cases_on `ELEM v i'` 755 THEN FULL_SIMP_TAC std_ss [B_SEM_def,COMPLEMENT_LETTER_def] 756 THEN IMP_RES_TAC ELEM_COMPLEMENT 757 THENL 758 [`ELEM (COMPLEMENT v) i' = TOP` 759 by PROVE_TAC[COMPLEMENT_LETTER_def] 760 THEN ASSUM_LIST(fn thl => FULL_SIMP_TAC std_ss [el 1 thl]) 761 THEN `B_SEM (COMPLEMENT_LETTER BOTTOM) c` by 762 SIMP_TAC std_ss [B_SEM_def,COMPLEMENT_LETTER_def] 763 THEN `?i''. i'' < i' /\ ~B_SEM (ELEM (COMPLEMENT v) i'') (B_NOT c)` 764 by PROVE_TAC[] 765 THEN `i'' < j` by DECIDE_TAC 766 THEN PROVE_TAC[], 767 `B_SEM (STATE f) (B_NOT c)` by PROVE_TAC[COMPLEMENT_LETTER_def] 768 THEN FULL_SIMP_TAC std_ss [B_SEM_def]]], 769 FULL_SIMP_TAC std_ss [NOT_EXISTS_THM] 770 THEN FULL_SIMP_TAC std_ss 771 [DECIDE ``~A \/ ~B \/ C = A ==> B ==> C``] 772 THEN DISJ2_TAC 773 THEN RW_TAC std_ss [] 774 THEN Cases_on `?j. j < i /\ (ELEM v j = TOP)` 775 THEN RW_TAC std_ss [] 776 THEN FULL_SIMP_TAC std_ss [NOT_EXISTS_THM,DECIDE ``~A \/ B = A ==> B``] 777 THEN Cases_on `B_SEM (ELEM v i) (B_NOT c)` 778 THEN RW_TAC std_ss [] 779 THEN Cases_on `ELEM v i` 780 THEN RW_TAC std_ss [] 781 THENL 782 [POP_ASSUM(fn th => FULL_SIMP_TAC std_ss [th,B_SEM_def]), 783 ASSUM_LIST 784 (fn thl => 785 STRIP_ASSUME_TAC 786 (SIMP_RULE std_ss 787 [el 1 thl,el 4 thl,ELEM_COMPLEMENT,COMPLEMENT_LETTER_def,B_SEM_def] 788 (Q.SPEC `i` (el 5 thl)))) 789 THEN `i' < LENGTH v` by PROVE_TAC [LS_TRANS_X] 790 THEN Cases_on `ELEM v i'` 791 THEN RW_TAC std_ss [] 792 THENL 793 [RES_TAC, 794 IMP_RES_TAC ELEM_COMPLEMENT 795 THEN ASSUM_LIST 796 (fn thl => 797 STRIP_ASSUME_TAC 798 (SIMP_RULE std_ss 799 [el 2 thl,el 3 thl,ELEM_COMPLEMENT, 800 COMPLEMENT_LETTER_def,B_SEM_def] 801 (el 5 thl))), 802 POP_ASSUM 803 (fn th => 804 ASSUME_TAC 805 (EXISTS(mk_exists(``f:'a -> bool``,concl th),``f:'a -> bool``)th)) 806 THEN ASSUM_LIST 807 (fn thl => 808 ASSUME_TAC 809 (LIST_CONJ[el 1 thl,el 3 thl,el 4 thl])) 810 THEN POP_ASSUM 811 (fn th => 812 STRIP_ASSUME_TAC 813 (MP 814 (BETA_RULE 815 (ISPECL[mk_abs(``i':num``,concl th),``i':num``]WOP_IMP)) 816 th)) 817 THEN `n < LENGTH v` by PROVE_TAC [LS_TRANS_X] 818 THEN `ELEM (COMPLEMENT v) n = STATE f` 819 by PROVE_TAC[ELEM_COMPLEMENT,COMPLEMENT_LETTER_def] 820 THEN ASSUM_LIST 821 (fn thl => 822 ASSUME_TAC(SIMP_RULE std_ss [el 1 thl,B_SEM_def](el 5 thl))) 823 THEN `B_SEM (ELEM (COMPLEMENT v) n) c` by PROVE_TAC[] 824 THEN ASSUM_LIST 825 (fn thl => 826 STRIP_ASSUME_TAC 827 (SIMP_RULE std_ss [el 1 thl,el 4 thl](Q.SPEC `n` (el 17 thl)))) 828 THEN `i'' < i` by DECIDE_TAC 829 THEN Cases_on `ELEM v i''` 830 THEN RW_TAC std_ss [] 831 THENL 832 [RES_TAC, 833 `i'' < LENGTH v` by PROVE_TAC [LS_TRANS_X] 834 THEN IMP_RES_TAC ELEM_COMPLEMENT 835 THEN ASSUM_LIST 836 (fn thl => 837 STRIP_ASSUME_TAC 838 (SIMP_RULE std_ss 839 [el 4 thl,el 7 thl,ELEM_COMPLEMENT, 840 COMPLEMENT_LETTER_def,B_SEM_def] 841 (el 9 thl))), 842 RES_TAC]], 843 `B_SEM (ELEM v i) c` by PROVE_TAC[B_SEM_def] 844 THEN `B_SEM (ELEM (COMPLEMENT v) i) c` 845 by PROVE_TAC[ELEM_COMPLEMENT,COMPLEMENT_LETTER_def] 846 THEN ASSUM_LIST 847 (fn thl => 848 STRIP_ASSUME_TAC(SIMP_RULE std_ss 849 [el 1 thl,el 6 thl](Q.SPEC `i` (el 7 thl)))) 850 THEN Cases_on `ELEM v i'` 851 THEN RW_TAC std_ss [] 852 THENL 853 [RES_TAC, 854 `i' < LENGTH v` by PROVE_TAC [LS_TRANS_X] 855 THEN IMP_RES_TAC ELEM_COMPLEMENT 856 THEN ASSUM_LIST 857 (fn thl => 858 STRIP_ASSUME_TAC 859 (SIMP_RULE std_ss 860 [el 2 thl,el 4 thl, 861 COMPLEMENT_LETTER_def,B_SEM_def] 862 (el 5 thl))), 863 `i' < LENGTH v` by PROVE_TAC[LS_TRANS_X] 864 THEN `ELEM (COMPLEMENT v) i' = STATE f'` 865 by PROVE_TAC[ELEM_COMPLEMENT,COMPLEMENT_LETTER_def] 866 THEN ASSUM_LIST 867 (fn thl => 868 ASSUME_TAC 869 (EXISTS 870 (mk_exists 871 (``f':'a -> bool``,concl(el 1 thl)),``f':'a -> bool``)(el 1 thl))) 872 THEN ASSUM_LIST 873 (fn thl => 874 ASSUME_TAC 875 (LIST_CONJ[el 1 thl,el 5 thl,el 6 thl])) 876 THEN POP_ASSUM 877 (fn th => 878 STRIP_ASSUME_TAC 879 (MP 880 (BETA_RULE 881 (ISPECL[mk_abs(``i':num``,concl th),``i':num``]WOP_IMP)) 882 th)) 883 THEN `n < LENGTH v` by PROVE_TAC[LS_TRANS_X] 884 THEN Cases_on `ELEM v n` 885 THEN RW_TAC std_ss [] 886 THENL 887 [RES_TAC, 888 IMP_RES_TAC ELEM_COMPLEMENT 889 THEN ASSUM_LIST 890 (fn thl => 891 STRIP_ASSUME_TAC 892 (SIMP_RULE std_ss 893 [el 3 thl,el 5 thl, 894 COMPLEMENT_LETTER_def,B_SEM_def] 895 (el 9 thl))), 896 IMP_RES_TAC ELEM_COMPLEMENT 897 THEN ASSUM_LIST 898 (fn thl => 899 STRIP_ASSUME_TAC 900 (SIMP_RULE std_ss 901 [el 3 thl,el 5 thl, 902 COMPLEMENT_LETTER_def,B_SEM_def] 903 (el 9 thl))) 904 THEN `B_SEM (ELEM (COMPLEMENT v) n) c` by PROVE_TAC[COMPLEMENT_LETTER_def] 905 THEN ASSUM_LIST 906 (fn thl => 907 STRIP_ASSUME_TAC(SIMP_RULE std_ss 908 [el 1 thl,el 8 thl](Q.SPEC `n` (el 24 thl)))) 909 THEN `i'' < i` by DECIDE_TAC 910 THEN ASSUM_LIST 911 (fn thl => 912 STRIP_ASSUME_TAC(SIMP_RULE std_ss 913 [el 2 thl,el 3 thl,el 11 thl](Q.SPEC `i''` (el 12 thl)))) 914 THEN Cases_on `ELEM v i''` 915 THEN RW_TAC std_ss [] 916 THENL 917 [RES_TAC, 918 `i'' < LENGTH v` by PROVE_TAC [LS_TRANS_X] 919 THEN IMP_RES_TAC ELEM_COMPLEMENT 920 THEN ASSUM_LIST 921 (fn thl => 922 STRIP_ASSUME_TAC 923 (SIMP_RULE std_ss 924 [el 1 thl,el 3 thl, 925 COMPLEMENT_LETTER_def,B_SEM_def] 926 (el 6 thl))), 927 `i'' < LENGTH v` by PROVE_TAC [LS_TRANS_X] 928 THEN IMP_RES_TAC ELEM_COMPLEMENT 929 THEN `ELEM (COMPLEMENT v) i'' = STATE f'''''` 930 by PROVE_TAC[COMPLEMENT_LETTER_def] 931 THEN RES_TAC]]]]]); 932 933val F_WEAK_BOOL_CLOCK_COMP_IMP2 = 934 store_thm 935 ("F_WEAK_BOOL_CLOCK_COMP_IMP2", 936 ``!b v c. UF_SEM v (F_CLOCK_COMP c (F_WEAK_BOOL b)) ==> 937 F_SEM v c (F_WEAK_BOOL b)``, 938 SIMP_TAC (arith_ss ++ resq_SS) [F_SEM_def] 939 THEN SIMP_TAC (list_ss ++ resq_SS) 940 [CLOCK_TICK_def,LENGTH_SEL,ELEM_EL, 941 EL_SEL_LEMMA1,EL_SEL_LEMMA2] 942 THEN SIMP_TAC (list_ss ++ resq_SS) 943 [F_CLOCK_COMP_def,UF_SEM_F_W_CLOCK,UF_SEM_F_U_CLOCK,UF_SEM_F_AND] 944 THEN ONCE_REWRITE_TAC 945 [DECIDE ``A /\ (B /\ C) /\ D = A /\ ((A /\ B) /\ (A /\ C)) /\ D``] 946 THEN SIMP_TAC (list_ss ++ resq_SS) 947 [UF_SEM_RESTN_F_WEAK_BOOL_COR] 948 THEN ONCE_REWRITE_TAC 949 [DECIDE ``A /\ ((A /\ B) /\ (A /\ C)) /\ D = A /\ B /\ C /\ D``] 950 THEN RW_TAC std_ss [] 951 THENL 952 [Cases_on `j:num = j'` 953 THEN RW_TAC std_ss [] 954 THEN `j < j' \/ j' < j` by DECIDE_TAC 955 THEN RES_TAC 956 THENL 957 [Cases_on `ELEM v j` 958 THEN RW_TAC std_ss [] 959 THENL 960 [IMP_RES_TAC ELEM_COMPLEMENT 961 THEN `ELEM (COMPLEMENT v) j = BOTTOM` by PROVE_TAC[COMPLEMENT_LETTER_def] 962 THEN PROVE_TAC[B_SEM_def], 963 IMP_RES_TAC ELEM_COMPLEMENT 964 THEN `ELEM (COMPLEMENT v) j = TOP` by PROVE_TAC[COMPLEMENT_LETTER_def] 965 THEN PROVE_TAC[B_SEM_def], 966 IMP_RES_TAC ELEM_COMPLEMENT 967 THEN `ELEM (COMPLEMENT v) j = STATE f` by PROVE_TAC[COMPLEMENT_LETTER_def] 968 THEN PROVE_TAC[B_SEM_def]], 969 Cases_on `ELEM v j'` 970 THEN RW_TAC std_ss [] 971 THENL 972 [IMP_RES_TAC ELEM_COMPLEMENT 973 THEN `ELEM (COMPLEMENT v) j' = BOTTOM` by PROVE_TAC[COMPLEMENT_LETTER_def] 974 THEN PROVE_TAC[B_SEM_def], 975 IMP_RES_TAC ELEM_COMPLEMENT 976 THEN `ELEM (COMPLEMENT v) j' = TOP` by PROVE_TAC[COMPLEMENT_LETTER_def] 977 THEN PROVE_TAC[B_SEM_def], 978 IMP_RES_TAC ELEM_COMPLEMENT 979 THEN `ELEM (COMPLEMENT v) j' = STATE f` by PROVE_TAC[COMPLEMENT_LETTER_def] 980 THEN PROVE_TAC[B_SEM_def]]], 981 RES_TAC 982 THENL 983 [Cases_on `ELEM v j` 984 THEN RW_TAC std_ss [] 985 THENL 986 [IMP_RES_TAC ELEM_COMPLEMENT 987 THEN `ELEM (COMPLEMENT v) j = BOTTOM` by PROVE_TAC[COMPLEMENT_LETTER_def] 988 THEN PROVE_TAC[B_SEM_def], 989 IMP_RES_TAC ELEM_COMPLEMENT 990 THEN `ELEM (COMPLEMENT v) j = TOP` by PROVE_TAC[COMPLEMENT_LETTER_def] 991 THEN PROVE_TAC[B_SEM_def], 992 IMP_RES_TAC ELEM_COMPLEMENT 993 THEN `ELEM (COMPLEMENT v) j = STATE f` by PROVE_TAC[COMPLEMENT_LETTER_def] 994 THEN PROVE_TAC[B_SEM_def]], 995 `B_SEM (ELEM (COMPLEMENT v) j') (B_NOT c)` by PROVE_TAC[] 996 THEN `j' < LENGTH v` by PROVE_TAC[LS_TRANS_X] 997 THEN IMP_RES_TAC ELEM_COMPLEMENT 998 THEN `ELEM (COMPLEMENT v) j' = BOTTOM` by PROVE_TAC[COMPLEMENT_LETTER_def] 999 THEN PROVE_TAC[B_SEM_def]]]); 1000 1001val F_WEAK_BOOL_CLOCK_COMP = 1002 store_thm 1003 ("F_WEAK_BOOL_CLOCK_COMP", 1004 ``!b v c. F_SEM v c (F_WEAK_BOOL b) = 1005 UF_SEM v (F_CLOCK_COMP c (F_WEAK_BOOL b))``, 1006 PROVE_TAC 1007 [F_WEAK_BOOL_CLOCK_COMP_IMP1,F_WEAK_BOOL_CLOCK_COMP_IMP2]); 1008 1009val EL_SEL_THM = 1010 store_thm 1011 ("EL_SEL_THM", 1012 ``!p. i + n <= j ==> (EL n (SEL p (i,j)) = ELEM p (i + n))``, 1013 PROVE_TAC[SIMP_RULE arith_ss [] (Q.SPECL[`i`,`n+i`,`j`]EL_SEL)]); 1014 1015val F_NEXT_CLOCK_COMP_IMP1 = 1016 store_thm 1017 ("F_NEXT_CLOCK_COMP_IMP1", 1018 ``!f. 1019 (!v c. 1020 F_SEM v c f = UF_SEM v (F_CLOCK_COMP c f)) 1021 ==> 1022 !v c. 1023 F_SEM v c (F_NEXT f) ==> UF_SEM v (F_CLOCK_COMP c (F_NEXT f))``, 1024 SIMP_TAC (arith_ss++resq_SS) 1025 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,CLOCK_TICK_def] 1026 THEN SIMP_TAC (arith_ss++resq_SS) 1027 [UF_SEM_F_U_CLOCK,RESTN_RESTN,LENGTH_SEL,UF_SEM_F_AND, 1028 EL_SEL_LEMMA1,EL_SEL_LEMMA2,ELEM_EL] 1029 THEN ONCE_REWRITE_TAC 1030 [DECIDE ``A /\ (B /\ C) /\ D = A /\ ((A /\ B) /\ (A /\ C)) /\ D``] 1031 THEN SIMP_TAC (list_ss ++ resq_SS) 1032 [UF_SEM_RESTN_F_WEAK_BOOL_COR] 1033 THEN ONCE_REWRITE_TAC 1034 [DECIDE ``A /\ ((A /\ B) /\ (A /\ C)) /\ D = A /\ B /\ C /\ D``] 1035 THEN SIMP_TAC (arith_ss++resq_SS) 1036 [UF_SEM_def,RESTN_RESTN,UF_SEM_F_U_CLOCK] 1037 THEN RW_TAC std_ss [] 1038 THEN Q.EXISTS_TAC `j` 1039 THEN RW_TAC list_ss [] 1040 THENL 1041 [Cases_on `v` 1042 THEN RW_TAC list_ss 1043 [GT,LENGTH_RESTN_INFINITE, 1044 IS_FINITE_def,LENGTH_RESTN,LENGTH_def,SUB] 1045 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS], 1046 RW_TAC list_ss [ELEM_RESTN] 1047 THEN `(j + 1) + (k - (j + 1)) <= k` by DECIDE_TAC 1048 THEN IMP_RES_TAC(ISPEC ``v :'a letter path`` EL_SEL_THM) 1049 THEN `j + 1 + (k - (j + 1)) = k` by DECIDE_TAC 1050 THEN `B_SEM (ELEM v k) c` by PROVE_TAC[] 1051 THEN `j + 1 <= k` by DECIDE_TAC 1052 THEN Q.EXISTS_TAC `k - (j + 1)` 1053 THEN RW_TAC list_ss [] 1054 THENL 1055 [Cases_on `v` 1056 THEN RW_TAC list_ss 1057 [GT,LENGTH_RESTN_INFINITE,RESTN_FINITE, 1058 IS_FINITE_def,LENGTH_RESTN,LENGTH_def,SUB] 1059 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS] 1060 THEN RW_TAC list_ss [FinitePSLPathTheory.LENGTH_RESTN], 1061 `(j + 1) + i <= k` by DECIDE_TAC 1062 THEN RES_TAC 1063 THEN `i + (j + 1) = (j + 1) + i` by DECIDE_TAC 1064 THEN PROVE_TAC[EL_SEL_THM]]]); 1065 1066val F_NEXT_CLOCK_COMP_IMP2 = 1067 store_thm 1068 ("F_NEXT_CLOCK_COMP_IMP2", 1069 ``!f. (!v c. F_SEM v c f = UF_SEM v (F_CLOCK_COMP c f)) 1070 ==> 1071 !v c. UF_SEM v (F_CLOCK_COMP c (F_NEXT f)) ==> F_SEM v c (F_NEXT f)``, 1072 SIMP_TAC (arith_ss++resq_SS) 1073 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,CLOCK_TICK_def] 1074 THEN SIMP_TAC (arith_ss++resq_SS) 1075 [UF_SEM_F_U_CLOCK,RESTN_RESTN,LENGTH_SEL,UF_SEM_F_AND, 1076 EL_SEL_LEMMA1,EL_SEL_LEMMA2,ELEM_EL] 1077 THEN ONCE_REWRITE_TAC 1078 [DECIDE ``A /\ (B /\ C) /\ D = A /\ ((A /\ B) /\ (A /\ C)) /\ D``] 1079 THEN SIMP_TAC (list_ss ++ resq_SS) 1080 [UF_SEM_RESTN_F_WEAK_BOOL_COR] 1081 THEN ONCE_REWRITE_TAC 1082 [DECIDE ``A /\ ((A /\ B) /\ (A /\ C)) /\ D = A /\ B /\ C /\ D``] 1083 THEN SIMP_TAC (arith_ss++resq_SS) 1084 [UF_SEM_def,RESTN_RESTN,UF_SEM_F_U_CLOCK] 1085 THEN RW_TAC std_ss [] 1086 THENL 1087 [Q.EXISTS_TAC `j` 1088 THEN RW_TAC list_ss [] 1089 THEN Q.EXISTS_TAC `j + (j' + 1)` 1090 THEN STRONG_CONJ_TAC THEN RW_TAC list_ss [] 1091 THENL 1092 [Cases_on `v` 1093 THEN RW_TAC list_ss 1094 [GT,LENGTH_RESTN_INFINITE,RESTN_FINITE, 1095 IS_FINITE_def,LENGTH_RESTN,LENGTH_def,SUB] 1096 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS,RESTN_FINITE,xnum_11,GT] 1097 THEN `LENGTH(RESTN l j) = LENGTH l - j` 1098 by PROVE_TAC[FinitePSLPathTheory.LENGTH_RESTN] 1099 THEN `j + 1 < LENGTH l` by DECIDE_TAC 1100 THEN `LENGTH(RESTN l (j + 1)) = LENGTH l - (j + 1)` 1101 by PROVE_TAC[FinitePSLPathTheory.LENGTH_RESTN] 1102 THEN DECIDE_TAC, 1103 RW_TAC list_ss [EL_SEL_THM] 1104 THEN `?l. (LENGTH l = j + (j' + 1)) /\ (v = FINITE l)` 1105 by PROVE_TAC[PATH_FINITE_LENGTH_RESTN_0_COR] 1106 THEN RW_TAC std_ss [] 1107 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS], 1108 RW_TAC list_ss [EL_SEL_THM] 1109 THEN `?l. (LENGTH l = j + (j' + 1)) /\ (v = FINITE l)` 1110 by PROVE_TAC[PATH_FINITE_LENGTH_RESTN_0_COR] 1111 THEN RW_TAC std_ss [] 1112 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS]], 1113 Q.EXISTS_TAC `j` 1114 THEN RW_TAC list_ss [] 1115 THEN Q.EXISTS_TAC `j + (j' + 1)` 1116 THEN RW_TAC list_ss [] 1117 THENL 1118 [Cases_on `v` 1119 THEN RW_TAC list_ss 1120 [GT,LENGTH_RESTN_INFINITE,RESTN_FINITE, 1121 IS_FINITE_def,LENGTH_RESTN,LENGTH_def,SUB] 1122 THEN FULL_SIMP_TAC list_ss [LENGTH_def,LS,RESTN_FINITE,xnum_11,GT] 1123 THEN `LENGTH(RESTN l j) = LENGTH l - j` 1124 by PROVE_TAC[FinitePSLPathTheory.LENGTH_RESTN] 1125 THEN `j + 1 < LENGTH l` by DECIDE_TAC 1126 THEN `LENGTH(RESTN l (j + 1)) = LENGTH l - (j + 1)` 1127 by PROVE_TAC[FinitePSLPathTheory.LENGTH_RESTN] 1128 THEN DECIDE_TAC, 1129 FULL_SIMP_TAC list_ss [ELEM_RESTN] 1130 THEN RW_TAC list_ss [EL_SEL_THM], 1131 FULL_SIMP_TAC list_ss [ELEM_RESTN] 1132 THEN RW_TAC list_ss [EL_SEL_THM]]]); 1133 1134val F_NEXT_CLOCK_COMP = 1135 store_thm 1136 ("F_NEXT_CLOCK_COMP", 1137 ``!f. (!v c. F_SEM v c f = UF_SEM v (F_CLOCK_COMP c f)) ==> 1138 !v c. F_SEM v c (F_NEXT f) = 1139 UF_SEM v (F_CLOCK_COMP c (F_NEXT f))``, 1140 PROVE_TAC[F_NEXT_CLOCK_COMP_IMP1,F_NEXT_CLOCK_COMP_IMP2]); 1141 1142val F_UNTIL_CLOCK_COMP_IMP1 = 1143 store_thm 1144 ("F_UNTIL_CLOCK_COMP_IMP1", 1145 ``!f1 f2. 1146 (!v c. F_SEM v c f1 = UF_SEM v (F_CLOCK_COMP c f1)) 1147 /\ 1148 (!v c. F_SEM v c f2 = UF_SEM v (F_CLOCK_COMP c f2)) 1149 ==> 1150 !v c. F_SEM v c (F_UNTIL(f1,f2)) 1151 ==> UF_SEM v (F_CLOCK_COMP c (F_UNTIL(f1,f2)))``, 1152 SIMP_TAC (arith_ss++resq_SS) 1153 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,CLOCK_TICK_def] 1154 THEN SIMP_TAC (arith_ss++resq_SS) 1155 [UF_SEM_F_U_CLOCK,RESTN_RESTN,LENGTH_SEL,UF_SEM_F_AND, 1156 EL_SEL_LEMMA1,EL_SEL_LEMMA2,ELEM_EL] 1157 THEN ONCE_REWRITE_TAC 1158 [DECIDE ``A /\ (B /\ C) /\ D = A /\ ((A /\ B) /\ (A /\ C)) /\ D``] 1159 THEN SIMP_TAC (list_ss ++ resq_SS) 1160 [UF_SEM_RESTN_F_WEAK_BOOL_COR] 1161 THEN ONCE_REWRITE_TAC 1162 [DECIDE ``A /\ ((A /\ B) /\ (A /\ C)) /\ D = A /\ B /\ C /\ D``] 1163 THEN SIMP_TAC (arith_ss++resq_SS) 1164 [UF_SEM_def,RESTN_RESTN,UF_SEM_F_U_CLOCK,ELEM_RESTN, 1165 UF_SEM_F_IMPLIES,LENGTH_COMPLEMENT] 1166 THEN RW_TAC std_ss [] 1167 THEN Q.EXISTS_TAC `k` 1168 THEN RW_TAC list_ss [] 1169 THEN `j < LENGTH v` by PROVE_TAC[LS_TRANS_X] 1170 THENL 1171 [IMP_RES_TAC PATH_FINITE_LENGTH_RESTN_0_COR 1172 THEN RW_TAC std_ss [] 1173 THEN FULL_SIMP_TAC arith_ss[LENGTH_def,LS], 1174 RES_TAC 1175 THEN IMP_RES_TAC RESTN_COMPLEMENT 1176 THEN `B_SEM (ELEM (RESTN (COMPLEMENT v) j) 0) c` 1177 by PROVE_TAC[] 1178 THEN FULL_SIMP_TAC arith_ss[ELEM_RESTN]]); 1179 1180val F_UNTIL_CLOCK_COMP_IMP2 = 1181 store_thm 1182 ("F_UNTIL_CLOCK_COMP_IMP2", 1183 ``!f1 f2. 1184 (!v c. F_SEM v c f1 = UF_SEM v (F_CLOCK_COMP c f1)) 1185 /\ 1186 (!v c. F_SEM v c f2 = UF_SEM v (F_CLOCK_COMP c f2)) 1187 ==> 1188 !v c. UF_SEM v (F_CLOCK_COMP c (F_UNTIL(f1,f2))) 1189 ==> F_SEM v c (F_UNTIL(f1,f2))``, 1190 SIMP_TAC (arith_ss++resq_SS) 1191 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,CLOCK_TICK_def] 1192 THEN SIMP_TAC (arith_ss++resq_SS) 1193 [UF_SEM_F_U_CLOCK,RESTN_RESTN,LENGTH_SEL,UF_SEM_F_AND, 1194 EL_SEL_LEMMA1,EL_SEL_LEMMA2,ELEM_EL] 1195 THEN ONCE_REWRITE_TAC 1196 [DECIDE ``A /\ (B /\ C) /\ D = A /\ ((A /\ B) /\ (A /\ C)) /\ D``] 1197 THEN SIMP_TAC (list_ss ++ resq_SS) 1198 [UF_SEM_RESTN_F_WEAK_BOOL_COR] 1199 THEN ONCE_REWRITE_TAC 1200 [DECIDE ``A /\ ((A /\ B) /\ (A /\ C)) /\ D = A /\ B /\ C /\ D``] 1201 THEN SIMP_TAC (arith_ss++resq_SS) 1202 [UF_SEM_def,RESTN_RESTN,UF_SEM_F_U_CLOCK,ELEM_RESTN, 1203 UF_SEM_F_IMPLIES,LENGTH_COMPLEMENT] 1204 THEN RW_TAC std_ss [] 1205 THEN Q.EXISTS_TAC `k` 1206 THEN RW_TAC list_ss [] 1207 THENL 1208 [IMP_RES_TAC PATH_FINITE_LENGTH_RESTN_0_COR 1209 THEN RW_TAC std_ss [] 1210 THEN FULL_SIMP_TAC arith_ss[LENGTH_def,LS], 1211 IMP_RES_TAC PATH_FINITE_LENGTH_RESTN_0_COR 1212 THEN RW_TAC std_ss [] 1213 THEN FULL_SIMP_TAC arith_ss[LENGTH_def,LS], 1214 1215 RES_TAC 1216 THEN `j < LENGTH v` by PROVE_TAC[LS_TRANS_X] 1217 THEN IMP_RES_TAC RESTN_COMPLEMENT 1218 THEN ASSUM_LIST 1219 (fn thl => 1220 ASSUME_TAC(SIMP_RULE arith_ss [GSYM(el 2 thl)] (el 5 thl))) 1221 THEN FULL_SIMP_TAC arith_ss[ELEM_RESTN]]); 1222 1223val F_UNTIL_CLOCK_COMP = 1224 store_thm 1225 ("F_UNTIL_CLOCK_COMP", 1226 ``!f1 f2. 1227 (!v c. F_SEM v c f1 = UF_SEM v (F_CLOCK_COMP c f1)) /\ 1228 (!v c. F_SEM v c f2 = UF_SEM v (F_CLOCK_COMP c f2)) 1229 ==> 1230 !v c. F_SEM v c (F_UNTIL(f1,f2)) = 1231 UF_SEM v (F_CLOCK_COMP c (F_UNTIL(f1,f2)))``, 1232 RW_TAC std_ss [] 1233 THEN EQ_TAC 1234 THEN RW_TAC std_ss [] 1235 THENL 1236 [IMP_RES_TAC F_UNTIL_CLOCK_COMP_IMP1, 1237 IMP_RES_TAC F_UNTIL_CLOCK_COMP_IMP2]); 1238 1239val AUX_TAC2 = 1240 RW_TAC (arith_ss ++ resq_SS) 1241 [F_SEM_def,UF_SEM_def,F_CLOCK_COMP_def,CLOCK_TICK_def]; 1242 1243val F_CLOCK_COMP_CORRECT = 1244 store_thm 1245 ("F_CLOCK_COMP_CORRECT", 1246 ``!f v c. F_SEM v c f = UF_SEM v (F_CLOCK_COMP c f)``, 1247 INDUCT_THEN fl_induct ASSUME_TAC 1248 THENL 1249 [(* F_STRONG_BOOL b *) 1250 RW_TAC std_ss [F_STRONG_BOOL_CLOCK_COMP], 1251 (* F_WEAK_BOOL b *) 1252 RW_TAC std_ss [F_WEAK_BOOL_CLOCK_COMP], 1253 (* F_NOT b *) 1254 AUX_TAC2, 1255 (* F_AND (f1,f2) *) 1256 AUX_TAC2, 1257 (* F_STRONG_SERE s *) 1258 AUX_TAC2 1259 THEN PROVE_TAC[S_CLOCK_COMP_CORRECT], 1260 (* F_WEAK_SERE s *) 1261 AUX_TAC2 1262 THEN PROVE_TAC[S_CLOCK_COMP_CORRECT], 1263 (* F_NEXT f *) 1264 RW_TAC std_ss [F_NEXT_CLOCK_COMP], 1265 (* F_UNTIL(f1,f2) f *) 1266 RW_TAC std_ss [F_UNTIL_CLOCK_COMP], 1267 (* F_ABORT(f,b)) *) 1268 AUX_TAC2, 1269 (* F_CLOCK(f,c) *) 1270 AUX_TAC2, 1271 (* F_SUFFIX_IMP(s,f) *) 1272 AUX_TAC2 1273 THEN PROVE_TAC[S_CLOCK_COMP_CORRECT] 1274 ]); 1275 1276val _ = export_theory(); 1277 1278(* Theoem saved when compiling: 1279Saving theorem US_SEM_BOOL_REWRITE_LEMMA 1280Saving theorem S_CLOCK_COMP_CORRECT 1281Saving theorem fl_induct 1282Saving theorem LS_LE_X 1283Saving theorem LS_TRANS_X 1284Saving theorem RESTN_NIL_LENGTH 1285Saving theorem PATH_LENGTH_RESTN_0 1286Saving theorem PATH_FINITE_LENGTH_RESTN_0 1287Saving theorem LIST_LENGTH_RESTN_0 1288Saving theorem PATH_FINITE_LENGTH_RESTN_0_COR 1289Saving theorem UF_SEM_F_U_CLOCK 1290Saving theorem COMPLEMENT_LETTER_COMPLEMENT_LETTER 1291Saving theorem COMPLEMENT_LETTER_COMPLEMENT_LETTER_o 1292Saving theorem MAP_I 1293Saving theorem COMPLEMENT_COMPLEMENT 1294Saving theorem LENGTH_COMPLEMENT 1295Saving theorem HD_MAP 1296Saving theorem TL_MAP 1297Saving theorem RESTN_COMPLEMENT 1298Saving theorem RESTN_COMPLEMENT_COR 1299Saving theorem ELEM_COMPLEMENT 1300Saving theorem ELEM_COMPLEMENT_COR 1301Saving theorem UF_SEM_F_OR 1302Saving theorem UF_SEM_F_AND 1303Saving theorem UF_SEM_F_IMPLIES 1304Saving theorem UF_SEM_RESTN_F_WEAK_BOOL 1305Saving theorem UF_SEM_RESTN_F_WEAK_BOOL_COR 1306Saving theorem UF_SEM_F_F_IMP 1307Saving theorem UF_SEM_F_F 1308Saving theorem UF_SEM_F_G 1309Saving theorem UF_SEM_F_W_CLOCK 1310Saving theorem F_STRONG_BOOL_CLOCK_COMP 1311Saving theorem F_WEAK_BOOL_CLOCK_COMP_IMP1 1312Saving theorem F_WEAK_BOOL_CLOCK_COMP_IMP2 1313Saving theorem F_WEAK_BOOL_CLOCK_COMP 1314Saving theorem EL_SEL_THM 1315Saving theorem F_NEXT_CLOCK_COMP_IMP1 1316Saving theorem F_NEXT_CLOCK_COMP_IMP2 1317Saving theorem F_NEXT_CLOCK_COMP 1318Saving theorem F_UNTIL_CLOCK_COMP_IMP1 1319Saving theorem F_UNTIL_CLOCK_COMP_IMP2 1320Saving theorem F_UNTIL_CLOCK_COMP 1321Saving theorem F_CLOCK_COMP_CORRECT 1322*) 1323