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