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