1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/tools") :: !loadPath; 9 10map load 11 ["prop_logicTheory", "xprop_logicTheory", "infinite_pathTheory", "pred_setTheory", "tuerk_tacticsLib", "numLib", "arithmeticTheory", "symbolic_kripke_structureTheory", "set_lemmataTheory"]; 12*) 13 14open pred_setTheory prop_logicTheory xprop_logicTheory infinite_pathTheory tuerk_tacticsLib numLib 15 arithmeticTheory symbolic_kripke_structureTheory set_lemmataTheory; 16open Sanity; 17 18val _ = hide "S"; 19val _ = hide "I"; 20 21(* 22show_assums := false; 23show_assums := true; 24show_types := true; 25show_types := false; 26quietdec := false; 27*) 28 29 30val _ = new_theory "full_ltl"; 31 32 33(****************************************************************************** 34* Syntax 35******************************************************************************) 36val ltl_def = 37 Hol_datatype 38 `ltl = LTL_PROP of 'prop prop_logic 39 | LTL_NOT of ltl 40 | LTL_AND of ltl # ltl 41 | LTL_NEXT of ltl 42 | LTL_SUNTIL of ltl # ltl 43 | LTL_PSNEXT of ltl 44 | LTL_PSUNTIL of ltl # ltl`; 45 46val ltl_induct = 47 save_thm 48 ("ltl_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`,`\(f1,f2). P f1 /\ P f2`] 60 (TypeBase.induction_of ``:'a ltl``))))); 61 62 63(****************************************************************************** 64* Semantic 65******************************************************************************) 66val LTL_SEM_TIME_def = 67 Define 68 `(LTL_SEM_TIME t v (LTL_NOT f) = 69 ~(LTL_SEM_TIME t v f)) 70 /\ 71 (LTL_SEM_TIME t v (LTL_AND (f1,f2)) = 72 LTL_SEM_TIME t v f1 /\ LTL_SEM_TIME t v f2) 73 /\ 74 (LTL_SEM_TIME t v (LTL_PROP b) = 75 (P_SEM (v t) b)) 76 /\ 77 (LTL_SEM_TIME t v (LTL_NEXT f) = 78 LTL_SEM_TIME (SUC t) v f) 79 /\ 80 (LTL_SEM_TIME t v (LTL_SUNTIL(f1,f2)) = 81 ?k. (k >= t) /\ (LTL_SEM_TIME k v f2) /\ (!j. (t <= j /\ j < k) ==> (LTL_SEM_TIME j v f1))) 82 /\ 83 (LTL_SEM_TIME t v (LTL_PSNEXT f) = 84 ((t > 0) /\ LTL_SEM_TIME (PRE t) v f)) 85 /\ 86 (LTL_SEM_TIME t v (LTL_PSUNTIL(f1,f2)) = 87 ?k. (k <= t) /\ (LTL_SEM_TIME k v f2) /\ (!j. (k < j /\ j <= t) ==> (LTL_SEM_TIME j v f1)))`; 88 89 90val LTL_SEM_def = 91 Define 92 `LTL_SEM v f = LTL_SEM_TIME 0 v f`; 93 94 95val LTL_KS_SEM_def = 96 Define 97 `LTL_KS_SEM M f = 98 !p. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p ==> LTL_SEM p f`; 99 100 101(****************************************************************************** 102* Syntactic Sugar 103******************************************************************************) 104val LTL_EQUIVALENT_def = 105 Define 106 `LTL_EQUIVALENT b1 b2 = !t w. (LTL_SEM_TIME t w b1) = (LTL_SEM_TIME t w b2)`; 107 108val LTL_EQUIVALENT_INITIAL_def = 109 Define 110 `LTL_EQUIVALENT_INITIAL b1 b2 = !w. (LTL_SEM w b1) = (LTL_SEM w b2)`; 111 112val LTL_OR_def = 113 Define 114 `LTL_OR(f1,f2) = LTL_NOT (LTL_AND((LTL_NOT f1),(LTL_NOT f2)))`; 115 116val LTL_IMPL_def = 117 Define 118 `LTL_IMPL(f1, f2) = LTL_OR(LTL_NOT f1, f2)`; 119 120val LTL_COND_def = 121 Define 122 `LTL_COND(c, f1, f2) = LTL_AND(LTL_IMPL(c, f1), LTL_IMPL(LTL_NOT c, f2))`; 123 124val LTL_EQUIV_def = 125 Define 126 `LTL_EQUIV(b1, b2) = LTL_AND(LTL_IMPL(b1, b2),LTL_IMPL(b2, b1))`; 127 128 129val LTL_EVENTUAL_def = 130 Define 131 `LTL_EVENTUAL f = LTL_SUNTIL (LTL_PROP(P_TRUE),f)`; 132 133val LTL_ALWAYS_def = 134 Define 135 `LTL_ALWAYS f = LTL_NOT (LTL_EVENTUAL (LTL_NOT f))`; 136 137val LTL_UNTIL_def = 138 Define 139 `LTL_UNTIL(f1,f2) = LTL_OR(LTL_SUNTIL(f1,f2),LTL_ALWAYS f1)`; 140 141val LTL_BEFORE_def = 142 Define 143 `LTL_BEFORE(f1,f2) = LTL_NOT(LTL_SUNTIL(LTL_NOT f1,f2))`; 144 145val LTL_SBEFORE_def = 146 Define 147 `LTL_SBEFORE(f1,f2) = LTL_SUNTIL(LTL_NOT f2,LTL_AND(f1, LTL_NOT f2))`; 148 149val LTL_WHILE_def = 150 Define 151 `LTL_WHILE(f1,f2) = LTL_NOT(LTL_SUNTIL(LTL_OR(LTL_NOT f1, LTL_NOT f2),LTL_AND(f2, LTL_NOT f1)))`; 152 153val LTL_SWHILE_def = 154 Define 155 `LTL_SWHILE(f1,f2) = LTL_SUNTIL(LTL_NOT f2,LTL_AND(f1, f2))`; 156 157 158 159val LTL_PEVENTUAL_def = 160 Define 161 `LTL_PEVENTUAL f = LTL_PSUNTIL (LTL_PROP(P_TRUE),f)`; 162 163val LTL_PALWAYS_def = 164 Define 165 `LTL_PALWAYS f = LTL_NOT (LTL_PEVENTUAL (LTL_NOT f))`; 166 167val LTL_PUNTIL_def = 168 Define 169 `LTL_PUNTIL(f1,f2) = LTL_OR(LTL_PSUNTIL(f1,f2),LTL_PALWAYS f1)`; 170 171val LTL_PNEXT_def = 172 Define 173 `LTL_PNEXT f = LTL_NOT(LTL_PSNEXT (LTL_NOT f))`; 174 175val LTL_PBEFORE_def = 176 Define 177 `LTL_PBEFORE(f1,f2) = LTL_NOT(LTL_PSUNTIL(LTL_NOT f1,f2))`; 178 179val LTL_PSBEFORE_def = 180 Define 181 `LTL_PSBEFORE(f1,f2) = LTL_PSUNTIL(LTL_NOT f2,LTL_AND(f1, LTL_NOT f2))`; 182 183val LTL_PWHILE_def = 184 Define 185 `LTL_PWHILE(f1,f2) = LTL_NOT(LTL_PSUNTIL(LTL_OR(LTL_NOT f1, LTL_NOT f2),LTL_AND(f2, LTL_NOT f1)))`; 186 187val LTL_PSWHILE_def = 188 Define 189 `LTL_PSWHILE(f1,f2) = LTL_PSUNTIL(LTL_NOT f2,LTL_AND(f1, f2))`; 190 191val LTL_TRUE_def = 192 Define 193 `LTL_TRUE = LTL_PROP P_TRUE`; 194 195val LTL_FALSE_def = 196 Define 197 `LTL_FALSE = LTL_PROP P_FALSE`; 198 199val LTL_INIT_def = 200 Define 201 `LTL_INIT = LTL_NOT (LTL_PSNEXT (LTL_PROP P_TRUE))`; 202 203 204 205 206(****************************************************************************** 207* Classes of LTL 208******************************************************************************) 209 210val IS_FUTURE_LTL_def = 211 Define 212 `(IS_FUTURE_LTL (LTL_PROP b) = T) /\ 213 (IS_FUTURE_LTL (LTL_NOT f) = (IS_FUTURE_LTL f)) /\ 214 (IS_FUTURE_LTL (LTL_AND(f1,f2)) = (IS_FUTURE_LTL f1 /\ IS_FUTURE_LTL f2)) /\ 215 (IS_FUTURE_LTL (LTL_NEXT f) = (IS_FUTURE_LTL f)) /\ 216 (IS_FUTURE_LTL (LTL_SUNTIL(f1,f2)) = (IS_FUTURE_LTL f1 /\ IS_FUTURE_LTL f2)) /\ 217 (IS_FUTURE_LTL (LTL_PSNEXT f) = F) /\ 218 (IS_FUTURE_LTL (LTL_PSUNTIL(f1,f2)) = F)`; 219 220 221val IS_PAST_LTL_def = 222 Define 223 `(IS_PAST_LTL (LTL_PROP b) = T) /\ 224 (IS_PAST_LTL (LTL_NOT f) = (IS_PAST_LTL f)) /\ 225 (IS_PAST_LTL (LTL_AND(f1,f2)) = (IS_PAST_LTL f1 /\ IS_PAST_LTL f2)) /\ 226 (IS_PAST_LTL (LTL_PSNEXT f) = (IS_PAST_LTL f)) /\ 227 (IS_PAST_LTL (LTL_PSUNTIL(f1,f2)) = (IS_PAST_LTL f1 /\ IS_PAST_LTL f2)) /\ 228 (IS_PAST_LTL (LTL_NEXT f) = F) /\ 229 (IS_PAST_LTL (LTL_SUNTIL(f1,f2)) = F)`; 230 231 232 233 234val IS_LTL_G_def = 235 Define 236 `(IS_LTL_G (LTL_PROP p) = T) /\ 237 (IS_LTL_G (LTL_NOT f) = IS_LTL_F f) /\ 238 (IS_LTL_G (LTL_AND (f,g)) = (IS_LTL_G f /\ IS_LTL_G g)) /\ 239 (IS_LTL_G (LTL_NEXT f) = IS_LTL_G f) /\ 240 (IS_LTL_G (LTL_SUNTIL(f,g)) = F) /\ 241 (IS_LTL_G (LTL_PSNEXT f) = IS_LTL_G f) /\ 242 (IS_LTL_G (LTL_PSUNTIL(f,g)) = (IS_LTL_G f /\ IS_LTL_G g)) /\ 243 244 (IS_LTL_F (LTL_PROP p) = T) /\ 245 (IS_LTL_F (LTL_NOT f) = IS_LTL_G f) /\ 246 (IS_LTL_F (LTL_AND (f,g)) = (IS_LTL_F f /\ IS_LTL_F g)) /\ 247 (IS_LTL_F (LTL_NEXT f) = IS_LTL_F f) /\ 248 (IS_LTL_F (LTL_SUNTIL(f,g)) = (IS_LTL_F f /\ IS_LTL_F g)) /\ 249 (IS_LTL_F (LTL_PSNEXT f) = IS_LTL_F f) /\ 250 (IS_LTL_F (LTL_PSUNTIL(f,g)) = (IS_LTL_F f /\ IS_LTL_F g))`; 251 252 253val IS_LTL_PREFIX_def = 254 Define 255 `(IS_LTL_PREFIX (LTL_NOT f) = IS_LTL_PREFIX f) /\ 256 (IS_LTL_PREFIX (LTL_AND (f,g)) = (IS_LTL_PREFIX f /\ IS_LTL_PREFIX g)) /\ 257 (IS_LTL_PREFIX f = (IS_LTL_G f \/ IS_LTL_F f))`; 258 259 260val IS_LTL_GF_def= 261 Define 262 `(IS_LTL_GF (LTL_PROP p) = T) /\ 263 (IS_LTL_GF (LTL_NOT f) = IS_LTL_FG f) /\ 264 (IS_LTL_GF (LTL_AND (f,g)) = (IS_LTL_GF f /\ IS_LTL_GF g)) /\ 265 (IS_LTL_GF (LTL_NEXT f) = IS_LTL_GF f) /\ 266 (IS_LTL_GF (LTL_SUNTIL(f,g)) = (IS_LTL_GF f /\ IS_LTL_F g)) /\ 267 (IS_LTL_GF (LTL_PSNEXT f) = IS_LTL_GF f) /\ 268 (IS_LTL_GF (LTL_PSUNTIL(f,g)) = (IS_LTL_GF f /\ IS_LTL_GF g)) /\ 269 270 (IS_LTL_FG (LTL_PROP p) = T) /\ 271 (IS_LTL_FG (LTL_NOT f) = IS_LTL_GF f) /\ 272 (IS_LTL_FG (LTL_AND (f,g)) = (IS_LTL_FG f /\ IS_LTL_FG g)) /\ 273 (IS_LTL_FG (LTL_NEXT f) = IS_LTL_FG f) /\ 274 (IS_LTL_FG (LTL_SUNTIL(f,g)) = (IS_LTL_FG f /\ IS_LTL_FG g)) /\ 275 (IS_LTL_FG (LTL_PSNEXT f) = IS_LTL_FG f) /\ 276 (IS_LTL_FG (LTL_PSUNTIL(f,g)) = (IS_LTL_FG f /\ IS_LTL_FG g))`; 277 278 279val IS_LTL_STREET_def = 280 Define 281 `(IS_LTL_STREET (LTL_NOT f) = IS_LTL_STREET f) /\ 282 (IS_LTL_STREET (LTL_AND (f,g)) = (IS_LTL_STREET f /\ IS_LTL_STREET g)) /\ 283 (IS_LTL_STREET f = (IS_LTL_GF f \/ IS_LTL_FG f))`; 284 285 286val IS_LTL_THM = save_thm("IS_LTL_THM", 287 LIST_CONJ [IS_FUTURE_LTL_def, 288 IS_PAST_LTL_def, 289 IS_LTL_G_def, 290 IS_LTL_GF_def, 291 IS_LTL_PREFIX_def, 292 IS_LTL_STREET_def]); 293 294 295val IS_LTL_RELATIONS = 296 store_thm 297 ("IS_LTL_RELATIONS", 298 ``!f. ((IS_LTL_F f = IS_LTL_G (LTL_NOT f)) /\ (IS_LTL_G f = IS_LTL_F (LTL_NOT f)) /\ 299 (IS_LTL_FG f = IS_LTL_GF (LTL_NOT f)) /\ (IS_LTL_GF f = IS_LTL_FG (LTL_NOT f)) /\ 300 (IS_LTL_F f ==> IS_LTL_FG f) /\ (IS_LTL_G f ==> IS_LTL_GF f) /\ 301 (IS_LTL_G f ==> IS_LTL_FG f) /\ (IS_LTL_F f ==> IS_LTL_GF f) /\ 302 (IS_LTL_PREFIX f ==> (IS_LTL_FG f /\ IS_LTL_GF f)))``, 303 304 INDUCT_THEN ltl_induct ASSUME_TAC THEN 305 REWRITE_TAC[IS_LTL_THM] THEN 306 METIS_TAC[] 307 ); 308 309(****************************************************************************** 310* Lemmata 311******************************************************************************) 312val LTL_USED_VARS_def= 313 Define 314 `(LTL_USED_VARS (LTL_PROP p) = P_USED_VARS p) /\ 315 (LTL_USED_VARS (LTL_NOT f) = LTL_USED_VARS f) /\ 316 (LTL_USED_VARS (LTL_AND (f,g)) = (LTL_USED_VARS f UNION LTL_USED_VARS g)) /\ 317 (LTL_USED_VARS (LTL_NEXT f) = LTL_USED_VARS f) /\ 318 (LTL_USED_VARS (LTL_SUNTIL(f,g)) = (LTL_USED_VARS f UNION LTL_USED_VARS g)) /\ 319 (LTL_USED_VARS (LTL_PSNEXT f) = LTL_USED_VARS f) /\ 320 (LTL_USED_VARS (LTL_PSUNTIL(f,g)) = (LTL_USED_VARS f UNION LTL_USED_VARS g))`; 321 322 323val LTL_USED_VARS_INTER_SUBSET_THM = 324 store_thm 325 ("LTL_USED_VARS_INTER_SUBSET_THM", 326 ``!f t v S. (LTL_USED_VARS f) SUBSET S ==> (LTL_SEM_TIME t v f = LTL_SEM_TIME t (PATH_RESTRICT v S) f)``, 327 328 INDUCT_THEN ltl_induct ASSUME_TAC THENL [ 329 SIMP_TAC arith_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, PATH_RESTRICT_def, PATH_MAP_def] THEN 330 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 331 332 REWRITE_TAC[LTL_SEM_TIME_def, LTL_USED_VARS_def] THEN 333 PROVE_TAC[], 334 335 REWRITE_TAC[LTL_SEM_TIME_def, LTL_USED_VARS_def, UNION_SUBSET] THEN 336 PROVE_TAC[], 337 338 REWRITE_TAC[LTL_SEM_TIME_def, LTL_USED_VARS_def] THEN 339 PROVE_TAC[], 340 341 REWRITE_TAC[LTL_SEM_TIME_def, LTL_USED_VARS_def, UNION_SUBSET] THEN 342 PROVE_TAC[], 343 344 REWRITE_TAC[LTL_SEM_TIME_def, LTL_USED_VARS_def] THEN 345 PROVE_TAC[], 346 347 REWRITE_TAC[LTL_SEM_TIME_def, LTL_USED_VARS_def, UNION_SUBSET] THEN 348 PROVE_TAC[] 349 ]); 350 351 352val LTL_USED_VARS_INTER_THM = 353 store_thm 354 ("LTL_USED_VARS_INTER_THM", 355 ``!f t v. (LTL_SEM_TIME t v f = LTL_SEM_TIME t (PATH_RESTRICT v (LTL_USED_VARS f)) f)``, 356 357 METIS_TAC [LTL_USED_VARS_INTER_SUBSET_THM, SUBSET_REFL]); 358 359 360val FINITE___LTL_USED_VARS = 361 store_thm 362 ("FINITE___LTL_USED_VARS", 363 364 ``!l. FINITE(LTL_USED_VARS l)``, 365 366 INDUCT_THEN ltl_induct ASSUME_TAC THEN1 ( 367 REWRITE_TAC[LTL_USED_VARS_def, FINITE___P_USED_VARS] 368 ) THEN 369 ASM_REWRITE_TAC[LTL_USED_VARS_def, FINITE_UNION]); 370 371 372val LTL_USED_VARS_EVAL= 373 store_thm ("LTL_USED_VARS_EVAL", 374 ``(LTL_USED_VARS (LTL_PROP p) = P_USED_VARS p) /\ 375 (LTL_USED_VARS (LTL_NOT r) = LTL_USED_VARS r) /\ 376 (LTL_USED_VARS (LTL_AND (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 377 (LTL_USED_VARS (LTL_NEXT r) = LTL_USED_VARS r) /\ 378 (LTL_USED_VARS (LTL_SUNTIL(r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 379 (LTL_USED_VARS (LTL_PSNEXT r) = LTL_USED_VARS r) /\ 380 (LTL_USED_VARS (LTL_PSUNTIL(r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 381 (LTL_USED_VARS (LTL_OR (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 382 (LTL_USED_VARS (LTL_IMPL (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 383 (LTL_USED_VARS (LTL_EQUIV (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 384 (LTL_USED_VARS (LTL_ALWAYS r) = LTL_USED_VARS r) /\ 385 (LTL_USED_VARS (LTL_EVENTUAL r) = LTL_USED_VARS r) /\ 386 (LTL_USED_VARS (LTL_PNEXT r) = LTL_USED_VARS r) /\ 387 (LTL_USED_VARS LTL_TRUE = EMPTY) /\ 388 (LTL_USED_VARS LTL_FALSE = EMPTY) /\ 389 (LTL_USED_VARS LTL_INIT = EMPTY) /\ 390 (LTL_USED_VARS (LTL_PALWAYS r) = LTL_USED_VARS r) /\ 391 (LTL_USED_VARS (LTL_PEVENTUAL r) = LTL_USED_VARS r) /\ 392 (LTL_USED_VARS (LTL_WHILE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 393 (LTL_USED_VARS (LTL_BEFORE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 394 (LTL_USED_VARS (LTL_SWHILE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 395 (LTL_USED_VARS (LTL_SBEFORE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 396 (LTL_USED_VARS (LTL_PWHILE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 397 (LTL_USED_VARS (LTL_PBEFORE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 398 (LTL_USED_VARS (LTL_PSWHILE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2) /\ 399 (LTL_USED_VARS (LTL_PSBEFORE (r1,r2)) = LTL_USED_VARS r1 UNION LTL_USED_VARS r2)``, 400 401 SIMP_TAC std_ss [LTL_USED_VARS_def, LTL_OR_def, LTL_IMPL_def, LTL_EQUIV_def, 402 LTL_ALWAYS_def, LTL_EVENTUAL_def, P_VAR_RENAMING_EVAL, LTL_PNEXT_def, LTL_TRUE_def, 403 LTL_FALSE_def, LTL_INIT_def, LTL_PALWAYS_def, LTL_PEVENTUAL_def, LTL_WHILE_def, 404 LTL_SWHILE_def, LTL_PSWHILE_def, LTL_PWHILE_def, LTL_BEFORE_def, LTL_SBEFORE_def, 405 LTL_PSBEFORE_def, LTL_PBEFORE_def, P_USED_VARS_EVAL, UNION_EMPTY] THEN 406 SIMP_TAC std_ss [EXTENSION, IN_UNION] THEN 407 PROVE_TAC[]); 408 409 410val LTL_VAR_RENAMING_def= 411 Define 412 `(LTL_VAR_RENAMING f (LTL_PROP p) = LTL_PROP (P_VAR_RENAMING f p)) /\ 413 (LTL_VAR_RENAMING f (LTL_NOT r) = LTL_NOT (LTL_VAR_RENAMING f r)) /\ 414 (LTL_VAR_RENAMING f (LTL_AND (r1,r2)) = LTL_AND(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 415 (LTL_VAR_RENAMING f (LTL_NEXT r) = LTL_NEXT (LTL_VAR_RENAMING f r)) /\ 416 (LTL_VAR_RENAMING f (LTL_SUNTIL(r1,r2)) = LTL_SUNTIL(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 417 (LTL_VAR_RENAMING f (LTL_PSNEXT r) = LTL_PSNEXT (LTL_VAR_RENAMING f r)) /\ 418 (LTL_VAR_RENAMING f (LTL_PSUNTIL(r1,r2)) = LTL_PSUNTIL(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2))`; 419 420 421val LTL_SEM_TIME___VAR_RENAMING___NOT_INJ = 422 store_thm 423 ("LTL_SEM_TIME___VAR_RENAMING___NOT_INJ", 424 ``!f' t v f. (LTL_SEM_TIME t v (LTL_VAR_RENAMING f f')) = 425 (LTL_SEM_TIME t (\n x. f x IN v n) f')``, 426 427 INDUCT_THEN ltl_induct ASSUME_TAC THEN ( 428 ASM_SIMP_TAC std_ss [LTL_VAR_RENAMING_def, LTL_SEM_TIME_def, P_SEM___VAR_RENAMING___NOT_INJ] 429 )) 430 431val LTL_SEM_TIME___VAR_RENAMING = 432 store_thm 433 ("LTL_SEM_TIME___VAR_RENAMING", 434 ``!f' t v f. (INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f') UNIV) ==> ((LTL_SEM_TIME t v f') = (LTL_SEM_TIME t 435 (PATH_VAR_RENAMING f v) (LTL_VAR_RENAMING f f')))``, 436 437 438 INDUCT_THEN ltl_induct ASSUME_TAC THENL [ 439 SIMP_TAC std_ss [LTL_SEM_TIME_def, 440 LTL_VAR_RENAMING_def, PATH_VAR_RENAMING_def, 441 PATH_MAP_def] THEN 442 REPEAT STRIP_TAC THEN 443 MATCH_MP_TAC P_SEM___VAR_RENAMING THEN 444 UNDISCH_HD_TAC THEN 445 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 446 REWRITE_TAC [SUBSET_DEF, IN_UNION, LTL_USED_VARS_def, 447 GSYM PATH_USED_VARS_THM] THEN 448 PROVE_TAC[], 449 450 451 ASM_SIMP_TAC std_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, 452 LTL_VAR_RENAMING_def], 453 454 455 SIMP_TAC std_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, 456 LTL_VAR_RENAMING_def] THEN 457 REPEAT STRIP_TAC THEN 458 REMAINS_TAC `INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f'') UNIV /\ 459 INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f') UNIV` THEN1 ( 460 RES_TAC THEN 461 ASM_REWRITE_TAC[] 462 ) THEN 463 NTAC 2 (WEAKEN_NO_TAC 1) THEN 464 STRIP_TAC THEN 465 UNDISCH_HD_TAC THEN 466 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 467 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 468 PROVE_TAC[], 469 470 471 ASM_SIMP_TAC std_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, 472 LTL_VAR_RENAMING_def], 473 474 475 SIMP_TAC std_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, 476 LTL_VAR_RENAMING_def] THEN 477 REPEAT STRIP_TAC THEN 478 REMAINS_TAC `INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f'') UNIV /\ 479 INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f') UNIV` THEN1 ( 480 RES_TAC THEN 481 ASM_REWRITE_TAC[] 482 ) THEN 483 NTAC 2 (WEAKEN_NO_TAC 1) THEN 484 STRIP_TAC THEN 485 UNDISCH_HD_TAC THEN 486 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 487 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 488 PROVE_TAC[], 489 490 491 SIMP_TAC std_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, 492 LTL_VAR_RENAMING_def] THEN 493 Cases_on `t` THENL [ 494 SIMP_TAC std_ss [], 495 ASM_SIMP_TAC std_ss [] 496 ], 497 498 499 SIMP_TAC std_ss [LTL_SEM_TIME_def, LTL_USED_VARS_def, 500 LTL_VAR_RENAMING_def] THEN 501 REPEAT STRIP_TAC THEN 502 REMAINS_TAC `INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f'') UNIV /\ 503 INJ f (PATH_USED_VARS v UNION LTL_USED_VARS f') UNIV` THEN1 ( 504 RES_TAC THEN 505 ASM_REWRITE_TAC[] 506 ) THEN 507 NTAC 2 (WEAKEN_NO_TAC 1) THEN 508 STRIP_TAC THEN 509 UNDISCH_HD_TAC THEN 510 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 511 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] THEN 512 PROVE_TAC[] 513 ]); 514 515 516 517 518val LTL_SEM_TIME___VAR_RENAMING___PATH_RESTRICT = 519 store_thm 520 ("LTL_SEM_TIME___VAR_RENAMING___PATH_RESTRICT", 521 ``!f' t v f. (INJ f (LTL_USED_VARS f') UNIV) ==> ((LTL_SEM_TIME t v f') = (LTL_SEM_TIME t 522 (PATH_VAR_RENAMING f (PATH_RESTRICT v (LTL_USED_VARS f'))) (LTL_VAR_RENAMING f f')))``, 523 524 REPEAT STRIP_TAC THEN 525 CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [LTL_USED_VARS_INTER_THM])) THEN 526 MATCH_MP_TAC LTL_SEM_TIME___VAR_RENAMING THEN 527 UNDISCH_HD_TAC THEN 528 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 529 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, GSYM PATH_USED_VARS_THM, 530 PATH_RESTRICT_def, PATH_MAP_def, IN_INTER] THEN 531 PROVE_TAC[]); 532 533 534 535val FUTURE_LTL_CONSIDERS_ONLY_FUTURE = 536 store_thm 537 ("FUTURE_LTL_CONSIDERS_ONLY_FUTURE", 538 ``!f t v. IS_FUTURE_LTL f ==> (LTL_SEM_TIME t v f <=> LTL_SEM (\t'. v (t'+t)) f)``, 539 540INDUCT_THEN ltl_induct ASSUME_TAC THEN ( 541 SIMP_TAC std_ss [IS_FUTURE_LTL_def, LTL_SEM_TIME_def, LTL_SEM_def] THEN 542 REWRITE_TAC [GSYM LTL_SEM_def] THEN 543 ASM_SIMP_TAC std_ss [] 544) THENL [ 545 (* NEXT *) 546 ASM_SIMP_TAC arith_ss [arithmeticTheory.ADD1], 547 548 (* SUNTIL *) 549 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 550 Q.EXISTS_TAC `k - t` THEN 551 FULL_SIMP_TAC arith_ss [] THEN 552 REPEAT STRIP_TAC THEN 553 Q.PAT_X_ASSUM `!j. _` (MP_TAC o Q.SPEC `j+t`) THEN 554 FULL_SIMP_TAC arith_ss [], 555 556 Q.EXISTS_TAC `k + t` THEN 557 FULL_SIMP_TAC arith_ss [] THEN 558 REPEAT STRIP_TAC THEN 559 Q.PAT_X_ASSUM `!j. _` (MP_TAC o Q.SPEC `j-t`) THEN 560 FULL_SIMP_TAC arith_ss [] 561 ] 562]); 563 564 565val FUTURE_LTL_EQUIVALENT_INITIAL_IS_EQUIVALENT = 566 store_thm 567 ("FUTURE_LTL_EQUIVALENT_INIT_IS_EQUIVALENT", 568 ``!l1 l2. IS_FUTURE_LTL l1 /\ IS_FUTURE_LTL l2 ==> 569 (LTL_EQUIVALENT_INITIAL l1 l2 <=> LTL_EQUIVALENT l1 l2)``, 570 571SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, 572 LTL_EQUIVALENT_def, FUTURE_LTL_CONSIDERS_ONLY_FUTURE] THEN 573REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN1 ( 574 ASM_SIMP_TAC std_ss [] 575) THEN 576Q.PAT_X_ASSUM `!t w. _` (MP_TAC o Q.SPECL [`0`, `w`]) THEN 577ASM_SIMP_TAC std_ss [ETA_THM]); 578 579 580val LTL_OR_SEM = 581 store_thm 582 ("LTL_OR_SEM", 583 ``!v.!f1.!f2.!t.((LTL_SEM_TIME t v (LTL_OR(f1,f2))) = ((LTL_SEM_TIME t v f1) \/ (LTL_SEM_TIME t v f2)))``, 584 REWRITE_TAC[LTL_OR_def, LTL_SEM_TIME_def] THEN SIMP_TAC arith_ss []); 585 586 587val LTL_IMPL_SEM = 588 store_thm 589 ("LTL_IMPL_SEM", 590 ``!v.!f1.!f2.!t.((LTL_SEM_TIME t v (LTL_IMPL(f1,f2))) = ((LTL_SEM_TIME t v f1) ==> (LTL_SEM_TIME t v f2)))``, 591 REWRITE_TAC[LTL_OR_def, LTL_IMPL_def, LTL_SEM_TIME_def] THEN METIS_TAC[]); 592 593 594val LTL_EQUIV_SEM = 595 store_thm 596 ("LTL_EQUIV_SEM", 597 ``!v.!f1.!f2.!t.((LTL_SEM_TIME t v (LTL_EQUIV(f1,f2))) = ((LTL_SEM_TIME t v f1) = (LTL_SEM_TIME t v f2)))``, 598 REWRITE_TAC[LTL_EQUIV_def, LTL_IMPL_SEM, LTL_SEM_TIME_def] THEN METIS_TAC[]); 599 600 601val LTL_SBEFORE_SEM = 602 store_thm 603 ("LTL_SBEFORE_SEM", 604 ``!v.!f1.!f2.!t. ((LTL_SEM_TIME t v (LTL_SBEFORE(f1,f2))) = ( 605 ?k. (k >= t /\ (LTL_SEM_TIME k v f1) /\ (!j. ((t <= j) /\ (j <= k)) ==> 606 (~(LTL_SEM_TIME j v f2))))))``, 607 REWRITE_TAC[LTL_SBEFORE_def, LTL_SEM_TIME_def] THEN 608 REPEAT STRIP_TAC THEN 609 EXISTS_EQ_STRIP_TAC THEN 610 REPEAT BOOL_EQ_STRIP_TAC THEN 611 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 612 Cases_on `j < k` THENL [ 613 PROVE_TAC[], 614 615 `j = k` by DECIDE_TAC THEN 616 PROVE_TAC[] 617 ], 618 619 `t <= k /\ k <= k` by DECIDE_TAC THEN 620 PROVE_TAC[], 621 622 `j <= k` by DECIDE_TAC THEN 623 PROVE_TAC[] 624 ]); 625 626 627val LTL_PSBEFORE_SEM = 628 store_thm 629 ("LTL_PSBEFORE_SEM", 630 ``!v.!f1.!f2.!t. ((LTL_SEM_TIME t v (LTL_PSBEFORE(f1,f2))) = ( 631 ?k. (k <= t /\ (LTL_SEM_TIME k v f1) /\ (!j. ((k <= j) /\ (j <= t)) ==> 632 (~(LTL_SEM_TIME j v f2))))))``, 633 REWRITE_TAC[LTL_PSBEFORE_def, LTL_SEM_TIME_def] THEN 634 REPEAT STRIP_TAC THEN 635 EXISTS_EQ_STRIP_TAC THEN 636 REPEAT BOOL_EQ_STRIP_TAC THEN 637 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 638 Cases_on `k < j` THENL [ 639 PROVE_TAC[], 640 641 `j = k` by DECIDE_TAC THEN 642 PROVE_TAC[] 643 ], 644 645 `k <= k` by DECIDE_TAC THEN 646 PROVE_TAC[], 647 648 `k <= j` by DECIDE_TAC THEN 649 PROVE_TAC[] 650 ]); 651 652 653val LTL_EVENTUAL_SEM = 654 store_thm 655 ("LTL_EVENTUAL_SEM", 656 ``!v.!f.!t.(LTL_SEM_TIME t v (LTL_EVENTUAL f) = (?k. (k >= t) /\ (LTL_SEM_TIME k v f)))``, 657 EVAL_TAC THEN SIMP_TAC arith_ss [P_SEM_THM]); 658 659 660val LTL_ALWAYS_SEM = 661 store_thm 662 ("LTL_ALWAYS_SEM", 663 ``!v.!f.!t. (LTL_SEM_TIME t v (LTL_ALWAYS f) = (!k. (k >= t) ==> (LTL_SEM_TIME k v f)))``, 664 EVAL_TAC THEN SIMP_TAC arith_ss [P_SEM_THM] THEN 665 PROVE_TAC[]); 666 667 668val LTL_PEVENTUAL_SEM = 669 store_thm 670 ("LTL_PEVENTUAL_SEM", 671 ``!v.!f.!t.(LTL_SEM_TIME t v (LTL_PEVENTUAL f) = (?k:num. (0 <= k /\ k <= t) /\ (LTL_SEM_TIME k v f)))``, 672 EVAL_TAC THEN SIMP_TAC arith_ss [P_SEM_THM]); 673 674 675val LTL_PALWAYS_SEM = 676 store_thm 677 ("LTL_PALWAYS_SEM", 678 ``!v.!f.!t. (LTL_SEM_TIME t v (LTL_PALWAYS f) = (!k. (k <= t) ==> (LTL_SEM_TIME k v f)))``, 679 EVAL_TAC THEN SIMP_TAC arith_ss [P_SEM_THM] THEN 680 PROVE_TAC[]); 681 682 683val LTL_PNEXT_SEM = 684 store_thm 685 ("LTL_PNEXT_SEM", 686 ``!v.!f.!t. (LTL_SEM_TIME t v (LTL_PNEXT f) = ((t = 0) \/ LTL_SEM_TIME (PRE t) v f))``, 687 EVAL_TAC THEN SIMP_TAC arith_ss [P_SEM_THM] THEN 688 `!t:num. (~(t > 0)) = (t = 0)` by DECIDE_TAC THEN 689 PROVE_TAC[]); 690 691val LTL_TRUE_SEM = 692 store_thm 693 ("LTL_TRUE_SEM", 694 ``!v t. LTL_SEM_TIME t v LTL_TRUE``, 695 REWRITE_TAC[LTL_TRUE_def, LTL_SEM_TIME_def, P_SEM_THM]); 696 697 698val LTL_FALSE_SEM = 699 store_thm 700 ("LTL_FALSE_SEM", 701 ``!v t. ~(LTL_SEM_TIME t v LTL_FALSE)``, 702 REWRITE_TAC[LTL_FALSE_def, LTL_SEM_TIME_def, P_SEM_THM]); 703 704 705val LTL_INIT_SEM = 706 store_thm 707 ("LTL_INIT_SEM", 708 ``!t v. (LTL_SEM_TIME t v LTL_INIT) = (t = 0)``, 709 710 REWRITE_TAC[LTL_INIT_def, LTL_SEM_TIME_def, P_SEM_def] THEN 711 DECIDE_TAC); 712 713 714val LTL_SEM_THM = LIST_CONJ [LTL_SEM_def, 715 LTL_SEM_TIME_def, 716 LTL_OR_SEM, 717 LTL_IMPL_SEM, 718 LTL_EQUIV_SEM, 719 LTL_ALWAYS_SEM, 720 LTL_EVENTUAL_SEM, 721 LTL_PNEXT_SEM, 722 LTL_PEVENTUAL_SEM, 723 LTL_PALWAYS_SEM, 724 LTL_TRUE_SEM, 725 LTL_FALSE_SEM, 726 LTL_INIT_SEM, 727 LTL_SBEFORE_SEM, 728 LTL_PSBEFORE_SEM]; 729val _ = save_thm("LTL_SEM_THM",LTL_SEM_THM); 730 731 732val LTL_VAR_RENAMING_EVAL= 733 store_thm ("LTL_VAR_RENAMING_EVAL", 734 ``(LTL_VAR_RENAMING f (LTL_PROP p) = LTL_PROP (P_VAR_RENAMING f p)) /\ 735 (LTL_VAR_RENAMING f (LTL_NOT r) = LTL_NOT (LTL_VAR_RENAMING f r)) /\ 736 (LTL_VAR_RENAMING f (LTL_AND (r1,r2)) = LTL_AND(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 737 (LTL_VAR_RENAMING f (LTL_NEXT r) = LTL_NEXT (LTL_VAR_RENAMING f r)) /\ 738 (LTL_VAR_RENAMING f (LTL_SUNTIL(r1,r2)) = LTL_SUNTIL(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 739 (LTL_VAR_RENAMING f (LTL_PSNEXT r) = LTL_PSNEXT (LTL_VAR_RENAMING f r)) /\ 740 (LTL_VAR_RENAMING f (LTL_PSUNTIL(r1,r2)) = LTL_PSUNTIL(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 741 (LTL_VAR_RENAMING f (LTL_OR (r1,r2)) = LTL_OR(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 742 (LTL_VAR_RENAMING f (LTL_IMPL (r1,r2)) = LTL_IMPL(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 743 (LTL_VAR_RENAMING f (LTL_EQUIV (r1,r2)) = LTL_EQUIV(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 744 (LTL_VAR_RENAMING f (LTL_ALWAYS r) = LTL_ALWAYS (LTL_VAR_RENAMING f r)) /\ 745 (LTL_VAR_RENAMING f (LTL_EVENTUAL r) = LTL_EVENTUAL (LTL_VAR_RENAMING f r)) /\ 746 (LTL_VAR_RENAMING f (LTL_PNEXT r) = LTL_PNEXT (LTL_VAR_RENAMING f r)) /\ 747 (LTL_VAR_RENAMING f LTL_TRUE = LTL_TRUE) /\ 748 (LTL_VAR_RENAMING f LTL_FALSE = LTL_FALSE) /\ 749 (LTL_VAR_RENAMING f LTL_INIT = LTL_INIT) /\ 750 (LTL_VAR_RENAMING f (LTL_PALWAYS r) = LTL_PALWAYS (LTL_VAR_RENAMING f r)) /\ 751 (LTL_VAR_RENAMING f (LTL_PEVENTUAL r) = LTL_PEVENTUAL (LTL_VAR_RENAMING f r)) /\ 752 (LTL_VAR_RENAMING f (LTL_WHILE (r1,r2)) = LTL_WHILE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 753 (LTL_VAR_RENAMING f (LTL_BEFORE (r1,r2)) = LTL_BEFORE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 754 (LTL_VAR_RENAMING f (LTL_SWHILE (r1,r2)) = LTL_SWHILE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 755 (LTL_VAR_RENAMING f (LTL_SBEFORE (r1,r2)) = LTL_SBEFORE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 756 (LTL_VAR_RENAMING f (LTL_PWHILE (r1,r2)) = LTL_PWHILE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 757 (LTL_VAR_RENAMING f (LTL_PBEFORE (r1,r2)) = LTL_PBEFORE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 758 (LTL_VAR_RENAMING f (LTL_PSWHILE (r1,r2)) = LTL_PSWHILE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2)) /\ 759 (LTL_VAR_RENAMING f (LTL_PSBEFORE (r1,r2)) = LTL_PSBEFORE(LTL_VAR_RENAMING f r1, LTL_VAR_RENAMING f r2))``, 760 761 SIMP_TAC std_ss [LTL_VAR_RENAMING_def, LTL_OR_def, LTL_IMPL_def, LTL_EQUIV_def, 762 LTL_ALWAYS_def, LTL_EVENTUAL_def, P_VAR_RENAMING_EVAL, LTL_PNEXT_def, LTL_TRUE_def, 763 LTL_FALSE_def, LTL_INIT_def, LTL_PALWAYS_def, LTL_PEVENTUAL_def, LTL_WHILE_def, 764 LTL_SWHILE_def, LTL_PSWHILE_def, LTL_PWHILE_def, LTL_BEFORE_def, LTL_SBEFORE_def, 765 LTL_PSBEFORE_def, LTL_PBEFORE_def]); 766 767 768(*LTL_ALWAYS is usually defined as NOT EVENTUAL. However, this is simplified by 769 the nnf rewrites defined in temporal_deep_simplifiactionsLib to ALWAYS again. Thus, the simplifier may loop. Therefore, here are 770 direct definitions of ALWAYS and PALWAYS to use with the nnf rewrites*) 771val LTL_ALWAYS_PALWAYS_ALTERNATIVE_DEFS = 772 store_thm ( 773 "LTL_ALWAYS_PALWAYS_ALTERNATIVE_DEFS", 774 ``(!l. (LTL_ALWAYS l) = (LTL_NOT (LTL_SUNTIL (LTL_TRUE, LTL_NOT l)))) /\ 775 (!l. (LTL_PALWAYS l) = (LTL_NOT (LTL_PSUNTIL (LTL_TRUE, LTL_NOT l))))``, 776 777 SIMP_TAC std_ss [LTL_ALWAYS_def, LTL_EVENTUAL_def, LTL_TRUE_def, 778 LTL_PALWAYS_def, LTL_PEVENTUAL_def]); 779 780 781val LTL_IS_CONTRADICTION_def = 782 Define 783 `LTL_IS_CONTRADICTION l = (!v. ~(LTL_SEM v l))`; 784 785val LTL_IS_TAUTOLOGY_def = 786 Define 787 `LTL_IS_TAUTOLOGY l = (!v. LTL_SEM v l)`; 788 789 790val LTL_TAUTOLOGY_CONTRADICTION_DUAL = 791 store_thm 792 ("LTL_TAUTOLOGY_CONTRADICTION_DUAL", 793 794 ``(!l. LTL_IS_CONTRADICTION (LTL_NOT l) = LTL_IS_TAUTOLOGY l) /\ 795 (!l. LTL_IS_TAUTOLOGY (LTL_NOT l) = LTL_IS_CONTRADICTION l)``, 796 797 REWRITE_TAC[LTL_IS_TAUTOLOGY_def, LTL_IS_CONTRADICTION_def, LTL_SEM_TIME_def, 798 LTL_SEM_def]); 799 800 801val LTL_TAUTOLOGY_CONTRADICTION___TO___EQUIVALENT_INITIAL = 802 store_thm 803 ("LTL_TAUTOLOGY_CONTRADICTION___TO___EQUIVALENT_INITIAL", 804 805 ``(!l. LTL_IS_CONTRADICTION l = LTL_EQUIVALENT_INITIAL l LTL_FALSE) /\ 806 (!l. LTL_IS_TAUTOLOGY l = LTL_EQUIVALENT_INITIAL l LTL_TRUE)``, 807 808 REWRITE_TAC[LTL_IS_TAUTOLOGY_def, LTL_IS_CONTRADICTION_def, LTL_SEM_THM, 809 LTL_EQUIVALENT_INITIAL_def] THEN 810 PROVE_TAC[]); 811 812 813val LTL_EQUIVALENT_INITIAL___TO___TAUTOLOGY = 814 store_thm 815 ("LTL_EQUIVALENT_INITIAL___TO___TAUTOLOGY", 816 817 ``!l1 l2. LTL_EQUIVALENT_INITIAL l1 l2 = LTL_IS_TAUTOLOGY (LTL_EQUIV(l1, l2))``, 818 819 REWRITE_TAC[LTL_IS_TAUTOLOGY_def, LTL_SEM_THM, 820 LTL_EQUIVALENT_INITIAL_def] THEN 821 PROVE_TAC[]); 822 823val LTL_EQUIVALENT_INITIAL___TO___CONTRADICTION = 824 store_thm 825 ("LTL_EQUIVALENT_INITIAL___TO___CONTRADICTION", 826 827 ``!l1 l2. LTL_EQUIVALENT_INITIAL l1 l2 = LTL_IS_CONTRADICTION (LTL_NOT (LTL_EQUIV(l1, l2)))``, 828 829 REWRITE_TAC[LTL_TAUTOLOGY_CONTRADICTION_DUAL, 830 LTL_EQUIVALENT_INITIAL___TO___TAUTOLOGY]); 831 832val LTL_EQUIVALENT___TO___CONTRADICTION = 833 store_thm 834 ("LTL_EQUIVALENT___TO___CONTRADICTION", 835 836 ``!l1 l2. LTL_EQUIVALENT l1 l2 = 837 LTL_IS_CONTRADICTION (LTL_EVENTUAL (LTL_NOT (LTL_EQUIV (l1,l2))))``, 838 839 SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_IS_CONTRADICTION_def, 840 LTL_SEM_THM] THEN 841 PROVE_TAC[]); 842 843 844val LTL_CONTRADICTION___VAR_RENAMING = 845 store_thm 846 ("LTL_CONTRADICTION___VAR_RENAMING", 847 ``!f' f. (INJ f (LTL_USED_VARS f') UNIV) ==> (LTL_IS_CONTRADICTION f' = LTL_IS_CONTRADICTION (LTL_VAR_RENAMING f f'))``, 848 849 SIMP_TAC std_ss [LTL_IS_CONTRADICTION_def, 850 LTL_SEM_def] THEN 851 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 852 SIMP_TAC std_ss [LTL_SEM_TIME___VAR_RENAMING___NOT_INJ], 853 PROVE_TAC[LTL_SEM_TIME___VAR_RENAMING___PATH_RESTRICT] 854 ]); 855 856 857val LTL_KS_SEM___VAR_RENAMING = 858 store_thm 859 ("LTL_KS_SEM___VAR_RENAMING", 860 ``!f' M f. (INJ f (LTL_USED_VARS f' UNION (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)) UNIV) ==> (LTL_KS_SEM M f' = LTL_KS_SEM 861 (SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING f M) 862 (LTL_VAR_RENAMING f f'))``, 863 864 SIMP_TAC std_ss [LTL_KS_SEM_def, LTL_SEM_def, 865 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 866 SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING_def, 867 symbolic_kripke_structure_REWRITES] THEN 868 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 869 SIMP_ALL_TAC std_ss [P_SEM___VAR_RENAMING___NOT_INJ, 870 XP_SEM___VAR_RENAMING___NOT_INJ, 871 LTL_SEM_TIME___VAR_RENAMING___NOT_INJ] THEN 872 Q_SPEC_NO_ASSUM 2 `(\n x. f x IN p n)` THEN 873 UNDISCH_HD_TAC THEN 874 ASM_SIMP_TAC std_ss [], 875 876 877 `?w. w = PATH_RESTRICT p (LTL_USED_VARS f' UNION SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)` by PROVE_TAC[] THEN 878 SUBGOAL_TAC `(LTL_SEM_TIME 0 p f' = LTL_SEM_TIME 0 w f') /\ 879 (P_SEM (p 0) M.S0 = P_SEM (w 0) M.S0) /\ 880 !n. (XP_SEM M.R (p n,p (SUC n)) = XP_SEM M.R (w n,w (SUC n)))` THEN1 ( 881 REPEAT STRIP_TAC THENL [ 882 ASM_REWRITE_TAC[] THEN 883 MATCH_MP_TAC LTL_USED_VARS_INTER_SUBSET_THM THEN 884 SIMP_TAC std_ss [SUBSET_UNION], 885 886 UNDISCH_HD_TAC THEN 887 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 888 DISCH_TAC THEN 889 MATCH_MP_TAC P_USED_VARS_INTER_SUBSET_THM THEN 890 SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, SUBSET_DEF, 891 IN_UNION], 892 893 UNDISCH_HD_TAC THEN 894 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 895 DISCH_TAC THEN 896 MATCH_MP_TAC XP_USED_VARS_INTER_SUBSET_BOTH_THM THEN 897 SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, SUBSET_DEF, 898 IN_UNION] 899 ] 900 ) THEN 901 `!n. w n SUBSET (LTL_USED_VARS f' UNION SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)` by METIS_TAC[PATH_RESTRICT_SUBSET] THEN 902 GSYM_NO_TAC 4 THEN 903 904 FULL_SIMP_TAC std_ss [] THEN NTAC 3 (WEAKEN_NO_TAC 2) THEN 905 906 907 Q_SPEC_NO_ASSUM 4 `PATH_VAR_RENAMING f w` THEN 908 UNDISCH_HD_TAC THEN 909 REMAINS_TAC `(!n. 910 XP_SEM (XP_VAR_RENAMING f M.R) 911 (PATH_VAR_RENAMING f w n,PATH_VAR_RENAMING f w (SUC n)) = 912 XP_SEM M.R (w n, w (SUC n))) /\ 913 (P_SEM (PATH_VAR_RENAMING f w 0) (P_VAR_RENAMING f M.S0) = 914 P_SEM (w 0) M.S0) /\ 915 (LTL_SEM_TIME 0 (PATH_VAR_RENAMING f w) (LTL_VAR_RENAMING f f') = 916 LTL_SEM_TIME 0 w f')` THEN1 ( 917 FULL_SIMP_TAC std_ss [] 918 ) THEN 919 920 REPEAT STRIP_TAC THENL [ 921 SIMP_TAC std_ss [PATH_VAR_RENAMING_def, PATH_MAP_def] THEN 922 MATCH_MP_TAC (GSYM XP_SEM___VAR_RENAMING) THEN 923 UNDISCH_NO_TAC 4 THEN 924 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 925 SIMP_ALL_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 926 IN_UNION, SUBSET_DEF] THEN 927 PROVE_TAC[], 928 929 930 SIMP_TAC std_ss [PATH_VAR_RENAMING_def, PATH_MAP_def] THEN 931 MATCH_MP_TAC (GSYM P_SEM___VAR_RENAMING) THEN 932 UNDISCH_NO_TAC 4 THEN 933 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 934 SIMP_ALL_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 935 IN_UNION, SUBSET_DEF] THEN 936 PROVE_TAC[], 937 938 939 MATCH_MP_TAC (GSYM LTL_SEM_TIME___VAR_RENAMING) THEN 940 UNDISCH_NO_TAC 4 THEN 941 MATCH_MP_TAC INJ_SUBSET_DOMAIN THEN 942 SIMP_ALL_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 943 IN_UNION, SUBSET_DEF, GSYM PATH_USED_VARS_THM] THEN 944 PROVE_TAC[] 945 ] 946 ] 947 ); 948 949 950 951val LTL_RECURSION_LAWS___LTL_ALWAYS = 952 store_thm 953 ("LTL_RECURSION_LAWS___LTL_ALWAYS", 954 ``!f. LTL_EQUIVALENT (LTL_ALWAYS f) (LTL_AND(f, LTL_NEXT(LTL_ALWAYS f)))``, 955 956 REWRITE_TAC [LTL_EQUIVALENT_def, LTL_SEM_THM] THEN 957 REPEAT STRIP_TAC THEN 958 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 959 `t >= t` by DECIDE_TAC THEN 960 PROVE_TAC[], 961 962 `k >= t` by DECIDE_TAC THEN 963 PROVE_TAC[], 964 965 Cases_on `k = t` THENL [ 966 PROVE_TAC[], 967 968 `k >= SUC t` by DECIDE_TAC THEN 969 PROVE_TAC[] 970 ] 971 ]); 972 973 974val LTL_RECURSION_LAWS___LTL_EVENTUAL = 975 store_thm 976 ("LTL_RECURSION_LAWS___LTL_EVENTUAL", 977 ``!f. LTL_EQUIVALENT (LTL_EVENTUAL f) (LTL_OR(f, LTL_NEXT(LTL_EVENTUAL f)))``, 978 979 REWRITE_TAC [LTL_EQUIVALENT_def, LTL_SEM_THM] THEN 980 REPEAT STRIP_TAC THEN 981 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 982 Cases_on `k = t` THENL [ 983 PROVE_TAC[], 984 985 `k >= SUC t` by DECIDE_TAC THEN 986 PROVE_TAC[] 987 ], 988 989 `t >= t` by DECIDE_TAC THEN 990 PROVE_TAC[], 991 992 `k >= t` by DECIDE_TAC THEN 993 PROVE_TAC[] 994 ]); 995 996 997 998val LTL_RECURSION_LAWS___LTL_SUNTIL = 999 store_thm 1000 ("LTL_RECURSION_LAWS___LTL_SUNTIL", 1001 ``!l1 l2. LTL_EQUIVALENT (LTL_SUNTIL (l1, l2)) 1002 (LTL_OR(l2, LTL_AND(l1, LTL_NEXT(LTL_SUNTIL (l1, l2)))))``, 1003 1004 1005SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_SEM_THM] THEN 1006REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1007 Cases_on `k = t` THENL [ 1008 PROVE_TAC[], 1009 1010 DISJ2_TAC THEN 1011 REPEAT STRIP_TAC THENL [ 1012 `t <= t /\ t < k` by DECIDE_TAC THEN 1013 PROVE_TAC[], 1014 1015 EXISTS_TAC ``k:num`` THEN 1016 REPEAT STRIP_TAC THENL [ 1017 DECIDE_TAC, 1018 ASM_REWRITE_TAC[], 1019 `t <= j` by DECIDE_TAC THEN PROVE_TAC[] 1020 ] 1021 ] 1022 ], 1023 1024 1025 EXISTS_TAC ``t:num`` THEN 1026 ASM_SIMP_TAC arith_ss [], 1027 1028 1029 EXISTS_TAC ``k:num`` THEN 1030 ASM_SIMP_TAC arith_ss [] THEN 1031 REPEAT STRIP_TAC THEN 1032 Cases_on `j = t` THENL [ 1033 PROVE_TAC[], 1034 `SUC t <= j` by DECIDE_TAC THEN PROVE_TAC[] 1035 ] 1036]); 1037 1038 1039 1040val LTL_RECURSION_LAWS___LTL_PSUNTIL = 1041 store_thm 1042 ("LTL_RECURSION_LAWS___LTL_PSUNTIL", 1043 ``!l1 l2. LTL_EQUIVALENT (LTL_PSUNTIL (l1, l2)) 1044 (LTL_OR(l2, LTL_AND(l1, LTL_PSNEXT(LTL_PSUNTIL (l1, l2)))))``, 1045 1046 1047SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_SEM_THM] THEN 1048REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1049 Cases_on `k = t` THENL [ 1050 PROVE_TAC[], 1051 1052 DISJ2_TAC THEN 1053 Cases_on `t` THEN SIMP_ALL_TAC arith_ss [] THEN 1054 REPEAT STRIP_TAC THENL [ 1055 `SUC n <= SUC n /\ k < SUC n` by DECIDE_TAC THEN 1056 PROVE_TAC[], 1057 1058 EXISTS_TAC ``k:num`` THEN 1059 REPEAT STRIP_TAC THENL [ 1060 DECIDE_TAC, 1061 ASM_REWRITE_TAC[], 1062 `j <= SUC n` by DECIDE_TAC THEN PROVE_TAC[] 1063 ] 1064 ] 1065 ], 1066 1067 1068 EXISTS_TAC ``t:num`` THEN 1069 ASM_SIMP_TAC arith_ss [], 1070 1071 1072 EXISTS_TAC ``k:num`` THEN 1073 ASM_SIMP_TAC arith_ss [] THEN 1074 REPEAT STRIP_TAC THEN 1075 Cases_on `j = t` THENL [ 1076 PROVE_TAC[], 1077 `j <= PRE t` by DECIDE_TAC THEN PROVE_TAC[] 1078 ] 1079]); 1080 1081 1082val LTL_EVENTUAL___PALWAYS = 1083 store_thm 1084 ("LTL_EVENTUAL___PALWAYS", 1085 ``!k w p. (LTL_SEM_TIME k w (LTL_EVENTUAL p)) ==> 1086 (!l. l <= k ==> LTL_SEM_TIME l w (LTL_EVENTUAL p))``, 1087 1088 REWRITE_TAC[LTL_SEM_THM] THEN 1089 REPEAT STRIP_TAC THEN 1090 EXISTS_TAC ``k':num`` THEN 1091 ASM_REWRITE_TAC[] THEN 1092 DECIDE_TAC); 1093 1094 1095val LTL_WEAK_UNTIL___ALTERNATIVE_DEF = 1096 store_thm 1097 ("LTL_WEAK_UNTIL___ALTERNATIVE_DEF", 1098 ``!f1 f2. LTL_EQUIVALENT (LTL_UNTIL(f1,f2)) (LTL_NOT (LTL_SUNTIL(LTL_NOT f2, LTL_AND(LTL_NOT f1, LTL_NOT f2))))``, 1099 1100 SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_UNTIL_def, LTL_SEM_THM] THEN 1101 REPEAT STRIP_TAC THEN 1102 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1103 Cases_on `k < k'` THENL [ 1104 `t <= k` by DECIDE_TAC THEN 1105 METIS_TAC[], 1106 1107 Cases_on `~(k' >= t)` THEN1 ASM_REWRITE_TAC[] THEN 1108 Cases_on `k' = k` THEN1 ASM_REWRITE_TAC[] THEN 1109 `t <= k' /\ k' < k` by DECIDE_TAC THEN 1110 METIS_TAC[] 1111 ], 1112 1113 METIS_TAC[], 1114 1115 Cases_on `!k. k >= t ==> LTL_SEM_TIME k w f1` THENL [ 1116 PROVE_TAC[], 1117 1118 DISJ1_TAC THEN 1119 SIMP_ASSUMPTIONS_TAC std_ss [] THEN 1120 SUBGOAL_TAC `?k. (k >= t /\ ~LTL_SEM_TIME k w f1) /\ !k'. k' < k ==> ~(k' >= t /\ ~LTL_SEM_TIME k' w f1)` THEN1 ( 1121 ASSUME_TAC (EXISTS_LEAST_CONV ``?k. k >= t /\ ~LTL_SEM_TIME k w f1``) THEN 1122 RES_TAC THEN PROVE_TAC[] 1123 ) THEN 1124 SUBGOAL_TAC `?l:num. l >= t /\ l <= k' /\ LTL_SEM_TIME l w f2` THEN1 ( 1125 Cases_on `LTL_SEM_TIME k' w f2` THENL [ 1126 EXISTS_TAC ``k':num`` THEN 1127 ASM_SIMP_TAC arith_ss [], 1128 1129 `?j. t <= j /\ j < k' /\ LTL_SEM_TIME j w f2` by METIS_TAC[] THEN 1130 EXISTS_TAC ``j:num`` THEN 1131 ASM_SIMP_TAC arith_ss [] 1132 ] 1133 ) THEN 1134 EXISTS_TAC ``l:num`` THEN 1135 ASM_SIMP_TAC arith_ss [] THEN 1136 REPEAT STRIP_TAC THEN 1137 `j < k' /\ j >= t` by DECIDE_TAC THEN 1138 METIS_TAC[] 1139 ] 1140 ]); 1141 1142 1143 1144val LTL_PAST_WEAK_UNTIL___ALTERNATIVE_DEF = 1145 store_thm 1146 ("LTL_PAST_WEAK_UNTIL___ALTERNATIVE_DEF", 1147 ``!f1 f2. LTL_EQUIVALENT (LTL_PUNTIL(f1,f2)) (LTL_NOT (LTL_PSUNTIL(LTL_NOT f2, LTL_AND(LTL_NOT f1, LTL_NOT f2))))``, 1148 1149 SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_PUNTIL_def, LTL_SEM_THM] THEN 1150 REPEAT STRIP_TAC THEN 1151 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1152 Cases_on `k' < k` THENL [ 1153 `k' < k` by DECIDE_TAC THEN 1154 METIS_TAC[], 1155 1156 Cases_on `~(k' <= t)` THEN1 ASM_REWRITE_TAC[] THEN 1157 Cases_on `k' = k` THEN1 ASM_REWRITE_TAC[] THEN 1158 `k < k'` by DECIDE_TAC THEN 1159 METIS_TAC[] 1160 ], 1161 1162 METIS_TAC[], 1163 1164 LEFT_DISJ_TAC THEN 1165 SIMP_ALL_TAC std_ss [] THEN 1166 `?P. P = \k. k <= t /\ ~(LTL_SEM_TIME k w f1)` by METIS_TAC[] THEN 1167 SUBGOAL_TAC `?x. P x /\ !z. z > x ==> ~(P z)` THEN1 ( 1168 ASM_SIMP_TAC std_ss [GSYM arithmeticTheory.EXISTS_GREATEST] THEN 1169 REPEAT STRIP_TAC THENL [ 1170 METIS_TAC[], 1171 1172 Q_TAC EXISTS_TAC `t` THEN 1173 SIMP_TAC arith_ss [] 1174 ] 1175 ) THEN 1176 NTAC 2 (UNDISCH_HD_TAC) THEN 1177 ASM_SIMP_TAC std_ss [] THEN 1178 REPEAT STRIP_TAC THEN 1179 SUBGOAL_TAC `?x'. (x' >= x) /\ (x' <= t) /\ LTL_SEM_TIME x' w f2` THEN1 ( 1180 Q_SPEC_NO_ASSUM 6 `x` THEN 1181 CLEAN_ASSUMPTIONS_TAC THENL [ 1182 EXISTS_TAC ``x:num`` THEN 1183 ASM_SIMP_TAC arith_ss [], 1184 1185 EXISTS_TAC ``j:num`` THEN 1186 ASM_SIMP_TAC arith_ss [] 1187 ] 1188 ) THEN 1189 Q_TAC EXISTS_TAC `x'` THEN 1190 ASM_SIMP_TAC arith_ss [] THEN 1191 REPEAT STRIP_TAC THEN 1192 `j > x` by DECIDE_TAC THEN 1193 METIS_TAC[] 1194 ]); 1195 1196 1197 1198val LTL_STRONG___WEAK__IMPL___UNTIL = 1199 store_thm 1200 ("LTL_STRONG___WEAK__IMPL___UNTIL", 1201 ``!k w p1 p2. 1202 ((LTL_SEM_TIME k w (LTL_SUNTIL(p1, p2))) ==> (LTL_SEM_TIME k w (LTL_UNTIL(p1, p2))))``, 1203 1204 REWRITE_TAC[LTL_UNTIL_def, LTL_OR_SEM] THEN 1205 PROVE_TAC[]); 1206 1207 1208val LTL_COND___OR = 1209 store_thm 1210 ("LTL_COND___OR", 1211 ``!k w c p1 p2. (LTL_SEM_TIME k w (LTL_COND (c, p1, p2))) ==> 1212 (LTL_SEM_TIME k w (LTL_OR (p1, p2)))``, 1213 1214 REWRITE_TAC[LTL_SEM_THM, LTL_COND_def] THEN 1215 METIS_TAC[]); 1216 1217 1218val LTL_MONOTICITY_LAWS = 1219 store_thm 1220 ("LTL_MONOTICITY_LAWS", 1221 ``!As Aw Bs Bw v. ((!t. LTL_SEM_TIME t v Aw ==> LTL_SEM_TIME t v As) /\ 1222 (!t. LTL_SEM_TIME t v Bw ==> LTL_SEM_TIME t v Bs)) ==> ( 1223 1224 (!t. LTL_SEM_TIME t v (LTL_NOT As) ==> LTL_SEM_TIME t v (LTL_NOT Aw)) /\ 1225 (!t. LTL_SEM_TIME t v (LTL_NEXT Aw) ==> LTL_SEM_TIME t v (LTL_NEXT As)) /\ 1226 (!t. LTL_SEM_TIME t v (LTL_AND(Aw, Bw)) ==> LTL_SEM_TIME t v (LTL_AND(As, Bs))) /\ 1227 (!t. LTL_SEM_TIME t v (LTL_OR(Aw, Bw)) ==> LTL_SEM_TIME t v (LTL_OR(As, Bs))) /\ 1228 (!t. LTL_SEM_TIME t v (LTL_ALWAYS Aw) ==> LTL_SEM_TIME t v (LTL_ALWAYS As)) /\ 1229 (!t. LTL_SEM_TIME t v (LTL_EVENTUAL Aw) ==> LTL_SEM_TIME t v (LTL_EVENTUAL As)) /\ 1230 (!t. LTL_SEM_TIME t v (LTL_UNTIL(Aw, Bw)) ==> LTL_SEM_TIME t v (LTL_UNTIL(As, Bs))) /\ 1231 (!t. LTL_SEM_TIME t v (LTL_SUNTIL(Aw, Bw)) ==> LTL_SEM_TIME t v (LTL_SUNTIL(As, Bs))) /\ 1232 (!t. LTL_SEM_TIME t v (LTL_BEFORE(Aw, Bs)) ==> LTL_SEM_TIME t v (LTL_BEFORE(As, Bw))) /\ 1233 (!t. LTL_SEM_TIME t v (LTL_SBEFORE(Aw, Bs)) ==> LTL_SEM_TIME t v (LTL_SBEFORE(As, Bw))) /\ 1234 (!t. LTL_SEM_TIME t v (LTL_PNEXT Aw) ==> LTL_SEM_TIME t v (LTL_PNEXT As)) /\ 1235 (!t. LTL_SEM_TIME t v (LTL_PSNEXT Aw) ==> LTL_SEM_TIME t v (LTL_PSNEXT As)) /\ 1236 (!t. LTL_SEM_TIME t v (LTL_PALWAYS Aw) ==> LTL_SEM_TIME t v (LTL_PALWAYS As)) /\ 1237 (!t. LTL_SEM_TIME t v (LTL_PEVENTUAL Aw) ==> LTL_SEM_TIME t v (LTL_PEVENTUAL As)) /\ 1238 (!t. LTL_SEM_TIME t v (LTL_PUNTIL(Aw, Bw)) ==> LTL_SEM_TIME t v (LTL_PUNTIL(As, Bs))) /\ 1239 (!t. LTL_SEM_TIME t v (LTL_PSUNTIL(Aw, Bw)) ==> LTL_SEM_TIME t v (LTL_PSUNTIL(As, Bs))) /\ 1240 (!t. LTL_SEM_TIME t v (LTL_PBEFORE(Aw, Bs)) ==> LTL_SEM_TIME t v (LTL_PBEFORE(As, Bw))) /\ 1241 (!t. LTL_SEM_TIME t v (LTL_PSBEFORE(Aw, Bs)) ==> LTL_SEM_TIME t v (LTL_PSBEFORE(As, Bw))) 1242 ) 1243 ``, 1244 1245 REWRITE_TAC[LTL_SEM_THM, LTL_UNTIL_def, LTL_BEFORE_def, LTL_SBEFORE_def, 1246 LTL_PUNTIL_def, LTL_PBEFORE_def, LTL_PSBEFORE_def] THEN 1247 METIS_TAC[] 1248 ); 1249 1250 1251val _ = export_theory(); 1252