1open HolKernel Parse boolLib bossLib; 2 3(* 4quietdec := true; 5 6val home_dir = (concat Globals.HOLDIR "/examples/temporal_deep/"); 7loadPath := (concat home_dir "src/deep_embeddings") :: 8 (concat home_dir "src/translations") :: 9 (concat home_dir "src/tools") :: 10 (concat hol_dir "examples/PSL/path") :: 11 (concat hol_dir "examples/PSL/1.1/official-semantics") :: !loadPath; 12 13map load 14 ["full_ltlTheory", "arithmeticTheory", "automaton_formulaTheory", "xprop_logicTheory", "prop_logicTheory", 15 "infinite_pathTheory", "tuerk_tacticsLib", "symbolic_semi_automatonTheory", "listTheory", "pred_setTheory", 16 "pred_setTheory", "rich_listTheory", "set_lemmataTheory", "temporal_deep_mixedTheory", 17 "pairTheory", "symbolic_kripke_structureTheory", 18 "numLib", "semi_automatonTheory", "omega_automatonTheory", 19 "omega_automaton_translationsTheory", "ctl_starTheory", 20 "ltl_to_automaton_formulaTheory", "containerTheory", 21 "psl_to_rltlTheory", "rltl_to_ltlTheory", "temporal_deep_simplificationsLib", "congLib", 22 "kripke_structureTheory"]; 23*) 24 25open full_ltlTheory arithmeticTheory automaton_formulaTheory xprop_logicTheory 26 prop_logicTheory 27 infinite_pathTheory tuerk_tacticsLib symbolic_semi_automatonTheory listTheory pred_setTheory 28 pred_setTheory rich_listTheory set_lemmataTheory temporal_deep_mixedTheory pairTheory symbolic_kripke_structureTheory 29 numLib semi_automatonTheory omega_automatonTheory 30 omega_automaton_translationsTheory ctl_starTheory 31 ltl_to_automaton_formulaTheory containerTheory 32 psl_to_rltlTheory rltl_to_ltlTheory temporal_deep_simplificationsLib congLib kripke_structureTheory; 33open Sanity; 34 35val _ = hide "K"; 36val _ = hide "S"; 37val _ = hide "I"; 38 39 40(* 41show_assums := false; 42show_assums := true; 43show_types := true; 44show_types := false; 45quietdec := false; 46*) 47 48 49val _ = new_theory "ibm"; 50 51 52val A_UNIV___LTL_KS_SEM___CONCRETE_THM = 53 store_thm ( 54 "A_UNIV___LTL_KS_SEM___CONCRETE_THM", 55 ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==> 56 (!i w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> 57 58 (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = 59 LTL_SEM (INPUT_RUN_PATH_UNION A i w) (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))))``, 60 61 62 REPEAT STRIP_TAC THEN 63 SIMP_TAC std_ss [A_SEM_THM, 64 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH] THEN 65 `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by 66 PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN 67 SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 68 WEAKEN_HD_TAC THEN 69 `(!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> 70 ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) = 71 ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN 72 ASM_SIMP_TAC std_ss [LTL_SEM_THM, ACCEPT_COND_TO_LTL_THM] THEN 73 74 MATCH_MP_TAC (prove (``(A = C) ==> ((B = A) = (B = C))``, PROVE_TAC[])) THEN 75 76 ONCE_REWRITE_TAC[LTL_USED_VARS_INTER_THM] THEN 77 AP_THM_TAC THEN AP_TERM_TAC THEN 78 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN GEN_TAC THEN 79 UNDISCH_NO_TAC 3 (*DISJOINT A.S (LTL_USED_VARS l)*) THEN 80 `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 81 UNDISCH_HD_TAC THEN 82 REPEAT WEAKEN_HD_TAC THEN 83 SIMP_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, DISJOINT_DISJ_THM, 84 INPUT_RUN_PATH_UNION_def, EXTENSION, INPUT_RUN_STATE_UNION_def, 85 IN_UNION, IN_INTER, IN_DIFF, PATH_SUBSET_def, SUBSET_DEF] THEN 86 METIS_TAC[] 87); 88 89 90 91 92val A_UNIV___A_SEM___CONCRETE_THM = 93 store_thm ( 94 "A_UNIV___A_SEM___CONCRETE_THM", 95 ``!A ac (l:'a ltl). (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l) /\ FINITE A.S /\ INFINITE (UNIV:'a set)) ==> 96 97 (?A' fc p. FINITE A'.S /\ 98 (!i. 99 (((A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = LTL_SEM i l) = 100 (A_SEM i (A_UNIV (A', 101 A_IMPL(A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc), 102 ACCEPT_COND_PROP p))))))))``, 103 104 105 REPEAT STRIP_TAC THEN 106 ASSUME_TAC A_UNIV___LTL_KS_SEM___CONCRETE_THM THEN 107 Q_SPECL_NO_ASSUM 0 [`A`, `ac`, `l`] THEN 108 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 109 ASM_SIMP_TAC std_ss [] THEN 110 111 `?pf DS. (pf, DS) = LTL_TO_GEN_BUECHI (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)) F T` by METIS_TAC[PAIR] THEN 112 113 `?UV. UV = (P_USED_VARS A.S0 UNION XP_USED_VARS A.R UNION 114 (ACCEPT_COND_USED_VARS ac) UNION LTL_USED_VARS l UNION A.S)` by METIS_TAC[] THEN 115 SUBGOAL_TAC `DS.IV SUBSET UV` THEN1 ( 116 `DS.IV = LTL_USED_VARS (LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l))` by METIS_TAC[LTL_TO_GEN_BUECHI___USED_INPUT_VARS, SND] THEN 117 ASM_SIMP_TAC std_ss [SUBSET_DEF, LTL_USED_VARS_EVAL, 118 LTL_USED_VARS___ACCEPT_COND_TO_LTL, DISJOINT_DISJ_THM, 119 IN_UNION] THEN 120 PROVE_TAC[] 121 ) THEN 122 123 SUBGOAL_TAC `FINITE UV` THEN1 ( 124 ASM_SIMP_TAC std_ss [FINITE_UNION, 125 FINITE___P_USED_VARS, FINITE___XP_USED_VARS, FINITE___LTL_USED_VARS, 126 FINITE___ACCEPT_COND_USED_VARS] 127 ) THEN 128 `?sv. IS_ELEMENT_ITERATOR sv DS.SN UV` by METIS_TAC[IS_ELEMENT_ITERATOR_EXISTS] THEN 129 130 ASSUME_TAC LTL_TO_GEN_BUECHI_DS___SEM___MIN THEN 131 Q_SPECL_NO_ASSUM 0 [`DS`, `LTL_EQUIV (ACCEPT_COND_TO_LTL ac,l)`, `pf`, `sv`, `F`] THEN 132 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 133 REPEAT STRIP_TAC THENL [ 134 ASM_SIMP_TAC std_ss [LTL_TO_GEN_BUECHI_DS___IS_ELEMENT_ITERATOR_def] THEN 135 PROVE_TAC[IS_ELEMENT_ITERATOR_SUBSET], 136 137 METIS_TAC[LTL_TO_GEN_BUECHI_THM, SND, FST], 138 METIS_TAC[LTL_TO_GEN_BUECHI_THM, SND, FST] 139 ] 140 ) THEN 141 FULL_SIMP_TAC std_ss [] THEN 142 WEAKEN_HD_TAC THEN 143 144 145 SIMP_ALL_TAC std_ss [LTL_TO_GEN_BUECHI_DS___A_UNIV_def, 146 LTL_TO_GEN_BUECHI_DS___FAIRNESS_CONSTRAINTS_def] THEN 147 Q.ABBREV_TAC `B = (LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON DS sv)` THEN 148 Q_TAC EXISTS_TAC `PRODUCT_SEMI_AUTOMATON A B` THEN 149 Q_TAC EXISTS_TAC `MAP (\x. x sv) DS.FC` THEN 150 Q_TAC EXISTS_TAC `pf sv` THEN 151 REPEAT STRIP_TAC THENL [ 152 Q.UNABBREV_TAC `B` THEN 153 ASM_SIMP_TAC std_ss [PRODUCT_SEMI_AUTOMATON_REWRITES, FINITE_UNION, 154 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, symbolic_semi_automaton_REWRITES, LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS___FINITE], 155 156 157 `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by 158 PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN 159 SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 160 Q_SPECL_NO_ASSUM 8 [`i`, `w`] THEN 161 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 162 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 163 164 SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF] THEN 165 166 ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (GSYM TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_PRODUCT_THM)) THEN 167 Q_SPECL_NO_ASSUM 0 [`A`, `B`, `i`, `w`] THEN 168 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 169 Q.UNABBREV_TAC `B` THEN 170 ASM_SIMP_TAC std_ss [DISJOINT_DISJ_THM, 171 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, 172 LTL_TO_GEN_BUECHI_DS___SEMI_AUTOMATON_def, 173 symbolic_semi_automaton_REWRITES, 174 LTL_TO_GEN_BUECHI_DS___USED_STATE_VARS_def, 175 IN_ABS] THEN 176 SIMP_ALL_TAC std_ss [IS_ELEMENT_ITERATOR_def] THEN 177 GEN_TAC THEN 178 RIGHT_DISJ_TAC THEN 179 SIMP_ALL_TAC std_ss [] THEN 180 `~(x IN UV)` by METIS_TAC[] THEN 181 UNDISCH_HD_TAC THEN 182 ASM_SIMP_TAC std_ss [IN_UNION] 183 ) THEN 184 ASM_SIMP_TAC std_ss [] 185 ] 186); 187 188 189 190 191 192 193 194 195val IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS = 196 store_thm ( 197 "IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS", 198 199``!A p (l:'a ltl). INFINITE (UNIV:'a set) /\ FINITE A.S ==> 200 201((!K. (A_KS_SEM K (A_UNIV (A, ACCEPT_COND_G p)) = LTL_KS_SEM K l)) = 202(!i. A_SEM i (A_UNIV (A, ACCEPT_COND_G p)) = LTL_SEM i l))``, 203 204 205REPEAT STRIP_TAC THEN EQ_TAC THENL [ 206 ALL_TAC, 207 SIMP_TAC std_ss [A_KS_SEM_def, LTL_KS_SEM_def] 208] THEN 209 210REPEAT STRIP_TAC THEN 211CCONTR_TAC THEN 212REMAINS_TAC `?i'. IS_ULTIMATIVELY_PERIODIC_PATH i' /\ 213 ~(A_SEM i' (A_UNIV (A,ACCEPT_COND_G p)) = LTL_SEM i' l)` THEN1 ( 214 215 `?V. V = SEMI_AUTOMATON_USED_INPUT_VARS A UNION (P_USED_VARS p DIFF A.S) UNION LTL_USED_VARS l` by METIS_TAC[] THEN 216 217 ASSUME_TAC ULTIMALTIVELY_PERIODIC_PATH_CORRESPONDING_TO_UNIQUE_PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURES THEN 218 Q_SPECL_NO_ASSUM 0 [`i'`, `V`] THEN 219 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 220 ASM_SIMP_TAC std_ss [FINITE_UNION, 221 FINITE___LTL_USED_VARS, 222 FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, 223 FINITE___P_USED_VARS, FINITE_DIFF] 224 ) THEN 225 CLEAN_ASSUMPTIONS_TAC THEN 226 227 SUBGOAL_TAC `!i. LTL_SEM i l = LTL_SEM (PATH_RESTRICT i V) l` THEN1 ( 228 SIMP_TAC std_ss [LTL_SEM_def] THEN 229 METIS_TAC[LTL_USED_VARS_INTER_SUBSET_THM, SUBSET_UNION] 230 ) THEN 231 232 SUBGOAL_TAC `!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = A_SEM (PATH_RESTRICT i V) (A_UNIV (A,ACCEPT_COND_G p))` THEN1 ( 233 MATCH_MP_TAC A_USED_INPUT_VARS_INTER_SUBSET_THM THEN 234 ASM_SIMP_TAC std_ss [A_USED_INPUT_VARS_def, A_UNIV_def, 235 ACCEPT_COND_G_def, ACCEPT_COND_USED_VARS_def, SUBSET_DEF, 236 IN_UNION] 237 ) THEN 238 239 Q_SPEC_NO_ASSUM 8 `M` THEN 240 UNDISCH_HD_TAC THEN 241 SIMP_TAC std_ss [A_KS_SEM_def, LTL_KS_SEM_def] THEN 242 METIS_TAC[] 243) THEN 244WEAKEN_NO_TAC 1 (*clean up LTL_KS_SEM M ...*) THEN 245 246ASSUME_TAC SYMBOLIC___UNIV_G___TO___DET_GF___EXISTS_THM THEN 247Q_SPECL_NO_ASSUM 0 [`LTL_USED_VARS l`, `A`, `p`] THEN 248PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[FINITE___LTL_USED_VARS] THEN 249CLEAN_ASSUMPTIONS_TAC THEN 250FULL_SIMP_TAC std_ss [ACCEPT_COND_GF_def] THEN 251WEAKEN_NO_TAC 4 THEN 252 253 254ASSUME_TAC A_UNIV___A_SEM___CONCRETE_THM THEN 255Q_SPECL_NO_ASSUM 0 [`A'`, `ACCEPT_G (ACCEPT_F (ACCEPT_PROP p'))`, `l`] THEN 256PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 257 258FULL_SIMP_TAC std_ss [] THEN 259FULL_SIMP_TAC std_ss [] THEN 260WEAKEN_HD_TAC THEN 261 262SUBGOAL_TAC `?B fc' p'. FINITE B.S /\ 263 IS_SIMPLE_SYMBOLIC_SEMI_AUTOMATON B /\ 264 (!i. A_SEM i 265 (A_UNIV 266 (A'', 267 A_IMPL 268 (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc), 269 ACCEPT_COND_PROP p))) = 270 A_SEM i 271 (A_UNIV 272 (B, 273 A_IMPL 274 (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc'), 275 ACCEPT_COND_PROP p'))))` THEN1 ( 276 277 278 SUBGOAL_TAC `!i A fc p. A_SEM i (A_UNIV (A, A_IMPL 279 (A_BIGAND (MAP (\x. ACCEPT_COND_GF x) fc), 280 ACCEPT_COND_PROP p))) = 281 A_SEM i (A_UNIV (A, ACCEPT_COND (ACCEPT_IMPL 282 (ACCEPT_BIGAND (MAP (\x. ACCEPT_G (ACCEPT_F (ACCEPT_PROP x))) fc), 283 ACCEPT_PROP p))))` THEN1 ( 284 ASM_SIMP_TAC std_ss [A_SEM_THM, A_BIGAND_SEM, MEM_MAP, 285 GSYM LEFT_FORALL_IMP_THM, ACCEPT_COND_GF_def, A_SEM_def, 286 ACCEPT_COND_SEM_def, ACCEPT_COND_PROP_def, 287 ACCEPT_IMPL_def, ACCEPT_OR_def, ACCEPT_COND_SEM_TIME_def, 288 ACCEPT_BIGAND_SEM] THEN 289 METIS_TAC[] 290 ) THEN 291 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 292 293 Q.ABBREV_TAC `ac = (ACCEPT_IMPL 294 (ACCEPT_BIGAND 295 (MAP (\x. ACCEPT_G (ACCEPT_F (ACCEPT_PROP x))) 296 fc),ACCEPT_PROP p))` THEN 297 SUBGOAL_TAC `?f. INJ f (SEMI_AUTOMATON_USED_INPUT_VARS A'') UNIV /\ 298 DISJOINT (IMAGE f (SEMI_AUTOMATON_USED_INPUT_VARS A'') ) 299 (SEMI_AUTOMATON_USED_VARS A'' UNION ACCEPT_COND_USED_VARS ac)` THEN1 ( 300 MATCH_MP_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] FINITE_INJ_EXISTS) THEN 301 ASM_SIMP_TAC std_ss [FINITE___SEMI_AUTOMATON_USED_INPUT_VARS, 302 FINITE_UNION, SEMI_AUTOMATON_USED_VARS_def, 303 FINITE___ACCEPT_COND_USED_VARS] 304 ) THEN 305 306 SUBGOAL_TAC `?SA. IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON SA A'' f` THEN1 ( 307 FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, IN_IMAGE, 308 SEMI_AUTOMATON_USED_VARS_def, IN_DIFF, IN_SING, 309 IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def] THEN 310 REPEAT STRIP_TAC THENL [ 311 METIS_TAC[], 312 METIS_TAC[], 313 FULL_SIMP_TAC std_ss [INJ_DEF, IN_UNIV] THEN METIS_TAC[] 314 ] 315 ) THEN 316 317 ASSUME_TAC A_UNIV___SIMPLIFIED_SEMI_AUTOMATON_THM THEN 318 Q_SPECL_NO_ASSUM 0 [`A''`, `SA`, `f`, `ac`] THEN 319 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 320 FULL_SIMP_TAC std_ss [DISJOINT_DISJ_THM, IN_UNION, IN_IMAGE, 321 SEMI_AUTOMATON_USED_VARS_def, IN_DIFF, IN_SING] THEN 322 METIS_TAC[] 323 ) THEN 324 325 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 326 Q.UNABBREV_TAC `ac` THEN 327 SIMP_TAC std_ss [ACCEPT_VAR_RENAMING_def, ACCEPT_IMPL_def, 328 ACCEPT_OR_def, ACCEPT_BIGAND___VAR_RENAMING, MAP_MAP_o, 329 combinTheory.o_DEF, ACCEPT_F_def] THEN 330 Q_TAC EXISTS_TAC `SA` THEN 331 Q_TAC EXISTS_TAC `MAP (P_VAR_RENAMING 332 (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A'' then f x else x))) fc` THEN 333 Q_TAC EXISTS_TAC `P_VAR_RENAMING 334 (\x. (if x IN SEMI_AUTOMATON_USED_INPUT_VARS A'' then f x else x)) p` THEN 335 REPEAT STRIP_TAC THENL [ 336 SIMP_ALL_TAC std_ss [IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON_def] THEN 337 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, 338 FINITE_UNION, IMAGE_FINITE, FINITE___SEMI_AUTOMATON_USED_INPUT_VARS], 339 340 METIS_TAC[IS_SIMPLIFIED_SYMBOLIC_SEMI_AUTOMATON___RUNS], 341 342 SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF] 343 ] 344) THEN 345FULL_SIMP_TAC std_ss [] THEN 346 347(*cleanup*) 348WEAKEN_HD_TAC THEN 349WEAKEN_NO_TAC 2 (*FINITE A''.S*) THEN 350NTAC 4 (WEAKEN_NO_TAC 2) (*A'*) THEN 351WEAKEN_NO_TAC 3 (*A*) THEN 352 353 354FULL_SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_PROP_def, ACCEPT_COND_SEM_def, 355 ACCEPT_COND_SEM_TIME_def, A_BIGAND_SEM, MEM_MAP, 356 GSYM LEFT_FORALL_IMP_THM, ACCEPT_COND_GF_def, ACCEPT_F_def, 357 IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_def, 358 IS_SYMBOLIC_RUN_THROUGH_SIMPLE_SEMI_AUTOMATON_THM] THEN 359 360SUBGOAL_TAC `?e. !n:num. ?m:num. m > n /\ (w m = e)` THEN1 ( 361 ASSUME_TAC (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] (INST_TYPE [alpha |-> alpha --> bool] INF_ELEMENTS_OF_PATH_NOT_EMPTY)) THEN 362 Q_SPECL_NO_ASSUM 0 [`POW B.S`, `w`] THEN 363 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 364 FULL_SIMP_TAC std_ss [PATH_SUBSET_def, IN_POW, FINITE_POW_IFF] 365 ) THEN 366 FULL_SIMP_TAC std_ss [GSYM MEMBER_NOT_EMPTY, 367 INF_ELEMENTS_OF_PATH_def, GSPECIFICATION] THEN 368 METIS_TAC[] 369) THEN 370 371`?n0. w n0 = e` by METIS_TAC[] THEN 372 373SUBGOAL_TAC `?m':num. (m' > n0) /\ 374 (!x. MEM x fc' ==> ?t. n0 <= t /\ t < m' /\ 375 P_SEM (INPUT_RUN_PATH_UNION B i w t) x)` THEN1 ( 376 Induct_on `fc'` THENL [ 377 SIMP_TAC list_ss [] THEN 378 Q_TAC EXISTS_TAC `SUC n0` THEN 379 DECIDE_TAC, 380 381 SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN 382 REPEAT STRIP_TAC THEN 383 PROVE_CONDITION_NO_ASSUM 2 THEN1 ASM_REWRITE_TAC[] THEN 384 Q_SPEC_NO_ASSUM 2 `n0` THEN 385 FULL_SIMP_TAC std_ss [] THEN 386 rename1 `P_SEM (INPUT_RUN_PATH_UNION B i w t2) h` THEN 387 Q_TAC EXISTS_TAC `MAX m' (SUC t2)` THEN 388 389 ASM_SIMP_TAC arith_ss [GREATER_DEF, MAX_LT] THEN 390 REPEAT STRIP_TAC THENL [ 391 Q_TAC EXISTS_TAC `t2` THEN 392 ASM_SIMP_TAC arith_ss [], 393 394 METIS_TAC[] 395 ] 396 ] 397) THEN 398SUBGOAL_TAC `?m. (m + n0) >= m' /\ (w (m + n0) = e)` THEN1 ( 399 Q_SPEC_NO_ASSUM 3 `m'` THEN 400 CLEAN_ASSUMPTIONS_TAC THEN 401 Q_TAC EXISTS_TAC `m - n0` THEN 402 ASM_SIMP_TAC arith_ss [] 403) THEN 404 405Q_TAC EXISTS_TAC `CUT_PATH_PERIODICALLY i n0 m` THEN 406STRIP_TAC THEN1 ( 407 REWRITE_TAC[IS_ULTIMATIVELY_PERIODIC_PATH_def] THEN 408 Q_TAC EXISTS_TAC `n0` THEN 409 Q_TAC EXISTS_TAC `m` THEN 410 ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___IS_ULTIMATIVELY_PERIODIC] 411) THEN 412 413Q_TAC EXISTS_TAC `CUT_PATH_PERIODICALLY w n0 m` THEN 414REPEAT STRIP_TAC THENL [ 415 SIMP_ALL_TAC std_ss [PATH_SUBSET_def, CUT_PATH_PERIODICALLY_def] THEN 416 METIS_TAC[], 417 418 419 FULL_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING, 420 INPUT_RUN_PATH_UNION_def], 421 422 Cases_on `SUC n < m + n0` THEN1 ( 423 ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING] 424 ) THEN 425 ASM_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY_def] THEN 426 Cases_on `m = 1` THEN1 ( 427 ASM_SIMP_TAC std_ss [MOD_1] THEN 428 `m + n0 = SUC n0` by DECIDE_TAC THEN 429 METIS_TAC[] 430 ) THEN 431 SUBGOAL_TAC `(SUC n - n0) MOD m = (1 + (n - n0) MOD m) MOD m` THEN1 ( 432 SUBGOAL_TAC `1 MOD m = 1` THEN1 ( 433 MATCH_RIGHT_EQ_MP_TAC X_MOD_Y_EQ_X THEN 434 DECIDE_TAC 435 ) THEN 436 GSYM_NO_TAC 0 THEN ONCE_ASM_REWRITE_TAC [] THEN WEAKEN_HD_TAC THEN 437 438 ASM_SIMP_TAC arith_ss [MOD_PLUS] THEN 439 AP_THM_TAC THEN AP_TERM_TAC THEN 440 DECIDE_TAC 441 ) THEN 442 ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 443 Q.ABBREV_TAC `r = (n - n0) MOD m` THEN 444 Cases_on `1 + r < m` THENL [ 445 ASM_SIMP_TAC arith_ss [] THEN 446 `n0 + (r + 1) = SUC (n0 + r)` by DECIDE_TAC THEN 447 METIS_TAC[], 448 449 SUBGOAL_TAC `1 + r = m` THEN1 ( 450 `0 < m` by DECIDE_TAC THEN 451 `r < m` by METIS_TAC [DIVISION] THEN 452 DECIDE_TAC 453 ) THEN 454 ASM_SIMP_TAC arith_ss [] THEN 455 456 `SUC (n0 + r) = (m + n0)` by DECIDE_TAC THEN 457 METIS_TAC[] 458 ], 459 460 RES_TAC THEN 461 rename1 `(_ >= t') /\ P_SEM _ p` THEN 462 Q_TAC EXISTS_TAC `m * t' + t` THEN 463 SUBGOAL_TAC `m * t' >= t'` THEN1 ( 464 `m > 0` by DECIDE_TAC THEN UNDISCH_HD_TAC THEN 465 SIMP_TAC arith_ss [GREATER_EQ] 466 ) THEN 467 ASM_SIMP_TAC arith_ss [] THEN WEAKEN_HD_TAC THEN 468 469 SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, CUT_PATH_PERIODICALLY_def] THEN 470 ASM_SIMP_TAC arith_ss [] THEN 471 REMAINS_TAC `(n0 + (t + m * t' - n0) MOD m) = t` THEN1 ( 472 ASM_REWRITE_TAC[] 473 ) THEN 474 `(t + m * t' - n0) = ((t - n0) + m * t')` by DECIDE_TAC THEN 475 ONCE_ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 476 `0 < m` by DECIDE_TAC THEN 477 478 ASSUME_TAC MOD_MULT THEN 479 Q_SPECL_NO_ASSUM 0 [`m`, `t - n0`] THEN 480 PROVE_CONDITION_NO_ASSUM 0 THEN1 FULL_SIMP_TAC arith_ss [] THEN 481 Q_SPEC_NO_ASSUM 0 `t'` THEN 482 UNDISCH_HD_TAC THEN 483 SIMP_TAC std_ss [ADD_SYM, MULT_SYM] THEN 484 DECIDE_TAC, 485 486 487 UNDISCH_HD_TAC THEN 488 FULL_SIMP_TAC arith_ss [CUT_PATH_PERIODICALLY___BEGINNING, 489 INPUT_RUN_PATH_UNION_def] 490]); 491 492 493 494 495 496 497val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___TO___AUTOMATON = 498 store_thm ( 499 "SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___TO___AUTOMATON", 500 501 ``!K A p. (DISJOINT (SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS K) A.S) ==> 502 ((CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A) 503 (CTL_A_ALWAYS (CTL_PROP p))) = 504 A_KS_SEM K (A_UNIV (A, ACCEPT_COND_G p)))``, 505 506 507 SIMP_TAC std_ss [CTL_KS_SEM_def, 508 SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT, 509 symbolic_kripke_structure_REWRITES, CTL_SEM_THM, 510 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, P_SEM_THM, XP_SEM_THM, 511 GSYM RIGHT_FORALL_IMP_THM, 512 A_KS_SEM_def, A_SEM_THM, ACCEPT_COND_G_def, ACCEPT_COND_SEM_def, 513 ACCEPT_COND_SEM_TIME_def, IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 514 IS_TRANSITION_def, GSYM SUBSET_COMPL_DISJOINT, 515 SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, UNION_SUBSET] THEN 516 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 517 rename1 `P_SEM (INPUT_RUN_PATH_UNION A i w t') p` THEN 518 REMAINS_TAC `P_SEM (INPUT_RUN_PATH_UNION A i w 0) K.S0 /\ 519 !n. XP_SEM K.R (INPUT_RUN_STATE_UNION A (i n) (w n), 520 INPUT_RUN_STATE_UNION A (i (SUC n)) (w (SUC n)))` THEN1 ( 521 Q_SPECL_NO_ASSUM 7 [`INPUT_RUN_PATH_UNION A i w`, `t'`] THEN 522 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def] 523 ) THEN 524 SUBGOAL_TAC `!n. (INPUT_RUN_STATE_UNION A (i n) (w n)) INTER (COMPL A.S) = 525 (i n) INTER (COMPL A.S)` THEN1 ( 526 SIMP_ALL_TAC std_ss [INPUT_RUN_STATE_UNION_def, EXTENSION, IN_INTER, IN_COMPL, IN_UNION, IN_DIFF, PATH_SUBSET_def, PATH_MAP_def, SUBSET_DEF] THEN 527 PROVE_TAC[] 528 ) THEN 529 SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN 530 REPEAT STRIP_TAC THENL [ 531 METIS_TAC[P_USED_VARS_INTER_SUBSET_THM], 532 METIS_TAC[XP_USED_VARS_INTER_SUBSET_BOTH_THM] 533 ], 534 535 536 Q_SPECL_NO_ASSUM 3 [`p'`, `PATH_RESTRICT p' A.S`, `k`] THEN 537 SIMP_ALL_TAC std_ss [INPUT_RUN_PATH_UNION_def, PATH_RESTRICT_def, PATH_MAP_def, 538 INPUT_RUN_STATE_UNION___SPLIT, PATH_SUBSET_def, INTER_SUBSET] THEN 539 PROVE_TAC[] 540 ]); 541 542 543val SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___CLEAN_STATE_VARS = 544 store_thm ( 545 "SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT___CLEAN_STATE_VARS", 546 547 ``!K A p. 548 (CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K A) 549 (CTL_A_ALWAYS (CTL_PROP p))) = 550 (CTL_KS_SEM (SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT K (symbolic_semi_automaton EMPTY A.S0 A.R)) 551 (CTL_A_ALWAYS (CTL_PROP p)))``, 552 553 SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE___WITH___SEMI_AUTOMATON___PRODUCT_def, 554 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 555 SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, symbolic_kripke_structure_REWRITES, 556 symbolic_semi_automaton_REWRITES] 557 ); 558 559 560 561val A_KS_SEM___cong = 562 store_thm ( 563 "A_KS_SEM___cong", 564 ``!A1 A2. AUTOMATON_EQUIV A1 A2 ==> !K. (A_KS_SEM K A1 = A_KS_SEM K A2)``, 565 SIMP_TAC std_ss [A_KS_SEM_def, AUTOMATON_EQUIV_def]); 566 567 568 569 570 571val A_UNIV___LTL_KS_SEM___THM = 572 store_thm ( 573 "A_UNIV___LTL_KS_SEM___THM", 574 ``!A ac l. (IS_TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON A /\ DISJOINT A.S (LTL_USED_VARS l)) ==> 575 ((!i. A_SEM i (A_UNIV (A, ACCEPT_COND ac)) = 576 LTL_SEM i l) = 577 LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE A) 578 (LTL_EQUIV (ACCEPT_COND_TO_LTL ac, l)))``, 579 580 581 REPEAT STRIP_TAC THEN 582 SIMP_TAC std_ss [LTL_KS_SEM_def, A_SEM_THM, 583 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE___INITIAL_PATH] THEN 584 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 585 Q_SPEC_NO_ASSUM 1 `p` THEN 586 `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A p w` by 587 PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN 588 SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 589 `LTL_SEM p l = ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A p (PATH_RESTRICT p A.S)) ac` by METIS_TAC[] THEN 590 FULL_SIMP_TAC std_ss [LTL_SEM_THM, ACCEPT_COND_TO_LTL_THM, INPUT_RUN_PATH_UNION___SPLIT], 591 592 `?!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w` by 593 PROVE_TAC[TOTAL_DET_SYMBOLIC_SEMI_AUTOMATON_UNIQUE_RUN] THEN 594 SIMP_ALL_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 595 `(!w. IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A i w ==> 596 ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac) = 597 ACCEPT_COND_SEM (INPUT_RUN_PATH_UNION A i w) ac` by METIS_TAC[] THEN 598 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 599 Q_SPEC_NO_ASSUM 2 `INPUT_RUN_PATH_UNION A i w` THEN 600 SUBGOAL_TAC `IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON A 601 (INPUT_RUN_PATH_UNION A i w) 602 (PATH_RESTRICT (INPUT_RUN_PATH_UNION A i w) A.S)` THEN1 ( 603 UNDISCH_NO_TAC 1 THEN 604 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, 605 INPUT_RUN_PATH_UNION_def, PATH_SUBSET_def, PATH_RESTRICT_def, PATH_MAP_def, 606 INTER_SUBSET, INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def] THEN 607 SUBGOAL_TAC `!n. ((w n UNION (i n DIFF A.S)) INTER A.S UNION 608 (w n UNION (i n DIFF A.S) DIFF A.S)) = 609 (w n UNION (i n DIFF A.S))` THEN1 ( 610 SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, IN_DIFF] THEN 611 METIS_TAC[] 612 ) THEN 613 ASM_SIMP_TAC std_ss [] 614 ) THEN 615 FULL_SIMP_TAC std_ss [LTL_SEM_THM, GSYM ACCEPT_COND_TO_LTL_THM, 616 ACCEPT_COND_SEM_def] THEN 617 ONCE_REWRITE_TAC[LTL_USED_VARS_INTER_THM] THEN 618 AP_THM_TAC THEN AP_TERM_TAC THEN 619 `PATH_SUBSET w A.S` by FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 620 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 621 SIMP_ALL_TAC std_ss [PATH_RESTRICT_def, PATH_MAP_def, EXTENSION, IN_INTER, 622 INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, IN_UNION, IN_DIFF, PATH_SUBSET_def, SUBSET_DEF, GSYM SUBSET_COMPL_DISJOINT, IN_COMPL] THEN 623 METIS_TAC[] 624 ]); 625 626 627 628 629 630 631 632val PROBLEM_TO_LTL_KS_SEM = 633 store_thm ("PROBLEM_TO_LTL_KS_SEM", 634 ``!A p psl i0 s0 f f'. (F_CLOCK_SERE_FREE psl /\ 635 ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION 636 F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ 637 (A.S = (INTERVAL_SET (SUC i0) s0)) /\ 638 (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ 639 (i0 <= s0) /\ 640 (f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)))) /\ 641 (f' = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)) + 2**(SUC(s0-i0))))) ==> 642 643 644 ((LTL_KS_SEM 645 (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE 646 (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON 647 (symbolic_semi_automaton (INTERVAL_SET (SUC i0) (SUC s0)) 648 (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0)) 649 (XP_AND 650 (XP_EQUIV 651 (XP_NEXT_PROP (SUC s0), 652 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R))) 653 f f' (P_PROP (SUC s0)))) 654 (LTL_EQUIV (LTL_ALWAYS (LTL_EVENTUAL 655 (LTL_PROP (P_NOT (P_BIGOR (SET_TO_LIST 656 (IMAGE (\s. P_PROP (f' s)) 657 (POW (INTERVAL_SET (SUC i0) (SUC s0))))))))), 658 PSL_TO_LTL psl)) 659 660 ) = 661 662 (!K. 663 ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = 664 UF_KS_SEM K psl)))``, 665 666 667 668REPEAT STRIP_TAC THEN 669ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_KS_SEM] THEN 670 671ASSUME_TAC (INST_TYPE [alpha |-> num] IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS) THEN 672Q_SPECL_NO_ASSUM 0 [`A`, `p`, `(PSL_TO_LTL psl)`] THEN 673PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 674 ASM_REWRITE_TAC[FINITE_INTERVAL_SET, 675 INFINITE_UNIV] THEN 676 Q_TAC EXISTS_TAC `SUC` THEN 677 SIMP_TAC arith_ss [] THEN 678 EXISTS_TAC ``0:num`` THEN 679 SIMP_TAC arith_ss [] 680) THEN 681ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 682 683 684SUBGOAL_TAC `!i. A_SEM i (A_UNIV (A,ACCEPT_COND_G p)) = 685 ~A_SEM i (A_NDET (A,ACCEPT_COND_F (P_NOT p)))` THEN1 ( 686 SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_G_def, 687 ACCEPT_COND_F_def, ACCEPT_F_def, 688 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, P_SEM_def] THEN 689 PROVE_TAC[] 690) THEN 691FULL_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 692 693 694ASSUME_TAC (INST_TYPE [alpha |-> num] A_SEM___NDET_F___TO___NDET_FG) THEN 695Q_SPECL_NO_ASSUM 0 [`A`, `P_NOT p`, `SUC s0`] THEN 696PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 697 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, P_USED_VARS_def, 698 IN_UNION, IN_INTERVAL_SET, SUBSET_DEF] THEN 699 `~(SUC s0 <= i0) /\ ~(SUC s0 <= s0)` by DECIDE_TAC THEN 700 PROVE_TAC[] 701) THEN 702SIMP_ALL_TAC std_ss [AUTOMATON_EQUIV_def] THEN 703ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 704 705 706SUBGOAL_TAC `SUC s0 INSERT INTERVAL_SET (SUC i0) s0 = 707 INTERVAL_SET (SUC i0) (SUC s0)` THEN1 ( 708 ONCE_REWRITE_TAC[EXTENSION] THEN GEN_TAC THEN 709 SIMP_TAC std_ss [IN_INTERVAL_SET, IN_INSERT] THEN 710 DECIDE_TAC 711) THEN 712ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 713 714 715 716ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC___NDET_FG___TO___DET_FG___CONCRETE_THM) THEN 717Q_SPECL_NO_ASSUM 0 [`symbolic_semi_automaton ((INTERVAL_SET (SUC i0) (SUC s0))) 718 (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0)) 719 (XP_AND 720 (XP_EQUIV 721 (XP_NEXT_PROP (SUC s0), 722 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R))`, 723 `P_PROP (SUC s0)`, `f`, `f'`] THEN 724SIMP_ALL_TAC std_ss [symbolic_semi_automaton_REWRITES] THEN 725PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 726 SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 ( 727 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, IN_UNION, 728 SUBSET_DEF, IN_INTERVAL_SET] THEN 729 REPEAT STRIP_TAC THEN 730 `x <= i0` by PROVE_TAC[] THEN 731 DECIDE_TAC 732 ) THEN 733 734 SUBGOAL_TAC `(SEMI_AUTOMATON_USED_VARS 735 (symbolic_semi_automaton (INTERVAL_SET (SUC i0) (SUC s0)) 736 (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0)) 737 (XP_AND 738 (XP_EQUIV 739 (XP_NEXT_PROP (SUC s0), 740 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))),A.R)))) SUBSET (INTERVAL_SET 0 (SUC s0))` THEN1 ( 741 SIMP_ALL_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 742 symbolic_semi_automaton_REWRITES, P_USED_VARS_EVAL, XP_USED_VARS_EVAL, SUBSET_DEF, IN_INTERVAL_SET, IN_UNION, IN_SING, IN_INSERT] THEN 743 REPEAT STRIP_TAC THEN ( 744 RES_TAC THEN 745 ASM_SIMP_TAC arith_ss [] 746 ) 747 ) THEN 748 749 REPEAT STRIP_TAC THENL [ 750 REWRITE_TAC[FINITE_INTERVAL_SET], 751 ASM_SIMP_TAC std_ss [P_USED_VARS_def, SUBSET_DEF, IN_INTERVAL_SET, IN_SING], 752 753 ASM_REWRITE_TAC[] THEN 754 MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN 755 ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET], 756 757 758 ASM_REWRITE_TAC[] THEN 759 MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN 760 ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET], 761 762 763 MATCH_MP_TAC DISJOINT_SUBSET THEN 764 Q_TAC EXISTS_TAC `INTERVAL_SET (0) (SUC s0)` THEN 765 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 766 DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN 767 PROVE_TAC[], 768 769 770 771 MATCH_MP_TAC DISJOINT_SUBSET THEN 772 Q_TAC EXISTS_TAC `INTERVAL_SET (0) (SUC s0)` THEN 773 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 774 DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN 775 REPEAT WEAKEN_HD_TAC THEN 776 GEN_TAC THEN 777 RIGHT_DISJ_TAC THEN 778 SIMP_ALL_TAC std_ss [] THEN 779 WEAKEN_NO_TAC 1 THEN 780 DECIDE_TAC, 781 782 783 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 784 DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN 785 REPEAT WEAKEN_HD_TAC THEN 786 GEN_TAC THEN 787 `?a:num. 2 ** SUC (s0 - i0) = a` by PROVE_TAC[] THEN 788 ASM_REWRITE_TAC[] THEN 789 SUBGOAL_TAC `~(a = 0)` THEN1 ( 790 GSYM_NO_TAC 0 THEN 791 ASM_SIMP_TAC std_ss [EXP_EQ_0] 792 ) THEN 793 WEAKEN_NO_TAC 1 THEN 794 DECIDE_TAC 795 ] 796) THEN 797SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN 798ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 799 800 801SUBGOAL_TAC `!A i (p:num prop_logic). ~(A_SEM i (A_NDET (A, ACCEPT_COND_FG p))) = 802 A_SEM i (A_UNIV (A, ACCEPT_COND_GF (P_NOT p)))` THEN1 ( 803 REPEAT WEAKEN_HD_TAC THEN 804 SIMP_TAC std_ss [A_SEM_THM, ACCEPT_COND_GF_def, ACCEPT_COND_SEM_def, 805 ACCEPT_COND_SEM_TIME_def, ACCEPT_COND_FG_def, ACCEPT_F_def, P_SEM_def] THEN 806 METIS_TAC[] 807) THEN 808ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 809 810 811SIMP_TAC std_ss [ACCEPT_COND_GF_def] THEN 812Q.MATCH_ABBREV_TAC `LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE B) l' = 813!i. A_SEM i (A_UNIV (B, ACCEPT_COND ac')) = LTL_SEM i (PSL_TO_LTL psl)` THEN 814 815ASSUME_TAC (INST_TYPE [alpha |-> num] A_UNIV___LTL_KS_SEM___THM) THEN 816Q_SPECL_NO_ASSUM 0 [`B`, `ac'`, `PSL_TO_LTL psl`] THEN 817PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 818 REPEAT STRIP_TAC THENL [ 819 PROVE_TAC[], 820 821 Q.UNABBREV_TAC `B` THEN 822 ASM_SIMP_TAC std_ss [SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 823 symbolic_semi_automaton_REWRITES, 824 SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 825 PSL_TO_LTL_def, 826 RLTL_USED_VARS___PSL_TO_RLTL, 827 LTL_USED_VARS___RLTL_TO_LTL, 828 P_USED_VARS_EVAL, UNION_EMPTY] THEN 829 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET, 830 DISJOINT_DISJ_THM] THEN 831 GEN_TAC THEN 832 LEFT_DISJ_TAC THEN 833 `x <= i0` by PROVE_TAC[] THEN 834 ASM_SIMP_TAC arith_ss [] 835 ] 836) THEN 837 838ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 839Q.UNABBREV_TAC `l'` THEN 840Q.UNABBREV_TAC `ac'` THEN 841 842MATCH_MP_TAC (prove (``LTL_EQUIVALENT l1 l2 ==> (LTL_KS_SEM M l1 = LTL_KS_SEM M l2)``, 843 SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_KS_SEM_def, LTL_SEM_def])) THEN 844SIMP_TAC std_ss [LTL_EQUIVALENT_def, LTL_EQUIV_SEM] THEN 845REPEAT GEN_TAC THEN 846MATCH_MP_TAC (prove (``(A = B) ==> ((A = x) = (B = x))``, PROVE_TAC[])) THEN 847SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def, LTL_SEM_THM, ACCEPT_F_def, P_SEM_def] 848); 849 850 851val PROBLEM_TO_LTL_KS_SEM___TOTAL = 852 store_thm ("PROBLEM_TO_LTL_KS_SEM___TOTAL", 853 ``!A p psl i0 s0 f. (F_CLOCK_SERE_FREE psl /\ 854 IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ 855 ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION 856 F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ 857 (A.S = (INTERVAL_SET (SUC i0) s0)) /\ 858 (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ 859 (i0 <= s0) /\ 860 (f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC s0))) ==> 861 862 ((LTL_KS_SEM 863 (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE 864 (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f)) 865 (LTL_EQUIV (LTL_ALWAYS (LTL_PROP ( 866 (P_FORALL (SET_TO_LIST A.S) 867 (P_IMPL (VAR_RENAMING_HASHTABLE A.S f,p))))), 868 PSL_TO_LTL psl)) 869 870 ) = 871 872 (!K. 873 ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = 874 UF_KS_SEM K psl)))``, 875 876 877 878REPEAT STRIP_TAC THEN 879ASM_SIMP_TAC std_ss [PSL_TO_LTL___UF_KS_SEM] THEN 880 881ASSUME_TAC (INST_TYPE [alpha |-> num] IBM_PROBLEM___REDUCTION_TO_SINGLE_PATHS) THEN 882Q_SPECL_NO_ASSUM 0 [`A`, `p`, `(PSL_TO_LTL psl)`] THEN 883PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 884 ASM_REWRITE_TAC[FINITE_INTERVAL_SET, 885 INFINITE_UNIV] THEN 886 Q_TAC EXISTS_TAC `SUC` THEN 887 SIMP_TAC arith_ss [] THEN 888 EXISTS_TAC ``0:num`` THEN 889 SIMP_TAC arith_ss [] 890) THEN 891ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 892 893 894SUBGOAL_TAC `DISJOINT (IMAGE f (POW A.S)) 895 (SEMI_AUTOMATON_USED_VARS A UNION P_USED_VARS p)` THEN1 ( 896 ASM_REWRITE_TAC[DISJOINT_DISJ_THM] THEN 897 Cases_on `i0 = s0` THENL [ 898 SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 ( 899 ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] 900 ) THEN 901 ASM_REWRITE_TAC[IN_IMAGE, IN_POW, 902 SUBSET_EMPTY] THEN 903 904 SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, 905 SET_BINARY_ENCODING_def, 906 IMAGE_EMPTY, 907 SUM_IMAGE_THM] THEN 908 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, 909 SUBSET_DEF, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, 910 NOT_IN_EMPTY] THEN 911 `~(SUC s0 <= s0)` by DECIDE_TAC THEN 912 METIS_TAC[], 913 914 `SUC i0 <= s0` by DECIDE_TAC THEN 915 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 916 DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN 917 FULL_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, IN_UNION, 918 SUBSET_DEF, IN_INTERVAL_SET, SEMI_AUTOMATON_USED_INPUT_VARS_def, IN_DIFF, 919 NOT_IN_EMPTY] THEN 920 GEN_TAC THEN 921 `~(SUC s0 <= s0)` by DECIDE_TAC THEN 922 Cases_on `x <= s0` THEN1 ASM_SIMP_TAC std_ss [] THEN 923 `~(x <= i0)` by DECIDE_TAC THEN 924 METIS_TAC[] 925 ] 926) THEN 927 928ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC___TOTAL_UNIV_G___TO___DET_G___CONCRETE_THM) THEN 929Q_SPECL_NO_ASSUM 0 [`A`, `p`, `f`] THEN 930PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 931 ASM_REWRITE_TAC[FINITE_INTERVAL_SET] THEN 932 MATCH_MP_TAC SET_BINARY_ENCODING_SHIFT___INJ THEN 933 ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET, FINITE_INTERVAL_SET] 934) THEN 935SIMP_ALL_TAC std_ss [FORALL_AND_THM] THEN 936ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 937 938 939 940SIMP_TAC std_ss [ACCEPT_COND_G_def] THEN 941Q.MATCH_ABBREV_TAC `LTL_KS_SEM (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE B) l' = 942!i. A_SEM i (A_UNIV (B, ACCEPT_COND ac')) = LTL_SEM i (PSL_TO_LTL psl)` THEN 943 944ASSUME_TAC (INST_TYPE [alpha |-> num] A_UNIV___LTL_KS_SEM___THM) THEN 945Q_SPECL_NO_ASSUM 0 [`B`, `ac'`, `PSL_TO_LTL psl`] THEN 946PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 947 REPEAT STRIP_TAC THENL [ 948 PROVE_TAC[], 949 950 Q.UNABBREV_TAC `B` THEN 951 ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, 952 symbolic_semi_automaton_REWRITES, 953 PSL_TO_LTL_def, 954 RLTL_USED_VARS___PSL_TO_RLTL, 955 LTL_USED_VARS___RLTL_TO_LTL, 956 P_USED_VARS_EVAL, UNION_EMPTY] THEN 957 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET, 958 DISJOINT_DISJ_THM] THEN 959 GEN_TAC THEN 960 LEFT_DISJ_TAC THEN 961 `x <= i0` by PROVE_TAC[] THEN 962 963 Cases_on `i0 = s0` THENL [ 964 SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 ( 965 ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] 966 ) THEN 967 ASM_REWRITE_TAC[IN_IMAGE, IN_POW, 968 SUBSET_EMPTY] THEN 969 970 SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, 971 SET_BINARY_ENCODING_def, 972 IMAGE_EMPTY, 973 SUM_IMAGE_THM] THEN 974 DECIDE_TAC, 975 976 `SUC i0 <= s0` by DECIDE_TAC THEN 977 ASM_SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, IN_INTERVAL_SET] 978 ] 979 ] 980) THEN 981 982ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 983Q.UNABBREV_TAC `l'` THEN 984Q.UNABBREV_TAC `ac'` THEN 985SIMP_TAC std_ss [ACCEPT_COND_TO_LTL_def] 986); 987 988 989 990 991 992 993 994 995 996 997 998 999 1000val P_EXISTS___SET_TO_LIST___INTERVAL_SET = 1001 store_thm ("P_EXISTS___SET_TO_LIST___INTERVAL_SET", 1002 ``(!n1 n2 p. PROP_LOGIC_EQUIVALENT (P_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (P_EXISTS (INTERVAL_LIST n1 n2) p))``, 1003 1004 SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_EXISTS_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST] 1005 ) 1006 1007val P_FORALL___SET_TO_LIST___INTERVAL_SET = 1008 store_thm ("P_FORALL___SET_TO_LIST___INTERVAL_SET", 1009 ``(!n1 n2 p. PROP_LOGIC_EQUIVALENT (P_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (P_FORALL (INTERVAL_LIST n1 n2) p))``, 1010 1011 SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_FORALL_SEM, SET_TO_LIST_INV, FINITE_INTERVAL_SET, LIST_TO_SET___INTERVAL_LIST] 1012 ) 1013 1014 1015val P_BIGOR___SET_TO_LIST___INTERVAL_SET = 1016 store_thm ("P_BIGOR___SET_TO_LIST___INTERVAL_SET", 1017 ``!n1 n2 f. (PROP_LOGIC_EQUIVALENT 1018 (P_BIGOR (SET_TO_LIST (IMAGE f 1019 (INTERVAL_SET n1 n2)))) 1020 (P_BIGOR (MAP f 1021 (INTERVAL_LIST n1 n2))))``, 1022 1023 REPEAT STRIP_TAC THEN 1024 ASM_SIMP_TAC std_ss [PROP_LOGIC_EQUIVALENT_def, P_BIGOR_SEM, 1025 MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_INTERVAL_LIST, 1026 MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_INTERVAL_SET, 1027 IN_IMAGE, IN_INTERVAL_SET] 1028 ) 1029 1030 1031val XP_BIGOR___SET_TO_LIST___INTERVAL_SET = 1032 store_thm ("XP_BIGOR___SET_TO_LIST___INTERVAL_SET", 1033 ``!n1 n2 f. (XPROP_LOGIC_EQUIVALENT 1034 (XP_BIGOR (SET_TO_LIST (IMAGE f 1035 (INTERVAL_SET n1 n2)))) 1036 (XP_BIGOR (MAP f 1037 (INTERVAL_LIST n1 n2))))``, 1038 1039 REPEAT STRIP_TAC THEN 1040 ASM_SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_BIGOR_SEM, 1041 MEM_MAP, GSYM LEFT_EXISTS_AND_THM, MEM_INTERVAL_LIST, 1042 MEM_SET_TO_LIST, IMAGE_FINITE, FINITE_INTERVAL_SET, 1043 IN_IMAGE, IN_INTERVAL_SET] 1044 ) 1045 1046 1047val XP_NEXT_EXISTS___SET_TO_LIST___INTERVAL_SET = 1048 store_thm ("XP_NEXT_EXISTS___SET_TO_LIST___INTERVAL_SET", 1049 ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_NEXT_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_NEXT_EXISTS (INTERVAL_LIST n1 n2) p)``, 1050 1051 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_NEXT_EXISTS_SEM, 1052 SET_TO_LIST_INV, FINITE_INTERVAL_SET, 1053 LIST_TO_SET___INTERVAL_LIST]); 1054 1055 1056val XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET = 1057 store_thm ("XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET", 1058 ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_CURRENT_EXISTS (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_CURRENT_EXISTS (INTERVAL_LIST n1 n2) p)``, 1059 1060 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_CURRENT_EXISTS_SEM, 1061 SET_TO_LIST_INV, FINITE_INTERVAL_SET, 1062 LIST_TO_SET___INTERVAL_LIST]); 1063 1064 1065val XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET = 1066 store_thm ("XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET", 1067 ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_NEXT_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_NEXT_FORALL (INTERVAL_LIST n1 n2) p)``, 1068 1069 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_NEXT_FORALL_SEM, 1070 SET_TO_LIST_INV, FINITE_INTERVAL_SET, 1071 LIST_TO_SET___INTERVAL_LIST]); 1072 1073 1074val XP_CURRENT_FORALL___SET_TO_LIST___INTERVAL_SET = 1075 store_thm ("XP_CURRENT_FORALL___SET_TO_LIST___INTERVAL_SET", 1076 ``!n1 n2 p. XPROP_LOGIC_EQUIVALENT (XP_CURRENT_FORALL (SET_TO_LIST (INTERVAL_SET n1 n2)) p) (XP_CURRENT_FORALL (INTERVAL_LIST n1 n2) p)``, 1077 1078 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_CURRENT_FORALL_SEM, 1079 SET_TO_LIST_INV, FINITE_INTERVAL_SET, 1080 LIST_TO_SET___INTERVAL_LIST]); 1081 1082 1083 1084 1085val IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong = 1086 store_thm ("IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong", 1087 1088 ``!S0 S0' R R' FC FC'. ( 1089 PROP_LOGIC_EQUIVALENT S0 S0' ==> 1090 XPROP_LOGIC_EQUIVALENT R R' ==> 1091 (FC = FC') ==> 1092 ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) FC) = 1093 (IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0' R') FC')))``, 1094 1095 SIMP_TAC std_ss [IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE_def, 1096 PATHS_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE___REWRITES, 1097 symbolic_kripke_structure_REWRITES, 1098 PROP_LOGIC_EQUIVALENT_def, 1099 XPROP_LOGIC_EQUIVALENT_def]); 1100 1101 1102 1103val ks_congset = 1104 mk_congset ([merge_cs [ 1105 (CSFRAG 1106 {rewrs = [], 1107 relations = [], 1108 dprocs = [], 1109 congs = [IS_EMPTY_FAIR_KRIPKE_STRUCTURE_cong]}), 1110 xprop_logic_CS, prop_logic_CS]]); 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120val XP_COND___XP_NEXT_FORALL___REWRITE = 1121 store_thm ("XP_COND___XP_NEXT_FORALL___REWRITE", 1122 ``!c l p1 p2. DISJOINT (XP_USED_X_VARS c) (LIST_TO_SET l) ==> ( 1123 XPROP_LOGIC_EQUIVALENT (XP_COND (c, XP_NEXT_FORALL l p1, XP_NEXT_FORALL l p2)) (XP_NEXT_FORALL l (XP_COND (c, p1,p2))))``, 1124 1125 REPEAT STRIP_TAC THEN 1126 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_SEM_THM, 1127 XP_NEXT_FORALL_SEM] THEN 1128 REPEAT GEN_TAC THEN 1129 SUBGOAL_TAC `!l'. l' SUBSET LIST_TO_SET l ==> 1130 (XP_SEM c (s1,s2 DIFF LIST_TO_SET l UNION l') = 1131 XP_SEM c (s1,s2))` THEN1 ( 1132 REPEAT STRIP_TAC THEN 1133 ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN 1134 AP_TERM_TAC THEN SIMP_TAC std_ss [] THEN 1135 1136 ONCE_REWRITE_TAC[EXTENSION] THEN 1137 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, IN_INTER, IN_DIFF, 1138 IN_UNION] THEN 1139 PROVE_TAC[] 1140 ) THEN 1141 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 1142 METIS_TAC[]); 1143 1144 1145val XP_COND___XP_CURRENT_EXISTS___REWRITE = 1146 store_thm ("XP_COND___XP_CURRENT_EXISTS___REWRITE", 1147 ``!c l p1 p2. DISJOINT (XP_USED_CURRENT_VARS c) (LIST_TO_SET l) ==> ( 1148 XPROP_LOGIC_EQUIVALENT (XP_COND (c, XP_CURRENT_EXISTS l p1, XP_CURRENT_EXISTS l p2)) (XP_CURRENT_EXISTS l (XP_COND (c, p1,p2))))``, 1149 1150 REPEAT STRIP_TAC THEN 1151 SIMP_TAC std_ss [XPROP_LOGIC_EQUIVALENT_def, XP_SEM_THM, 1152 XP_CURRENT_EXISTS_SEM] THEN 1153 REPEAT GEN_TAC THEN 1154 SUBGOAL_TAC `!l'. l' SUBSET LIST_TO_SET l ==> 1155 (XP_SEM c (s1 DIFF LIST_TO_SET l UNION l', s2) = 1156 XP_SEM c (s1,s2))` THEN1 ( 1157 REPEAT STRIP_TAC THEN 1158 ONCE_REWRITE_TAC[XP_USED_VARS_INTER_THM] THEN 1159 AP_TERM_TAC THEN SIMP_TAC std_ss [] THEN 1160 1161 ONCE_REWRITE_TAC[EXTENSION] THEN 1162 SIMP_ALL_TAC std_ss [DISJOINT_DISJ_THM, SUBSET_DEF, IN_INTER, IN_DIFF, 1163 IN_UNION] THEN 1164 PROVE_TAC[] 1165 ) THEN 1166 METIS_TAC[]); 1167 1168 1169 1170 1171val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def = 1172Define 1173 `(VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING [] n n0 = P_PROP n) /\ 1174 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (e::l) n n0 = 1175 P_OR (P_AND (P_PROP e, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l ((2**(e-n0)) + n) n0), 1176 P_AND (P_NOT (P_PROP e), VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l n n0)))`; 1177 1178val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET = 1179 store_thm ("VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET", 1180 ``!l n n0 m:num d. ((d <= n) /\ (d >= m) /\ (!e. MEM e l ==> e < m)) ==> 1181 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l n n0 = 1182 (P_VAR_RENAMING (\x. if (x >= m) then x + (n-d) else x)) (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING l d n0))``, 1183 1184 Induct_on `l` THENL [ 1185 SIMP_TAC list_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, 1186 P_VAR_RENAMING_EVAL], 1187 1188 SIMP_TAC list_ss [VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, 1189 P_VAR_RENAMING_EVAL, P_OR_def, prop_logic_11] THEN 1190 REPEAT GEN_TAC THEN STRIP_TAC THEN 1191 `h < m` by PROVE_TAC[] THEN 1192 ASM_SIMP_TAC arith_ss [] THEN 1193 REPEAT STRIP_TAC THENL [ 1194 Q_SPECL_NO_ASSUM 4 [`n + (2:num) ** (h - n0)`, `n0`, `m`, `d + (2:num) ** (h - n0)`] THEN 1195 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC arith_ss [] THEN 1196 FULL_SIMP_TAC arith_ss [], 1197 1198 1199 1200 Q_SPECL_NO_ASSUM 4 [`n`, `n0`, `m`, `d`] THEN 1201 PROVE_CONDITION_NO_ASSUM 0 THEN ASM_SIMP_TAC std_ss [] THEN 1202 FULL_SIMP_TAC arith_ss [] 1203 ] 1204 ]); 1205 1206 1207val VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST = 1208 store_thm ("VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST", 1209 ``!n1 n2 n3 n4. (n3 <= n1) ==> (VAR_RENAMING_HASHTABLE_LIST (INTERVAL_LIST n1 n2) {} (SET_BINARY_ENCODING_SHIFT n3 n4) = VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING (INTERVAL_LIST n1 n2) n4 n3)``, 1210 1211 NTAC 2 GEN_TAC THEN 1212 Cases_on `n2 < n1` THENL [ 1213 ASM_SIMP_TAC std_ss [INTERVAL_LIST_THM, VAR_RENAMING_HASHTABLE_LIST_def, VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, 1214 SET_BINARY_ENCODING_SHIFT_def, IMAGE_EMPTY, 1215 SET_BINARY_ENCODING_def, SUM_IMAGE_THM], 1216 1217 Induct_on `n2 - n1` THENL [ 1218 REPEAT STRIP_TAC THEN 1219 `n2 = n1` by DECIDE_TAC THEN 1220 NTAC 2 (WEAKEN_NO_TAC 2) THEN 1221 ASM_SIMP_TAC std_ss [INTERVAL_LIST_THM, 1222 VAR_RENAMING_HASHTABLE_LIST_def, 1223 VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, 1224 SET_BINARY_ENCODING_SHIFT_def, 1225 IMAGE_SING, SET_BINARY_ENCODING_def, 1226 SUM_IMAGE_SING, IMAGE_EMPTY, 1227 SUM_IMAGE_THM], 1228 1229 1230 REPEAT STRIP_TAC THEN 1231 `INTERVAL_LIST n1 n2 = n1::INTERVAL_LIST (SUC n1) n2` by 1232 ASM_SIMP_TAC arith_ss [INTERVAL_LIST_THM] THEN 1233 ASM_SIMP_TAC std_ss [VAR_RENAMING_HASHTABLE_LIST_def, 1234 VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING_def, P_OR_def, 1235 prop_logic_11] THEN 1236 REPEAT STRIP_TAC THENL [ 1237 ONCE_REWRITE_TAC[VAR_RENAMING_HASHTABLE_LIST___CLEAN_VAR_SET] THEN 1238 1239 REMAINS_TAC `!x. (x SUBSET {} UNION (LIST_TO_SET (INTERVAL_LIST (SUC n1) n2))) ==> 1240 ((\x. SET_BINARY_ENCODING_SHIFT n3 n4 (x UNION {n1})) x = SET_BINARY_ENCODING_SHIFT n3 (2**(n1 - n3) + n4) x)` THEN1 ( 1241 1242 ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___FUN_RESTRICT) THEN 1243 1244 Q_SPECL_NO_ASSUM 0 [`INTERVAL_LIST (SUC n1) n2`, `EMPTY:num set`, `\x. SET_BINARY_ENCODING_SHIFT n3 n4 (x UNION {n1})`, `SET_BINARY_ENCODING_SHIFT n3 (2**(n1 - n3) + n4)`] THEN 1245 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 1246 1247 ASM_REWRITE_TAC[] THEN 1248 Q_SPECL_NO_ASSUM 6 [`n2`, `SUC n1`] THEN 1249 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 1250 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 1251 Q_SPECL_NO_ASSUM 0 [`n3`, `(2 ** (n1 - n3) + n4)`] THEN 1252 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 1253 ASM_REWRITE_TAC[] 1254 ) THEN 1255 1256 1257 SIMP_TAC std_ss [UNION_EMPTY, LIST_TO_SET___INTERVAL_LIST] THEN 1258 REPEAT STRIP_TAC THEN 1259 `FINITE x` by PROVE_TAC[FINITE_INTERVAL_SET, SUBSET_FINITE] THEN 1260 SUBGOAL_TAC `~(n1 IN x)` THEN1 ( 1261 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_INTERVAL_SET] THEN 1262 `~(SUC n1 <= n1)` by DECIDE_TAC THEN 1263 PROVE_TAC[] 1264 ) THEN 1265 ASM_SIMP_TAC arith_ss [FUN_EQ_THM, UNION_SING, 1266 SET_BINARY_ENCODING_SHIFT_def, 1267 IMAGE_INSERT, SET_BINARY_ENCODING_def, SUM_IMAGE_THM, 1268 IMAGE_FINITE] THEN 1269 1270 AP_TERM_TAC THEN 1271 SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_DELETE] THEN 1272 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1273 PROVE_TAC[], 1274 PROVE_TAC[], 1275 1276 `~(n1 = n)` by PROVE_TAC[] THEN 1277 `n < n3` by DECIDE_TAC THEN 1278 1279 `n IN INTERVAL_SET (SUC n1) n2` by PROVE_TAC[SUBSET_DEF] THEN 1280 SIMP_ALL_TAC std_ss [IN_INTERVAL_SET] THEN 1281 DECIDE_TAC 1282 ], 1283 1284 1285 1286 Q_SPECL_NO_ASSUM 4 [`n2`, `SUC n1`] THEN 1287 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 1288 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 1289 Q_SPECL_NO_ASSUM 0 [`n3`, `n4`] THEN 1290 PROVE_CONDITION_NO_ASSUM 0 THEN1 DECIDE_TAC THEN 1291 ASM_REWRITE_TAC[] 1292 ] 1293 ] 1294 ]); 1295 1296 1297 1298 1299val PROBLEM_TO_KRIPKE_STRUCTURE = 1300 store_thm ("PROBLEM_TO_KRIPKE_STRUCTURE", 1301 ``!A p psl i0 s0 DS S0 R l' pf sv a. (F_CLOCK_SERE_FREE psl /\ 1302 ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION 1303 F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ 1304 (A.S = (INTERVAL_SET (SUC i0) s0)) /\ 1305 (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ 1306 (i0 <= s0) /\ 1307 (sv = \n:num. 2 * 2**(SUC s0 - i0) + s0 + 3 + n) /\ 1308 LTL_TO_GEN_BUECHI_DS___SEM DS /\ 1309 (l',a,T,pf) IN DS.B /\ 1310 DS.IV SUBSET INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2) /\ 1311 LTL_EQUIVALENT_INITIAL 1312 (LTL_EQUIV 1313 (LTL_ALWAYS 1314 (LTL_EVENTUAL 1315 (LTL_PROP 1316 (P_NOT 1317 (P_BIGOR 1318 (MAP (\p. P_PROP p) 1319 (INTERVAL_LIST 1320 (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 1321 (SUC (SUC s0) + 2 ** SUC (s0 - i0) + 1322 PRE (2 ** SUC (s0 - i0))))))))), PSL_TO_LTL psl)) l' /\ 1323 1324 (PROP_LOGIC_EQUIVALENT (P_AND 1325 (P_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) 1326 (P_EQUIV 1327 (P_AND (P_EQUIV (P_PROP (SUC s0),P_NOT p),A.S0), 1328 VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1329 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) 1330 (SUC i0))), 1331 P_AND 1332 (P_NOT 1333 (P_BIGOR 1334 (MAP P_PROP 1335 (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 1336 (PRE (2 ** SUC (s0 - i0)) + 1337 (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))), 1338 P_AND 1339 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv, 1340 P_NOT (pf sv))))) S0) /\ 1341 1342 (XPROP_LOGIC_EQUIVALENT 1343 (XP_AND 1344 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) 1345 (XP_EQUIV 1346 (XP_NEXT 1347 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1348 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) 1349 (SUC i0)), 1350 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0)) 1351 (XP_AND 1352 (XP_EQUIV 1353 (XP_NEXT_PROP (SUC s0), 1354 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))), 1355 XP_AND 1356 (A.R, 1357 XP_CURRENT 1358 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1359 (INTERVAL_LIST (SUC i0) (SUC s0)) 1360 (SUC (SUC s0)) (SUC i0))))))), 1361 XP_AND 1362 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0)) 1363 (XP_EQUIV 1364 (XP_NEXT 1365 (P_VAR_RENAMING 1366 (\n. 1367 (if n >= SUC (SUC s0) then 1368 n + (2:num) ** SUC (s0 - i0) 1369 else 1370 n)) 1371 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1372 (INTERVAL_LIST (SUC i0) (SUC s0)) 1373 (SUC (SUC s0)) (SUC i0))), 1374 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0)) 1375 (XP_AND 1376 (XP_EQUIV 1377 (XP_NEXT_PROP (SUC s0), 1378 XP_OR (XP_PROP (SUC s0),XP_NEXT (P_NOT p))), 1379 XP_AND 1380 (A.R, 1381 XP_AND 1382 (XP_NEXT (P_PROP (SUC s0)), 1383 XP_COND 1384 (XP_BIGOR 1385 (MAP XP_PROP 1386 (INTERVAL_LIST 1387 (SUC (SUC s0) + 1388 2 ** SUC (s0 - i0)) 1389 (PRE (2 ** SUC (s0 - i0)) + 1390 (SUC (SUC s0) + 1391 2 ** SUC (s0 - i0))))), 1392 XP_CURRENT 1393 (P_VAR_RENAMING 1394 (\n. 1395 (if n >= SUC (SUC s0) then 1396 n + 2 ** SUC (s0 - i0) 1397 else 1398 n)) 1399 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1400 (INTERVAL_LIST (SUC i0) 1401 (SUC s0)) (SUC (SUC s0)) 1402 (SUC i0))), 1403 XP_CURRENT 1404 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1405 (INTERVAL_LIST (SUC i0) (SUC s0)) 1406 (SUC (SUC s0)) (SUC i0))))))))), 1407 XP_BIGAND (MAP (\xp. xp sv) DS.R)))) R) 1408 ) ==> 1409 1410 ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 1411 (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC)) 1412 = 1413 1414 (!K. 1415 ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = 1416 UF_KS_SEM K psl)))``, 1417 1418 1419REPEAT STRIP_TAC THEN 1420 1421`?f. f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)))` by METIS_TAC[] THEN 1422`?f'. f' = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC (SUC (s0)) + 2**(SUC(s0-i0)))` by METIS_TAC[] THEN 1423 1424ASSUME_TAC (GSYM PROBLEM_TO_LTL_KS_SEM) THEN 1425Q_SPECL_NO_ASSUM 0 [`A`, `p`, `psl`, `i0`, `s0`, `f`, `f'`] THEN 1426PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN 1427ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1428 1429 1430MATCH_MP_TAC (prove (``!M X f f'. (LTL_EQUIVALENT_INITIAL f f' /\ 1431 (X = LTL_KS_SEM M f)) ==> (X = LTL_KS_SEM M f')``, 1432 SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_KS_SEM_def] THEN 1433 PROVE_TAC[])) THEN 1434Q_TAC EXISTS_TAC `l'` THEN 1435REPEAT STRIP_TAC THEN1 ( 1436 1437 SUBGOAL_TAC `!S. (IMAGE (\s. P_PROP (f' s)) S) = 1438 (IMAGE (\p. P_PROP p) (IMAGE f' S))` THEN1 ( 1439 SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF] 1440 ) THEN 1441 UNDISCH_HD_TAC THEN ASM_SIMP_TAC std_ss [] THEN 1442 DISCH_TAC THEN WEAKEN_HD_TAC THEN 1443 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN 1444 1445 ASM_CONGRUENCE_SIMP_TAC ltl_cs std_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET] THEN 1446 PROVE_TAC[LTL_EQUIVALENT_INITIAL_def] 1447) THEN 1448WEAKEN_NO_TAC 4 (*LTL_EQUIVALENT_INITIAL l'*) THEN 1449 1450GSYM_NO_TAC 7 (*Def sv*) THEN 1451NTAC 2 (GSYM_NO_TAC 2) (*Def f, f'*) THEN 1452ASM_SIMP_TAC std_ss [] THEN 1453 1454 1455Q.MATCH_ABBREV_TAC `IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE (symbolic_kripke_structure S0 R) 1456 (MAP (\x. x sv) DS.FC) = LTL_KS_SEM KS l'` THEN 1457ASSUME_TAC (INST_TYPE [alpha |-> num] LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN 1458Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `KS`, `a`] THEN 1459PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1460 ASM_REWRITE_TAC[] THEN 1461 1462 SUBGOAL_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS KS SUBSET 1463 INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2)` THEN1 ( 1464 Q.UNABBREV_TAC `KS` THEN 1465 ASM_SIMP_TAC std_ss [] THEN 1466 Q.MATCH_ABBREV_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS 1467 (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE 1468 (SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON 1469 A' f 1470 f' (P_PROP (SUC s0)))) SUBSET 1471 INTERVAL_SET 0 (2 * 2 ** (SUC s0 - i0) + s0 + 2)` THEN 1472 1473 1474 REMAINS_TAC `SEMI_AUTOMATON_USED_VARS ((SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON A' f f' 1475 (P_PROP (SUC s0)))) SUBSET 1476 INTERVAL_SET 0 (2 * 2 ** (SUC s0 - i0) + s0 + 2)` THEN1 ( 1477 UNDISCH_HD_TAC THEN 1478 MATCH_MP_TAC (prove (``(C SUBSET A) ==> (A SUBSET B ==> C SUBSET B)``, METIS_TAC[SUBSET_TRANS])) THEN 1479 SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 1480 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 1481 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 1482 symbolic_kripke_structure_REWRITES, SUBSET_DEF, 1483 IN_UNION] 1484 ) THEN 1485 1486 SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 ( 1487 ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN 1488 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET] THEN 1489 REPEAT STRIP_TAC THEN 1490 RES_TAC THEN 1491 DECIDE_TAC 1492 ) THEN 1493 1494 ASSUME_TAC (INST_TYPE [alpha |-> num] SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS) THEN 1495 Q_SPECL_NO_ASSUM 0 [`A'`, `f`, `f'`, `P_PROP (SUC s0)`] THEN 1496 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1497 Q.UNABBREV_TAC `A'` THEN 1498 NTAC 2 (GSYM_NO_TAC 2) (*f, f'*) THEN 1499 ASM_SIMP_TAC std_ss [symbolic_semi_automaton_REWRITES, 1500 FINITE_INTERVAL_SET, SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 1501 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 1502 P_USED_VARS_EVAL, XP_USED_VARS_EVAL, 1503 DISJOINT_DISJ_THM] THEN 1504 SIMP_ALL_TAC std_ss [IN_UNION, SUBSET_DEF, IN_INTERVAL_SET, IN_SING, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF] THEN 1505 REPEAT STRIP_TAC THEN ( 1506 LEFT_DISJ_TAC THEN 1507 SIMP_ALL_TAC std_ss [] THEN 1508 RES_TAC THEN 1509 ASM_SIMP_TAC arith_ss [] 1510 ) 1511 ) THEN 1512 1513 ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def, 1514 SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 1515 symbolic_semi_automaton_REWRITES] THEN 1516 Q.UNABBREV_TAC `A'` THEN 1517 NTAC 2 (GSYM_NO_TAC 3) THEN 1518 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 1519 symbolic_semi_automaton_REWRITES, SEMI_AUTOMATON_USED_INPUT_VARS_def, 1520 P_USED_VARS_EVAL, XP_USED_VARS_EVAL] THEN 1521 `(SUC s0) - i0 = SUC (s0 - i0)` by DECIDE_TAC THEN 1522 SUBGOAL_TAC `~(2:num ** (s0 - i0) = 0)` THEN1 ( 1523 SIMP_TAC std_ss [EXP_EQ_0] 1524 ) THEN 1525 `?a. (2 :num) ** (s0 - i0) = a` by METIS_TAC[] THEN 1526 FULL_SIMP_TAC std_ss [EXP] THEN 1527 UNDISCH_NO_TAC 1 (*~a = 0*) THEN 1528 UNDISCH_NO_TAC 5 (*SEMI_AUTOMATON_USED_VARS*) THEN 1529 UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN 1530 UNDISCH_NO_TAC 12 (*P_USED_VARS p *) THEN 1531 REPEAT WEAKEN_HD_TAC THEN 1532 SIMP_TAC std_ss [SUBSET_DEF, 1533 IN_UNION, IN_DIFF, IN_SING, SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 1534 IN_INTERVAL_SET, EXP] THEN 1535 1536 REPEAT STRIP_TAC THEN ( 1537 RES_TAC THEN 1538 DECIDE_TAC 1539 ) 1540 ) THEN 1541 1542 UNDISCH_HD_TAC THEN 1543 UNDISCH_NO_TAC 9 (*i0 <= s0*) THEN 1544 UNDISCH_NO_TAC 6 (*DS.IV*) THEN 1545 GSYM_NO_TAC 3 (*def sv*) THEN 1546 ASM_SIMP_TAC std_ss [] THEN 1547 REPEAT WEAKEN_HD_TAC THEN 1548 SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IN_UNION, 1549 SUBSET_DEF, IN_INTERVAL_SET] THEN 1550 REPEAT STRIP_TAC THENL [ 1551 RES_TAC THEN 1552 DECIDE_TAC, 1553 1554 RES_TAC THEN 1555 DECIDE_TAC 1556 ] 1557) THEN 1558ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1559 1560 1561Q.UNABBREV_TAC `KS` THEN 1562NTAC 3 (GSYM_NO_TAC 2) (*Def f, f', sv*) THEN 1563ASM_SIMP_TAC std_ss [] THEN 1564 1565SUBGOAL_TAC `!n1 n2 S. (IMAGE (\s. P_PROP (SET_BINARY_ENCODING_SHIFT n1 n2 s)) S) = 1566 (IMAGE P_PROP (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n2) S))` THEN1 ( 1567 SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF] 1568) THEN 1569SUBGOAL_TAC `!n1 n2 S. (IMAGE (\s. XP_PROP (SET_BINARY_ENCODING_SHIFT n1 n2 s)) S) = 1570 (IMAGE XP_PROP (IMAGE (SET_BINARY_ENCODING_SHIFT n1 n2) S))` THEN1 ( 1571 SIMP_TAC std_ss [GSYM IMAGE_COMPOSE, combinTheory.o_DEF] 1572) THEN 1573ASM_SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, 1574 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 1575 symbolic_semi_automaton_REWRITES, 1576 symbolic_kripke_structure_REWRITES, 1577 SYMBOLIC_BREAKPOINT_CONSTRUCTION_AUTOMATON_def, 1578 SET_BINARY_ENCODING_SHIFT___IMAGE_THM] THEN 1579NTAC 2 WEAKEN_HD_TAC THEN 1580 1581 1582ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET) THEN 1583Q_SPEC_NO_ASSUM 0 `INTERVAL_LIST (SUC i0) (SUC s0)` THEN 1584SIMP_ALL_TAC std_ss [LIST_TO_SET___INTERVAL_LIST] THEN 1585 1586GSYM_NO_TAC 3 (*sv*) THEN 1587ASM_SIMP_TAC std_ss [] THEN 1588 1589ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET, 1590XP_BIGOR___SET_TO_LIST___INTERVAL_SET, 1591P_FORALL___SET_TO_LIST___INTERVAL_SET, 1592XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET, 1593XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET, 1594VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET, 1595VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST] THEN 1596 1597ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (INST_TYPE [alpha |-> num] XP_COND___XP_NEXT_FORALL___REWRITE)) THEN 1598Q_SPECL_NO_ASSUM 0 [`XP_BIGOR 1599 (MAP XP_PROP 1600 (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 1601 (PRE (2 ** SUC (s0 - i0)) + 1602 (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))`, 1603 `(INTERVAL_LIST (SUC i0) (SUC s0))`] THEN 1604PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1605 ASM_SIMP_TAC list_ss [DISJOINT_DISJ_THM, XP_BIGOR___XP_USED_VARS, IN_LIST_BIGUNION, 1606 MAP_MAP_o, combinTheory.o_DEF, XP_USED_VARS_EVAL, MEM_MAP, 1607 GSYM LEFT_FORALL_OR_THM, NOT_IN_EMPTY] 1608) THEN 1609 1610 1611 1612 1613 1614 1615`?ht. VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1616 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0)) 1617 (SUC i0) = ht` by METIS_TAC[] THEN 1618SUBGOAL_TAC `(VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1619 (INTERVAL_LIST (SUC i0) (SUC s0)) 1620 (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 1621 (SUC i0)) = P_VAR_RENAMING (\n:num. if (n >= (SUC (SUC s0))) then n + 2 ** SUC (s0 - i0) else n) ht` THEN1 ( 1622 GSYM_NO_TAC 0 THEN 1623 ASM_REWRITE_TAC[] THEN 1624 ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___CLEAN_OFFSET) THEN 1625 Q_SPECL_NO_ASSUM 0 [`INTERVAL_LIST (SUC i0) (SUC s0)`, `(SUC (SUC s0) + 2 ** SUC (s0 - i0))`, `(SUC i0)`, `SUC (SUC s0)`, `SUC (SUC s0)`] THEN 1626 PROVE_CONDITION_NO_ASSUM 0 THEN1 SIMP_TAC arith_ss [MEM_INTERVAL_LIST] THEN 1627 1628 ASM_REWRITE_TAC[] THEN 1629 SIMP_TAC arith_ss [] 1630) THEN 1631ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1632 1633ASSUME_TAC (SIMP_RULE std_ss [RIGHT_FORALL_IMP_THM] (INST_TYPE [alpha |-> num] XP_COND___XP_CURRENT_EXISTS___REWRITE)) THEN 1634Q_SPECL_NO_ASSUM 0 [`XP_BIGOR 1635 (MAP XP_PROP 1636 (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0)) 1637 (PRE (2 ** SUC (s0 - i0)) + 1638 (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))`, 1639 `(INTERVAL_LIST (SUC i0) (SUC s0))`] THEN 1640PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1641 ASM_SIMP_TAC list_ss [DISJOINT_DISJ_THM, XP_BIGOR___XP_USED_VARS, IN_LIST_BIGUNION, 1642 MAP_MAP_o, combinTheory.o_DEF, XP_USED_VARS_EVAL, MEM_MAP, 1643 GSYM LEFT_FORALL_OR_THM, IN_SING] THEN 1644 REWRITE_TAC [MEM_INTERVAL_LIST] THEN 1645 REPEAT WEAKEN_HD_TAC THEN GEN_TAC THEN 1646 LEFT_DISJ_TAC THEN 1647 FULL_SIMP_TAC arith_ss [] 1648) THEN 1649 1650GSYM_NO_TAC 1 THEN 1651ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [] 1652); 1653 1654 1655 1656 1657 1658val PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL = 1659 store_thm ("PROBLEM_TO_KRIPKE_STRUCTURE___TOTAL", 1660 ``!A p psl i0 s0 DS S0 R l' pf sv a. ( 1661 F_CLOCK_SERE_FREE psl /\ 1662 IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A /\ 1663 ((SEMI_AUTOMATON_USED_INPUT_VARS A UNION 1664 F_USED_VARS psl) SUBSET (INTERVAL_SET 0 i0)) /\ 1665 (A.S = (INTERVAL_SET (SUC i0) s0)) /\ 1666 (P_USED_VARS p SUBSET (INTERVAL_SET 0 s0)) /\ 1667 (i0 <= s0) /\ 1668 (sv = \n:num. 2**(s0 - i0) + s0 + 1 + n) /\ 1669 LTL_TO_GEN_BUECHI_DS___SEM DS /\ 1670 (l',a,T,pf) IN DS.B /\ 1671 DS.IV SUBSET INTERVAL_SET 0 (2**(s0 - i0) + s0) /\ 1672 LTL_EQUIVALENT_INITIAL 1673 (LTL_EQUIV 1674 (LTL_ALWAYS 1675 (LTL_PROP 1676 (P_FORALL (INTERVAL_LIST (SUC i0) s0) 1677 (P_IMPL 1678 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1679 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0), 1680 p)))), PSL_TO_LTL psl)) l' /\ 1681 1682 (PROP_LOGIC_EQUIVALENT (P_AND 1683 (P_FORALL (INTERVAL_LIST (SUC i0) s0) 1684 (P_EQUIV 1685 (A.S0, 1686 VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1687 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0))), 1688 P_AND 1689 (LTL_TO_GEN_BUECHI_DS___INITIAL_STATES DS sv,P_NOT (pf sv)))) S0) /\ 1690 1691 (XPROP_LOGIC_EQUIVALENT 1692 (XP_AND 1693 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) s0) 1694 (XP_EQUIV 1695 (XP_NEXT 1696 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1697 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0)), 1698 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) s0) 1699 (XP_AND 1700 (A.R, 1701 XP_CURRENT 1702 (VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING 1703 (INTERVAL_LIST (SUC i0) s0) (SUC s0) 1704 (SUC i0)))))), 1705 XP_BIGAND (MAP (\xp. xp sv) DS.R))) R) 1706 ) ==> 1707 1708 ((IS_EMPTY_FAIR_SYMBOLIC_KRIPKE_STRUCTURE 1709 (symbolic_kripke_structure S0 R) (MAP (\x. x sv) DS.FC)) 1710 = 1711 1712 (!K. 1713 ((A_KS_SEM K (A_UNIV (A,ACCEPT_COND_G p))) = 1714 UF_KS_SEM K psl)))``, 1715 1716 1717REPEAT STRIP_TAC THEN 1718 1719`?f. f = SET_BINARY_ENCODING_SHIFT (SUC i0) (SUC s0)` by METIS_TAC[] THEN 1720 1721ASSUME_TAC (GSYM PROBLEM_TO_LTL_KS_SEM___TOTAL) THEN 1722Q_SPECL_NO_ASSUM 0 [`A`, `p`, `psl`, `i0`, `s0`, `f`] THEN 1723PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_SIMP_TAC std_ss [] THEN 1724ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1725 1726 1727MATCH_MP_TAC (prove (``!M X f f'. (LTL_EQUIVALENT_INITIAL f f' /\ 1728 (X = LTL_KS_SEM M f)) ==> (X = LTL_KS_SEM M f')``, 1729 SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def, LTL_KS_SEM_def] THEN 1730 PROVE_TAC[])) THEN 1731Q_TAC EXISTS_TAC `l'` THEN 1732REPEAT STRIP_TAC THEN1 ( 1733 1734 FULL_SIMP_TAC std_ss [LTL_EQUIVALENT_INITIAL_def] THEN 1735 GSYM_NO_TAC 3 THEN 1736 ASM_SIMP_TAC arith_ss [LTL_SEM_THM, P_FORALL_SEM, LIST_TO_SET___INTERVAL_LIST, 1737 SET_TO_LIST_INV, FINITE_INTERVAL_SET, P_SEM_THM, 1738 GSYM VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST, 1739 GSYM (SIMP_RULE std_ss [PROP_LOGIC_EQUIVALENT_def] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET)] 1740) THEN 1741WEAKEN_NO_TAC 3 (*LTL_EQUIVALENT_INITIAL l'*) THEN 1742 1743GSYM_NO_TAC 6 (*Def sv*) THEN 1744GSYM_NO_TAC 1 (*Def f*) THEN 1745ASM_SIMP_TAC std_ss [] THEN 1746 1747 1748Q.ABBREV_TAC `KS = (SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE 1749 (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f))` THEN 1750ASSUME_TAC (INST_TYPE [alpha |-> num] LTL_TO_GEN_BUECHI_DS___KS_SEM___KRIPKE_STRUCTURE) THEN 1751Q_SPECL_NO_ASSUM 0 [`DS`, `l'`, `pf`, `sv`, `KS`, `a`] THEN 1752PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1753 ASM_REWRITE_TAC[] THEN 1754 1755 SUBGOAL_TAC `SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS KS SUBSET 1756 INTERVAL_SET 0 (2**(s0 - i0) + s0)` THEN1 ( 1757 Q.UNABBREV_TAC `KS` THEN 1758 REMAINS_TAC `SEMI_AUTOMATON_USED_VARS (RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON A f) SUBSET INTERVAL_SET 0 (2 ** (s0 - i0) + s0)` THEN1 ( 1759 UNDISCH_HD_TAC THEN 1760 MATCH_MP_TAC (prove (``(C SUBSET A) ==> (A SUBSET B ==> C SUBSET B)``, METIS_TAC[SUBSET_TRANS])) THEN 1761 SIMP_TAC std_ss [SYMBOLIC_KRIPKE_STRUCTURE_USED_VARS_def, 1762 SEMI_AUTOMATON_USED_VARS___DIRECT_DEF, 1763 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 1764 symbolic_kripke_structure_REWRITES, SUBSET_DEF, 1765 IN_UNION] 1766 ) THEN 1767 1768 SUBGOAL_TAC `SEMI_AUTOMATON_USED_VARS A SUBSET (INTERVAL_SET 0 s0)` THEN1 ( 1769 ASM_REWRITE_TAC[SEMI_AUTOMATON_USED_VARS_def] THEN 1770 SIMP_ALL_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INTERVAL_SET] THEN 1771 REPEAT STRIP_TAC THEN 1772 RES_TAC THEN 1773 DECIDE_TAC 1774 ) THEN 1775 1776 ASSUME_TAC (INST_TYPE [alpha |-> num] RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON___USED_INPUT_VARS) THEN 1777 Q_SPECL_NO_ASSUM 0 [`A`, `f`] THEN 1778 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1779 GSYM_NO_TAC 1 (*Def f*) THEN 1780 ASM_SIMP_TAC std_ss [FINITE_INTERVAL_SET, 1781 DISJOINT_DISJ_THM, SEMI_AUTOMATON_USED_VARS_def, IN_UNION] THEN 1782 GEN_TAC THEN 1783 LEFT_DISJ_TAC THEN 1784 SUBGOAL_TAC `x <= s0` THEN1 ( 1785 CLEAN_ASSUMPTIONS_TAC THENL [ 1786 `x IN INTERVAL_SET 0 i0` by METIS_TAC[UNION_SUBSET, SUBSET_DEF] THEN 1787 FULL_SIMP_TAC arith_ss [IN_INTERVAL_SET], 1788 1789 FULL_SIMP_TAC arith_ss [IN_INTERVAL_SET] 1790 ] 1791 ) THEN 1792 1793 Cases_on `i0 = s0` THENL [ 1794 SUBGOAL_TAC `INTERVAL_SET (SUC i0) s0 = EMPTY` THEN1 ( 1795 ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] 1796 ) THEN 1797 ASM_REWRITE_TAC[IN_IMAGE, IN_POW, 1798 SUBSET_EMPTY] THEN 1799 1800 SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT_def, 1801 SET_BINARY_ENCODING_def, 1802 IMAGE_EMPTY, 1803 SUM_IMAGE_THM] THEN 1804 DECIDE_TAC, 1805 1806 `SUC i0 <= s0` by DECIDE_TAC THEN 1807 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 1808 DISJOINT_DISJ_THM, IN_INTERVAL_SET] 1809 ] 1810 ) THEN 1811 1812 ASM_SIMP_TAC std_ss [SEMI_AUTOMATON_USED_VARS_def, 1813 RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, 1814 symbolic_semi_automaton_REWRITES, UNION_SUBSET, SUBSET_DEF, 1815 IN_INTERVAL_SET, IN_UNION] THEN 1816 REPEAT STRIP_TAC THENL [ 1817 `x IN INTERVAL_SET 0 i0` by PROVE_TAC[UNION_SUBSET, SUBSET_DEF] THEN 1818 UNDISCH_HD_TAC THEN 1819 ASM_SIMP_TAC arith_ss [IN_INTERVAL_SET], 1820 1821 1822 UNDISCH_HD_TAC THEN 1823 GSYM_NO_TAC 2 (*Def f*) THEN 1824 ASM_REWRITE_TAC[] THEN 1825 Cases_on `i0 = s0` THENL [ 1826 SUBGOAL_TAC `INTERVAL_SET (SUC s0) s0 = EMPTY` THEN1 ( 1827 ASM_SIMP_TAC arith_ss [EXTENSION, IN_INTERVAL_SET, NOT_IN_EMPTY] 1828 ) THEN 1829 ASM_REWRITE_TAC[IN_IMAGE, IN_POW, 1830 SUBSET_EMPTY] THEN 1831 1832 SIMP_TAC arith_ss [SET_BINARY_ENCODING_SHIFT_def, 1833 SET_BINARY_ENCODING_def, 1834 IMAGE_EMPTY, 1835 SUM_IMAGE_THM], 1836 1837 `SUC i0 <= s0` by DECIDE_TAC THEN 1838 `SUC (s0 - SUC i0) = (s0 - i0)` by DECIDE_TAC THEN 1839 ASM_SIMP_TAC std_ss [SET_BINARY_ENCODING_SHIFT___IMAGE_THM, 1840 DISJOINT_DISJ_THM, IN_INTERVAL_SET] THEN 1841 WEAKEN_HD_TAC THEN 1842 `~((2:num)**(s0 - i0) = 0)` by SIMP_TAC std_ss [EXP_EQ_0] THEN 1843 DECIDE_TAC 1844 ] 1845 ] 1846 ) THEN 1847 GSYM_NO_TAC 3 THEN 1848 ASM_SIMP_TAC std_ss [IS_ELEMENT_ITERATOR_def, IN_UNION] THEN 1849 REPEAT STRIP_TAC THEN ( 1850 `2 ** (s0 - i0) + s0 + 1 + i IN INTERVAL_SET 0 (2 ** (s0 - i0) + s0)` by 1851 METIS_TAC[SUBSET_DEF] THEN 1852 UNDISCH_HD_TAC THEN 1853 SIMP_TAC arith_ss [IN_INTERVAL_SET] 1854 ) 1855) THEN 1856ASM_REWRITE_TAC[] THEN WEAKEN_HD_TAC THEN 1857 1858 1859Q.UNABBREV_TAC `KS` THEN 1860NTAC 2 (GSYM_NO_TAC 1) (*Def f, sv*) THEN 1861ASM_SIMP_TAC std_ss [RABIN_SCOTT_SUBSET_CONSTRUCTION_AUTOMATON_def, 1862 SYMBOLIC_KRIPKE_STRUCTURE_PRODUCT_def, 1863 SYMBOLIC_SEMI_AUTOMATON___TO___KRIPKE_STRUCTURE_def, 1864 symbolic_semi_automaton_REWRITES, 1865 symbolic_kripke_structure_REWRITES] THEN 1866 1867ASSUME_TAC (INST_TYPE [alpha |-> num] VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET) THEN 1868Q_SPEC_NO_ASSUM 0 `INTERVAL_LIST (SUC i0) s0` THEN 1869SIMP_ALL_TAC std_ss [LIST_TO_SET___INTERVAL_LIST] THEN 1870 1871GSYM_NO_TAC 2 (*sv*) THEN 1872ASM_SIMP_TAC std_ss [] THEN 1873 1874ASM_CONGRUENCE_SIMP_TAC ks_congset arith_ss [P_BIGOR___SET_TO_LIST___INTERVAL_SET, 1875XP_BIGOR___SET_TO_LIST___INTERVAL_SET, 1876P_FORALL___SET_TO_LIST___INTERVAL_SET, 1877XP_NEXT_FORALL___SET_TO_LIST___INTERVAL_SET, 1878XP_CURRENT_EXISTS___SET_TO_LIST___INTERVAL_SET, 1879VAR_RENAMING_HASHTABLE_LIST___EQUIVALENT_HASHTABLE_SET, 1880VAR_RENAMING_HASHTABLE_LIST___BINARY_ENCODING___HASHTABLE_LIST] 1881); 1882 1883 1884 1885val _ = export_theory(); 1886