1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (Globals.HOLDIR ^ "/examples/temporal_deep/"); 7loadPath := (home_dir ^ "src/deep_embeddings") :: 8 (home_dir ^ "src/tools") :: !loadPath; 9 10map load 11 ["infinite_pathTheory", "prop_logicTheory", "pred_setTheory", "arithmeticTheory", "tuerk_tacticsLib", "numLib", "symbolic_kripke_structureTheory", "set_lemmataTheory"]; 12*) 13 14open pred_setTheory arithmeticTheory infinite_pathTheory prop_logicTheory tuerk_tacticsLib numLib set_lemmataTheory symbolic_kripke_structureTheory 15open Sanity; 16 17(* 18show_assums := false; 19show_assums := true; 20show_types := true; 21show_types := false; 22quietdec := false; 23*) 24 25val _ = hide "S"; 26val _ = hide "I"; 27 28 29val _ = new_theory "rltl"; 30 31 32(****************************************************************************** 33* Syntax and semantic 34******************************************************************************) 35val rltl_def = 36 Hol_datatype 37 `rltl = RLTL_PROP of 'prop prop_logic (* b! *) 38 | RLTL_NOT of rltl (* not f *) 39 | RLTL_AND of rltl # rltl (* f1 and f2 *) 40 | RLTL_NEXT of rltl (* X! f *) 41 | RLTL_SUNTIL of rltl # rltl (* [f1 U f2] *) 42 | RLTL_ACCEPT of rltl # 'prop prop_logic`; (* f abort b *) 43 44 45val rltl_induct = 46 save_thm 47 ("rltl_induct", 48 Q.GEN 49 `P` 50 (MATCH_MP 51 (DECIDE ``(A ==> (B1 /\ B2)) ==> (A ==> B1)``) 52 (SIMP_RULE 53 std_ss 54 [pairTheory.FORALL_PROD, 55 PROVE[]``(!x y. P x ==> Q(x,y)) = !x. P x ==> !y. Q(x,y)``, 56 PROVE[]``(!x y. P y ==> Q(x,y)) = !y. P y ==> !x. Q(x,y)``] 57 (Q.SPECL 58 [`P`,`\(f,b). P f`,`\(f1,f2). P f1 /\ P f2`] 59 (TypeBase.induction_of ``:'a rltl``))))); 60 61 62val RLTL_SEM_TIME_def = 63 Define 64 `(RLTL_SEM_TIME t v a r (RLTL_PROP b) = 65 ((P_SEM (v t) a) \/ ((P_SEM (v t) b) /\ ~(P_SEM (v t) r)))) 66 /\ 67 (RLTL_SEM_TIME t v a r (RLTL_NOT f) = 68 ~(RLTL_SEM_TIME t v r a f)) 69 /\ 70 (RLTL_SEM_TIME t v a r (RLTL_AND (f1,f2)) = 71 RLTL_SEM_TIME t v a r f1 /\ RLTL_SEM_TIME t v a r f2) 72 /\ 73 (RLTL_SEM_TIME t v a r (RLTL_NEXT f) = 74 ((P_SEM (v t) a) \/ (~(P_SEM (v t) r) /\ RLTL_SEM_TIME (SUC t) v a r f))) 75 /\ 76 (RLTL_SEM_TIME t v a r (RLTL_SUNTIL(f1,f2)) = 77 ?k. (k >= t) /\ (RLTL_SEM_TIME k v a r f2) /\ (!j. (t <= j /\ j < k) ==> (RLTL_SEM_TIME j v a r f1))) 78 /\ 79 (RLTL_SEM_TIME t v a r (RLTL_ACCEPT (f, b)) = 80 RLTL_SEM_TIME t v (P_OR(a, P_AND(b, P_NOT(r)))) r f)`; 81 82 83val RLTL_SEM_def = 84 Define 85 `RLTL_SEM v f = RLTL_SEM_TIME 0 v P_FALSE P_FALSE f`; 86 87 88val RLTL_KS_SEM_def = 89 Define 90 `RLTL_KS_SEM M f = 91 !p. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p ==> RLTL_SEM p f`; 92 93 94(****************************************************************************** 95* Syntactic Sugar 96******************************************************************************) 97val RLTL_TRUE_def = 98 Define 99 `RLTL_TRUE = RLTL_PROP P_TRUE`; 100 101val RLTL_FALSE_def = 102 Define 103 `RLTL_FALSE = RLTL_PROP P_FALSE`; 104 105 106 107val RLTL_OR_def = 108 Define 109 `RLTL_OR(f1,f2) = RLTL_NOT (RLTL_AND((RLTL_NOT f1),(RLTL_NOT f2)))`; 110 111 112val RLTL_IMPL_def = 113 Define 114 `RLTL_IMPL(f1, f2) = RLTL_OR(RLTL_NOT f1, f2)`; 115 116 117val RLTL_COND_def = 118 Define 119 `RLTL_COND(c, f1, f2) = RLTL_AND(RLTL_IMPL(c, f1), RLTL_IMPL(RLTL_NOT c, f2))`; 120 121 122val RLTL_EQUIV_def = 123 Define 124 `RLTL_EQUIV(b1, b2) = RLTL_AND(RLTL_IMPL(b1, b2),RLTL_IMPL(b2, b1))`; 125 126 127val RLTL_REJECT_def = 128 Define 129 `RLTL_REJECT(f,b) = RLTL_NOT (RLTL_ACCEPT((RLTL_NOT f),b))`; 130 131 132val RLTL_EVENTUAL_def = 133 Define 134 `RLTL_EVENTUAL f = RLTL_SUNTIL (RLTL_PROP(P_TRUE),f)`; 135 136 137val RLTL_ALWAYS_def = 138 Define 139 `RLTL_ALWAYS f = RLTL_NOT (RLTL_EVENTUAL (RLTL_NOT f))`; 140 141 142val RLTL_UNTIL_def = 143 Define 144 `RLTL_UNTIL(f1,f2) = RLTL_OR(RLTL_SUNTIL(f1,f2),RLTL_ALWAYS f1)`; 145 146 147val RLTL_BEFORE_def = 148 Define 149 `RLTL_BEFORE(f1,f2) = RLTL_NOT(RLTL_SUNTIL(RLTL_NOT f1,f2))`; 150 151 152val RLTL_SBEFORE_def = 153 Define 154 `RLTL_SBEFORE(f1,f2) = RLTL_SUNTIL(RLTL_NOT f2,RLTL_AND(f1, RLTL_NOT f2))`; 155 156 157val RLTL_WHILE_def = 158 Define 159 `RLTL_WHILE(f1,f2) = RLTL_NOT(RLTL_SUNTIL(RLTL_OR(RLTL_NOT f1, RLTL_NOT f2),RLTL_AND(f2, RLTL_NOT f1)))`; 160 161 162val RLTL_SWHILE_def = 163 Define 164 `RLTL_SWHILE(f1,f2) = RLTL_SUNTIL(RLTL_NOT f2,RLTL_AND(f1, f2))`; 165 166 167val RLTL_EQUIV_PATH_STRONG_def = 168 Define `RLTL_EQUIV_PATH_STRONG (t:num) v1 v2 a r = 169 ?k. (k >= t) /\ 170 (((P_SEM (v1 k) a) /\ (P_SEM (v2 k) a) /\ ~(P_SEM (v1 k) r) /\ ~(P_SEM (v2 k) r)) \/ 171 ((P_SEM (v1 k) r) /\ (P_SEM (v2 k) r) /\ ~(P_SEM (v1 k) a) /\ ~(P_SEM (v2 k) a))) /\ 172 (!l. (t <= l /\ l < k ==> ((v1 l) = (v2 l))))`; 173 174val RLTL_EQUIV_PATH_def = 175 Define `RLTL_EQUIV_PATH t v1 v2 a r = 176 (EQUIV_PATH_RESTN t v1 v2) \/ (RLTL_EQUIV_PATH_STRONG t v1 v2 a r)`; 177 178 179 180 181 182 183(****************************************************************************** 184* Classes of RLTL 185******************************************************************************) 186 187val IS_RLTL_G_def = 188 Define 189 `(IS_RLTL_G (RLTL_PROP p) = T) /\ 190 (IS_RLTL_G (RLTL_NOT f) = IS_RLTL_F f) /\ 191 (IS_RLTL_G (RLTL_AND (f,g)) = (IS_RLTL_G f /\ IS_RLTL_G g)) /\ 192 (IS_RLTL_G (RLTL_NEXT f) = IS_RLTL_G f) /\ 193 (IS_RLTL_G (RLTL_SUNTIL(f,g)) = F) /\ 194 (IS_RLTL_G (RLTL_ACCEPT (f,p)) = IS_RLTL_G f) /\ 195 196 (IS_RLTL_F (RLTL_PROP p) = T) /\ 197 (IS_RLTL_F (RLTL_NOT f) = IS_RLTL_G f) /\ 198 (IS_RLTL_F (RLTL_AND (f,g)) = (IS_RLTL_F f /\ IS_RLTL_F g)) /\ 199 (IS_RLTL_F (RLTL_NEXT f) = IS_RLTL_F f) /\ 200 (IS_RLTL_F (RLTL_SUNTIL(f,g)) = (IS_RLTL_F f /\ IS_RLTL_F g)) /\ 201 (IS_RLTL_F (RLTL_ACCEPT (f,p)) = IS_RLTL_F f)`; 202 203 204val IS_RLTL_PREFIX_def = 205 Define 206 `(IS_RLTL_PREFIX (RLTL_NOT f) = IS_RLTL_PREFIX f) /\ 207 (IS_RLTL_PREFIX (RLTL_AND (f,g)) = (IS_RLTL_PREFIX f /\ IS_RLTL_PREFIX g)) /\ 208 (IS_RLTL_PREFIX (RLTL_ACCEPT (f, p)) = (IS_RLTL_PREFIX f)) /\ 209 (IS_RLTL_PREFIX f = (IS_RLTL_G f \/ IS_RLTL_F f))`; 210 211 212val IS_RLTL_GF_def= 213 Define 214 `(IS_RLTL_GF (RLTL_PROP p) = T) /\ 215 (IS_RLTL_GF (RLTL_NOT f) = IS_RLTL_FG f) /\ 216 (IS_RLTL_GF (RLTL_AND (f,g)) = (IS_RLTL_GF f /\ IS_RLTL_GF g)) /\ 217 (IS_RLTL_GF (RLTL_NEXT f) = IS_RLTL_GF f) /\ 218 (IS_RLTL_GF (RLTL_SUNTIL(f,g)) = (IS_RLTL_GF f /\ IS_RLTL_F g)) /\ 219 (IS_RLTL_GF (RLTL_ACCEPT (f,p)) = IS_RLTL_GF f) /\ 220 221 (IS_RLTL_FG (RLTL_PROP p) = T) /\ 222 (IS_RLTL_FG (RLTL_NOT f) = IS_RLTL_GF f) /\ 223 (IS_RLTL_FG (RLTL_AND (f,g)) = (IS_RLTL_FG f /\ IS_RLTL_FG g)) /\ 224 (IS_RLTL_FG (RLTL_NEXT f) = IS_RLTL_FG f) /\ 225 (IS_RLTL_FG (RLTL_SUNTIL(f,g)) = (IS_RLTL_FG f /\ IS_RLTL_FG g)) /\ 226 (IS_RLTL_FG (RLTL_ACCEPT (f,p)) = IS_RLTL_FG f)`; 227 228 229val IS_RLTL_STREET_def = 230 Define 231 `(IS_RLTL_STREET (RLTL_NOT f) = IS_RLTL_STREET f) /\ 232 (IS_RLTL_STREET (RLTL_AND (f,g)) = (IS_RLTL_STREET f /\ IS_RLTL_STREET g)) /\ 233 (IS_RLTL_STREET (RLTL_ACCEPT (f, p)) = (IS_RLTL_STREET f)) /\ 234 (IS_RLTL_STREET f = (IS_RLTL_GF f \/ IS_RLTL_FG f))`; 235 236 237val IS_RLTL_THM = save_thm("IS_RLTL_THM", 238 LIST_CONJ [IS_RLTL_G_def, 239 IS_RLTL_GF_def, 240 IS_RLTL_PREFIX_def, 241 IS_RLTL_STREET_def]); 242 243 244(****************************************************************************** 245 * Tautologies und Contradictions 246 ******************************************************************************) 247val RLTL_EQUIVALENT_def = 248 Define 249 `RLTL_EQUIVALENT l1 l2 = !w t a r. (RLTL_SEM_TIME t w a r l1) = (RLTL_SEM_TIME t w a r l2)`; 250 251val RLTL_EQUIVALENT_INITIAL_def = 252 Define 253 `RLTL_EQUIVALENT_INITIAL l1 l2 = !w. (RLTL_SEM w l1) = (RLTL_SEM w l2)`; 254 255val RLTL_IS_CONTRADICTION_def = 256 Define 257 `RLTL_IS_CONTRADICTION l = (!v. ~(RLTL_SEM v l))`; 258 259val RLTL_IS_TAUTOLOGY_def = 260 Define 261 `RLTL_IS_TAUTOLOGY l = (!v. RLTL_SEM v l)`; 262 263 264val RLTL_TAUTOLOGY_CONTRADICTION_DUAL = 265 store_thm 266 ("RLTL_TAUTOLOGY_CONTRADICTION_DUAL", 267 268 ``(!l. RLTL_IS_CONTRADICTION (RLTL_NOT l) = RLTL_IS_TAUTOLOGY l) /\ 269 (!l. RLTL_IS_TAUTOLOGY (RLTL_NOT l) = RLTL_IS_CONTRADICTION l)``, 270 271 REWRITE_TAC[RLTL_IS_TAUTOLOGY_def, RLTL_IS_CONTRADICTION_def, RLTL_SEM_def, RLTL_SEM_TIME_def]); 272 273 274val RLTL_TAUTOLOGY_CONTRADICTION___TO___EQUIVALENT_INITIAL = 275 store_thm 276 ("RLTL_TAUTOLOGY_CONTRADICTION___TO___EQUIVALENT_INITIAL", 277 278 ``(!l. RLTL_IS_CONTRADICTION l = RLTL_EQUIVALENT_INITIAL l RLTL_FALSE) /\ 279 (!l. RLTL_IS_TAUTOLOGY l = RLTL_EQUIVALENT_INITIAL l RLTL_TRUE)``, 280 281 REWRITE_TAC[RLTL_IS_TAUTOLOGY_def, RLTL_IS_CONTRADICTION_def, 282 RLTL_SEM_TIME_def, RLTL_EQUIVALENT_INITIAL_def, RLTL_FALSE_def, P_SEM_THM, 283 RLTL_TRUE_def, RLTL_SEM_def] THEN 284 PROVE_TAC[]); 285 286 287val RLTL_EQUIVALENT_INITIAL___TO___TAUTOLOGY = 288 store_thm 289 ("RLTL_EQUIVALENT_INITIAL___TO___TAUTOLOGY", 290 291 ``!l1 l2. RLTL_EQUIVALENT_INITIAL l1 l2 = RLTL_IS_TAUTOLOGY (RLTL_EQUIV(l1, l2))``, 292 293 REWRITE_TAC[RLTL_IS_TAUTOLOGY_def, RLTL_SEM_TIME_def, RLTL_EQUIV_def, 294 RLTL_IMPL_def, RLTL_OR_def, 295 RLTL_EQUIVALENT_INITIAL_def, RLTL_SEM_def] THEN 296 PROVE_TAC[]); 297 298 299(****************************************************************************** 300* Some simple Lemmata 301******************************************************************************) 302 303val RLTL_SEM_PROP_RLTL_OPERATOR_EQUIV = 304 store_thm 305 ("RLTL_SEM_PROP_RLTL_OPERATOR_EQUIV", 306 307 ``(!t v a r f. (~(P_SEM (v t) a) \/ ~(P_SEM (v t) r)) ==> 308 (RLTL_SEM_TIME t v a r (RLTL_PROP (P_NOT f)) = 309 RLTL_SEM_TIME t v a r (RLTL_NOT (RLTL_PROP f)))) /\ 310 311 (!t v a r f1 f2. 312 (RLTL_SEM_TIME t v a r (RLTL_PROP (P_AND(f1, f2))) = 313 RLTL_SEM_TIME t v a r (RLTL_AND (RLTL_PROP f1, RLTL_PROP f2))))``, 314 315 REPEAT STRIP_TAC THEN 316 ASM_REWRITE_TAC[RLTL_SEM_TIME_def, P_SEM_def] THEN 317 PROVE_TAC[]) 318 319 320val RLTL_USED_VARS_def= 321 Define 322 `(RLTL_USED_VARS (RLTL_PROP p) = P_USED_VARS p) /\ 323 (RLTL_USED_VARS (RLTL_NOT f) = RLTL_USED_VARS f) /\ 324 (RLTL_USED_VARS (RLTL_AND (f,g)) = (RLTL_USED_VARS f UNION RLTL_USED_VARS g)) /\ 325 (RLTL_USED_VARS (RLTL_NEXT f) = RLTL_USED_VARS f) /\ 326 (RLTL_USED_VARS (RLTL_SUNTIL(f,g)) = (RLTL_USED_VARS f UNION RLTL_USED_VARS g)) /\ 327 (RLTL_USED_VARS (RLTL_ACCEPT (f, p)) = (RLTL_USED_VARS f UNION P_USED_VARS p))`; 328 329 330val RLTL_USED_VARS_INTER_SUBSET_THM = 331 store_thm 332 ("RLTL_USED_VARS_INTER_SUBSET_THM", 333 ``!f t a r v S. ((RLTL_USED_VARS f) SUBSET S /\ (P_USED_VARS a) SUBSET S /\ (P_USED_VARS r) SUBSET S) ==> (RLTL_SEM_TIME t v a r f = RLTL_SEM_TIME t (PATH_RESTRICT v S) a r f)``, 334 335 INDUCT_THEN rltl_induct ASSUME_TAC THENL [ 336 SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, PATH_RESTRICT_def, PATH_MAP_def] THEN 337 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM, UNION_SUBSET], 338 339 340 REWRITE_TAC[RLTL_SEM_TIME_def, RLTL_USED_VARS_def] THEN 341 FULL_SIMP_TAC std_ss [UNION_SUBSET], 342 343 344 FULL_SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, UNION_SUBSET] THEN 345 PROVE_TAC[], 346 347 348 REWRITE_TAC[RLTL_SEM_TIME_def, RLTL_USED_VARS_def] THEN 349 FULL_SIMP_TAC std_ss [UNION_SUBSET] THEN 350 REPEAT STRIP_TAC THEN 351 BINOP_TAC THENL [ 352 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 353 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 354 355 BINOP_TAC THENL [ 356 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 357 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 358 359 METIS_TAC[] 360 ] 361 ], 362 363 364 REWRITE_TAC[RLTL_SEM_TIME_def, RLTL_USED_VARS_def] THEN 365 FULL_SIMP_TAC std_ss [UNION_SUBSET] THEN 366 METIS_TAC[], 367 368 369 REWRITE_TAC[RLTL_SEM_TIME_def, RLTL_USED_VARS_def] THEN 370 FULL_SIMP_TAC std_ss [UNION_SUBSET] THEN 371 REPEAT STRIP_TAC THEN 372 `(P_USED_VARS (P_OR (a,P_AND (p_2,P_NOT r)))) SUBSET S` by ASM_REWRITE_TAC[P_USED_VARS_def, P_OR_def, UNION_SUBSET] THEN 373 METIS_TAC[] 374 ]); 375 376 377val RLTL_USED_VARS_INTER_THM = 378 store_thm 379 ("RLTL_USED_VARS_INTER_THM", 380 ``!f t a r v. (RLTL_SEM_TIME t v a r f = RLTL_SEM_TIME t (PATH_RESTRICT v (RLTL_USED_VARS f UNION P_USED_VARS a UNION P_USED_VARS r)) a r f)``, 381 382 REPEAT STRIP_TAC THEN 383 MATCH_MP_TAC RLTL_USED_VARS_INTER_SUBSET_THM THEN 384 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION]); 385 386 387val RLTL_RESTN_SEM = 388 store_thm 389 ("RLTL_RESTN_SEM", 390 ``!f v a r t1 t2. ((RLTL_SEM_TIME (t1+t2) v a r f) = (RLTL_SEM_TIME t1 (PATH_RESTN v t2) a r f))``, 391 392 INDUCT_THEN rltl_induct ASSUME_TAC THENL [ 393 REWRITE_TAC[RLTL_SEM_TIME_def, PATH_RESTN_def] THEN METIS_TAC[], 394 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 395 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 396 397 FULL_SIMP_TAC arith_ss [RLTL_SEM_TIME_def, PATH_RESTN_def] THEN 398 `!t1 t2. SUC (t1 + t2) = SUC t1 + t2` by DECIDE_TAC THEN 399 METIS_TAC[], 400 401 REWRITE_TAC[RLTL_SEM_TIME_def] THEN 402 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 403 404 EXISTS_TAC ``(k:num)-(t2:num)`` THEN 405 REPEAT STRIP_TAC THENL [ 406 DECIDE_TAC, 407 408 `((k - t2) + t2) = k` by DECIDE_TAC THEN 409 METIS_TAC[], 410 411 `(t1 + t2 <= j+t2) /\ (j+t2 < k)` by DECIDE_TAC THEN 412 `RLTL_SEM_TIME (j+t2) v a r f` by METIS_TAC[] THEN 413 METIS_TAC[] 414 ], 415 416 EXISTS_TAC ``(k:num)+(t2:num)`` THEN 417 REPEAT STRIP_TAC THENL [ 418 DECIDE_TAC, 419 METIS_TAC[], 420 421 `(t1 <= j - t2) /\ (j-t2 < k)` by DECIDE_TAC THEN 422 `RLTL_SEM_TIME (j-t2) (PATH_RESTN v t2) a r f` by METIS_TAC[] THEN 423 `((j - t2) + t2) = j` by DECIDE_TAC THEN 424 METIS_TAC[] 425 ] 426 ], 427 428 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[] 429 ]); 430 431 432val RLTL_SEM_TIME___TIME_ELIM = 433 store_thm 434 ("RLTL_SEM_TIME___TIME_ELIM", 435 ``!f v a r t. ((RLTL_SEM_TIME t v a r f) = (RLTL_SEM_TIME 0 (PATH_RESTN v t) a r f))``, 436 437 `!t. t = 0+t` by DECIDE_TAC THEN 438 METIS_TAC[RLTL_RESTN_SEM]); 439 440 441val RLTL_SEM_TIME___EQUIV_PATH = 442 store_thm 443 ("RLTL_SEM_TIME___EQUIV_PATH", 444 ``!f v1 v2 a r t. (EQUIV_PATH_RESTN t v1 v2) ==> 445 ((RLTL_SEM_TIME t v1 a r f) = (RLTL_SEM_TIME t v2 a r f))``, 446 447 ONCE_REWRITE_TAC[RLTL_SEM_TIME___TIME_ELIM] THEN 448 PROVE_TAC[EQUIV_PATH_RESTN___PATH_RESTN]); 449 450 451val RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV = 452 store_thm 453 ("RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV", 454 ``!f v a1 a2 r t. (PROP_LOGIC_EQUIVALENT a1 a2) ==> 455 (((RLTL_SEM_TIME t v a1 r f) = (RLTL_SEM_TIME t v a2 r f)) /\ 456 ((RLTL_SEM_TIME t v r a1 f) = (RLTL_SEM_TIME t v r a2 f)))``, 457 458 REWRITE_TAC[PROP_LOGIC_EQUIVALENT_def] THEN 459 INDUCT_THEN rltl_induct ASSUME_TAC THEN 460 REPEAT GEN_TAC THEN DISCH_TAC THEN 461 RES_TAC THEN ASM_REWRITE_TAC[RLTL_SEM_TIME_def] THEN 462 `(!s. P_SEM s (P_OR (a1,P_AND (p_2,P_NOT r))) = P_SEM s (P_OR (a2,P_AND (p_2,P_NOT r)))) /\ 463 (!s. P_SEM s (P_OR (r,P_AND (p_2,P_NOT a1))) = P_SEM s (P_OR (r,P_AND (p_2,P_NOT a2))))` 464 by ASM_REWRITE_TAC[P_SEM_THM] THEN 465 RES_TAC THEN ASM_REWRITE_TAC[]); 466 467 468 469val RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV___BOTH = 470 store_thm 471 ("RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV___BOTH", 472 ``!f v a1 a2 r1 r2 t. (PROP_LOGIC_EQUIVALENT a1 a2) ==> 473 (PROP_LOGIC_EQUIVALENT r1 r2) ==> 474 ((RLTL_SEM_TIME t v a1 r1 f) = (RLTL_SEM_TIME t v a2 r2 f))``, 475 476 PROVE_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV]); 477 478 479val RLTL_REJECT_SEM = 480 store_thm 481 ("RLTL_REJECT_SEM", 482 ``!v a r f b t.((RLTL_SEM_TIME t v a r (RLTL_REJECT(f,b))) = 483 RLTL_SEM_TIME t v a (P_OR(r, P_AND(b, P_NOT(a)))) f)``, 484 REWRITE_TAC[RLTL_REJECT_def, RLTL_SEM_TIME_def]); 485 486 487val RLTL_OR_SEM = 488 store_thm 489 ("RLTL_OR_SEM", 490 ``!v a r f1 f2 t.((RLTL_SEM_TIME t v a r (RLTL_OR(f1,f2))) = ((RLTL_SEM_TIME t v a r f1) \/ (RLTL_SEM_TIME t v a r f2)))``, 491 REWRITE_TAC[RLTL_OR_def, RLTL_SEM_TIME_def] THEN SIMP_TAC std_ss []); 492 493 494val RLTL_IMPL_SEM = 495 store_thm 496 ("RLTL_IMPL_SEM", 497 ``!v a r f1 f2 t.((RLTL_SEM_TIME t v a r (RLTL_IMPL(f1,f2))) = ((RLTL_SEM_TIME t v r a f1) ==> (RLTL_SEM_TIME t v a r f2)))``, 498 REWRITE_TAC[RLTL_IMPL_def, RLTL_OR_SEM,RLTL_SEM_TIME_def] THEN METIS_TAC[]); 499 500 501val RLTL_EVENTUAL_SEM = 502 store_thm 503 ("RLTL_EVENTUAL_SEM", 504 ``!v a r f t. ((RLTL_SEM_TIME t v a r (RLTL_EVENTUAL f)) = 505 (?k. (k >= t) /\ (RLTL_SEM_TIME k v a r f) /\ (!j. t <= j /\ j < k ==> 506 P_SEM (v j) a \/ ~P_SEM (v j) r)))``, 507 508 REWRITE_TAC[RLTL_EVENTUAL_def,RLTL_SEM_TIME_def, P_SEM_def]); 509 510 511val RLTL_ALWAYS_SEM = 512 store_thm 513 ("RLTL_ALWAYS_SEM", 514 ``!v a r f t. (RLTL_SEM_TIME t v a r (RLTL_ALWAYS f)) = 515 (!k. ((k >= t) /\ (!j. (t <= j /\ j < k) ==> (P_SEM (v j) r \/ ~P_SEM (v j) a))) ==> (RLTL_SEM_TIME k v a r f))``, 516 517 SIMP_TAC std_ss [RLTL_ALWAYS_def, RLTL_EVENTUAL_def,RLTL_SEM_TIME_def, P_SEM_def] THEN 518 PROVE_TAC[]); 519 520 521val RLTL_SEM_THM = LIST_CONJ [RLTL_SEM_def, 522 RLTL_SEM_TIME_def, 523 RLTL_OR_SEM, 524 RLTL_IMPL_SEM, 525 RLTL_ALWAYS_SEM, 526 RLTL_EVENTUAL_SEM]; 527val _ = save_thm("RLTL_SEM_THM",RLTL_SEM_THM); 528 529 530val RLTL_EQUIV_PATH_STRONG___SYM_PATH = 531 store_thm 532 ("RLTL_EQUIV_PATH_STRONG___SYM_PATH", 533 ``!v1 v2 a r t. RLTL_EQUIV_PATH_STRONG t v1 v2 a r = RLTL_EQUIV_PATH_STRONG t v2 v1 a r``, 534 535 REWRITE_TAC[RLTL_EQUIV_PATH_STRONG_def] THEN 536 METIS_TAC[]); 537 538 539val RLTL_EQUIV_PATH_STRONG___SYM_ACCEPT_REJECT = 540 store_thm 541 ("RLTL_EQUIV_PATH_STRONG___SYM_ACCEPT_REJECT", 542 ``!v1 v2 a r t. RLTL_EQUIV_PATH_STRONG t v1 v2 a r = RLTL_EQUIV_PATH_STRONG t v1 v2 r a``, 543 544 REWRITE_TAC[RLTL_EQUIV_PATH_STRONG_def] THEN 545 METIS_TAC[]); 546 547 548val RLTL_EQUIV_PATH___SYM_PATH = 549 store_thm 550 ("RLTL_EQUIV_PATH___SYM_PATH", 551 ``!v1 v2 a r t. RLTL_EQUIV_PATH t v1 v2 a r = RLTL_EQUIV_PATH t v2 v1 a r``, 552 553 REWRITE_TAC[RLTL_EQUIV_PATH_def] THEN 554 PROVE_TAC[EQUIV_PATH_RESTN_SYM, RLTL_EQUIV_PATH_STRONG___SYM_PATH]); 555 556 557val RLTL_EQUIV_PATH___SYM_ACCEPT_REJECT = 558 store_thm 559 ("RLTL_EQUIV_PATH___SYM_ACCEPT_REJECT", 560 ``!v1 v2 a r t. RLTL_EQUIV_PATH t v1 v2 a r = RLTL_EQUIV_PATH t v1 v2 r a``, 561 REWRITE_TAC[RLTL_EQUIV_PATH_def] THEN 562 PROVE_TAC[RLTL_EQUIV_PATH_STRONG___SYM_ACCEPT_REJECT]); 563 564 565val RLTL_EQUIV_PATH_STRONG___GREATER_IMPL = 566 store_thm 567 ("RLTL_EQUIV_PATH_STRONG___GREATER_IMPL", 568 ``!v1 v2 t t2 a r. (t2 >= t /\ (RLTL_EQUIV_PATH_STRONG t v1 v2 a r) /\ (!j. (t <= j /\ j < t2) ==> ((~(P_SEM (v1 j) a) \/ ~(P_SEM (v2 j) a)) /\ 569 (~(P_SEM (v1 j) r) \/ ~(P_SEM (v2 j) r))))) ==> (RLTL_EQUIV_PATH_STRONG t2 v1 v2 a r)``, 570 571 REWRITE_TAC [RLTL_EQUIV_PATH_STRONG_def] THEN 572 REPEAT STRIP_TAC THEN ( 573 `~(k < t2)` by PROVE_TAC[GREATER_EQ] THEN 574 EXISTS_TAC ``k:num`` THEN 575 ASM_SIMP_TAC arith_ss [] 576 )); 577 578 579val RLTL_EQUIV_PATH___GREATER_IMPL = 580 store_thm 581 ("RLTL_EQUIV_PATH___GREATER_IMPL", 582 ``!v1 v2 t t2 a r. (t2 >= t /\ (RLTL_EQUIV_PATH t v1 v2 a r) /\ (!j. (t <= j /\ j < t2) ==> ((~(P_SEM (v1 j) a) \/ ~(P_SEM (v2 j) a)) /\ 583 (~(P_SEM (v1 j) r) \/ ~(P_SEM (v2 j) r))))) ==> (RLTL_EQUIV_PATH t2 v1 v2 a r)``, 584 585 REWRITE_TAC[RLTL_EQUIV_PATH_def] THEN 586 REPEAT STRIP_TAC THENL [ 587 PROVE_TAC[EQUIV_PATH_RESTN___GREATER_IMPL], 588 589 ASSUME_TAC RLTL_EQUIV_PATH_STRONG___GREATER_IMPL THEN 590 RES_TAC THEN ASM_REWRITE_TAC[] 591 ]); 592 593 594val RLTL_EQUIV_PATH_STRONG___SUC = 595 store_thm 596 ("RLTL_EQUIV_PATH_STRONG___SUC", 597 ``!v1 v2 t a r. ((RLTL_EQUIV_PATH_STRONG t v1 v2 a r) /\ (~(P_SEM (v1 t) a) \/ ~(P_SEM (v2 t) a)) /\ 598 (~(P_SEM (v1 t) r) \/ ~(P_SEM (v2 t) r))) ==> (RLTL_EQUIV_PATH_STRONG (SUC t) v1 v2 a r)``, 599 600 `!t. SUC t >= t /\ (!j. (t <= j /\ j < SUC t) ==> (j = t))` by DECIDE_TAC THEN 601 METIS_TAC[RLTL_EQUIV_PATH_STRONG___GREATER_IMPL]); 602 603 604val RLTL_EQUIV_PATH___SUC = 605 store_thm 606 ("RLTL_EQUIV_PATH___SUC", 607 ``!v1 v2 t a r. ((RLTL_EQUIV_PATH t v1 v2 a r) /\ (~(P_SEM (v1 t) a) \/ ~(P_SEM (v2 t) a)) /\ 608 (~(P_SEM (v1 t) r) \/ ~(P_SEM (v2 t) r))) ==> (RLTL_EQUIV_PATH (SUC t) v1 v2 a r)``, 609 610 `!t. SUC t >= t /\ (!j. (t <= j /\ j < SUC t) ==> (j = t))` by DECIDE_TAC THEN 611 METIS_TAC[RLTL_EQUIV_PATH___GREATER_IMPL]); 612 613 614 615val RLTL_EQUIV_PATH_STRONG___INITIAL = 616 store_thm 617 ("RLTL_EQUIV_PATH_STRONG___INITIAL", 618 ``!v1 v2 t a r. (RLTL_EQUIV_PATH_STRONG t v1 v2 a r) ==> 619 (((P_SEM (v1 t) a) = (P_SEM (v2 t) a)) /\ 620 ((P_SEM (v1 t) r) = (P_SEM (v2 t) r)))``, 621 622 REWRITE_TAC [RLTL_EQUIV_PATH_STRONG_def] THEN 623 REPEAT GEN_TAC THEN STRIP_TAC THEN ( 624 Cases_on `k = t` THENL [ 625 PROVE_TAC[], 626 627 `t < k` by DECIDE_TAC THEN 628 PROVE_TAC[LESS_EQ_REFL] 629 ] 630 )); 631 632 633val RLTL_EQUIV_PATH___INITIAL = 634 store_thm 635 ("RLTL_EQUIV_PATH___INITIAL", 636 ``!v1 v2 t a r. (RLTL_EQUIV_PATH t v1 v2 a r) ==> 637 (((P_SEM (v1 t) a) = (P_SEM (v2 t) a)) /\ 638 ((P_SEM (v1 t) r) = (P_SEM (v2 t) r)))``, 639 640 REWRITE_TAC [RLTL_EQUIV_PATH_def] THEN 641 REPEAT GEN_TAC THEN STRIP_TAC THENL [ 642 FULL_SIMP_TAC std_ss [EQUIV_PATH_RESTN_def], 643 PROVE_TAC[RLTL_EQUIV_PATH_STRONG___INITIAL] 644 ] 645 ); 646 647 648 649val RLTL_ACCEPT_REJECT_THM = 650 store_thm 651 ("RLTL_ACCEPT_REJECT_THM", 652 ``!f v a r t. (((P_SEM (v t) a) /\ ~(P_SEM (v t) r)) ==> RLTL_SEM_TIME t v a r f) /\ 653 ((~(P_SEM (v t) a) /\ (P_SEM (v t) r)) ==> ~(RLTL_SEM_TIME t v a r f))``, 654 655 656INDUCT_THEN rltl_induct ASSUME_TAC THENL [ 657 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 658 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 659 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 660 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 661 662 REWRITE_TAC[RLTL_SEM_TIME_def] THEN 663 REPEAT STRIP_TAC THENL [ 664 EXISTS_TAC ``t:num`` THEN 665 ASM_SIMP_TAC arith_ss [], 666 667 `(t <= t) /\ ((t < k) \/ (t = k))` by DECIDE_TAC THEN 668 METIS_TAC[] 669 ], 670 671 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[P_SEM_THM] 672]); 673 674 675val RLTL_SEM_TIME___STRANGE_NEGATION_EXAMPLE = 676 store_thm 677 ("RLTL_SEM_TIME___STRANGE_NEGATION_EXAMPLE", 678 679 ``!v a r p1 p2 t. (P_SEM (v t) a /\ P_SEM (v t) r /\ (!j:num. j > t ==> ( 680 ~(P_SEM (v j) p1) /\ ~(P_SEM (v j) p2) /\ ~(P_SEM (v j) r))) /\ (!j:num. (P_SEM (v j) a = (j <= SUC t)))) ==> 681 682 ((RLTL_SEM_TIME t v a r (RLTL_SUNTIL(RLTL_PROP p1, RLTL_NOT(RLTL_PROP p2)))) /\ 683 (RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_SUNTIL(RLTL_PROP p1, RLTL_NOT(RLTL_PROP p2))))))``, 684 685 REPEAT STRIP_TAC THEN 686 ASM_SIMP_TAC std_ss [RLTL_SEM_THM] THENL [ 687 EXISTS_TAC ``SUC t`` THEN 688 ASM_SIMP_TAC arith_ss [], 689 690 REPEAT STRIP_TAC THEN 691 Cases_on `k >= t` THEN ASM_REWRITE_TAC[] THEN 692 Cases_on `k <= SUC t` THEN ASM_REWRITE_TAC[] THEN 693 `k > SUC t` by DECIDE_TAC THEN 694 DISJ2_TAC THEN 695 EXISTS_TAC ``SUC t`` THEN 696 ASM_SIMP_TAC arith_ss [] 697 ]); 698 699 700 701val RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH = 702 store_thm 703 ("RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH", 704 ``!f t v a1 a2 r. (IMP_ON_PATH_RESTN t v a1 a2) ==> 705 ((RLTL_SEM_TIME t v a1 r f ==> RLTL_SEM_TIME t v a2 r f) /\ 706 (RLTL_SEM_TIME t v r a2 f ==> RLTL_SEM_TIME t v r a1 f))``, 707 708 INDUCT_THEN rltl_induct ASSUME_TAC THENL [ 709 REWRITE_TAC[RLTL_SEM_TIME_def, IMP_ON_PATH_RESTN_def] THEN METIS_TAC[LESS_EQ_REFL, GREATER_EQ], 710 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 711 REWRITE_TAC[RLTL_SEM_TIME_def] THEN METIS_TAC[], 712 713 REWRITE_TAC[RLTL_SEM_TIME_def] THEN 714 REPEAT STRIP_TAC THENL [ 715 METIS_TAC[IMP_ON_PATH_RESTN_def, LESS_EQ_REFL, GREATER_EQ], 716 717 `SUC t >= t` by DECIDE_TAC THEN 718 `IMP_ON_PATH_RESTN (SUC t) v a1 a2` by METIS_TAC[IMP_ON_PATH_RESTN___GREATER_IMPL] THEN 719 METIS_TAC[], 720 721 ASM_REWRITE_TAC[], 722 723 `~ P_SEM (v t) a1` by METIS_TAC[IMP_ON_PATH_RESTN_def, LESS_EQ_REFL, GREATER_EQ] THEN 724 `SUC t >= t` by DECIDE_TAC THEN 725 `IMP_ON_PATH_RESTN (SUC t) v a1 a2` by METIS_TAC[IMP_ON_PATH_RESTN___GREATER_IMPL] THEN 726 METIS_TAC[] 727 ], 728 729 730 ONCE_REWRITE_TAC[RLTL_SEM_TIME_def, IMP_ON_PATH_RESTN___GREATER_IMPL] THEN 731 REPEAT STRIP_TAC THEN 732 EXISTS_TAC ``k:num`` THEN 733 METIS_TAC[GREATER_EQ], 734 735 736 737 REWRITE_TAC[RLTL_SEM_TIME_def] THEN 738 REPEAT GEN_TAC THEN DISCH_TAC THEN 739 REPEAT STRIP_TAC THENL[ 740 `IMP_ON_PATH_RESTN t v (P_OR (a1,P_AND (p_2,P_NOT r))) (P_OR (a2,P_AND (p_2,P_NOT r)))` by 741 (FULL_SIMP_TAC std_ss [P_SEM_def, P_SEM_THM, IMP_ON_PATH_RESTN_def] THEN METIS_TAC[]) THEN 742 METIS_TAC[], 743 744 745 `IMP_ON_PATH_RESTN t v (P_OR (r,P_AND (p_2,P_NOT a2))) (P_OR (r,P_AND (p_2,P_NOT a1)))` by 746 (FULL_SIMP_TAC std_ss [P_SEM_def, P_SEM_THM, IMP_ON_PATH_RESTN_def] THEN METIS_TAC[]) THEN 747 METIS_TAC[] 748 ] 749 ]); 750 751 752val RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV_ON_PATH = 753 store_thm 754 ("RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV_ON_PATH", 755 ``!f t v a1 a2 r. (EQUIV_ON_PATH_RESTN t v a1 a2) ==> 756 ((RLTL_SEM_TIME t v a1 r f = RLTL_SEM_TIME t v a2 r f) /\ 757 (RLTL_SEM_TIME t v r a1 f = RLTL_SEM_TIME t v r a2 f))``, 758 759 METIS_TAC[EQUIV_ON_PATH_RESTN___IMP_ON_PATH_RESTN, RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH]); 760 761 762val RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV_ON_PATH___BOTH = 763 store_thm 764 ("RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV_ON_PATH___BOTH", 765 ``!f t v a1 a2 r1 r2. (EQUIV_ON_PATH_RESTN t v a1 a2) ==> 766 (EQUIV_ON_PATH_RESTN t v r1 r2) ==> 767 (RLTL_SEM_TIME t v a1 r1 f = RLTL_SEM_TIME t v a2 r2 f)``, 768 769 METIS_TAC[EQUIV_ON_PATH_RESTN___IMP_ON_PATH_RESTN, RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH]); 770 771 772val RLTL_SEM_TIME___ACCEPT_REJECT_IMPL_EQUIV = 773 store_thm 774 ("RLTL_SEM_TIME___ACCEPT_REJECT_IMPL_EQUIV", 775 776 ``!t v r a1 a2. 777 (!f. (RLTL_SEM_TIME t v r a2 f ==> RLTL_SEM_TIME t v r a1 f)) = 778 (!f. (RLTL_SEM_TIME t v a1 r f ==> RLTL_SEM_TIME t v a2 r f))``, 779 780 METIS_TAC[RLTL_SEM_TIME_def]); 781 782 783 784val RLTL_EQUIV_PATH_STRONG_THM = 785 store_thm 786 ("RLTL_EQUIV_PATH_STRONG_THM", 787 ``!f t a r v1 v2. (RLTL_EQUIV_PATH_STRONG t v1 v2 a r) ==> (RLTL_SEM_TIME t v1 a r f = RLTL_SEM_TIME 788 t v2 a r f)``, 789 790 INDUCT_THEN rltl_induct ASSUME_TAC THEN REPEAT STRIP_TAC THENL [ 791 792 FULL_SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_EQUIV_PATH_STRONG_def] THEN 793 (Cases_on `k = t` THENL [ 794 METIS_TAC[], 795 796 `t <= t /\ t < k` by DECIDE_TAC THEN 797 METIS_TAC[] 798 ]), 799 800 ASM_SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_EQUIV_PATH_STRONG___SYM_ACCEPT_REJECT], 801 ASM_SIMP_TAC std_ss [RLTL_SEM_TIME_def] THEN METIS_TAC[], 802 803 804 REWRITE_TAC [RLTL_SEM_TIME_def] THEN 805 METIS_TAC [RLTL_EQUIV_PATH_STRONG___SUC, RLTL_EQUIV_PATH_STRONG___INITIAL], 806 807 REMAINS_TAC `!v1 v2. RLTL_EQUIV_PATH_STRONG t v1 v2 a r /\ RLTL_SEM_TIME t v1 a r (RLTL_SUNTIL (f,f')) ==> RLTL_SEM_TIME t v2 a r (RLTL_SUNTIL (f,f'))` THEN1 ( 808 METIS_TAC[RLTL_EQUIV_PATH_STRONG___SYM_PATH] 809 ) THEN 810 WEAKEN_HD_TAC THEN 811 SIMP_TAC arith_ss [RLTL_EQUIV_PATH_STRONG_def, RLTL_SEM_TIME_def] THEN 812 REPEAT STRIP_TAC THEN ( 813 `?l. MIN k k' = l` by METIS_TAC[] THEN 814 SUBGOAL_TAC `l <= k /\ l <= k' /\ l >= t` THEN1 ( 815 REWRITE_TAC[GSYM (ASSUME ``MIN k k' = l``), MIN_DEF] THEN 816 Cases_on `k < k'` THEN 817 ASM_REWRITE_TAC[] THEN 818 DECIDE_TAC 819 ) THEN 820 SUBGOAL_TAC `!j. (t <= j /\ j <= l) ==> (RLTL_EQUIV_PATH_STRONG j v1 v2 a r)` THEN1 ( 821 REWRITE_TAC[RLTL_EQUIV_PATH_STRONG_def] THEN 822 REPEAT STRIP_TAC THEN 823 `k >= j /\ !j':num. (j <= j') ==> (t <= j')` by DECIDE_TAC THEN 824 EXISTS_TAC ``k:num`` THEN 825 METIS_TAC[] 826 ) THEN 827 EXISTS_TAC ``l:num`` THEN 828 `l >= t` by DECIDE_TAC THEN 829 ASM_REWRITE_TAC [] THEN 830 REPEAT STRIP_TAC 831 ) THENL [ 832 `(l = k) \/ (l = k')` by METIS_TAC[MIN_DEF] THENL [ 833 METIS_TAC[RLTL_ACCEPT_REJECT_THM], 834 METIS_TAC[GREATER_EQ, LESS_EQ_REFL] 835 ], 836 837 `t <= j /\ j < k' /\ j <= l` by DECIDE_TAC THEN 838 METIS_TAC[], 839 840 `(k < k') \/ (l = k')` by METIS_TAC[MIN_DEF] THENL [ 841 METIS_TAC[RLTL_ACCEPT_REJECT_THM, GREATER_EQ], 842 METIS_TAC[GREATER_EQ, LESS_EQ_REFL] 843 ], 844 845 `t <= j /\ j < k' /\ j <= l` by DECIDE_TAC THEN 846 METIS_TAC[] 847 ], 848 849 850 SIMP_TAC std_ss [RLTL_SEM_TIME_def] THEN 851 SUBGOAL_TAC `RLTL_EQUIV_PATH_STRONG t v1 v2 (P_OR (a,P_AND (p_2,P_NOT r))) r` THEN1 ( 852 REWRITE_ALL_TAC[RLTL_EQUIV_PATH_STRONG_def, P_SEM_THM] THEN 853 EXISTS_TAC ``k:num`` THEN 854 ASM_REWRITE_TAC[] 855 ) THEN 856 METIS_TAC[] 857 ]); 858 859 860 861 862val RLTL_EQUIV_PATH_THM = 863 store_thm 864 ("RLTL_EQUIV_PATH_THM", 865 ``!f t a r v1 v2. (RLTL_EQUIV_PATH t v1 v2 a r) ==> (RLTL_SEM_TIME t v1 a r f = RLTL_SEM_TIME 866 t v2 a r f)``, 867 868 METIS_TAC[RLTL_EQUIV_PATH_def, RLTL_SEM_TIME___EQUIV_PATH, RLTL_EQUIV_PATH_STRONG_THM]); 869 870 871 872val RLTL_SEM_TIME___ACCEPT_BEFORE_ON_PATH = 873 store_thm 874 ("RLTL_SEM_TIME___ACCEPT_BEFORE_ON_PATH", 875 876 ``!t v a1 a2 r f. (NAND_ON_PATH_RESTN t v a1 r /\ BEFORE_ON_PATH_RESTN t v a1 a2) ==> 877 ((RLTL_SEM_TIME t v a2 r f ==> RLTL_SEM_TIME t v a1 r f))``, 878 879 REPEAT GEN_TAC THEN 880 REPEAT DISCH_TAC THEN 881 CLEAN_ASSUMPTIONS_TAC THEN 882 Cases_on `NOT_ON_PATH_RESTN t v a2` THENL [ 883 `IMP_ON_PATH_RESTN t v a2 a1` by 884 (REWRITE_ALL_TAC [IMP_ON_PATH_RESTN_def, NOT_ON_PATH_RESTN_def, GREATER_EQ] THEN 885 METIS_TAC[]) THEN 886 METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH], 887 888 889 SUBGOAL_TAC `?u. (t <= u /\ P_SEM (v u) a1) /\ (!u'. (t <= u' /\ u' < u) ==> 890 (~P_SEM (v u') a1) /\ ~P_SEM (v u') a2)` THEN1 ( 891 892 SIMP_ALL_TAC std_ss [NOT_ON_PATH_RESTN_def] THEN 893 SUBGOAL_TAC `?k. (P_SEM (v k) a2 /\ t <= k) /\ !k'. (t <= k' /\ k' < k) ==> ~(P_SEM (v k') a2)` THEN1 ( 894 ASSUME_TAC (EXISTS_LEAST_CONV ``?k. (P_SEM (v k) a2) /\ t <= k``) THEN 895 METIS_TAC[] 896 ) THEN 897 REWRITE_ALL_TAC [BEFORE_ON_PATH_RESTN_def] THEN 898 `?k'. t <= k' /\ k' <= k /\ P_SEM (v k') a1` by METIS_TAC[] THEN 899 900 SUBGOAL_TAC `?u. (P_SEM (v u) a1 /\ t <= u) /\ !l'. (t <= l' /\ l' < u) ==> ~(P_SEM (v l') a1)` THEN1 ( 901 ASSUME_TAC (EXISTS_LEAST_CONV ``?u. (P_SEM (v u) a1) /\ t <= u``) THEN 902 METIS_TAC[] 903 ) THEN 904 905 EXISTS_TAC ``u:num`` THEN 906 ASM_REWRITE_TAC[] THEN 907 `~(k' < u)` by METIS_TAC[] THEN 908 `!u'. u' < u ==> u' < k` by DECIDE_TAC THEN 909 METIS_TAC[] 910 ) THEN 911 912 913 914 `~P_SEM (v u) r` by 915 (SIMP_ALL_TAC arith_ss [NAND_ON_PATH_RESTN_def] THEN 916 METIS_TAC[GREATER_EQ, LESS_EQ_REFL]) THEN 917 Cases_on `t = u` THEN1 (METIS_TAC[RLTL_ACCEPT_REJECT_THM]) THEN 918 `t < u` by DECIDE_TAC THEN 919 `?w. (\n. if (u < n) then (v t) else v n) = w` by METIS_TAC[] THEN 920 921 922 SUBGOAL_TAC `RLTL_SEM_TIME t v (P_OR(a1, a2)) r f` THEN1 ( 923 SUBGOAL_TAC `IMP_ON_PATH_RESTN t v a2 (P_OR (a1,a2))` THEN1 ( 924 SIMP_TAC std_ss [IMP_ON_PATH_RESTN_def, P_SEM_THM] 925 ) THEN 926 METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH] 927 ) THEN 928 929 SUBGOAL_TAC `(RLTL_EQUIV_PATH_STRONG t v w a1 r) /\ (RLTL_EQUIV_PATH_STRONG t v w (P_OR(a1, a2)) r)` THEN1 ( 930 REWRITE_TAC[RLTL_EQUIV_PATH_STRONG_def, GREATER_EQ, P_SEM_THM] THEN 931 REPEAT STRIP_TAC THEN 932 EXISTS_TAC ``u:num`` THEN 933 `w u = v u` by METIS_TAC[] THEN 934 ASM_REWRITE_TAC[] THEN 935 REPEAT STRIP_TAC THEN 936 `~(u < l)` by DECIDE_TAC THEN 937 METIS_TAC[] 938 ) THEN 939 940 SUBGOAL_TAC `IMP_ON_PATH_RESTN t w (P_OR(a1,a2)) a1` THEN1 ( 941 REWRITE_TAC [IMP_ON_PATH_RESTN_def, GREATER_EQ, P_SEM_THM] THEN 942 REPEAT STRIP_TAC THEN 943 Cases_on `u < t'` THENL [ 944 `w t' = v t` by METIS_TAC[] THEN 945 METIS_TAC[LESS_EQ_REFL], 946 947 `w t' = v t'` by METIS_TAC[] THEN 948 Cases_on `t' = u` THENL [ 949 METIS_TAC[], 950 951 `t' < u` by DECIDE_TAC THEN 952 METIS_TAC[] 953 ] 954 ]) THEN 955 956 PROVE_TAC[RLTL_EQUIV_PATH_STRONG_THM, RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH] 957 ]); 958 959 960val RLTL_SEM_TIME___REJECT_BEFORE_ON_PATH = 961 store_thm 962 ("RLTL_SEM_TIME___REJECT_BEFORE_ON_PATH", 963 964 ``!t v a1 a2 r f. (NAND_ON_PATH_RESTN t v a1 r /\ BEFORE_ON_PATH_RESTN t v a1 a2) ==> 965 ((RLTL_SEM_TIME t v r a1 f ==> RLTL_SEM_TIME t v r a2 f))``, 966 967 REPEAT GEN_TAC THEN DISCH_TAC THEN 968 `!f. RLTL_SEM_TIME t v a2 r f ==> RLTL_SEM_TIME t v a1 r f` by PROVE_TAC[RLTL_SEM_TIME___ACCEPT_BEFORE_ON_PATH] THEN 969 PROVE_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IMPL_EQUIV]); 970 971 972 973val RLTL_SEM_TIME___ACCEPT_OR_THM = 974 store_thm 975 ("RLTL_SEM_TIME___ACCEPT_OR_THM", 976 ``!t v a1 a2 r f. (NAND_ON_PATH_RESTN t v a1 r /\ NAND_ON_PATH_RESTN t v a2 r) ==> 977 ((RLTL_SEM_TIME t v (P_OR (a1, a2)) r f = (RLTL_SEM_TIME t v a1 r f \/ RLTL_SEM_TIME t v a2 r f)))``, 978 979 REPEAT STRIP_TAC THEN 980 EQ_TAC THENL [ 981 DISJ_CASES_TAC (SPECL [``v:num->'a set``, ``t:num``, ``a1:'a prop_logic``, ``a2:'a prop_logic``] BEFORE_ON_PATH_CASES) THENL [ 982 SUBGOAL_TAC `BEFORE_ON_PATH_RESTN t v a1 (P_OR (a1,a2))` THEN1 ( 983 REWRITE_ALL_TAC [BEFORE_ON_PATH_RESTN_def, P_SEM_THM] THEN 984 PROVE_TAC[LESS_EQ_REFL] 985 ) THEN 986 PROVE_TAC[RLTL_SEM_TIME___ACCEPT_BEFORE_ON_PATH], 987 988 SUBGOAL_TAC `BEFORE_ON_PATH_RESTN t v a2 (P_OR (a1,a2))` THEN1 ( 989 REWRITE_ALL_TAC [BEFORE_ON_PATH_RESTN_def, P_SEM_THM] THEN 990 PROVE_TAC[LESS_EQ_REFL] 991 ) THEN 992 PROVE_TAC[RLTL_SEM_TIME___ACCEPT_BEFORE_ON_PATH] 993 ], 994 995 REPEAT STRIP_TAC THENL [ 996 `IMP_ON_PATH_RESTN t v a1 (P_OR(a1, a2))` by PROVE_TAC[IMP_ON_PATH_RESTN_def, P_SEM_THM, LESS_EQ_REFL], 997 `IMP_ON_PATH_RESTN t v a2 (P_OR(a1, a2))` by PROVE_TAC[IMP_ON_PATH_RESTN_def, P_SEM_THM, LESS_EQ_REFL] 998 ] THEN 999 PROVE_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH] 1000 ]); 1001 1002 1003 1004val RLTL_SEM_TIME___REJECT_OR_THM = 1005 store_thm 1006 ("RLTL_SEM_TIME___REJECT_OR_THM", 1007 ``!t v a r1 r2 f. (NAND_ON_PATH_RESTN t v r1 a /\ NAND_ON_PATH_RESTN t v r2 a) ==> 1008 ((RLTL_SEM_TIME t v a (P_OR (r1, r2)) f = (RLTL_SEM_TIME t v a r1 f /\ RLTL_SEM_TIME t v a r2 f)))``, 1009 1010 REPEAT STRIP_TAC THEN 1011 `RLTL_SEM_TIME t v a (P_OR (r1,r2)) f = ~(RLTL_SEM_TIME t v (P_OR (r1,r2)) a (RLTL_NOT f))` by 1012 REWRITE_TAC[RLTL_SEM_TIME_def] THEN 1013 ASM_REWRITE_TAC[] THEN 1014 `(RLTL_SEM_TIME t v (P_OR (r1,r2)) a (RLTL_NOT f)) = 1015 (RLTL_SEM_TIME t v r1 a (RLTL_NOT f) \/ RLTL_SEM_TIME t v r2 a (RLTL_NOT f))` by 1016 METIS_TAC[RLTL_SEM_TIME___ACCEPT_OR_THM] THEN 1017 ASM_REWRITE_TAC[RLTL_SEM_TIME_def] THEN 1018 PROVE_TAC[]); 1019 1020 1021 1022 1023val RLTL_SEM_TIME___ACCEPT_REJECT_IS_ON_PATH = 1024 store_thm 1025 ("RLTL_SEM_TIME___ACCEPT_REJECT_IS_ON_PATH", 1026 ``!v t a b r f. ((RLTL_SEM_TIME t v a r f /\ ~RLTL_SEM_TIME t v b r f) \/ 1027 (RLTL_SEM_TIME t v r b f /\ ~RLTL_SEM_TIME t v r a f)) ==> 1028 IS_ON_PATH_RESTN t v a``, 1029 1030 REPEAT STRIP_TAC THEN 1031 CCONTR_TAC THEN 1032 `IMP_ON_PATH_RESTN t v a b` by PROVE_TAC[IS_ON_PATH_RESTN_def, NOT_ON_PATH___IMP_ON_PATH] THEN 1033 PROVE_TAC [RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH]); 1034 1035 1036 1037 1038 1039 1040val RLTL_SEM_TIME___ACCEPT_REJECT_BEFORE_ON_PATH_STRONG = 1041 store_thm 1042 ("RLTL_SEM_TIME___ACCEPT_REJECT_BEFORE_ON_PATH_STRONG", 1043 ``!v t a1 a2 r f. (NAND_ON_PATH_RESTN t v a2 r /\ 1044 ((RLTL_SEM_TIME t v a1 r f /\ ~RLTL_SEM_TIME t v a2 r f) \/ 1045 (~RLTL_SEM_TIME t v r a1 f /\ RLTL_SEM_TIME t v r a2 f))) ==> BEFORE_ON_PATH_RESTN_STRONG t v a1 a2``, 1046 1047 REPEAT STRIP_TAC THEN 1048 CCONTR_TAC THEN 1049 `BEFORE_ON_PATH_RESTN t v a2 a1` by METIS_TAC[BEFORE_ON_PATH_RESTN___NEGATION_IMPL] THENL [ 1050 METIS_TAC[RLTL_SEM_TIME___ACCEPT_BEFORE_ON_PATH], 1051 METIS_TAC[RLTL_SEM_TIME___REJECT_BEFORE_ON_PATH] 1052 ]); 1053 1054 1055 1056val RLTL_WEAK_UNTIL___ALTERNATIVE_DEF = 1057 store_thm 1058 ("RLTL_WEAK_UNTIL___ALTERNATIVE_DEF", 1059 ``!v a r t f1 f2. 1060 (RLTL_SEM_TIME t v a r (RLTL_UNTIL(f1,f2)) = 1061 RLTL_SEM_TIME t v a r (RLTL_NOT (RLTL_SUNTIL(RLTL_NOT f2, RLTL_AND(RLTL_NOT f1, RLTL_NOT f2)))))``, 1062 1063 SIMP_TAC std_ss [RLTL_UNTIL_def, RLTL_SEM_THM] THEN 1064 REPEAT STRIP_TAC THEN 1065 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1066 Cases_on `k < k'` THENL [ 1067 `t <= k` by DECIDE_TAC THEN 1068 METIS_TAC[], 1069 1070 Cases_on `~(k' >= t)` THEN1 ASM_REWRITE_TAC[] THEN 1071 Cases_on `k' = k` THEN1 ASM_REWRITE_TAC[] THEN 1072 `t <= k' /\ k' < k` by DECIDE_TAC THEN 1073 METIS_TAC[] 1074 ], 1075 1076 1077 Cases_on `(!j. t <= j /\ j < k ==> P_SEM (v j) r \/ ~P_SEM (v j) a)` THENL [ 1078 PROVE_TAC[], 1079 PROVE_TAC[RLTL_ACCEPT_REJECT_THM] 1080 ], 1081 1082 1083 Cases_on `!k. k >= t ==> RLTL_SEM_TIME k v a r f1` THENL [ 1084 PROVE_TAC[], 1085 1086 DISJ1_TAC THEN 1087 SIMP_ASSUMPTIONS_TAC std_ss [] THEN 1088 SUBGOAL_TAC `?k. (k >= (t:num) /\ ~RLTL_SEM_TIME k v a r f1) /\ !k'. k' < k ==> ~(k' >= t /\ ~RLTL_SEM_TIME k' v a r f1)` THEN1 ( 1089 ASSUME_TAC (EXISTS_LEAST_CONV ``?k. k >= (t:num) /\ ~RLTL_SEM_TIME k (v:num -> 'a set) a r f1``) THEN 1090 RES_TAC THEN 1091 PROVE_TAC[] 1092 ) THEN 1093 SUBGOAL_TAC `?l:num. l >= (t:num) /\ l <= (k':num) /\ RLTL_SEM_TIME l v a r f2` THEN1 ( 1094 Cases_on `RLTL_SEM_TIME k' v a r f2` THENL [ 1095 EXISTS_TAC ``k':num`` THEN 1096 ASM_SIMP_TAC arith_ss [], 1097 1098 `?j. t <= j /\ j < k' /\ RLTL_SEM_TIME j v a r f2` by METIS_TAC[] THEN 1099 EXISTS_TAC ``j:num`` THEN 1100 ASM_SIMP_TAC arith_ss [] 1101 ] 1102 ) THEN 1103 EXISTS_TAC ``l:num`` THEN 1104 ASM_SIMP_TAC arith_ss [] THEN 1105 REPEAT STRIP_TAC THEN 1106 `j < k' /\ j >= t` by DECIDE_TAC THEN 1107 PROVE_TAC[] 1108 ] 1109 ]); 1110 1111 1112 1113 1114 1115val RLTL_NEGATION_NORMAL_FORM = 1116 store_thm 1117 ("RLTL_NEGATION_NORMAL_FORM", 1118 1119 ``!v t a r f f1 f2 b p. (~(P_SEM (v t) a /\ P_SEM (v t) r) ==> 1120 ((RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_PROP p)) = RLTL_SEM_TIME t v a r (RLTL_PROP (P_NOT p))) /\ 1121 (RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_NEXT f)) = RLTL_SEM_TIME t v a r (RLTL_NEXT(RLTL_NOT f))))) /\ 1122 1123 (RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_NOT f)) = RLTL_SEM_TIME t v a r f) /\ 1124 (RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_AND(f1, f2))) = RLTL_SEM_TIME t v a r (RLTL_OR (RLTL_NOT f1, RLTL_NOT f2))) /\ 1125 (RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_SUNTIL(f1,f2))) = RLTL_SEM_TIME t v a r (RLTL_BEFORE(RLTL_NOT f1, f2))) /\ 1126 (RLTL_SEM_TIME t v a r (RLTL_NOT(RLTL_ACCEPT(f,b))) = RLTL_SEM_TIME t v a r (RLTL_REJECT (RLTL_NOT f, b)))``, 1127 1128 SIMP_TAC std_ss [RLTL_BEFORE_def, RLTL_SEM_TIME_def, P_SEM_def, RLTL_OR_def, RLTL_REJECT_def] THEN 1129 PROVE_TAC[]); 1130 1131 1132 1133val IS_RLTL_RELATIONS = 1134 store_thm 1135 ("IS_RLTL_RELATIONS", 1136 ``!f. ((IS_RLTL_F f = IS_RLTL_G (RLTL_NOT f)) /\ (IS_RLTL_G f = IS_RLTL_F (RLTL_NOT f)) /\ 1137 (IS_RLTL_FG f = IS_RLTL_GF (RLTL_NOT f)) /\ (IS_RLTL_GF f = IS_RLTL_FG (RLTL_NOT f)) /\ 1138 (IS_RLTL_F f ==> IS_RLTL_FG f) /\ (IS_RLTL_G f ==> IS_RLTL_GF f) /\ 1139 (IS_RLTL_G f ==> IS_RLTL_FG f) /\ (IS_RLTL_F f ==> IS_RLTL_GF f) /\ 1140 (IS_RLTL_PREFIX f ==> (IS_RLTL_FG f /\ IS_RLTL_GF f)))``, 1141 1142 INDUCT_THEN rltl_induct ASSUME_TAC THEN 1143 REWRITE_TAC[IS_RLTL_G_def, IS_RLTL_PREFIX_def, IS_RLTL_GF_def] THEN 1144 METIS_TAC[] 1145 ); 1146 1147 1148 1149val RLTL_VAR_RENAMING_def= 1150 Define 1151 `(RLTL_VAR_RENAMING f (RLTL_PROP p) = RLTL_PROP (P_VAR_RENAMING f p)) /\ 1152 (RLTL_VAR_RENAMING f (RLTL_NOT r) = RLTL_NOT (RLTL_VAR_RENAMING f r)) /\ 1153 (RLTL_VAR_RENAMING f (RLTL_AND (r1,r2)) = RLTL_AND(RLTL_VAR_RENAMING f r1, RLTL_VAR_RENAMING f r2)) /\ 1154 (RLTL_VAR_RENAMING f (RLTL_NEXT r) = RLTL_NEXT (RLTL_VAR_RENAMING f r)) /\ 1155 (RLTL_VAR_RENAMING f (RLTL_SUNTIL(r1,r2)) = RLTL_SUNTIL(RLTL_VAR_RENAMING f r1, RLTL_VAR_RENAMING f r2)) /\ 1156 (RLTL_VAR_RENAMING f (RLTL_ACCEPT (r, p)) = RLTL_ACCEPT(RLTL_VAR_RENAMING f r, P_VAR_RENAMING f p))`; 1157 1158 1159 1160val RLTL_SEM_TIME___VAR_RENAMING = 1161 store_thm 1162 ("RLTL_SEM_TIME___VAR_RENAMING", 1163 ``!f' t v a r f. 1164 (INJ f (PATH_USED_VARS v UNION RLTL_USED_VARS f' UNION P_USED_VARS a UNION P_USED_VARS r) UNIV) ==> 1165 ((RLTL_SEM_TIME t v a r f') = 1166 (RLTL_SEM_TIME t (PATH_VAR_RENAMING f v) (P_VAR_RENAMING f a) (P_VAR_RENAMING f r) (RLTL_VAR_RENAMING f f')))``, 1167 1168 1169 INDUCT_THEN rltl_induct ASSUME_TAC THENL [ 1170 SIMP_TAC std_ss [RLTL_SEM_TIME_def, 1171 RLTL_VAR_RENAMING_def, PATH_VAR_RENAMING_def, 1172 PATH_MAP_def] THEN 1173 REPEAT STRIP_TAC THEN 1174 REMAINS_TAC `INJ f ((v t) UNION P_USED_VARS a) UNIV /\ 1175 INJ f ((v t) UNION P_USED_VARS p) UNIV /\ 1176 INJ f ((v t) UNION P_USED_VARS r) UNIV` THEN1 ( 1177 ASM_SIMP_TAC std_ss [GSYM P_SEM___VAR_RENAMING] 1178 ) THEN STRIP_TAC THEN 1179 REPEAT STRIP_TAC THEN 1180 UNDISCH_HD_TAC THEN 1181 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1182 REWRITE_TAC [SUBSET_DEF, IN_UNION, RLTL_USED_VARS_def, 1183 GSYM PATH_USED_VARS_THM] THEN 1184 PROVE_TAC[], 1185 1186 1187 SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, 1188 RLTL_VAR_RENAMING_def] THEN 1189 REPEAT STRIP_TAC THEN 1190 POP_NO_ASSUM 1 MATCH_MP_TAC THEN 1191 PROVE_TAC[UNION_COMM, UNION_ASSOC], 1192 1193 1194 SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, 1195 RLTL_VAR_RENAMING_def] THEN 1196 REPEAT STRIP_TAC THEN 1197 REMAINS_TAC `INJ f (PATH_USED_VARS v UNION RLTL_USED_VARS f'' UNION 1198 P_USED_VARS a UNION P_USED_VARS r) UNIV /\ 1199 INJ f (PATH_USED_VARS v UNION RLTL_USED_VARS f' UNION 1200 P_USED_VARS a UNION P_USED_VARS r) UNIV` THEN1 ( 1201 RES_TAC THEN 1202 ASM_REWRITE_TAC[] 1203 ) THEN 1204 NTAC 2 (WEAKEN_NO_TAC 1) THEN 1205 STRIP_TAC THEN 1206 UNDISCH_HD_TAC THEN 1207 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1208 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1209 PROVE_TAC[], 1210 1211 1212 SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, 1213 RLTL_VAR_RENAMING_def] THEN 1214 REPEAT STRIP_TAC THEN 1215 Q_SPECL_NO_ASSUM 1 [`SUC t`, `v`, `a`, `r`, `f`] THEN 1216 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 1217 ASM_REWRITE_TAC[] THEN 1218 WEAKEN_HD_TAC THEN 1219 REMAINS_TAC `INJ f ((v t) UNION P_USED_VARS a) UNIV /\ 1220 INJ f ((v t) UNION P_USED_VARS r) UNIV` THEN1 ( 1221 ASM_SIMP_TAC std_ss [GSYM P_SEM___VAR_RENAMING, PATH_VAR_RENAMING_def, 1222 PATH_MAP_def] 1223 ) THEN 1224 STRIP_TAC THEN UNDISCH_HD_TAC THEN 1225 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1226 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, GSYM PATH_USED_VARS_THM] THEN 1227 PROVE_TAC[], 1228 1229 1230 SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, 1231 RLTL_VAR_RENAMING_def] THEN 1232 REPEAT STRIP_TAC THEN 1233 REMAINS_TAC `INJ f (PATH_USED_VARS v UNION RLTL_USED_VARS f'' UNION 1234 P_USED_VARS a UNION P_USED_VARS r) UNIV /\ 1235 INJ f (PATH_USED_VARS v UNION RLTL_USED_VARS f' UNION 1236 P_USED_VARS a UNION P_USED_VARS r) UNIV` THEN1 ( 1237 RES_TAC THEN 1238 ASM_REWRITE_TAC[] 1239 ) THEN 1240 NTAC 2 (WEAKEN_NO_TAC 1) THEN 1241 STRIP_TAC THEN 1242 UNDISCH_HD_TAC THEN 1243 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1244 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 1245 PROVE_TAC[], 1246 1247 1248 1249 SIMP_TAC std_ss [RLTL_SEM_TIME_def, RLTL_USED_VARS_def, 1250 RLTL_VAR_RENAMING_def, GSYM P_VAR_RENAMING_def, P_OR_def] THEN 1251 REPEAT STRIP_TAC THEN 1252 REMAINS_TAC `INJ f (PATH_USED_VARS v UNION RLTL_USED_VARS f' UNION 1253 P_USED_VARS (P_NOT (P_AND (P_NOT a,P_NOT (P_AND (p_2,P_NOT r))))) UNION P_USED_VARS r) UNIV` THEN1 ( 1254 RES_TAC THEN 1255 ASM_REWRITE_TAC[] 1256 ) THEN 1257 UNDISCH_HD_TAC THEN 1258 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1259 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, P_USED_VARS_def] THEN 1260 PROVE_TAC[] 1261 ]); 1262 1263 1264 1265 1266val RLTL_SEM_TIME___VAR_RENAMING___PATH_RESTRICT = 1267 store_thm 1268 ("RLTL_SEM_TIME___VAR_RENAMING___PATH_RESTRICT", 1269 ``!f' t v a r f. (INJ f (RLTL_USED_VARS f' UNION P_USED_VARS a UNION P_USED_VARS r) UNIV) ==> ((RLTL_SEM_TIME t v a r f') = (RLTL_SEM_TIME t 1270 (PATH_VAR_RENAMING f (PATH_RESTRICT v (RLTL_USED_VARS f' UNION P_USED_VARS a UNION P_USED_VARS r))) (P_VAR_RENAMING f a) (P_VAR_RENAMING f r) (RLTL_VAR_RENAMING f f')))``, 1271 1272 REPEAT STRIP_TAC THEN 1273 CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [RLTL_USED_VARS_INTER_THM])) THEN 1274 MATCH_MP_TAC RLTL_SEM_TIME___VAR_RENAMING THEN 1275 UNDISCH_HD_TAC THEN 1276 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 1277 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, GSYM PATH_USED_VARS_THM, 1278 PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 1279 PROVE_TAC[]); 1280 1281 1282val RLTL_SEM___VAR_RENAMING___PATH_RESTRICT = 1283 store_thm 1284 ("RLTL_SEM___VAR_RENAMING___PATH_RESTRICT", 1285 ``!f' v f. (INJ f (RLTL_USED_VARS f') UNIV) ==> ((RLTL_SEM v f') = (RLTL_SEM 1286 (PATH_VAR_RENAMING f (PATH_RESTRICT v (RLTL_USED_VARS f'))) (RLTL_VAR_RENAMING f f')))``, 1287 1288 REPEAT STRIP_TAC THEN 1289 REWRITE_TAC[RLTL_SEM_def] THEN 1290 SUBGOAL_TAC `P_FALSE = P_VAR_RENAMING f P_FALSE` THEN1 ( 1291 SIMP_TAC std_ss [P_FALSE_def, P_VAR_RENAMING_def] 1292 ) THEN 1293 ASM_REWRITE_TAC[] THEN 1294 ASSUME_TAC RLTL_SEM_TIME___VAR_RENAMING___PATH_RESTRICT THEN 1295 Q_SPECL_NO_ASSUM 0 [`f'`, `0:num`, `v`, `P_FALSE`, `P_FALSE`, `f`] THEN 1296 UNDISCH_HD_TAC THEN 1297 ASM_SIMP_TAC std_ss [P_USED_VARS_EVAL, UNION_EMPTY]); 1298 1299 1300 1301val _ = export_theory(); 1302