1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val base_dir = concat Globals.HOLDIR "/examples/temporal_deep/"; 7loadPath := (concat base_dir "src/tools") :: (concat base_dir "src/deep_embeddings") :: !loadPath; 8map load 9 ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory", 10 "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory", 11 "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "temporal_deep_mixedTheory", 12 "pairTheory", "symbolic_kripke_structureTheory", 13 "numLib"]; 14*) 15 16open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory 17 prop_logicTheory 18 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory 19 pred_setTheory rich_listTheory set_lemmataTheory temporal_deep_mixedTheory pairTheory symbolic_kripke_structureTheory 20 numLib; 21open Sanity; 22 23val _ = hide "S"; 24val _ = hide "I"; 25 26 27(* 28show_assums := false; 29show_assums := true; 30show_types := true; 31show_types := false; 32quietdec := false; 33*) 34 35 36val _ = new_theory "ltl_to_automaton_formula"; 37 38(**************************************************************** 39 * A datastructure for the translation. For the idea behind this 40 * datastructure look at LTL_TO_GEN_BUECHI_DS_SEM 41 * 42 * It contains the necessary informations to construct a GENERALISED 43 * Buechi-Automaton. However, state variables have to be distinct to 44 * input variables. To avoid varrenamings, the set of input variables 45 * is explicitely modelled and all parameters get 46 * a function enumeration state var distinct from this 47 * set of input variables 48 ****************************************************************) 49val LTL_TO_GEN_BUECHI_DS_def = 50 Hol_datatype 51 `ltl_to_gen_buechi_ds = 52 <| SN: num; (*number of needed state variables*) 53 S0: (num # bool) list; (*initial states, state variables can be true or false or unspecified*) 54 IV: ('var->bool); (*the set of input variables*) 55 R: ((num->'var) -> 'var xprop_logic) list; (*transition relation*) 56 FC: ((num->'var) -> 'var prop_logic) list; (*fairness conditions*) 57 B: ('var ltl # bool # bool # ((num->'var) -> 'var prop_logic)) set (*Bindings*) 58 |>`; 59 60val ltl_to_gen_buechi_ds_SN = DB.fetch "-" "ltl_to_gen_buechi_ds_SN"; 61val ltl_to_gen_buechi_ds_S0 = DB.fetch "-" "ltl_to_gen_buechi_ds_S0"; 62val ltl_to_gen_buechi_ds_IV = DB.fetch "-" "ltl_to_gen_buechi_ds_IV"; 63val ltl_to_gen_buechi_ds_R = DB.fetch "-" "ltl_to_gen_buechi_ds_R"; 64val ltl_to_gen_buechi_ds_FC = DB.fetch "-" "ltl_to_gen_buechi_ds_FC"; 65val ltl_to_gen_buechi_ds_B = DB.fetch "-" "ltl_to_gen_buechi_ds_B"; 66val ltl_to_gen_buechi_ds_11 = DB.fetch "-" "ltl_to_gen_buechi_ds_11"; 67 68val ltl_to_gen_buechi_ds_REWRITES = save_thm("ltl_to_gen_buechi_ds_REWRITES", 69 LIST_CONJ [ltl_to_gen_buechi_ds_SN, 70 ltl_to_gen_buechi_ds_S0, 71 ltl_to_gen_buechi_ds_IV, 72 ltl_to_gen_buechi_ds_R, 73 ltl_to_gen_buechi_ds_FC, 74 ltl_to_gen_buechi_ds_B, 75 ltl_to_gen_buechi_ds_11]) 76 77 78(*Some definitions to get meaning to this datastructure*) 79val LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def = 80 Define 81 `LTL_TO_GEN_BUECHI_DS___INITIAL_STATES (DS:'a ltl_to_gen_buechi_ds) = (\sv:num->'a. 82 P_BIGAND (MAP (\(n, b). if b then P_PROP (sv n) else P_NOT(P_PROP (sv n))) DS.S0))`; 83 84val LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def = 85 Define 86 `LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS DS = (\sv. 87 (A_BIGAND (MAP (\p. ACCEPT_COND_GF (p sv)) DS.FC)))`; 88 89 90val LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def = 91 Define 92 `LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS = 93 (\sv s. (?n. (n < DS.SN) /\ (s = sv n)))`; 94 95 96val LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS = 97 store_thm 98 ("LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS", 99 100 ``!DS s sv. s IN LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv = 101 (?n. (n < DS.SN) /\ (s = sv n))``, 102 103 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, IN_DEF]); 104 105 106val LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___COUNT = 107 store_thm 108 ("LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___COUNT", 109 110 ``!DS sv. LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv = 111 IMAGE sv (count DS.SN)``, 112 113 SIMP_TAC std_ss [EXTENSION, 114 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, IN_IMAGE, 115 IN_COUNT] THEN 116 METIS_TAC[]); 117 118 119val LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___FINITE = 120 store_thm 121 ("LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___FINITE", 122 123 ``!DS sv. FINITE (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)``, 124 125 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___COUNT, 126 IMAGE_FINITE, FINITE_COUNT]); 127 128 129 130val LTL_TO_GEN_BUECHI_DS___USED_VARS_def = 131 Define 132 `LTL_TO_GEN_BUECHI_DS___USED_VARS DS = 133 (\sv. (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) UNION 134 (LIST_BIGUNION (MAP (\xpf. XP_USED_VARS (xpf sv)) DS.R)) UNION 135 (LIST_BIGUNION (MAP (\pf. P_USED_VARS (pf sv)) DS.FC)) UNION 136 (BIGUNION (IMAGE (\(l, b1, b2, pf). (P_USED_VARS (pf sv) UNION LTL_USED_VARS l)) DS.B)))`; 137 138 139 140val LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def = 141 Define 142 `LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS = 143 (\sv. symbolic_semi_automaton 144 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) 145 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv) 146 (XP_BIGAND (MAP (\xp. xp sv) DS.R)))`; 147 148 149 150(*a suitable function creating new state variables*) 151val LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def = 152 Define ` 153 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv = (IS_ELEMENT_ITERATOR sv DS.SN DS.IV)`; 154 155 156val LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def = 157 Define 158 `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv = 159 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w /\ A_SEM (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w) (LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS DS sv))`; 160 161 162val LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET = 163 store_thm 164 ("LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET", 165 166 ``!DS sv i w. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv ==> 167 PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)``, 168 169 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 170 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 171 symbolic_semi_automaton_REWRITES]); 172 173 174 175(*a fair run, that is minimal according to 176 some special propositional formula *) 177val LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def = 178 Define 179 `LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN DS i w p sv = 180 !w'. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w' sv ==> 181 (!t. P_SEM ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w) t) p ==> 182 P_SEM ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w') t) p)`; 183 184 185(*a fair run, that is maximal according to 186 some special propositional formula *) 187val LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def = 188 Define 189 `LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN DS i w p sv = 190 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN DS i w (P_NOT p) sv`; 191 192(*a fair run, such that the propositinal part of 193 the binding behaves as the ltl part 194 and such that the run is according to the binding minimal or maximal according to the propositional part *) 195val LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def = 196 Define 197 `LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l, b1, b2, pf) i sv = 198 (((!t. LTL_SEM_TIME t i l = P_SEM (w t UNION (i t DIFF (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))) (pf sv))) /\ 199 (b1 ==> LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN DS i w (pf sv) sv) /\ 200 (b2 ==> LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN DS i w (pf sv) sv) 201 )`; 202 203 204val LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE = 205 store_thm 206 ("LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE", 207 208 ``!DS sv i w l pf b1 b2. LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l, b1, b2, pf) i sv = 209 (!wi. (wi = INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w) ==> 210 211 ((!t. (LTL_SEM_TIME t i l = P_SEM (wi t) (pf sv))) /\ 212 !w' wi'. (LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w' sv /\ 213 (wi' = INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w')) ==> 214 ((!t. (b1 /\ P_SEM (wi' t) (pf sv) ==> P_SEM (wi t) (pf sv))) /\ 215 (!t. (b2 /\ P_SEM (wi t) (pf sv) ==> P_SEM (wi' t) (pf sv)))) 216 ))``, 217 218 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, P_SEM_def, 219 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def] THEN 220 REPEAT GEN_TAC THEN 221 REMAINS_TAC `!t. (w t UNION (i t DIFF LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) = 222 (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w t)` THEN1 ( 223 METIS_TAC[] 224 ) THEN 225 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 226 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 227 symbolic_semi_automaton_REWRITES] 228 ); 229 230 231 232(*The meaning "semantics" of the datastructure*) 233val LTL_TO_GEN_BUECHI_DS___SEM_def = 234 Define 235 `LTL_TO_GEN_BUECHI_DS___SEM DS = 236 !sv. 237 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> 238 239 ((!n b. (MEM (n, b) DS.S0 ==> (n < DS.SN))) /\ 240 (LTL_TO_GEN_BUECHI_DS___USED_VARS DS sv SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) /\ 241 (!i. ?w. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv /\ 242 (!l b1 b2 pf. ((l,b1,b2,pf) IN DS.B) ==> 243 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l, b1, b2, pf) i sv 244 )))`; 245 246 247val LTL_TO_GEN_BUECHI_DS___EQUIVALENT_def = 248 Define 249 `LTL_TO_GEN_BUECHI_DS___EQUIVALENT DS DS' = 250 (LTL_TO_GEN_BUECHI_DS___SEM DS = LTL_TO_GEN_BUECHI_DS___SEM DS')`; 251 252 253 254(*This meaning implies that all bindings in it, we 255 can easily construct equivalent generalised buechi 256 automata*) 257 258val LTL_TO_GEN_BUECHI_DS___A_NDET_def = 259 Define 260 `LTL_TO_GEN_BUECHI_DS___A_NDET DS pf = 261 (\sv. A_NDET (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv, 262 A_AND(LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS DS sv, ACCEPT_COND_PROP (pf sv))))`; 263 264 265val LTL_TO_GEN_BUECHI_DS___A_UNIV_def = 266 Define 267 `LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf = 268 (\sv. A_UNIV (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv, 269 A_IMPL(LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS DS sv, ACCEPT_COND_PROP (pf sv))))`; 270 271 272val LTL_TO_GEN_BUECHI_DS___KRIPKE_STRUCTURE_def = 273 Define 274 `LTL_TO_GEN_BUECHI_DS___KRIPKE_STRUCTURE DS pf = 275 (\sv. symbolic_kripke_structure (P_AND(pf sv, (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv))) 276 (XP_BIGAND (MAP (\xp. xp sv) DS.R)))`; 277 278 279val LTL_TO_GEN_BUECHI_DS___SEM___MAX = 280 store_thm 281 ("LTL_TO_GEN_BUECHI_DS___SEM___MAX", 282 283 ``!DS l pf sv a. 284 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 285 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, T, a, pf) IN DS.B) ==> 286 287 (!i. LTL_SEM i l = A_SEM i (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv))``, 288 289 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def, LTL_SEM_def, LTL_TO_GEN_BUECHI_DS___A_NDET_def, 290 A_SEM_def, ACCEPT_COND_PROP_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, 291 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, 292 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 293 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def] THEN 294 REPEAT STRIP_TAC THEN 295 SPECL_NO_ASSUM 1 [``sv:num->'a``] THEN 296 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 297 SPECL_NO_ASSUM 0 [``i:num->'a set``] THEN 298 CLEAN_ASSUMPTIONS_TAC THEN 299 SPECL_NO_ASSUM 2 [``l:'a ltl``, ``T``, ``a:bool``, ``pf:(num->'a)->'a prop_logic``] THEN 300 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN REPEAT STRIP_TAC THEN 301 METIS_TAC[P_SEM_def] 302 ); 303 304 305 306val LTL_TO_GEN_BUECHI_DS___SEM___MIN = 307 store_thm 308 ("LTL_TO_GEN_BUECHI_DS___SEM___MIN", 309 310 ``!DS l pf sv a. 311 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 312 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, a, T, pf) IN DS.B) ==> 313 314 (!i. LTL_SEM i l = A_SEM i (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv))``, 315 316 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def, LTL_SEM_THM, LTL_TO_GEN_BUECHI_DS___A_UNIV_def, 317 A_SEM_THM, ACCEPT_COND_PROP_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, 318 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, 319 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 320 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def] THEN 321 REPEAT STRIP_TAC THEN 322 SPECL_NO_ASSUM 1 [``sv:num->'a``] THEN 323 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 324 SPECL_NO_ASSUM 0 [``i:num->'a set``] THEN 325 CLEAN_ASSUMPTIONS_TAC THEN 326 SPECL_NO_ASSUM 2 [``l:'a ltl``, ``a:bool``, ``T``, ``pf:(num->'a)->'a prop_logic``] THEN 327 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN REPEAT STRIP_TAC THEN 328 METIS_TAC[P_SEM_def] 329 ); 330 331 332val LTL_TO_GEN_BUECHI_DS___KS_SEM___MIN = 333 store_thm 334 ("LTL_TO_GEN_BUECHI_DS___KS_SEM___MIN", 335 336 ``!DS l pf sv a. 337 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 338 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, a, T, pf) IN DS.B) ==> 339 340 (!M. LTL_KS_SEM M l = A_KS_SEM M (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv))``, 341 342 SIMP_TAC std_ss [LTL_KS_SEM_def, A_KS_SEM_def] THEN 343 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___MIN] 344 ); 345 346 347val LTL_TO_GEN_BUECHI_DS___KS_SEM___MAX = 348 store_thm 349 ("LTL_TO_GEN_BUECHI_DS___KS_SEM___MAX", 350 351 ``!DS l pf sv a. 352 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 353 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, T, a, pf) IN DS.B) ==> 354 355 (!M. LTL_KS_SEM M l = A_KS_SEM M (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv))``, 356 357 SIMP_TAC std_ss [LTL_KS_SEM_def, A_KS_SEM_def] THEN 358 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___MAX] 359 ); 360 361 362 363val LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___MAX = 364 store_thm 365 ("LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___MAX", 366 367 ``!DS l pf sv a. 368 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 369 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, T, a, pf) IN DS.B) ==> 370 371 (LTL_IS_CONTRADICTION l = A_IS_EMPTY (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv))``, 372 373 REPEAT STRIP_TAC THEN 374 ASM_SIMP_TAC std_ss [A_IS_EMPTY_def, LTL_IS_CONTRADICTION_def] THEN 375 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___MAX] 376 ); 377 378 379 380val LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___MIN = 381 store_thm 382 ("LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___MIN", 383 384 ``!DS l pf sv a. 385 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 386 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, a, T, pf) IN DS.B) ==> 387 388 (LTL_IS_CONTRADICTION l = A_IS_EMPTY (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv))``, 389 390 REPEAT STRIP_TAC THEN 391 ASM_SIMP_TAC std_ss [A_IS_EMPTY_def, LTL_IS_CONTRADICTION_def] THEN 392 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___MIN] 393 ); 394 395 396 397val LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___MIN = 398 store_thm 399 ("LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___MIN", 400 401 ``!DS l pf sv a. 402 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 403 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (LTL_EVENTUAL l, a, T, pf) IN DS.B) ==> 404 405 (LTL_EQUIVALENT l LTL_FALSE = A_IS_EMPTY (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv))``, 406 407 REPEAT STRIP_TAC THEN 408 ASM_SIMP_TAC std_ss [A_IS_EMPTY_def, LTL_IS_CONTRADICTION_def, LTL_EQUIVALENT_def] THEN 409 ASSUME_TAC (GSYM LTL_TO_GEN_BUECHI_DS___SEM___MIN) THEN 410 Q_SPECL_NO_ASSUM 0 [`DS`, `LTL_EVENTUAL l`, `pf`, `sv`, `a`] THEN 411 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 412 ASM_SIMP_TAC std_ss [LTL_SEM_THM] THEN 413 PROVE_TAC[] 414 ); 415 416 417val LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___MAX = 418 store_thm 419 ("LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___MAX", 420 421 ``!DS l pf sv a. 422 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ 423 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (LTL_EVENTUAL l, T, a, pf) IN DS.B) ==> 424 425 (LTL_EQUIVALENT l LTL_FALSE = A_IS_EMPTY (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv))``, 426 427 REPEAT STRIP_TAC THEN 428 ASM_SIMP_TAC std_ss [A_IS_EMPTY_def, LTL_IS_CONTRADICTION_def, LTL_EQUIVALENT_def] THEN 429 ASSUME_TAC (GSYM LTL_TO_GEN_BUECHI_DS___SEM___MAX) THEN 430 Q_SPECL_NO_ASSUM 0 [`DS`, `LTL_EVENTUAL l`, `pf`, `sv`, `a`] THEN 431 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 432 ASM_SIMP_TAC std_ss [LTL_SEM_THM] THEN 433 PROVE_TAC[] 434 ); 435 436 437 438 439val GEN_BUECHI_IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY = 440 store_thm 441 ("GEN_BUECHI_IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY", 442 ``!A fc. 443 A_IS_EMPTY (A_NDET(A, A_BIGAND (MAP (\p. ACCEPT_COND_GF p) fc))) = 444 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure A.S0 A.R) fc``, 445 446 447SIMP_TAC std_ss [A_IS_EMPTY_def, 448 A_SEM_THM, IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 449 IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 450 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 451 symbolic_kripke_structure_REWRITES, 452 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 453 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 454 IS_TRANSITION_def, 455 A_BIGAND_SEM, 456 ACCEPT_COND_GF_def, ACCEPT_F_def, 457 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, 458 MEM_MAP, GSYM LEFT_EXISTS_AND_THM 459 ] THEN 460REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 461 Q_SPECL_NO_ASSUM 0 [`p`, `PATH_RESTRICT p A.S`] THEN 462 CLEAN_ASSUMPTIONS_TAC THENL [ 463 SIMP_ASSUMPTIONS_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, 464 INTER_SUBSET], 465 466 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION___SPLIT], 467 468 SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INPUT_RUN_STATE_UNION___SPLIT] THEN 469 PROVE_TAC[], 470 471 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION___SPLIT] THEN 472 PROVE_TAC[] 473 ], 474 475 476 Q_SPEC_NO_ASSUM 0 `INPUT_RUN_PATH_UNION A i w` THEN 477 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN 478 PROVE_TAC[] 479]); 480 481 482val LTL_TO_GEN_BUECHO_DS___A_NDET___IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY = 483 store_thm 484 ("LTL_TO_GEN_BUECHO_DS___A_NDET___IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY", 485 ``!DS sv pf. 486 A_IS_EMPTY (LTL_TO_GEN_BUECHI_DS___A_NDET DS pf sv) = 487 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure 488 (P_AND 489 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,pf sv)) 490 (XP_BIGAND (MAP (\xp. xp sv) DS.R))) (MAP (\x. x sv) DS.FC)``, 491 492 REPEAT STRIP_TAC THEN 493 ASSUME_TAC (GSYM GEN_BUECHI_IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY) THEN 494 Q_SPEC_NO_ASSUM 0 `symbolic_semi_automaton (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) 495 (P_AND (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,pf sv)) 496 (XP_BIGAND (MAP (\xp. xp sv) DS.R))` THEN 497 FULL_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES] THEN 498 WEAKEN_HD_TAC THEN 499 500 SIMP_TAC std_ss [A_IS_EMPTY_def, LTL_TO_GEN_BUECHI_DS___A_NDET_def, 501 A_SEM_THM, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 502 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 503 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 504 IS_TRANSITION_def, symbolic_semi_automaton_REWRITES, 505 P_SEM_THM, ACCEPT_COND_PROP_def, ACCEPT_COND_SEM_def, 506 ACCEPT_COND_SEM_TIME_def, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 507 MAP_MAP_o, combinTheory.o_DEF] THEN 508 METIS_TAC[]); 509 510 511val GEN_BUECHI_KS_SEM___TO___KRIPKE_STRUCTURE_EMPTY = 512 store_thm 513 ("GEN_BUECHI_KS_SEM___TO___KRIPKE_STRUCTURE_EMPTY", 514 ``!A fc M. DISJOINT A.S (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M) ==> ( 515 A_KS_SEM M (A_UNIV(A, A_NOT (A_BIGAND (MAP (\p. ACCEPT_COND_GF p) fc)))) = 516 IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE ( 517 (SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT M 518 (symbolic_kripke_structure A.S0 A.R))) fc)``, 519 520 521SIMP_TAC std_ss [A_IS_EMPTY_def, A_KS_SEM_def, 522 A_SEM_THM, IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 523 IS_FAIR_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 524 IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 525 symbolic_kripke_structure_REWRITES, 526 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 527 IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 528 IS_TRANSITION_def, 529 A_BIGAND_SEM, 530 ACCEPT_COND_GF_def, ACCEPT_F_def, 531 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, 532 MEM_MAP, GSYM LEFT_EXISTS_AND_THM, 533 SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, 534 IS_INITIAL_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE_def, 535 XP_SEM_THM, P_SEM_THM 536 ] THEN 537REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 538 Q_SPEC_NO_ASSUM 0 `p` THEN 539 Cases_on `(!n. XP_SEM M.R (p n,p (SUC n))) /\ P_SEM (p 0) M.S0` THENL [ 540 FULL_SIMP_TAC std_ss [IMP_DISJ_THM], 541 METIS_TAC[] 542 ] THEN 543 Q_SPEC_NO_ASSUM 2 `PATH_RESTRICT p A.S` THEN 544 CLEAN_ASSUMPTIONS_TAC THENL [ 545 SIMP_ASSUMPTIONS_TAC std_ss [PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, 546 INTER_SUBSET], 547 548 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION___SPLIT], 549 550 SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, INPUT_RUN_STATE_UNION___SPLIT] THEN 551 PROVE_TAC[], 552 553 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION___SPLIT] THEN 554 PROVE_TAC[] 555 ], 556 557 SUBGOAL_TAC `P_SEM (INPUT_RUN_PATH_UNION A i w 0) M.S0` THEN1 ( 558 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def] THEN 559 UNDISCH_NO_TAC 3 THEN 560 ONCE_REWRITE_TAC[P_USED_VARS_INTER_THM] THEN 561 IMP_TO_EQ_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN 562 SIMP_ALL_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 563 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 564 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, PATH_SUBSET_def] THEN 565 METIS_TAC[] 566 ) THEN 567 SUBGOAL_TAC `!n. 568 XP_SEM M.R 569 (INPUT_RUN_STATE_UNION A (i n) (w n), 570 INPUT_RUN_STATE_UNION A (i (SUC n)) (w (SUC n)))` THEN1 ( 571 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def] THEN 572 UNDISCH_NO_TAC 5 THEN 573 ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN 574 IMP_TO_EQ_TAC THEN FORALL_EQ_STRIP_TAC THEN BINOP_TAC THEN SIMP_TAC std_ss [] THEN 575 SIMP_ALL_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 576 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 577 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, PATH_SUBSET_def, XP_USED_VARS_def] THEN 578 METIS_TAC[] 579 ) THEN 580 Q_SPEC_NO_ASSUM 7 `INPUT_RUN_PATH_UNION A i w` THEN 581 METIS_TAC[INPUT_RUN_PATH_UNION_def] 582]); 583 584 585 586val LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE = 587 store_thm 588 ("LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE", 589 590 ``!DS l pf sv M a. 591 (IS_ELEMENT_ITERATOR sv DS.SN (DS.IV UNION (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)) /\ 592 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, a, T, pf) IN DS.B) ==> 593 594 (LTL_KS_SEM M l = IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 595 (SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT M (symbolic_kripke_structure (P_AND 596 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,P_NOT (pf sv))) 597 (XP_BIGAND (MAP (\xp. xp sv) DS.R)))) (MAP (\x. x sv) DS.FC))``, 598 599 REPEAT STRIP_TAC THEN 600 ASSUME_TAC LTL_TO_GEN_BUECHI_DS___KS_SEM___MIN THEN 601 Q_SPECL_NO_ASSUM 0 [`DS`, `l`, `pf`, `sv`, `a`] THEN 602 UNDISCH_HD_TAC THEN 603 SUBGOAL_TAC `LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv` THEN1 ( 604 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def] THEN 605 PROVE_TAC[IS_ELEMENT_ITERATOR_SUBSET, SUBSET_UNION] 606 ) THEN 607 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN DISCH_TAC THEN WEAKEN_HD_TAC THEN 608 609 SUBGOAL_TAC `A_KS_SEM M (LTL_TO_GEN_BUECHI_DS___A_UNIV DS pf sv) = 610 A_KS_SEM M (A_UNIV(symbolic_semi_automaton 611 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) 612 (P_AND(LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, (P_NOT (pf sv)))) 613 (XP_BIGAND (MAP (\xp. xp sv) DS.R)), 614 A_NOT (A_BIGAND ((MAP (\p. ACCEPT_COND_GF p)) ((MAP (\x. x sv) DS.FC))))))` THEN1 ( 615 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___A_UNIV_def, 616 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, A_SEM_THM, 617 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 618 symbolic_semi_automaton_REWRITES, INPUT_RUN_PATH_UNION_def, 619 INPUT_RUN_STATE_UNION_def, P_SEM_THM, ACCEPT_COND_PROP_def, 620 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, IMP_DISJ_THM, 621 IS_TRANSITION_def, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, MAP_MAP_o, combinTheory.o_DEF, A_KS_SEM_def] THEN 622 FORALL_EQ_STRIP_TAC THEN 623 BOOL_EQ_STRIP_TAC THEN 624 FORALL_EQ_STRIP_TAC THEN 625 REPEAT BOOL_EQ_STRIP_TAC 626 ) THEN 627 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 628 629 REMAINS_TAC `DISJOINT (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) 630 (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS M)` THEN1 ( 631 PROVE_TAC[GEN_BUECHI_KS_SEM___TO___KRIPKE_STRUCTURE_EMPTY, 632 symbolic_semi_automaton_REWRITES] 633 ) THEN 634 SIMP_ALL_TAC std_ss [GSYM SUBSET_COMPL_DISJOINT, IS_ELEMENT_ITERATOR_def, 635 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, SUBSET_DEF, IN_ABS, 636 IN_COMPL, IN_UNION] THEN 637 PROVE_TAC[] 638 ); 639 640 641 642 643val LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___KRIPKE_STRUCTURE = 644 save_thm 645 ("LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___KRIPKE_STRUCTURE", 646 647 SIMP_RULE std_ss [LTL_TO_GEN_BUECHO_DS___A_NDET___IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY] 648 LTL_TO_GEN_BUECHI_DS___SEM___CONTRADICTION___MAX); 649 650 651val LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___KRIPKE_STRUCTURE = 652 save_thm 653 ("LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___KRIPKE_STRUCTURE", 654 655 SIMP_RULE std_ss [LTL_TO_GEN_BUECHO_DS___A_NDET___IS_EMPTY___TO___KRIPKE_STRUCTURE_EMPTY] 656 LTL_TO_GEN_BUECHI_DS___SEM___GEN_CONTRADICTION___MAX); 657 658 659 660 661 662 663 664val LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS = 665 store_thm 666 ("LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS", 667 668 ``!DS sv l b1 b2 pf. 669 (LTL_TO_GEN_BUECHI_DS___SEM DS /\ LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ (l, b1, b2, pf) IN DS.B) ==> 670 (P_USED_VARS (pf sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) /\ 671 LTL_USED_VARS l SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))``, 672 673 REWRITE_TAC [GSYM UNION_SUBSET] THEN 674 REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN 675 676 REMAINS_TAC `(P_USED_VARS (pf sv) UNION LTL_USED_VARS l) SUBSET LTL_TO_GEN_BUECHI_DS___USED_VARS DS sv` THEN1 ( 677 SIMP_ASSUMPTIONS_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def] THEN 678 PROVE_TAC[SUBSET_TRANS] 679 ) THEN 680 681 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def] THEN 682 REMAINS_TAC `P_USED_VARS (pf sv) UNION LTL_USED_VARS l SUBSET 683 BIGUNION (IMAGE (\(l,b1,b2,pf). P_USED_VARS (pf sv) UNION LTL_USED_VARS l) DS.B)` THEN1 ( 684 PROVE_TAC[SUBSET_UNION, UNION_ASSOC, SUBSET_TRANS] 685 ) THEN 686 SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, 687 GSYM RIGHT_EXISTS_AND_THM] THEN 688 REPEAT STRIP_TAC THEN 689 Q_TAC EXISTS_TAC `(l, b1, b2, pf)` THEN 690 ASM_SIMP_TAC std_ss [] 691 ); 692 693 694 695val LTL_TO_GEN_BUECHI_DS___SEM___S0 = 696 store_thm 697 ("LTL_TO_GEN_BUECHI_DS___SEM___S0", 698 699 ``!DS sv A. 700 (LTL_TO_GEN_BUECHI_DS___SEM DS /\ LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ (A = LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv)) ==> 701 (P_USED_VARS A.S0 SUBSET A.S)``, 702 703 704 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___SEM_def, 705 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def] THEN 706 REPEAT GEN_TAC THEN 707 `?S0. DS.S0 = S0` by PROVE_TAC[] THEN 708 ASM_REWRITE_TAC[] THEN 709 REPEAT STRIP_TAC THEN 710 `(!n b. MEM (n,b) S0 ==> n < DS.SN)` by PROVE_TAC[] THEN 711 UNDISCH_HD_TAC THEN 712 REPEAT WEAKEN_HD_TAC THEN 713 Induct_on `S0` THENL [ 714 SIMP_TAC list_ss [P_BIGAND_def, P_USED_VARS_def, EMPTY_SUBSET], 715 716 SIMP_TAC list_ss [P_BIGAND_def, P_USED_VARS_def, UNION_SUBSET] THEN 717 REPEAT STRIP_TAC THENL [ 718 ALL_TAC, 719 METIS_TAC[] 720 ] THEN 721 Cases_on `h` THEN 722 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_S, 723 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def] THEN 724 Cases_on `r` THEN 725 SIMP_ALL_TAC arith_ss [SUBSET_DEF, P_USED_VARS_def, IN_SING] THEN 726 SIMP_TAC std_ss [IN_DEF] THEN 727 METIS_TAC[IN_DEF] 728 ]); 729 730 731 732val LTL_TO_GEN_BUECHI_DS___SEM___R = 733 store_thm 734 ("LTL_TO_GEN_BUECHI_DS___SEM___R", 735 736 ``!DS sv A. 737 (LTL_TO_GEN_BUECHI_DS___SEM DS /\ LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv /\ (A = LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv)) ==> 738 (XP_USED_VARS A.R SUBSET (A.S UNION DS.IV))``, 739 740 741 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___SEM_def, 742 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_VARS_def, 743 UNION_SUBSET] THEN 744 REPEAT GEN_TAC THEN 745 `?R. DS.R = R` by PROVE_TAC[] THEN 746 ASM_REWRITE_TAC[] THEN 747 REPEAT STRIP_TAC THEN 748 `LIST_BIGUNION (MAP (\xpf. XP_USED_VARS (xpf sv)) R) SUBSET 749 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by METIS_TAC[] THEN 750 UNDISCH_HD_TAC THEN 751 REPEAT WEAKEN_HD_TAC THEN 752 Induct_on `R` THENL [ 753 SIMP_TAC list_ss [LIST_BIGUNION_def, XP_USED_VARS___DIRECT_DEF, XP_BIGAND_def, 754 EMPTY_SUBSET, UNION_EMPTY], 755 756 757 SIMP_TAC list_ss [LIST_BIGUNION_def, XP_USED_VARS___DIRECT_DEF, XP_BIGAND_def, 758 UNION_SUBSET] THEN 759 REPEAT STRIP_TAC THEN 760 METIS_TAC[] 761 ]); 762 763 764 765(*This are the basic definitions, now we can start to 766 construct such valid datastructures*) 767 768(*The basic one is the empty datastructure*) 769val EMPTY_LTL_TO_GEN_BUECHI_DS_def = 770 Define ` 771 EMPTY_LTL_TO_GEN_BUECHI_DS = ltl_to_gen_buechi_ds 0 [] {} [] [] {}`; 772 773 774val EMPTY_LTL_TO_GEN_BUECHI_DS___SEM = 775 store_thm 776 ("EMPTY_LTL_TO_GEN_BUECHI_DS___SEM", 777 ``LTL_TO_GEN_BUECHI_DS___SEM EMPTY_LTL_TO_GEN_BUECHI_DS``, 778 779 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___SEM_def, EMPTY_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, 780 IS_ELEMENT_ITERATOR_0, LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, A_BIGAND_def, 781 A_SEM_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, IS_TRANSITION_def, XP_BIGAND_def, XP_SEM_def, 782 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, P_BIGAND_def, P_SEM_def, 783 PATH_SUBSET_def, SUBSET_DEF, LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 784 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, LTL_TO_GEN_BUECHI_DS___USED_VARS_def, LIST_BIGUNION_def, NOT_IN_EMPTY, 785 IMAGE_EMPTY, BIGUNION_EMPTY] THEN 786 EXISTS_TAC ``\n:num. EMPTY`` THEN 787 SIMP_TAC std_ss [NOT_IN_EMPTY]); 788 789 790(*Then we can extend an existing datastructure*) 791val EXTEND_LTL_TO_GEN_BUECHI_DS_def = 792 Define ` 793 EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B' = 794 (ltl_to_gen_buechi_ds (DS.SN + n') (S0' ++ DS.S0) (IV' UNION DS.IV) (R' ++ DS.R) (FC' ++ DS.FC) (B' UNION DS.B))`; 795 796 797val EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES = 798 store_thm 799 ("EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES", 800 ``!DS n' S0' IV' R' FC' B'. 801 802 ((EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B').SN = DS.SN + n') /\ 803 ((EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B').S0 = S0'++DS.S0) /\ 804 ((EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B').IV = IV' UNION DS.IV) /\ 805 ((EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B').R = R'++DS.R) /\ 806 ((EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B').FC = FC'++DS.FC) /\ 807 ((EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B').B = B' UNION DS.B)``, 808 809 SIMP_TAC std_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES]); 810 811 812 813val EXTEND_LTL_TO_GEN_BUECHI_DS___EXTEND_LTL_TO_GEN_BUECHI_DS = 814 store_thm 815 ("EXTEND_LTL_TO_GEN_BUECHI_DS___EXTEND_LTL_TO_GEN_BUECHI_DS", 816 ``!DS n' S0' IV' R' FC' B' n'' S0'' IV'' R'' FC'' B''. 817 818 (EXTEND_LTL_TO_GEN_BUECHI_DS (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') n'' S0'' IV'' R'' FC'' B'') = 819 (EXTEND_LTL_TO_GEN_BUECHI_DS DS (n''+n') (S0''++S0') (IV'' UNION IV') (R''++R') (FC''++FC') (B'' UNION B'))``, 820 821 SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, 822 UNION_ASSOC]); 823 824 825val EXTEND_LTL_TO_GEN_BUECHI_DS___USED_VARS = 826 store_thm 827 ("EXTEND_LTL_TO_GEN_BUECHI_DS___USED_VARS", 828 ``!DS sv n' S0' IV' R' FC' B'. 829 LTL_TO_GEN_BUECHI_DS___USED_VARS DS sv SUBSET 830 LTL_TO_GEN_BUECHI_DS___USED_VARS (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') sv``, 831 832 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, SUBSET_DEF, IN_UNION, 833 EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, LIST_BIGUNION_APPEND, 834 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 835 IN_BIGUNION, IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM] THEN 836 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL [ 837 NTAC 3 DISJ1_TAC THEN 838 EXISTS_TAC ``n:num`` THEN 839 DECIDE_TAC, 840 841 PROVE_TAC[] 842 ]); 843 844 845 846 847val EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR = 848 store_thm 849 ("EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR", 850 851 ``!DS sv n' S0' IV' R' FC' B'. 852 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') sv ==> 853 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv``, 854 855 REPEAT GEN_TAC THEN 856 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES] THEN 857 `DS.SN <= DS.SN + n'` by DECIDE_TAC THEN 858 `DS.IV SUBSET IV' UNION DS.IV` by PROVE_TAC[SUBSET_UNION] THEN 859 PROVE_TAC[IS_ELEMENT_ITERATOR_GE, IS_ELEMENT_ITERATOR_SUBSET]); 860 861 862 863val EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN = 864 store_thm 865 ("EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN", 866 867``!DS sv w i DS' w' n' S0' IV' R' FC' B'. 868 869(LTL_TO_GEN_BUECHI_DS___SEM DS /\ 870 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS' sv /\ 871(!n b. (MEM (n, b) S0' ==> (n < n' + DS.SN))) /\ 872(DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') /\ 873(w' = INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w)) ==> 874 875(LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS' i w sv = 876 877PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS' sv) /\ 878P_SEM (w 0) (P_BIGAND (MAP (\(n, b). if b then P_PROP (sv n) else P_NOT(P_PROP (sv n))) S0')) /\ 879(!n xp. MEM xp R' ==> XP_SEM (xp sv) (w' n, w' (SUC n))) /\ 880(!p. MEM p FC' ==> A_SEM w' (ACCEPT_COND_GF (p sv))) /\ 881LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w 882 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv)``, 883 884 885SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def, 886 LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 887 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 888 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, IS_TRANSITION_def, 889 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 890 symbolic_semi_automaton_REWRITES, PATH_SUBSET_def, 891 (SIMP_RULE std_ss [] PATH_RESTRICT_SUBSET), 892 PATH_RESTRICT_def, PATH_MAP_def] THEN 893REPEAT STRIP_TAC THEN 894CONJ_EQ_STRIP_TAC THEN 895 896SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS_def, 897 ltl_to_gen_buechi_ds_REWRITES, 898 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 899 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 900 XP_BIGAND_SEM, P_BIGAND_SEM, A_BIGAND_SEM, 901 MEM_MAP, GSYM LEFT_FORALL_IMP_THM, GSYM EXISTS_OR_THM, 902 GSYM LEFT_AND_OVER_OR, 903 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def] THEN 904 905SPECL_NO_ASSUM 3 [``sv:num->'a``] THEN 906`LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv` by 907 METIS_TAC[EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 908FULL_SIMP_TAC std_ss [] THEN 909WEAKEN_NO_TAC 1 THEN 910 911 912SUBGOAL_TAC `(!y. MEM y S0' \/ MEM y DS.S0 ==> 913 P_SEM (w 0 UNION (i 0 DIFF (\s. ?n. n < n' + DS.SN /\ (s = sv n)))) 914 ((\(n,b). (if b then P_PROP (sv n) else P_NOT (P_PROP (sv n)))) y)) = 915 916 ((!y. MEM y DS.S0 ==> P_SEM 917 (w 0 INTER (\s. ?n. n < DS.SN /\ (s = sv n)) UNION 918 (i 0 DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) 919 ((\(n,b). (if b then P_PROP (sv n) else P_NOT (P_PROP (sv n)))) y)) /\ 920 (!y. MEM y S0' ==> P_SEM (w 0) 921 ((\(n,b). (if b then P_PROP (sv n) else P_NOT (P_PROP (sv n)))) y)))` THEN1 ( 922 923 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 924 FORALL_EQ_STRIP_TAC THEN 925 Cases_on `y` THEN 926 SIMP_TAC std_ss [P_SEM_def, IN_UNION, IN_DIFF, IN_INTER, 927 prove (``!s b p1 p2. P_SEM s (if b then p1 else p2) = 928 if b then P_SEM s p1 else P_SEM s p2``, METIS_TAC[]), 929 prove (``!x f. x IN (\x. f x) = f x``, 930 SIMP_TAC std_ss [IN_DEF])] THEN 931 SIMP_ALL_TAC arith_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 932 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IS_ELEMENT_ITERATOR_def, 933 IN_UNION, SUBSET_DEF, LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 934 `!n. n < DS.SN ==> n < n' + DS.SN` by DECIDE_TAC THEN 935 Cases_on `r` THEN 936 METIS_TAC[] 937) THEN 938ASM_SIMP_TAC std_ss [INTER_SUBSET] THEN 939REPEAT CONJ_EQ_STRIP_TAC THEN 940NTAC 3 WEAKEN_HD_TAC THEN 941 942 943SIMP_TAC std_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN 944REPEAT CONJ_EQ_STRIP_TAC THEN 945NTAC 2 WEAKEN_HD_TAC THEN 946 947SUBGOAL_TAC `(!xp. MEM xp DS.R ==> 948 XP_USED_VARS (xp sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) UNION DS.IV) /\ 949 (!p. MEM p DS.FC ==> 950 P_USED_VARS (p sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) UNION DS.IV)` THEN1 ( 951 952 UNDISCH_NO_TAC 1 THEN 953 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, UNION_SUBSET] THEN 954 SIMP_TAC std_ss [SUBSET_DEF, IN_LIST_BIGUNION, MEM_MAP, GSYM LEFT_FORALL_IMP_THM, IN_UNION, 955 prove (``!B1 B2 B3. (B1 /\ B2) ==> B3 = (B1 ==> B2 ==> B3)``, METIS_TAC[])] THEN 956 METIS_TAC[] 957) THEN 958 959REMAINS_TAC `!n. (w n INTER (\s. ?n. n < DS.SN /\ (s = sv n)) UNION 960 (i n DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 961 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) = 962 963 (w n UNION (i n DIFF (\s. ?n. n < n' + DS.SN /\ (s = sv n)))) INTER 964 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)` THEN1 ( 965 966 SIMP_TAC std_ss [ACCEPT_COND_GF_def, A_SEM_def, 967 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, ACCEPT_F_def] THEN 968 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM, XP_USED_VARS_INTER_SUBSET_BOTH_THM] 969) THEN 970 971 972SIMP_ALL_TAC arith_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF, 973 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, SUBSET_DEF, 974 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 975 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 976 IS_ELEMENT_ITERATOR_def, 977 prove (``!x f. x IN (\x. f x) = f x``, METIS_TAC[IN_DEF])] THEN 978 979`!n. n < DS.SN ==> n < n' + DS.SN` by DECIDE_TAC THEN 980METIS_TAC []); 981 982 983 984 985 986(*Usually it is only extended in special ways. So 987 the following lemmata is helpful*) 988val EXTEND_LTL_TO_GEN_BUECHI_DS___SEM = 989 store_thm 990 ("EXTEND_LTL_TO_GEN_BUECHI_DS___SEM", 991 992 ``!DS DS' n' S0' IV' R' FC' B'. 993 (LTL_TO_GEN_BUECHI_DS___SEM DS /\ 994 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') /\ 995 996 (*The extension does not conflict with old 997 binding runs. Every old binding run can be extended 998 to a new binding run. Obviously new binding runs can 999 be restricted to old ones. So its really 1000 an extension.*) 1001 (!sv w i. (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS' sv /\ 1002 LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv /\ 1003 (!l b1 b2 pf. ((l,b1,b2,pf) IN DS.B ==> 1004 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l,b1,b2,pf) i sv))) ==> 1005 ((?w'. (w = (PATH_RESTRICT w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))) /\ 1006 LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS' i w' sv /\ 1007 (!l b1 b2 pf. (((l,b1,b2,pf) IN B' /\ LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS' i w' sv) ==> 1008 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS' w' (l,b1,b2,pf) i sv))))) /\ 1009 1010 1011 (*The set of state variables is extended 1012 large enough*) 1013 (!n b. (MEM (n, b) S0') ==> (n < n' + DS.SN)) /\ 1014 1015 (*The set of input variables IV is extended 1016 large enough*) 1017 (!sv. 1018 (LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS' sv /\ 1019 (!l' b1' b2' pf'. ((l',b1',b2',pf') IN DS.B ==> 1020 P_USED_VARS (pf' sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) /\ 1021 LTL_USED_VARS l' SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) ==> 1022 1023 ((LIST_BIGUNION (MAP (\xpf. XP_USED_VARS (xpf sv)) R') UNION 1024 LIST_BIGUNION (MAP (\pf. P_USED_VARS (pf sv)) FC') UNION 1025 BIGUNION 1026 (IMAGE (\(l,b1,b2,pf). P_USED_VARS (pf sv) UNION LTL_USED_VARS l) B')) SUBSET 1027 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS' sv UNION IV' UNION DS.IV))))) ==> 1028 1029 LTL_TO_GEN_BUECHI_DS___SEM DS'``, 1030 1031SIMP_TAC std_ss [] THEN 1032REPEAT STRIP_TAC THEN 1033UNDISCH_KEEP_NO_TAC 3 THEN 1034SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___SEM_def] THEN 1035NTAC 3 STRIP_TAC THEN 1036 1037SPECL_NO_ASSUM 1 [``sv:num->'a``] THEN 1038SPECL_NO_ASSUM 3 [``sv:num->'a``] THEN 1039SPECL_NO_ASSUM 5 [``sv:num->'a``] THEN 1040 1041`LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv` by 1042 PROVE_TAC[EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 1043 1044`LIST_BIGUNION (MAP (\xpf. XP_USED_VARS (xpf sv)) R') UNION 1045 LIST_BIGUNION (MAP (\pf. P_USED_VARS (pf sv)) FC') UNION 1046 BIGUNION (IMAGE (\(l,b1,b2,pf). P_USED_VARS (pf sv) UNION LTL_USED_VARS l) B') SUBSET 1047 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') sv UNION IV' UNION DS.IV` by METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS] THEN 1048WEAKEN_NO_TAC 3 THEN 1049GSYM_NO_TAC 6 THEN 1050FULL_SIMP_TAC std_ss [] THEN 1051REPEAT STRIP_TAC THENL [ 1052 UNDISCH_HD_TAC THEN 1053 SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 1054 `!n. n < DS.SN ==> n < n' + DS.SN` by DECIDE_TAC THEN 1055 METIS_TAC[], 1056 1057 1058 1059 UNDISCH_NO_TAC 5 THEN UNDISCH_NO_TAC 1 THEN 1060 REPEAT WEAKEN_HD_TAC THEN 1061 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, 1062 EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, 1063 IN_UNION, IMAGE_UNION, BIGUNION_UNION, 1064 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, LIST_BIGUNION_APPEND] THEN 1065 SUBGOAL_TAC `!x. (?n. n < DS.SN /\ (x = sv n)) ==> (?n. n < n' + DS.SN /\ (x = sv n))` THEN1 ( 1066 REPEAT STRIP_TAC THEN 1067 EXISTS_TAC ``n:num`` THEN 1068 ASM_SIMP_TAC arith_ss [] 1069 ) THEN 1070 METIS_TAC[], 1071 1072 1073 SPECL_NO_ASSUM 4 [``i:num->'a set``] THEN 1074 CLEAN_ASSUMPTIONS_TAC THEN 1075 SPECL_NO_ASSUM 5 [``w:num->'a set``, ``i:num->'a set``] THEN 1076 UNDISCH_HD_TAC THEN 1077 ASM_REWRITE_TAC[] THEN 1078 REPEAT STRIP_TAC THEN 1079 EXISTS_TAC ``w':num->'a set`` THEN 1080 ASM_SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IN_UNION] THEN 1081 REPEAT STRIP_TAC THEN1 PROVE_TAC[] THEN 1082 RES_TAC THEN 1083 UNDISCH_HD_TAC THEN 1084 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, P_SEM_def, 1085 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def] THEN 1086 1087 ASM_SIMP_TAC std_ss [GSYM LEFT_FORALL_IMP_THM] THEN 1088 1089 SUBGOAL_TAC `P_USED_VARS (pf sv) SUBSET 1090 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)` THEN1 ( 1091 METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS] 1092 ) THEN 1093 1094 SUBGOAL_TAC `!w' t. 1095 (LTL_TO_GEN_BUECHI_DS___FAIR_RUN 1096 (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') i w' sv) ==> 1097 1098 ((w' t INTER LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION 1099 (i t DIFF LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) INTER 1100 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) = 1101 1102 (w' t UNION (i t DIFF LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS 1103 (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') sv)) INTER 1104 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))` THEN1 ( 1105 1106 UNDISCH_NO_TAC 13 THEN (*Element Iterator DS'*) 1107 REPEAT WEAKEN_HD_TAC THEN 1108 REPEAT STRIP_TAC THEN 1109 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] THEN 1110 SUBGOAL_TAC `PATH_SUBSET w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS 1111 (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') sv)` THEN1 ( 1112 FULL_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1113 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES] 1114 ) THEN 1115 SUBGOAL_TAC `(LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) SUBSET 1116 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS 1117 (EXTEND_LTL_TO_GEN_BUECHI_DS DS n' S0' IV' R' FC' B') sv)` THEN1 ( 1118 1119 SIMP_TAC arith_ss [SUBSET_DEF, LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 1120 EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES] THEN 1121 REPEAT STRIP_TAC THEN 1122 EXISTS_TAC ``n:num`` THEN 1123 ASM_SIMP_TAC arith_ss [] 1124 ) THEN 1125 1126 SIMP_ALL_TAC arith_ss [PATH_SUBSET_def, SUBSET_DEF, 1127 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 1128 IS_ELEMENT_ITERATOR_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 1129 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, IN_UNION] THEN 1130 `!n. n < DS.SN ==> n < n' + DS.SN` by DECIDE_TAC THEN 1131 METIS_TAC[] 1132 ) THEN 1133 1134 SIMP_TAC std_ss [prove (``(~A ==> ~B) = (B ==> A)``, PROVE_TAC[])] THEN 1135 REPEAT STRIP_TAC THENL [ 1136 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def] THEN 1137 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1138 1139 `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv` by 1140 METIS_TAC[EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN] THEN 1141 FULL_SIMP_TAC std_ss [] THEN 1142 SPECL_NO_ASSUM 5 [``(PATH_RESTRICT (w'':num->'a set) (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (DS:'a ltl_to_gen_buechi_ds) sv))``] THEN 1143 UNDISCH_HD_TAC THEN UNDISCH_NO_TAC 1 THEN 1144 ASM_SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1145 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, symbolic_semi_automaton_REWRITES] THEN 1146 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1147 1148 1149 `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv` by 1150 METIS_TAC[EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN] THEN 1151 FULL_SIMP_TAC std_ss [] THEN 1152 SPECL_NO_ASSUM 4 [``(PATH_RESTRICT (w'':num->'a set) (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (DS:'a ltl_to_gen_buechi_ds) sv))``] THEN 1153 UNDISCH_HD_TAC THEN UNDISCH_NO_TAC 1 THEN 1154 ASM_SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1155 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, symbolic_semi_automaton_REWRITES] THEN 1156 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1157 ] 1158]); 1159 1160 1161 1162(*often we can restrict to just extending the 1163 bindings and the set of input vars, this 1164 simplifies a lot*) 1165val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def = 1166 Define ` 1167 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV= 1168 EXTEND_LTL_TO_GEN_BUECHI_DS DS 0 [] IV [] [] B`; 1169 1170 1171val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON = 1172 prove ( 1173 ``!DS B IV. 1174 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1175 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS``, 1176 1177 SIMP_TAC list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 1178 EXTEND_LTL_TO_GEN_BUECHI_DS_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 1179 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, ltl_to_gen_buechi_ds_REWRITES, 1180 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def]); 1181 1182 1183val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS = 1184 prove ( 1185 ``!DS B IV. 1186 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1187 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS DS``, 1188 1189 SIMP_TAC list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 1190 EXTEND_LTL_TO_GEN_BUECHI_DS_def, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 1191 ltl_to_gen_buechi_ds_REWRITES]); 1192 1193 1194val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___FAIR_RUN = 1195 prove ( 1196 ``!DS B IV. 1197 LTL_TO_GEN_BUECHI_DS___FAIR_RUN (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1198 LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS``, 1199 1200 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, FUN_EQ_THM, 1201 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON, 1202 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS]); 1203 1204 1205val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN = 1206 prove ( 1207 ``!DS B IV. 1208 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1209 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN DS``, 1210 1211 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, FUN_EQ_THM, 1212 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON, 1213 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___FAIR_RUN]); 1214 1215 1216val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN = 1217 prove ( 1218 ``!DS B IV. 1219 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1220 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN DS``, 1221 1222 SIMP_TAC std_ss [FUN_EQ_THM, 1223 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN]); 1224 1225val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS = 1226 prove ( 1227 ``!DS B IV. 1228 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1229 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS``, 1230 1231 SIMP_TAC std_ss [FUN_EQ_THM, EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 1232 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 1233 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def]); 1234 1235 1236val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___BINDING_RUN = 1237 prove ( 1238 ``!DS B IV. 1239 LTL_TO_GEN_BUECHI_DS___BINDING_RUN (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) = 1240 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS``, 1241 1242 SIMP_TAC std_ss [FUN_EQ_THM] THEN 1243 REPEAT GEN_TAC THEN 1244 Cases_on `x'` THEN Cases_on `r` THEN Cases_on `r'` THEN 1245 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, 1246 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS, 1247 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN, 1248 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN]); 1249 1250 1251 1252val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___ELEMENT_FUNCTIONS = 1253 prove ( 1254 ``!DS B IV. 1255 ((EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV).SN = DS.SN) /\ 1256 ((EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV).S0 = DS.S0) /\ 1257 ((EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV).IV = (IV UNION DS.IV)) /\ 1258 ((EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV).R = DS.R) /\ 1259 ((EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV).FC = DS.FC) /\ 1260 ((EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV).B = (B UNION DS.B))``, 1261 1262 SIMP_TAC list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 1263 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES]); 1264 1265 1266 1267val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES = 1268 save_thm ("EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES", 1269 LIST_CONJ [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN, 1270 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN, 1271 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___FAIR_RUN, 1272 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON, 1273 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS, 1274 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS, 1275 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___BINDING_RUN, 1276 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___ELEMENT_FUNCTIONS]); 1277 1278 1279 1280 1281(*Some simple lemmata about how to extend and remove bindings*) 1282val LTL_TO_GEN_BUECHI_DS___PRODUCT_def = 1283 Define 1284 `LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2 = 1285 ltl_to_gen_buechi_ds 1286 (DS1.SN+DS2.SN) 1287 (DS1.S0++(MAP (\(n, b). (n+DS1.SN, b)) DS2.S0)) 1288 (DS1.IV UNION DS2.IV) 1289 (DS1.R++(MAP (\pf sv. (pf (\n. (sv (n+DS1.SN))))) DS2.R)) 1290 (DS1.FC++(MAP (\fc sv. (fc (\n. (sv (n+DS1.SN))))) DS2.FC)) 1291 (DS1.B UNION (IMAGE (\(l, b1, b2, pf). (l, b1, b2, (\sv. pf (\n. (sv (n+DS1.SN)))))) DS2.B))`; 1292 1293 1294val LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def = 1295 Define 1296 `LTL_TO_GEN_BUECHI_DS___SET_BINDINGS DS B = 1297 ltl_to_gen_buechi_ds 1298 DS.SN DS.S0 DS.IV DS.R DS.FC B`; 1299 1300 1301 1302 1303val LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS = 1304 store_thm 1305 ("LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS", 1306 ``!DS DS'. 1307 ((DS.SN = DS'.SN) /\ (DS.S0 = DS'.S0) /\ (DS.IV = DS'.IV) /\ 1308 (DS.R = DS'.R) /\ (DS.FC = DS'.FC) /\ (DS'.B SUBSET DS.B)) ==> 1309 (LTL_TO_GEN_BUECHI_DS___SEM DS ==> LTL_TO_GEN_BUECHI_DS___SEM DS')``, 1310 1311 1312 REPEAT STRIP_TAC THEN 1313 `!sv. LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR DS sv ==> 1314 (!l b1 b2 pf. (l, b1, b2, pf) IN DS.B ==> 1315 ((P_USED_VARS (pf sv) SUBSET 1316 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) /\ 1317 (LTL_USED_VARS l SUBSET 1318 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` by METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS] THEN 1319 1320 UNDISCH_NO_TAC 1 THEN 1321 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def] THEN 1322 DISCH_TAC THEN GEN_TAC THEN 1323 NTAC 2 (SPECL_NO_ASSUM 1 [``sv:num->'a``]) THEN 1324 NTAC 2 UNDISCH_HD_TAC THEN 1325 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 1326 ltl_to_gen_buechi_ds_REWRITES] THEN 1327 REPEAT STRIP_TAC THENL [ 1328 PROVE_TAC[], 1329 1330 UNDISCH_NO_TAC 1 THEN UNDISCH_NO_TAC 1 THEN 1331 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, 1332 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, UNION_SUBSET, 1333 ltl_to_gen_buechi_ds_REWRITES] THEN 1334 REPEAT STRIP_TAC THEN 1335 UNDISCH_NO_TAC 1 THEN 1336 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, 1337 GSYM RIGHT_EXISTS_AND_THM] THEN 1338 METIS_TAC[], 1339 1340 FULL_SIMP_TAC std_ss [] THEN 1341 SPECL_NO_ASSUM 1 [``i:num->'a set``] THEN 1342 CLEAN_ASSUMPTIONS_TAC THEN 1343 EXISTS_TAC ``w:num->'a set`` THEN 1344 REPEAT STRIP_TAC THENL [ 1345 UNDISCH_HD_TAC THEN 1346 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 1347 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1348 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1349 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 1350 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 1351 ltl_to_gen_buechi_ds_REWRITES], 1352 1353 `LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l,b1,b2,pf) i sv` by PROVE_TAC[SUBSET_DEF] THEN 1354 UNDISCH_HD_TAC THEN 1355 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1356 LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 1357 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1358 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1359 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 1360 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 1361 ltl_to_gen_buechi_ds_REWRITES] THEN 1362 ASM_SIMP_TAC std_ss [] THEN 1363 METIS_TAC[] 1364 ] 1365 ]); 1366 1367 1368 1369 1370val LTL_TO_GEN_BUECHI_DS___SEM___SET_BINDINGS = 1371 store_thm 1372 ("LTL_TO_GEN_BUECHI_DS___SEM___SET_BINDINGS", 1373 ``!DS B. 1374 ((B SUBSET DS.B) /\ (LTL_TO_GEN_BUECHI_DS___SEM DS) ==> 1375 LTL_TO_GEN_BUECHI_DS___SEM (LTL_TO_GEN_BUECHI_DS___SET_BINDINGS DS B))``, 1376 1377 REPEAT STRIP_TAC THEN 1378 UNDISCH_HD_TAC THEN 1379 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 1380 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SET_BINDINGS_def, 1381 ltl_to_gen_buechi_ds_REWRITES]); 1382 1383 1384 1385val LTL_TO_GEN_BUECHI_DS___SEM___EQ = 1386 store_thm 1387 ("LTL_TO_GEN_BUECHI_DS___SEM___EQ", 1388 ``!DS DS'. 1389 ((DS.SN = DS'.SN) /\ (DS.S0 = DS'.S0) /\ (DS.IV = DS'.IV) /\ 1390 (EVERY (\r. (?r'. (MEM r' DS'.R) /\ !sv. 1391 XPROP_LOGIC_EQUIVALENT (r sv) (r' sv))) DS.R) /\ 1392 (EVERY (\r'. (?r. (MEM r DS.R) /\ !sv. 1393 XPROP_LOGIC_EQUIVALENT (r sv) (r' sv))) DS'.R) /\ 1394 1395 (EVERY (\fc. (?fc'. (MEM fc' DS'.FC) /\ !sv. 1396 PROP_LOGIC_EQUIVALENT (fc sv) (fc' sv))) DS.FC) /\ 1397 (EVERY (\fc'. (?fc. (MEM fc DS.FC) /\ !sv. 1398 PROP_LOGIC_EQUIVALENT (fc sv) (fc' sv))) DS'.FC) /\ 1399 1400 (!l b1 b2 pf. ((l, b1, b2, pf) IN DS.B) ==> (?l' pf' b1' b2'. (b1 ==> b1') /\ (b2 ==> b2') /\ ((l', b1', b2', pf') IN DS'.B) /\ 1401 LTL_EQUIVALENT l l' /\ !sv. 1402 PROP_LOGIC_EQUIVALENT (pf sv) (pf' sv))) /\ 1403 (!l b1 b2 pf. ((l, b1, b2, pf) IN DS'.B) ==> (?l' pf' b1' b2'. (b1 ==> b1') /\ (b2 ==> b2') /\ ((l', b1', b2', pf') IN DS.B) /\ 1404 LTL_EQUIVALENT l l' /\ !sv. 1405 PROP_LOGIC_EQUIVALENT (pf sv) (pf' sv))) /\ 1406 (!sv. (LTL_TO_GEN_BUECHI_DS___USED_VARS DS sv = LTL_TO_GEN_BUECHI_DS___USED_VARS DS' sv))) ==> 1407 (LTL_TO_GEN_BUECHI_DS___SEM DS = LTL_TO_GEN_BUECHI_DS___SEM DS')``, 1408 1409 1410 Cases_on `DS` THEN Cases_on `DS'` THEN 1411 SIMP_TAC std_ss [ltl_to_gen_buechi_ds_REWRITES] THEN 1412 STRIP_TAC THEN 1413 NTAC 7 UNDISCH_HD_TAC (*everything except eq*) THEN 1414 ASM_SIMP_TAC std_ss [] THEN 1415 REPEAT WEAKEN_HD_TAC THEN 1416 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def, 1417 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 1418 ltl_to_gen_buechi_ds_REWRITES, 1419 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1420 EVERY_MEM, 1421 XPROP_LOGIC_EQUIVALENT_def, 1422 PROP_LOGIC_EQUIVALENT_def, 1423 LTL_EQUIVALENT_def] THEN 1424 REPEAT STRIP_TAC THEN 1425 ONCE_REWRITE_TAC [IMP_DISJ_THM] THEN 1426 FORALL_EQ_STRIP_TAC THEN 1427 REPEAT BOOL_EQ_STRIP_TAC THEN 1428 FORALL_EQ_STRIP_TAC THEN 1429 EXISTS_EQ_STRIP_TAC THEN 1430 MATCH_MP_TAC (prove (``!A A' B B' w i sv. ((!i w sv. (A i w sv = A' i w sv)) /\ (B = B')) ==> (((A i w sv) /\ B) = ((A' i w sv) /\ B'))``, 1431 METIS_TAC[])) THEN 1432 LEFT_CONJ_TAC THENL [ 1433 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 1434 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1435 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1436 ltl_to_gen_buechi_ds_REWRITES, 1437 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1438 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 1439 symbolic_semi_automaton_REWRITES, 1440 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 1441 IS_TRANSITION_def, INPUT_RUN_PATH_UNION_def, 1442 INPUT_RUN_STATE_UNION_def, XP_BIGAND_SEM, 1443 A_BIGAND_SEM, 1444 MEM_MAP, GSYM LEFT_FORALL_IMP_THM] THEN 1445 REPEAT STRIP_TAC THEN 1446 REPEAT BOOL_EQ_STRIP_TAC THEN 1447 BINOP_TAC THENL [ 1448 METIS_TAC[], 1449 1450 SIMP_TAC std_ss [ACCEPT_COND_GF_def, A_SEM_THM, 1451 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, 1452 ACCEPT_F_def] THEN 1453 METIS_TAC[] 1454 ], 1455 1456 1457 1458 1459 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1460 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, 1461 INPUT_RUN_STATE_UNION_def, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1462 ltl_to_gen_buechi_ds_REWRITES, symbolic_semi_automaton_REWRITES 1463 ] THEN 1464 EQ_TAC THEN ( 1465 REPEAT STRIP_TAC THEN 1466 RES_TAC THEN 1467 RES_TAC THEN 1468 METIS_TAC[] 1469 ) 1470 ]); 1471 1472 1473 1474val LTL_TO_GEN_BUECHI_DS___SEM___EXTEND_EQUIV_BINDING = 1475 store_thm 1476 ("LTL_TO_GEN_BUECHI_DS___SEM___EXTEND_EQUIV_BINDING", 1477 ``!DS l l' b1 b2 b1' b2' pf pf'. 1478 ((l, b1, b2, pf) IN DS.B /\ 1479 LTL_EQUIVALENT l l' /\ (LTL_USED_VARS l' SUBSET LTL_USED_VARS l) /\ !sv. (PROP_LOGIC_EQUIVALENT (pf sv) (pf' sv) /\ (P_USED_VARS (pf' sv) SUBSET P_USED_VARS (pf sv))) /\ (b1' ==> b1) /\ (b2' ==> b2)) ==> 1480 1481 (LTL_TO_GEN_BUECHI_DS___SEM DS = LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(l', b1', b2', pf')} {}))``, 1482 1483 REPEAT STRIP_TAC THEN 1484 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___EQ THEN 1485 SIMP_ALL_TAC std_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES, 1486 UNION_EMPTY, IN_SING, IN_UNION, LTL_EQUIVALENT_def, 1487 XPROP_LOGIC_EQUIVALENT_def, PROP_LOGIC_EQUIVALENT_def, 1488 EVERY_MEM] THEN 1489 REPEAT STRIP_TAC THENL [ 1490 PROVE_TAC[], 1491 PROVE_TAC[], 1492 PROVE_TAC[], 1493 PROVE_TAC[], 1494 METIS_TAC[], 1495 1496 Q_TAC EXISTS_TAC `l` THEN 1497 Q_TAC EXISTS_TAC `pf` THEN 1498 Q_TAC EXISTS_TAC `b1` THEN 1499 Q_TAC EXISTS_TAC `b2` THEN 1500 ASM_SIMP_TAC std_ss [], 1501 1502 METIS_TAC[], 1503 1504 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, 1505 EXTENSION, IN_UNION, 1506 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 1507 REPEAT STRIP_TAC THEN 1508 REPEAT BOOL_EQ_STRIP_TAC THEN 1509 SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, 1510 GSYM RIGHT_EXISTS_AND_THM, IN_UNION, IN_SING] THEN 1511 EQ_TAC THEN STRIP_TAC THENL [ 1512 METIS_TAC[], 1513 1514 Q_TAC EXISTS_TAC `(l, b1, b2, pf)` THEN 1515 FULL_SIMP_TAC std_ss [IN_UNION, SUBSET_DEF], 1516 1517 METIS_TAC[] 1518 ] 1519 ]); 1520 1521 1522val LTL_TO_GEN_BUECHI_DS___SEM___WEAKEN_BINDING = 1523 store_thm 1524 ("LTL_TO_GEN_BUECHI_DS___SEM___WEAKEN_BINDING", 1525 ``!DS l b1 b2 b1' b2' pf IV. 1526 (LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(l, b1, b2, pf)} IV) /\ 1527 (b1' ==> b1) /\ (b2' ==> b2)) ==> 1528 1529 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(l, b1', b2', pf)} IV)``, 1530 1531REPEAT STRIP_TAC THEN 1532ASSUME_TAC LTL_TO_GEN_BUECHI_DS___SEM___EXTEND_EQUIV_BINDING THEN 1533Q_SPECL_NO_ASSUM 0 [`EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(l,b1,b2,pf)} IV`, `l`, `l`, `b1`, `b2`, `b1'`, `b2'`, `pf`, `pf`] THEN 1534PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1535 ASM_SIMP_TAC std_ss [LTL_EQUIVALENT_def, SUBSET_REFL, PROP_LOGIC_EQUIVALENT_def, 1536 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES, IN_UNION, IN_SING] 1537) THEN 1538FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 1539UNDISCH_NO_TAC 2 THEN 1540MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 1541 1542SIMP_TAC std_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_SING, 1543 SUBSET_DEF, IN_INSERT, UNION_EMPTY] THEN 1544METIS_TAC[]); 1545 1546 1547 1548val EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM = 1549 store_thm 1550 ("EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM", 1551 1552 ``!DS B IV. 1553 (LTL_TO_GEN_BUECHI_DS___SEM DS /\ 1554 (!sv l b1 b2 pf. 1555 ((l, b1, b2, pf) IN B /\ 1556 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) sv /\ 1557 (!l' b1' b2' pf'. ((l',b1',b2',pf') IN DS.B ==> 1558 P_USED_VARS (pf' sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) /\ 1559 LTL_USED_VARS l' SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))) ==> 1560 1561 P_USED_VARS (pf sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION IV UNION DS.IV) /\ 1562 LTL_USED_VARS l SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION IV UNION DS.IV)) /\ 1563 1564 (!sv l b1 b2 pf w i. 1565 ((l, b1, b2, pf) IN B /\ LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv /\ 1566 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV) sv /\ 1567 (!l' b1' b2' pf'. ((l',b1',b2',pf') IN DS.B ==> 1568 P_USED_VARS (pf' sv) SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) /\ 1569 LTL_USED_VARS l' SUBSET (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV) /\ 1570 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l',b1',b2',pf') i sv))) ==> 1571 1572 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l,b1,b2,pf) i sv)) ==> 1573 1574 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS B IV)``, 1575 1576REWRITE_TAC[EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def] THEN 1577REPEAT STRIP_TAC THEN 1578MATCH_MP_TAC (SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___SEM) THEN 1579ASM_SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_EMPTY] THEN 1580REPEAT STRIP_TAC THENL [ 1581 EXISTS_TAC ``w:num->'a set`` THEN 1582 ASM_REWRITE_TAC[GSYM EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 1583 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 1584 REPEAT STRIP_TAC THENL [ 1585 METIS_TAC[PATH_RESTRICT_PATH_SUBSET, LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET], 1586 1587 METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] 1588 ], 1589 1590 1591 REMAINS_TAC `!l b1 b2 pf. (l, b1, b2, pf) IN B ==> 1592 P_USED_VARS (pf sv) UNION LTL_USED_VARS l SUBSET 1593 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION IV UNION DS.IV` THEN1 ( 1594 UNDISCH_HD_TAC THEN 1595 REPEAT WEAKEN_HD_TAC THEN 1596 SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, IN_IMAGE, 1597 GSYM RIGHT_EXISTS_AND_THM] THEN 1598 REPEAT STRIP_TAC THEN 1599 Cases_on `x'` THEN Cases_on `r` THEN Cases_on `r'` THEN 1600 FULL_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 1601 EXTEND_LTL_TO_GEN_BUECHI_DS_def, IN_UNION, 1602 ltl_to_gen_buechi_ds_REWRITES] THEN 1603 METIS_TAC[IN_UNION] 1604 ) THEN 1605 1606 REPEAT STRIP_TAC THEN 1607 RES_TAC THEN 1608 ASM_REWRITE_TAC[UNION_SUBSET] 1609]); 1610 1611 1612(*Combining two complete datastructures*) 1613val LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM = 1614 store_thm 1615 ("LTL_TO_GEN_BUECHI_DS___PRODUCT___SEM___THM", 1616 1617 ``!DS1 DS2. LTL_TO_GEN_BUECHI_DS___SEM DS1 ==> 1618 LTL_TO_GEN_BUECHI_DS___SEM DS2 ==> 1619 (LTL_TO_GEN_BUECHI_DS___SEM (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2))``, 1620 1621SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEM_def, LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1622 ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def] THEN 1623REPEAT GEN_TAC THEN NTAC 4 STRIP_TAC THEN 1624SUBGOAL_TAC `IS_ELEMENT_ITERATOR sv DS1.SN DS1.IV /\ 1625 IS_ELEMENT_ITERATOR (\n. sv (n + DS1.SN)) DS2.SN DS2.IV` THEN1 ( 1626 UNDISCH_HD_TAC THEN 1627 REPEAT WEAKEN_HD_TAC THEN 1628 SIMP_TAC arith_ss [IS_ELEMENT_ITERATOR_def, IN_UNION] 1629) THEN 1630Q_SPEC_NO_ASSUM 4 `sv` THEN 1631Q_SPEC_NO_ASSUM 4 `(\n. sv (n + DS1.SN))` THEN 1632NTAC 2 UNDISCH_HD_TAC THEN 1633ASM_SIMP_TAC list_ss [MEM_MAP] THEN 1634NTAC 2 WEAKEN_HD_TAC THEN 1635REPEAT STRIP_TAC THEN1 ( 1636 `n < DS1.SN` by PROVE_TAC[] THEN 1637 DECIDE_TAC 1638) THEN1 ( 1639 Cases_on `y` THEN 1640 SIMP_ALL_TAC std_ss [] THEN 1641 `q < DS2.SN` by PROVE_TAC[] THEN 1642 ASM_SIMP_TAC arith_ss [] 1643) THEN1 ( 1644 UNDISCH_NO_TAC 1 THEN 1645 UNDISCH_NO_TAC 3 THEN 1646 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, 1647 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1648 ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, 1649 IN_UNION, IN_LIST_BIGUNION, IMAGE_UNION, 1650 BIGUNION_UNION, MEM_MAP, IN_BIGUNION, 1651 IN_IMAGE, 1652 GSYM RIGHT_EXISTS_AND_THM, 1653 IN_ABS, 1654 pairTheory.EXISTS_PROD] THEN 1655 `!n. n < DS1.SN ==> n < DS1.SN + DS2.SN` by DECIDE_TAC THEN 1656 `!n. n < DS2.SN ==> n + DS1.SN < DS1.SN + DS2.SN` by DECIDE_TAC THEN 1657 METIS_TAC[] 1658) THEN1 ( 1659 REWRITE_TAC [GSYM LTL_TO_GEN_BUECHI_DS___PRODUCT_def] THEN 1660 `!n. n < DS1.SN ==> n < DS1.SN + DS2.SN` by DECIDE_TAC THEN 1661 `!n. n < DS2.SN ==> n + DS1.SN < DS1.SN + DS2.SN` by DECIDE_TAC THEN 1662 `!n. ~((n + DS1.SN) < DS1.SN)` by DECIDE_TAC THEN 1663 1664 `(?S1. (COMPL (\x. ?n. n < DS2.SN /\ (x = sv (n + DS1.SN)))) = S1) /\ 1665 (?S2. (COMPL (\x. ?n. n < DS1.SN /\ (x = sv n))) = S2)` 1666 by SIMP_TAC std_ss [] THEN 1667 SUBGOAL_TAC `(!fc. MEM fc DS1.FC ==> P_USED_VARS (fc sv) SUBSET S1) /\ 1668 (!fc. MEM fc DS2.FC ==> P_USED_VARS (fc (\n. sv (n + DS1.SN))) SUBSET S2) /\ 1669 (!xp. MEM xp DS1.R ==> XP_USED_VARS (xp sv) SUBSET S1) /\ 1670 (!xp. MEM xp DS2.R ==> XP_USED_VARS (xp (\n. sv (n + DS1.SN))) SUBSET S2) /\ 1671 (!l b1 b2 pf. (l, b1, b2, pf) IN DS1.B ==> P_USED_VARS (pf sv) SUBSET S1) /\ 1672 (!l b1 b2 pf. (l, b1, b2, pf) IN DS2.B ==> P_USED_VARS (pf (\n. sv (n + DS1.SN))) SUBSET S2)` THEN1 ( 1673 UNDISCH_NO_TAC 9 (*USED VARS DS1*) THEN 1674 UNDISCH_NO_TAC 6 (*USED VARS DS2*) THEN 1675 GSYM_NO_TAC 1 THEN 1676 GSYM_NO_TAC 1 THEN 1677 UNDISCH_NO_TAC 9 THEN (*ELEMENT_ITERATOR*) 1678 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___USED_VARS_def, 1679 SUBSET_DEF, IN_COMPL, 1680 IN_ABS, IN_UNION, IN_LIST_BIGUNION, MEM_MAP, 1681 GSYM LEFT_EXISTS_AND_THM, DISJ_IMP_THM, FORALL_AND_THM, 1682 GSYM LEFT_FORALL_IMP_THM, GSYM RIGHT_EXISTS_AND_THM, 1683 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1684 IS_ELEMENT_ITERATOR_def, 1685 IN_BIGUNION, IN_IMAGE, 1686 prove (``!P. (!x. P x) = (!x1 x2 x3 x4. P (x1,x2,x3,x4))``, METIS_TAC[PAIR])] THEN 1687 METIS_TAC[] 1688 ) THEN 1689 1690 SUBGOAL_TAC `(?P. !w w' n. (w n UNION w' n UNION 1691 (i n DIFF (\s. ?n. n < DS1.SN + DS2.SN /\ (s = sv n)))) = P w w' n) /\ 1692 (?P1. !w n. (w n UNION (i n DIFF (\s. ?n. n < DS1.SN /\ (s = sv n)))) = P1 w n) /\ 1693 (?P2. !w' n. (w' n UNION (i n DIFF (\s. ?n. n < DS2.SN /\ (s = sv (n+ DS1.SN))))) = P2 w' n) /\ 1694 (?P3. !w n. (w n UNION 1695 (i n DIFF (\s. ?n. n < DS1.SN + DS2.SN /\ (s = sv n)))) = P3 w n)` THEN1 ( 1696 SIMP_TAC std_ss [GSYM FUN_EQ_THM, 1697 prove (``(\x y. f x y) = f``, METIS_TAC[]), 1698 prove (``(\x y z. f x y z) = f``, METIS_TAC[])] 1699 ) THEN 1700 SUBGOAL_TAC `(!w w'. (PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv) /\ 1701 PATH_SUBSET w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 (\n. sv (n + DS1.SN)))) ==> 1702 ((!n. ((P w w' n) INTER S1) = (P1 w n) INTER S1) /\ 1703 (!n. ((P w w' n) INTER S2) = (P2 w' n) INTER S2))) /\ 1704 1705 (!w. (PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) sv)) ==> 1706 ((!n. ((P3 w n) INTER S1) = ((P1 (PATH_RESTRICT w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv)) n) INTER S1)) /\ 1707 (!n. ((P3 w n) INTER S2) = ((P2 (PATH_RESTRICT w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 (\n. sv (n + DS1.SN)))) n) INTER S2))))` THEN1 ( 1708 NTAC 2 (GSYM_NO_TAC 11) THEN 1709 NTAC 4 (GSYM_NO_TAC 5) THEN 1710 UNDISCH_NO_TAC 21 (*Element iterator*) THEN 1711 ASM_SIMP_TAC arith_ss [EXTENSION, IN_UNION, IN_INTER, IN_COMPL, 1712 IN_DIFF, IN_ABS, IS_ELEMENT_ITERATOR_def, 1713 PATH_SUBSET_def, LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1714 ltl_to_gen_buechi_ds_REWRITES, PATH_RESTRICT_def, 1715 PATH_MAP_def, 1716 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, SUBSET_DEF] THEN 1717 NTAC 12 WEAKEN_HD_TAC THEN 1718 NTAC 3 UNDISCH_HD_TAC THEN 1719 REPEAT WEAKEN_HD_TAC THEN 1720 REPEAT DISCH_TAC THEN 1721 SUBGOAL_TAC `!x. ((!n. ~(n < DS1.SN) \/ ~(x = sv n)) ==> 1722 ((!n. ~(n < DS1.SN + DS2.SN) \/ ~(x = sv n)) = 1723 (!n. ~(n < DS2.SN) \/ ~(x = sv (n + DS1.SN))))) /\ 1724 ((!n. ~(n < DS2.SN) \/ ~(x = sv (n+DS1.SN))) ==> 1725 ((!n. ~(n < DS1.SN + DS2.SN) \/ ~(x = sv n)) = 1726 (!n. ~(n < DS1.SN) \/ ~(x = sv n))))` THEN1 ( 1727 REPEAT STRIP_TAC THEN 1728 (EQ_TAC THENL [ 1729 METIS_TAC[], 1730 1731 REPEAT STRIP_TAC THEN 1732 RIGHT_DISJ_TAC THEN 1733 Cases_on `n < DS1.SN` THENL [ 1734 METIS_TAC[], 1735 1736 `(n - DS1.SN < DS2.SN) /\ 1737 (((n - DS1.SN) + DS1.SN) = n)` by DECIDE_TAC THEN 1738 METIS_TAC[] 1739 ] 1740 ]) 1741 ) THEN 1742 METIS_TAC[] 1743 ) THEN 1744 1745 SUBGOAL_TAC `!w w'. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS1 i w sv /\ 1746 LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS2 i w' 1747 (\n. sv (n + DS1.SN)) = 1748 (PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv) /\ 1749 PATH_SUBSET w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 (\n. sv (n + DS1.SN))) /\ 1750 LTL_TO_GEN_BUECHI_DS___FAIR_RUN (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) i (\n. (w n UNION w' n)) sv)` THEN1 ( 1751 REPEAT GEN_TAC THEN 1752 Q_SPECL_NO_ASSUM 1 [`w`, `w'`] THEN 1753 UNDISCH_HD_TAC THEN 1754 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 1755 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 1756 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1757 IS_TRANSITION_def, 1758 INPUT_RUN_STATE_UNION_def, 1759 INPUT_RUN_PATH_UNION_def, 1760 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 1761 LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1762 symbolic_semi_automaton_REWRITES, 1763 ltl_to_gen_buechi_ds_REWRITES, 1764 A_BIGAND___A_SEM, 1765 MAP_MAP_o, 1766 combinTheory.o_DEF, 1767 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1768 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 1769 P_BIGAND_SEM, 1770 XP_BIGAND_SEM, 1771 A_BIGAND_SEM, MEM_MAP, 1772 GSYM LEFT_FORALL_IMP_THM, 1773 ACCEPT_COND_GF_def, 1774 ACCEPT_F_def, 1775 A_SEM_def, ACCEPT_COND_SEM_def, 1776 ACCEPT_COND_SEM_TIME_def, 1777 PATH_SUBSET_def, SUBSET_DEF, IN_UNION, 1778 IN_ABS 1779 ] THEN 1780 STRIP_TAC THEN 1781 REPEAT BOOL_EQ_STRIP_TAC THEN 1782 UNDISCH_NO_TAC 2 THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN 1783 MATCH_MP_TAC (prove (``((X30 /\ ((X11 /\ X21) = X31)) /\ 1784 (((X12 /\ X22) = X32) /\ ((X13 /\ X23) = X33))) ==> 1785 ((((X11 /\ X12) /\ X13) /\ ((X21 /\ X22) /\ X23)) = 1786 ((X30 /\ (X31 /\ X32)) /\ X33))``, METIS_TAC[])) THEN 1787 STRIP_TAC THENL [ 1788 REPEAT STRIP_TAC THENL [ 1789 METIS_TAC[], 1790 METIS_TAC[], 1791 1792 SIMP_TAC std_ss [ 1793 prove (``!P. (!y. P y) = (!y1 y2. P (y1, y2))``, METIS_TAC[PAIR]), 1794 prove (``!P. (?y. P y) = (?y1 y2. P (y1, y2))``, METIS_TAC[PAIR]), 1795 DISJ_IMP_THM, FORALL_AND_THM, 1796 GSYM LEFT_FORALL_IMP_THM 1797 ] THEN 1798 UNDISCH_NO_TAC 26 (*Element Iterator*) THEN 1799 NTAC 4 (GSYM_NO_TAC 8) THEN (*P1, P2, P*) 1800 ASM_SIMP_TAC std_ss [ 1801 P_SEM_THM, IN_UNION, 1802 IN_DIFF, IN_ABS, 1803 COND_RAND, 1804 IS_ELEMENT_ITERATOR_def 1805 ] THEN 1806 NTAC 2 (UNDISCH_NO_TAC 6) THEN (*PATH_SUBSET w w'*) 1807 NTAC 3 (UNDISCH_NO_TAC 15) THEN (*< helpers*) 1808 UNDISCH_NO_TAC 20 THEN (*DS1.S0*) 1809 UNDISCH_NO_TAC 17 THEN (*DS1.S0*) 1810 REPEAT WEAKEN_HD_TAC THEN 1811 REPEAT STRIP_TAC THEN 1812 1813 SIMP_TAC std_ss [GSYM FORALL_AND_THM, IMP_DISJ_THM] THEN 1814 NTAC 2 FORALL_EQ_STRIP_TAC THEN 1815 Cases_on `y2` THEN SIMP_TAC std_ss [] THEN 1816 BINOP_TAC THEN 1817 REPEAT BOOL_EQ_STRIP_TAC THEN 1818 METIS_TAC[] 1819 ], 1820 1821 SIMP_TAC std_ss [DISJ_IMP_THM, FORALL_AND_THM, 1822 GSYM LEFT_FORALL_IMP_THM] THEN 1823 NTAC 2 UNDISCH_HD_TAC (*P_INTER*) THEN 1824 NTAC 4 (UNDISCH_NO_TAC 9) (*DS1.R DS.R DS.FC*) THEN 1825 REPEAT WEAKEN_HD_TAC THEN 1826 REPEAT DISCH_TAC THEN 1827 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM, 1828 P_USED_VARS_INTER_SUBSET_THM] 1829 ] 1830 ) THEN 1831 1832 1833 Q_SPEC_NO_ASSUM 18 `i` THEN 1834 Q_SPEC_NO_ASSUM 21 `i` THEN 1835 CLEAN_ASSUMPTIONS_TAC THEN 1836 Q_TAC EXISTS_TAC `(\n. w n UNION w' n)` THEN 1837 STRIP_TAC THEN1 METIS_TAC[] THEN 1838 REPEAT GEN_TAC THEN 1839 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1840 IMP_CONJ_THM, GSYM IN_UNION] THEN 1841 `PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv) /\ 1842 PATH_SUBSET w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 (\n. sv (n + DS1.SN)))` by METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 1843 Q_SPECL_NO_ASSUM 8 [`w`, `w'`] THEN 1844 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 1845 STRIP_TAC THENL [ 1846 SIMP_TAC std_ss [IN_UNION, IN_IMAGE, 1847 prove (``(?x. P x) = (?l b1 b2 pf. P (l,b1,b2,pf))``, METIS_TAC[PAIR])] THEN 1848 REPEAT STRIP_TAC THENL [ 1849 Q_SPECL_NO_ASSUM 6 [`l`, `b1`, `b2`, `pf`] THEN 1850 UNDISCH_HD_TAC THEN 1851 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1852 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1853 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1854 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1855 LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1856 ltl_to_gen_buechi_ds_REWRITES, 1857 symbolic_semi_automaton_REWRITES] THEN 1858 STRIP_TAC THEN NTAC 2 WEAKEN_HD_TAC THEN 1859 `P_USED_VARS (pf sv) SUBSET S1` by METIS_TAC[] THEN 1860 NTAC 4 UNDISCH_HD_TAC THEN 1861 REPEAT WEAKEN_HD_TAC THEN 1862 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1863 1864 1865 Q_SPECL_NO_ASSUM 9 [`l`, `b1`, `b2`, `pf'`] THEN 1866 UNDISCH_HD_TAC THEN 1867 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1868 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1869 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1870 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1871 LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1872 ltl_to_gen_buechi_ds_REWRITES, 1873 symbolic_semi_automaton_REWRITES] THEN 1874 STRIP_TAC THEN NTAC 2 WEAKEN_HD_TAC THEN 1875 `P_USED_VARS (pf' (\n. sv (n + DS1.SN))) SUBSET S2` by METIS_TAC[] THEN 1876 NTAC 5 UNDISCH_HD_TAC THEN 1877 REPEAT WEAKEN_HD_TAC THEN 1878 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1879 ], 1880 1881 1882 SIMP_TAC std_ss [prove (``((X ==> Y1) /\ (X ==> Y2)) = (X ==> (Y1 /\ Y2))``, METIS_TAC[]), GSYM FORALL_AND_THM] THEN 1883 NTAC 4 STRIP_TAC THEN 1884 `?v1. v1 = PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv)` by METIS_TAC[] THEN 1885 `?v2. v2 = PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 1886 (\n. sv (n + DS1.SN)))` by METIS_TAC[] THEN 1887 SUBGOAL_TAC `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS1 i v1 sv /\ 1888 LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS2 i v2 (\n. sv (n + DS1.SN))` THEN1 ( 1889 Q_SPECL_NO_ASSUM 12 [`v1`, `v2`] THEN 1890 UNDISCH_HD_TAC THEN 1891 ASM_SIMP_TAC std_ss [PATH_SUBSET_def, SIMP_RULE std_ss [] PATH_RESTRICT_SUBSET] THEN 1892 REMAINS_TAC `(\n. 1893 PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv) 1894 n UNION 1895 PATH_RESTRICT w'' 1896 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 1897 (\n. sv (n + DS1.SN))) n) = w''` THEN1 ( 1898 ASM_REWRITE_TAC[] 1899 ) THEN 1900 `PATH_SUBSET w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) sv)` by 1901 METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 1902 UNDISCH_HD_TAC THEN 1903 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN 1904 SIMP_TAC std_ss [EXTENSION, PATH_RESTRICT_def, PATH_MAP_def, 1905 PATH_SUBSET_def, IN_UNION, IN_INTER, 1906 LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1907 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1908 ltl_to_gen_buechi_ds_REWRITES, SUBSET_DEF, 1909 IN_ABS] THEN 1910 REPEAT WEAKEN_HD_TAC THEN 1911 REPEAT STRIP_TAC THEN 1912 Cases_on `x' IN w'' x` THEN ASM_REWRITE_TAC[] THEN 1913 RES_TAC THEN 1914 Cases_on `n' < DS1.SN` THENL [ 1915 PROVE_TAC[], 1916 1917 DISJ2_TAC THEN 1918 EXISTS_TAC ``n' - DS1.SN`` THEN 1919 ASM_SIMP_TAC arith_ss [] 1920 ] 1921 ) THEN 1922 1923 `PATH_SUBSET w'' 1924 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS 1925 (LTL_TO_GEN_BUECHI_DS___PRODUCT DS1 DS2) sv) /\ 1926 PATH_SUBSET v1 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS1 sv) /\ 1927 PATH_SUBSET v2 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS2 (\n. sv (n + DS1.SN)))` by METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 1928 UNDISCH_NO_TAC 8 THEN (*l, b1, b2, pf IN DS.B*) 1929 SIMP_TAC std_ss [IN_UNION, IN_IMAGE, 1930 prove (``(?x. P x) = (?l b1 b2 pf. P (l,b1,b2,pf))``, METIS_TAC[PAIR])] THEN 1931 STRIP_TAC THENL [ 1932 Q_SPECL_NO_ASSUM 14 [`l`, `b1`, `b2`, `pf`] THEN 1933 UNDISCH_HD_TAC THEN 1934 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1935 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1936 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1937 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1938 LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1939 ltl_to_gen_buechi_ds_REWRITES, 1940 IN_UNION, 1941 symbolic_semi_automaton_REWRITES] THEN 1942 STRIP_TAC THEN 1943 Q_SPEC_NO_ASSUM 0 `v1` THEN 1944 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN 1945 `P_USED_VARS (pf sv) SUBSET S1` by METIS_TAC[] THEN 1946 UNDISCH_HD_TAC THEN 1947 Q_SPEC_NO_ASSUM 18 `w''` THEN 1948 UNDISCH_HD_TAC THEN 1949 ASM_REWRITE_TAC[] THEN 1950 UNDISCH_NO_TAC 11 (*INTER S1*) THEN 1951 REPEAT WEAKEN_HD_TAC THEN 1952 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 1953 1954 1955 Q_SPECL_NO_ASSUM 17 [`l`, `b1`, `b2`, `pf'`] THEN 1956 UNDISCH_HD_TAC THEN 1957 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 1958 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 1959 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 1960 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 1961 LTL_TO_GEN_BUECHI_DS___PRODUCT_def, 1962 ltl_to_gen_buechi_ds_REWRITES, 1963 symbolic_semi_automaton_REWRITES] THEN 1964 STRIP_TAC THEN 1965 Q_SPEC_NO_ASSUM 0 `v2` THEN 1966 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN 1967 `P_USED_VARS (pf' (\n. sv (n + DS1.SN))) SUBSET S2` by METIS_TAC[] THEN 1968 UNDISCH_HD_TAC THEN 1969 Q_SPEC_NO_ASSUM 19 `w''` THEN 1970 UNDISCH_HD_TAC THEN 1971 ASM_REWRITE_TAC[] THEN 1972 UNDISCH_NO_TAC 11 (*INTER S2*) THEN 1973 REPEAT WEAKEN_HD_TAC THEN 1974 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 1975 ] 1976 ] 1977)); 1978 1979 1980 1981 1982 1983 1984 1985 1986(* Now we have the necessary basics to start 1987 proving the translation *) 1988 1989val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP = 1990 store_thm 1991 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP", 1992 1993 ``!DS p. 1994 LTL_TO_GEN_BUECHI_DS___SEM DS ==> 1995 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(LTL_PROP p, T, T, \sv. p)} (P_USED_VARS p))``, 1996 1997 REPEAT STRIP_TAC THEN 1998 MATCH_MP_TAC EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM THEN 1999 ASM_SIMP_TAC list_ss [LTL_USED_VARS_def, SUBSET_DEF, IN_UNION, IN_SING] THEN 2000 REPEAT STRIP_TAC THEN 2001 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, LTL_SEM_TIME_def, LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 2002 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 2003 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, P_SEM_def] THEN 2004 2005 UNDISCH_NO_TAC 1 THEN UNDISCH_NO_TAC 1 THEN 2006 REPEAT WEAKEN_HD_TAC THEN DISCH_TAC THEN DISCH_TAC THEN 2007 SUBGOAL_TAC `DISJOINT (P_USED_VARS p) (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` THEN1 ( 2008 FULL_SIMP_TAC list_ss [GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL, 2009 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 2010 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 2011 EXTEND_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, 2012 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 2013 IS_ELEMENT_ITERATOR_def, IN_UNION, 2014 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 2015 PROVE_TAC[] 2016 ) THEN 2017 2018 SUBGOAL_TAC `!w t. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv ==> 2019 (((w t UNION (i t DIFF LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) INTER (P_USED_VARS p)) = 2020 ((i t) INTER (P_USED_VARS p)))` THEN1 ( 2021 UNDISCH_HD_TAC THEN 2022 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 2023 symbolic_semi_automaton_REWRITES, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, PATH_SUBSET_def, SUBSET_DEF, 2024 GSYM SUBSET_COMPL_DISJOINT, SUBSET_DEF, IN_COMPL] THEN 2025 REPEAT STRIP_TAC THEN 2026 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_UNION, IN_DIFF] THEN 2027 PROVE_TAC[] 2028 ) THEN 2029 METIS_TAC[P_USED_VARS_INTER_THM] 2030); 2031 2032 2033 2034val LTL_TO_GEN_BUECHI_DS___BINDING_RUN_NOT = 2035 store_thm 2036 ("LTL_TO_GEN_BUECHI_DS___BINDING_RUN_NOT", 2037 2038 ``!DS i w l b1 b2 pf sv. 2039 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (LTL_NOT l, b1, b2, (\sv. P_NOT (pf sv))) i sv = 2040 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l, b2, b1, pf) i sv``, 2041 2042 REPEAT GEN_TAC THEN 2043 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, LTL_SEM_THM, 2044 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 2045 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, P_SEM_def] THEN 2046 METIS_TAC[]); 2047 2048 2049 2050val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT = 2051 store_thm 2052 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT", 2053 2054 ``!b1 b2 DS l pf. 2055 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, b1, b2, pf) IN DS.B ==> 2056 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(LTL_NOT l, b2, b1, \sv. P_NOT (pf sv))} {})``, 2057 2058 2059 REPEAT STRIP_TAC THEN 2060 MATCH_MP_TAC EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM THEN 2061 ASM_SIMP_TAC list_ss [UNION_EMPTY, P_USED_VARS_def, LTL_USED_VARS_def, 2062 LTL_TO_GEN_BUECHI_DS___BINDING_RUN_NOT, IN_SING] THEN 2063 PROVE_TAC[]); 2064 2065 2066 2067 2068val LTL_TO_GEN_BUECHI_DS___BINDING_RUN_AND = 2069 store_thm 2070 ("LTL_TO_GEN_BUECHI_DS___BINDING_RUN_AND", 2071 2072 ``!DS i w b11 b12 l1 pf1 b21 b22 l2 pf2 sv. 2073 (LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l1, b11, b12, pf1) i sv /\ 2074 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l2, b21, b22, pf2) i sv) ==> 2075 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (LTL_AND(l1, l2), b11 /\ b21, b12 /\ b22, (\sv. P_AND(pf1 sv, pf2 sv))) i sv``, 2076 2077 REPEAT GEN_TAC THEN 2078 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, LTL_SEM_THM, 2079 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 2080 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, P_SEM_THM] THEN 2081 METIS_TAC[]); 2082 2083 2084 2085 2086val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND = 2087 store_thm 2088 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND", 2089 2090 ``!DS b11 b12 b21 b22 l1 l2 pf1 pf2. 2091 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, b11, b12, pf1) IN DS.B /\ (l2, b21, b22, pf2) IN DS.B ==> 2092 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(LTL_AND(l1,l2), b11 /\ b21, b12 /\ b22, \sv. P_AND (pf1 sv, pf2 sv))} {})``, 2093 2094 REPEAT STRIP_TAC THEN 2095 MATCH_MP_TAC EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM THEN 2096 ASM_SIMP_TAC list_ss [UNION_EMPTY, P_USED_VARS_def, LTL_USED_VARS_def, 2097 UNION_SUBSET, IN_SING] THEN 2098 METIS_TAC[LTL_TO_GEN_BUECHI_DS___BINDING_RUN_AND]); 2099 2100 2101val LTL_TO_GEN_BUECHI_DS___BINDING_RUN_OR = 2102 store_thm 2103 ("LTL_TO_GEN_BUECHI_DS___BINDING_RUN_OR", 2104 2105 ``!DS i w b11 b12 b21 b22 l1 pf1 l2 pf2 sv. 2106 (LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l1, b11, b12, pf1) i sv /\ 2107 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l2, b21, b22, pf2) i sv) ==> 2108 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (LTL_OR(l1, l2), b11 /\ b21, b12 /\ b22, (\sv. P_OR(pf1 sv, pf2 sv))) i sv``, 2109 2110 REPEAT GEN_TAC THEN 2111 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, LTL_SEM_THM, 2112 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 2113 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, P_SEM_THM] THEN 2114 METIS_TAC[]); 2115 2116 2117val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR = 2118 store_thm 2119 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_OR", 2120 2121 ``!DS b11 b12 b21 b22 l1 l2 pf1 pf2. 2122 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, b11, b12, pf1) IN DS.B /\ (l2, b21, b22, pf2) IN DS.B==> 2123 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(LTL_OR(l1,l2), b11 /\ b21, b12 /\ b22, \sv. P_OR (pf1 sv, pf2 sv))} {})``, 2124 2125 REPEAT STRIP_TAC THEN 2126 MATCH_MP_TAC EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM THEN 2127 ASM_SIMP_TAC list_ss [UNION_EMPTY, P_USED_VARS_def, LTL_USED_VARS_def, 2128 UNION_SUBSET, P_OR_def, LTL_OR_def, IN_SING] THEN 2129 ASM_SIMP_TAC list_ss [GSYM P_OR_def, GSYM LTL_OR_def] THEN 2130 METIS_TAC[LTL_TO_GEN_BUECHI_DS___BINDING_RUN_OR]); 2131 2132 2133val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT = 2134 store_thm 2135 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT", 2136 2137 ``!b1 b2 DS DS' l pf. 2138 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [] {} [\sv. XP_EQUIV(XP_PROP (sv DS.SN), XP_NEXT (pf sv))] [] 2139 {(LTL_NEXT l, b1, b2, \sv. P_PROP(sv DS.SN))}) ==> 2140 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, b1, b2, pf) IN DS.B) ==> 2141 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 2142 2143 REPEAT STRIP_TAC THEN 2144 ASM_SIMP_TAC std_ss [] THEN 2145 MATCH_MP_TAC (SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___SEM) THEN 2146 ASM_SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_EMPTY, IMAGE_SING, BIGUNION_SING, IN_SING] THEN 2147 REPEAT STRIP_TAC THENL [ 2148 2149 2150 `?P. (\n. LTL_SEM_TIME (SUC n) i l) = P` by METIS_TAC[] THEN 2151 `?w'. PATH_EXTENSION w (sv DS.SN) P = w'` by PROVE_TAC[] THEN 2152 `PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2153 METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 2154 SUBGOAL_TAC `~((sv DS.SN) IN (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))` THEN1 ( 2155 CCONTR_TAC THEN 2156 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2157 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 2158 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IS_ELEMENT_ITERATOR_def] THEN 2159 `DS.SN < DS.SN + 1 /\ n < DS.SN + 1 /\ ~(DS.SN < DS.SN)` by DECIDE_TAC THEN 2160 PROVE_TAC[] 2161 ) THEN 2162 EXISTS_TAC ``(w':num->'a set)`` THEN 2163 LEFT_CONJ_TAC THEN1 ( 2164 PROVE_TAC [PATH_EXTENSION_EQUIV_THM] 2165 ) THEN 2166 2167 2168 SUBGOAL_TAC `!n w. (sv DS.SN IN INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w n = 2169 sv DS.SN IN w n)` THEN1 ( 2170 2171 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF] THEN 2172 REPEAT GEN_TAC THEN 2173 DISJ_EQ_STRIP_TAC THEN 2174 SIMP_TAC std_ss [] THEN 2175 DISJ2_TAC THEN 2176 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 2177 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 2178 EXISTS_TAC ``DS.SN`` THEN 2179 SIMP_TAC arith_ss [] 2180 ) THEN 2181 2182 2183 REPEAT STRIP_TAC THENL [ 2184 ASM_SIMP_TAC list_ss [SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN] THEN 2185 GSYM_NO_TAC 1 THEN 2186 ASM_SIMP_TAC std_ss [P_BIGAND_def, P_SEM_def] THEN 2187 REPEAT STRIP_TAC THENL [ 2188 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2189 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2190 UNDISCH_HD_TAC THEN 2191 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_INSERT, 2192 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 2193 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 2194 PROVE_TAC[], 2195 2196 UNDISCH_NO_TAC 1 (*sv DS.SN IN ...*) THEN GSYM_NO_TAC 4 (*Definition P*) THEN 2197 `sv DS.SN IN w' n = P n` by PROVE_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2198 ASM_SIMP_TAC std_ss [XP_SEM_THM, XP_SEM___XP_NEXT] THEN 2199 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2200 RES_TAC THEN UNDISCH_HD_TAC THEN 2201 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, 2202 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 2203 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 2204 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 2205 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def] THEN 2206 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2207 2208 `P_USED_VARS (pf sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by 2209 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 2210 2211 REMAINS_TAC `(((w (SUC n) UNION (i (SUC n) DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 2212 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 2213 (((w' (SUC n) UNION (i (SUC n) DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 2214 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` THEN1 ( 2215 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] 2216 ) THEN 2217 2218 2219 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2220 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2221 `!x n. x IN (PATH_RESTRICT w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) n) = 2222 x IN (w n)` by METIS_TAC[FUN_EQ_THM, EXTENSION] THEN 2223 SIMP_ALL_TAC arith_ss [EXTENSION, PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 2224 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2225 prove (``!x f. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF]), 2226 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, PATH_RESTRICT_def, PATH_MAP_def, 2227 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, IS_ELEMENT_ITERATOR_def, IN_INSERT] THEN 2228 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by DECIDE_TAC THEN 2229 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 2230 METIS_TAC[] 2231 ], 2232 2233 2234 GSYM_NO_TAC 12 (*Def. DS'*) THEN 2235 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 2236 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, P_SEM_def, LTL_SEM_TIME_def] THEN 2237 CONJ_TAC THEN1 ( 2238 `!n. sv DS.SN IN w' n = P n` by METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2239 METIS_TAC[] 2240 ) THEN 2241 GEN_TAC THEN STRIP_TAC THEN 2242 2243 REMAINS_TAC `!w. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS' i w sv ==> 2244 (!t. (sv DS.SN IN w t) = P_SEM (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) 2245 i (PATH_RESTRICT w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) (SUC t)) (pf sv))` THEN1 ( 2246 `LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l,b1,b2,pf) i sv` by RES_TAC THEN 2247 `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w'' 2248 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv` by 2249 METIS_TAC[EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN, MEM] THEN 2250 UNDISCH_HD_TAC THEN 2251 FULL_SIMP_TAC std_ss [] THEN 2252 METIS_TAC[LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE] 2253 ) THEN 2254 2255 2256 REPEAT GEN_TAC THEN 2257 GSYM_NO_TAC 1 (*DS' def*) THEN 2258 UNDISCH_NO_TAC 3 (*sv DS.SN IN INPUT ...*) THEN 2259 ASM_SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 2260 IS_TRANSITION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 2261 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS_def, 2262 ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 2263 XP_BIGAND_def, XP_SEM_THM, XP_SEM___XP_NEXT, 2264 INPUT_RUN_PATH_UNION_def] THEN 2265 2266 (*Keep only PATH_SUBSET w''' STATE_VARS*) 2267 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2268 STRIP_TAC THEN NTAC 3 WEAKEN_HD_TAC THEN 2269 2270 SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, symbolic_semi_automaton_REWRITES, 2271 PATH_RESTRICT_def, PATH_MAP_def] THEN 2272 2273 REMAINS_TAC `!n. (((w''' n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 2274 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 2275 ((((w''' n INTER (\s. ?n. n < DS.SN /\ (s = sv n))) UNION (i n DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 2276 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` THEN1 ( 2277 `P_USED_VARS (pf sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by 2278 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 2279 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 2280 ) THEN 2281 2282 UNDISCH_HD_TAC (*PathSUBSET*) THEN 2283 UNDISCH_NO_TAC 10 (*ELEMENT_ITERATOR*) THEN 2284 REPEAT WEAKEN_HD_TAC THEN 2285 SIMP_TAC arith_ss [PATH_SUBSET_def, EXTENSION, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 2286 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2287 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 2288 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, 2289 IS_ELEMENT_ITERATOR_def, 2290 prove(``!f x. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF])] THEN 2291 `!n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 2292 METIS_TAC[] 2293 ], 2294 2295 2296 FULL_SIMP_TAC std_ss [XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, 2297 XP_EQUIV_def, XP_IMPL_def, XP_OR_def, XP_USED_X_VARS_def, 2298 XP_NEXT___XP_USED_VARS, UNION_EMPTY, SUBSET_DEF, IN_UNION, 2299 IN_SING, P_USED_VARS_def, LTL_USED_VARS_def, 2300 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 2301 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 2302 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by 2303 DECIDE_TAC THEN 2304 METIS_TAC[] 2305 ]); 2306 2307 2308 2309 2310 2311 2312val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT = 2313 store_thm 2314 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT", 2315 2316 ``!b1 b2 DS DS' l pf. 2317 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [(DS.SN, F)] {} [\sv. XP_EQUIV(XP_NEXT_PROP (sv DS.SN), XP_CURRENT (pf sv))] [] { 2318 (LTL_PSNEXT l, b1, b2, \sv. P_PROP(sv DS.SN))}) ==> 2319 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, b1, b2, pf) IN DS.B) ==> 2320 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 2321 2322 REPEAT STRIP_TAC THEN 2323 ASM_SIMP_TAC std_ss [] THEN 2324 MATCH_MP_TAC (SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___SEM) THEN 2325 ASM_SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_EMPTY, IMAGE_SING, BIGUNION_SING, 2326 IN_SING] THEN 2327 REPEAT STRIP_TAC THENL [ 2328 2329 2330 `?P. (\n. (n > 0) /\ LTL_SEM_TIME (PRE n) i l) = P` by METIS_TAC[] THEN 2331 `?w'. PATH_EXTENSION w (sv DS.SN) P = w'` by PROVE_TAC[] THEN 2332 `PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2333 METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 2334 SUBGOAL_TAC `~((sv DS.SN) IN (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))` THEN1 ( 2335 CCONTR_TAC THEN 2336 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2337 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 2338 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IS_ELEMENT_ITERATOR_def] THEN 2339 `DS.SN < DS.SN + 1 /\ n < DS.SN + 1 /\ ~(DS.SN < DS.SN)` by DECIDE_TAC THEN 2340 PROVE_TAC[] 2341 ) THEN 2342 EXISTS_TAC ``(w':num->'a set)`` THEN 2343 LEFT_CONJ_TAC THEN1 ( 2344 PROVE_TAC [PATH_EXTENSION_EQUIV_THM] 2345 ) THEN 2346 2347 2348 SUBGOAL_TAC `!n w. (sv DS.SN IN INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w n = 2349 sv DS.SN IN w n)` THEN1 ( 2350 2351 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF] THEN 2352 REPEAT GEN_TAC THEN 2353 DISJ_EQ_STRIP_TAC THEN 2354 SIMP_TAC std_ss [] THEN 2355 DISJ2_TAC THEN 2356 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 2357 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 2358 EXISTS_TAC ``DS.SN`` THEN 2359 SIMP_TAC arith_ss [] 2360 ) THEN 2361 2362 2363 REPEAT STRIP_TAC THENL [ 2364 ASM_SIMP_TAC list_ss [SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN] THEN 2365 GSYM_NO_TAC 1 THEN 2366 ASM_SIMP_TAC std_ss [P_BIGAND_def, P_SEM_def] THEN 2367 REPEAT STRIP_TAC THENL [ 2368 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2369 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2370 UNDISCH_HD_TAC THEN 2371 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_INSERT, 2372 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 2373 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 2374 PROVE_TAC[], 2375 2376 2377 UNDISCH_HD_TAC THEN 2378 `sv DS.SN IN w' 0 = P 0` by PROVE_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2379 GSYM_NO_TAC 6 (*Definition P*) THEN 2380 ASM_SIMP_TAC arith_ss [], 2381 2382 2383 2384 UNDISCH_NO_TAC 1 (*sv DS.SN IN ...*) THEN GSYM_NO_TAC 4 (*Definition P*) THEN 2385 `sv DS.SN IN w' (SUC n) = P (SUC n)` by PROVE_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2386 ASM_SIMP_TAC std_ss [XP_SEM_THM, XP_SEM___XP_CURRENT] THEN 2387 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2388 RES_TAC THEN UNDISCH_HD_TAC THEN 2389 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, 2390 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 2391 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 2392 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 2393 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def] THEN 2394 DISCH_TAC THEN WEAKEN_HD_TAC THEN 2395 2396 `P_USED_VARS (pf sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by 2397 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 2398 2399 REMAINS_TAC `(((w n UNION (i n DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 2400 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 2401 (((w' n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 2402 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` THEN1 ( 2403 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] 2404 ) THEN 2405 2406 2407 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2408 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2409 `!x n. x IN (PATH_RESTRICT w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) n) = 2410 x IN (w n)` by METIS_TAC[FUN_EQ_THM, EXTENSION] THEN 2411 SIMP_ALL_TAC arith_ss [EXTENSION, PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 2412 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2413 prove (``!x f. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF]), 2414 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, PATH_RESTRICT_def, PATH_MAP_def, 2415 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, IS_ELEMENT_ITERATOR_def, IN_INSERT] THEN 2416 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by DECIDE_TAC THEN 2417 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 2418 METIS_TAC[] 2419 ], 2420 2421 2422 GSYM_NO_TAC 12 (*Def. DS'*) THEN 2423 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 2424 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, P_SEM_def, LTL_SEM_TIME_def] THEN 2425 CONJ_TAC THEN1 ( 2426 `!n. sv DS.SN IN w' n = P n` by METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2427 METIS_TAC[] 2428 ) THEN 2429 GEN_TAC THEN STRIP_TAC THEN 2430 2431 REMAINS_TAC `!w. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS' i w sv ==> 2432 (!t. (sv DS.SN IN w t) = ((t > 0) /\ P_SEM (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) 2433 i (PATH_RESTRICT w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) (PRE t)) (pf sv)))` THEN1 ( 2434 `LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l,b1,b2,pf) i sv` by RES_TAC THEN 2435 2436 SUBGOAL_TAC `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w'' 2437 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv` THEN1 ( 2438 ASSUME_TAC (SPECL [``DS:'a ltl_to_gen_buechi_ds``, ``sv:num -> 'a``, ``w'':num -> 'a set``, ``i:num -> 'a set``, 2439 ``DS':'a ltl_to_gen_buechi_ds``] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN) THEN 2440 SIMP_ALL_TAC std_ss [] THEN 2441 SPECL_NO_ASSUM 0 [``1:num``, ``[((DS:'a ltl_to_gen_buechi_ds).SN,F)]``] THEN 2442 SIMP_ALL_TAC list_ss [] THEN 2443 METIS_TAC[] 2444 ) THEN 2445 UNDISCH_HD_TAC THEN 2446 FULL_SIMP_TAC std_ss [] THEN 2447 METIS_TAC[LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE] 2448 ) THEN 2449 2450 2451 REPEAT GEN_TAC THEN 2452 GSYM_NO_TAC 1 (*DS' def*) THEN 2453 UNDISCH_NO_TAC 3 (*sv DS.SN IN INPUT ...*) THEN 2454 ASM_SIMP_TAC list_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 2455 IS_TRANSITION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 2456 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS_def, 2457 ltl_to_gen_buechi_ds_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 2458 XP_BIGAND_def, XP_SEM_THM, XP_SEM___XP_CURRENT, 2459 INPUT_RUN_PATH_UNION_def, LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, 2460 P_BIGAND_def, P_SEM_THM, FORALL_AND_THM] THEN 2461 REPEAT STRIP_TAC THEN 2462 Cases_on `t` THEN ( 2463 ASM_SIMP_TAC arith_ss [] 2464 ) THEN 2465 2466 (*Keep only PATH_SUBSET w''' STATE_VARS*) 2467 NTAC 5 WEAKEN_HD_TAC THEN 2468 2469 SIMP_TAC std_ss [INPUT_RUN_STATE_UNION_def, symbolic_semi_automaton_REWRITES, 2470 PATH_RESTRICT_def, PATH_MAP_def] THEN 2471 2472 REMAINS_TAC `!n. (((w''' n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 2473 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 2474 ((((w''' n INTER (\s. ?n. n < DS.SN /\ (s = sv n))) UNION (i n DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 2475 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` THEN1 ( 2476 `P_USED_VARS (pf sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by 2477 PROVE_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 2478 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 2479 ) THEN 2480 2481 UNDISCH_HD_TAC (*PathSUBSET*) THEN 2482 UNDISCH_NO_TAC 11 (*ELEMENT_ITERATOR*) THEN 2483 REPEAT WEAKEN_HD_TAC THEN 2484 SIMP_TAC arith_ss [PATH_SUBSET_def, EXTENSION, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 2485 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2486 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, 2487 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, 2488 IS_ELEMENT_ITERATOR_def, 2489 prove(``!f x. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF])] THEN 2490 `!n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 2491 METIS_TAC[] 2492 ], 2493 2494 2495 FULL_SIMP_TAC std_ss [XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, 2496 XP_EQUIV_def, XP_IMPL_def, XP_OR_def, XP_USED_X_VARS_def, 2497 XP_CURRENT___XP_USED_VARS, UNION_EMPTY, SUBSET_DEF, IN_UNION, 2498 IN_SING, P_USED_VARS_def, LTL_USED_VARS_def, 2499 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, NOT_IN_EMPTY, 2500 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 2501 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by 2502 DECIDE_TAC THEN 2503 METIS_TAC[] 2504 ]); 2505 2506 2507 2508 2509(*before we can prove the cases of SUNTIL and PSUNTIL, we need some lemmata about 2510 the semantics of these operators. These are quite specialised lemmata, which are probably not 2511 of general interest. Therefore, they are profed here and not in full_ltlTheory. Moreover, 2512 they are not exported, because they are just of insterest to proof the cases of 2513 SUNTIL and PSUNTIL. The names of these lemmata go back to their number 2514 in the book "Verification of Reactive Systems" by Klaus Schneider, 2515 Springer Verlag 2004*) 2516 2517val LEMMA_5_35___2 = 2518 prove ( 2519 ``!w p1 p2 q. (LTL_SEM w (LTL_ALWAYS( 2520 LTL_EQUIV(q, LTL_OR(p2, LTL_AND(p1, LTL_NEXT q)))))) ==> 2521 2522 ((LTL_SEM w (LTL_ALWAYS(LTL_IMPL(LTL_EVENTUAL(LTL_IMPL(p1, p2)), LTL_EQUIV(q, LTL_SUNTIL(p1, p2)))))))``, 2523 2524 REWRITE_TAC [LTL_SEM_THM] THEN 2525 ASM_REWRITE_TAC[prove (``!k:num. k >= 0``, DECIDE_TAC)] THEN 2526 REPEAT STRIP_TAC THEN 2527 2528 SUBGOAL_THEN ``?l. (l >= k /\ (LTL_SEM_TIME l w p1 ==> LTL_SEM_TIME l w p2)) /\ 2529 !l'. (k <= l' /\ l' < l) ==> (LTL_SEM_TIME l' w p1 /\ ~LTL_SEM_TIME l' w p2)`` STRIP_ASSUME_TAC THEN1( 2530 ASSUME_TAC (EXISTS_LEAST_CONV ``?l. (l >= k) /\ (LTL_SEM_TIME l w p1 ==> LTL_SEM_TIME l w p2)``) THEN 2531 RES_TAC THEN 2532 EXISTS_TAC ``l:num`` THEN 2533 ASM_REWRITE_TAC[] THEN 2534 REPEAT STRIP_TAC THEN 2535 `l'' >= k` by DECIDE_TAC THEN 2536 METIS_TAC[] 2537 ) THEN 2538 2539 2540 `!l'. (k <= l' /\ l' < l) ==> (LTL_SEM_TIME l' w q = LTL_SEM_TIME (SUC l') w q)` by METIS_TAC[] THEN 2541 2542 SUBGOAL_THEN ``!l'. (k <= l' /\ l' <= l) ==> (LTL_SEM_TIME l' w q = LTL_SEM_TIME l w q)`` STRIP_ASSUME_TAC THEN1 ( 2543 Induct_on `(l:num)-(l':num)` THENL [ 2544 SIMP_TAC arith_ss [] THEN 2545 REPEAT STRIP_TAC THEN 2546 `l = l'` by DECIDE_TAC THEN 2547 METIS_TAC[], 2548 2549 SIMP_TAC arith_ss [] THEN 2550 REPEAT STRIP_TAC THEN 2551 `v = l - SUC l'` by DECIDE_TAC THEN 2552 `SUC l' <= l` by DECIDE_TAC THEN 2553 `k <= SUC l'` by DECIDE_TAC THEN 2554 RES_TAC 2555 ] 2556 ) THEN 2557 2558 `LTL_SEM_TIME k w q = LTL_SEM_TIME l w q` by METIS_TAC[LESS_EQ_REFL, GREATER_EQ] THEN 2559 2560 Cases_on `LTL_SEM_TIME l w p2` THENL [ 2561 METIS_TAC[], 2562 2563 `~LTL_SEM_TIME l w p1` by METIS_TAC[] THEN 2564 `~LTL_SEM_TIME l w q` by METIS_TAC[] THEN 2565 `~LTL_SEM_TIME k w q` by METIS_TAC[] THEN 2566 ASM_SIMP_TAC std_ss [] THEN 2567 REPEAT STRIP_TAC THEN 2568 Cases_on `(k'' >= k) /\ LTL_SEM_TIME k'' w p2` THENL [ 2569 ASM_REWRITE_TAC[] THEN 2570 `~(k'' <= l)` by METIS_TAC[GREATER_EQ] THEN 2571 `l < k''` by DECIDE_TAC THEN 2572 METIS_TAC[GREATER_EQ], 2573 2574 METIS_TAC[] 2575 ] 2576 ]); 2577 2578 2579val LEMMA_5_35___3 = 2580 prove( 2581 ``!w p1 p2 q. (LTL_SEM w (LTL_ALWAYS( 2582 LTL_EQUIV(q, LTL_OR(p2, LTL_AND(p1, LTL_NEXT q)))))) ==> 2583 2584 ((LTL_SEM w (LTL_ALWAYS(LTL_COND(LTL_EVENTUAL(LTL_IMPL(p1, p2)), 2585 LTL_PALWAYS(LTL_EQUIV(q, LTL_SUNTIL(p1, p2))), 2586 LTL_OR(LTL_ALWAYS q, LTL_ALWAYS (LTL_NOT q)))))))``, 2587 2588REPEAT STRIP_TAC THEN 2589REWRITE_TAC [LTL_SEM_def, LTL_ALWAYS_SEM, LTL_COND_def] THEN 2590ONCE_REWRITE_TAC [LTL_SEM_TIME_def] THEN 2591REWRITE_TAC[prove (``!k:num. k >= 0``, DECIDE_TAC)] THEN 2592REWRITE_TAC [LTL_IMPL_SEM, LTL_PALWAYS_SEM] THEN 2593REPEAT STRIP_TAC THENL [ 2594 `!l. l <= k ==> LTL_SEM_TIME l w (LTL_EVENTUAL (LTL_IMPL (p1,p2)))` by METIS_TAC[LTL_EVENTUAL___PALWAYS] THEN 2595 ASSUME_TAC (REWRITE_RULE [LTL_SEM_def, LTL_IMPL_SEM, LTL_ALWAYS_SEM, prove (``!k:num. k >= 0``, DECIDE_TAC)] LEMMA_5_35___2) THEN 2596 FULL_SIMP_TAC arith_ss [LTL_ALWAYS_SEM, LTL_SEM_def], 2597 2598 2599 SIMP_TAC std_ss [LTL_SEM_THM] THEN 2600 SIMP_ASSUMPTIONS_TAC std_ss [LTL_SEM_THM] THEN 2601 REWRITE_ASSUMPTIONS_TAC [prove (``!k:num. k >= 0``, DECIDE_TAC)] THEN 2602 `!k'. (k' >= k) ==> ((LTL_SEM_TIME k' w q) = (LTL_SEM_TIME (SUC k') w q))` by METIS_TAC[] THEN 2603 2604 SUBGOAL_THEN ``!k'. (k' >= k) ==> ((LTL_SEM_TIME k' w q) = (LTL_SEM_TIME k w q))`` ASSUME_TAC THEN1( 2605 Induct_on `k' - k` THENL [ 2606 REPEAT STRIP_TAC THEN 2607 `k = k'` by DECIDE_TAC THEN 2608 METIS_TAC[], 2609 2610 REPEAT STRIP_TAC THEN 2611 `v = k' - SUC k` by DECIDE_TAC THEN 2612 `k' >= SUC k` by DECIDE_TAC THEN 2613 `!j l. (j >= SUC l) ==> (j >= l)` by DECIDE_TAC THEN 2614 `!k'. ~(k' >= SUC k) \/ LTL_SEM_TIME k' w p1 /\ ~LTL_SEM_TIME k' w p2` by METIS_TAC[] THEN 2615 `!k'. (k' >= SUC k) ==> (LTL_SEM_TIME k' w q = LTL_SEM_TIME (SUC k') w q)` by METIS_TAC[] THEN 2616 RES_TAC THEN 2617 `LTL_SEM_TIME k w q = LTL_SEM_TIME (SUC k) w q` by METIS_TAC[LESS_EQ_REFL, GREATER_EQ] THEN 2618 METIS_TAC[] 2619 ] 2620 ) THEN 2621 2622 Cases_on `LTL_SEM_TIME k w q` THEN 2623 METIS_TAC[] 2624]); 2625 2626 2627 2628val LEMMA_5_35___4 = 2629 prove ( 2630 ``!w p1 p2 q. (LTL_SEM w (LTL_ALWAYS( 2631 LTL_EQUIV(q, LTL_OR(p2, LTL_AND(p1, LTL_NEXT q)))))) ==> 2632 2633 ((LTL_SEM w (LTL_OR(LTL_ALWAYS(LTL_EQUIV(q, LTL_SUNTIL(p1, p2))), 2634 LTL_ALWAYS(LTL_EQUIV(q, LTL_UNTIL(p1, p2)))))))``, 2635 2636 2637REPEAT STRIP_TAC THEN 2638REWRITE_TAC [LTL_SEM_def, LTL_ALWAYS_SEM, LTL_COND_def] THEN 2639ONCE_REWRITE_TAC [LTL_SEM_TIME_def] THEN 2640REWRITE_TAC [LTL_IMPL_SEM, LTL_OR_SEM, LTL_ALWAYS_SEM] THEN 2641REWRITE_TAC[prove (``!k:num. k >= 0``, DECIDE_TAC)] THEN 2642Cases_on `!k. LTL_SEM_TIME k w (LTL_EVENTUAL(LTL_IMPL(p1, p2)))` THENL [ 2643 ASSUME_TAC (REWRITE_RULE [LTL_SEM_def, LTL_IMPL_SEM, LTL_ALWAYS_SEM, prove (``!k:num. k >= 0``, DECIDE_TAC)] LEMMA_5_35___2) THEN 2644 FULL_SIMP_TAC arith_ss [LTL_ALWAYS_SEM, LTL_SEM_def], 2645 2646 2647 REPEAT STRIP_TAC THEN 2648 REWRITE_ALL_TAC [LTL_SEM_TIME_def, LTL_ALWAYS_SEM, prove (``!k:num. k >= 0``, DECIDE_TAC)] THEN 2649 FULL_SIMP_TAC std_ss [] THEN 2650 REPEAT STRIP_TAC THEN 2651 2652 SUBGOAL_THEN ``?l. ~LTL_SEM_TIME l w (LTL_EVENTUAL (LTL_IMPL (p1,p2))) /\ 2653 !l'. l' < l ==> LTL_SEM_TIME l' w (LTL_EVENTUAL (LTL_IMPL (p1,p2)))`` STRIP_ASSUME_TAC THEN1( 2654 2655 ASSUME_TAC (EXISTS_LEAST_CONV ``?k. ~LTL_SEM_TIME k w (LTL_EVENTUAL (LTL_IMPL (p1,p2)))``) THEN 2656 RES_TAC THEN 2657 EXISTS_TAC ``k':num`` THEN 2658 FULL_SIMP_TAC std_ss [] 2659 ) THEN 2660 2661 REWRITE_TAC[LTL_EQUIV_SEM, LTL_UNTIL_def, LTL_OR_SEM] THEN 2662 Cases_on `!k. LTL_SEM_TIME k w q = LTL_SEM_TIME k w (LTL_SUNTIL (p1,p2))` THEN 2663 ASM_REWRITE_TAC[] THEN 2664 REPEAT STRIP_TAC THEN 2665 Cases_on `k' < l` THENL [ 2666 `LTL_SEM_TIME k' w (LTL_EVENTUAL (LTL_IMPL (p1,p2)))` by METIS_TAC[] THEN 2667 2668 SUBGOAL_THEN ``LTL_SEM_TIME k' w (LTL_EQUIV (q,LTL_SUNTIL (p1,p2)))`` ASSUME_TAC THEN1( 2669 ASSUME_TAC (REWRITE_RULE [LTL_SEM_def, LTL_IMPL_SEM, LTL_ALWAYS_SEM, prove (``!k:num. k >= 0``, DECIDE_TAC)] LEMMA_5_35___2) THEN 2670 FULL_SIMP_TAC arith_ss [LTL_ALWAYS_SEM, LTL_SEM_def] 2671 ) THEN 2672 2673 FULL_SIMP_TAC std_ss [LTL_EQUIV_SEM, LTL_OR_SEM, LTL_UNTIL_def] THEN 2674 EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 2675 REWRITE_TAC[LTL_SEM_THM] THEN 2676 FULL_SIMP_TAC std_ss [LTL_ALWAYS_SEM, LTL_EVENTUAL_SEM, LTL_IMPL_SEM] THEN 2677 EXISTS_TAC ``k''':num`` THEN 2678 METIS_TAC[GREATER_EQ], 2679 2680 2681 2682 SUBGOAL_THEN ``(!l':num. l' >= l ==> LTL_SEM_TIME l' w q) \/ (!l':num. l' >= l ==> ~LTL_SEM_TIME l' w q)`` STRIP_ASSUME_TAC THEN1( 2683 ASSUME_TAC LEMMA_5_35___3 THEN 2684 REWRITE_ASSUMPTIONS_TAC [prove (``!k:num. k >= 0``, DECIDE_TAC), LTL_SEM_THM, LTL_COND_def] THEN 2685 SIMP_TAC std_ss [LTL_SEM_THM] THEN 2686 RES_TAC THENL [ 2687 REWRITE_TAC [(ASSUME ``!k. k >= l ==> LTL_SEM_TIME k w q``)], 2688 REWRITE_TAC [(ASSUME ``!k. k >= l ==> LTL_SEM_TIME k w q``)], 2689 REWRITE_TAC [(ASSUME ``!k. k >= l ==> ~LTL_SEM_TIME k w q``)], 2690 REWRITE_TAC [(ASSUME ``!k. k >= l ==> ~LTL_SEM_TIME k w q``)] 2691 ] 2692 ) THENL [ 2693 `k' >= l` by DECIDE_TAC THEN 2694 FULL_SIMP_TAC std_ss [LTL_SEM_THM, LTL_UNTIL_def] THEN 2695 DISJ2_TAC THEN 2696 REPEAT STRIP_TAC THEN 2697 `k''' >= l` by DECIDE_TAC THEN 2698 METIS_TAC[], 2699 2700 `k' >= l` by DECIDE_TAC THEN 2701 ASM_SIMP_TAC std_ss [] THEN 2702 STRIP_TAC THENL [ 2703 FULL_SIMP_TAC std_ss [LTL_SEM_THM, LTL_UNTIL_def] THEN 2704 REPEAT STRIP_TAC THEN 2705 Cases_on `(k''' >= k') /\ LTL_SEM_TIME k''' w p2` THENL [ 2706 CLEAN_ASSUMPTIONS_TAC THEN 2707 ASM_REWRITE_TAC[] THEN 2708 `k''' >= 0` by DECIDE_TAC THEN 2709 `k''' >= l` by DECIDE_TAC THEN 2710 METIS_TAC[], 2711 2712 METIS_TAC[] 2713 ], 2714 2715 2716 FULL_SIMP_TAC arith_ss [] THEN 2717 Cases_on `k'' >= l` THENL [ 2718 FULL_SIMP_TAC std_ss [LTL_SEM_THM] THEN 2719 `k''' >= l` by DECIDE_TAC THEN 2720 METIS_TAC[], 2721 2722 2723 2724 `k'' < l` by DECIDE_TAC THEN 2725 `LTL_SEM_TIME k'' w (LTL_EVENTUAL (LTL_IMPL (p1,p2)))` by METIS_TAC[] THEN 2726 2727 SUBGOAL_THEN ``LTL_SEM_TIME k'' w (LTL_EQUIV (q,LTL_SUNTIL (p1,p2)))`` ASSUME_TAC THEN1( 2728 ASSUME_TAC (REWRITE_RULE [LTL_SEM_def, LTL_IMPL_SEM, LTL_ALWAYS_SEM, prove (``!k:num. k >= 0``, DECIDE_TAC)] LEMMA_5_35___2) THEN 2729 FULL_SIMP_TAC arith_ss [LTL_ALWAYS_SEM, LTL_SEM_def] 2730 ) THEN 2731 2732 FULL_SIMP_TAC std_ss [LTL_EQUIV_SEM] 2733 ] 2734 ] 2735 ] 2736 ] 2737]); 2738 2739 2740val LTL_UNTIL_SUNTIL_CONDITION = 2741 prove ( 2742 ``!w p1 p2 q. 2743 2744 ((LTL_SEM w (LTL_ALWAYS(LTL_EQUIV(q, LTL_UNTIL(p1, p2))))) /\ 2745 (LTL_SEM w (LTL_ALWAYS(LTL_EVENTUAL(LTL_IMPL(q, p2)))))) ==> 2746 2747 (LTL_SEM w (LTL_ALWAYS(LTL_EQUIV(q, LTL_SUNTIL(p1, p2)))))``, 2748 2749 2750 FULL_SIMP_TAC std_ss [LTL_UNTIL_def, LTL_SEM_THM] THEN 2751 REPEAT STRIP_TAC THEN 2752 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2753 METIS_TAC[], 2754 2755 ASM_SIMP_TAC std_ss [GREATER_EQ] THEN 2756 `!l l' l''. l >= l' /\ l' >= l'' ==> l >= l''` by DECIDE_TAC THEN 2757 `!k'. k' >= k ==> LTL_SEM_TIME k' w q` by METIS_TAC[] THEN 2758 `?l. l >= k /\ (LTL_SEM_TIME l w q ==> LTL_SEM_TIME l w p2)` by METIS_TAC[] THEN 2759 EXISTS_TAC ``l:num`` THEN 2760 METIS_TAC [GREATER_EQ], 2761 2762 METIS_TAC[] 2763 ]); 2764 2765 2766 2767val LEMMA_5_36___PSUNTIL = 2768 prove ( 2769 ``!w p1 p2 q. 2770 2771 (LTL_SEM w (LTL_ALWAYS(LTL_EQUIV(q, LTL_OR(p2, LTL_AND(p1, LTL_PSNEXT q)))))) = 2772 (LTL_SEM w (LTL_ALWAYS(LTL_EQUIV(q, LTL_PSUNTIL(p1, p2)))))``, 2773 2774 2775 SIMP_TAC std_ss [LTL_SEM_THM] THEN 2776 REPEAT STRIP_TAC THEN 2777 EQ_TAC THENL [ 2778 REPEAT DISCH_TAC THEN 2779 Induct_on `k` THENL [ 2780 ONCE_ASM_REWRITE_TAC [] THEN 2781 SIMP_TAC arith_ss [], 2782 2783 ONCE_ASM_REWRITE_TAC [] THEN 2784 SIMP_TAC arith_ss [] THEN 2785 ONCE_ASM_REWRITE_TAC[] THEN 2786 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2787 EXISTS_TAC ``SUC k`` THEN 2788 ASM_SIMP_TAC arith_ss [], 2789 2790 EXISTS_TAC ``k':num`` THEN 2791 ASM_SIMP_TAC arith_ss [] THEN 2792 REPEAT STRIP_TAC THEN 2793 Cases_on `j <= k` THENL [ 2794 METIS_TAC[], 2795 2796 `j = SUC k` by DECIDE_TAC THEN 2797 METIS_TAC[] 2798 ], 2799 2800 Cases_on `k' = SUC k` THENL [ 2801 METIS_TAC[], 2802 2803 DISJ2_TAC THEN 2804 REPEAT STRIP_TAC THENL [ 2805 `k' < SUC k /\ SUC k <= SUC k` by DECIDE_TAC THEN 2806 METIS_TAC[], 2807 2808 EXISTS_TAC ``k':num`` THEN 2809 `k' <= k /\ !j. j <= k ==> j <= SUC k` by DECIDE_TAC THEN 2810 METIS_TAC[] 2811 ] 2812 ] 2813 ] 2814 ], 2815 2816 REPEAT STRIP_TAC THEN 2817 Cases_on `k` THENL [ 2818 ASM_SIMP_TAC arith_ss [], 2819 2820 rename1 `SUC k > 0` THEN 2821 ASM_SIMP_TAC arith_ss [] THEN 2822 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2823 rename1 `k' <= SUC k` THEN 2824 Cases_on `k' = SUC k` THENL [ 2825 METIS_TAC[], 2826 2827 DISJ2_TAC THEN 2828 REPEAT STRIP_TAC THENL [ 2829 `k' < SUC k /\ SUC k <= SUC k` by DECIDE_TAC THEN 2830 METIS_TAC[], 2831 2832 EXISTS_TAC ``k':num`` THEN 2833 `k' <= k /\ !j. j <= k ==> j <= SUC k` by DECIDE_TAC THEN 2834 METIS_TAC[] 2835 ] 2836 ], 2837 2838 EXISTS_TAC ``SUC k`` THEN 2839 ASM_SIMP_TAC arith_ss [], 2840 2841 2842 rename1 `k' <= k` THEN 2843 EXISTS_TAC ``k':num`` THEN 2844 ASM_SIMP_TAC arith_ss [] THEN 2845 REPEAT STRIP_TAC THEN 2846 Cases_on `j <= k` THENL [ 2847 METIS_TAC[], 2848 2849 `j = SUC k` by DECIDE_TAC THEN 2850 METIS_TAC[] 2851 ] 2852 ] 2853 ] 2854 ]); 2855 2856 2857(*now we can prove the lemma for SUNTIL*) 2858val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL = 2859 store_thm 2860 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL", 2861 2862 ``!b11 b12 b21 b22 a DS DS' l1 l2 pf1 pf2. 2863 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [] {} 2864 [\sv. XP_EQUIV(XP_PROP (sv DS.SN), XP_OR(XP_CURRENT (pf2 sv), 2865 XP_AND( 2866 XP_CURRENT (pf1 sv), 2867 XP_NEXT_PROP (sv DS.SN))))] 2868 (if (b11 /\ b21 /\ a) then [\sv. P_IMPL(P_PROP(sv DS.SN), pf2 sv)] else []) 2869 {(LTL_SUNTIL(l1, l2), b11 /\ b21 /\ a, b12 /\ b22, \sv. P_PROP(sv DS.SN))}) ==> 2870 2871 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, b11, b12, pf1) IN DS.B /\ (l2, b21, b22, pf2) IN DS.B) ==> 2872 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 2873 2874 REPEAT STRIP_TAC THEN 2875 ASM_SIMP_TAC std_ss [] THEN 2876 MATCH_MP_TAC (SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___SEM) THEN 2877 ASM_SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_EMPTY, 2878 IN_SING, IMAGE_SING, BIGUNION_SING] THEN 2879 REPEAT STRIP_TAC THENL [ 2880 2881 2882 Q.ABBREV_TAC `P = (\n. LTL_SEM_TIME n (INPUT_RUN_PATH_UNION 2883 (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w) 2884 (LTL_SUNTIL(LTL_PROP (pf1 sv), LTL_PROP (pf2 sv))))` THEN 2885 Q.ABBREV_TAC `w' = PATH_EXTENSION w (sv DS.SN) P` THEN 2886 2887 2888 `PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2889 METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 2890 2891 SUBGOAL_TAC `~((sv DS.SN) IN (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))` THEN1 ( 2892 CCONTR_TAC THEN 2893 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2894 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 2895 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IS_ELEMENT_ITERATOR_def] THEN 2896 `DS.SN < DS.SN + 1 /\ n < DS.SN + 1 /\ ~(DS.SN < DS.SN)` by DECIDE_TAC THEN 2897 PROVE_TAC[] 2898 ) THEN 2899 EXISTS_TAC ``(w':num->'a set)`` THEN 2900 LEFT_CONJ_TAC THEN1 ( 2901 METIS_TAC [PATH_EXTENSION_EQUIV_THM] 2902 ) THEN 2903 2904 2905 (*some usefull lemmata*) 2906 `P_USED_VARS (pf1 sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV /\ 2907 P_USED_VARS (pf2 sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by 2908 METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 2909 SUBGOAL_TAC `!n. ((((w n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 2910 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 2911 (((w' n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 2912 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))))` THEN1 ( 2913 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2914 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2915 `!x n. x IN (PATH_RESTRICT w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) n) = 2916 x IN (w n)` by METIS_TAC[FUN_EQ_THM, EXTENSION] THEN 2917 SIMP_ALL_TAC arith_ss [EXTENSION, PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 2918 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 2919 prove (``!x f. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF]), 2920 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, PATH_RESTRICT_def, PATH_MAP_def, 2921 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, IS_ELEMENT_ITERATOR_def, IN_INSERT] THEN 2922 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by DECIDE_TAC THEN 2923 REPEAT GEN_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 2924 METIS_TAC[] 2925 ) THEN 2926 2927 `!n. sv DS.SN IN w' n = P n` by METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2928 SUBGOAL_TAC `!n w'. sv DS.SN IN INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w' n = 2929 sv DS.SN IN w' n` THEN1 ( 2930 REPEAT GEN_TAC THEN 2931 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF] THEN 2932 DISJ_EQ_STRIP_TAC THEN 2933 SIMP_TAC std_ss [] THEN 2934 DISJ2_TAC THEN 2935 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 2936 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 2937 EXISTS_TAC ``DS.SN`` THEN 2938 SIMP_TAC arith_ss [] 2939 ) THEN 2940 2941 2942 REPEAT STRIP_TAC THENL [ 2943 ASM_SIMP_TAC list_ss [SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN] THEN 2944 GSYM_NO_TAC 5 (*w = PATH_RESTRICT w'*) THEN 2945 ASM_SIMP_TAC std_ss [P_BIGAND_def, P_SEM_def] THEN 2946 REPEAT STRIP_TAC THENL [ 2947 2948 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 2949 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 2950 UNDISCH_HD_TAC THEN 2951 REPEAT WEAKEN_HD_TAC THEN 2952 SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_INSERT, 2953 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 2954 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 2955 PROVE_TAC[], 2956 2957 2958 2959 2960 UNDISCH_NO_TAC 1 (*sv DS.SN IN_INPUT_RUN_...*) THEN 2961 ASM_SIMP_TAC std_ss [XP_SEM_THM, INPUT_RUN_PATH_UNION_def, XP_SEM___XP_CURRENT, INPUT_RUN_STATE_UNION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 2962 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def] THEN 2963 Q.UNABBREV_TAC `P` THEN 2964 SUBGOAL_TAC `!w. (LTL_SEM_TIME n w 2965 (LTL_SUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv)))) = 2966 P_SEM (w n) (pf2 sv) \/ 2967 (P_SEM (w n) (pf1 sv) /\ 2968 (LTL_SEM_TIME (SUC n) w 2969 (LTL_SUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv)))))` THEN1 ( 2970 REPEAT WEAKEN_HD_TAC THEN 2971 GEN_TAC THEN 2972 ASSUME_TAC (SPECL [``LTL_PROP ((pf1:(num->'a)->'a prop_logic) sv)``, 2973 ``LTL_PROP ((pf2:(num->'a)->'a prop_logic) sv)``] 2974 LTL_RECURSION_LAWS___LTL_SUNTIL) THEN 2975 SIMP_ALL_TAC std_ss [LTL_SEM_THM, LTL_EQUIVALENT_def] THEN 2976 SPECL_NO_ASSUM 0 [``n:num``] THEN 2977 ASM_REWRITE_TAC[] 2978 ) THEN 2979 ASM_REWRITE_TAC[] THEN 2980 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 2981 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 2982 ltl_to_gen_buechi_ds_REWRITES, symbolic_semi_automaton_REWRITES, 2983 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, GSYM IN_UNION, IN_ABS] THEN 2984 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 2985 2986 2987 Cases_on `b11 /\ b21 /\ a` THEN ( 2988 CLEAN_ASSUMPTIONS_TAC THEN 2989 FULL_SIMP_TAC list_ss [] 2990 ) THEN 2991 UNDISCH_NO_TAC 5 (*sv DS.SN IN ...*) THEN 2992 ASM_SIMP_TAC std_ss [A_SEM_def, ACCEPT_COND_GF_def, 2993 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, 2994 ACCEPT_F_def, P_SEM_THM] THEN 2995 REPEAT STRIP_TAC THEN 2996 rename1 `(_ >= t1)` THEN 2997 Q.UNABBREV_TAC `P` THEN 2998 FULL_SIMP_TAC std_ss [LTL_SEM_TIME_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 2999 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 3000 ltl_to_gen_buechi_ds_REWRITES, symbolic_semi_automaton_REWRITES, 3001 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IN_ABS] THEN 3002 Cases_on `?t2. t2 >= t1 /\ P_SEM 3003 (w' t2 UNION (i t2 DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) (pf2 sv)` THENL [ 3004 METIS_TAC[], 3005 3006 SIMP_ASSUMPTIONS_TAC std_ss [] THEN 3007 EXISTS_TAC ``t1:num`` THEN 3008 ASM_SIMP_TAC arith_ss [] THEN 3009 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3010 ] 3011 ], 3012 3013 3014 GSYM_NO_TAC 17 (*Def. DS'*) THEN 3015 GSYM_NO_TAC 11 (*Definition of P*) THEN 3016 GSYM_NO_TAC 8 (*w = PATH_RESTRICT ...*) THEN 3017 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 3018 P_SEM_def] THEN 3019 3020 (*Usefull lemmata*) 3021 `LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l1,b11,b12,pf1) i sv /\ 3022 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l2,b21,b22,pf2) i sv` by 3023 (RES_TAC THEN ASM_REWRITE_TAC[]) THEN 3024 3025 CONJ_TAC THENL [ 3026 GEN_TAC THEN 3027 ASM_SIMP_TAC std_ss [P_SEM_def, LTL_SEM_TIME_def] THEN 3028 NTAC 2 UNDISCH_HD_TAC THEN 3029 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE] THEN 3030 REPEAT (DISCH_TAC THEN WEAKEN_HD_TAC) THEN 3031 EXISTS_EQ_STRIP_TAC THEN 3032 REMAINS_TAC `!n. ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w n) 3033 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) = 3034 ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w n) 3035 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))` THEN1 ( 3036 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3037 ) THEN 3038 GSYM_NO_TAC 2 (*Definition DS'*) THEN 3039 UNDISCH_NO_TAC 14 (*Iterator*) THEN 3040 UNDISCH_NO_TAC 10 (*Path Subset*) THEN 3041 ASM_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3042 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 3043 EXTENSION, IN_UNION, IN_INTER, IN_DIFF, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3044 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, PATH_SUBSET_def, SUBSET_DEF, 3045 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 3046 IS_ELEMENT_ITERATOR_def] THEN 3047 REPEAT WEAKEN_HD_TAC THEN 3048 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 3049 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 3050 METIS_TAC[], 3051 3052 GEN_TAC THEN STRIP_TAC THEN 3053 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN 3054 GEN_TAC THEN 3055 REMAINS_TAC ` ((b11 /\ b21 /\ a) /\ sv DS.SN IN w'' t ==> 3056 LTL_SEM_TIME t 3057 (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) 3058 i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))) (LTL_SUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv)))) /\ 3059 ((b12 /\ b22) /\ 3060 LTL_SEM_TIME t 3061 (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) 3062 i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))) (LTL_SUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv))) ==> 3063 sv DS.SN IN w'' t)` THEN1 ( 3064 3065 NTAC 2 UNDISCH_HD_TAC THEN 3066 ASM_SIMP_TAC std_ss [P_SEM_def, LTL_SEM_THM, LTL_UNTIL_def] THEN 3067 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE] THEN 3068 SUBGOAL_TAC `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv` THEN1 ( 3069 UNDISCH_NO_TAC 0 THEN UNDISCH_NO_TAC 18 THEN 3070 UNDISCH_NO_TAC 6 THEN UNDISCH_NO_TAC 19 THEN 3071 REPEAT WEAKEN_HD_TAC THEN 3072 SIMP_TAC std_ss [] THEN 3073 REPEAT STRIP_TAC THEN 3074 ASSUME_TAC (SPECL [``DS:'a ltl_to_gen_buechi_ds``, ``sv:num -> 'a``, ``w'':num -> 'a set``, ``i:num -> 'a set``, 3075 ``DS':'a ltl_to_gen_buechi_ds``] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN) THEN 3076 SIMP_ALL_TAC std_ss [] THEN 3077 SPECL_NO_ASSUM 0 [``1:num``, ``[]:(num # bool) list``] THEN 3078 SIMP_ALL_TAC list_ss [] THEN 3079 METIS_TAC[] 3080 ) THEN 3081 3082 3083 REMAINS_TAC `!n w. LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i w sv ==> 3084 (((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w n) 3085 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) = 3086 ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w n) 3087 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` THEN1 ( 3088 3089 3090 (*Cleaning up*) 3091 NTAC 2 UNDISCH_HD_TAC (*current FairRun Stuff*) THEN 3092 UNDISCH_NO_TAC 18 (*w Fair run*) THEN 3093 UNDISCH_NO_TAC 4 (*Binding-Run pf2*) THEN 3094 UNDISCH_NO_TAC 2 (*Binding-Run pf1*) THEN 3095 NTAC 2 (UNDISCH_NO_TAC 10) (*P_USED_VARS pf1 pf2*) THEN 3096 SIMP_TAC std_ss [] THEN 3097 REPEAT WEAKEN_HD_TAC THEN 3098 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3099 ) THEN 3100 UNDISCH_NO_TAC 20 (*Iterator*) THEN 3101 GSYM_NO_TAC 8 (*DEF DS'*) THEN 3102 ASM_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3103 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 3104 EXTENSION, IN_UNION, IN_INTER, IN_DIFF, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3105 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, PATH_SUBSET_def, SUBSET_DEF, 3106 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 3107 IS_ELEMENT_ITERATOR_def, LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 3108 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 3109 REPEAT WEAKEN_HD_TAC THEN 3110 REPEAT STRIP_TAC THEN 3111 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 3112 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 3113 METIS_TAC[] 3114 ) THEN 3115 3116 `?q. q = LTL_PROP (P_PROP (sv DS.SN))` by METIS_TAC[] THEN 3117 `?v. v = (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w'')` by METIS_TAC[] THEN 3118 3119 SUBGOAL_TAC `(sv DS.SN IN w'' t = LTL_SEM_TIME t v q) /\ 3120 (LTL_SEM v (LTL_ALWAYS(LTL_EQUIV(q, LTL_OR(LTL_PROP (pf2 sv), LTL_AND(LTL_PROP (pf1 sv), LTL_NEXT q)))))) /\ 3121 (b11 /\ b21 /\ a ==> (LTL_SEM v (LTL_ALWAYS(LTL_EVENTUAL(LTL_IMPL(q, LTL_PROP (pf2 sv)))))))` THEN1 ( 3122 (*Cleaning up*) 3123 NTAC 3 UNDISCH_HD_TAC THEN 3124 UNDISCH_NO_TAC 6 (*sv DS.SN IN ...*) THEN 3125 GSYM_NO_TAC 4 (*Definition D'*) THEN 3126 ASM_REWRITE_TAC[] THEN 3127 REPEAT WEAKEN_HD_TAC THEN 3128 REPEAT DISCH_TAC THEN 3129 ASM_REWRITE_TAC[] THEN 3130 3131 SIMP_ALL_TAC list_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 3132 IS_TRANSITION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 3133 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3134 XP_BIGAND_def, XP_SEM_THM, LTL_SEM_THM, P_SEM_THM, 3135 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3136 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, XP_SEM___XP_CURRENT, 3137 FORALL_AND_THM, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def] THEN 3138 UNDISCH_NO_TAC 4 THEN 3139 ONCE_ASM_REWRITE_TAC[] THEN 3140 REPEAT STRIP_TAC THENL [ 3141 REWRITE_TAC[], 3142 METIS_TAC[], 3143 3144 WEAKEN_NO_TAC 3 THEN 3145 FULL_SIMP_TAC list_ss [A_BIGAND_def, A_SEM_THM, 3146 ACCEPT_COND_GF_def, ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, 3147 ACCEPT_F_def, P_SEM_THM] THEN 3148 METIS_TAC[] 3149 ] 3150 ) THEN 3151 3152 SUBGOAL_TAC `(LTL_SEM_TIME t (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) 3153 i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))) 3154 (LTL_SUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv))) = 3155 LTL_SEM_TIME t v (LTL_SUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv)))) /\ 3156 (LTL_SEM_TIME t (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) 3157 i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))) 3158 (LTL_UNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv))) = 3159 LTL_SEM_TIME t v (LTL_UNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv))))` THEN1 ( 3160 SUBGOAL_TAC `!n. ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w'' n) 3161 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) = 3162 ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i 3163 (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) n) 3164 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))` THEN1 ( 3165 GSYM_NO_TAC 10 (*Definition DS'*) THEN 3166 UNDISCH_NO_TAC 22 (*Iterator*) THEN 3167 `PATH_SUBSET w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS' sv)` by 3168 METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 3169 UNDISCH_HD_TAC THEN 3170 ASM_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3171 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 3172 EXTENSION, IN_UNION, IN_INTER, IN_DIFF, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3173 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, PATH_SUBSET_def, SUBSET_DEF, 3174 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 3175 IS_ELEMENT_ITERATOR_def, PATH_RESTRICT_def, PATH_MAP_def] THEN 3176 REPEAT WEAKEN_HD_TAC THEN 3177 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 3178 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 3179 METIS_TAC[] 3180 ) THEN 3181 ASM_SIMP_TAC std_ss [LTL_SEM_THM, LTL_UNTIL_def] THEN 3182 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3183 ) THEN 3184 3185 3186 (*Cleaning up*) 3187 GSYM_NO_TAC 6 (*Definition q*) THEN 3188 GSYM_NO_TAC 6 (*Definition v*) THEN 3189 ASM_REWRITE_TAC[] THEN 3190 NTAC 2 UNDISCH_HD_TAC THEN 3191 NTAC 2 WEAKEN_HD_TAC THEN 3192 NTAC 3 UNDISCH_HD_TAC THEN 3193 REPEAT WEAKEN_HD_TAC THEN 3194 REPEAT DISCH_TAC THEN 3195 (*continuing proof*) 3196 `LTL_SEM v (LTL_OR(LTL_ALWAYS(LTL_EQUIV(q, LTL_SUNTIL(LTL_PROP (pf1 sv), LTL_PROP (pf2 sv)))), 3197 LTL_ALWAYS(LTL_EQUIV(q, LTL_UNTIL(LTL_PROP (pf1 sv), LTL_PROP (pf2 sv))))))` by 3198 METIS_TAC[LEMMA_5_35___4] THEN UNDISCH_HD_TAC THEN 3199 SIMP_TAC std_ss [LTL_SEM_def, LTL_OR_SEM, LTL_ALWAYS_SEM, LTL_EQUIV_SEM] THEN 3200 REPEAT STRIP_TAC THENL [ 3201 METIS_TAC[], 3202 METIS_TAC[], 3203 3204 ASSUME_TAC LTL_UNTIL_SUNTIL_CONDITION THEN 3205 FULL_SIMP_TAC std_ss [LTL_SEM_def, LTL_ALWAYS_SEM, LTL_EQUIV_SEM] THEN 3206 SPECL_NO_ASSUM 0 [``v:num->'a set``, ``LTL_PROP ((pf1:(num->'a)->'a prop_logic) sv)``, 3207 ``LTL_PROP ((pf2:(num->'a)->'a prop_logic) sv)``, ``q:'a ltl``] THEN 3208 METIS_TAC[], 3209 3210 ASM_SIMP_TAC std_ss [LTL_UNTIL_def, LTL_OR_SEM] 3211 ] 3212 ] 3213 ], 3214 3215 Q.ABBREV_TAC `a' = b11 /\ b21 /\ a` THEN 3216 Cases_on `a'` THEN 3217 FULL_SIMP_TAC list_ss [XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, 3218 XP_EQUIV_def, XP_IMPL_def, XP_OR_def, XP_USED_X_VARS_def, 3219 XP_CURRENT___XP_USED_VARS, UNION_EMPTY, SUBSET_DEF, IN_UNION, 3220 IN_SING, P_USED_VARS_def, LTL_USED_VARS_def, 3221 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, NOT_IN_EMPTY, 3222 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, LIST_BIGUNION_def, 3223 P_USED_VARS_def, P_IMPL_def, P_OR_def] THEN 3224 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by 3225 DECIDE_TAC THEN 3226 METIS_TAC[] 3227 ]); 3228 3229 3230 3231 3232 3233val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL = 3234 store_thm 3235 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL", 3236 3237 ``!b11 b12 b21 b22 DS DS' l1 l2 pf1 pf2. 3238 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [(DS.SN, F)] {} 3239 [\sv. XP_EQUIV(XP_NEXT_PROP (sv DS.SN), XP_OR(XP_CURRENT (pf2 sv), 3240 XP_AND( 3241 XP_CURRENT (pf1 sv), 3242 XP_PROP (sv DS.SN))))] 3243 [] 3244 {(LTL_PSUNTIL(l1, l2), b11 /\ b21, b12 /\ b22, \sv. (P_OR(pf2 sv, P_AND(pf1 sv, P_PROP(sv DS.SN)))))}) ==> 3245 3246 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, b11, b12, pf1) IN DS.B /\ (l2, b21, b22, pf2) IN DS.B) ==> 3247 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 3248 3249 REPEAT STRIP_TAC THEN 3250 ASM_SIMP_TAC std_ss [] THEN 3251 MATCH_MP_TAC (SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___SEM) THEN 3252 ASM_SIMP_TAC list_ss [LIST_BIGUNION_def, UNION_EMPTY, IN_SING, IMAGE_SING, BIGUNION_SING] THEN 3253 REPEAT STRIP_TAC THENL [ 3254 3255 3256 `?P. (\n. n > 0 /\ LTL_SEM_TIME (PRE n) (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w) 3257 (LTL_PSUNTIL(LTL_PROP (pf1 sv), LTL_PROP (pf2 sv)))) = P` by METIS_TAC [] THEN 3258 `?w'. PATH_EXTENSION w (sv DS.SN) P = w'` by PROVE_TAC[] THEN 3259 3260 3261 `PATH_SUBSET w (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 3262 METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 3263 3264 SUBGOAL_TAC `~((sv DS.SN) IN (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv))` THEN1 ( 3265 CCONTR_TAC THEN 3266 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 3267 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 3268 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IS_ELEMENT_ITERATOR_def] THEN 3269 `DS.SN < DS.SN + 1 /\ n < DS.SN + 1 /\ ~(DS.SN < DS.SN)` by DECIDE_TAC THEN 3270 PROVE_TAC[] 3271 ) THEN 3272 EXISTS_TAC ``(w':num->'a set)`` THEN 3273 LEFT_CONJ_TAC THEN1 ( 3274 METIS_TAC [PATH_EXTENSION_EQUIV_THM] 3275 ) THEN 3276 3277 3278 (*some usefull lemmata*) 3279 `P_USED_VARS (pf1 sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV /\ 3280 P_USED_VARS (pf2 sv) SUBSET LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV` by 3281 METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___USED_BINDING_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR] THEN 3282 3283 `!n. sv DS.SN IN w' n = P n` by METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 3284 SUBGOAL_TAC `!n w'. sv DS.SN IN INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w' n = 3285 sv DS.SN IN w' n` THEN1 ( 3286 REPEAT GEN_TAC THEN 3287 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF] THEN 3288 DISJ_EQ_STRIP_TAC THEN 3289 SIMP_TAC std_ss [] THEN 3290 DISJ2_TAC THEN 3291 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3292 symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS] THEN 3293 EXISTS_TAC ``DS.SN`` THEN 3294 SIMP_TAC arith_ss [] 3295 ) THEN 3296 3297 3298 REPEAT STRIP_TAC THENL [ 3299 ASM_SIMP_TAC list_ss [SIMP_RULE std_ss [] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN] THEN 3300 GSYM_NO_TAC 4 (*w = PATH_RESTRICT w'*) THEN 3301 ASM_SIMP_TAC std_ss [P_BIGAND_def, P_SEM_def] THEN 3302 REPEAT STRIP_TAC THENL [ 3303 3304 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 3305 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 3306 UNDISCH_HD_TAC THEN 3307 REPEAT WEAKEN_HD_TAC THEN 3308 SIMP_TAC std_ss [PATH_SUBSET_def, SUBSET_DEF, IN_INSERT, 3309 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3310 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 3311 PROVE_TAC[], 3312 3313 3314 UNDISCH_HD_TAC THEN 3315 GSYM_NO_TAC 8 (*Definition P*) THEN 3316 ASM_SIMP_TAC arith_ss [], 3317 3318 3319 3320 3321 UNDISCH_NO_TAC 1 (*sv DS.SN IN_INPUT_RUN_...*) THEN 3322 ASM_SIMP_TAC std_ss [XP_SEM_THM, INPUT_RUN_PATH_UNION_def, XP_SEM___XP_CURRENT, INPUT_RUN_STATE_UNION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 3323 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def] THEN 3324 GSYM_NO_TAC 7 (*Definition P*) THEN 3325 ASM_SIMP_TAC std_ss [] THEN 3326 SUBGOAL_TAC `!w. (LTL_SEM_TIME n w 3327 (LTL_PSUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv)))) = 3328 P_SEM (w n) (pf2 sv) \/ 3329 (P_SEM (w n) (pf1 sv) /\ 3330 n > 0 /\ 3331 (LTL_SEM_TIME (PRE n) w 3332 (LTL_PSUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv)))))` THEN1 ( 3333 REPEAT WEAKEN_HD_TAC THEN 3334 GEN_TAC THEN 3335 ASSUME_TAC (SPECL [``LTL_PROP ((pf1:(num->'a)->'a prop_logic) sv)``, 3336 ``LTL_PROP ((pf2:(num->'a)->'a prop_logic) sv)``] 3337 LTL_RECURSION_LAWS___LTL_PSUNTIL) THEN 3338 SIMP_ALL_TAC std_ss [LTL_SEM_THM, LTL_EQUIVALENT_def] THEN 3339 SPECL_NO_ASSUM 0 [``n:num``] THEN 3340 ASM_REWRITE_TAC[] 3341 ) THEN 3342 ASM_REWRITE_TAC[] THEN 3343 SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3344 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 3345 ltl_to_gen_buechi_ds_REWRITES, symbolic_semi_automaton_REWRITES, 3346 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3347 3348 REMAINS_TAC `!n. ((((w n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 3349 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 3350 (((w' n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 3351 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))))` THEN1 ( 3352 3353 (*Keep only the new proposition and P_USED_VARS pf1, pf2 SUBSET ....*) 3354 REPEAT (DISCH_TAC THEN WEAKEN_HD_TAC) THEN 3355 UNDISCH_HD_TAC THEN 3356 NTAC 4 WEAKEN_HD_TAC THEN 3357 NTAC 2 UNDISCH_HD_TAC THEN 3358 REPEAT WEAKEN_HD_TAC THEN 3359 REPEAT STRIP_TAC THEN 3360 3361 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3362 ) THEN 3363 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 3364 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 3365 `!x n. x IN (PATH_RESTRICT w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) n) = 3366 x IN (w n)` by METIS_TAC[FUN_EQ_THM, EXTENSION] THEN 3367 SIMP_ALL_TAC arith_ss [EXTENSION, PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 3368 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 3369 prove (``!x f. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF]), 3370 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, PATH_RESTRICT_def, PATH_MAP_def, 3371 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, IS_ELEMENT_ITERATOR_def, IN_INSERT] THEN 3372 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by DECIDE_TAC THEN 3373 REPEAT GEN_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 3374 METIS_TAC[] 3375 ], 3376 3377 3378 GSYM_NO_TAC 16 (*Def. DS'*) THEN 3379 GSYM_NO_TAC 10 (*Definition of P*) THEN 3380 GSYM_NO_TAC 7 (*w = PATH_RESTRICT ...*) THEN 3381 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE, 3382 P_SEM_THM] THEN 3383 3384 (*Usefull lemmata*) 3385 `LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l1,b11,b12,pf1) i sv /\ 3386 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l2,b21,b22,pf2) i sv` by 3387 (RES_TAC THEN ASM_REWRITE_TAC[]) THEN 3388 3389 CONJ_TAC THENL [ 3390 GEN_TAC THEN 3391 ASSUME_TAC (SPECL [``l1:'a ltl``, ``l2:'a ltl``, ``t:num``] 3392 (REWRITE_RULE [LTL_EQUIVALENT_def] LTL_RECURSION_LAWS___LTL_PSUNTIL)) THEN 3393 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 3394 NTAC 2 UNDISCH_HD_TAC THEN 3395 GSYM_NO_TAC 2 (*Definition DS'*) THEN 3396 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, LTL_SEM_THM] THEN 3397 REPEAT (DISCH_TAC THEN WEAKEN_HD_TAC) THEN 3398 ASM_SIMP_TAC std_ss [ 3399 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 3400 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3401 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 3402 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3403 symbolic_semi_automaton_REWRITES] THEN 3404 3405 REMAINS_TAC `!n. ((((w n UNION (i n DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 3406 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 3407 (((w' n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 3408 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))) /\ 3409 3410 ((((w n UNION (i n DIFF (\s. ?n. n < DS.SN /\ (s = sv n)))) INTER 3411 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) = 3412 (((w n UNION (i n DIFF (\s. ?n. n < DS.SN + 1 /\ (s = sv n)))) INTER 3413 (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))))` THEN1 ( 3414 3415 (*Keep only the new proposition and P_USED_VARS pf1, pf2 SUBSET ....*) 3416 UNDISCH_HD_TAC THEN 3417 NTAC 6 WEAKEN_HD_TAC THEN 3418 NTAC 2 UNDISCH_HD_TAC THEN 3419 REPEAT WEAKEN_HD_TAC THEN 3420 REPEAT STRIP_TAC THEN 3421 3422 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3423 ) THEN 3424 3425 `PATH_SUBSET w' ((sv DS.SN) INSERT LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)` by 3426 METIS_TAC[PATH_EXTENSION_EQUIV_THM] THEN 3427 `!x n. x IN (PATH_RESTRICT w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv) n) = 3428 x IN (w n)` by METIS_TAC[FUN_EQ_THM, EXTENSION] THEN 3429 SIMP_ALL_TAC arith_ss [EXTENSION, PATH_SUBSET_def, SUBSET_DEF, IN_UNION, IN_INTER, IN_DIFF, 3430 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, 3431 prove (``!x f. x IN (\x. f x) = f x``, SIMP_TAC std_ss [IN_DEF]), 3432 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, PATH_RESTRICT_def, PATH_MAP_def, 3433 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_EMPTY, IS_ELEMENT_ITERATOR_def, IN_INSERT] THEN 3434 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by DECIDE_TAC THEN 3435 REPEAT GEN_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 3436 METIS_TAC[], 3437 3438 3439 3440 3441 GEN_TAC THEN DISCH_TAC THEN 3442 SIMP_TAC std_ss [GSYM FORALL_AND_THM] THEN GEN_TAC THEN 3443 REMAINS_TAC `!t. ((sv DS.SN IN w'' t) = (t > 0) /\ LTL_SEM_TIME (PRE t) 3444 (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) 3445 i w'') 3446 (LTL_PSUNTIL (LTL_PROP (pf1 sv),LTL_PROP (pf2 sv))))` THEN1 ( 3447 3448 3449 UNDISCH_HD_TAC THEN 3450 ASM_SIMP_TAC std_ss [P_SEM_def, LTL_SEM_THM] THEN 3451 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN___REWRITE] THEN 3452 SUBGOAL_TAC `LTL_TO_GEN_BUECHI_DS___FAIR_RUN DS i (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) sv` THEN1 ( 3453 UNDISCH_NO_TAC 0 THEN UNDISCH_NO_TAC 17 THEN 3454 UNDISCH_NO_TAC 6 THEN UNDISCH_NO_TAC 18 THEN 3455 REPEAT WEAKEN_HD_TAC THEN 3456 SIMP_TAC std_ss [] THEN 3457 REPEAT STRIP_TAC THEN 3458 ASSUME_TAC (SPECL [``DS:'a ltl_to_gen_buechi_ds``, ``sv:num -> 'a``, ``w'':num -> 'a set``, ``i:num -> 'a set``, 3459 ``DS':'a ltl_to_gen_buechi_ds``] EXTEND_LTL_TO_GEN_BUECHI_DS___FAIR_RUN) THEN 3460 SIMP_ALL_TAC std_ss [] THEN 3461 SPECL_NO_ASSUM 0 [``1:num``, ``[((DS:'a ltl_to_gen_buechi_ds).SN, F)]``] THEN 3462 SIMP_ALL_TAC list_ss [] THEN 3463 METIS_TAC[] 3464 ) THEN 3465 3466 3467 DISCH_TAC THEN WEAKEN_HD_TAC THEN 3468 SUBGOAL_TAC `!n. (((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w' n) 3469 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) = 3470 ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w n) 3471 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) /\ 3472 3473 (((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w n) 3474 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) = 3475 ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i w n) 3476 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV))) /\ 3477 3478 (((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv) i 3479 (PATH_RESTRICT w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv)) n) 3480 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)) = 3481 ((INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w'' n) 3482 INTER (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS sv UNION DS.IV)))` THEN1 ( 3483 3484 UNDISCH_NO_TAC 19 (*Iterator*) THEN 3485 UNDISCH_NO_TAC 15 (*PATH_SUBSET w*) THEN 3486 GSYM_NO_TAC 8 (*DEF DS'*) THEN 3487 UNDISCH_NO_TAC 7 (*PATH_RESTRICT w' = w*) THEN 3488 `PATH_SUBSET w' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS' sv)` 3489 by METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 3490 `PATH_SUBSET w'' (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS DS' sv)` 3491 by METIS_TAC[LTL_TO_GEN_BUECHI_DS___FAIR_RUN___PATH_SUBSET] THEN 3492 NTAC 2 UNDISCH_HD_TAC THEN 3493 3494 SIMP_TAC std_ss [EXTENSION] THEN 3495 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 3496 ASM_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3497 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, 3498 EXTENSION, IN_UNION, IN_INTER, IN_DIFF, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3499 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, PATH_SUBSET_def, SUBSET_DEF, 3500 LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def, UNION_EMPTY, 3501 IS_ELEMENT_ITERATOR_def, LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, 3502 PATH_RESTRICT_def, PATH_MAP_def, PATH_SUBSET_def] THEN 3503 REPEAT WEAKEN_HD_TAC THEN 3504 REPEAT STRIP_TAC THEN 3505 `DS.SN < DS.SN + 1 /\ !n. n < DS.SN ==> n < DS.SN + 1` by DECIDE_TAC THEN 3506 REPEAT STRIP_TAC THEN REPEAT BOOL_EQ_STRIP_TAC THEN 3507 METIS_TAC[] 3508 ) THEN 3509 3510 3511 (*Cleaning up*) 3512 SPECL_NO_ASSUM 4 [``PATH_RESTRICT (w'':num->'a set) (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (DS:'a ltl_to_gen_buechi_ds) sv)``] THEN 3513 SPECL_NO_ASSUM 6 [``PATH_RESTRICT (w'':num->'a set) (LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS (DS:'a ltl_to_gen_buechi_ds) sv)``] THEN 3514 NTAC 4 UNDISCH_HD_TAC (*path constraints*) THEN 3515 NTAC 2 (UNDISCH_NO_TAC 9) (*P_USED_VARS pf1 pf2*) THEN 3516 REPEAT WEAKEN_HD_TAC THEN 3517 REPEAT STRIP_TAC THEN 3518 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM] 3519 ) THEN 3520 3521 3522 `?q. q = LTL_NEXT(LTL_PROP (P_PROP (sv DS.SN)))` by METIS_TAC[] THEN 3523 `?v. v = (INPUT_RUN_PATH_UNION (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS' sv) i w'')` by METIS_TAC[] THEN 3524 3525 3526 REMAINS_TAC `(!t. (sv DS.SN IN w'' t = (t > 0 /\ LTL_SEM_TIME (PRE t) v q))) /\ 3527 (LTL_SEM v (LTL_ALWAYS(LTL_EQUIV(q, LTL_OR(LTL_PROP (pf2 sv), LTL_AND(LTL_PROP (pf1 sv), LTL_PSNEXT q))))))` THEN1 ( 3528 3529 SIMP_ALL_TAC std_ss [LEMMA_5_36___PSUNTIL] THEN 3530 UNDISCH_HD_TAC THEN 3531 ASM_SIMP_TAC arith_ss [LTL_SEM_THM] 3532 ) THEN 3533 3534 (*Cleaning up*) 3535 NTAC 3 UNDISCH_HD_TAC THEN 3536 UNDISCH_NO_TAC 6 (*sv DS.SN IN ...*) THEN 3537 GSYM_NO_TAC 4 (*Definition D'*) THEN 3538 ASM_REWRITE_TAC[] THEN 3539 REPEAT WEAKEN_HD_TAC THEN 3540 REPEAT DISCH_TAC THEN 3541 ASM_REWRITE_TAC[] THEN 3542 3543 SIMP_ALL_TAC list_ss [LTL_TO_GEN_BUECHI_DS___FAIR_RUN_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 3544 IS_TRANSITION_def, LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 3545 symbolic_semi_automaton_REWRITES, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3546 XP_BIGAND_def, XP_SEM_THM, LTL_SEM_THM, P_SEM_THM, 3547 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 3548 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, XP_SEM___XP_CURRENT, 3549 FORALL_AND_THM, LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def, 3550 LTL_TO_GEN_BUECHI_DS___INITIAL_STATES_def, P_BIGAND_def] THEN 3551 UNDISCH_NO_TAC 3 THEN 3552 UNDISCH_NO_TAC 4 THEN 3553 ONCE_ASM_REWRITE_TAC[] THEN 3554 REPEAT STRIP_TAC THENL [ 3555 Cases_on `t` THEN 3556 ASM_SIMP_TAC arith_ss [] THEN 3557 PROVE_TAC[], 3558 3559 Cases_on `k` THENL [ 3560 ASM_REWRITE_TAC[] THEN 3561 SIMP_TAC arith_ss [], 3562 3563 SIMP_TAC arith_ss [] THEN 3564 METIS_TAC[] 3565 ] 3566 ] 3567 ] 3568 ], 3569 3570 3571 FULL_SIMP_TAC list_ss [XP_USED_VARS_def, XP_USED_CURRENT_VARS_def, 3572 XP_EQUIV_def, XP_IMPL_def, XP_OR_def, XP_USED_X_VARS_def, 3573 XP_CURRENT___XP_USED_VARS, UNION_EMPTY, SUBSET_DEF, IN_UNION, 3574 IN_SING, P_USED_VARS_def, LTL_USED_VARS_def, 3575 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, NOT_IN_EMPTY, 3576 LTL_TO_GEN_BUECHI_DS___IN_USED_STATE_VARS, LIST_BIGUNION_def, 3577 P_USED_VARS_def, P_IMPL_def, P_OR_def] THEN 3578 `(!n. n < DS.SN ==> n < DS.SN + 1) /\ DS.SN < DS.SN + 1` by 3579 DECIDE_TAC THEN 3580 METIS_TAC[] 3581 ]); 3582 3583 3584 3585 3586val LTL_TO_GEN_BUECHI___EXTEND_def = 3587 Define 3588 `(LTL_TO_GEN_BUECHI___EXTEND (LTL_PROP p) b1 b2 DS = ((\sv:num->'a. p:'a prop_logic), 3589 (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(LTL_PROP p, b1, b2, \sv. p)} (P_USED_VARS p)))) /\ 3590 3591 (LTL_TO_GEN_BUECHI___EXTEND (LTL_NOT l) b1 b2 DS = (let 3592 ((pf1', DS1') = (LTL_TO_GEN_BUECHI___EXTEND l b2 b1 DS)) 3593 in 3594 ((\sv. P_NOT (pf1' sv)), 3595 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS1' {(LTL_NOT l, b1, b2, \sv. P_NOT (pf1' sv))} {}))) /\ 3596 3597 (LTL_TO_GEN_BUECHI___EXTEND (LTL_AND (l1, l2)) b1 b2 DS = (let 3598 ((pf1', DS1') = (LTL_TO_GEN_BUECHI___EXTEND l1 b1 b2 DS)) 3599 in 3600 (let 3601 ((pf2', DS2') = (LTL_TO_GEN_BUECHI___EXTEND l2 b1 b2 DS1')) 3602 in 3603 ((\sv. P_AND (pf1' sv, pf2' sv)), 3604 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS2' {(LTL_AND(l1,l2), b1, b2, \sv. P_AND (pf1' sv, pf2' sv))} {})))) /\ 3605 3606 3607 (LTL_TO_GEN_BUECHI___EXTEND (LTL_NEXT l) b1 b2 DS = (let 3608 ((pf1', DS1') = (LTL_TO_GEN_BUECHI___EXTEND l b1 b2 DS)) 3609 in 3610 ((\sv. P_PROP (sv DS1'.SN)), 3611 EXTEND_LTL_TO_GEN_BUECHI_DS DS1' 1 [] {} [\sv. XP_EQUIV(XP_PROP (sv DS1'.SN), XP_NEXT (pf1' sv))] [] { 3612 (LTL_NEXT l, b1, b2, \sv. P_PROP(sv DS1'.SN))}))) /\ 3613 3614 (LTL_TO_GEN_BUECHI___EXTEND (LTL_PSNEXT l) b1 b2 DS = (let 3615 ((pf1', DS1') = (LTL_TO_GEN_BUECHI___EXTEND l b1 b2 DS)) 3616 in 3617 ((\sv. P_PROP (sv DS1'.SN)), 3618 EXTEND_LTL_TO_GEN_BUECHI_DS DS1' 1 [(DS1'.SN, F)] {} [\sv. XP_EQUIV(XP_NEXT_PROP (sv DS1'.SN), XP_CURRENT (pf1' sv))] [] { 3619 (LTL_PSNEXT l, b1, b2, \sv. P_PROP(sv DS1'.SN))}))) /\ 3620 3621 3622 (LTL_TO_GEN_BUECHI___EXTEND (LTL_SUNTIL (l1, l2)) b1 b2 DS = (let 3623 ((pf1', DS1') = (LTL_TO_GEN_BUECHI___EXTEND l1 b1 b2 DS)) 3624 in 3625 (let 3626 ((pf2', DS2') = (LTL_TO_GEN_BUECHI___EXTEND l2 b1 b2 DS1')) 3627 in 3628 ((\sv:num->'a. P_PROP (sv DS2'.SN)), 3629 EXTEND_LTL_TO_GEN_BUECHI_DS (DS2':'a ltl_to_gen_buechi_ds) 1 [] {} 3630 [\sv:num->'a. XP_EQUIV(XP_PROP (sv DS2'.SN), XP_OR(XP_CURRENT (pf2' sv), 3631 XP_AND( 3632 XP_CURRENT (pf1' sv), 3633 XP_NEXT_PROP (sv DS2'.SN))))] 3634 (if b1 then [\sv. P_IMPL(P_PROP(sv DS2'.SN), pf2' sv)] else []) 3635 {(LTL_SUNTIL(l1, l2), b1, b2, \sv. P_PROP(sv DS2'.SN))})))) /\ 3636 3637 3638 (LTL_TO_GEN_BUECHI___EXTEND (LTL_PSUNTIL (l1, l2)) b1 b2 DS = (let 3639 ((pf1', DS1') = (LTL_TO_GEN_BUECHI___EXTEND l1 b1 b2 DS)) 3640 in 3641 (let 3642 ((pf2', DS2') = (LTL_TO_GEN_BUECHI___EXTEND l2 b1 b2 DS1')) 3643 in 3644 ((\sv. (P_OR(pf2' sv, P_AND(pf1' sv, P_PROP(sv DS2'.SN))))), 3645 EXTEND_LTL_TO_GEN_BUECHI_DS DS2' 1 [(DS2'.SN, F)] {} 3646 [\sv. XP_EQUIV(XP_NEXT_PROP (sv DS2'.SN), XP_OR(XP_CURRENT (pf2' sv), 3647 XP_AND( 3648 XP_CURRENT (pf1' sv), 3649 XP_PROP (sv DS2'.SN))))] 3650 [] 3651 {(LTL_PSUNTIL(l1, l2), b1, b2, \sv. (P_OR(pf2' sv, P_AND(pf1' sv, P_PROP(sv DS2'.SN)))))}))))`; 3652 3653 3654 3655val LTL_TO_GEN_BUECHI_def = 3656 Define 3657 `LTL_TO_GEN_BUECHI l b1 b2 = LTL_TO_GEN_BUECHI___EXTEND l b1 b2 (EMPTY_LTL_TO_GEN_BUECHI_DS)`; 3658 3659 3660 3661 3662val LTL_TO_GEN_BUECHI___EXTEND___THM = 3663 store_thm 3664 ("LTL_TO_GEN_BUECHI___EXTEND___THM", 3665 3666``!l b1 b2 DS DS' pf. ((pf, DS') = LTL_TO_GEN_BUECHI___EXTEND l b1 b2 DS) ==> ( 3667 ((l, b1, b2, pf) IN DS'.B /\ (DS.B SUBSET DS'.B) /\ 3668 (LTL_TO_GEN_BUECHI_DS___SEM DS ==> LTL_TO_GEN_BUECHI_DS___SEM DS')))``, 3669 3670 3671 3672ONCE_REWRITE_TAC[GSYM PAIR] THEN 3673REWRITE_TAC[PAIR_EQ] THEN 3674INDUCT_THEN ltl_induct ASSUME_TAC THENL [ 3675 SIMP_TAC list_ss [LTL_TO_GEN_BUECHI___EXTEND_def, 3676 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, IN_UNION, IN_SING, 3677 SUBSET_DEF] THEN 3678 REPEAT STRIP_TAC THEN 3679 METIS_TAC[LTL_TO_GEN_BUECHI_DS___SEM___WEAKEN_BINDING, CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PROP, 3680 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def], 3681 3682 3683 SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, LET_THM, 3684 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3685 REPEAT STRIP_TAC THENL [ 3686 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 3687 3688 REWRITE_TAC [GSYM EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def] THEN 3689 `?y. (x = (~y)) /\ ((~x) = y)` by METIS_TAC[] THEN 3690 ASM_SIMP_TAC std_ss [] THEN 3691 METIS_TAC[CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT] 3692 ], 3693 3694 3695 SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, LET_THM, 3696 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3697 REPEAT STRIP_TAC THENL [ 3698 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 3699 3700 SIMP_ALL_TAC std_ss [GSYM EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def] THEN 3701 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_AND THEN 3702 Q_SPECL_NO_ASSUM 0 [`SND (LTL_TO_GEN_BUECHI___EXTEND l' b1 b2 3703 (SND (LTL_TO_GEN_BUECHI___EXTEND l b1 b2 DS)))`, `b1`, `b2`, `b1`, `b2`] THEN 3704 METIS_TAC[SUBSET_DEF] 3705 ], 3706 3707 3708 3709 SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, LET_THM, 3710 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3711 REPEAT STRIP_TAC THENL [ 3712 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 3713 METIS_TAC[CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NEXT] 3714 ], 3715 3716 3717 SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, LET_THM, 3718 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3719 REPEAT STRIP_TAC THENL [ 3720 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 3721 3722 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL THEN 3723 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b1`, `b2`, `b1`] THEN 3724 3725 Cases_on `b1` THEN ( 3726 SIMP_ALL_TAC std_ss [SUBSET_DEF] THEN 3727 METIS_TAC[] 3728 ) 3729 ], 3730 3731 3732 SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, LET_THM, 3733 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3734 REPEAT STRIP_TAC THENL [ 3735 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 3736 METIS_TAC[CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT, SUBSET_DEF] 3737 ], 3738 3739 3740 SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, LET_THM, 3741 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES] THEN 3742 REPEAT STRIP_TAC THENL [ 3743 PROVE_TAC[SUBSET_UNION, SUBSET_TRANS], 3744 3745 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL THEN 3746 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `b1`, `b2`] THEN 3747 METIS_TAC[SUBSET_DEF] 3748 ] 3749]); 3750 3751 3752 3753 3754val LTL_TO_GEN_BUECHI_THM = 3755 store_thm 3756 ("LTL_TO_GEN_BUECHI_THM", 3757 3758``!l b1 b2. LTL_TO_GEN_BUECHI_DS___SEM (SND (LTL_TO_GEN_BUECHI l b1 b2)) /\ 3759 (l, b1, b2, FST (LTL_TO_GEN_BUECHI l b1 b2)) IN (SND (LTL_TO_GEN_BUECHI l b1 b2)).B``, 3760 3761 REPEAT GEN_TAC THEN 3762 REWRITE_TAC[LTL_TO_GEN_BUECHI_def] THEN 3763 ASSUME_TAC (SPECL [``l:'a ltl``, ``b1:bool``, ``b2:bool``, ``EMPTY_LTL_TO_GEN_BUECHI_DS:'a ltl_to_gen_buechi_ds``] LTL_TO_GEN_BUECHI___EXTEND___THM) THEN 3764 UNDISCH_HD_TAC THEN 3765 ONCE_REWRITE_TAC[GSYM PAIR] THEN 3766 REWRITE_TAC[PAIR_EQ] THEN 3767 SIMP_TAC std_ss [] THEN 3768 METIS_TAC[EMPTY_LTL_TO_GEN_BUECHI_DS___SEM]); 3769 3770 3771 3772val LTL_TO_GEN_BUECHI___EXTEND___IS_LTL_G_F = 3773 store_thm 3774 ("LTL_TO_GEN_BUECHI___EXTEND___IS_LTL_G_F", 3775 3776``!l DS. (IS_LTL_G l ==> ((SND (LTL_TO_GEN_BUECHI___EXTEND l T F DS)).FC = DS.FC)) /\ 3777 (IS_LTL_F l ==> ((SND (LTL_TO_GEN_BUECHI___EXTEND l F T DS)).FC = DS.FC))``, 3778 3779 INDUCT_THEN ltl_induct ASSUME_TAC THEN ( 3780 ASM_SIMP_TAC (list_ss++pairSimps.gen_beta_ss) [IS_LTL_G_def, LTL_TO_GEN_BUECHI___EXTEND_def, 3781 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, LET_THM, 3782 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, ltl_to_gen_buechi_ds_REWRITES] 3783 )); 3784 3785 3786val LTL_TO_GEN_BUECHI___IS_LTL_G_F = 3787 store_thm 3788 ("LTL_TO_GEN_BUECHI___IS_LTL_G_F", 3789 3790``!l. (IS_LTL_G l ==> ((SND (LTL_TO_GEN_BUECHI l T F)).FC = [])) /\ 3791 (IS_LTL_F l ==> ((SND (LTL_TO_GEN_BUECHI l F T)).FC = []))``, 3792 3793 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_def, LTL_TO_GEN_BUECHI___EXTEND___IS_LTL_G_F, 3794 EMPTY_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES]); 3795 3796 3797 3798val LTL_TO_GEN_BUECHI___EXTEND___USED_INPUT_VARS = 3799 store_thm 3800 ("LTL_TO_GEN_BUECHI___EXTEND___USED_INPUT_VARS", 3801 3802``!l b1 b2 DS. (SND (LTL_TO_GEN_BUECHI___EXTEND l b1 b2 DS)).IV = (LTL_USED_VARS l) UNION DS.IV``, 3803 3804 INDUCT_THEN ltl_induct ASSUME_TAC THEN ( 3805 ASM_SIMP_TAC (std_ss++pairSimps.gen_beta_ss) [LTL_TO_GEN_BUECHI___EXTEND_def, 3806 EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, LET_THM, 3807 EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, ltl_to_gen_buechi_ds_REWRITES, 3808 LTL_USED_VARS_def, NOT_IN_EMPTY, EXTENSION, IN_UNION] THEN 3809 REPEAT GEN_TAC THEN REPEAT BOOL_EQ_STRIP_TAC 3810 )); 3811 3812 3813val LTL_TO_GEN_BUECHI___USED_INPUT_VARS = 3814 store_thm 3815 ("LTL_TO_GEN_BUECHI___USED_INPUT_VARS", 3816 3817``!l b1 b2. (SND (LTL_TO_GEN_BUECHI l b1 b2)).IV = (LTL_USED_VARS l)``, 3818 3819 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_def, LTL_TO_GEN_BUECHI___EXTEND___USED_INPUT_VARS, 3820 EMPTY_LTL_TO_GEN_BUECHI_DS_def, ltl_to_gen_buechi_ds_REWRITES, UNION_EMPTY]); 3821 3822 3823 3824 3825(*Derived construction rules for operators defined as 3826 syntactic sugar*) 3827 3828 3829val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE = 3830 store_thm 3831 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_BEFORE", 3832 3833 ``!b11 b12 b21 b22 a DS DS' l1 l2 pf1 pf2. 3834 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [] {} 3835 [\sv. XP_EQUIV(XP_PROP (sv DS.SN), XP_OR(XP_CURRENT (pf2 sv), 3836 XP_AND( 3837 XP_CURRENT (P_NOT (pf1 sv)), 3838 XP_NEXT_PROP (sv DS.SN))))] 3839 (if ~(b12 /\ b21 /\ a) then [] else [\sv. P_IMPL(P_PROP(sv DS.SN), pf2 sv)]) 3840 {(LTL_BEFORE(l1, l2), b11 /\ b22, b12 /\ b21 /\ a, \sv. P_NOT (P_PROP(sv DS.SN)))}) ==> 3841 3842 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, b11, b12, pf1) IN DS.B /\ (l2, b21, b22, pf2) IN DS.B) ==> 3843 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 3844 3845 REWRITE_TAC [LTL_BEFORE_def] THEN 3846 REPEAT STRIP_TAC THEN 3847 3848 (*Negation of l1*) 3849 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT THEN 3850 Q_SPECL_NO_ASSUM 0 [`b11`, `b12`, `DS`, `l1`, `pf1`] THEN 3851 UNDISCH_HD_TAC THEN 3852 `?DS1. (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS 3853 {(LTL_NOT l1,b12, b11,(\sv. P_NOT (pf1 sv)))} {}) = DS1` by METIS_TAC[] THEN 3854 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN 3855 SUBGOAL_TAC `(LTL_NOT l1, b12, b11, (\sv. P_NOT (pf1 sv))) IN DS1.B /\ 3856 (l2,b21,b22,pf2) IN DS1.B` THEN1 ( 3857 GSYM_NO_TAC 1 THEN 3858 ASM_SIMP_TAC std_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES, 3859 IN_UNION, IN_SING] 3860 ) THEN 3861 3862 3863 (*SUNTIL*) 3864 ASSUME_TAC (SIMP_RULE std_ss [] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_SUNTIL) THEN 3865 Q_SPECL_NO_ASSUM 0 [`b12`,`b11`,`b21`, `b22`, `a`, `DS1`, `LTL_NOT l1`, `l2`, `(\sv. P_NOT (pf1 sv))`, `pf2`] THEN 3866 UNDISCH_HD_TAC THEN 3867 `?DS2. (EXTEND_LTL_TO_GEN_BUECHI_DS DS1 1 [] {} 3868 [(\sv. 3869 XP_EQUIV 3870 (XP_PROP (sv DS1.SN), 3871 XP_OR 3872 (XP_CURRENT (pf2 sv), 3873 XP_AND 3874 (XP_CURRENT ((\sv. P_NOT (pf1 sv)) sv), 3875 XP_NEXT_PROP (sv DS1.SN)))))] 3876 (if b12 /\ b21 /\ a then [(\sv. P_IMPL (P_PROP (sv DS1.SN),pf2 sv))] else []) 3877 {(LTL_SUNTIL (LTL_NOT l1,l2),b12 /\ b21 /\ a, b11 /\ b22,(\sv. P_PROP (sv DS1.SN)))}) = DS2` by METIS_TAC[] THEN 3878 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN 3879 SUBGOAL_TAC `(LTL_SUNTIL (LTL_NOT l1,l2), b12 /\ b21 /\ a, b11 /\ b22, (\sv. P_PROP (sv DS1.SN))) IN DS2.B` THEN1 ( 3880 GSYM_NO_TAC 1 THEN 3881 ASM_SIMP_TAC std_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3882 IN_UNION, IN_SING] 3883 ) THEN 3884 `?pf. pf = (\(sv :num -> 'a). 3885 P_PROP (sv (DS1 :'a ltl_to_gen_buechi_ds).SN))` by METIS_TAC[] THEN 3886 3887 (*NOT*) 3888 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT THEN 3889 Q_SPECL_NO_ASSUM 0 [`b12 /\ b21 /\ a`, `b11 /\ b22`, `DS2`, `LTL_SUNTIL (LTL_NOT l1,l2)`, `pf`] THEN 3890 UNDISCH_HD_TAC THEN ASM_REWRITE_TAC[] THEN 3891 GSYM_NO_TAC 3 (*Def DS2*) THEN 3892 GSYM_NO_TAC 7 (*Def DS1*) THEN 3893 FULL_SIMP_TAC std_ss [] THEN 3894 REPEAT WEAKEN_HD_TAC THEN 3895 3896 SIMP_TAC list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 3897 EXTEND_LTL_TO_GEN_BUECHI_DS___EXTEND_LTL_TO_GEN_BUECHI_DS, 3898 UNION_EMPTY, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_SING] THEN 3899 3900 (*REMOVE UNNECESSARY BINDINGS*) 3901 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 3902 REPEAT STRIP_TAC THEN 3903 FULL_SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, SUBSET_DEF, IN_UNION, 3904 IN_SING, IN_INSERT, DISJ_IMP_THM] THEN 3905 METIS_TAC[]); 3906 3907 3908 3909 3910val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE = 3911 store_thm 3912 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PBEFORE", 3913 3914 ``!b11 b12 b21 b22 DS DS' l1 l2 pf1 pf2. 3915 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [(DS.SN,F)] {} 3916 [\sv. XP_EQUIV(XP_NEXT_PROP (sv DS.SN), XP_OR(XP_CURRENT (pf2 sv), 3917 XP_AND( 3918 XP_CURRENT (P_NOT (pf1 sv)), 3919 XP_PROP (sv DS.SN))))] 3920 [] 3921 {(LTL_PBEFORE(l1, l2), b11 /\ b22, b12 /\ b21, (\sv. 3922 P_NOT 3923 (P_OR (pf2 sv,P_AND (P_NOT (pf1 sv),P_PROP (sv DS.SN))))))}) ==> 3924 3925 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, b11, b12, pf1) IN DS.B /\ (l2, b21, b22, pf2) IN DS.B) ==> 3926 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 3927 3928 REWRITE_TAC [LTL_PBEFORE_def] THEN 3929 REPEAT STRIP_TAC THEN 3930 3931 (*Negation of l1*) 3932 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT THEN 3933 Q_SPECL_NO_ASSUM 0 [`b11`, `b12`, `DS`, `l1`, `pf1`] THEN 3934 UNDISCH_HD_TAC THEN 3935 `?DS1. (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS 3936 {(LTL_NOT l1,b12, b11,(\sv. P_NOT (pf1 sv)))} {}) = DS1` by METIS_TAC[] THEN 3937 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN 3938 SUBGOAL_TAC `(LTL_NOT l1, b12, b11, (\sv. P_NOT (pf1 sv))) IN DS1.B /\ 3939 (l2,b21,b22,pf2) IN DS1.B` THEN1 ( 3940 GSYM_NO_TAC 1 THEN 3941 ASM_SIMP_TAC std_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES, 3942 IN_UNION, IN_SING] 3943 ) THEN 3944 3945 3946 (*PSUNTIL*) 3947 ASSUME_TAC (SIMP_RULE std_ss [] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSUNTIL) THEN 3948 Q_SPECL_NO_ASSUM 0 [`b12`, `b11`, `b21`, `b22`, `DS1`, `LTL_NOT l1`, `l2`, `(\sv. P_NOT (pf1 sv))`, `pf2`] THEN 3949 UNDISCH_HD_TAC THEN 3950 `?DS2. (EXTEND_LTL_TO_GEN_BUECHI_DS DS1 1 [(DS1.SN,F)] {} 3951 [(\sv. 3952 XP_EQUIV 3953 (XP_NEXT_PROP (sv DS1.SN), 3954 XP_OR 3955 (XP_CURRENT (pf2 sv), 3956 XP_AND 3957 (XP_CURRENT ((\sv. P_NOT (pf1 sv)) sv), 3958 XP_PROP (sv DS1.SN)))))] 3959 [] 3960 {(LTL_PSUNTIL (LTL_NOT l1,l2),b12 /\ b21,b11 /\ b22,(\sv. P_OR(pf2 sv, P_AND(P_NOT (pf1 sv), P_PROP (sv DS1.SN)))))}) = DS2` by METIS_TAC[] THEN 3961 FULL_SIMP_TAC std_ss [] THEN STRIP_TAC THEN 3962 SUBGOAL_TAC `(LTL_PSUNTIL (LTL_NOT l1,l2),b12 /\ b21, b11 /\ b22, (\sv. 3963 P_OR 3964 (pf2 sv,P_AND (P_NOT (pf1 sv),P_PROP (sv DS1.SN))))) IN DS2.B` THEN1 ( 3965 GSYM_NO_TAC 1 THEN 3966 ASM_SIMP_TAC std_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 3967 IN_UNION, IN_SING] 3968 ) THEN 3969 `?pf. pf = (\(sv:num -> 'a). 3970 P_OR 3971 (pf2 sv,P_AND (P_NOT (pf1 sv),P_PROP (sv (DS1:'a ltl_to_gen_buechi_ds).SN))))` by METIS_TAC[] THEN 3972 3973 (*NOT*) 3974 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT THEN 3975 Q_SPECL_NO_ASSUM 0 [`b12 /\ b21`, `b11 /\ b22`, `DS2`, `LTL_PSUNTIL (LTL_NOT l1,l2)`, `pf`] THEN 3976 UNDISCH_HD_TAC THEN 3977 GSYM_NO_TAC 3 (*Def DS2*) THEN 3978 GSYM_NO_TAC 7 (*Def DS1*) THEN 3979 FULL_SIMP_TAC std_ss [] THEN 3980 REPEAT WEAKEN_HD_TAC THEN 3981 3982 SIMP_TAC list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 3983 EXTEND_LTL_TO_GEN_BUECHI_DS___EXTEND_LTL_TO_GEN_BUECHI_DS, 3984 UNION_EMPTY, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_SING] THEN 3985 3986 (*REMOVE UNNECESSARY BINDINGS*) 3987 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 3988 REPEAT STRIP_TAC THEN 3989 FULL_SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, SUBSET_DEF, IN_UNION, 3990 IN_SING, IN_INSERT, DISJ_IMP_THM]); 3991 3992 3993 3994 3995val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT = 3996 store_thm 3997 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PNEXT", 3998 3999 ``!b1 b2 DS DS' l pf. 4000 (DS' = EXTEND_LTL_TO_GEN_BUECHI_DS DS 1 [(DS.SN,F)] {} 4001 [(\sv. XP_EQUIV 4002 (XP_NEXT_PROP (sv DS.SN),XP_CURRENT (P_NOT (pf sv))))] [] 4003 {(LTL_PNEXT l, b1, b2, (\sv. P_NOT (P_PROP (sv DS.SN))))}) ==> 4004 4005 ((LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l, b1, b2, pf) IN DS.B) ==> 4006 LTL_TO_GEN_BUECHI_DS___SEM DS')``, 4007 4008 REWRITE_TAC [LTL_PNEXT_def] THEN 4009 REPEAT STRIP_TAC THEN 4010 4011 (*Negation of l*) 4012 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT THEN 4013 Q_SPECL_NO_ASSUM 0 [`b1`, `b2`, `DS`, `l`, `pf`] THEN 4014 UNDISCH_HD_TAC THEN 4015 `?DS1. (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS 4016 {(LTL_NOT l,b2,b1,(\sv. P_NOT (pf sv)))} {}) = DS1` by METIS_TAC[] THEN 4017 ASM_REWRITE_TAC [] THEN STRIP_TAC THEN 4018 SUBGOAL_TAC `(LTL_NOT l, b2,b1, (\sv. P_NOT (pf sv))) IN DS1.B` THEN1 ( 4019 GSYM_NO_TAC 1 THEN 4020 ASM_SIMP_TAC std_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___REWRITES, 4021 IN_UNION, IN_SING] 4022 ) THEN 4023 4024 4025 (*PSNEXT*) 4026 ASSUME_TAC (SIMP_RULE std_ss [] CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_PSNEXT) THEN 4027 Q_SPECL_NO_ASSUM 0 [`b2`,`b1`, `DS1`, `LTL_NOT l`, `(\sv. P_NOT (pf sv))`] THEN 4028 UNDISCH_HD_TAC THEN 4029 `?DS2. (EXTEND_LTL_TO_GEN_BUECHI_DS DS1 1 [(DS1.SN,F)] {} 4030 [(\sv. 4031 XP_EQUIV 4032 (XP_NEXT_PROP (sv DS1.SN), 4033 XP_CURRENT ((\sv. P_NOT (pf sv)) sv)))] 4034 [] 4035 {(LTL_PSNEXT (LTL_NOT l),b2,b1,(\sv. P_PROP (sv DS1.SN)))}) = DS2` by METIS_TAC[] THEN 4036 FULL_SIMP_TAC std_ss [] THEN STRIP_TAC THEN 4037 SUBGOAL_TAC `(LTL_PSNEXT (LTL_NOT l),b2,b1, (\sv. 4038 P_PROP (sv DS1.SN))) IN DS2.B` THEN1 ( 4039 GSYM_NO_TAC 1 THEN 4040 ASM_SIMP_TAC std_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, 4041 IN_UNION, IN_SING] 4042 ) THEN 4043 `?pf2. pf2 = (\(sv:num -> 'a). 4044 P_PROP (sv (DS1:'a ltl_to_gen_buechi_ds).SN))` by METIS_TAC[] THEN 4045 4046 (*NOT*) 4047 ASSUME_TAC CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_NOT THEN 4048 Q_SPECL_NO_ASSUM 0 [`b2`,`b1`, `DS2`, `LTL_PSNEXT (LTL_NOT l)`, `pf2`] THEN 4049 UNDISCH_HD_TAC THEN 4050 GSYM_NO_TAC 3 (*Def DS2*) THEN 4051 GSYM_NO_TAC 6 (*Def DS1*) THEN 4052 FULL_SIMP_TAC std_ss [] THEN 4053 REPEAT WEAKEN_HD_TAC THEN 4054 4055 SIMP_TAC list_ss [EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS_def, 4056 EXTEND_LTL_TO_GEN_BUECHI_DS___EXTEND_LTL_TO_GEN_BUECHI_DS, 4057 UNION_EMPTY, EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, UNION_SING] THEN 4058 4059 (*REMOVE UNNECESSARY BINDINGS*) 4060 MATCH_MP_TAC LTL_TO_GEN_BUECHI_DS___SEM___REMOVE_BINDINGS THEN 4061 REPEAT STRIP_TAC THEN 4062 FULL_SIMP_TAC list_ss [EXTEND_LTL_TO_GEN_BUECHI_DS___REWRITES, SUBSET_DEF, IN_UNION, 4063 IN_SING, IN_INSERT, DISJ_IMP_THM]); 4064 4065 4066 4067 4068 4069val LTL_TO_GEN_BUECHI_DS___BINDING_RUN_EQUIV = 4070 store_thm 4071 ("LTL_TO_GEN_BUECHI_DS___BINDING_RUN_EQUIV", 4072 4073 ``!DS i w l1 pf1 l2 pf2 sv. 4074 (LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l1, T, T, pf1) i sv /\ 4075 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (l2, T, T, pf2) i sv) ==> 4076 LTL_TO_GEN_BUECHI_DS___BINDING_RUN DS w (LTL_EQUIV(l1, l2), T, T, (\sv. P_EQUIV(pf1 sv, pf2 sv))) i sv``, 4077 4078 REPEAT GEN_TAC THEN 4079 SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___BINDING_RUN_def, LTL_SEM_THM, 4080 LTL_TO_GEN_BUECHI_DS___MAX_FAIR_RUN_def, 4081 LTL_TO_GEN_BUECHI_DS___MIN_FAIR_RUN_def, P_SEM_THM] THEN 4082 METIS_TAC[]); 4083 4084 4085val CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV = 4086 store_thm 4087 ("CONSTRUCTION_LTL_TO_GEN_BUECHI_DS___CASE_EQUIV", 4088 4089 ``!DS l1 l2 pf1 pf2. 4090 LTL_TO_GEN_BUECHI_DS___SEM DS /\ (l1, T, T, pf1) IN DS.B /\ (l2, T, T, pf2) IN DS.B==> 4091 LTL_TO_GEN_BUECHI_DS___SEM (EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS DS {(LTL_EQUIV(l1,l2), T, T, \sv. P_EQUIV (pf1 sv, pf2 sv))} {})``, 4092 4093 REPEAT STRIP_TAC THEN 4094 MATCH_MP_TAC EXTEND_IV_BINDING_LTL_TO_GEN_BUECHI_DS___SEM THEN 4095 ASM_SIMP_TAC list_ss [UNION_EMPTY, P_USED_VARS_EVAL, LTL_USED_VARS_EVAL, 4096 UNION_SUBSET, IN_SING] THEN 4097 METIS_TAC[LTL_TO_GEN_BUECHI_DS___BINDING_RUN_EQUIV]); 4098 4099 4100val _ = export_theory(); 4101