1open HolKernel Parse boolLib bossLib; 2 3open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory prop_logicTheory 4 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory 5 listTheory pred_setTheory temporal_deep_mixedTheory 6 pred_setTheory rich_listTheory set_lemmataTheory pairTheory 7 ltl_to_automaton_formulaTheory numLib listLib rltlTheory 8 rltl_to_ltlTheory psl_to_rltlTheory PSLPathTheory UnclockedSemanticsTheory 9 ProjectionTheory symbolic_kripke_structureTheory 10 temporal_deep_simplificationsLibTheory; 11 12open Sanity; 13 14val _ = hide "S"; 15val _ = hide "I"; 16 17(* This theory contains lemmata and definitions used by 18 translationsLib. Most of these are simple correlars from 19 the lemmata in the specialised translation theories. In contrast 20 to the lemmata proved in these theories, the lemmata proved in 21 this theory are not of general interest. They are just 22 used as helpers for temporalLib. 23 24 Ideally they would be proved in translationsLib. However, then 25 the proofs would be redone every time, the library is used. *) 26 27val _ = new_theory "translationsLib"; 28 29(* Helper theorems for the rewrite translation of LTL to gen. Buechi *) 30Theorem LTL_TO_GEN_BUECHI___TRANSLATION_THM___MAX : 31 !x l DS pf sv. 32 ((pf = FST(LTL_TO_GEN_BUECHI l T x)) /\ 33 (DS = SND(LTL_TO_GEN_BUECHI l T x)) /\ 34 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv) ==> 35 (!i. LTL_SEM i l = A_SEM i (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv)) 36Proof 37 METIS_TAC [LTL_TO_GEN_BUECHI_THM, LTL_TO_GEN_BUECHI_DS___SEM___MAX] 38QED 39 40Theorem LTL_TO_GEN_BUECHI___TRANSLATION_THM___MIN : 41 !x l DS pf sv. 42 ((pf = FST(LTL_TO_GEN_BUECHI l x T)) /\ 43 (DS = SND(LTL_TO_GEN_BUECHI l x T)) /\ 44 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv) ==> 45 (!i. LTL_SEM i l = A_SEM i (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv)) 46Proof 47 METIS_TAC [LTL_TO_GEN_BUECHI_THM, LTL_TO_GEN_BUECHI_DS___SEM___MIN] 48QED 49 50(* Specicalised version 51 |- !DS p. 52 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 53 LTL_TO_GEN_BUECHI_DS___SEM 54 (ltl_to_gen_buechi_ds DS.SN DS.S0 (P_USED_VARS p UNION DS.IV) 55 DS.R DS.FC ((LTL_PROP p,T,T,(\sv. p)) INSERT DS.B)) 56 *) 57Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP___eval = 58 SIMP_RULE list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 59 EXTEND_LTL_TO_GEN_BUECHI_DS_def, 60 UNION_SING] 61 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP; 62 63(* |- !b1 b2 DS l pf. 64 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 65 (l,b1,b2,pf) IN DS.B ==> 66 LTL_TO_GEN_BUECHI_DS___SEM 67 (ltl_to_gen_buechi_ds DS.SN DS.S0 DS.IV DS.R DS.FC 68 ((LTL_NOT l,b2,b1,(\sv. P_NOT (pf sv))) INSERT DS.B)) 69 *) 70Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___eval = 71 SIMP_RULE list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 72 EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY, 73 GSYM AND_IMP_INTRO] 74 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT; 75 76val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___eval = save_thm 77 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___eval", 78 let 79 val thm = SIMP_RULE list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 80 EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY 81 ] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND; 82 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 83 in 84 thm 85 end); 86 87val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___eval = save_thm 88 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___eval", 89 let 90 val thm = SIMP_RULE list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 91 EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY 92 ] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR; 93 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 94 in 95 thm 96 end); 97 98val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___eval = save_thm 99 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___eval", 100 let 101 val thm = SIMP_RULE list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 102 EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY 103 ] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV; 104 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 105 in 106 thm 107 end); 108 109val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___eval = save_thm 110 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___eval", 111 SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY, 112 GSYM AND_IMP_INTRO] 113 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT); 114 115val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___eval = save_thm 116 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___eval", 117 SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY, 118 GSYM AND_IMP_INTRO] 119 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT); 120 121val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___eval = save_thm 122 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___eval", 123 SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY, 124 GSYM AND_IMP_INTRO] 125 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT); 126 127val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___eval = save_thm 128 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___eval", 129 let 130 val thm = SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY] 131 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL; 132 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 133 in 134 thm 135 end); 136 137val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___eval = save_thm 138 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___eval", 139 let 140 val thm = SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY] 141 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL; 142 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 143 in 144 thm 145 end); 146 147val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___eval = save_thm 148 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___eval", 149 let 150 val thm = SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY] 151 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE; 152 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 153 in 154 thm 155 end); 156 157val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___eval = save_thm 158 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___eval", 159 let 160 val thm = SIMP_RULE list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, UNION_SING, UNION_EMPTY] 161 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE; 162 val thm = ONCE_REWRITE_RULE [GSYM AND_IMP_INTRO] thm 163 in 164 thm 165 end); 166 167(* forget bindings specicalised version *) 168val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP___forget_eval = save_thm 169 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP___forget_eval", 170 SIMP_RULE list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 171 EXTEND_LTL_TO_GEN_BUECHI_DS_def, 172 UNION_EMPTY, 173 EMPTY_LTL_TO_GEN_BUECHI_DS_def, 174 ltl_to_gen_buechi_ds_REWRITES] 175 (prove (``!b1 b2 p. 176 LTL_TO_GEN_BUECHI_DS___SEM 177 (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS EMPTY_LTL_TO_GEN_BUECHI_DS 178 {(LTL_PROP p,b1,b2,(\sv. p))} (P_USED_VARS p))``, 179 METIS_TAC[CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP, 180 LTL_TO_GEN_BUECHI_DS___SEM___WEAKEN_BINDING, 181 EMPTY_LTL_TO_GEN_BUECHI_DS___SEM]))); 182 183val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___forget_eval = 184 prove (`` 185 !b1 b2 DS l pf. 186 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 187 (DS.B = {(l,b2,b1,pf)}) ==> 188 LTL_TO_GEN_BUECHI_DS___SEM 189 (LTL_TO_GEN_BUECHI_DS___SET_BINDINGS DS 190 {(LTL_NOT l,b1,b2,(\sv. P_NOT (pf sv)))})``, 191 192 REPEAT STRIP_TAC THEN 193 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___eval THEN 194 Q_SPECL_NO_ASSUM 0 [`b2`, `b1`, `DS`, `l`, `pf`] THEN 195 UNDISCH_HD_TAC THEN 196 ASM_SIMP_TAC std_ss [IN_SING, LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def] THEN 197 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 198 SIMP_TAC std_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, IN_SING, IN_INSERT]); 199 200val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___forget_eval = save_thm 201 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___forget_eval", 202 SIMP_RULE std_ss [LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def] 203 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT___forget_eval); 204 205val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___forget_eval = 206 prove (`` 207 !b1 b2 DS1 DS2 l1 l2 pf1 pf2. 208 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 209 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 210 (DS1.B = {(l1,b1,b2,pf1)}) ==> 211 (DS2.B = {(l2,b1,b2,pf2)}) ==> 212 LTL_TO_GEN_BUECHI_DS___SEM 213 (LTL_TO_GEN_BUECHI_DS___SET_BINDINGS 214 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) 215 {(LTL_AND (l1, l2), b1,b2,(\sv. P_AND(pf1 sv, pf2 (\n. sv (n + DS1.SN)))))})``, 216 217 REPEAT STRIP_TAC THEN 218 `?DS'. LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS'` by METIS_TAC[] THEN 219 SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\ 220 (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 221 GSYM_NO_TAC 0 (*DS'*) THEN 222 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 223 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 224 ) THEN 225 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 226 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 227 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___eval THEN 228 Q_SPECL_NO_ASSUM 0 [`DS'`, `b1`,`b2`, `b1`, `b2`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 229 UNDISCH_HD_TAC THEN 230 ASM_REWRITE_TAC[LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def] THEN 231 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 232 SIMP_TAC std_ss [SUBSET_DEF, IN_SING, IN_INSERT, ltl_to_gen_buechi_ds_REWRITES]); 233 234val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___forget_eval = save_thm 235 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___forget_eval", 236 SIMP_RULE std_ss [LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def, 237 ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 238 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND___forget_eval); 239 240val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___forget_eval = 241 prove (`` 242 !b1 b2 DS1 DS2 l1 l2 pf1 pf2. 243 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 244 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 245 (DS1.B = {(l1,b1,b2,pf1)}) ==> 246 (DS2.B = {(l2,b1,b2,pf2)}) ==> 247 LTL_TO_GEN_BUECHI_DS___SEM 248 (LTL_TO_GEN_BUECHI_DS___SET_BINDINGS 249 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) 250 {(LTL_OR (l1, l2), b1,b2,(\sv. P_OR(pf1 sv, pf2 (\n. sv (n + DS1.SN)))))})``, 251 252 REPEAT STRIP_TAC THEN 253 `?DS'. LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS'` by METIS_TAC[] THEN 254 SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\ 255 (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 256 GSYM_NO_TAC 0 (*DS'*) THEN 257 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 258 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 259 ) THEN 260 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 261 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 262 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___eval THEN 263 Q_SPECL_NO_ASSUM 0 [`DS'`, `b1`, `b2`, `b1`, `b2`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 264 UNDISCH_HD_TAC THEN 265 ASM_REWRITE_TAC[LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def] THEN 266 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 267 SIMP_TAC std_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, IN_SING, IN_INSERT]); 268 269Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___forget_eval = 270 SIMP_RULE std_ss [LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def, 271 ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 272 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR___forget_eval; 273 274val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___forget_eval = 275 prove (`` 276 !b1 b2 DS1 DS2 l1 l2 pf1 pf2. 277 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 278 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 279 (DS1.B = {(l1,T,T,pf1)}) ==> 280 (DS2.B = {(l2,T,T,pf2)}) ==> 281 LTL_TO_GEN_BUECHI_DS___SEM 282 (LTL_TO_GEN_BUECHI_DS___SET_BINDINGS 283 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) 284 {(LTL_EQUIV (l1, l2),b1,b2,(\sv. P_EQUIV(pf1 sv, pf2 (\n. sv (n + DS1.SN)))))})``, 285 286 REPEAT STRIP_TAC THEN 287 `?DS'. LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS'` by METIS_TAC[] THEN 288 SUBGOAL_TAC `(l1,T,T,pf1) IN DS'.B /\ 289 (l2,T,T,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 290 GSYM_NO_TAC 0 (*DS'*) THEN 291 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 292 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 293 ) THEN 294 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 295 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 296 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV THEN 297 Q_SPECL_NO_ASSUM 0 [`DS'`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 298 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 299 `LTL_TO_GEN_BUECHI_DS___SEM 300 (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS' 301 {(LTL_EQUIV (l1,l2),b1,b2, 302 (\sv. 303 P_EQUIV (pf1 sv,(\sv. pf2 (\n. sv (n + DS1.SN))) sv)))} 304 {})` by METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___WEAKEN_BINDING] THEN 305 UNDISCH_HD_TAC THEN 306 ASM_REWRITE_TAC[LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def, 307 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 308 EXTEND_LTL_TO_GEN_BUECHI_DS_def] THEN 309 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 310 SIMP_TAC list_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, 311 IN_SING, IN_INSERT, IN_UNION, UNION_EMPTY]); 312 313Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___forget_eval = 314 SIMP_RULE std_ss [LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def, 315 ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 316 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV___forget_eval; 317 318Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___forget_eval : 319 !b1 b2 DS l pf. 320 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 321 (DS.B = {(l,b1,b2,pf)}) ==> 322 LTL_TO_GEN_BUECHI_DS___SEM 323 (ltl_to_gen_buechi_ds (DS.SN + 1) DS.S0 DS.IV 324 ((\sv. XP_EQUIV (XP_PROP (sv DS.SN),XP_NEXT (pf sv)))::DS.R) 325 DS.FC {(LTL_NEXT l,b1,b2,(\sv. P_PROP (sv DS.SN)))}) 326Proof 327 REPEAT STRIP_TAC THEN 328 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT___eval THEN 329 Q_SPECL_NO_ASSUM 0 [`b1`,`b2`, `DS`, `l`, `pf`] THEN 330 UNDISCH_HD_TAC THEN 331 ASM_SIMP_TAC std_ss [IN_SING] THEN 332 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 333 SIMP_TAC std_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, IN_SING, IN_INSERT] 334QED 335 336Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___forget_eval : 337 !b1 b2 DS l pf. 338 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 339 (DS.B = {(l,b1,b2,pf)}) ==> 340 LTL_TO_GEN_BUECHI_DS___SEM 341 (ltl_to_gen_buechi_ds (DS.SN + 1) ((DS.SN,F)::DS.S0) DS.IV 342 ((\sv. XP_EQUIV (XP_NEXT_PROP (sv DS.SN),XP_CURRENT (pf sv)))::DS.R) 343 DS.FC {(LTL_PSNEXT l,b1,b2,(\sv. P_PROP (sv DS.SN)))}) 344Proof 345 REPEAT STRIP_TAC THEN 346 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT___eval THEN 347 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `DS`, `l`, `pf`] THEN 348 UNDISCH_HD_TAC THEN 349 ASM_SIMP_TAC std_ss [IN_SING] THEN 350 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 351 SIMP_TAC std_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, IN_SING, IN_INSERT] 352QED 353 354Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___forget_eval : 355 !b1 b2 DS l pf. 356 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 357 (DS.B = {(l,b1,b2,pf)}) ==> 358 LTL_TO_GEN_BUECHI_DS___SEM 359 (ltl_to_gen_buechi_ds (DS.SN + 1) ((DS.SN,F)::DS.S0) DS.IV 360 ((\sv. XP_EQUIV (XP_NEXT_PROP (sv DS.SN),XP_CURRENT (P_NOT (pf sv))))::DS.R) 361 DS.FC {(LTL_PNEXT l,b1,b2,(\sv. P_NOT (P_PROP (sv DS.SN))))}) 362Proof 363 REPEAT STRIP_TAC THEN 364 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT___eval THEN 365 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `DS`, `l`, `pf`] THEN 366 UNDISCH_HD_TAC THEN 367 ASM_SIMP_TAC std_ss [IN_SING] THEN 368 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 369 SIMP_TAC std_ss [ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, IN_SING, IN_INSERT] 370QED 371 372val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___forget_eval = prove (`` 373 !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'. 374 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS') ==> 375 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 376 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 377 (DS1.B = {(l1,b1,b2,pf1)}) ==> 378 (DS2.B = {(l2,b1,b2,pf2)}) ==> 379 LTL_TO_GEN_BUECHI_DS___SEM 380 (ltl_to_gen_buechi_ds (DS'.SN + 1) DS'.S0 DS'.IV 381 ((\sv. 382 XP_EQUIV 383 (XP_PROP (sv DS'.SN), 384 XP_OR 385 (XP_CURRENT ((\sv. pf2 (\n. sv (n + DS1.SN))) sv), 386 XP_AND 387 (XP_CURRENT (pf1 sv),XP_NEXT_PROP (sv DS'.SN))))):: 388 DS'.R) 389 ((if b1 then 390 [(\sv. 391 P_IMPL 392 (P_PROP (sv DS'.SN), 393 (\sv. pf2 (\n. sv (n + DS1.SN))) sv))] 394 else 395 []) <> DS'.FC) 396 {(LTL_SUNTIL (l1,l2),b1,b2,(\sv. P_PROP (sv DS'.SN)))})``, 397 398 REPEAT STRIP_TAC THEN 399 SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\ 400 (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 401 GSYM_NO_TAC 4 (*DS'*) THEN 402 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 403 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 404 ) THEN 405 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 406 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 407 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___eval THEN 408 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b1`, `b2`, `b1`, `DS'`, `l1`, `l2`, `pf1`, 409 `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 410 UNDISCH_HD_TAC THEN 411 ASM_REWRITE_TAC[LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def] THEN 412 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 413 SIMP_TAC std_ss [SUBSET_DEF, IN_SING, IN_INSERT, ltl_to_gen_buechi_ds_REWRITES]); 414 415Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___forget_eval = 416 SIMP_RULE std_ss [ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 417 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL___forget_eval; 418 419val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___forget_eval = prove (`` 420 !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'. 421 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS') ==> 422 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 423 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 424 (DS1.B = {(l1,b1,b2,pf1)}) ==> 425 (DS2.B = {(l2,b1,b2,pf2)}) ==> 426 LTL_TO_GEN_BUECHI_DS___SEM 427 (ltl_to_gen_buechi_ds (DS'.SN + 1) ((DS'.SN,F)::DS'.S0) DS'.IV 428 ((\sv. 429 XP_EQUIV 430 (XP_NEXT_PROP (sv DS'.SN), 431 XP_OR 432 (XP_CURRENT ((\sv. pf2 (\n. sv (n + DS1.SN))) sv), 433 XP_AND (XP_CURRENT (pf1 sv),XP_PROP (sv DS'.SN))))):: 434 DS'.R) DS'.FC 435 {(LTL_PSUNTIL (l1,l2),b1,b2, 436 (\sv. 437 P_OR 438 ((\sv. pf2 (\n. sv (n + DS1.SN))) sv, 439 P_AND (pf1 sv,P_PROP (sv DS'.SN)))))})``, 440 441 REPEAT STRIP_TAC THEN 442 SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\ 443 (l2,b1,b2,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 444 GSYM_NO_TAC 4 (*DS'*) THEN 445 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 446 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 447 ) THEN 448 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 449 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 450 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___eval THEN 451 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b1`, `b2`, `DS'`, `l1`, `l2`, `pf1`, 452 `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 453 UNDISCH_HD_TAC THEN 454 ASM_REWRITE_TAC[LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def] THEN 455 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 456 SIMP_TAC std_ss [SUBSET_DEF, IN_SING, IN_INSERT, ltl_to_gen_buechi_ds_REWRITES]); 457 458Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___forget_eval = 459 SIMP_RULE std_ss [ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 460 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL___forget_eval; 461 462val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___forget_eval = prove (`` 463 !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'. 464 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS') ==> 465 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 466 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 467 (DS1.B = {(l1,b1,b2,pf1)}) ==> 468 (DS2.B = {(l2,b2,b1,pf2)}) ==> 469 LTL_TO_GEN_BUECHI_DS___SEM 470 (ltl_to_gen_buechi_ds (DS'.SN + 1) DS'.S0 DS'.IV 471 ((\sv. 472 XP_EQUIV 473 (XP_PROP (sv DS'.SN), 474 XP_OR 475 (XP_CURRENT ((\sv. pf2 (\n. sv (n + DS1.SN))) sv), 476 XP_AND 477 (XP_CURRENT (P_NOT (pf1 sv)),XP_NEXT_PROP (sv DS'.SN))))):: 478 DS'.R) 479 ((if ~b2 then 480 [] 481 else 482 [(\sv. 483 P_IMPL 484 (P_PROP (sv DS'.SN), 485 (\sv. pf2 (\n. sv (n + DS1.SN))) sv))]) <> DS'.FC) 486 {(LTL_BEFORE (l1,l2),b1,b2,(\sv. P_NOT (P_PROP (sv DS'.SN))))})``, 487 488 REPEAT STRIP_TAC THEN 489 SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\ 490 (l2,b2,b1,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 491 GSYM_NO_TAC 4 (*DS'*) THEN 492 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 493 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 494 ) THEN 495 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 496 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 497 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___eval THEN 498 Q_SPECL_NO_ASSUM 0 [`b1`,`b2`,`b2`,`b1`,`b2`, `DS'`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 499 UNDISCH_HD_TAC THEN 500 ASM_REWRITE_TAC[] THEN 501 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 502 SIMP_TAC std_ss [SUBSET_DEF, IN_SING, IN_INSERT, ltl_to_gen_buechi_ds_REWRITES]); 503 504 505Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___forget_eval = 506 SIMP_RULE std_ss [ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 507 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE___forget_eval; 508 509val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___forget_eval = prove (`` 510 !b1 b2 DS1 DS2 l1 l2 pf1 pf2 DS'. 511 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = DS') ==> 512 LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 513 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 514 (DS1.B = {(l1,b1,b2,pf1)}) ==> 515 (DS2.B = {(l2,b2,b1,pf2)}) ==> 516 LTL_TO_GEN_BUECHI_DS___SEM 517 (ltl_to_gen_buechi_ds (DS'.SN + 1) ((DS'.SN,F)::DS'.S0) DS'.IV 518 ((\sv. 519 XP_EQUIV 520 (XP_NEXT_PROP (sv DS'.SN), 521 XP_OR 522 (XP_CURRENT ((\sv. pf2 (\n. sv (n + DS1.SN))) sv), 523 XP_AND (XP_CURRENT (P_NOT (pf1 sv)),XP_PROP (sv DS'.SN))))):: 524 DS'.R) DS'.FC 525 {(LTL_PBEFORE (l1,l2),b1,b2, 526 (\sv. 527 P_NOT (P_OR 528 ((\sv. pf2 (\n. sv (n + DS1.SN))) sv, 529 P_AND (P_NOT (pf1 sv),P_PROP (sv DS'.SN))))))})``, 530 531 REPEAT STRIP_TAC THEN 532 SUBGOAL_TAC `(l1,b1,b2,pf1) IN DS'.B /\ 533 (l2,b2,b1,(\sv. pf2 (\n. sv (n + DS1.SN)))) IN DS'.B` THEN1 ( 534 GSYM_NO_TAC 4 (*DS'*) THEN 535 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 536 ltl_to_gen_buechi_ds_REWRITES, IN_SING, IN_UNION, IMAGE_SING] 537 ) THEN 538 `LTL_TO_GEN_BUECHI_DS___SEM DS'` by 539 METIS_TAC[LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM] THEN 540 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___eval THEN 541 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b2`, `b1`, `DS'`, `l1`, `l2`, `pf1`, `(\sv. pf2 (\n. sv (n + DS1.SN)))`] THEN 542 UNDISCH_HD_TAC THEN 543 ASM_REWRITE_TAC[] THEN 544 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 545 SIMP_TAC std_ss [SUBSET_DEF, IN_SING, IN_INSERT, ltl_to_gen_buechi_ds_REWRITES]); 546 547Theorem CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___forget_eval = 548 SIMP_RULE std_ss [ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___PRODUCT_def] 549 CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE___forget_eval; 550 551Theorem LTL_TO_GEN_BUECHI_DS___SEM___MAX___eval : 552 !DS l l' pf a. 553 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 554 (LTL_EQUIVALENT l l') ==> 555 (l',T, a, pf) IN DS.B ==> !sv. ( 556 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> 557 !i. 558 LTL_SEM i l = A_SEM i (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv)) 559Proof 560 METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___MAX, LTL_SEM_def, LTL_EQUIVALENT_def] 561QED 562 563Theorem LTL_TO_GEN_BUECHI_DS___SEM___MIN___eval : 564 !DS l l' pf a. 565 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 566 (LTL_EQUIVALENT l l') ==> 567 (l',a, T,pf) IN DS.B ==> !sv. ( 568 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> 569 !i. 570 LTL_SEM i l = A_SEM i (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv)) 571Proof 572 METIS_TAC [LTL_TO_GEN_BUECHI_DS___SEM___MIN, LTL_SEM_def, LTL_EQUIVALENT_def] 573QED 574 575Theorem LTL_TO_GEN_BUECHI_DS___KS_SEM___MAX___eval : 576 !DS l l' pf a. 577 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 578 (LTL_EQUIVALENT l l') ==> 579 (l',T, a,pf) IN DS.B ==> 580 !sv. LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> 581 !M. 582 LTL_KS_SEM M l = A_KS_SEM M (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv) 583Proof 584 METIS_TAC [LTL_TO_GEN_BUECHI_DS___KS_SEM___MAX, LTL_KS_SEM_def, 585 LTL_EQUIVALENT_def, LTL_SEM_def] 586QED 587 588Theorem LTL_TO_GEN_BUECHI_DS___KS_SEM___MIN___eval : 589 !DS l l' pf a. 590 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 591 (LTL_EQUIVALENT l l') ==> 592 (l',a,T,pf) IN DS.B ==> 593 !sv. LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> 594 !M. 595 LTL_KS_SEM M l = A_KS_SEM M (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv) 596Proof 597 METIS_TAC [LTL_TO_GEN_BUECHI_DS___KS_SEM___MIN, LTL_KS_SEM_def, 598 LTL_SEM_def, LTL_EQUIVALENT_def] 599QED 600 601Theorem LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE___eval : 602 !DS l l' pf a. 603 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 604 (LTL_EQUIVALENT l l') ==> 605 (l',a,T,pf) IN DS.B ==> !M sv. ( 606 IS_ELEMENT_ITERATOR sv DS.SN 607 (DS.IV UNION SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M) ==> ( 608 LTL_KS_SEM M l = IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 609 (SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT M 610 (symbolic_kripke_structure 611 (P_AND 612 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, 613 P_NOT (pf sv))) (XP_BIGAND (MAP (\xp. xp sv) DS.R)))) 614 (MAP (\x. x sv) DS.FC))) 615Proof 616 REPEAT STRIP_TAC THEN 617 ASSUME_TAC (GSYM LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN 618 Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `M`, `a`] THEN 619 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN DISCH_TAC THEN WEAKEN_HD_TAC THEN 620 FULL_SIMP_TAC std_ss [LTL_KS_SEM_def, LTL_SEM_def, LTL_EQUIVALENT_def] 621QED 622 623Theorem LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___KRIPKE_STRUCTURE___eval : 624 !DS l l' pf a. 625 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 626 (LTL_EQUIVALENT l l') ==> 627 (l',T,a,pf) IN DS.B ==> !sv. (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> ( 628 LTL_IS_CONTRADICTION l = IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 629 (symbolic_kripke_structure 630 (P_AND 631 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, 632 pf sv)) (XP_BIGAND (MAP (\xp. xp sv) DS.R))) 633 (MAP (\x. x sv) DS.FC))) 634Proof 635 REPEAT STRIP_TAC THEN 636 ASSUME_TAC (GSYM LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___KRIPKE_STRUCTURE) THEN 637 Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `a`] THEN 638 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN DISCH_TAC THEN WEAKEN_HD_TAC THEN 639 FULL_SIMP_TAC std_ss [LTL_IS_CONTRADICTION_def, LTL_SEM_def, LTL_EQUIVALENT_def] 640QED 641 642Theorem LTL_TO_GEN_BUECHI_DS___SEM___EQUIVALENT___KRIPKE_STRUCTURE___eval : 643 !DS l1 l2 l' pf a. 644 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 645 (LTL_EQUIVALENT (LTL_EVENTUAL (LTL_NOT (LTL_EQUIV(l1, l2)))) l') ==> 646 (l',T, a,pf) IN DS.B ==> !sv. (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> ( 647 LTL_EQUIVALENT l1 l2 = IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 648 (symbolic_kripke_structure 649 (P_AND 650 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, 651 pf sv)) (XP_BIGAND (MAP (\xp. xp sv) DS.R))) 652 (MAP (\x. x sv) DS.FC))) 653Proof 654 REPEAT STRIP_TAC THEN 655 ASSUME_TAC (GSYM LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___KRIPKE_STRUCTURE___eval) THEN 656 Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `l'`, `pf`, `a`] THEN 657 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [LTL_EQUIVALENT_def] THEN DISCH_TAC THEN WEAKEN_HD_TAC THEN 658 FULL_SIMP_TAC std_ss [LTL_IS_CONTRADICTION_def, LTL_EQUIVALENT_def, LTL_SEM_THM] THEN 659 GSYM_NO_TAC 2 THEN 660 ASM_SIMP_TAC std_ss [] THEN 661 PROVE_TAC[] 662QED 663 664Theorem IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_cong : 665 !S0 R fc S0' R' fc'. 666 (PROP_LOGIC_EQUIVALENT S0 S0') ==> 667 (XPROP_LOGIC_EQUIVALENT R R') ==> 668 (PROP_LOGIC_EQUIVALENT_LIST_AS_SET fc fc') ==> 669 (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) fc = 670 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0' R') fc') 671Proof 672 SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, 673 XPROP_LOGIC_EQUIVALENT_def, 674 symbolic_kripke_structure_REWRITES, 675 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 676 IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 677 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 678 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 679 PROP_LOGIC_EQUIVALENT_LIST_AS_SET_def, 680 congToolsLibTheory.LIST_AS_SET_CONGRUENCE_RELATION_def] THEN 681 METIS_TAC[] 682QED 683 684Theorem IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___VAR_RENAMING___eval : 685 !f k fc. COND_IMP_EQ (INJ f (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS k UNION 686 LIST_BIGUNION (MAP P_USED_VARS fc)) UNIV) 687 (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE k fc) 688 (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 689 (SYMBOLIC_KRIPKE_STRUCTURE_VAR_RENAMING f k) (MAP (P_VAR_RENAMING f) fc)) 690Proof 691 SIMP_TAC std_ss [COND_IMP_EQ___REWRITE, 692 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___IDENTIFY_VARIABLES, 693 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE___VAR_RENAMING] 694QED 695 696Theorem IS_ELEMENT_ITERATOR___ID : 697 !S n0. IS_ELEMENT_ITERATOR (\n:num. n) n0 S = 698 RES_FORALL S (\n. n >= n0) 699Proof 700 SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IMP_DISJ_THM, 701 NOT_LESS, GREATER_EQ, RES_FORALL_THM] THEN 702 PROVE_TAC[] 703QED 704 705Theorem INJ___ADD_FUNC : 706 !S f n:num. INJ (\x. f x + n) S UNIV = INJ f S UNIV 707Proof 708 SIMP_TAC std_ss [INJ_DEF, IN_UNIV] 709QED 710 711val POS_START_def = Define ` 712 (POS_START n [] h = 0) /\ 713 (POS_START n (h'::l) h = (if (h = h') then (SUC n) else (POS_START (SUC n) l h)))`; 714 715Theorem POS_START_NOT_FOUND : 716 !n l h. ((POS_START n l h = 0) = ~(MEM h l)) 717Proof 718 Induct_on `l` THENL 719 [ SIMP_TAC list_ss [POS_START_def], 720 ASM_SIMP_TAC list_ss [POS_START_def] THEN 721 REPEAT GEN_TAC THEN 722 Cases_on `h' = h` THENL [ 723 ASM_SIMP_TAC arith_ss [], 724 ASM_REWRITE_TAC[] ] ] 725QED 726 727Theorem POS_START_FOUND : 728 !n l h. MEM h l ==> (POS_START n l h > n) /\ (EL ((PRE (POS_START n l h)) - n) l = h) 729Proof 730 Induct_on `l` THENL [ 731 SIMP_TAC list_ss [], 732 733 ASM_SIMP_TAC list_ss [POS_START_def] THEN 734 REPEAT GEN_TAC THEN 735 Cases_on `h' = h` THENL [ 736 ASM_SIMP_TAC list_ss [], 737 738 ASM_SIMP_TAC list_ss [] THEN 739 STRIP_TAC THEN 740 Q_SPECL_NO_ASSUM 2 [`SUC n`, `h'`] THEN 741 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THENL [ 742 ASM_SIMP_TAC arith_ss [], 743 Cases_on `(POS_START (SUC n) l h')` THEN ( 744 SIMP_ALL_TAC arith_ss [] 745 ) THEN 746 Cases_on `n'` THEN SIMP_ALL_TAC arith_ss [] THEN 747 `SUC n'' - n = SUC (n'' - n)` by DECIDE_TAC THEN 748 ASM_SIMP_TAC list_ss [] ] ] ] 749QED 750 751Theorem POS_START_RANGE : 752 !n l h. (POS_START n l h > n) \/ (POS_START n l h = 0) 753Proof 754 PROVE_TAC[POS_START_FOUND, POS_START_NOT_FOUND] 755QED 756 757Theorem INJ_POS_START___MP_HELPER : 758 !l S n. (!s. s IN S ==> MEM s l) ==> 759 (ALL_DISTINCT l ==> INJ (\x. PRE (POS_START n l x)) S UNIV) 760Proof 761SIMP_TAC std_ss [INJ_DEF, IN_UNIV] THEN 762Induct_on `l` THENL [ 763 SIMP_TAC list_ss [IMP_DISJ_THM, MEMBER_NOT_EMPTY, NOT_IN_EMPTY], 764 765 SIMP_TAC list_ss [POS_START_def] THEN 766 REPEAT STRIP_TAC THEN 767 Q_SPECL_NO_ASSUM 6 [`S DELETE h`, `SUC n`] THEN 768 UNDISCH_HD_TAC THEN 769 `(!s. s IN S /\ ~(s = h) ==> MEM s l)` by METIS_TAC[] THEN 770 ASM_REWRITE_TAC [IN_DELETE] THEN 771 Cases_on `x = h` THEN Cases_on `x' = h` THENL [ 772 ASM_REWRITE_TAC[], 773 774 `(POS_START (SUC n) l x' > SUC n)` by 775 PROVE_TAC[POS_START_FOUND] THEN 776 FULL_SIMP_TAC arith_ss [], 777 778 `(POS_START (SUC n) l x > SUC n)` by 779 PROVE_TAC[POS_START_FOUND] THEN 780 FULL_SIMP_TAC arith_ss [], 781 FULL_SIMP_TAC std_ss [] ] ] 782QED 783 784Theorem PRE_POS_START___REWRITES : 785 !n h. (PRE (POS_START n [] h) = 0) /\ 786 (!n h h' l. (PRE (POS_START n (h'::l) h)) = 787 (if (h' = h) then n else PRE (POS_START (SUC n) l h))) 788Proof 789 SIMP_TAC std_ss [POS_START_def, COND_RAND] 790QED 791 792Theorem NUM_FINITE_INJ_EXISTS : 793 !S. FINITE S ==> ?f:'a -> num. INJ f S UNIV 794Proof 795 REPEAT STRIP_TAC THEN 796 SUBGOAL_TAC `INFINITE (UNIV:num set)` THEN1 ( 797 SIMP_TAC std_ss [INFINITE_UNIV] THEN 798 EXISTS_TAC ``\x. SUC x`` THEN 799 SIMP_TAC arith_ss [] THEN 800 EXISTS_TAC ``0:num`` THEN 801 SIMP_TAC arith_ss [] 802 ) THEN 803 MP_TAC (Q.SPECL [`S`, `EMPTY`] 804 (INST_TYPE [beta |-> num] temporal_deep_mixedTheory.FINITE_INJ_EXISTS)) THEN 805 ASM_SIMP_TAC std_ss [FINITE_EMPTY, DISJOINT_EMPTY] 806QED 807 808Theorem RES_FORALL_INSERT : 809 !x xs P. RES_FORALL (x INSERT xs) P <=> P x /\ RES_FORALL xs P 810Proof 811 SIMP_TAC std_ss [res_quanTheory.RES_FORALL, IN_INSERT, DISJ_IMP_THM, FORALL_AND_THM] THEN 812 METIS_TAC[] 813QED 814 815val _ = export_theory(); 816