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/tools") :: !loadPath; 9 10map load 11 ["xprop_logicTheory", "prop_logicTheory", "infinite_pathTheory", "pred_setTheory", "listTheory", "pairTheory", "set_lemmataTheory", 12 "containerTheory", "prim_recTheory", "tuerk_tacticsLib", "temporal_deep_mixedTheory", "arithmeticTheory", "numLib", 13 "alternating_omega_automataTheory", "symbolic_semi_automatonTheory", "automaton_formulaTheory"]; 14*) 15 16open infinite_pathTheory pred_setTheory listTheory pairTheory xprop_logicTheory 17 containerTheory prop_logicTheory set_lemmataTheory prim_recTheory 18 tuerk_tacticsLib temporal_deep_mixedTheory arithmeticTheory numLib 19 automaton_formulaTheory alternating_omega_automataTheory 20 symbolic_semi_automatonTheory; 21open Sanity; 22 23val _ = hide "S"; 24val _ = hide "I"; 25 26(* 27show_assums := false; 28show_assums := true; 29show_types := true; 30show_types := false; 31quietdec := false; 32*) 33 34 35val _ = new_theory "alternating_omega_automata_to_automaton_formula"; 36 37(*This file contains some definitions and lemmata about a translation of 38 alternating omega-automata to automaton formulas, i.e. symbolic 39 nondeterminisation algorithms for alternating automata. 40 41 However, it is far away from beeing complete. The main interest has been 42 in proving some very simple cases. Alternating and symbolically represented 43 nondeterministic automata are strongly connected for finite words. In fact, 44 alternating automata on finite words can be considered as a special normal 45 form of nonderministic automata, i.e. there is a very very simple nondetermisation 46 algorithm for finite words. 47 48 The same idea also works for simple classes of alternating omega automata. 49 Here it is proved for alternating automata representing savety properties. 50 51 For more details you can have a look at the internal report 52 "Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata" by Thomas Tuerk and Klaus Schneider, 53 University of Kaiserslautern, November 2005. 54 It can be found at http://rsg.informatik.uni-kl.de/publications/. 55 *) 56 57 58 59 60 61 62 63 64val IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def = Define 65 `IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON (A:('a, 'a) alternating_semi_automaton) (fi:'a->'a set) = 66 (symbolic_semi_automaton (A:('a, 'a) alternating_semi_automaton).S 67 A.S0 68 (XP_BIGAND (SET_TO_LIST (IMAGE (\s. XP_IMPL (XP_PROP s, 69 XP_BIGOR (SET_TO_LIST (IMAGE (\i. XP_AND(XP_CURRENT (P_PROP_SET_MODEL (fi i) (BIGUNION(IMAGE fi A.I))), XP_NEXT (A.R s i))) A.I)))) A.S))))`; 70 71 72val EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def = Define 73 `EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON (A:('a, 'a) alternating_semi_automaton) (fi:'a->'a set) = 74 (symbolic_semi_automaton (A:('a, 'a) alternating_semi_automaton).S 75 A.S0 76 (XP_BIGAND (SET_TO_LIST (IMAGE (\s. XP_EQUIV(XP_PROP s, 77 XP_BIGOR (SET_TO_LIST (IMAGE (\i. XP_AND(XP_CURRENT (P_PROP_SET_MODEL (fi i) (BIGUNION(IMAGE fi A.I))), XP_NEXT (A.R s i))) A.I)))) A.S))))`; 78 79 80 81val COLLAPSED_ALTERNATING_RUN_def = 82Define 83 `COLLAPSED_ALTERNATING_RUN (r:'a alternating_run) = \n:num. 84 {s | IS_REACHABLE_BY_RUN (s, n) r}`; 85 86 87val DECOLLAPSED_RUN_def = 88Define 89 `DECOLLAPSED_RUN (r:num->'a set) = alternating_run (r 0) (\s n:num. r (SUC n))`; 90 91val EMPTY_ABORT_RUN_def = 92Define 93 `EMPTY_ABORT_RUN (r:num->'a set) = (\n. if (?n'. (n' < n) /\ (r n' = EMPTY)) then EMPTY else r n)`; 94 95val IS_VALID_INPUT_ENCODING_def = 96Define 97 `IS_VALID_INPUT_ENCODING (A:('a,'b) alternating_semi_automaton) (f:'a->'b set) = 98 ((INJ f A.I UNIV) /\ (!i. (i IN A.I ==> (FINITE (f i) /\ DISJOINT A.S (f i)))))`; 99 100val IS_VALID_ENCODED_INPUT_def = 101Define 102 `IS_VALID_ENCODED_INPUT (A:('a,'b) alternating_semi_automaton) (f:'a->'b set) i i' = 103 (!n. (i n IN A.I) /\ (i' n = f (i n)))`; 104 105 106 107 108 109 110 111val EQ_COLLAPSED_RUN___IMPLIES___IMPL_COLLAPSED_RUN = 112 store_thm 113 ("EQ_COLLAPSED_RUN___IMPLIES___IMPL_COLLAPSED_RUN", 114 ``!A fi r i. (FINITE A.S /\ IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i r) ==> 115 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i r``, 116 117 SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 118 IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, 119 INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def, XP_BIGAND_SEM, 120 symbolic_semi_automaton_REWRITES] THEN 121 REPEAT STRIP_TAC THEN 122 UNDISCH_HD_TAC THEN UNDISCH_HD_TAC THEN 123 ASM_SIMP_TAC std_ss [IMAGE_FINITE, MEM_SET_TO_LIST, IN_IMAGE] THEN 124 SIMP_TAC std_ss [GSYM LEFT_FORALL_IMP_THM, GSYM LEFT_EXISTS_IMP_THM, 125 GSYM RIGHT_FORALL_IMP_THM] THEN 126 SIMP_TAC std_ss [XP_SEM_THM] THEN 127 METIS_TAC[]); 128 129 130 131 132val IMPL_COLLAPSED_RUN_SEM = 133 store_thm 134 ("IMPL_COLLAPSED_RUN_SEM", 135 136 ``!A f i' i w. 137 (IS_VALID_ALTERNATING_SEMI_AUTOMATON A /\ 138 IS_VALID_INPUT_ENCODING A f /\ 139 IS_VALID_ENCODED_INPUT A f i i') ==> ( 140 141 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A f) i' w = 142 (PATH_SUBSET w A.S /\ P_SEM (w 0) A.S0 /\ 143 !n s. (s IN w n) ==> P_SEM (w (SUC n)) (A.R s (i n))))``, 144 145 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, 146 INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def, XP_BIGAND_SEM, MEM_SET_TO_LIST, 147 IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 148 EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 149 IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, GSYM LEFT_FORALL_IMP_THM, XP_BIGOR_SEM, 150 GSYM LEFT_EXISTS_AND_THM, IS_VALID_INPUT_ENCODING_def, 151 IS_VALID_ENCODED_INPUT_def, symbolic_semi_automaton_REWRITES, IMAGE_FINITE, 152 IN_IMAGE, XP_SEM_THM, XP_SEM___XP_CURRENT, 153 XP_SEM___XP_NEXT, IN_UNION, IN_DIFF] THEN 154 REPEAT STRIP_TAC THEN 155 SUBGOAL_TAC `FINITE (BIGUNION (IMAGE f A.I))` THEN1 ( 156 ASM_SIMP_TAC std_ss [FINITE_BIGUNION_EQ, IMAGE_FINITE, IN_IMAGE] THEN 157 PROVE_TAC[]) THEN 158 ASM_SIMP_TAC std_ss [P_PROP_SET_MODEL_SEM] THEN 159 160 SUBGOAL_TAC `!n. ((w n UNION (f (i n) DIFF A.S)) INTER A.S) = (w n INTER A.S)` THEN1 ( 161 SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, IN_DIFF] THEN 162 REPEAT STRIP_TAC THEN 163 REPEAT BOOL_EQ_STRIP_TAC 164 ) THEN 165 `P_SEM (w 0 UNION (f (i 0) DIFF A.S)) A.S0 = 166 P_SEM (w 0) A.S0` by PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] THEN 167 `!i' n s. i' IN A.I ==> (P_SEM (w n UNION (f (i n) DIFF A.S)) (A.R s i') = 168 P_SEM (w n) (A.R s i'))` by PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] THEN 169 ASM_REWRITE_TAC[] THEN 170 REPEAT BOOL_EQ_STRIP_TAC THEN 171 REPEAT FORALL_EQ_STRIP_TAC THEN 172 rename1 `s IN A.S` THEN 173 Cases_on `~(s IN w n)` THENL [ 174 ASM_REWRITE_TAC[], 175 176 `s IN A.S` by PROVE_TAC[PATH_SUBSET_def, SUBSET_DEF] THEN 177 FULL_SIMP_TAC std_ss [] THEN 178 SUBGOAL_TAC `((w n UNION (f (i n) DIFF A.S)) INTER BIGUNION (IMAGE f A.I)) = f (i n)` THEN1 ( 179 SIMP_TAC std_ss [EXTENSION] THEN 180 SIMP_ALL_TAC std_ss [IN_INTER, IN_UNION, IN_DIFF, IN_BIGUNION, 181 IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM, GSYM SUBSET_COMPL_DISJOINT, 182 PATH_SUBSET_def, SUBSET_DEF, COMPL_DEF, IN_UNIV] THEN 183 METIS_TAC[] 184 ) THEN 185 SUBGOAL_TAC `!i'. (i' IN A.I) ==> (f i' INTER BIGUNION (IMAGE f A.I) = f i')` THEN1 ( 186 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_BIGUNION, 187 IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM] THEN 188 METIS_TAC[] 189 ) THEN 190 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 191 PROVE_TAC[INJ_DEF], 192 193 EXISTS_TAC ``i:num->'a n`` THEN 194 ASM_REWRITE_TAC[] THEN 195 PROVE_TAC[] 196 ] 197 ]); 198 199 200 201val EQ_COLLAPSED_RUN_SEM = 202 store_thm 203 ("EQ_COLLAPSED_RUN_SEM", 204 205 ``!A f i' i w. 206 (IS_VALID_ALTERNATING_SEMI_AUTOMATON A /\ 207 IS_VALID_INPUT_ENCODING A f /\ 208 IS_VALID_ENCODED_INPUT A f i i') ==> ( 209 210 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A f) i' w = 211 (PATH_SUBSET w A.S /\ P_SEM (w 0) A.S0 /\ 212 !n s. (s IN w n) = ((s IN A.S) /\ P_SEM (w (SUC n)) (A.R s (i n)))))``, 213 214 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, INPUT_RUN_PATH_UNION_def, 215 INPUT_RUN_STATE_UNION_def, IS_TRANSITION_def, XP_BIGAND_SEM, MEM_SET_TO_LIST, 216 IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 217 EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 218 IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, GSYM LEFT_FORALL_IMP_THM, XP_BIGOR_SEM, 219 GSYM LEFT_EXISTS_AND_THM, IS_VALID_INPUT_ENCODING_def, 220 IS_VALID_ENCODED_INPUT_def, symbolic_semi_automaton_REWRITES, IMAGE_FINITE, 221 IN_IMAGE, XP_SEM_THM, XP_SEM___XP_CURRENT, 222 XP_SEM___XP_NEXT, IN_UNION, IN_DIFF] THEN 223 REPEAT STRIP_TAC THEN 224 SUBGOAL_TAC `FINITE (BIGUNION (IMAGE f A.I))` THEN1 ( 225 ASM_SIMP_TAC std_ss [FINITE_BIGUNION_EQ, IMAGE_FINITE, IN_IMAGE] THEN 226 PROVE_TAC[] 227 ) THEN 228 ASM_SIMP_TAC std_ss [P_PROP_SET_MODEL_SEM] THEN 229 230 SUBGOAL_TAC `!n. ((w n UNION (f (i n) DIFF A.S)) INTER A.S) = (w n INTER A.S)` THEN1 ( 231 SIMP_TAC std_ss [EXTENSION, IN_UNION, IN_INTER, IN_DIFF] THEN 232 REPEAT STRIP_TAC THEN 233 REPEAT BOOL_EQ_STRIP_TAC 234 ) THEN 235 `P_SEM (w 0 UNION (f (i 0) DIFF A.S)) A.S0 = 236 P_SEM (w 0) A.S0` by PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] THEN 237 `!i' n s. i' IN A.I ==> (P_SEM (w n UNION (f (i n) DIFF A.S)) (A.R s i') = 238 P_SEM (w n) (A.R s i'))` by PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] THEN 239 ASM_REWRITE_TAC[] THEN 240 REPEAT BOOL_EQ_STRIP_TAC THEN 241 REPEAT FORALL_EQ_STRIP_TAC THEN 242 rename1 `s IN A.S` THEN 243 Cases_on `~(s IN A.S)` THENL [ 244 ASM_REWRITE_TAC[] THEN 245 PROVE_TAC[PATH_SUBSET_def, SUBSET_DEF], 246 247 FULL_SIMP_TAC std_ss [] THEN 248 ASM_SIMP_TAC std_ss [prove(``!a:bool b:bool c:bool. ((a = b) = (a = c)) = (b = c)``, METIS_TAC[])] THEN 249 250 SUBGOAL_TAC `((w n UNION (f (i n) DIFF A.S)) INTER BIGUNION (IMAGE f A.I)) = f (i n)` THEN1 ( 251 SIMP_TAC std_ss [EXTENSION] THEN 252 SIMP_ALL_TAC std_ss [IN_INTER, IN_UNION, IN_DIFF, IN_BIGUNION, 253 IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM, GSYM SUBSET_COMPL_DISJOINT, 254 PATH_SUBSET_def, SUBSET_DEF, COMPL_DEF, IN_UNIV] THEN 255 METIS_TAC[] 256 ) THEN 257 SUBGOAL_TAC `!i'. (i' IN A.I) ==> (f i' INTER BIGUNION (IMAGE f A.I) = f i')` THEN1 ( 258 SIMP_TAC std_ss [EXTENSION, IN_INTER, IN_BIGUNION, 259 IN_IMAGE, GSYM RIGHT_EXISTS_AND_THM] THEN 260 METIS_TAC[] 261 ) THEN 262 263 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 264 PROVE_TAC[INJ_DEF], 265 266 EXISTS_TAC ``i:num->'a n`` THEN 267 ASM_REWRITE_TAC[] THEN 268 PROVE_TAC[] 269 ] 270 ]); 271 272 273val EMPTY_ABORT_RUN_ELIM = 274 store_thm 275 ("EMPTY_ABORT_RUN_ELIM", 276 ``!r. (!n. ~(r n = EMPTY)) ==> (EMPTY_ABORT_RUN r = r)``, 277 SIMP_TAC std_ss [EMPTY_ABORT_RUN_def] THEN 278 SIMP_TAC std_ss [FUN_EQ_THM]); 279 280 281val EMPTY_ABORT_RUN_EMPTY_SUC = 282 store_thm 283 ("EMPTY_ABORT_RUN_EMPTY_SUC", 284 ``!r n. (EMPTY_ABORT_RUN r n = EMPTY) ==> (EMPTY_ABORT_RUN r (SUC n) = EMPTY)``, 285 SIMP_TAC std_ss [EMPTY_ABORT_RUN_def] THEN 286 REPEAT STRIP_TAC THEN 287 Tactical.REVERSE (SUBGOAL_THEN ``?n'. n' < SUC n /\ (r n' = EMPTY)`` ASSUME_TAC) THEN1 ( 288 PROVE_TAC[] 289 ) THEN 290 Cases_on `?n'. n' < n /\ (r n' = EMPTY)` THENL [ 291 CLEAN_ASSUMPTIONS_TAC THEN 292 `n' < SUC n` by DECIDE_TAC THEN 293 PROVE_TAC[], 294 295 `r n = EMPTY` by PROVE_TAC[] THEN 296 `n < SUC n` by DECIDE_TAC THEN 297 PROVE_TAC[] 298 ]); 299 300 301val COLLAPSED_DECOLLAPSED_ELIM = 302 store_thm 303 ("COLLAPSED_DECOLLAPSED_ELIM", 304 ``!r. ((COLLAPSED_ALTERNATING_RUN (DECOLLAPSED_RUN (EMPTY_ABORT_RUN r))) = (EMPTY_ABORT_RUN r))``, 305 306 SIMP_TAC std_ss [COLLAPSED_ALTERNATING_RUN_def, DECOLLAPSED_RUN_def] THEN 307 REPEAT STRIP_TAC THEN 308 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN 309 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] THEN 310 Induct_on `x` THENL [ 311 REWRITE_TAC [IS_REACHABLE_BY_RUN_def, alternating_run_S0], 312 313 ASM_REWRITE_TAC [IS_REACHABLE_BY_RUN_def, alternating_run_R] THEN 314 Cases_on `EMPTY_ABORT_RUN r x = EMPTY` THENL [ 315 PROVE_TAC[MEMBER_NOT_EMPTY, EMPTY_ABORT_RUN_EMPTY_SUC], 316 PROVE_TAC[MEMBER_NOT_EMPTY] 317 ] 318 ]); 319 320 321 322val IS_REACHABLE_BY_DECOLLAPSED_EMPTY_ABORT_RUN_ELIM = 323 store_thm 324 ("IS_REACHABLE_BY_DECOLLAPSED_EMPTY_ABORT_RUN_ELIM", 325 ``!s n r. (IS_REACHABLE_BY_RUN (s, n) (DECOLLAPSED_RUN (EMPTY_ABORT_RUN r))) = (s IN (EMPTY_ABORT_RUN r) n)``, 326 327 Induct_on `n` THENL [ 328 SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, DECOLLAPSED_RUN_def, alternating_run_S0], 329 330 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_R, DECOLLAPSED_RUN_def] THEN 331 REPEAT GEN_TAC THEN 332 Cases_on `EMPTY_ABORT_RUN r n = EMPTY` THENL [ 333 PROVE_TAC[MEMBER_NOT_EMPTY, EMPTY_ABORT_RUN_EMPTY_SUC], 334 PROVE_TAC[MEMBER_NOT_EMPTY] 335 ] 336 ]); 337 338 339val IS_REACHABLE_BY_DECOLLAPSED_RUN = 340 store_thm 341 ("IS_REACHABLE_BY_DECOLLAPSED_RUN", 342 ``!s n r. (IS_REACHABLE_BY_RUN (s, n) (DECOLLAPSED_RUN r)) ==> (s IN r n)``, 343 344 Induct_on `n` THENL [ 345 SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, DECOLLAPSED_RUN_def, alternating_run_S0], 346 347 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_R, DECOLLAPSED_RUN_def] THEN 348 PROVE_TAC[] 349 ]); 350 351 352 353val IMPL_COLLAPSED_SEMI_AUTOMATON___EMPTY_ABORT_RUN = 354 store_thm 355 ("IMPL_COLLAPSED_SEMI_AUTOMATON___EMPTY_ABORT_RUN", 356 ``!A fi r i. FINITE A.S /\ IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i r ==> 357 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i (EMPTY_ABORT_RUN r)``, 358 359REPEAT STRIP_TAC THEN 360Cases_on `~?n. ((r n = EMPTY) /\ (!m. m < n ==> ~(r m = EMPTY)))` THENL [ 361 FULL_SIMP_TAC std_ss [] THEN 362 SUBGOAL_TAC `!n:num. ~(r n = EMPTY)` THEN1 ( 363 REMAINS_TAC `!n:num. (!m. m < n ==> ~(r m = EMPTY))` THEN1 ( 364 REPEAT STRIP_TAC THEN 365 `n < SUC n` by DECIDE_TAC THEN 366 PROVE_TAC[] 367 ) THEN 368 Induct_on `n` THENL [ 369 SIMP_TAC arith_ss [], 370 371 REPEAT STRIP_TAC THEN 372 `~(m < n)` by PROVE_TAC[] THEN 373 `m = n` by DECIDE_TAC THEN 374 PROVE_TAC[] 375 ] 376 ) THEN 377 PROVE_TAC[EMPTY_ABORT_RUN_ELIM], 378 379 380 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def] THEN 381 REPEAT STRIP_TAC THENL [ 382 FULL_SIMP_TAC std_ss [IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON_def, IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 383 symbolic_semi_automaton_REWRITES, PATH_SUBSET_def, EMPTY_ABORT_RUN_def] THEN 384 PROVE_TAC[EMPTY_SUBSET], 385 386 FULL_SIMP_TAC std_ss [INPUT_RUN_PATH_UNION_def] THEN 387 `EMPTY_ABORT_RUN r 0 = r 0` by SIMP_TAC arith_ss [EMPTY_ABORT_RUN_def] THEN 388 ASM_REWRITE_TAC[], 389 390 Cases_on `~(EMPTY_ABORT_RUN r n' = EMPTY)` THENL [ 391 SUBGOAL_TAC `EMPTY_ABORT_RUN r n' = r n'` THEN1 ( 392 FULL_SIMP_TAC arith_ss [EMPTY_ABORT_RUN_def] THEN 393 PROVE_TAC[] 394 ) THEN 395 SUBGOAL_TAC `EMPTY_ABORT_RUN r (SUC n') = r (SUC n')` THEN1 ( 396 FULL_SIMP_TAC arith_ss [EMPTY_ABORT_RUN_def] THEN 397 REMAINS_TAC `~?n''. n'' < SUC n' /\ (r n'' = {})` THEN1 ( 398 ASM_REWRITE_TAC[] 399 ) THEN 400 SIMP_TAC std_ss [] THEN 401 REPEAT STRIP_TAC THEN 402 Cases_on `n'' < n'` THEN1 PROVE_TAC[] THEN 403 Cases_on `n'' < SUC n'` THEN ASM_REWRITE_TAC[] THEN 404 `n'' = n'` by DECIDE_TAC THEN 405 ASM_REWRITE_TAC[] 406 ) THEN 407 ASM_REWRITE_TAC[], 408 409 CLEAN_ASSUMPTIONS_TAC THEN 410 ASM_SIMP_TAC std_ss [IS_TRANSITION_def, IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, 411 INPUT_RUN_STATE_UNION_def, XP_BIGAND_SEM, IMAGE_FINITE, MEM_SET_TO_LIST, IN_IMAGE, 412 GSYM LEFT_FORALL_IMP_THM, symbolic_semi_automaton_REWRITES, 413 IN_DIFF, XP_SEM_THM, UNION_EMPTY] 414 ] 415 ] 416]); 417 418 419val COLLAPSED_ALTERNATING_RUN___IMPL_COLLAPSED___THM = 420 store_thm 421 ("COLLAPSED_ALTERNATING_RUN___IMPL_COLLAPSED___THM", 422 423``!A fi i i' r. 424 ((IS_VALID_ALTERNATING_SEMI_AUTOMATON A) /\ 425 IS_VALID_INPUT_ENCODING A fi /\ 426 IS_VALID_ENCODED_INPUT A fi i i') ==> 427 428 (ALTERNATING_RUN A i r ==> 429 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i' (COLLAPSED_ALTERNATING_RUN r))``, 430 431 REPEAT STRIP_TAC THEN 432 ASSUME_TAC ((SPECL [``A:('a,'a) alternating_semi_automaton``, ``fi:'a->'a->bool``, 433 ``i':num->'a->bool``, ``i:num->'a``] IMPL_COLLAPSED_RUN_SEM)) THEN 434 ASM_SIMP_TAC std_ss [] THEN 435 WEAKEN_HD_TAC THEN 436 FULL_SIMP_TAC std_ss [ 437 COLLAPSED_ALTERNATING_RUN_def, IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 438 IS_REACHABLE_BY_RUN_def, IS_VALID_INPUT_ENCODING_def, IS_VALID_ENCODED_INPUT_def, 439 GSPECIFICATION, PATH_SUBSET_def, SUBSET_DEF, GSPEC_ID] THEN 440 441 REPEAT STRIP_TAC THENL [ 442 PROVE_TAC[REACHABLE_STATES_IN_STATES_SET, 443 ALTERNATING_RUN_IS_PRERUN], 444 445 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def], 446 447 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def] THEN 448 SUBGOAL_TAC `r.R s n SUBSET ({s | ?s'. IS_REACHABLE_BY_RUN (s',n) r /\ s IN r.R s' n})` THEN1 ( 449 ASM_SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] THEN 450 PROVE_TAC[]) THEN 451 PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM] 452 ]); 453 454 455val DECOLLAPSED_RUN___IMPL_COLLAPSED___THM = 456 store_thm 457 ("DECOLLAPSED_RUN___IMPL_COLLAPSED___THM", 458 459 ``!A fi i i' r. 460 ((IS_VALID_ALTERNATING_SEMI_AUTOMATON A) /\ 461 IS_VALID_INPUT_ENCODING A fi /\ 462 IS_VALID_ENCODED_INPUT A fi i i') ==> 463 464 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i' r ==> 465 ALTERNATING_RUN A i (DECOLLAPSED_RUN r))``, 466 467 REPEAT STRIP_TAC THEN 468 `PATH_SUBSET r A.S /\ P_SEM (r 0) A.S0 /\ 469 !n s. s IN r n ==> P_SEM (r (SUC n)) (A.R s (i n))` by PROVE_TAC[IMPL_COLLAPSED_RUN_SEM] THEN 470 471 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def, DECOLLAPSED_RUN_def, 472 alternating_run_S0, alternating_run_R, IS_VALID_ENCODED_INPUT_def, 473 PATH_SUBSET_def] THEN 474 METIS_TAC[IS_REACHABLE_BY_DECOLLAPSED_RUN, DECOLLAPSED_RUN_def]); 475 476 477 478 479val IMPL_COLLAPSED_RUN___EQ_COLLAPSED_RUN___ENRICHMENT = 480 store_thm 481 ("IMPL_COLLAPSED_RUN___EQ_COLLAPSED_RUN___ENRICHMENT", 482 483 ``!A f i i' w. (IS_VALID_ALTERNATING_SEMI_AUTOMATON A /\ 484 IS_VALID_INPUT_ENCODING A f /\ IS_VALID_ENCODED_INPUT A f i i' /\ 485 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A f) i' w) ==> 486 (?w'. (!n. w n SUBSET w' n) /\ 487 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A f) i' w')``, 488 489 REPEAT STRIP_TAC THEN 490 UNDISCH_HD_TAC THEN 491 ASSUME_TAC ((SPECL [``A:('a,'a) alternating_semi_automaton``, ``f:'a->'a->bool``, 492 ``i':num->'a->bool``, ``i:num->'a``] EQ_COLLAPSED_RUN_SEM)) THEN 493 ASSUME_TAC ((SPECL [``A:('a,'a) alternating_semi_automaton``, ``f:'a->'a->bool``, 494 ``i':num->'a->bool``, ``i:num->'a``] IMPL_COLLAPSED_RUN_SEM)) THEN 495 ASM_SIMP_TAC std_ss [] THEN 496 WEAKEN_HD_TAC THEN WEAKEN_HD_TAC THEN 497 REPEAT STRIP_TAC THEN 498 499 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, PATH_SUBSET_def] THEN 500 `?fw. fw = (\w n. (w n) UNION ({s | s IN A.S /\ P_SEM (w (SUC n)) (A.R s (i n))}))` by METIS_TAC[] THEN 501 `?w'. w' = (\n:num. BIGUNION {FUNPOW fw m w n | m IN UNIV})` by 502 METIS_TAC[] THEN 503 504 505 SUBGOAL_TAC `(!m n:num. (w n SUBSET (FUNPOW fw m w n)) /\ ((FUNPOW fw m w n) SUBSET (A:('a,'a) alternating_semi_automaton).S))` THEN1 ( 506 Induct_on `m` THENL [ 507 ASM_SIMP_TAC std_ss [FUNPOW_0, SUBSET_REFL], 508 509 `?x. FUNPOW fw m w = x` by PROVE_TAC[] THEN 510 ASM_SIMP_TAC std_ss [FUNPOW_SUC, UNION_SUBSET] THEN 511 REPEAT STRIP_TAC THENL [ 512 PROVE_TAC[SUBSET_UNION, SUBSET_REFL, SUBSET_TRANS], 513 PROVE_TAC[], 514 SIMP_TAC std_ss [SUBSET_DEF, GSPECIFICATION] 515 ] 516 ] 517 ) THEN 518 519 520 SUBGOAL_TAC `!m m':num n:num. m' >= m ==> ((FUNPOW fw m w n) SUBSET (FUNPOW fw m' w n))` THEN1 ( 521 Induct_on `m'-m` THENL [ 522 523 REPEAT STRIP_TAC THEN 524 `m' = m` by DECIDE_TAC THEN 525 ASM_REWRITE_TAC[SUBSET_REFL], 526 527 REPEAT STRIP_TAC THEN 528 `(v = m' - SUC m) /\ (m' >= SUC m)` by DECIDE_TAC THEN 529 `(FUNPOW fw m w n) SUBSET (FUNPOW fw (SUC m) w n)` by ( 530 REWRITE_TAC [FUNPOW_SUC] THEN 531 `?x. FUNPOW fw m w = x` by PROVE_TAC[] THEN 532 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_UNION] 533 ) THEN 534 PROVE_TAC[SUBSET_TRANS] 535 ] 536 ) THEN 537 538 539 SUBGOAL_TAC `!n:num. (w n SUBSET w' n)` THEN1 ( 540 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, 541 GSYM RIGHT_EXISTS_AND_THM, GSPECIFICATION, IN_UNIV] THEN 542 REPEAT STRIP_TAC THEN 543 EXISTS_TAC ``0:num`` THEN 544 ASM_REWRITE_TAC[FUNPOW_0] 545 ) THEN 546 547 548 SUBGOAL_TAC `!n:num. w' n SUBSET (A:('a,'a) alternating_semi_automaton).S` THEN1 ( 549 GSYM_NO_TAC 4 (*Def fw*) THEN 550 ASM_SIMP_TAC std_ss [SUBSET_DEF, IN_BIGUNION, 551 GSYM RIGHT_EXISTS_AND_THM, GSPECIFICATION, IN_UNIV] THEN 552 PROVE_TAC[SUBSET_DEF] 553 ) THEN 554 555 SUBGOAL_TAC `!n. ?m0. !m. m >= m0 ==> (FUNPOW fw m w n = FUNPOW fw m0 w n)` THEN1 ( 556 CCONTR_TAC THEN 557 FULL_SIMP_TAC std_ss [] THEN 558 559 `?z. (!m. CARD (FUNPOW fw m w n) <= z) /\ !z'. z' < z ==> ~!m. CARD (FUNPOW fw m w n) <= z'` by 560 METIS_TAC[CARD_SUBSET, 561 EXISTS_LEAST_CONV ``?z. !m. CARD (FUNPOW fw m (w:num->'a set) n) <= z``] THEN 562 SUBGOAL_TAC `?m0. CARD (FUNPOW fw m0 w n) = z` THEN1 ( 563 CCONTR_TAC THEN 564 FULL_SIMP_TAC std_ss [] THEN 565 `!x z. (x <= z /\ (~(x = z))) ==> (x <= PRE z /\ PRE z < z)` by DECIDE_TAC THEN 566 `!m:num. CARD (FUNPOW fw m w n) <= (PRE z) /\ PRE z < z` by METIS_TAC[] THEN 567 METIS_TAC[] 568 ) THEN 569 570 `?m1. m1 >= m0 /\ ~(FUNPOW fw m1 w n = FUNPOW fw m0 w n)` by METIS_TAC[] THEN 571 `FUNPOW fw m0 w n PSUBSET FUNPOW fw m1 w n` by PROVE_TAC[PSUBSET_DEF] THEN 572 `z < CARD (FUNPOW fw m1 w n)` by PROVE_TAC[CARD_PSUBSET, SUBSET_FINITE] THEN 573 `!x y. ~(x <= y /\ y < x)` by DECIDE_TAC THEN 574 PROVE_TAC[] 575 ) THEN 576 577 SUBGOAL_TAC `!n. ?m0. (w' n = (FUNPOW fw m0 w n)) /\ 578 (!m. m >= m0 ==> (FUNPOW fw m w n = FUNPOW fw m0 w n))` THEN1 ( 579 GSYM_NO_TAC 6 THEN 580 ASM_SIMP_TAC std_ss [] THEN 581 REPEAT STRIP_TAC THEN 582 `?m0. !m. m >= m0 ==> (FUNPOW fw m w n = FUNPOW fw m0 w n)` by PROVE_TAC[] THEN 583 EXISTS_TAC ``m0:num`` THEN 584 ASM_REWRITE_TAC[EXTENSION] THEN 585 SIMP_TAC std_ss [GSYM RIGHT_EXISTS_AND_THM, IN_BIGUNION, 586 GSPECIFICATION, IN_UNIV] THEN 587 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 588 Cases_on `m >= m0` THENL [ 589 PROVE_TAC[], 590 591 `m0 >= m` by DECIDE_TAC THEN 592 PROVE_TAC[SUBSET_DEF] 593 ], 594 595 PROVE_TAC[] 596 ] 597 ) THEN 598 599 600 SUBGOAL_TAC `!n s m. (s IN (FUNPOW fw m w n)) ==> 601 (P_SEM (FUNPOW fw m w (SUC n)) ((A:('a, 'a) alternating_semi_automaton).R s (i n)))` THEN1 ( 602 Induct_on `m` THENL [ 603 ASM_SIMP_TAC std_ss [FUNPOW_0], 604 605 `?x. FUNPOW fw m w = x` by PROVE_TAC[] THEN 606 ONCE_REWRITE_TAC [FUNPOW_SUC] THEN 607 FULL_SIMP_TAC std_ss [IN_UNION, GSPECIFICATION] THEN 608 PROVE_TAC[SUBSET_UNION, IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM] 609 ] 610 ) THEN 611 612 EXISTS_TAC ``w':num->'a set`` THEN 613 REPEAT STRIP_TAC THENL [ 614 ASM_REWRITE_TAC[], 615 ASM_REWRITE_TAC[], 616 PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM], 617 618 SUBGOAL_TAC `?l. (w' n = FUNPOW fw l w n) /\ 619 (!m. m >= l ==> (FUNPOW fw m w n = FUNPOW fw l w n)) /\ 620 (w' (SUC n) = FUNPOW fw l w (SUC n)) /\ 621 (!m. m >= l ==> (FUNPOW fw m w (SUC n) = FUNPOW fw l w (SUC n)))` THEN1 ( 622 `?m0. (w' n = FUNPOW fw m0 w n) /\ !m. m >= m0 ==> (FUNPOW fw m w n = FUNPOW fw m0 w n)` 623 by METIS_TAC[] THEN 624 `?m1. (w' (SUC n) = FUNPOW fw m1 w (SUC n)) /\ !m. m >= m1 ==> (FUNPOW fw m w (SUC n) = FUNPOW fw m1 w (SUC n))` by METIS_TAC[] THEN 625 SUBGOAL_TAC `?l. l >= m0 /\ l >= m1` THEN1 ( 626 Cases_on `m0 >= m1` THENL [ 627 EXISTS_TAC ``m0:num``, 628 EXISTS_TAC ``m1:num`` 629 ] THEN 630 ASM_SIMP_TAC arith_ss []) THEN 631 EXISTS_TAC ``l:num`` THEN 632 `!m:num. m >= l ==> (m >= m0 /\ m >= m1)` by DECIDE_TAC THEN 633 PROVE_TAC[] 634 ) THEN 635 EQ_TAC THENL [ 636 PROVE_TAC[SUBSET_DEF], 637 638 `?x. FUNPOW fw l w = x` by PROVE_TAC[] THEN 639 `w' (SUC n) = x (SUC n)` by PROVE_TAC[] THEN 640 `SUC l >= l` by DECIDE_TAC THEN 641 `w' n = (fw x) n` by METIS_TAC[FUNPOW_SUC, FUNPOW_0] THEN 642 ASM_SIMP_TAC std_ss [IN_UNION, GSPECIFICATION] 643 ] 644 ] 645); 646 647 648 649val COLLAPSED_ALTERNATING_RUN___EQ_COLLAPSED___THM = 650 store_thm 651 ("COLLAPSED_ALTERNATING_RUN___EQ_COLLAPSED___THM", 652 653``!A fi i i' r. 654 ((IS_VALID_ALTERNATING_SEMI_AUTOMATON A) /\ 655 IS_VALID_INPUT_ENCODING A fi /\ 656 IS_VALID_ENCODED_INPUT A fi i i') ==> 657 658 (ALTERNATING_RUN A i r ==> (?w. 659 (!n. (COLLAPSED_ALTERNATING_RUN r) n SUBSET w n) /\ 660 IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i' w))``, 661 662 663 PROVE_TAC[COLLAPSED_ALTERNATING_RUN___IMPL_COLLAPSED___THM, 664 IMPL_COLLAPSED_RUN___EQ_COLLAPSED_RUN___ENRICHMENT]); 665 666 667val DECOLLAPSED_RUN___EQ_COLLAPSED___THM = 668 store_thm 669 ("DECOLLAPSED_RUN___EQ_COLLAPSED___THM", 670 671 ``!A fi i i' r. 672 ((IS_VALID_ALTERNATING_SEMI_AUTOMATON A) /\ 673 IS_VALID_INPUT_ENCODING A fi /\ 674 IS_VALID_ENCODED_INPUT A fi i i') ==> 675 676 (IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A fi) i' r ==> 677 ALTERNATING_RUN A i (DECOLLAPSED_RUN r))``, 678 679 PROVE_TAC[IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 680 EQ_COLLAPSED_RUN___IMPLIES___IMPL_COLLAPSED_RUN, 681 DECOLLAPSED_RUN___IMPL_COLLAPSED___THM]); 682 683 684val NDET_TRUE___A_TRUE___IMPL = 685 store_thm 686 ("NDET_TRUE___A_TRUE___IMPL", 687 688 ``!A fi i i'. (IS_VALID_ALTERNATING_AUTOMATON A /\ (A.AC = TRUE) /\ 689 IS_VALID_INPUT_ENCODING A.A fi /\ 690 IS_VALID_ENCODED_INPUT A.A fi i i') ==> 691 ((A_SEM i' (A_NDET (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A.A fi, A_TRUE))) = ALT_SEM A i)``, 692 693 REWRITE_TAC[IS_VALID_ALTERNATING_AUTOMATON_def] THEN 694 REPEAT STRIP_TAC THEN 695 ASM_REWRITE_TAC[A_SEM_def, ALT_SEM_def, ALT_ACCEPT_COND_SEM_def] THEN 696 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 697 PROVE_TAC[IS_VALID_ENCODED_INPUT_def], 698 PROVE_TAC[DECOLLAPSED_RUN___IMPL_COLLAPSED___THM], 699 PROVE_TAC[COLLAPSED_ALTERNATING_RUN___IMPL_COLLAPSED___THM] 700 ]); 701 702 703 704val NDET_TRUE___A_TRUE___EQ = 705 store_thm 706 ("NDET_TRUE___A_TRUE___EQ", 707 708 ``!A fi i i'. (IS_VALID_ALTERNATING_AUTOMATON A /\ (A.AC = TRUE) /\ 709 IS_VALID_INPUT_ENCODING A.A fi /\ 710 IS_VALID_ENCODED_INPUT A.A fi i i') ==> 711 ((A_SEM i' (A_NDET (EQ_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A.A fi, A_TRUE))) = ALT_SEM A i)``, 712 713 REWRITE_TAC[IS_VALID_ALTERNATING_AUTOMATON_def] THEN 714 REPEAT STRIP_TAC THEN 715 ASM_REWRITE_TAC[A_SEM_def, ALT_SEM_def, ALT_ACCEPT_COND_SEM_def] THEN 716 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 717 PROVE_TAC[IS_VALID_ENCODED_INPUT_def], 718 `FINITE A.A.S` by FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def] THEN 719 `IS_SYMBOLIC_RUN_THROUGH_SEMI_AUTOMATON (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A.A fi) i' w` by 720 PROVE_TAC[EQ_COLLAPSED_RUN___IMPLIES___IMPL_COLLAPSED_RUN] THEN 721 PROVE_TAC[DECOLLAPSED_RUN___IMPL_COLLAPSED___THM], 722 723 PROVE_TAC[COLLAPSED_ALTERNATING_RUN___IMPL_COLLAPSED___THM, 724 IMPL_COLLAPSED_RUN___EQ_COLLAPSED_RUN___ENRICHMENT] 725 ]); 726 727 728 729 730val NDET_G___A_UNIVERSALLY_TOTAL_WEAK_CO_BUECHI___IMPL = 731 store_thm 732 ("NDET_G___A_UNIVERSALLY_TOTAL_WEAK_CO_BUECHI___IMPL", 733 734 ``!A fi i i' ac. (IS_VALID_ALTERNATING_AUTOMATON A /\ 735 IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A.A /\ 736 (A.AC = WEAK_CO_BUECHI ac) /\ 737 IS_VALID_INPUT_ENCODING A.A fi /\ 738 IS_VALID_ENCODED_INPUT A.A fi i i') ==> 739 ((A_SEM i' (A_NDET (IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON A.A fi, 740 ACCEPT_COND_G (P_NOT(P_PROP_DISJUNCTION (SET_TO_LIST ac)))))) = ALT_SEM A i)``, 741 742 REWRITE_TAC[IS_VALID_ALTERNATING_AUTOMATON_def] THEN 743 REPEAT STRIP_TAC THEN 744 `ac SUBSET A.A.S` by PROVE_TAC[IS_VALID_ACCEPTANCE_COMPONENT_def] THEN 745 `FINITE ac` by PROVE_TAC[SUBSET_FINITE, 746 IS_VALID_ALTERNATING_SEMI_AUTOMATON_def] THEN 747 ASM_SIMP_TAC std_ss [ALT_SEM_def, ALT_ACCEPT_COND_SEM_THM, 748 ACCEPT_COND_G_def, INPUT_RUN_PATH_UNION_def, INPUT_RUN_STATE_UNION_def, 749 IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def, P_PROP_DISJUNCTION_SEM, 750 MEM_SET_TO_LIST, symbolic_semi_automaton_REWRITES, A_SEM_def, 751 ACCEPT_COND_SEM_def, ACCEPT_COND_SEM_TIME_def, P_SEM_THM, 752 EXISTS_MEM, IN_UNION, IN_DIFF] THEN 753 SIMP_TAC std_ss [GSYM IMPL_COLLAPSED_ALTERNATING_SEMI_AUTOMATON_def] THEN 754 755 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 756 PROVE_TAC[IS_VALID_ENCODED_INPUT_def], 757 758 EXISTS_TAC ``DECOLLAPSED_RUN w`` THEN 759 REPEAT STRIP_TAC THENL [ 760 PROVE_TAC[DECOLLAPSED_RUN___IMPL_COLLAPSED___THM], 761 762 `~(w' n IN w n)` by PROVE_TAC[] THEN 763 `IS_REACHABLE_BY_RUN (w' n, n) (DECOLLAPSED_RUN w)` by 764 PROVE_TAC[IS_PATH_THROUGH_RUN___IS_REACHABLE_BY_RUN] THEN 765 PROVE_TAC[IS_REACHABLE_BY_DECOLLAPSED_RUN] 766 ], 767 768 EXISTS_TAC ``COLLAPSED_ALTERNATING_RUN r`` THEN 769 REPEAT STRIP_TAC THENL [ 770 PROVE_TAC[COLLAPSED_ALTERNATING_RUN___IMPL_COLLAPSED___THM], 771 772 SIMP_TAC std_ss [COLLAPSED_ALTERNATING_RUN_def, GSPECIFICATION] THEN 773 Cases_on `s IN ac` THEN ASM_REWRITE_TAC[] THEN 774 REPEAT STRIP_TAC THENL [ 775 `NO_EMPTY_SET_IN_RUN r` by 776 PROVE_TAC[UNIVERSALLY_TOTAL_NO_EMPTY_SET_IN_RUN] THEN 777 PROVE_TAC[NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_AND_REACHABLE_STATE_EXISTS], 778 779 PROVE_TAC[SUBSET_DEF] 780 ] 781 ] 782 ]); 783 784 785 786 787 788 789 790 791val _ = export_theory(); 792