1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val hol_dir = concat Globals.HOLDIR "/"; 7val home_dir = (concat hol_dir "examples/temporal_deep/"); 8loadPath := (concat home_dir "src/deep_embeddings") :: 9 (concat home_dir "src/translations") :: 10 (concat home_dir "src/tools") :: 11 (concat hol_dir "examples/PSL/path") :: 12 (concat hol_dir "examples/PSL/1.1/official-semantics") :: !loadPath; 13 14map load 15 ["FinitePSLPathTheory", "PSLPathTheory", "UnclockedSemanticsTheory", "SyntacticSugarTheory", "LemmasTheory", "RewritesTheory", 16 "RewritesPropertiesTheory", "ProjectionTheory", "SyntacticSugarTheory", "arithmeticTheory", "psl_lemmataTheory", 17 "listTheory", "numLib", "intLib", "rich_listTheory", "pred_setTheory", "ModelTheory", "rltl_to_ltlTheory", 18 "rltlTheory", "full_ltlTheory", "tuerk_tacticsLib", "prop_logicTheory", "infinite_pathTheory", "res_quanTools", "temporal_deep_mixedTheory"]; 19*) 20 21open FinitePSLPathTheory PSLPathTheory UnclockedSemanticsTheory SyntacticSugarTheory 22 LemmasTheory RewritesTheory ModelTheory rltl_to_ltlTheory 23 RewritesPropertiesTheory ProjectionTheory SyntacticSugarTheory 24 arithmeticTheory psl_lemmataTheory 25 listTheory numLib intLib rich_listTheory pred_setTheory prop_logicTheory 26 infinite_pathTheory temporal_deep_mixedTheory 27 rltlTheory full_ltlTheory tuerk_tacticsLib res_quanTools; 28open Sanity; 29 30val _ = intLib.deprecate_int(); 31 32(* 33show_assums := false; 34show_assums := true; 35show_types := true; 36show_types := false; 37quietdec := false; 38*) 39 40 41val _ = new_theory "psl_to_rltl"; 42 43 44val TRANSLATE_TOP_BOTTOM_def = 45 Define 46 `(TRANSLATE_TOP_BOTTOM (t:'prop) (b:'prop) TOP = (\x.x = t)) /\ 47 (TRANSLATE_TOP_BOTTOM (t:'prop) (b:'prop) BOTTOM = (\x.x = b)) /\ 48 (TRANSLATE_TOP_BOTTOM (t:'prop) (b:'prop) (STATE s) = s)`; 49 50 51val TRANSLATE_STATE_def = 52 Define 53 `(TRANSLATE_STATE (STATE s) = s)`; 54 55 56val CONVERT_PATH_PSL_LTL_def = 57 Define 58 `CONVERT_PATH_PSL_LTL (t:'prop) (b:'prop) = (\p.\n. if (n < LENGTH p) then ((TRANSLATE_TOP_BOTTOM t b) (ELEM p n)) else EMPTY)`; 59 60 61val CONVERT_PATH_PSL_LTL___NO_TOP_BOT_def = 62 Define 63 `CONVERT_PATH_PSL_LTL___NO_TOP_BOT = (\p.\n. if (n < LENGTH p) then (TRANSLATE_STATE (ELEM p n)) else EMPTY)`; 64 65 66val CONVERT_PATH_LTL_PSL_def = 67 Define 68 `CONVERT_PATH_LTL_PSL = (\p. INFINITE (\n. STATE (p n)))`; 69 70 71val BEXP_TO_PROP_LOGIC_def = 72 Define 73 `(BEXP_TO_PROP_LOGIC (B_PROP b) = P_PROP b) /\ 74 (BEXP_TO_PROP_LOGIC (B_TRUE) = P_TRUE) /\ 75 (BEXP_TO_PROP_LOGIC (B_FALSE) = P_FALSE) /\ 76 (BEXP_TO_PROP_LOGIC (B_NOT p) = P_NOT (BEXP_TO_PROP_LOGIC p)) /\ 77 (BEXP_TO_PROP_LOGIC (B_AND (p1, p2)) = P_AND(BEXP_TO_PROP_LOGIC p1,BEXP_TO_PROP_LOGIC p2))`; 78 79 80val PROP_LOGIC_TO_BEXP_def = 81 Define 82 `(PROP_LOGIC_TO_BEXP (P_PROP b) = B_PROP b) /\ 83 (PROP_LOGIC_TO_BEXP (P_TRUE) = B_TRUE) /\ 84 (PROP_LOGIC_TO_BEXP (P_NOT p) = B_NOT (PROP_LOGIC_TO_BEXP p)) /\ 85 (PROP_LOGIC_TO_BEXP (P_AND (p1, p2)) = B_AND(PROP_LOGIC_TO_BEXP p1,PROP_LOGIC_TO_BEXP p2))`; 86 87 88val PSL_TO_RLTL_def = 89 Define 90 `(PSL_TO_RLTL (F_STRONG_BOOL b) = (RLTL_PROP (BEXP_TO_PROP_LOGIC b))) 91 /\ 92 (PSL_TO_RLTL (F_WEAK_BOOL b) = (RLTL_PROP (BEXP_TO_PROP_LOGIC b))) 93 /\ 94 (PSL_TO_RLTL (F_NOT f) = RLTL_NOT (PSL_TO_RLTL f)) 95 /\ 96 (PSL_TO_RLTL (F_AND(f1,f2)) = RLTL_AND(PSL_TO_RLTL f1,PSL_TO_RLTL f2)) 97 /\ 98 (PSL_TO_RLTL (F_NEXT f) = RLTL_NEXT(PSL_TO_RLTL f)) 99 /\ 100 (PSL_TO_RLTL (F_UNTIL(f1,f2)) = RLTL_SUNTIL(PSL_TO_RLTL f1,PSL_TO_RLTL f2)) 101 /\ 102 (PSL_TO_RLTL (F_ABORT (f,b)) = RLTL_ACCEPT(PSL_TO_RLTL f, BEXP_TO_PROP_LOGIC b))`; 103 104 105val PSL_TO_LTL_def = 106 Define 107 `PSL_TO_LTL f = (RLTL_TO_LTL P_FALSE P_FALSE (PSL_TO_RLTL f))`; 108 109val PSL_TO_LTL_CLOCK_def = 110 Define 111 `PSL_TO_LTL_CLOCK c f = (RLTL_TO_LTL P_FALSE P_FALSE (PSL_TO_RLTL (F_CLOCK_COMP c f)))`; 112 113 114val CONVERT_PATH_PSL_LTL___NO_TOP_BOT_LEMMA = 115 store_thm 116 ("CONVERT_PATH_PSL_LTL___NO_TOP_BOT_LEMMA", 117 ``!v b t. IS_INFINITE_TOP_BOTTOM_FREE_PATH v ==> 118 (CONVERT_PATH_PSL_LTL t b v = CONVERT_PATH_PSL_LTL___NO_TOP_BOT v)``, 119 120 SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 121 CONVERT_PATH_PSL_LTL_def, 122 CONVERT_PATH_PSL_LTL___NO_TOP_BOT_def] THEN 123 REPEAT STRIP_TAC THEN 124 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 125 ASM_SIMP_TAC std_ss [LENGTH_def, LS, ELEM_INFINITE] THEN 126 GEN_TAC THEN 127 `?s. p x = STATE s` by PROVE_TAC[] THEN 128 ASM_SIMP_TAC std_ss [TRANSLATE_STATE_def, TRANSLATE_TOP_BOTTOM_def]); 129 130 131val CONVERT_PATH_LTL_PSL___IS_INFINITE_TOP_BOTTOM_FREE = 132 store_thm 133 ("CONVERT_PATH_LTL_PSL___IS_INFINITE_TOP_BOTTOM_FREE", 134 ``!p. IS_INFINITE_TOP_BOTTOM_FREE_PATH (CONVERT_PATH_LTL_PSL p)``, 135 136 SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 137 CONVERT_PATH_LTL_PSL_def, path_11, letter_11]); 138 139val CONVERT_PATH_LTL_PSL___CONVERT_PATH_PSL_LTL = 140 store_thm 141 ("CONVERT_PATH_LTL_PSL___CONVERT_PATH_PSL_LTL", 142 ``(!p. CONVERT_PATH_PSL_LTL___NO_TOP_BOT (CONVERT_PATH_LTL_PSL p) = p) /\ 143 (!p t b. CONVERT_PATH_PSL_LTL t b (CONVERT_PATH_LTL_PSL p) = p)``, 144 145 SIMP_TAC std_ss [CONVERT_PATH_LTL_PSL_def, 146 CONVERT_PATH_PSL_LTL_def, 147 CONVERT_PATH_PSL_LTL___NO_TOP_BOT_def, 148 LENGTH_def, LS, ELEM_INFINITE, 149 TRANSLATE_STATE_def, 150 TRANSLATE_TOP_BOTTOM_def] THEN 151 METIS_TAC[]); 152 153 154val BEXP_TO_PROP_LOGIC_THM = 155 store_thm 156 ("BEXP_TO_PROP_LOGIC_THM", 157 ``!p s. (P_SEM s (BEXP_TO_PROP_LOGIC p)) = (B_SEM (STATE s) p)``, 158 159 INDUCT_THEN bexp_induct ASSUME_TAC THEN 160 ASM_SIMP_TAC std_ss [B_SEM_def, BEXP_TO_PROP_LOGIC_def, P_SEM_THM] 161); 162 163 164val PROP_LOGIC_TO_BEXP_THM = 165 store_thm 166 ("PROP_LOGIC_TO_BEXP_THM", 167 ``!p s. (P_SEM s p) = (B_SEM (STATE s) (PROP_LOGIC_TO_BEXP p))``, 168 169 INDUCT_THEN prop_logic_induct ASSUME_TAC THEN 170 ASM_SIMP_TAC std_ss [B_SEM_def, PROP_LOGIC_TO_BEXP_def, P_SEM_THM] 171); 172 173 174val CONVERT_PATH_PSL_LTL_COMPLEMENT = 175 store_thm 176 ("CONVERT_PATH_PSL_LTL_COMPLEMENT", 177 ``!t b f. CONVERT_PATH_PSL_LTL b t (COMPLEMENT f) = CONVERT_PATH_PSL_LTL t b f``, 178 179 SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, COMPLEMENT_def, LENGTH_COMPLEMENT, ELEM_COMPLEMENT] THEN 180 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 181 REPEAT STRIP_TAC THEN 182 SIMP_TAC std_ss [] THEN 183 Cases_on `x < LENGTH f` THENL [ 184 ASM_SIMP_TAC std_ss [] THEN 185 Cases_on `ELEM f x` THEN 186 REWRITE_TAC[COMPLEMENT_LETTER_def, TRANSLATE_TOP_BOTTOM_def], 187 188 ASM_SIMP_TAC std_ss [] 189 ]); 190 191 192 193val CONVERT_PATH_PSL_LTL_ELEM_INFINITE = 194 store_thm 195 ("CONVERT_PATH_PSL_LTL_ELEM_INFINITE", 196 ``!p t b t'. ((CONVERT_PATH_PSL_LTL t b (INFINITE p)) t' = TRANSLATE_TOP_BOTTOM t b (p t'))``, 197 198 SIMP_TAC std_ss [LENGTH_def, LESS_def, CONVERT_PATH_PSL_LTL_def, ELEM_INFINITE, LS]); 199 200 201 202val CONVERT_PATH_PSL_LTL___NAND_ON_PATH = 203 store_thm 204 ("CONVERT_PATH_PSL_LTL___NAND_ON_PATH", 205 206 ``!t' t b v. (~(t=b) /\ PATH_PROP_FREE t v /\ PATH_PROP_FREE b v) ==> NAND_ON_PATH_RESTN t' (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b)``, 207 208 SIMP_TAC std_ss [NAND_ON_PATH_RESTN_def, CONVERT_PATH_PSL_LTL_def] THEN 209 REPEAT STRIP_TAC THEN 210 Cases_on `t'' < LENGTH v` THENL [ 211 ASM_REWRITE_TAC [] THEN 212 Cases_on `ELEM v t''` THENL [ 213 ASM_SIMP_TAC std_ss [IN_DEF, TRANSLATE_TOP_BOTTOM_def, P_SEM_def], 214 ASM_SIMP_TAC std_ss [IN_DEF, TRANSLATE_TOP_BOTTOM_def, P_SEM_def], 215 216 REWRITE_ALL_TAC [PATH_PROP_FREE_def, TRANSLATE_TOP_BOTTOM_def, P_SEM_def] THEN 217 PROVE_TAC[IN_DEF] 218 ], 219 220 ASM_REWRITE_TAC [NOT_IN_EMPTY, P_SEM_def] 221 ]); 222 223 224 225val PSL_TO_RLTL_THM = 226 store_thm 227 ("PSL_TO_RLTL_THM", 228 ``!f v b t. ((IS_INFINITE_PROPER_PATH v) /\ (F_CLOCK_SERE_FREE f) /\ ~(t = b) /\ (PATH_PROP_FREE t v) /\ (PATH_PROP_FREE b v)) ==> 229 ((UF_SEM v f) = (RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)))``, 230 231 232INDUCT_THEN fl_induct ASSUME_TAC THENL [ 233 234 REPEAT STRIP_TAC THEN 235 FULL_SIMP_TAC std_ss [IS_INFINITE_PROPER_PATH_def, PSL_TO_RLTL_def, UF_SEM_def, LENGTH_def, GT, 236 ELEM_INFINITE, RLTL_SEM_TIME_def, CONVERT_PATH_PSL_LTL_def, LS, BEXP_TO_PROP_LOGIC_THM, P_SEM_THM] THEN 237 Cases_on `p 0` THENL [ 238 ASM_SIMP_TAC std_ss [IN_DEF, CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, B_SEM_def], 239 ASM_SIMP_TAC std_ss [IN_DEF, CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, B_SEM_def], 240 241 ASM_SIMP_TAC std_ss [IN_DEF, CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, BEXP_TO_PROP_LOGIC_THM] THEN 242 PROVE_TAC[PATH_PROP_FREE_SEM] 243 ], 244 245 246 REPEAT STRIP_TAC THEN 247 FULL_SIMP_TAC std_ss [IS_INFINITE_PROPER_PATH_def, PSL_TO_RLTL_def, UF_SEM_def, LENGTH_def, GT, 248 ELEM_INFINITE, RLTL_SEM_TIME_def, CONVERT_PATH_PSL_LTL_def, LS, BEXP_TO_PROP_LOGIC_THM, P_SEM_THM, 249 xnum_distinct] THEN 250 Cases_on `p 0` THENL [ 251 ASM_SIMP_TAC std_ss [IN_DEF, CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, B_SEM_def], 252 ASM_SIMP_TAC std_ss [IN_DEF, CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, B_SEM_def], 253 254 ASM_SIMP_TAC std_ss [IN_DEF, CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, BEXP_TO_PROP_LOGIC_THM] THEN 255 PROVE_TAC[PATH_PROP_FREE_SEM] 256 ], 257 258 259 REWRITE_ALL_TAC[UF_SEM_def, PSL_TO_RLTL_def, RLTL_SEM_TIME_def, F_CLOCK_SERE_FREE_def, 260 F_CLOCK_FREE_def, F_SERE_FREE_def] THEN 261 METIS_TAC[CONVERT_PATH_PSL_LTL_COMPLEMENT, IS_INFINITE_PROPER_PATH___COMPLEMENT, PATH_PROP_FREE_COMPLEMENT], 262 263 264 REWRITE_ALL_TAC[UF_SEM_def, PSL_TO_RLTL_def, RLTL_SEM_def, RLTL_SEM_TIME_def, F_CLOCK_SERE_FREE_def, 265 F_CLOCK_FREE_def, F_SERE_FREE_def] THEN 266 METIS_TAC[], 267 268 269 REWRITE_TAC[F_CLOCK_SERE_FREE_def, F_SERE_FREE_def], 270 REWRITE_TAC[F_CLOCK_SERE_FREE_def, F_SERE_FREE_def], 271 272 273 REPEAT STRIP_TAC THEN 274 REWRITE_ALL_TAC[UF_SEM_def, PSL_TO_RLTL_def, RLTL_SEM_THM, F_CLOCK_SERE_FREE_def, F_CLOCK_SERE_FREE_def, F_SERE_FREE_def, F_CLOCK_FREE_def] THEN 275 `?p. v = INFINITE p` by METIS_TAC[IS_INFINITE_PROPER_PATH_def] THEN 276 ASM_REWRITE_TAC[LENGTH_def, GT, CONVERT_PATH_PSL_LTL_ELEM_INFINITE] THEN 277 `ELEM v 0 = p 0` by METIS_TAC[ELEM_INFINITE] THEN 278 Cases_on `p 0` THENL [ 279 `0:num <= 1` by DECIDE_TAC THEN 280 `RESTN (INFINITE p) 1 = TOP_OMEGA` by PROVE_TAC [INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA] THEN 281 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def, IN_DEF, P_SEM_THM, RLTL_SEM_TIME_def] THEN 282 PROVE_TAC[UF_SEM___F_CLOCK_SERE_FREE___OMEGA_TOP_BOTTOM, F_CLOCK_SERE_FREE_def], 283 284 285 `0:num <= 1` by DECIDE_TAC THEN 286 `RESTN (INFINITE p) 1 = BOTTOM_OMEGA` by PROVE_TAC [INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA] THEN 287 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def, IN_DEF, P_SEM_THM, RLTL_SEM_TIME_def] THEN 288 PROVE_TAC[UF_SEM___F_CLOCK_SERE_FREE___OMEGA_TOP_BOTTOM, F_CLOCK_SERE_FREE_def], 289 290 291 `(~f' b) /\ (~f' t)` by PROVE_TAC[PATH_PROP_FREE_def, IN_DEF, LS, LENGTH_def] THEN 292 ASM_SIMP_TAC std_ss [P_SEM_def, TRANSLATE_TOP_BOTTOM_def, IN_DEF] THEN 293 `1 < LENGTH (INFINITE p)` by EVAL_TAC THEN 294 `?v'. v' = RESTN (INFINITE p) 1` by PROVE_TAC[] THEN 295 `IS_INFINITE_PROPER_PATH v'` by PROVE_TAC[IS_INFINITE_PROPER_PATH_RESTN] THEN 296 `PATH_PROP_FREE t v'` by PROVE_TAC [PATH_PROP_FREE_RESTN] THEN 297 `PATH_PROP_FREE b v'` by PROVE_TAC [PATH_PROP_FREE_RESTN] THEN 298 `(UF_SEM (RESTN (INFINITE p) 1) f = RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v') (P_PROP t) (P_PROP b) (PSL_TO_RLTL f))` by 299 METIS_TAC[] THEN 300 ONCE_REWRITE_TAC [RLTL_SEM_TIME___TIME_ELIM] THEN 301 ASM_SIMP_TAC arith_ss [CONVERT_PATH_PSL_LTL_def, LENGTH_def, LS, ELEM_INFINITE, RESTN_INFINITE, 302 PATH_RESTN_def] 303 ], 304 305 306 307 REPEAT STRIP_TAC THEN 308 SUBGOAL_TAC `(!k. (UF_SEM (RESTN v k) f) = (RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b (RESTN v k)) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f))) /\ 309 (!k. (UF_SEM (RESTN v k) f') = (RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b (RESTN v k)) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f')))` THEN1 ( 310 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 311 GEN_TAC THEN 312 `IS_INFINITE_PROPER_PATH (RESTN v k)` by METIS_TAC[IS_INFINITE_PROPER_PATH_RESTN] THEN 313 `F_CLOCK_SERE_FREE f /\ F_CLOCK_SERE_FREE f'` by FULL_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, F_SERE_FREE_def, F_CLOCK_FREE_def] THEN 314 `k < LENGTH v` by FULL_SIMP_TAC std_ss [LENGTH_def, LS, IS_INFINITE_PROPER_PATH_def] THEN 315 `PATH_PROP_FREE t (RESTN v k)` by METIS_TAC[PATH_PROP_FREE_RESTN] THEN 316 `PATH_PROP_FREE b (RESTN v k)` by METIS_TAC[PATH_PROP_FREE_RESTN] THEN 317 METIS_TAC[] 318 ) THEN 319 SIMP_ASSUMPTIONS_TAC std_ss [IS_INFINITE_PROPER_PATH_def] THEN 320 ASM_SIMP_TAC (std_ss++resq_SS) [CONVERT_PATH_PSL_LTL_def, PSL_TO_RLTL_def, UF_SEM_def, LENGTH_def, LS, IN_LESSX, 321 RLTL_SEM_TIME_def, LS, IN_LESSX, ELEM_INFINITE, IN_LESS, RESTN_INFINITE] THEN 322 ONCE_REWRITE_TAC [RLTL_SEM_TIME___TIME_ELIM] THEN 323 SIMP_TAC std_ss [PATH_RESTN_def], 324 325 326 REPEAT STRIP_TAC THEN 327 `?p. v = INFINITE p` by METIS_TAC[IS_INFINITE_PROPER_PATH_def] THEN 328 FULL_SIMP_TAC (std_ss++resq_SS) [PSL_TO_RLTL_def, UF_SEM_def, LENGTH_def, IN_LESSX, 329 ELEM_INFINITE, F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, F_SERE_FREE_def, RLTL_SEM_TIME_def] THEN 330 Cases_on `UF_SEM (INFINITE p) f` THENL [ 331 ASM_REWRITE_TAC[] THEN 332 `RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)` by METIS_TAC[] THEN 333 334 `NAND_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b)` by 335 METIS_TAC[CONVERT_PATH_PSL_LTL___NAND_ON_PATH] THEN 336 `NAND_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))) (P_PROP b)` by 337 (REWRITE_TAC [NAND_ON_PATH_RESTN_def, P_SEM_THM] THEN METIS_TAC[]) THEN 338 339 METIS_TAC [RLTL_SEM_TIME___ACCEPT_OR_THM, RLTL_SEM_def], 340 341 342 343 344 `~RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b (INFINITE p)) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)` by METIS_TAC[RLTL_SEM_def] THEN 345 ASM_REWRITE_TAC[] THEN 346 EQ_TAC THENL [ 347 REPEAT STRIP_TAC THEN 348 Cases_on `j = 0` THENL [ 349 REMAINS_TAC `(P_SEM ((CONVERT_PATH_PSL_LTL t b v) 0) (BEXP_TO_PROP_LOGIC p_2)) /\ 350 ~(P_SEM ((CONVERT_PATH_PSL_LTL t b v) 0) (P_PROP b))` THEN1 ( 351 METIS_TAC[RLTL_ACCEPT_REJECT_THM, P_SEM_THM] 352 ) THEN 353 354 Cases_on `p 0` THENL [ 355 `!t:num. 0 <= t` by DECIDE_TAC THEN 356 `v = TOP_OMEGA` by METIS_TAC [INFINITE_PROPER_PATH___RESTN_TOP_BOTTOM_OMEGA, RESTN_def, ELEM_INFINITE] THEN 357 METIS_TAC[UF_SEM___F_CLOCK_SERE_FREE___OMEGA_TOP_BOTTOM, TOP_OMEGA_def], 358 359 FULL_SIMP_TAC std_ss [B_SEM_def], 360 361 FULL_SIMP_TAC std_ss [B_SEM_def, BEXP_TO_PROP_LOGIC_THM, TRANSLATE_TOP_BOTTOM_def, 362 CONVERT_PATH_PSL_LTL_def, LENGTH_def, LS, ELEM_INFINITE, P_SEM_def, IN_DEF] THEN 363 PROVE_TAC[PATH_PROP_FREE_SEM] 364 ], 365 366 367 (*Case ~(j = 0)*) 368 `?v'. (CAT (SEL v (0,j - 1),TOP_OMEGA)) = v'` by METIS_TAC[] THEN 369 FULL_SIMP_TAC std_ss [] THEN 370 SUBGOAL_TAC `RLTL_EQUIV_PATH_STRONG 0 (CONVERT_PATH_PSL_LTL t b v) (CONVERT_PATH_PSL_LTL t b v') (P_OR (P_PROP t, P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))) (P_PROP b)` THEN1 ( 371 372 `LENGTH v' = INFINITY` by PROVE_TAC[LENGTH_CAT_SEL_TOP_OMEGA] THEN 373 ASM_SIMP_TAC std_ss [RLTL_EQUIV_PATH_STRONG_def, CONVERT_PATH_PSL_LTL_def, LENGTH_def, LS] THEN 374 375 SUBGOAL_THEN ``ELEM v' j = TOP`` ASSUME_TAC THEN1( 376 `j > j-1` by DECIDE_TAC THEN 377 `!x. ELEM TOP_OMEGA x = TOP` by REWRITE_TAC [TOP_OMEGA_def, ELEM_INFINITE] THEN 378 METIS_TAC [ELEM_CAT_SEL___GREATER] 379 ) THEN 380 381 SUBGOAL_THEN ``!l:num. l < j:num ==> ((ELEM (v':'a letter path) l) = (ELEM v l))`` ASSUME_TAC THEN1 ( 382 REPEAT STRIP_TAC THEN 383 `l <= j-1` by DECIDE_TAC THEN 384 METIS_TAC[ELEM_CAT_SEL___LESS_EQ] 385 ) THEN 386 387 EXISTS_TAC ``j:num`` THEN 388 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def, IN_DEF, ELEM_INFINITE, P_SEM_THM] THEN 389 390 Cases_on `p j` THENL [ 391 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def], 392 REWRITE_ASSUMPTIONS_TAC [B_SEM_def], 393 394 FULL_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def, BEXP_TO_PROP_LOGIC_THM] THEN 395 METIS_TAC[PATH_PROP_FREE_SEM, IN_DEF] 396 ] 397 ) THEN 398 399 400 SUBGOAL_TAC `RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v') (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)` THEN1 ( 401 `~(ELEM v j = BOTTOM)` by METIS_TAC[B_SEM_def, ELEM_INFINITE] THEN 402 `IS_INFINITE_PROPER_PATH v'` by METIS_TAC[IS_INFINITE_PROPER_PATH___CAT_SEL_TOP_OMEGA] THEN 403 `?p. INFINITE p = v` by METIS_TAC[IS_INFINITE_PROPER_PATH_def] THEN 404 `PATH_PROP_FREE t v'` by METIS_TAC[PATH_PROP_FREE___CAT_SEL_INFINITE___IMPLIES] THEN 405 `PATH_PROP_FREE b v'` by METIS_TAC[PATH_PROP_FREE___CAT_SEL_INFINITE___IMPLIES] THEN 406 407 METIS_TAC[] 408 ) THEN 409 410 SUBGOAL_TAC `IMP_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v') (P_PROP t) (P_OR 411 (P_PROP t,P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))))` THEN1 ( 412 REWRITE_TAC[IMP_ON_PATH_RESTN_def, P_SEM_THM] THEN 413 METIS_TAC[] 414 ) THEN 415 416 417 `RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v') 418 (P_OR (P_PROP t,P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))) 419 (P_PROP b) (PSL_TO_RLTL f)` by 420 METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH, RLTL_SEM_def] THEN 421 METIS_TAC[RLTL_EQUIV_PATH_STRONG_THM] 422 ], 423 424 425 426 427 `NAND_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b (INFINITE p)) (P_PROP t) (P_PROP b)` by METIS_TAC[CONVERT_PATH_PSL_LTL___NAND_ON_PATH] THEN 428 `NAND_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b (INFINITE p)) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))) (P_PROP b)` by (REWRITE_TAC [NAND_ON_PATH_RESTN_def, P_SEM_THM] THEN METIS_TAC[]) THEN 429 430 ASM_SIMP_TAC std_ss [RLTL_SEM_TIME___ACCEPT_OR_THM] THEN 431 REPEAT STRIP_TAC THEN 432 433 SUBGOAL_TAC `?j. (P_SEM ((CONVERT_PATH_PSL_LTL t b v) j) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))) /\ 434 !j'. (j' < j) ==> (~(P_SEM ((CONVERT_PATH_PSL_LTL t b v) j') (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))) /\ ~(P_SEM ((CONVERT_PATH_PSL_LTL t b v) j') (P_PROP t)))` THEN1 ( 435 436 `IS_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))` by METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IS_ON_PATH] THEN 437 SIMP_ASSUMPTIONS_TAC std_ss [IS_ON_PATH_RESTN_def, NOT_ON_PATH_RESTN_def] THEN 438 439 `?j. P_SEM (CONVERT_PATH_PSL_LTL t b v j) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))) /\ 440 !j'. j' < j ==> ~P_SEM (CONVERT_PATH_PSL_LTL t b v j') (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))` by 441 METIS_TAC [EXISTS_LEAST_CONV ``?j. P_SEM (CONVERT_PATH_PSL_LTL t b v j) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))``] THEN 442 443 EXISTS_TAC ``j:num`` THEN 444 ASM_SIMP_TAC std_ss [] THEN 445 `BEFORE_ON_PATH_RESTN_STRONG 0 (CONVERT_PATH_PSL_LTL t b v) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))) (P_PROP t)` by METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_BEFORE_ON_PATH_STRONG] THEN 446 447 CCONTR_TAC THEN 448 SIMP_ASSUMPTIONS_TAC std_ss [BEFORE_ON_PATH_RESTN_STRONG_def] THEN 449 `?u. u < j' /\ 450 P_SEM (CONVERT_PATH_PSL_LTL t b v u) 451 (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))` by METIS_TAC[] THEN 452 `u < j` by DECIDE_TAC THEN 453 METIS_TAC[]) THEN 454 455 SIMP_ASSUMPTIONS_TAC std_ss [P_SEM_THM] THEN 456 EXISTS_TAC ``j:num`` THEN 457 REPEAT STRIP_TAC THENL [ 458 Cases_on `p j` THENL [ 459 REWRITE_TAC [B_SEM_def], 460 461 UNDISCH_TAC ``~(b IN CONVERT_PATH_PSL_LTL t b v j)`` THEN 462 ASM_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, IN_DEF, TRANSLATE_TOP_BOTTOM_def, LENGTH_def, LS, ELEM_INFINITE], 463 464 UNDISCH_TAC ``P_SEM (CONVERT_PATH_PSL_LTL t b v j) 465 (BEXP_TO_PROP_LOGIC p_2)`` THEN 466 ASM_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, TRANSLATE_TOP_BOTTOM_def, BEXP_TO_PROP_LOGIC_THM, LS, 467 LENGTH_def, LESS_def, ELEM_INFINITE] 468 ], 469 470 471 Cases_on `j=0` THEN ASM_REWRITE_TAC[] THEN1 ( 472 METIS_TAC[UF_SEM___F_CLOCK_SERE_FREE___OMEGA_TOP_BOTTOM, F_CLOCK_SERE_FREE_def] 473 ) THEN 474 475 `?v'. (CAT (SEL (INFINITE p) (0,j - 1),TOP_OMEGA)) = v'` by METIS_TAC[] THEN 476 SUBGOAL_TAC `~(ELEM v j = BOTTOM)` THEN1 ( 477 UNDISCH_TAC ``~(b IN CONVERT_PATH_PSL_LTL t b v j)`` THEN 478 Cases_on `p j` THEN 479 ASM_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, IN_DEF, TRANSLATE_TOP_BOTTOM_def, ELEM_INFINITE, 480 letter_distinct, LENGTH_def, LS] 481 ) THEN 482 SUBGOAL_TAC `UF_SEM v' f = RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v') (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)` THEN1 ( 483 `IS_INFINITE_PROPER_PATH v'` by METIS_TAC[IS_INFINITE_PROPER_PATH___CAT_SEL_TOP_OMEGA] THEN 484 `PATH_PROP_FREE t v'` by METIS_TAC[PATH_PROP_FREE___CAT_SEL_INFINITE___IMPLIES] THEN 485 `PATH_PROP_FREE b v'` by METIS_TAC[PATH_PROP_FREE___CAT_SEL_INFINITE___IMPLIES] THEN 486 487 METIS_TAC[] 488 ) THEN 489 ASM_REWRITE_TAC[] THEN 490 491 `!k:num. k < LENGTH v'` by METIS_TAC [LENGTH_CAT_SEL_TOP_OMEGA, LS, IS_INFINITE_PROPER_PATH_def] THEN 492 SUBGOAL_TAC `RLTL_EQUIV_PATH_STRONG 0 (CONVERT_PATH_PSL_LTL t b v) (CONVERT_PATH_PSL_LTL t b v') (P_OR (P_PROP t, P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))) (P_PROP b)` THEN1 ( 493 494 ASM_SIMP_TAC std_ss [RLTL_EQUIV_PATH_STRONG_def, CONVERT_PATH_PSL_LTL_def, LENGTH_def, LS] THEN 495 496 SUBGOAL_TAC `ELEM v' j = TOP` THEN1( 497 `j > j-1` by DECIDE_TAC THEN 498 `!x. ELEM TOP_OMEGA x = TOP` by REWRITE_TAC [TOP_OMEGA_def, ELEM_INFINITE] THEN 499 METIS_TAC [ELEM_CAT_SEL___GREATER] 500 ) THEN 501 502 SUBGOAL_TAC `!l:num. l < j:num ==> ((ELEM (v':'a letter path) l) = (ELEM v l))` THEN1 ( 503 REPEAT STRIP_TAC THEN 504 `l <= j-1` by DECIDE_TAC THEN 505 METIS_TAC[ELEM_CAT_SEL___LESS_EQ] 506 ) THEN 507 508 EXISTS_TAC ``j:num`` THEN 509 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def, IN_DEF, ELEM_INFINITE, P_SEM_THM, 510 BEXP_TO_PROP_LOGIC_THM] THEN 511 512 Cases_on `p j` THENL [ 513 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def], 514 METIS_TAC[ELEM_INFINITE], 515 516 SUBGOAL_TAC `B_SEM (STATE (TRANSLATE_TOP_BOTTOM t b (STATE f'))) p_2` THEN1( 517 UNDISCH_TAC ``P_SEM (CONVERT_PATH_PSL_LTL t b v j) (BEXP_TO_PROP_LOGIC p_2)`` THEN 518 ASM_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, LENGTH_def, LS, ELEM_INFINITE, BEXP_TO_PROP_LOGIC_THM] 519 ) THEN 520 FULL_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def] THEN 521 METIS_TAC[PATH_PROP_FREE_SEM] 522 ] 523 ) THEN 524 525 SUBGOAL_TAC `RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v') 526 (P_OR(P_PROP t, (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))))) (P_PROP b) 527 (PSL_TO_RLTL f)` THEN1 ( 528 529 `IMP_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))) (P_OR(P_PROP t, (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b)))))` by 530 (REWRITE_TAC[IMP_ON_PATH_RESTN_def, P_SEM_THM] THEN METIS_TAC[]) THEN 531 METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH, RLTL_EQUIV_PATH_STRONG_THM]) THEN 532 533 SUBGOAL_TAC `IMP_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v') (P_OR(P_PROP t, (P_AND (BEXP_TO_PROP_LOGIC p_2,P_NOT (P_PROP b))))) (P_PROP t)` THEN1 ( 534 REWRITE_TAC[IMP_ON_PATH_RESTN_def, P_SEM_THM] THEN 535 REPEAT STRIP_TAC THEN 536 Cases_on `t' <= j-1` THENL [ 537 SUBGOAL_TAC `CONVERT_PATH_PSL_LTL t b v' t' = CONVERT_PATH_PSL_LTL t b v t'` THEN1 ( 538 ASM_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, LENGTH_def, LS] THEN 539 METIS_TAC[ELEM_CAT_SEL___LESS_EQ] 540 ) THEN 541 `t' < j` by DECIDE_TAC THEN 542 METIS_TAC[], 543 544 545 SUBGOAL_TAC `ELEM v' t' = TOP` THEN1 ( 546 `t' > j-1` by DECIDE_TAC THEN 547 `ELEM v' t' = ELEM (TOP_OMEGA) (t' - (SUC (j-1)))` by 548 METIS_TAC[ELEM_CAT_SEL___GREATER] THEN 549 ASM_SIMP_TAC std_ss [TOP_OMEGA_def, ELEM_INFINITE] 550 ) THEN 551 ASM_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL_def, IN_DEF, TRANSLATE_TOP_BOTTOM_def] 552 ] 553 ) THEN 554 555 METIS_TAC [RLTL_SEM_TIME___ACCEPT_REJECT_IMP_ON_PATH] 556 ] 557 ] 558 ], 559 560 561 REWRITE_TAC[F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def], 562 REWRITE_TAC[F_CLOCK_SERE_FREE_def, F_SERE_FREE_def] 563]); 564 565 566 567val P_USED_VARS___BEXP_TO_PROP_LOGIC = 568 store_thm 569 ("P_USED_VARS___BEXP_TO_PROP_LOGIC", 570 ``!b. P_USED_VARS (BEXP_TO_PROP_LOGIC b) = B_USED_VARS b``, 571 572 INDUCT_THEN bexp_induct ASSUME_TAC THEN ( 573 ASM_SIMP_TAC std_ss [P_USED_VARS_def, BEXP_TO_PROP_LOGIC_def, 574 B_USED_VARS_def, P_FALSE_def] 575 )); 576 577 578val RLTL_USED_VARS___PSL_TO_RLTL = 579 store_thm 580 ("RLTL_USED_VARS___PSL_TO_RLTL", 581 ``!f. F_CLOCK_SERE_FREE f ==> 582 (RLTL_USED_VARS (PSL_TO_RLTL f) = F_USED_VARS f)``, 583 584REWRITE_TAC[F_CLOCK_SERE_FREE_def] THEN 585INDUCT_THEN fl_induct ASSUME_TAC THEN ( 586 ASM_SIMP_TAC std_ss [RLTL_USED_VARS_def, 587 F_USED_VARS_def, 588 F_CLOCK_FREE_def, F_SERE_FREE_def, 589 PSL_TO_RLTL_def, P_USED_VARS___BEXP_TO_PROP_LOGIC] 590)); 591 592 593 594val PSL_TO_RLTL___F_USED_VARS = 595 store_thm 596 ("PSL_TO_RLTL___F_USED_VARS", 597 ``!f v b t. ((IS_INFINITE_PROPER_PATH v) /\ (F_CLOCK_SERE_FREE f) /\ ~(t = b) /\ (~(t IN F_USED_VARS f)) /\ (~(b IN F_USED_VARS f))) ==> 598 ((UF_SEM v f) = (RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b (PATH_LETTER_RESTRICT (F_USED_VARS f) v)) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)))``, 599 600 REPEAT STRIP_TAC THEN 601 `?w. w = PATH_LETTER_RESTRICT ((F_USED_VARS f)) v` by METIS_TAC[] THEN 602 `UF_SEM v f = UF_SEM w f` by 603 PROVE_TAC[F_USED_VARS_INTER_SUBSET_THM, SUBSET_REFL, F_CLOCK_SERE_FREE_def] THEN 604 SUBGOAL_TAC `PATH_PROP_FREE t w /\ PATH_PROP_FREE b w` THEN1 ( 605 ASM_SIMP_TAC std_ss [PATH_PROP_FREE_def, 606 PATH_LETTER_RESTRICT_def, LENGTH_PATH_MAP, ELEM_PATH_MAP, GT_LS, 607 GSYM FORALL_AND_THM] THEN 608 REPEAT GEN_TAC THEN 609 Cases_on `ELEM v n` THEN ( 610 SIMP_TAC std_ss [LETTER_RESTRICT_def, letter_distinct, letter_11] THEN 611 PROVE_TAC[IN_INTER] 612 ) 613 ) THEN 614 615 616 SUBGOAL_TAC `IS_INFINITE_PROPER_PATH w` THEN1 ( 617 SIMP_ALL_TAC std_ss [IS_INFINITE_PROPER_PATH_def] THEN 618 ASM_SIMP_TAC std_ss [PATH_LETTER_RESTRICT_def, psl_lemmataTheory.PATH_MAP_def, path_11, 619 LETTER_RESTRICT_Cases] 620 ) THEN 621 622 ASSUME_TAC PSL_TO_RLTL_THM THEN 623 Q_SPECL_NO_ASSUM 0 [`f`, `w`, `b`, `t`] THEN 624 UNDISCH_HD_TAC THEN 625 ASM_SIMP_TAC std_ss []); 626 627 628val PSL_TO_RLTL___ELIM_ACCEPT_REJECT_THM = 629 store_thm 630 ("PSL_TO_RLTL___ELIM_ACCEPT_REJECT_THM", 631 ``!f v b t. ((IS_INFINITE_PROPER_PATH v) /\ ~(t = b) /\ (PATH_PROP_FREE t v) /\ (PATH_PROP_FREE b v)) ==> 632 (RLTL_SEM (CONVERT_PATH_PSL_LTL t b v) (RLTL_ACCEPT (RLTL_REJECT (f,P_PROP b), P_PROP t)) = (RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b) f))``, 633 634 REPEAT STRIP_TAC THEN 635 SIMP_TAC std_ss [RLTL_SEM_def, RLTL_SEM_TIME_def, RLTL_REJECT_def] THEN 636 637 REMAINS_TAC `(EQUIV_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_OR (P_FALSE,P_AND (P_PROP t,P_NOT P_FALSE))) (P_PROP t)) /\ 638 (EQUIV_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_OR (P_FALSE, P_AND (P_PROP b, P_NOT (P_OR (P_FALSE,P_AND (P_PROP t,P_NOT P_FALSE)))))) (P_PROP b))` THEN1 ( 639 METIS_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV_ON_PATH] 640 ) THEN 641 642 `NAND_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b)` by PROVE_TAC[CONVERT_PATH_PSL_LTL___NAND_ON_PATH] THEN 643 FULL_SIMP_TAC std_ss [NAND_ON_PATH_RESTN_def, EQUIV_ON_PATH_RESTN_def, P_SEM_THM] THEN 644 PROVE_TAC[]); 645 646 647val PSL_TO_RLTL___CLOCKED_THM = 648 store_thm 649 ("PSL_TO_RLTL___CLOCKED_THM", 650 ``!f v b t c. ((IS_INFINITE_PROPER_PATH v) /\ (F_SERE_FREE f) /\ ~(t = b) /\ 651 (PATH_PROP_FREE t v) /\ (PATH_PROP_FREE b v)) ==> 652 ((F_SEM v c f) = (RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b) (PSL_TO_RLTL (F_CLOCK_COMP c f))))``, 653 654 PROVE_TAC[PSL_TO_RLTL_THM, F_CLOCK_COMP_CORRECT, F_CLOCK_SERE_FREE_def, 655 F_SERE_FREE___IMPLIES___F_SERE_FREE_F_CLOCK_COMP, 656 F_CLOCK_FREE___F_CLOCK_COMP]); 657 658 659val P_VAR_RENAMING___BEXP_TO_PROP_LOGIC = 660 store_thm 661 ("P_VAR_RENAMING___BEXP_TO_PROP_LOGIC", 662 663 ``!f g. P_VAR_RENAMING g (BEXP_TO_PROP_LOGIC f) = 664 BEXP_TO_PROP_LOGIC (B_VAR_RENAMING g f)``, 665 666INDUCT_THEN bexp_induct ASSUME_TAC THEN ( 667 ASM_SIMP_TAC std_ss [BEXP_TO_PROP_LOGIC_def, 668 P_VAR_RENAMING_def, 669 B_VAR_RENAMING_def, 670 P_FALSE_def] 671)) 672 673val RLTL_VAR_RENAMING___PSL_TO_RLTL = 674 store_thm 675 ("RLTL_VAR_RENAMING___PSL_TO_RLTL", 676 677 ``!f g. F_CLOCK_SERE_FREE f ==> ( 678 RLTL_VAR_RENAMING g (PSL_TO_RLTL f) = 679 PSL_TO_RLTL (F_VAR_RENAMING g f))``, 680 681 INDUCT_THEN fl_induct ASSUME_TAC THEN ( 682 ASM_SIMP_TAC std_ss [PSL_TO_RLTL_def, RLTL_VAR_RENAMING_def, 683 PSL_TO_RLTL_def, F_VAR_RENAMING_def, 684 P_VAR_RENAMING___BEXP_TO_PROP_LOGIC, 685 F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, 686 F_SERE_FREE_def] 687 )); 688 689 690 691 692(*Prove the semantic with additional variables t and b first, then 693 move to a universe, where enough variables exist and eliminate t and b*) 694val PSL_TO_RLTL___NO_TOP_BOT_THM___WITH_T_B = 695 prove ( 696 ``!f t b v. (IS_INFINITE_TOP_BOTTOM_FREE_PATH v) /\ (F_CLOCK_SERE_FREE f) /\ ~(t = b) /\ (PATH_PROP_FREE t v) /\ (PATH_PROP_FREE b v)==> 697 ((UF_SEM v f) = RLTL_SEM (CONVERT_PATH_PSL_LTL___NO_TOP_BOT v) (PSL_TO_RLTL f))``, 698 699 REPEAT STRIP_TAC THEN 700 `IS_INFINITE_PROPER_PATH v` by PROVE_TAC[IS_INFINITE_TOP_BOTTOM_FREE_PATH___IMPLIES___IS_INFINITE_PROPER_PATH] THEN 701 `CONVERT_PATH_PSL_LTL___NO_TOP_BOT v = CONVERT_PATH_PSL_LTL t b v` by 702 PROVE_TAC[CONVERT_PATH_PSL_LTL___NO_TOP_BOT_LEMMA] THEN 703 `UF_SEM v f = RLTL_SEM_TIME 0 (CONVERT_PATH_PSL_LTL t b v) (P_PROP t) (P_PROP b) (PSL_TO_RLTL f)` by 704 PROVE_TAC[PSL_TO_RLTL_THM] THEN 705 ASM_REWRITE_TAC[RLTL_SEM_def] THEN 706 REMAINS_TAC `(EQUIV_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b (v:'a letter path)) (P_PROP t) P_FALSE) /\ 707 (EQUIV_ON_PATH_RESTN 0 (CONVERT_PATH_PSL_LTL t b (v:'a letter path)) (P_PROP b) P_FALSE)` THEN1 ( 708 PROVE_TAC[RLTL_SEM_TIME___ACCEPT_REJECT_EQUIV_ON_PATH] 709 ) THEN 710 711 FULL_SIMP_TAC arith_ss [EQUIV_ON_PATH_RESTN_def, GSYM FORALL_AND_THM, CONVERT_PATH_PSL_LTL_def, IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 712 LENGTH_def, LS, P_SEM_THM, ELEM_INFINITE] THEN 713 GEN_TAC THEN 714 `?s. p t' = STATE s` by PROVE_TAC[] THEN 715 ASM_SIMP_TAC std_ss [TRANSLATE_TOP_BOTTOM_def, IN_DEF] THEN 716 PROVE_TAC[PATH_PROP_FREE_SEM] 717 ); 718 719 720 721val PSL_TO_RLTL___NO_TOP_BOT_THM = 722 store_thm 723 ("PSL_TO_RLTL___NO_TOP_BOT_THM", 724 ``!f v. (IS_INFINITE_TOP_BOTTOM_FREE_PATH v) /\ (F_CLOCK_SERE_FREE f) ==> 725 ((UF_SEM v f) = RLTL_SEM (CONVERT_PATH_PSL_LTL___NO_TOP_BOT v) (PSL_TO_RLTL f))``, 726 727 REPEAT STRIP_TAC THEN 728 REMAINS_TAC `UF_SEM (PATH_LETTER_RESTRICT (F_USED_VARS f) v) f = 729 RLTL_SEM (CONVERT_PATH_PSL_LTL___NO_TOP_BOT (PATH_LETTER_RESTRICT (F_USED_VARS f) v)) (PSL_TO_RLTL f)` THEN1 ( 730 731 SUBGOAL_TAC `UF_SEM v f = UF_SEM (PATH_LETTER_RESTRICT (F_USED_VARS f) v) f` THEN1 ( 732 MATCH_MP_TAC (SIMP_RULE std_ss [AND_IMP_INTRO] F_USED_VARS_INTER_SUBSET_THM) THEN 733 FULL_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, SUBSET_REFL] 734 ) THEN 735 FULL_SIMP_TAC std_ss [RLTL_SEM_def] THEN 736 ONCE_REWRITE_TAC[RLTL_USED_VARS_INTER_THM] THEN 737 REPEAT AP_THM_TAC THEN AP_TERM_TAC THEN 738 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 739 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, 740 CONVERT_PATH_PSL_LTL___NO_TOP_BOT_def, 741 LENGTH_PATH_LETTER_RESTRICT, EXTENSION, IN_INTER, IN_UNION, 742 P_USED_VARS_EVAL, NOT_IN_EMPTY] THEN 743 REPEAT STRIP_TAC THEN 744 BOOL_EQ_STRIP_TAC THEN 745 Cases_on `x < LENGTH v` THEN ASM_REWRITE_TAC[] THEN 746 SIMP_ALL_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def] THEN 747 `?s. p x = STATE s` by METIS_TAC[] THEN 748 ASM_SIMP_TAC std_ss [ELEM_PATH_LETTER_RESTRICT, GT_LS, ELEM_INFINITE, TRANSLATE_STATE_def, 749 LETTER_RESTRICT_def, IN_INTER] THEN 750 `?s. p x = STATE s` by METIS_TAC[] THEN 751 METIS_TAC [RLTL_USED_VARS___PSL_TO_RLTL] 752 ) THEN 753 754 SUBGOAL_TAC `?g. INJ g (F_USED_VARS f) UNIV /\ 755 (!x. x IN F_USED_VARS f ==> (~(g x = 0) /\ ~(g x = 1:num)))` THEN1 ( 756 757 SUBGOAL_TAC `(INFINITE (UNIV:num set)):bool` THEN1 ( 758 REWRITE_TAC[INFINITE_UNIV] THEN 759 Q_TAC EXISTS_TAC `\n. SUC n` THEN 760 SIMP_TAC std_ss [] THEN 761 EXISTS_TAC ``0:num`` THEN 762 DECIDE_TAC 763 ) THEN 764 `?h:'a -> num. INJ h (F_USED_VARS f) UNIV` by PROVE_TAC[FINITE_INJ_EXISTS, FINITE___F_USED_VARS] THEN 765 Q_TAC EXISTS_TAC `\x. h x + 2` THEN 766 SIMP_TAC arith_ss [] THEN 767 UNDISCH_HD_TAC THEN 768 SIMP_TAC std_ss [INJ_DEF, IN_UNIV] 769 ) THEN 770 771 SUBGOAL_TAC `UF_SEM (PATH_LETTER_RESTRICT (F_USED_VARS f) v) f = 772 UF_SEM (PATH_VAR_RENAMING g (PATH_LETTER_RESTRICT (F_USED_VARS f) v)) (F_VAR_RENAMING g f)` THEN1 ( 773 MATCH_MP_TAC UF_SEM___VAR_RENAMING THEN 774 FULL_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def] THEN 775 UNDISCH_NO_TAC 1 THEN 776 MATCH_MP_TAC set_lemmataTheory.INJ_SUBSET_DOMAIN THEN 777 FULL_SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, 778 PATH_LETTER_RESTRICT_def, IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 779 psl_lemmataTheory.PATH_MAP_def, IN_ABS, 780 psl_lemmataTheory.PATH_USED_VARS_def, LENGTH_def, GT, ELEM_INFINITE] THEN 781 REPEAT STRIP_TAC THEN 782 `?s. p n = STATE s` by PROVE_TAC[] THEN 783 FULL_SIMP_TAC std_ss [LETTER_RESTRICT_def, LETTER_USED_VARS_def, 784 IN_INTER] 785 ) THEN 786 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 787 788 SUBGOAL_TAC `UF_SEM (PATH_VAR_RENAMING g (PATH_LETTER_RESTRICT (F_USED_VARS f) v)) (F_VAR_RENAMING g f) = 789 RLTL_SEM (CONVERT_PATH_PSL_LTL___NO_TOP_BOT ((PATH_VAR_RENAMING g (PATH_LETTER_RESTRICT (F_USED_VARS f) v)))) (PSL_TO_RLTL (F_VAR_RENAMING g f))` THEN1 ( 790 MATCH_MP_TAC PSL_TO_RLTL___NO_TOP_BOT_THM___WITH_T_B THEN 791 EXISTS_TAC ``1:num`` THEN 792 EXISTS_TAC ``0:num`` THEN 793 FULL_SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 794 F_VAR_RENAMING___F_CLOCK_SERE_FREE, 795 PATH_LETTER_RESTRICT_def, psl_lemmataTheory.PATH_VAR_RENAMING_def, 796 psl_lemmataTheory.PATH_MAP_def, path_11, 797 PATH_PROP_FREE_def, LENGTH_def, LS, ELEM_INFINITE, 798 GSYM FORALL_AND_THM] THEN 799 GEN_TAC THEN 800 `?s. p n = STATE s` by PROVE_TAC[] THEN 801 ASM_SIMP_TAC std_ss [LETTER_RESTRICT_def, LETTER_VAR_RENAMING_def, 802 letter_11] THEN 803 SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_INTER] THEN 804 PROVE_TAC[] 805 ) THEN 806 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 807 808 809 ASSUME_TAC (ISPECL [``PSL_TO_RLTL (f:'a fl)``, ``(CONVERT_PATH_PSL_LTL___NO_TOP_BOT 810 (PATH_LETTER_RESTRICT (F_USED_VARS f) v))``, ``g:'a -> num``] RLTL_SEM___VAR_RENAMING___PATH_RESTRICT) THEN 811 UNDISCH_HD_TAC THEN 812 ASM_SIMP_TAC std_ss [RLTL_USED_VARS___PSL_TO_RLTL] THEN 813 DISCH_TAC THEN WEAKEN_HD_TAC THEN 814 ASM_SIMP_TAC std_ss [RLTL_VAR_RENAMING___PSL_TO_RLTL] THEN 815 AP_THM_TAC THEN AP_TERM_TAC THEN 816 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 817 FULL_SIMP_TAC std_ss [CONVERT_PATH_PSL_LTL___NO_TOP_BOT_def, 818 IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 819 PATH_LETTER_RESTRICT_def, 820 psl_lemmataTheory.PATH_MAP_def, 821 psl_lemmataTheory.PATH_VAR_RENAMING_def, 822 LENGTH_def, LS, ELEM_INFINITE, 823 PATH_RESTRICT_def, PATH_MAP_def, 824 PATH_VAR_RENAMING_def] THEN 825 GEN_TAC THEN 826 `?s. p x = STATE s` by PROVE_TAC[] THEN 827 ASM_SIMP_TAC std_ss [LETTER_RESTRICT_def, LETTER_VAR_RENAMING_def, 828 TRANSLATE_STATE_def, set_lemmataTheory.INTER_INTER_ABSORPTION] 829 ); 830 831 832 833val UF_KS_SEM_def = 834 Define 835 `!M f. UF_KS_SEM M f = 836 (!p. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p ==> 837 UF_SEM (CONVERT_PATH_LTL_PSL p) f)`; 838 839val F_KS_SEM_def = 840 Define 841 `!M f c. F_KS_SEM M c f = 842 (!p. IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p ==> 843 F_SEM (CONVERT_PATH_LTL_PSL p) c f)`; 844 845 846val PSL_TO_RLTL___UF_KS_SEM = 847 store_thm 848 ("PSL_TO_RLTL___UF_KS_SEM", 849 ``!M f. F_CLOCK_SERE_FREE f 850 ==> 851 (UF_KS_SEM M f = 852 RLTL_KS_SEM M (PSL_TO_RLTL f))``, 853 854 855 856 REPEAT STRIP_TAC THEN 857 SIMP_TAC std_ss [UF_KS_SEM_def, 858 RLTL_KS_SEM_def] THEN 859 FORALL_EQ_STRIP_TAC THEN 860 BOOL_EQ_STRIP_TAC THEN 861 SUBGOAL_TAC `IS_INFINITE_TOP_BOTTOM_FREE_PATH (CONVERT_PATH_LTL_PSL p)` THEN1 ( 862 SIMP_TAC std_ss [IS_INFINITE_TOP_BOTTOM_FREE_PATH_def, 863 CONVERT_PATH_LTL_PSL_def, path_11, letter_11] 864 ) THEN 865 ASSUME_TAC PSL_TO_RLTL___NO_TOP_BOT_THM THEN 866 Q_SPECL_NO_ASSUM 0 [`f`, `CONVERT_PATH_LTL_PSL p`] THEN 867 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN 868 STRIP_TAC THEN WEAKEN_HD_TAC THEN 869 AP_THM_TAC THEN AP_TERM_TAC THEN 870 SIMP_TAC std_ss [CONVERT_PATH_LTL_PSL_def, 871 CONVERT_PATH_PSL_LTL___NO_TOP_BOT_def, 872 LENGTH_def, LS, ELEM_INFINITE, TRANSLATE_STATE_def, 873 FUN_EQ_THM]); 874 875 876 877val PSL_TO_RLTL___F_KS_SEM = 878 store_thm 879 ("PSL_TO_RLTL___F_KS_SEM", 880 ``!M f c. F_SERE_FREE f 881 ==> 882 (F_KS_SEM M c f = 883 RLTL_KS_SEM M (PSL_TO_RLTL (F_CLOCK_COMP c f)))``, 884 885 886 REPEAT STRIP_TAC THEN 887 SUBGOAL_TAC `RLTL_KS_SEM M (PSL_TO_RLTL (F_CLOCK_COMP c f)) = 888 UF_KS_SEM M (F_CLOCK_COMP c f)` THEN1 ( 889 SUBGOAL_TAC `F_CLOCK_SERE_FREE (F_CLOCK_COMP c f)` THEN1 ( 890 FULL_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, 891 F_CLOCK_FREE___F_CLOCK_COMP, 892 F_SERE_FREE___IMPLIES___F_SERE_FREE_F_CLOCK_COMP] 893 ) THEN 894 METIS_TAC [PSL_TO_RLTL___UF_KS_SEM] 895 ) THEN 896 ASM_REWRITE_TAC[] THEN 897 SIMP_TAC std_ss [F_KS_SEM_def, UF_KS_SEM_def, 898 F_CLOCK_COMP_CORRECT]); 899 900 901 902val PSL_TO_RLTL___NO_TOP_BOT___CLOCKED_THM = 903 store_thm 904 ("PSL_TO_RLTL___NO_TOP_BOT___CLOCKED_THM", 905 ``!f c v. ((IS_INFINITE_TOP_BOTTOM_FREE_PATH v) /\ (F_SERE_FREE f)) ==> 906 ((F_SEM v c f) = RLTL_SEM (CONVERT_PATH_PSL_LTL___NO_TOP_BOT v) (PSL_TO_RLTL (F_CLOCK_COMP c f)))``, 907 908 PROVE_TAC[PSL_TO_RLTL___NO_TOP_BOT_THM, F_CLOCK_COMP_CORRECT, F_CLOCK_SERE_FREE_def, 909 F_SERE_FREE___IMPLIES___F_SERE_FREE_F_CLOCK_COMP, 910 F_CLOCK_FREE___F_CLOCK_COMP]); 911 912 913 914val PSL_TO_LTL_THM = 915 store_thm 916 ("PSL_TO_LTL_THM", 917 ``!f v b t. ((IS_INFINITE_PROPER_PATH v) /\ (F_CLOCK_SERE_FREE f) /\ ~(t = b) /\ (PATH_PROP_FREE t v) /\ (PATH_PROP_FREE b v)) ==> 918 ((UF_SEM v f) = (LTL_SEM (CONVERT_PATH_PSL_LTL t b v) (RLTL_TO_LTL (P_PROP t) (P_PROP b) (PSL_TO_RLTL f))))``, 919 920 SIMP_TAC std_ss [LTL_SEM_def] THEN 921 METIS_TAC[RLTL_TO_LTL_THM, PSL_TO_RLTL_THM]); 922 923 924 925val PSL_TO_LTL___UF_KS_SEM = 926 store_thm 927 ("PSL_TO_LTL___UF_KS_SEM", 928 ``!M f. F_CLOCK_SERE_FREE f ==> 929 (UF_KS_SEM M f = 930 LTL_KS_SEM M (PSL_TO_LTL f))``, 931 932 SIMP_TAC std_ss [PSL_TO_LTL_def, PSL_TO_RLTL___UF_KS_SEM, RLTL_TO_LTL_THM___KS_SEM]); 933 934 935val PSL_TO_LTL___F_KS_SEM = 936 store_thm 937 ("PSL_TO_LTL___F_KS_SEM", 938 ``!M f c. F_SERE_FREE f ==> 939 (F_KS_SEM M c f = 940 LTL_KS_SEM M (PSL_TO_LTL_CLOCK c f))``, 941 942 SIMP_TAC std_ss [PSL_TO_LTL_CLOCK_def, PSL_TO_RLTL___F_KS_SEM, RLTL_TO_LTL_THM___KS_SEM]); 943 944val F_KS_SEM___TO___UF_KS_SEM = 945 store_thm 946 ("F_KS_SEM___TO___UF_KS_SEM", 947 ``!M f c. (F_KS_SEM M c f = 948 UF_KS_SEM M (F_CLOCK_COMP c f))``, 949 950 SIMP_TAC std_ss [F_KS_SEM_def, UF_KS_SEM_def, F_CLOCK_COMP_CORRECT]); 951 952 953val PSL_TO_LTL___UF_CONTRADICTION = 954 store_thm 955 ("PSL_TO_LTL___UF_CONTRADICTION", 956 ``!f. F_CLOCK_SERE_FREE f ==> 957 (UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE f = 958 LTL_IS_CONTRADICTION (PSL_TO_LTL f))``, 959 960 SIMP_TAC std_ss [PSL_TO_LTL_def, UF_IS_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE_def, 961 LTL_IS_CONTRADICTION_def, PSL_TO_RLTL___NO_TOP_BOT_THM, 962 RLTL_SEM_def, LTL_SEM_def, RLTL_TO_LTL_THM] THEN 963 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 964 Q_SPECL_NO_ASSUM 1 [`CONVERT_PATH_LTL_PSL v`] THEN 965 SIMP_ALL_TAC std_ss [CONVERT_PATH_LTL_PSL___IS_INFINITE_TOP_BOTTOM_FREE, 966 CONVERT_PATH_LTL_PSL___CONVERT_PATH_PSL_LTL], 967 968 PROVE_TAC[] 969 ]); 970 971 972val PSL_TO_LTL___UF_TAUTOLOGY = 973 store_thm 974 ("PSL_TO_LTL___UF_TAUTOLOGY", 975 ``!f. F_CLOCK_SERE_FREE f ==> 976 (UF_IS_TAUTOLOGY___INFINITE_TOP_BOTTOM_FREE f = 977 LTL_IS_TAUTOLOGY (PSL_TO_LTL f))``, 978 979 REPEAT STRIP_TAC THEN 980 ASSUME_TAC PSL_TO_LTL___UF_CONTRADICTION THEN 981 Q_SPEC_NO_ASSUM 0 `F_NOT f` THEN 982 SIMP_ALL_TAC std_ss [UF_IS_TAUTOLOGY_CONTRADICTION___INFINITE_TOP_BOTTOM_FREE___DUAL, 983 LTL_TAUTOLOGY_CONTRADICTION_DUAL, PSL_TO_LTL_def, PSL_TO_RLTL_def, 984 RLTL_TO_LTL_def, F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, F_SERE_FREE_def] THEN 985 PROVE_TAC[]); 986 987 988val PSL_TO_LTL___UF_EQUIVALENT = 989 store_thm 990 ("PSL_TO_LTL___UF_EQUIVALENT", 991 ``!f1 f2. F_CLOCK_SERE_FREE f1 ==> F_CLOCK_SERE_FREE f2 ==> 992 (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 = 993 LTL_IS_CONTRADICTION (LTL_NOT (LTL_EQUIV(PSL_TO_LTL f1, PSL_TO_LTL f2))))``, 994 995 REWRITE_TAC[UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE___TO___CONTRADICTION] THEN 996 REPEAT STRIP_TAC THEN 997 `F_CLOCK_SERE_FREE (F_NOT (F_IFF (f1,f2)))` by 998 FULL_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, F_SERE_FREE_def, F_IFF_def, F_OR_def, F_IMPLIES_def] THEN 999 ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_CONTRADICTION] THEN 1000 SIMP_TAC std_ss [PSL_TO_LTL_def, F_IFF_def, F_OR_def, F_IMPLIES_def, 1001 PSL_TO_RLTL_def, RLTL_TO_LTL_def, 1002 LTL_IS_CONTRADICTION_def, LTL_SEM_THM] THEN 1003 PROVE_TAC[]); 1004 1005 1006 1007 1008val IS_PSL_RELATIONS = 1009 store_thm 1010 ("IS_PSL_RELATIONS", 1011 ``!f. ((IS_PSL_F f = IS_PSL_G (F_NOT f)) /\ (IS_PSL_G f = IS_PSL_F (F_NOT f)) /\ 1012 (IS_PSL_FG f = IS_PSL_GF (F_NOT f)) /\ (IS_PSL_GF f = IS_PSL_FG (F_NOT f)) /\ 1013 (IS_PSL_F f ==> IS_PSL_FG f) /\ (IS_PSL_G f ==> IS_PSL_GF f) /\ 1014 (IS_PSL_G f ==> IS_PSL_FG f) /\ (IS_PSL_F f ==> IS_PSL_GF f) /\ 1015 (IS_PSL_PREFIX f ==> (IS_PSL_FG f /\ IS_PSL_GF f)))``, 1016 1017 INDUCT_THEN fl_induct ASSUME_TAC THEN 1018 FULL_SIMP_TAC std_ss [IS_PSL_G_def, IS_PSL_PREFIX_def, IS_PSL_GF_def] THEN 1019 METIS_TAC[] 1020 ); 1021 1022 1023val IS_PSL___NOT_F_CLOCK_SERE_FREE = 1024 store_thm 1025 ("IS_PSL___NOT_F_CLOCK_SERE_FREE", 1026 1027 ``!f. (~F_CLOCK_SERE_FREE f ==> ( 1028 ~IS_PSL_G f /\ ~IS_PSL_F f /\ ~IS_PSL_GF f /\ 1029 ~IS_PSL_FG f /\ ~IS_PSL_PREFIX f /\ ~IS_PSL_STREET f))``, 1030 1031 INDUCT_THEN fl_induct STRIP_ASSUME_TAC THEN 1032 ASM_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, F_SERE_FREE_def, IS_RLTL_THM, IS_PSL_THM, PSL_TO_RLTL_def] THEN 1033 PROVE_TAC[F_CLOCK_SERE_FREE_def]); 1034 1035 1036 1037val IS_PSL_RLTL_THM = 1038 store_thm 1039 ("IS_PSL_RLTL_THM", 1040 1041 ``!f. (F_CLOCK_SERE_FREE f ==> ( 1042 (IS_PSL_G f = IS_RLTL_G (PSL_TO_RLTL f)) /\ 1043 (IS_PSL_F f = IS_RLTL_F (PSL_TO_RLTL f)) /\ 1044 (IS_PSL_GF f = IS_RLTL_GF (PSL_TO_RLTL f)) /\ 1045 (IS_PSL_FG f = IS_RLTL_FG (PSL_TO_RLTL f)) /\ 1046 (IS_PSL_PREFIX f = IS_RLTL_PREFIX (PSL_TO_RLTL f)) /\ 1047 (IS_PSL_STREET f = IS_RLTL_STREET (PSL_TO_RLTL f))))``, 1048 1049 INDUCT_THEN fl_induct STRIP_ASSUME_TAC THEN 1050 ASM_SIMP_TAC std_ss [F_CLOCK_SERE_FREE_def, F_CLOCK_FREE_def, F_SERE_FREE_def, IS_RLTL_THM, IS_PSL_THM, PSL_TO_RLTL_def]); 1051 1052 1053 1054val IS_PSL_LTL_THM = 1055 store_thm 1056 ("IS_PSL_LTL_THM", 1057 1058 ``!f a r. (F_CLOCK_SERE_FREE f ==> ( 1059 (IS_PSL_G f = IS_LTL_G (RLTL_TO_LTL a r (PSL_TO_RLTL f))) /\ 1060 (IS_PSL_F f = IS_LTL_F (RLTL_TO_LTL a r (PSL_TO_RLTL f))) /\ 1061 (IS_PSL_GF f = IS_LTL_GF (RLTL_TO_LTL a r (PSL_TO_RLTL f))) /\ 1062 (IS_PSL_FG f = IS_LTL_FG (RLTL_TO_LTL a r (PSL_TO_RLTL f))) /\ 1063 (IS_PSL_PREFIX f = IS_LTL_PREFIX (RLTL_TO_LTL a r (PSL_TO_RLTL f))) /\ 1064 (IS_PSL_STREET f = IS_LTL_STREET (RLTL_TO_LTL a r (PSL_TO_RLTL f)))))``, 1065 1066 PROVE_TAC[IS_PSL_RLTL_THM, IS_RLTL_LTL_THM]); 1067 1068 1069 1070val FUTURE_LTL_TO_PSL_def = 1071 Define 1072 `(FUTURE_LTL_TO_PSL (LTL_PROP b) = (F_STRONG_BOOL (PROP_LOGIC_TO_BEXP b))) /\ 1073 (FUTURE_LTL_TO_PSL (LTL_NOT f) = (F_NOT (FUTURE_LTL_TO_PSL f))) /\ 1074 (FUTURE_LTL_TO_PSL (LTL_AND(f1,f2)) = (F_AND(FUTURE_LTL_TO_PSL f1, FUTURE_LTL_TO_PSL f2))) /\ 1075 (FUTURE_LTL_TO_PSL (LTL_NEXT f) = (F_NEXT (FUTURE_LTL_TO_PSL f))) /\ 1076 (FUTURE_LTL_TO_PSL (LTL_SUNTIL(f1,f2)) = (F_UNTIL(FUTURE_LTL_TO_PSL f1, FUTURE_LTL_TO_PSL f2)))`; 1077 1078 1079 1080val FUTURE_LTL_TO_PSL_THM = 1081 store_thm 1082 ("FUTURE_LTL_TO_PSL_THM", 1083 1084 ``!f t v. (IS_FUTURE_LTL f) ==> 1085 ((LTL_SEM_TIME t v f) = (UF_SEM (RESTN (CONVERT_PATH_LTL_PSL v) t) (FUTURE_LTL_TO_PSL f)))``, 1086 1087 1088 INDUCT_THEN ltl_induct ASSUME_TAC THENL [ 1089 SIMP_TAC std_ss [CONVERT_PATH_LTL_PSL_def, FUTURE_LTL_TO_PSL_def, UF_SEM_def, 1090 ELEM_INFINITE, RESTN_INFINITE, GSYM PROP_LOGIC_TO_BEXP_THM, LENGTH_def, GT, IS_FUTURE_LTL_def, LTL_SEM_TIME_def], 1091 1092 1093 FULL_SIMP_TAC std_ss [CONVERT_PATH_LTL_PSL_def, FUTURE_LTL_TO_PSL_def, UF_SEM_def, LTL_SEM_TIME_def, 1094 IS_FUTURE_LTL_def, COMPLEMENT_def, COMPLEMENT_LETTER_def, RESTN_INFINITE, combinTheory.o_DEF], 1095 1096 1097 FULL_SIMP_TAC std_ss [CONVERT_PATH_LTL_PSL_def, FUTURE_LTL_TO_PSL_def, UF_SEM_def, IS_FUTURE_LTL_def, LTL_SEM_TIME_def], 1098 1099 1100 FULL_SIMP_TAC arith_ss [CONVERT_PATH_LTL_PSL_def, FUTURE_LTL_TO_PSL_def, UF_SEM_def, IS_FUTURE_LTL_def, 1101 RESTN_INFINITE, LENGTH_def, GT, LTL_SEM_TIME_def] THEN 1102 `!t. SUC t = (t+1)` by DECIDE_TAC THEN 1103 METIS_TAC[], 1104 1105 1106 FULL_SIMP_TAC (arith_ss++resq_SS) [CONVERT_PATH_LTL_PSL_def, FUTURE_LTL_TO_PSL_def, IS_FUTURE_LTL_def, RESTN_INFINITE, 1107 LTL_SEM_TIME_def, UF_SEM_def, LENGTH_def, IN_LESSX, IN_LESS] THEN 1108 REPEAT STRIP_TAC THEN 1109 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1110 EXISTS_TAC ``k:num - t:num`` THEN 1111 REPEAT STRIP_TAC THENL [ 1112 `!n:num. k - t + (n+t) = (k + n)` by DECIDE_TAC THEN 1113 ASM_SIMP_TAC arith_ss [], 1114 1115 `?j'. j + t = j'` by PROVE_TAC[] THEN 1116 `(!n:num. j + (n+t) = (j' + n)) /\ (j' < k /\ t <= j')` by DECIDE_TAC THEN 1117 ASM_SIMP_TAC std_ss [] 1118 ], 1119 1120 EXISTS_TAC ``(k:num) + (t:num)`` THEN 1121 REPEAT STRIP_TAC THENL [ 1122 DECIDE_TAC, 1123 1124 ASM_SIMP_TAC arith_ss [], 1125 1126 `?j'. j - t = j'` by PROVE_TAC[] THEN 1127 `(!n:num. j + n = (j' + (n + t))) /\ (j' < k)` by DECIDE_TAC THEN 1128 ASM_SIMP_TAC std_ss [] 1129 ] 1130 ], 1131 1132 REWRITE_TAC[IS_FUTURE_LTL_def], 1133 REWRITE_TAC[IS_FUTURE_LTL_def] 1134 ]); 1135 1136 1137val IS_LTL_PSL_THM = 1138 store_thm 1139 ("IS_LTL_PSL_THM", 1140 1141 ``!f. (IS_FUTURE_LTL f) ==> 1142 ((IS_LTL_G f = IS_PSL_G (FUTURE_LTL_TO_PSL f)) /\ 1143 (IS_LTL_F f = IS_PSL_F (FUTURE_LTL_TO_PSL f)) /\ 1144 (IS_LTL_GF f = IS_PSL_GF (FUTURE_LTL_TO_PSL f)) /\ 1145 (IS_LTL_FG f = IS_PSL_FG (FUTURE_LTL_TO_PSL f)) /\ 1146 (IS_LTL_PREFIX f = IS_PSL_PREFIX (FUTURE_LTL_TO_PSL f)) /\ 1147 (IS_LTL_STREET f = IS_PSL_STREET (FUTURE_LTL_TO_PSL f)))``, 1148 1149 INDUCT_THEN ltl_induct STRIP_ASSUME_TAC THEN 1150 FULL_SIMP_TAC std_ss[IS_PSL_THM, IS_LTL_THM, IS_FUTURE_LTL_def, FUTURE_LTL_TO_PSL_def, LTL_OR_def]); 1151 1152val _ = export_theory(); 1153