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