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*) 14 15open infinite_pathTheory pred_setTheory listTheory pairTheory xprop_logicTheory 16 containerTheory prop_logicTheory set_lemmataTheory prim_recTheory 17 tuerk_tacticsLib temporal_deep_mixedTheory arithmeticTheory numLib; 18open Sanity; 19 20val _ = hide "S"; 21val _ = hide "I"; 22 23(* 24show_assums := false; 25show_assums := true; 26show_types := true; 27show_types := false; 28quietdec := false; 29*) 30 31 32val _ = new_theory "alternating_omega_automata"; 33 34 35(*****************************************************************************) 36(* symbolic representation of alternating automata *) 37(*****************************************************************************) 38val alternating_acceptance_condition_def = 39Hol_datatype 40`alternating_acceptance_condition = 41 TRUE | 42 FALSE | 43 INITIAL of 'state set | 44 CO_INITIAL of 'state set | 45 BUECHI of 'state set | 46 CO_BUECHI of 'state set | 47 PARITY of 'state->num | 48 WEAK_PARITY of 'state->num | 49 WEAK_BUECHI of 'state set | 50 WEAK_CO_BUECHI of 'state set`; 51 52val alternating_semi_automaton_def = 53Hol_datatype 54`alternating_semi_automaton = 55 <| S: 'state set; (*set of all used statevariables *) 56 I: 'input set; 57 S0: 'state prop_logic; (*initial condition*) 58 R: 'state -> 'input -> 'state prop_logic (*transition function*) 59 |>`; 60 61val alternating_automaton_def = 62Hol_datatype 63`alternating_automaton = 64 <| A: ('input, 'state) alternating_semi_automaton; 65 AC: 'state alternating_acceptance_condition (*acceptance condition*) 66 |>`; 67 68val alternating_run_def = 69Hol_datatype 70`alternating_run = 71 <| S0: 'state set; (*choosen initial states*) 72 R: 'state -> num -> 'state set (*choosen transitions*) 73 |>`; 74 75 76val alternating_semi_automaton_S = DB.fetch "-" "alternating_semi_automaton_S"; 77val alternating_semi_automaton_I = DB.fetch "-" "alternating_semi_automaton_I"; 78val alternating_semi_automaton_S0 = DB.fetch "-" "alternating_semi_automaton_S0"; 79val alternating_semi_automaton_R = DB.fetch "-" "alternating_semi_automaton_R"; 80val alternating_automaton_A = DB.fetch "-" "alternating_automaton_A"; 81val alternating_automaton_AC = DB.fetch "-" "alternating_automaton_AC"; 82 83val alternating_run_S0 = DB.fetch "-" "alternating_run_S0"; 84val alternating_run_R = DB.fetch "-" "alternating_run_R"; 85 86 87val alternating_automaton_REWRITES = save_thm("alternating_automaton_REWRITES", 88 LIST_CONJ [ 89 alternating_semi_automaton_S, 90 alternating_semi_automaton_I, 91 alternating_semi_automaton_S0, 92 alternating_semi_automaton_R, 93 alternating_automaton_A, 94 alternating_automaton_AC, 95 alternating_run_S0, 96 alternating_run_R]); 97 98 99(*============================================================ 100= Semantic 101============================================================*) 102 103val IS_REACHABLE_BY_RUN_def = 104Define 105`(IS_REACHABLE_BY_RUN (s, 0) r = (s IN r.S0)) /\ 106 (IS_REACHABLE_BY_RUN (s, SUC n) r = ( 107 ?s'. IS_REACHABLE_BY_RUN (s', n) r /\ (s IN r.R s' n)))`; 108 109val ALTERNATING_RUN_def = 110Define 111`ALTERNATING_RUN (A:('input, 'state) alternating_semi_automaton) 112 (i:(num -> 'input)) 113 (r:'state alternating_run) = ( 114 (r.S0 SUBSET A.S) /\ (P_SEM (r.S0) A.S0) /\ 115 (!n s. (r.R s n SUBSET A.S)) /\ 116 (!n s. 117 (IS_REACHABLE_BY_RUN (s, n) r) ==> 118 (P_SEM (r.R s n) (A.R s (i n)))))`; 119 120val IS_PATH_THROUGH_RUN_def = 121Define 122`IS_PATH_THROUGH_RUN w r = ((w 0 IN r.S0) /\ !n. 123 ((w (SUC n)) IN r.R (w n) n))`; 124 125 126val ALT_ACCEPT_COND_SEM_def = 127Define 128`(ALT_ACCEPT_COND_SEM TRUE i = T) /\ 129 (ALT_ACCEPT_COND_SEM FALSE i = F) /\ 130 (ALT_ACCEPT_COND_SEM (INITIAL S) i = (i 0 IN S)) /\ 131 (ALT_ACCEPT_COND_SEM (CO_INITIAL S) i = ~(i 0 IN S)) /\ 132 (ALT_ACCEPT_COND_SEM (BUECHI S) i = 133 (~(((INF_ELEMENTS_OF_PATH i) INTER S) = EMPTY))) /\ 134 (ALT_ACCEPT_COND_SEM (PARITY f) i = 135 (?n. EVEN n /\ (?s. (s IN (INF_ELEMENTS_OF_PATH i)) /\ (n = (f s))) /\ 136 (!s. (s IN (INF_ELEMENTS_OF_PATH i)) ==> (n <= (f s))))) /\ 137 (ALT_ACCEPT_COND_SEM (WEAK_PARITY f) i = 138 (?n. EVEN n /\ (?s. (s IN (ELEMENTS_OF_PATH i)) /\ (n = (f s))) /\ 139 (!s. (s IN (ELEMENTS_OF_PATH i)) ==> (n <= (f s))))) /\ 140 (ALT_ACCEPT_COND_SEM (CO_BUECHI S) i = 141 (((INF_ELEMENTS_OF_PATH i) INTER S) = EMPTY)) /\ 142 (ALT_ACCEPT_COND_SEM (WEAK_BUECHI S) i = 143 (~(((ELEMENTS_OF_PATH i) INTER S) = EMPTY))) /\ 144 (ALT_ACCEPT_COND_SEM (WEAK_CO_BUECHI S) i = 145 (((ELEMENTS_OF_PATH i) INTER S) = EMPTY))`; 146 147 148val ALT_SEM_def = 149Define 150`ALT_SEM A i = ((!n. i n IN A.A.I) /\ 151 ?r. ALTERNATING_RUN A.A i r /\ (!w. IS_PATH_THROUGH_RUN w r ==> ALT_ACCEPT_COND_SEM A.AC w))`; 152 153 154val ALT_AUTOMATON_EQUIV_def = 155Define 156`ALT_AUTOMATON_EQUIV A A' = 157 (!i. ALT_SEM A i = ALT_SEM A' i)`; 158 159(*============================================================ 160= Lemmata and Definitions about Acceptance Component 161============================================================*) 162 163val ALT_ACCEPT_COND_SEM_THM_1 = 164 prove ( 165 ``!S i. ALT_ACCEPT_COND_SEM (BUECHI S) i = (?s. s IN S /\ (!n. ?m. m > n /\ (i m = s)))``, 166 167 SIMP_TAC arith_ss [ALT_ACCEPT_COND_SEM_def, INF_ELEMENTS_OF_PATH_def, 168 INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] THEN 169 PROVE_TAC[]); 170 171val ALT_ACCEPT_COND_SEM_THM_2 = 172 prove (``!S i. ALT_ACCEPT_COND_SEM (WEAK_BUECHI S) i = (?n. i n IN S)``, 173 174 SIMP_TAC arith_ss [ALT_ACCEPT_COND_SEM_def, ELEMENTS_OF_PATH_def, 175 INTER_DEF, EXTENSION, NOT_IN_EMPTY, GSPECIFICATION] THEN 176 PROVE_TAC[]); 177 178val ALT_ACCEPT_COND_SEM_THM_3 = 179 prove ( 180 ``!S i. (ALT_ACCEPT_COND_SEM (CO_BUECHI S) i = 181 ~ALT_ACCEPT_COND_SEM (BUECHI S) i) /\ 182 (ALT_ACCEPT_COND_SEM (WEAK_CO_BUECHI S) i = 183 ~ALT_ACCEPT_COND_SEM (WEAK_BUECHI S) i) /\ 184 (ALT_ACCEPT_COND_SEM (CO_INITIAL S) i = 185 ~ALT_ACCEPT_COND_SEM (INITIAL S) i)``, 186 187 SIMP_TAC arith_ss [ALT_ACCEPT_COND_SEM_def]); 188 189 190val ALT_ACCEPT_COND_SEM_THM = LIST_CONJ [ 191 ALT_ACCEPT_COND_SEM_THM_1, 192 ALT_ACCEPT_COND_SEM_THM_2, 193 ALT_ACCEPT_COND_SEM_THM_3]; 194val _ = save_thm("ALT_ACCEPT_COND_SEM_THM",ALT_ACCEPT_COND_SEM_THM); 195 196 197val ALT_ACCEPT_COND_NEG_def = 198Define 199`(ALT_ACCEPT_COND_NEG TRUE = FALSE) /\ 200 (ALT_ACCEPT_COND_NEG FALSE = TRUE) /\ 201 (ALT_ACCEPT_COND_NEG (INITIAL S) = (CO_INITIAL S)) /\ 202 (ALT_ACCEPT_COND_NEG (CO_INITIAL S) = (INITIAL S)) /\ 203 (ALT_ACCEPT_COND_NEG (BUECHI S) = (CO_BUECHI S)) /\ 204 (ALT_ACCEPT_COND_NEG (CO_BUECHI S) = (BUECHI S)) /\ 205 (ALT_ACCEPT_COND_NEG (WEAK_BUECHI S) = (WEAK_CO_BUECHI S)) /\ 206 (ALT_ACCEPT_COND_NEG (WEAK_CO_BUECHI S) = (WEAK_BUECHI S)) /\ 207 (ALT_ACCEPT_COND_NEG (PARITY f) = (PARITY (\n. SUC(f n)))) /\ 208 (ALT_ACCEPT_COND_NEG (WEAK_PARITY f) = (WEAK_PARITY (\n. SUC(f n))))`; 209 210 211val ALT_ACCEPT_COND_NEG_SEM = 212 store_thm 213 ("ALT_ACCEPT_COND_NEG_SEM", 214 ``!a i. ((?f. a = PARITY f) ==> ~(INF_ELEMENTS_OF_PATH i = EMPTY)) ==> (ALT_ACCEPT_COND_SEM (ALT_ACCEPT_COND_NEG a) i = ~ALT_ACCEPT_COND_SEM a i)``, 215 216 REPEAT STRIP_TAC THEN 217 Cases_on `a` THEN 218 REWRITE_TAC[ALT_ACCEPT_COND_NEG_def, ALT_ACCEPT_COND_SEM_def] THENL [ 219 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 220 FULL_SIMP_TAC arith_ss [] THEN 221 `f s' <= f s` by PROVE_TAC[] THEN 222 `SUC (f s) <= (SUC (f s'))` by PROVE_TAC[] THEN 223 `f s' = f s` by DECIDE_TAC THEN 224 PROVE_TAC[EVEN], 225 226 227 FULL_SIMP_TAC arith_ss [GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM, 228 EVEN, GSYM LEFT_FORALL_OR_THM, GSYM RIGHT_FORALL_OR_THM] THEN 229 `?n. (?s. s IN INF_ELEMENTS_OF_PATH i /\ (f s = n)) /\ 230 !n'. n' < n ==> ~?s. s IN INF_ELEMENTS_OF_PATH i /\ (f s = n')` by ( 231 ASSUME_TAC (EXISTS_LEAST_CONV ``?n:num. (?s:'a. s IN (INF_ELEMENTS_OF_PATH i) /\ (f s = n))``) THEN 232 METIS_TAC[MEMBER_NOT_EMPTY] 233 ) THEN 234 `!s'. s' IN INF_ELEMENTS_OF_PATH i ==> (n <= f s')` by ( 235 CCONTR_TAC THEN 236 FULL_SIMP_TAC std_ss [] THEN 237 `f s' < n` by DECIDE_TAC THEN 238 PROVE_TAC[] 239 ) THEN 240 METIS_TAC[] 241 ], 242 243 244 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 245 FULL_SIMP_TAC arith_ss [] THEN 246 `f s' <= f s` by PROVE_TAC[] THEN 247 `SUC (f s) <= (SUC (f s'))` by PROVE_TAC[] THEN 248 `f s' = f s` by DECIDE_TAC THEN 249 PROVE_TAC[EVEN], 250 251 FULL_SIMP_TAC arith_ss [GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM, 252 EVEN, GSYM LEFT_FORALL_OR_THM, GSYM RIGHT_FORALL_OR_THM] THEN 253 `?n. (?s. s IN ELEMENTS_OF_PATH i /\ (f s = n)) /\ 254 !n'. n' < n ==> ~?s. s IN ELEMENTS_OF_PATH i /\ (f s = n')` by ( 255 ASSUME_TAC (EXISTS_LEAST_CONV ``?n:num. (?s:'a. s IN (ELEMENTS_OF_PATH i) /\ (f s = n))``) THEN 256 METIS_TAC[MEMBER_NOT_EMPTY, ELEMENTS_OF_PATH_NOT_EMPTY] 257 ) THEN 258 `!s'. s' IN ELEMENTS_OF_PATH i ==> (n <= f s')` by ( 259 CCONTR_TAC THEN 260 FULL_SIMP_TAC std_ss [] THEN 261 `f s' < n` by DECIDE_TAC THEN 262 PROVE_TAC[] 263 ) THEN 264 METIS_TAC[] 265 ] 266 ]); 267 268 269 270(*============================================================ 271= Min Semantic 272============================================================*) 273 274val ALTERNATING_MIN_RUN_def = 275Define 276`ALTERNATING_MIN_RUN (A:('input, 'state) alternating_semi_automaton) 277 (i:(num -> 'input)) 278 (r:'state alternating_run) = ( 279 (r.S0 SUBSET A.S) /\ (P_SEM_MIN (r.S0) A.S0) /\ 280 (!n s. (r.R s n SUBSET A.S)) /\ 281 (!n s. 282 (IS_REACHABLE_BY_RUN (s, n) r) ==> 283 (P_SEM_MIN (r.R s n) (A.R s (i n)))))`; 284 285 286val ALT_SEM_MIN_def = 287Define 288`ALT_SEM_MIN A i = ((!n. i n IN A.A.I) /\ 289 ?r. ALTERNATING_MIN_RUN A.A i r /\ (!w. IS_PATH_THROUGH_RUN w r ==> ALT_ACCEPT_COND_SEM A.AC w))`; 290 291 292val IS_ALTERNATING_SUBRUN_def = 293Define 294`IS_ALTERNATING_SUBRUN r r' = 295 (r.S0 SUBSET r'.S0 /\ !s n. (r.R s n SUBSET r'.R s n))`; 296 297 298val IS_PATH_THROUGH_SUBRUN_THM = 299 store_thm 300 ("IS_PATH_THROUGH_SUBRUN_THM", 301 ``!w r r'. (IS_ALTERNATING_SUBRUN r' r /\ IS_PATH_THROUGH_RUN w r') ==> 302 IS_PATH_THROUGH_RUN w r``, 303 304 SIMP_TAC std_ss [IS_ALTERNATING_SUBRUN_def, IS_PATH_THROUGH_RUN_def] THEN 305 PROVE_TAC[SUBSET_DEF]); 306 307 308val SUBRUN_REACHABLE_STATES = 309 store_thm 310 ("SUBRUN_REACHABLE_STATES", 311 ``!r r'. (IS_ALTERNATING_SUBRUN r r') ==> 312 (!s n. (IS_REACHABLE_BY_RUN (s, n) r ==> 313 IS_REACHABLE_BY_RUN (s, n) r'))``, 314 315 REWRITE_TAC[IS_ALTERNATING_SUBRUN_def] THEN 316 REPEAT GEN_TAC THEN STRIP_TAC THEN 317 Induct_on `n` THENL [ 318 REWRITE_TAC[IS_REACHABLE_BY_RUN_def] THEN 319 PROVE_TAC[SUBSET_DEF], 320 321 REWRITE_TAC[IS_REACHABLE_BY_RUN_def] THEN 322 PROVE_TAC[SUBSET_DEF] 323 ]); 324 325 326val ALTERNATING_RUN___ALTERNATING_MIN_RUN_EXISTS = 327 store_thm 328 ("ALTERNATING_RUN___ALTERNATING_MIN_RUN_EXISTS", 329 ``!A i r. ALTERNATING_RUN A i r ==> 330 (?r'. ALTERNATING_MIN_RUN A i r' /\ IS_ALTERNATING_SUBRUN r' r)``, 331 332 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def, ALTERNATING_MIN_RUN_def] THEN 333 REPEAT STRIP_TAC THENL [ 334 `?r'. r' = (alternating_run (@S0'. S0' SUBSET r.S0 /\ 335 P_SEM_MIN S0' A.S0) (\s n. @S'. S' SUBSET r.R s n /\ 336 (IS_REACHABLE_BY_RUN (s, n) r ==> 337 P_SEM_MIN S' (A.R s (i n)))))` by PROVE_TAC[] THEN 338 EXISTS_TAC ``r':'b alternating_run`` THEN 339 SUBGOAL_THEN ``IS_ALTERNATING_SUBRUN (r':'b alternating_run) r`` ASSUME_TAC THEN1 ( 340 ASM_SIMP_TAC std_ss [IS_ALTERNATING_SUBRUN_def, 341 alternating_run_S0, alternating_run_R] THEN 342 REPEAT STRIP_TAC THENL [ 343 SELECT_ELIM_TAC THEN 344 PROVE_TAC[P_SEM_MIN_MODEL_EXISTS], 345 346 SELECT_ELIM_TAC THEN 347 REPEAT STRIP_TAC THEN 348 Cases_on `IS_REACHABLE_BY_RUN (s, n) r` THENL [ 349 PROVE_TAC[P_SEM_MIN_MODEL_EXISTS], 350 PROVE_TAC[SUBSET_REFL] 351 ] 352 ]) THEN 353 354 REPEAT STRIP_TAC THENL [ 355 PROVE_TAC[SUBSET_TRANS, IS_ALTERNATING_SUBRUN_def], 356 357 ASM_REWRITE_TAC[alternating_run_S0] THEN 358 SELECT_ELIM_TAC THEN 359 PROVE_TAC[P_SEM_MIN_MODEL_EXISTS], 360 361 PROVE_TAC[SUBSET_TRANS, IS_ALTERNATING_SUBRUN_def], 362 363 `IS_REACHABLE_BY_RUN (s, n) r` by PROVE_TAC[SUBRUN_REACHABLE_STATES] THEN 364 RES_TAC THEN 365 ASM_REWRITE_TAC[alternating_run_R] THEN 366 BETA_TAC THEN 367 SELECT_ELIM_TAC THEN 368 REPEAT STRIP_TAC THENL [ 369 PROVE_TAC[P_SEM_MIN_MODEL_EXISTS], 370 fs [] 371 ], 372 373 ASM_REWRITE_TAC[] 374 ] 375 ]); 376 377 378val ALT_SEM___ALT_SEM_MIN___EQUIV = 379 store_thm 380 ("ALT_SEM___ALT_SEM_MIN___EQUIV", 381 ``!A i. ALT_SEM A i = ALT_SEM_MIN A i``, 382 383 REWRITE_TAC [ALT_SEM_def, ALT_SEM_MIN_def] THEN 384 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL [ 385 PROVE_TAC[ALTERNATING_RUN___ALTERNATING_MIN_RUN_EXISTS, IS_PATH_THROUGH_SUBRUN_THM], 386 387 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def, ALTERNATING_MIN_RUN_def, P_SEM_MIN_def] THEN 388 METIS_TAC[] 389 ]); 390 391 392(*============================================================ 393= Negation of alternating automata 394============================================================*) 395 396val ALT_SEMI_AUTOMATON_NEG_def = 397Define 398 `ALT_SEMI_AUTOMATON_NEG A = alternating_semi_automaton A.S A.I (P_DUAL A.S0) 399 (\s i. P_DUAL (A.R s i))`; 400 401 402val ALT_AUTOMATON_NEG_def = 403Define 404 `ALT_AUTOMATON_NEG A = (alternating_automaton (ALT_SEMI_AUTOMATON_NEG A.A) (ALT_ACCEPT_COND_NEG A.AC))`; 405 406 407 408val ALT_AUTOMATON_NEG_NEG_SEM = 409 store_thm 410 ("ALT_AUTOMATON_NEG_NEG_SEM", 411 412 ``!A. (FINITE A.A.S) ==> (ALT_AUTOMATON_EQUIV (ALT_AUTOMATON_NEG (ALT_AUTOMATON_NEG A)) A)``, 413 414 SIMP_TAC std_ss [ALT_AUTOMATON_EQUIV_def, ALT_SEM_def, ALT_AUTOMATON_NEG_def, 415 P_DUAL_def, 416 ALT_ACCEPT_COND_NEG_SEM, ALT_SEMI_AUTOMATON_NEG_def, 417 alternating_automaton_REWRITES, 418 ALTERNATING_RUN_def, P_SEM_MIN_def, P_SEM_THM, 419 P_NEGATE_VARS_SEM, DIFF_DIFF_INTER, INTER_UNIV] THEN 420 REPEAT STRIP_TAC THEN 421 REPEAT BOOL_EQ_STRIP_TAC THEN 422 EXISTS_EQ_STRIP_TAC THEN 423 REPEAT BOOL_EQ_STRIP_TAC THEN 424 FORALL_EQ_STRIP_TAC THEN 425 Cases_on `IS_PATH_THROUGH_RUN w r` THEN ASM_REWRITE_TAC[] THEN 426 `!n:num. (w n) IN A.A.S` by (Cases_on `n` THEN 427 PROVE_TAC[SUBSET_DEF, IS_PATH_THROUGH_RUN_def]) THEN 428 PROVE_TAC[INF_ELEMENTS_OF_PATH_NOT_EMPTY, ALT_ACCEPT_COND_NEG_SEM]); 429 430 431val ALTERNATING_PRERUN_def = 432Define 433`ALTERNATING_PRERUN (A:('input, 'state) alternating_semi_automaton) 434 (i:(num -> 'input)) 435 (r:'state alternating_run) = ( 436 (r.S0 SUBSET A.S) /\ ((P_SEM (r.S0) A.S0) \/ ((r.S0 = EMPTY) /\ P_IS_CONTRADICTION A.S0)) /\ 437 (!n s. (r.R s n SUBSET A.S)) /\ 438 (!n s. 439 (IS_REACHABLE_BY_RUN (s, n) r) ==> 440 (P_SEM (r.R s n) (A.R s (i n)) \/ ((r.R s n = EMPTY) /\ P_IS_CONTRADICTION (A.R s (i n))))))`; 441 442 443val ALTERNATING_RUN_IS_PRERUN = 444 store_thm 445 ("ALTERNATING_RUN_IS_PRERUN", 446 447 ``!A i r. ALTERNATING_RUN A i r ==> ALTERNATING_PRERUN A i r``, 448 449 SIMP_TAC std_ss [ALTERNATING_RUN_def, ALTERNATING_PRERUN_def]); 450 451(*****************************************************************************) 452(* Some Classes of alternating automata *) 453(*****************************************************************************) 454 455val IS_NONDETERMINISTIC_SEMI_AUTOMATON_def = 456Define 457`IS_NONDETERMINISTIC_SEMI_AUTOMATON A = 458 ((IS_PROP_DISJUNCTION A.S0) /\ 459 (!s i. IS_PROP_DISJUNCTION (A.R s i)))`; 460 461val IS_UNIVERSAL_SEMI_AUTOMATON_def = 462Define 463`IS_UNIVERSAL_SEMI_AUTOMATON A = 464 ((IS_PROP_CONJUNCTION A.S0) /\ 465 (!s i. IS_PROP_CONJUNCTION (A.R s i)))`; 466 467val IS_DETERMINISTIC_SEMI_AUTOMATON_def = 468Define 469`IS_DETERMINISTIC_SEMI_AUTOMATON A = 470 (IS_NONDETERMINISTIC_SEMI_AUTOMATON A /\ 471 IS_UNIVERSAL_SEMI_AUTOMATON A)`; 472 473 474val IS_NONDETERMINISTIC_AUTOMATON_def = 475Define 476`IS_NONDETERMINISTIC_AUTOMATON A = 477 IS_NONDETERMINISTIC_SEMI_AUTOMATON A.A`; 478 479val IS_UNIVERSAL_AUTOMATON_def = 480Define 481`IS_UNIVERSAL_AUTOMATON A = IS_UNIVERSAL_SEMI_AUTOMATON A.A`; 482 483val IS_DETERMINISTIC_AUTOMATON_def = 484Define 485`IS_DETERMINISTIC_AUTOMATON A = IS_DETERMINISTIC_SEMI_AUTOMATON A.A`; 486 487 488val IS_VALID_ALTERNATING_SEMI_AUTOMATON_def = Define 489 `IS_VALID_ALTERNATING_SEMI_AUTOMATON A = 490 (FINITE A.S /\ FINITE A.I /\ (P_USED_VARS A.S0 SUBSET A.S) /\ 491 (!s i. (P_USED_VARS (A.R s i) SUBSET A.S)) /\ 492 IS_POSITIVE_PROP_FORMULA A.S0 /\ (!s i. IS_POSITIVE_PROP_FORMULA (A.R s i)))`; 493 494val IS_VALID_ACCEPTANCE_COMPONENT_def = Define 495 `(IS_VALID_ACCEPTANCE_COMPONENT TRUE A = T) /\ 496 (IS_VALID_ACCEPTANCE_COMPONENT FALSE A = T) /\ 497 (IS_VALID_ACCEPTANCE_COMPONENT (INITIAL s) A = (s SUBSET A.S)) /\ 498 (IS_VALID_ACCEPTANCE_COMPONENT (CO_INITIAL s) A = (s SUBSET A.S)) /\ 499 (IS_VALID_ACCEPTANCE_COMPONENT (BUECHI s) A = (s SUBSET A.S)) /\ 500 (IS_VALID_ACCEPTANCE_COMPONENT (CO_BUECHI s) A = (s SUBSET A.S)) /\ 501 (IS_VALID_ACCEPTANCE_COMPONENT (PARITY f) A = T) /\ 502 (IS_VALID_ACCEPTANCE_COMPONENT (WEAK_PARITY f) A = T) /\ 503 (IS_VALID_ACCEPTANCE_COMPONENT (WEAK_BUECHI s) A = (s SUBSET A.S)) /\ 504 (IS_VALID_ACCEPTANCE_COMPONENT (WEAK_CO_BUECHI s) A = (s SUBSET A.S))`; 505 506 507val IS_VALID_ALTERNATING_AUTOMATON_def = Define 508 `IS_VALID_ALTERNATING_AUTOMATON A = 509 ((IS_VALID_ALTERNATING_SEMI_AUTOMATON A.A) /\ 510 (IS_VALID_ACCEPTANCE_COMPONENT A.AC A.A))`; 511 512val IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def = Define 513 `IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A = 514 ((?p. P_SEM p A.S0) /\ (!s i. ?p. P_SEM p (A.R s i)))`; 515 516 517val IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def = Define 518 `IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A = 519 ((?p. ~P_SEM p A.S0) /\ (!s i. ?p. ~P_SEM p (A.R s i)))`; 520 521 522val IS_TOTAL_ALTERNATING_SEMI_AUTOMATON_def = Define 523 `IS_TOTAL_ALTERNATING_SEMI_AUTOMATON A = 524 (IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A /\ 525 IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A)`; 526 527val UNIVERSAL_IS_EXISTENTIALLY_TOTAL = 528 store_thm 529 ("UNIVERSAL_IS_EXISTENTIALLY_TOTAL", 530 531 ``!A. IS_UNIVERSAL_SEMI_AUTOMATON A ==> IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A``, 532 533 REWRITE_TAC[IS_UNIVERSAL_SEMI_AUTOMATON_def, 534 IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def, 535 IS_PROP_CONJUNCTION_def] THEN 536 REPEAT STRIP_TAC THENL [ 537 ALL_TAC, 538 `?S'. A.R s i = P_PROP_CONJUNCTION S'` by PROVE_TAC[] 539 ] THEN 540 EXISTS_TAC ``UNIV:'b set`` THEN 541 ASM_SIMP_TAC list_ss [P_PROP_CONJUNCTION_SEM, IN_UNIV]); 542 543 544val NONDETERMINISTIC_IS_UNIVERSALLY_TOTAL = 545 store_thm 546 ("NONDETERMINISTIC_IS_UNIVERSALLY_TOTAL", 547 548 ``!A. IS_NONDETERMINISTIC_SEMI_AUTOMATON A ==> IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A``, 549 550 REWRITE_TAC[IS_NONDETERMINISTIC_SEMI_AUTOMATON_def, 551 IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def, 552 IS_PROP_DISJUNCTION_def] THEN 553 REPEAT STRIP_TAC THENL [ 554 ALL_TAC, 555 `?S'. A.R s i = P_PROP_DISJUNCTION S'` by PROVE_TAC[] 556 ] THEN 557 EXISTS_TAC ``EMPTY:'b set`` THEN 558 ASM_SIMP_TAC list_ss [P_PROP_DISJUNCTION_SEM, NOT_IN_EMPTY]); 559 560 561val UNIVERSAL_EXISTENTIALLY_TOTAL_DUAL = 562 store_thm 563 ("UNIVERSAL_EXISTENTIALLY_TOTAL_DUAL", 564 ``(!A:('a, 'b) alternating_semi_automaton. IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON (ALT_SEMI_AUTOMATON_NEG A) = IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A) /\ 565(!A:('a, 'b) alternating_semi_automaton. IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON (ALT_SEMI_AUTOMATON_NEG A) = IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A)``, 566 567 SIMP_TAC std_ss [IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def, 568 IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def, 569 ALT_SEMI_AUTOMATON_NEG_def, alternating_semi_automaton_S0, 570 ALT_SEMI_AUTOMATON_NEG_def, alternating_semi_automaton_R, 571 P_DUAL_MODELS_THM, P_DUAL_def, P_NEGATE_VARS_SEM, P_SEM_THM] THEN 572 573 `!p. (UNIV:'b set) DIFF (UNIV DIFF p) = p` by 574 SIMP_TAC std_ss [EXTENSION, IN_DIFF, IN_UNIV] THEN 575 METIS_TAC[] 576 ); 577 578 579 580val IS_WEAK_ALTERNATING_SEMI_AUTOMATON_def = 581Define 582`IS_WEAK_ALTERNATING_SEMI_AUTOMATON A f = 583 (!s n S s'. (P_SEM_MIN S (A.R s n) /\ (s' IN S)) ==> (f s' <= f s))`; 584 585 586val NO_EMPTY_SET_IN_RUN_def = 587Define 588 `NO_EMPTY_SET_IN_RUN r = ((!s n. IS_REACHABLE_BY_RUN (s, n) r ==> 589 ~(r.R s n = EMPTY)) /\ ~(r.S0 = EMPTY))`; 590 591 592val UNIVERSALLY_TOTAL_NO_EMPTY_SET_IN_RUN = 593 store_thm 594 ("UNIVERSALLY_TOTAL_NO_EMPTY_SET_IN_RUN", 595 ``!A i r. (ALTERNATING_RUN A i r /\ IS_VALID_ALTERNATING_SEMI_AUTOMATON A /\ IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A) ==> NO_EMPTY_SET_IN_RUN r``, 596 597FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def, IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def, 598IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 599NO_EMPTY_SET_IN_RUN_def, IS_PROP_DISJUNCTION_def] THEN 600PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM, EMPTY_SUBSET]); 601 602 603val EXISTENTIALLY_TOTAL_PRERUN_IS_RUN = 604 store_thm 605 ("EXISTENTIALLY_TOTAL_PRERUN_IS_RUN", 606 ``!A i r. IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A ==> 607 (ALTERNATING_PRERUN A i r = ALTERNATING_RUN A i r)``, 608 609 FULL_SIMP_TAC std_ss [IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON_def, 610 ALTERNATING_PRERUN_def, ALTERNATING_RUN_def, P_IS_CONTRADICTION_def] THEN 611 PROVE_TAC[]); 612 613 614 615val ALTERNATING_PRERUN_EXISTS = 616 store_thm 617 ("ALTERNATING_PRERUN_EXISTS", 618 ``!A i. (IS_VALID_ALTERNATING_SEMI_AUTOMATON A) ==> (?r. ALTERNATING_PRERUN A i r)``, 619 620 FULL_SIMP_TAC std_ss [ALTERNATING_PRERUN_def, 621 IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 622 P_IS_CONTRADICTION_def] THEN 623 REPEAT STRIP_TAC THEN 624 EXISTS_TAC ``alternating_run (if (P_IS_CONTRADICTION A.S0) then EMPTY else A.S:'b set) 625 (\s n. if (P_IS_CONTRADICTION (A.R s (i n))) then EMPTY else A.S)`` THEN 626 REWRITE_TAC[alternating_run_S0, alternating_run_R, 627 P_IS_CONTRADICTION_def] THEN 628 REPEAT STRIP_TAC THENL [ 629 Cases_on `!P. ~P_SEM P A.S0` THEN ASM_REWRITE_TAC[SUBSET_REFL, EMPTY_SUBSET], 630 631 Cases_on `!P. ~P_SEM P A.S0` THEN ASM_REWRITE_TAC[] THEN 632 FULL_SIMP_TAC std_ss [] THEN 633 `P_SEM (P INTER A.S) A.S0` by PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] THEN 634 `P INTER A.S SUBSET A.S` by PROVE_TAC[INTER_SUBSET] THEN 635 PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM], 636 637 Cases_on `!P. ~P_SEM P (A.R s (i n))` THEN ASM_SIMP_TAC std_ss [SUBSET_REFL, EMPTY_SUBSET], 638 639 640 Cases_on `!P. ~P_SEM P (A.R s (i n))` THEN ASM_SIMP_TAC std_ss [] THEN 641 FULL_SIMP_TAC std_ss [] THEN 642 `P_SEM (P INTER A.S) (A.R s (i n))` by PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM] THEN 643 `P INTER A.S SUBSET A.S` by PROVE_TAC[INTER_SUBSET] THEN 644 PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM] 645 ]); 646 647 648val EXISTENTIALLY_TOTAL_RUN_EXISTS = 649 store_thm 650 ("EXISTENTIALLY_TOTAL_RUN_EXISTS", 651 ``!A i. (IS_VALID_ALTERNATING_SEMI_AUTOMATON A /\ IS_EXISTENTIALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A) ==> (?r. ALTERNATING_RUN A i r)``, 652 653 PROVE_TAC[EXISTENTIALLY_TOTAL_PRERUN_IS_RUN, ALTERNATING_PRERUN_EXISTS]); 654 655 656val IS_PATH_TO_def = 657Define 658 `IS_PATH_TO w r s n = ((w 0 IN r.S0) /\ (w n = s) /\ 659 (!m. m < n ==> (((w (SUC m)) IN r.R (w m) m))))`; 660 661 662val IS_PATH_THROUGH_RUN___PATH_TO = 663 store_thm 664 ("IS_PATH_THROUGH_RUN___PATH_TO", 665 ``!w r. IS_PATH_THROUGH_RUN w r ==> (!n. IS_PATH_TO w r (w n) n)``, 666 667 REWRITE_TAC [IS_PATH_THROUGH_RUN_def, IS_PATH_TO_def] THEN 668 PROVE_TAC[]); 669 670 671val REACHABLE_STATES_IN_STATES_SET = 672 store_thm 673 ("REACHABLE_STATES_IN_STATES_SET", 674 675 ``!A i r. ALTERNATING_PRERUN A i r ==> (!s n. IS_REACHABLE_BY_RUN (s, n) r ==> s IN A.S)``, 676 677 REWRITE_TAC[ALTERNATING_PRERUN_def] THEN 678 REPEAT STRIP_TAC THEN 679 Cases_on `n:num` THEN 680 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def] THEN 681 PROVE_TAC[SUBSET_DEF]); 682 683 684val PATH_TO_REACHABLE_STATES_EXISTS = 685 store_thm 686 ("PATH_TO_REACHABLE_STATES_EXISTS", 687 688``!r s n. (IS_REACHABLE_BY_RUN (s, n) r) = (?w. IS_PATH_TO w r s n)``, 689 690REWRITE_TAC [IS_PATH_TO_def] THEN 691Induct_on `n` THENL [ 692 SIMP_TAC arith_ss [IS_REACHABLE_BY_RUN_def] THEN 693 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 694 EXISTS_TAC ``(\n. s):num -> 'a`` THEN 695 BETA_TAC THEN 696 ASM_REWRITE_TAC[], 697 698 PROVE_TAC[] 699 ], 700 701 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 702 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def] THEN 703 RES_TAC THEN 704 EXISTS_TAC ``(\n'. if (n' = SUC n) then s else w n'):num->'a`` THEN 705 ASM_SIMP_TAC arith_ss [] THEN 706 REPEAT STRIP_TAC THEN 707 Cases_on `m < n` THENL [ 708 ASM_SIMP_TAC arith_ss [], 709 710 `m = n` by DECIDE_TAC THEN 711 ASM_SIMP_TAC arith_ss [] 712 ], 713 714 715 REWRITE_TAC[IS_REACHABLE_BY_RUN_def] THEN 716 `!m. m < n ==> m < SUC n` by DECIDE_TAC THEN 717 `IS_REACHABLE_BY_RUN (w n, n) r` by PROVE_TAC[] THEN 718 EXISTS_TAC ``(w:num -> 'a) n`` THEN 719 ASM_REWRITE_TAC[] THEN 720 `n < SUC n` by DECIDE_TAC THEN 721 PROVE_TAC[] 722 ] 723]); 724 725 726val IS_PATH_THROUGH_RUN___IS_REACHABLE_BY_RUN = 727 store_thm 728 ("IS_PATH_THROUGH_RUN___IS_REACHABLE_BY_RUN", 729 ``!w r. IS_PATH_THROUGH_RUN w r ==> (!n. IS_REACHABLE_BY_RUN (w n, n) r)``, 730 731 PROVE_TAC[IS_PATH_THROUGH_RUN___PATH_TO, 732 PATH_TO_REACHABLE_STATES_EXISTS]); 733 734 735val NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_AND_REACHABLE_STATE_EXISTS = 736 store_thm 737 ("NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_AND_REACHABLE_STATE_EXISTS", 738 739 ``!r s n. ((IS_REACHABLE_BY_RUN (s, n) r) /\ (NO_EMPTY_SET_IN_RUN r)) ==> 740 ?w. ((IS_PATH_THROUGH_RUN w r) /\ (w n = s))``, 741 742REWRITE_TAC [IS_PATH_THROUGH_RUN_def] THEN 743REPEAT STRIP_TAC THEN 744`?w. w = \n'. (if (n' <= n) then ((@w1. IS_PATH_TO w1 r s n) n') else 745 ((CHOOSEN_PATH {s} (\S n''. r.R S (PRE n'' + n))) (n' - n)))` by METIS_TAC[] THEN 746SUBGOAL_THEN ``!n'. IS_REACHABLE_BY_RUN (w n', n') r`` ASSUME_TAC THEN1 ( 747 Induct_on `n'` THENL [ 748 ASM_SIMP_TAC arith_ss [IS_REACHABLE_BY_RUN_def] THEN 749 SELECT_ELIM_TAC THEN 750 REPEAT STRIP_TAC THENL [ 751 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 752 PROVE_TAC[IS_PATH_TO_def] 753 ], 754 755 ASM_SIMP_TAC arith_ss [IS_REACHABLE_BY_RUN_def] THEN 756 EXISTS_TAC ``(w:num->'a) n'`` THEN 757 ASM_REWRITE_TAC[] THEN 758 Cases_on `SUC n' <= n` THENL [ 759 ASM_SIMP_TAC arith_ss [] THEN 760 SELECT_ELIM_TAC THEN 761 REPEAT STRIP_TAC THENL [ 762 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 763 FULL_SIMP_TAC arith_ss [IS_PATH_TO_def] 764 ], 765 766 Cases_on `n' <= n` THENL [ 767 `n' = n` by DECIDE_TAC THEN 768 FULL_SIMP_TAC arith_ss [] THEN 769 `(SUC n - n = SUC 0)` by DECIDE_TAC THEN 770 ASM_REWRITE_TAC [CHOOSEN_PATH_def, IN_SING] THEN 771 SIMP_TAC arith_ss [] THEN 772 SELECT_ELIM_TAC THEN 773 SELECT_ELIM_TAC THEN 774 REPEAT STRIP_TAC THENL [ 775 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 776 PROVE_TAC[NO_EMPTY_SET_IN_RUN_def, MEMBER_NOT_EMPTY], 777 PROVE_TAC[IS_PATH_TO_def] 778 ], 779 780 FULL_SIMP_TAC arith_ss [] THEN 781 `SUC n' - n = SUC (n' - n)` by DECIDE_TAC THEN 782 ASM_SIMP_TAC arith_ss [CHOOSEN_PATH_def] THEN 783 SELECT_ELIM_TAC THEN 784 REWRITE_TAC[MEMBER_NOT_EMPTY] THEN 785 UNDISCH_TAC ``IS_REACHABLE_BY_RUN (w n', n') r`` THEN 786 FULL_SIMP_TAC arith_ss [] THEN 787 PROVE_TAC[NO_EMPTY_SET_IN_RUN_def] 788 ] 789 ] 790 ] 791) THEN 792EXISTS_TAC ``w:num -> 'a`` THEN 793REPEAT STRIP_TAC THENL [ 794 ASM_SIMP_TAC arith_ss [] THEN 795 SELECT_ELIM_TAC THEN 796 REPEAT STRIP_TAC THENL [ 797 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 798 PROVE_TAC[IS_PATH_TO_def] 799 ], 800 801 `(SUC n' <= n) \/ (n' = n) \/ (n < n')` by DECIDE_TAC THENL [ 802 ASM_SIMP_TAC arith_ss [] THEN 803 SELECT_ELIM_TAC THEN 804 REPEAT STRIP_TAC THENL [ 805 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 806 FULL_SIMP_TAC arith_ss [IS_PATH_TO_def] 807 ], 808 809 ASM_SIMP_TAC arith_ss [] THEN 810 SELECT_ELIM_TAC THEN 811 REPEAT STRIP_TAC THENL [ 812 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 813 814 `x n = s` by PROVE_TAC[IS_PATH_TO_def] THEN 815 `SUC n - n = SUC 0` by DECIDE_TAC THEN 816 ASM_REWRITE_TAC [CHOOSEN_PATH_def, ADD_CLAUSES, IN_SING] THEN 817 SIMP_TAC arith_ss [] THEN 818 SELECT_ELIM_TAC THEN 819 ASM_REWRITE_TAC [MEMBER_NOT_EMPTY] THEN 820 PROVE_TAC [NO_EMPTY_SET_IN_RUN_def] 821 ], 822 823 824 ASM_SIMP_TAC arith_ss [] THEN 825 `SUC n' - n = SUC (n' - n)` by DECIDE_TAC THEN 826 ASM_SIMP_TAC arith_ss [CHOOSEN_PATH_def] THEN 827 SELECT_ELIM_TAC THEN 828 ASM_REWRITE_TAC [MEMBER_NOT_EMPTY] THEN 829 FULL_SIMP_TAC arith_ss [NO_EMPTY_SET_IN_RUN_def] THEN 830 `?m. n' - n = m` by PROVE_TAC[] THEN 831 `n' = n + m` by DECIDE_TAC THEN 832 ASM_REWRITE_TAC[] THEN 833 `IS_REACHABLE_BY_RUN (w n', n') r` by PROVE_TAC[] THEN 834 `(CHOOSEN_PATH {s} (\S n'''. r.R S (n + PRE n''')) m) = w n'` by 835 (ASM_REWRITE_TAC [] THEN 836 SIMP_TAC std_ss [] THEN 837 `~(n + m <= n) /\ (n + m - n = m)` by DECIDE_TAC THEN 838 ASM_REWRITE_TAC[]) THEN 839 PROVE_TAC[NO_EMPTY_SET_IN_RUN_def] 840 ], 841 842 ASM_SIMP_TAC arith_ss [] THEN 843 SELECT_ELIM_TAC THEN 844 REPEAT STRIP_TAC THENL [ 845 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS], 846 PROVE_TAC[IS_PATH_TO_def] 847 ] 848]); 849 850 851 852val NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_EXISTS = 853 store_thm 854 ("NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_EXISTS", 855 ``!r. (NO_EMPTY_SET_IN_RUN r) ==> ((?w. IS_PATH_THROUGH_RUN w r))``, 856 857 REPEAT STRIP_TAC THEN 858 `?x. x IN r.S0` by PROVE_TAC[NO_EMPTY_SET_IN_RUN_def, MEMBER_NOT_EMPTY] THEN 859 `IS_REACHABLE_BY_RUN (x, 0) r` by PROVE_TAC[IS_REACHABLE_BY_RUN_def] THEN 860 PROVE_TAC[NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_AND_REACHABLE_STATE_EXISTS]); 861 862 863 864val NDET_MIN_RUN_SING = 865 store_thm 866 ("NDET_MIN_RUN_SING", 867 868 ``!A i r. (ALTERNATING_MIN_RUN A i r /\ IS_NONDETERMINISTIC_SEMI_AUTOMATON A) ==> 869 ((SING r.S0) /\ (!n s. IS_REACHABLE_BY_RUN (s,n) r ==> SING (r.R s n)))``, 870 871 SIMP_TAC std_ss [ALTERNATING_MIN_RUN_def, IS_NONDETERMINISTIC_SEMI_AUTOMATON_def, IS_PROP_DISJUNCTION_def] THEN 872 REPEAT STRIP_TAC THENL [ 873 FULL_SIMP_TAC std_ss [P_PROP_DISJUNCTION_MIN_SEM, EXISTS_MEM, SING_DEF] THEN 874 PROVE_TAC[], 875 876 RES_TAC THEN 877 `?S. A.R s (i n) = P_PROP_DISJUNCTION S` by PROVE_TAC[] THEN 878 FULL_SIMP_TAC std_ss [P_PROP_DISJUNCTION_MIN_SEM, EXISTS_MEM, SING_DEF] THEN 879 PROVE_TAC[] 880 ]); 881 882 883val NDET_MIN_RUN_REACHABLE = 884 store_thm 885 ("NDET_MIN_RUN_REACHABLE", 886 887 ``!A i r. (ALTERNATING_MIN_RUN A i r /\ IS_NONDETERMINISTIC_SEMI_AUTOMATON A) ==> 888 (!n. ?!s. IS_REACHABLE_BY_RUN (s,n) r)``, 889 890 SIMP_TAC std_ss [EXISTS_UNIQUE_DEF] THEN 891 REPEAT GEN_TAC THEN STRIP_TAC THEN 892 Induct_on `n` THENL [ 893 `SING r.S0` by PROVE_TAC[NDET_MIN_RUN_SING] THEN 894 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, SING_DEF, IN_SING], 895 896 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def] THEN 897 `SING (r.R s n)` by PROVE_TAC[NDET_MIN_RUN_SING] THEN 898 FULL_SIMP_TAC std_ss [SING_DEF] THEN 899 METIS_TAC[IN_SING] 900 ]); 901 902 903 904 905val ALT_SEM_S0_TRUE = 906 store_thm 907 ("ALT_SEM_S0_TRUE", 908 ``!A i. ((A.A.S0 = P_TRUE) /\ (!n. i n IN A.A.I)) ==> ALT_SEM A i``, 909 910 SIMP_TAC std_ss [ALT_SEM_def, ALTERNATING_RUN_def, P_SEM_THM] THEN 911 REPEAT STRIP_TAC THEN 912 EXISTS_TAC ``alternating_run (EMPTY:'b set) (\s n. EMPTY)`` THEN 913 SIMP_TAC std_ss [alternating_run_S0, alternating_run_R, EMPTY_SUBSET, 914 IS_PATH_THROUGH_RUN_def, NOT_IN_EMPTY] THEN 915 Cases_on `n` THEN 916 SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, 917 alternating_run_R, NOT_IN_EMPTY]); 918 919 920val ALT_SEM_S0_FALSE = 921 store_thm 922 ("ALT_SEM_S0_FALSE", 923 ``!A i. ((A.A.S0 = P_FALSE)) ==> ~ALT_SEM A i``, 924 SIMP_TAC std_ss [ALT_SEM_def, ALTERNATING_RUN_def, P_SEM_THM]); 925 926 927val ALT_SEM_S0_OR_SPLIT = 928 store_thm 929 ("ALT_SEM_S0_OR_SPLIT", 930 ``!A i p1 p2. ((A.A.S0 = P_OR(p1, p2))) ==> 931 (ALT_SEM A i = (ALT_SEM (alternating_automaton (alternating_semi_automaton A.A.S A.A.I 932 p1 A.A.R) A.AC) i \/ ALT_SEM (alternating_automaton (alternating_semi_automaton A.A.S A.A.I p2 A.A.R) A.AC) i))``, 933 934 SIMP_TAC std_ss [ALT_SEM_def, ALTERNATING_RUN_def, P_SEM_THM, 935 alternating_automaton_REWRITES] THEN 936 METIS_TAC[]); 937 938 939 940val ALT_SEM_INITIAL_S0_P_PROP = 941 store_thm 942 ("ALT_SEM_INITIAL_S0_P_PROP", 943 ``!A s0 f i. (A.S0 = P_PROP s0) ==> 944 (ALT_SEM (alternating_automaton A (INITIAL f)) i = 945 ALT_SEM (alternating_automaton A (if (s0 IN f) then TRUE else FALSE)) i)``, 946 947 948 SIMP_TAC std_ss [ALT_SEM___ALT_SEM_MIN___EQUIV, 949 ALT_SEM_MIN_def, alternating_automaton_REWRITES, 950 ALT_ACCEPT_COND_SEM_def] THEN 951 REPEAT STRIP_TAC THEN 952 BOOL_EQ_STRIP_TAC THEN 953 EXISTS_EQ_STRIP_TAC THEN 954 BOOL_EQ_STRIP_TAC THEN 955 FORALL_EQ_STRIP_TAC THEN 956 REWRITE_TAC[IMP_DISJ_THM] THEN 957 BOOL_EQ_STRIP_TAC THEN 958 `P_SEM_MIN r.S0 (P_PROP s0)` by 959 PROVE_TAC[ALTERNATING_MIN_RUN_def, alternating_semi_automaton_S0] THEN 960 FULL_SIMP_TAC std_ss [P_PROP_MIN_SEM] THEN 961 `w 0 = s0` by PROVE_TAC[IS_PATH_THROUGH_RUN_def, IN_SING] THEN 962 Cases_on `s0 IN f` THEN 963 ASM_REWRITE_TAC [ALT_ACCEPT_COND_SEM_def]); 964 965 966 967 968 969val ALT_SEM_S0_AND_SPLIT___INITIAL = 970 store_thm 971 ("ALT_SEM_S0_AND_SPLIT___INITIAL", 972 ``!A f i p1 p2. (IS_VALID_ALTERNATING_AUTOMATON A /\ (A.A.S0 = P_AND(p1, p2)) /\ (A.AC = INITIAL f)) ==> 973 (ALT_SEM A i = (ALT_SEM (alternating_automaton (alternating_semi_automaton A.A.S A.A.I 974 p1 A.A.R) A.AC) i /\ ALT_SEM (alternating_automaton (alternating_semi_automaton A.A.S A.A.I p2 A.A.R) A.AC) i))``, 975 976 SIMP_TAC std_ss [ALT_SEM_def, ALTERNATING_RUN_def, P_SEM_THM, 977 alternating_automaton_REWRITES] THEN 978 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 979 ASM_REWRITE_TAC[], 980 METIS_TAC[], 981 ASM_REWRITE_TAC[], 982 METIS_TAC[], 983 ASM_REWRITE_TAC[], 984 985 Q.ABBREV_TAC `P = (\s n. (?w. (IS_PATH_TO w r s n) /\ ~(w 0 IN f)))` THEN 986 Q.ABBREV_TAC `P' = (\s n. (?w. (IS_PATH_TO w r' s n) /\ ~(w 0 IN f)))` THEN 987 `!s:'b n:num. P s n ==> IS_REACHABLE_BY_RUN (s, n) r` by 988 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS] THEN 989 `!s:'b n:num. P' s n ==> IS_REACHABLE_BY_RUN (s, n) r'` by 990 PROVE_TAC[PATH_TO_REACHABLE_STATES_EXISTS] THEN 991 `?ru. ru = (alternating_run (r.S0 UNION r'.S0) (\s n. if (P s n) then r.R s n else 992 (if (P' s n) then r'.R s n else 993 (if ~(IS_REACHABLE_BY_RUN (s, n) r) then r'.R s n else ( 994 (if ~(IS_REACHABLE_BY_RUN (s, n) r') then r.R s n else ( 995 r.R s n UNION r'.R s n)))))))` by METIS_TAC[] THEN 996 997 SUBGOAL_TAC `!s n. IS_REACHABLE_BY_RUN (s, n) (ru:'b alternating_run) ==> 998 (IS_REACHABLE_BY_RUN (s, n) r \/ IS_REACHABLE_BY_RUN (s, n) r')` THEN1 ( 999 Induct_on `n` THENL [ 1000 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, IN_UNION], 1001 1002 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_R] THEN 1003 METIS_TAC[IN_UNION] 1004 ]) THEN 1005 1006 EXISTS_TAC ``ru:'b alternating_run`` THEN 1007 FULL_SIMP_TAC std_ss [alternating_run_S0, alternating_run_R, 1008 IS_VALID_ALTERNATING_AUTOMATON_def, IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1009 IS_POSITIVE_PROP_FORMULA_def, IS_POSITIVE_PROP_FORMULA_SUBSET_def, 1010 UNION_SUBSET] 1011 THEN 1012 REPEAT STRIP_TAC THENL [ 1013 METIS_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM, SUBSET_UNIV], 1014 METIS_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM, SUBSET_UNIV, UNION_COMM], 1015 METIS_TAC[UNION_SUBSET], 1016 METIS_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SUBSET_SEM, SUBSET_UNIV], 1017 1018 CCONTR_TAC THEN 1019 FULL_SIMP_TAC std_ss [ALT_ACCEPT_COND_SEM_def] THEN 1020 1021 Cases_on `?n. P (w n) n` THENL [ 1022 CLEAN_ASSUMPTIONS_TAC THEN 1023 UNDISCH_HD_TAC THEN 1024 GSYM_NO_TAC 7 THEN 1025 ASM_SIMP_TAC std_ss [] THEN 1026 GSYM_NO_TAC 0 THEN 1027 CCONTR_TAC THEN 1028 FULL_SIMP_TAC std_ss [] THEN 1029 `?v. v = \m. if (m <= n) then w' m else w m` by METIS_TAC[] THEN 1030 1031 Tactical.REVERSE (SUBGOAL_THEN ``(!n:num. P ((v n):'b) n) /\ IS_PATH_THROUGH_RUN v r`` ASSUME_TAC) THEN1 ( 1032 `v 0 = w' 0` by ASM_SIMP_TAC arith_ss [] THEN 1033 PROVE_TAC[] 1034 ) THEN 1035 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, GSYM FORALL_AND_THM, 1036 alternating_run_S0, alternating_run_R, IS_PATH_TO_def] THEN 1037 Tactical.REVERSE (SUBGOAL_THEN ``(!m:num n:num. (n <= m) ==> (P (v n) n /\ v (SUC n) IN (r:'b alternating_run).R (v n) n))`` ASSUME_TAC) THEN1 ( 1038 UNDISCH_HD_TAC THEN 1039 ASM_SIMP_TAC arith_ss [] THEN 1040 METIS_TAC[LESS_EQ_REFL] 1041 ) THEN 1042 1043 Induct_on `m` THENL [ 1044 SIMP_TAC arith_ss [] THEN 1045 LEFT_CONJ_TAC THENL [ 1046 GSYM_NO_TAC 5 THEN 1047 ASM_SIMP_TAC arith_ss [] THEN 1048 METIS_TAC[], 1049 1050 ASM_SIMP_TAC arith_ss [] THEN 1051 `1 = SUC 0` by DECIDE_TAC THEN 1052 Cases_on `1 <= n` THENL [ 1053 ASM_REWRITE_TAC[] THEN 1054 `0 < n` by DECIDE_TAC THEN 1055 PROVE_TAC[], 1056 1057 ASM_REWRITE_TAC[] THEN 1058 `n = 0` by DECIDE_TAC THEN 1059 METIS_TAC[] 1060 ] 1061 ], 1062 1063 REPEAT GEN_TAC THEN 1064 STRIP_TAC THEN 1065 LEFT_CONJ_TAC THENL [ 1066 GSYM_NO_TAC 7 THEN 1067 ASM_SIMP_TAC arith_ss [] THEN 1068 EXISTS_TAC ``v:num->'b `` THEN 1069 ASM_SIMP_TAC arith_ss [], 1070 1071 ASM_SIMP_TAC arith_ss [] THEN 1072 Cases_on `SUC n' <= n` THENL [ 1073 `n' <= n /\ n' < n` by DECIDE_TAC THEN 1074 ASM_REWRITE_TAC[] THEN 1075 METIS_TAC[], 1076 1077 ASM_REWRITE_TAC[] THEN 1078 Cases_on `n' <= n` THENL [ 1079 `n' = n` by DECIDE_TAC THEN 1080 METIS_TAC[], 1081 1082 METIS_TAC[] 1083 ] 1084 ] 1085 ] 1086 ], 1087 1088 1089 1090 1091 1092 FULL_SIMP_TAC std_ss [] THEN 1093 `w 0 IN r'.S0` by ( 1094 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, IN_UNION] THEN 1095 UNDISCH_HD_TAC THEN 1096 GSYM_NO_TAC 8 THEN 1097 `P (w 0) 0` by (ASM_SIMP_TAC arith_ss [IS_PATH_TO_def] THEN PROVE_TAC[]) THEN 1098 PROVE_TAC[] 1099 ) THEN 1100 1101 Tactical.REVERSE (SUBGOAL_THEN ``(!n:num. P' ((w n):'b) n) /\ IS_PATH_THROUGH_RUN w r'`` ASSUME_TAC) THEN1 ( 1102 PROVE_TAC[] 1103 ) THEN 1104 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, GSYM FORALL_AND_THM, 1105 alternating_run_S0, alternating_run_R, IS_PATH_TO_def] THEN 1106 Tactical.REVERSE (SUBGOAL_THEN ``(!m:num n:num. (n <= m) ==> (P' (w n) n /\ w (SUC n) IN (r':'b alternating_run).R (w n) n))`` ASSUME_TAC) THEN1 ( 1107 PROVE_TAC[LESS_EQ_REFL] 1108 ) THEN 1109 1110 Induct_on `m` THENL [ 1111 SIMP_TAC arith_ss [] THEN 1112 LEFT_CONJ_TAC THENL [ 1113 GSYM_NO_TAC 9 THEN 1114 ASM_SIMP_TAC arith_ss [] THEN 1115 METIS_TAC[], 1116 1117 `1 = SUC 0` by DECIDE_TAC THEN 1118 PROVE_TAC[] 1119 ], 1120 1121 REPEAT GEN_TAC THEN 1122 STRIP_TAC THEN 1123 LEFT_CONJ_TAC THENL [ 1124 GSYM_NO_TAC 11 THEN 1125 ASM_SIMP_TAC arith_ss [] THEN 1126 EXISTS_TAC ``w:num->'b `` THEN 1127 ASM_SIMP_TAC arith_ss [], 1128 1129 PROVE_TAC[] 1130 ] 1131 ] 1132 ] 1133 ] 1134 ]); 1135 1136 1137 1138 1139 1140 1141 1142val ALTERNATING_AUTOMATA_CONJUNCTION = 1143 store_thm 1144 ("ALTERNATING_AUTOMATA_CONJUNCTION", 1145 ``!A A1 A2 i. (IS_VALID_ALTERNATING_SEMI_AUTOMATON A1.A /\ 1146 IS_VALID_ALTERNATING_SEMI_AUTOMATON A2.A /\ 1147 (DISJOINT A1.A.S A2.A.S) /\ (A.A = (alternating_semi_automaton (A1.A.S UNION A2.A.S) 1148 (A1.A.I INTER A2.A.I) (P_AND (A1.A.S0, A2.A.S0)) (\s n. if (s IN A1.A.S) then A1.A.R s n else 1149 A2.A.R s n))) /\ (!w. (!n:num. (w n) IN A1.A.S) ==> (ALT_ACCEPT_COND_SEM A.AC = ALT_ACCEPT_COND_SEM A1.AC)) 1150 /\ (!w. (!n:num. (w n) IN A2.A.S) ==> (ALT_ACCEPT_COND_SEM A.AC = ALT_ACCEPT_COND_SEM A2.AC))) ==> 1151 (IS_VALID_ALTERNATING_SEMI_AUTOMATON A.A /\ ((ALT_SEM A1 i /\ ALT_SEM A2 i) = ALT_SEM A i))``, 1152 1153 REPEAT GEN_TAC THEN 1154 STRIP_TAC THEN 1155 SUBGOAL_TAC `IS_VALID_ALTERNATING_SEMI_AUTOMATON A.A` THEN1 ( 1156 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1157 alternating_automaton_REWRITES, IS_POSITIVE_PROP_FORMULA_SUBSET_def, 1158 FINITE_UNION, P_USED_VARS_def, UNION_SUBSET, 1159 IS_POSITIVE_PROP_FORMULA_def, INTER_FINITE] THEN 1160 METIS_TAC[SUBSET_TRANS, SUBSET_UNION] 1161 ) THEN 1162 ASM_SIMP_TAC std_ss [ALT_SEM_def, ALTERNATING_RUN_def, P_SEM_THM, 1163 alternating_automaton_REWRITES, IN_INTER, FORALL_AND_THM] THEN 1164 REPEAT CONJ_EQ_STRIP_TAC THEN 1165 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1166 `?ru. ru = alternating_run ((r:'b alternating_run).S0 UNION r'.S0) (\s n. 1167 (if s IN A1.A.S then r.R s n else r'.R s n))` by PROVE_TAC[] THEN 1168 SUBGOAL_TAC `!w. (IS_PATH_THROUGH_RUN w (ru:'b alternating_run)) = 1169 (IS_PATH_THROUGH_RUN w r \/ IS_PATH_THROUGH_RUN w r')` THEN1 ( 1170 1171 ASM_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, alternating_run_R, 1172 IN_UNION] THEN 1173 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 1174 REPEAT STRIP_TAC THENL [ 1175 `~(w 0 IN r'.S0)` by METIS_TAC[IN_DISJOINT, SUBSET_DEF] THEN 1176 ASM_REWRITE_TAC[] THEN 1177 Induct_on `n` THEN 1178 METIS_TAC[IN_DISJOINT, SUBSET_DEF], 1179 1180 `~(w 0 IN r.S0)` by METIS_TAC[IN_DISJOINT, SUBSET_DEF] THEN 1181 ASM_REWRITE_TAC[] THEN 1182 Induct_on `n` THEN 1183 METIS_TAC[IN_DISJOINT, SUBSET_DEF] 1184 ], 1185 1186 REPEAT STRIP_TAC THENL [ 1187 ASM_REWRITE_TAC[], 1188 Cases_on `n` THEN METIS_TAC[SUBSET_DEF], 1189 ASM_REWRITE_TAC[], 1190 Cases_on `n` THEN METIS_TAC[SUBSET_DEF, IN_DISJOINT] 1191 ] 1192 ] 1193 ) THEN 1194 1195 SUBGOAL_TAC `!s n. (IS_REACHABLE_BY_RUN (s, n) (ru:'b alternating_run)) = 1196 (IS_REACHABLE_BY_RUN (s,n) r \/ IS_REACHABLE_BY_RUN (s,n) r')` THEN1 ( 1197 1198 Induct_on `n` THENL [ 1199 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, 1200 alternating_run_R, IN_UNION], 1201 1202 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, 1203 alternating_run_R, IN_UNION] THEN 1204 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1205 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, 1206 ALTERNATING_PRERUN_def], 1207 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, IN_DISJOINT, 1208 ALTERNATING_PRERUN_def], 1209 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, 1210 ALTERNATING_PRERUN_def], 1211 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, 1212 ALTERNATING_PRERUN_def, IN_DISJOINT] 1213 ] 1214 ] 1215 ) THEN 1216 1217 EXISTS_TAC ``ru : 'b alternating_run`` THEN 1218 FULL_SIMP_TAC std_ss [alternating_run_S0, alternating_run_R, IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, UNION_SUBSET] THEN 1219 REPEAT STRIP_TAC THENL [ 1220 METIS_TAC[SUBSET_TRANS, SUBSET_UNION], 1221 METIS_TAC[SUBSET_TRANS, SUBSET_UNION], 1222 METIS_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM, SUBSET_UNION], 1223 METIS_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM, SUBSET_UNION], 1224 METIS_TAC[SUBSET_TRANS, SUBSET_UNION], 1225 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, 1226 ALTERNATING_PRERUN_def], 1227 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, IN_DISJOINT, 1228 ALTERNATING_PRERUN_def], 1229 1230 SUBGOAL_TAC `!n. w n IN A1.A.S` THEN1 ( 1231 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def] THEN 1232 Cases_on `n` THEN 1233 PROVE_TAC[SUBSET_DEF] 1234 ) THEN 1235 METIS_TAC[], 1236 1237 SUBGOAL_TAC `!n. w n IN A2.A.S` THEN1 ( 1238 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def] THEN 1239 Cases_on `n` THEN 1240 PROVE_TAC[SUBSET_DEF] 1241 ) THEN 1242 METIS_TAC[] 1243 ], 1244 1245 1246 1247 `?r1. r1 = alternating_run ((r:'b alternating_run).S0 INTER A1.A.S) (\s n. (r.R s n) INTER A1.A.S)` by PROVE_TAC[] THEN 1248 `IS_ALTERNATING_SUBRUN r1 r` by FULL_SIMP_TAC std_ss [IS_ALTERNATING_SUBRUN_def, 1249 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1250 1251 EXISTS_TAC ``r1:'b alternating_run`` THEN 1252 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1253 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1254 REPEAT STRIP_TAC THENL [ 1255 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1256 1257 SUBGOAL_TAC `s IN A1.A.S` THEN1 ( 1258 Cases_on `n` THEN 1259 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, alternating_run_R, IN_INTER] 1260 ) THEN 1261 METIS_TAC[SUBRUN_REACHABLE_STATES, P_USED_VARS_INTER_SUBSET_THM], 1262 1263 SUBGOAL_TAC `!n. w n IN A1.A.S` THEN1 ( 1264 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, 1265 alternating_run_R, IN_INTER] THEN 1266 Cases_on `n` THEN 1267 ASM_REWRITE_TAC[] 1268 ) THEN 1269 PROVE_TAC[IS_PATH_THROUGH_SUBRUN_THM] 1270 ], 1271 1272 1273 1274 `?r2. r2 = alternating_run ((r:'b alternating_run).S0 INTER A2.A.S) (\s n. (r.R s n) INTER A2.A.S)` by PROVE_TAC[] THEN 1275 `IS_ALTERNATING_SUBRUN r2 r` by FULL_SIMP_TAC std_ss [IS_ALTERNATING_SUBRUN_def, 1276 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1277 1278 EXISTS_TAC ``r2:'b alternating_run`` THEN 1279 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1280 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1281 REPEAT STRIP_TAC THENL [ 1282 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1283 1284 SUBGOAL_TAC `s IN A2.A.S` THEN1 ( 1285 Cases_on `n` THEN 1286 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, alternating_run_R, IN_INTER] 1287 ) THEN 1288 `~(s IN A1.A.S)` by PROVE_TAC[IN_DISJOINT] THEN 1289 METIS_TAC[SUBRUN_REACHABLE_STATES, P_USED_VARS_INTER_SUBSET_THM], 1290 1291 SUBGOAL_TAC `!n. w n IN A2.A.S` THEN1 ( 1292 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, 1293 alternating_run_R, IN_INTER] THEN 1294 Cases_on `n` THEN 1295 ASM_REWRITE_TAC[] 1296 ) THEN 1297 PROVE_TAC[IS_PATH_THROUGH_SUBRUN_THM] 1298 ] 1299 ]); 1300 1301 1302 1303val ALTERNATING_AUTOMATA_DISJUNCTION = 1304 store_thm 1305 ("ALTERNATING_AUTOMATA_DISJUNCTION", 1306 ``!A A1 A2 i. (IS_VALID_ALTERNATING_SEMI_AUTOMATON A1.A /\ 1307 IS_VALID_ALTERNATING_SEMI_AUTOMATON A2.A /\ 1308 (A2.A.I = A1.A.I) /\ 1309 (DISJOINT A1.A.S A2.A.S) /\ (A.A = (alternating_semi_automaton (A1.A.S UNION A2.A.S) 1310 (A1.A.I) (P_OR (A1.A.S0, A2.A.S0)) (\s n. if (s IN A1.A.S) then A1.A.R s n else 1311 A2.A.R s n))) /\ (!w. (!n:num. (w n) IN A1.A.S) ==> (ALT_ACCEPT_COND_SEM A.AC = ALT_ACCEPT_COND_SEM A1.AC)) 1312 /\ (!w. (!n:num. (w n) IN A2.A.S) ==> (ALT_ACCEPT_COND_SEM A.AC = ALT_ACCEPT_COND_SEM A2.AC))) ==> 1313 (IS_VALID_ALTERNATING_SEMI_AUTOMATON A.A /\ ((ALT_SEM A1 i \/ ALT_SEM A2 i) = ALT_SEM A i))``, 1314 1315 REPEAT GEN_TAC THEN 1316 STRIP_TAC THEN 1317 SUBGOAL_TAC `IS_VALID_ALTERNATING_SEMI_AUTOMATON A.A` THEN1 ( 1318 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1319 alternating_automaton_REWRITES, IS_POSITIVE_PROP_FORMULA_SUBSET_def, 1320 FINITE_UNION, P_USED_VARS_def, P_OR_def, UNION_SUBSET, 1321 IS_POSITIVE_PROP_FORMULA_def, INTER_FINITE] THEN 1322 METIS_TAC[SUBSET_TRANS, SUBSET_UNION] 1323 ) THEN 1324 ASM_SIMP_TAC std_ss [ALT_SEM_def, ALTERNATING_RUN_def, P_SEM_THM, 1325 alternating_automaton_REWRITES, IN_INTER, FORALL_AND_THM] THEN 1326 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1327 ASM_REWRITE_TAC[], 1328 1329 EXISTS_TAC ``r:'b alternating_run`` THEN 1330 ASM_REWRITE_TAC[] THEN 1331 REPEAT STRIP_TAC THENL [ 1332 PROVE_TAC[SUBSET_TRANS, SUBSET_UNION], 1333 PROVE_TAC[SUBSET_TRANS, SUBSET_UNION], 1334 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, ALTERNATING_PRERUN_def], 1335 1336 SUBGOAL_TAC `!n. w n IN A1.A.S` THEN1 ( 1337 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def] THEN 1338 Cases_on `n` THEN 1339 PROVE_TAC[SUBSET_DEF] 1340 ) THEN 1341 METIS_TAC[] 1342 ], 1343 1344 ASM_REWRITE_TAC[], 1345 1346 EXISTS_TAC ``r:'b alternating_run`` THEN 1347 ASM_REWRITE_TAC[] THEN 1348 REPEAT STRIP_TAC THENL [ 1349 PROVE_TAC[SUBSET_TRANS, SUBSET_UNION], 1350 PROVE_TAC[SUBSET_TRANS, SUBSET_UNION], 1351 METIS_TAC[REACHABLE_STATES_IN_STATES_SET, ALTERNATING_PRERUN_def, 1352 IN_DISJOINT], 1353 1354 SUBGOAL_TAC `!n. w n IN A2.A.S` THEN1 ( 1355 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def] THEN 1356 Cases_on `n` THEN 1357 PROVE_TAC[SUBSET_DEF] 1358 ) THEN 1359 METIS_TAC[] 1360 ], 1361 1362 1363 DISJ1_TAC THEN 1364 ASM_REWRITE_TAC[] THEN 1365 `?r1. r1 = alternating_run ((r:'b alternating_run).S0 INTER A1.A.S) (\s n. (r.R s n) INTER A1.A.S)` by PROVE_TAC[] THEN 1366 `IS_ALTERNATING_SUBRUN r1 r` by FULL_SIMP_TAC std_ss [IS_ALTERNATING_SUBRUN_def, 1367 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1368 1369 EXISTS_TAC ``r1:'b alternating_run`` THEN 1370 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1371 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1372 REPEAT STRIP_TAC THENL [ 1373 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1374 1375 `s IN A1.A.S` by (Cases_on `n` THEN 1376 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, alternating_run_R, IN_INTER]) THEN 1377 METIS_TAC[SUBRUN_REACHABLE_STATES, P_USED_VARS_INTER_SUBSET_THM], 1378 1379 `!n. w n IN A1.A.S` by ( 1380 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, 1381 alternating_run_R, IN_INTER] THEN 1382 Cases_on `n` THEN 1383 ASM_REWRITE_TAC[] 1384 ) THEN 1385 PROVE_TAC[IS_PATH_THROUGH_SUBRUN_THM] 1386 ], 1387 1388 DISJ2_TAC THEN 1389 ASM_REWRITE_TAC[] THEN 1390 `?r2. r2 = alternating_run ((r:'b alternating_run).S0 INTER A2.A.S) (\s n. (r.R s n) INTER A2.A.S)` by PROVE_TAC[] THEN 1391 `IS_ALTERNATING_SUBRUN r2 r` by FULL_SIMP_TAC std_ss [IS_ALTERNATING_SUBRUN_def, 1392 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1393 1394 EXISTS_TAC ``r2:'b alternating_run`` THEN 1395 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, 1396 alternating_run_S0, alternating_run_R, INTER_SUBSET] THEN 1397 REPEAT STRIP_TAC THENL [ 1398 PROVE_TAC[P_USED_VARS_INTER_SUBSET_THM], 1399 1400 SUBGOAL_TAC `s IN A2.A.S` THEN1 ( 1401 Cases_on `n` THEN 1402 FULL_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, alternating_run_R, IN_INTER] 1403 ) THEN 1404 `~(s IN A1.A.S)` by PROVE_TAC[IN_DISJOINT] THEN 1405 METIS_TAC[SUBRUN_REACHABLE_STATES, P_USED_VARS_INTER_SUBSET_THM], 1406 1407 SUBGOAL_TAC `!n. w n IN A2.A.S` THEN1 ( 1408 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, 1409 alternating_run_R, IN_INTER] THEN 1410 Cases_on `n` THEN 1411 ASM_REWRITE_TAC[] 1412 ) THEN 1413 PROVE_TAC[IS_PATH_THROUGH_SUBRUN_THM] 1414 ] 1415 ]); 1416 1417 1418 1419val ALT_AUTOMATON_NEG_COMMON_PATH_THROUGH_RUNS_EXISTS = 1420 prove ( 1421 ``!A i r r'. (IS_VALID_ALTERNATING_SEMI_AUTOMATON A /\ 1422 ALTERNATING_RUN A i r /\ ALTERNATING_RUN (ALT_SEMI_AUTOMATON_NEG A) i r') ==> (?w. IS_PATH_THROUGH_RUN w r /\ IS_PATH_THROUGH_RUN w r')``, 1423 1424 1425 1426 SIMP_TAC std_ss [ALT_AUTOMATON_NEG_def, 1427 ALT_SEMI_AUTOMATON_NEG_def, ALTERNATING_RUN_def, 1428 alternating_automaton_REWRITES, P_SEM_MIN_def, P_SEM_THM, P_NEGATE_VARS_SEM, P_DUAL_def, 1429 IS_VALID_ALTERNATING_SEMI_AUTOMATON_def] THEN 1430 REPEAT STRIP_TAC THEN 1431 ASM_SIMP_TAC std_ss [] THEN 1432 `?r''. r'' = alternating_run (r.S0 INTER r'.S0) (\s n. (r.R s n INTER r'.R s n))` by METIS_TAC[] THEN 1433 1434 REMAINS_TAC `?w. IS_PATH_THROUGH_RUN w (r'':'b alternating_run)` THEN1 ( 1435 EXISTS_TAC ``w:num->'b`` THEN 1436 UNDISCH_HD_TAC THEN 1437 FULL_SIMP_TAC std_ss [IS_PATH_THROUGH_RUN_def, alternating_run_S0, 1438 alternating_run_R, IN_INTER] 1439 ) THEN 1440 1441 REMAINS_TAC `NO_EMPTY_SET_IN_RUN (r'':'b alternating_run)` THEN1 ( 1442 PROVE_TAC[NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_EXISTS] 1443 ) THEN 1444 1445 REWRITE_TAC[NO_EMPTY_SET_IN_RUN_def] THEN 1446 Tactical.REVERSE STRIP_TAC THENL [ 1447 ASM_SIMP_TAC std_ss [alternating_run_S0] THEN 1448 REPEAT STRIP_TAC THEN 1449 `r.S0 SUBSET (UNIV DIFF r'.S0)` by PROVE_TAC[SUBSET_COMPL_DISJOINT, DISJOINT_DEF, COMPL_DEF] THEN 1450 PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM], 1451 1452 1453 SUBGOAL_TAC `!n (s:'b). (IS_REACHABLE_BY_RUN (s, n) r'') ==> (IS_REACHABLE_BY_RUN (s, n) r /\ 1454 IS_REACHABLE_BY_RUN (s, n) r')` THEN1 ( 1455 Induct_on `n` THENL [ 1456 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_S0, IN_INTER], 1457 1458 ASM_SIMP_TAC std_ss [IS_REACHABLE_BY_RUN_def, alternating_run_R, IN_INTER] THEN 1459 PROVE_TAC[] 1460 ] 1461 ) THEN 1462 REPEAT GEN_TAC THEN STRIP_TAC THEN 1463 RES_TAC THEN 1464 ASM_SIMP_TAC std_ss [alternating_run_R] THEN 1465 REPEAT STRIP_TAC THEN 1466 `r.R s n SUBSET (UNIV DIFF r'.R s n)` by PROVE_TAC[SUBSET_COMPL_DISJOINT, DISJOINT_DEF, COMPL_DEF] THEN 1467 PROVE_TAC[IS_POSITIVE_NEGATIVE_PROP_FORMULA_SEM] 1468 ]); 1469 1470 1471 1472val A_TRUE___A_UNIVERSALLY_TOTAL_WEAK_CO_BUECHI = 1473 store_thm 1474 ("A_TRUE___A_UNIVERSALLY_TOTAL_WEAK_CO_BUECHI", 1475 1476 ``!A:('input, 'states) alternating_automaton S. (IS_VALID_ALTERNATING_AUTOMATON A /\ IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A.A /\ (A.AC = WEAK_CO_BUECHI S)) ==> 1477 (?B:('input, 'states) alternating_automaton. (B=(alternating_automaton (alternating_semi_automaton A.A.S A.A.I A.A.S0 (\s i. if (s IN S) then P_FALSE else A.A.R s i)) TRUE)) /\ (IS_VALID_ALTERNATING_AUTOMATON B) /\ (ALT_AUTOMATON_EQUIV A B))``, 1478 1479 SIMP_TAC std_ss [] THEN 1480 REPEAT STRIP_TAC THENL [ 1481 FULL_SIMP_TAC std_ss [IS_VALID_ALTERNATING_AUTOMATON_def, 1482 IS_VALID_ALTERNATING_SEMI_AUTOMATON_def, IS_VALID_ACCEPTANCE_COMPONENT_def, 1483 alternating_automaton_REWRITES] THEN 1484 REPEAT STRIP_TAC THENL [ 1485 Cases_on `s IN S` THEN 1486 ASM_SIMP_TAC std_ss [P_USED_VARS_def, P_FALSE_def, EMPTY_SUBSET], 1487 1488 Cases_on `s IN S` THEN 1489 FULL_SIMP_TAC std_ss [IS_POSITIVE_PROP_FORMULA_def, 1490 IS_POSITIVE_PROP_FORMULA_SUBSET_def, P_FALSE_def] 1491 ], 1492 1493 FULL_SIMP_TAC std_ss [ALT_AUTOMATON_EQUIV_def, ALT_SEM_def, 1494 IS_NONDETERMINISTIC_AUTOMATON_def, 1495 ALT_ACCEPT_COND_SEM_THM, ALT_ACCEPT_COND_SEM_def, 1496 alternating_automaton_REWRITES, 1497 IS_VALID_ALTERNATING_AUTOMATON_def] THEN 1498 REPEAT STRIP_TAC THEN 1499 CONJ_EQ_STRIP_TAC THEN 1500 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1501 EXISTS_TAC ``r:'states alternating_run`` THEN 1502 `NO_EMPTY_SET_IN_RUN r` by PROVE_TAC[UNIVERSALLY_TOTAL_NO_EMPTY_SET_IN_RUN] THEN 1503 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def, 1504 alternating_automaton_REWRITES] THEN 1505 REPEAT STRIP_TAC THEN 1506 `?w. IS_PATH_THROUGH_RUN w r /\ (w n = s)` by PROVE_TAC[NO_EMPTY_SET_IN_RUN___PATH_THROUGH_RUN_AND_REACHABLE_STATE_EXISTS] THEN 1507 `~(s IN S)` by PROVE_TAC[] THEN 1508 PROVE_TAC[], 1509 1510 EXISTS_TAC ``r:'states alternating_run`` THEN 1511 FULL_SIMP_TAC std_ss [ALTERNATING_RUN_def, 1512 alternating_automaton_REWRITES] THEN 1513 REPEAT STRIP_TAC THENL [ 1514 RES_TAC THEN 1515 Cases_on `s IN S` THEN 1516 FULL_SIMP_TAC std_ss [P_SEM_THM], 1517 1518 `IS_REACHABLE_BY_RUN (w n, n) r` by PROVE_TAC[ 1519 IS_PATH_THROUGH_RUN___IS_REACHABLE_BY_RUN] THEN 1520 RES_TAC THEN 1521 PROVE_TAC[P_SEM_THM] 1522 ] 1523 ] 1524 ]); 1525 1526 1527 1528 1529val NDET_TRUE___NDET_WEAK_CO_BUECHI = 1530 store_thm 1531 ("NDET_TRUE___NDET_WEAK_CO_BUECHI", 1532 1533 ``!A:('input, 'states) alternating_automaton. (IS_VALID_ALTERNATING_AUTOMATON A /\ IS_NONDETERMINISTIC_AUTOMATON A /\ (?S. A.AC = WEAK_CO_BUECHI S)) ==> 1534 (?B:('input, 'states) alternating_automaton. (IS_VALID_ALTERNATING_AUTOMATON B /\ IS_NONDETERMINISTIC_AUTOMATON B) /\ (B.AC = TRUE) /\ (ALT_AUTOMATON_EQUIV A B))``, 1535 1536 REPEAT STRIP_TAC THEN 1537 `IS_UNIVERSALLY_TOTAL_ALTERNATING_SEMI_AUTOMATON A.A` by PROVE_TAC[ 1538 NONDETERMINISTIC_IS_UNIVERSALLY_TOTAL, IS_NONDETERMINISTIC_AUTOMATON_def] THEN 1539 `?B. (B = alternating_automaton (alternating_semi_automaton A.A.S A.A.I A.A.S0 1540 (\s i. (if s IN S then P_FALSE else A.A.R s i))) 1541 TRUE) /\ IS_VALID_ALTERNATING_AUTOMATON B /\ 1542 ALT_AUTOMATON_EQUIV A B` by METIS_TAC[A_TRUE___A_UNIVERSALLY_TOTAL_WEAK_CO_BUECHI] THEN 1543 EXISTS_TAC ``B:('input, 'states) alternating_automaton`` THEN 1544 ASM_REWRITE_TAC [alternating_automaton_AC] THEN 1545 FULL_SIMP_TAC std_ss [IS_NONDETERMINISTIC_AUTOMATON_def, 1546 alternating_automaton_A, IS_NONDETERMINISTIC_SEMI_AUTOMATON_def, 1547 alternating_semi_automaton_S0, alternating_semi_automaton_R] THEN 1548 REPEAT STRIP_TAC THEN 1549 Cases_on `s IN S` THEN ASM_REWRITE_TAC[] THEN 1550 REWRITE_TAC[IS_PROP_DISJUNCTION_def] THEN 1551 PROVE_TAC[P_PROP_DISJUNCTION_def]); 1552 1553 1554 1555 1556val _ = export_theory(); 1557