1open HolKernel Parse boolLib bossLib pred_setTheory arithmeticTheory relationTheory set_relationTheory pairTheory 2 3open generalHelpersTheory wordTheory 4 5val _ = new_theory "alterA" 6val _ = ParseExtras.temp_loose_equality() 7 8val _ = Datatype 9 `ALTER_A = <| states : 's set; 10 alphabet : 'a set; 11 trans : 's -> (('a set # 's set) set); 12 initial : ('s set) set; 13 final : 's set 14 |>`; 15 16val isValidAlterA_def = 17 Define `isValidAlterA (A: ('s,'a) ALTER_A) = 18 (A.initial ��� POW A.states) 19 /\ (A.final ��� A.states) 20 /\ (!s a d. (s ��� A.states) /\ ((a, d) ��� (A.trans s)) 21 ==> (d ��� A.states ��� a ��� A.alphabet))`; 22 23(* An alternating automata is very weak if there is a partial order po on 24 the states s.t. for every state s all states appearing in trans(s) 25 are lower or equal to s 26*) 27 28val isVeryWeakWithOrder_def = Define 29 `isVeryWeakWithOrder A ord = 30 partial_order ord A.states 31 /\ !s a d. (s ��� A.states) /\ ((a,d) ��� (A.trans s)) 32 ==> (!s'. (s' ��� d) ==> ((s',s) ��� ord))`; 33 34val isVeryWeakAlterA_def = 35 Define `isVeryWeakAlterA A = ?ord. isVeryWeakWithOrder A ord`; 36 37val FINITE_LEMM = store_thm 38 ("FINITE_LEMM", 39 ``!aut. FINITE aut.alphabet ��� FINITE aut.states ��� isValidAlterA aut 40 ==> (!q. q ��� aut.states ==> FINITE (aut.trans q))``, 41 rpt strip_tac 42 >> `aut.trans q ��� ((POW aut.alphabet) �� (POW aut.states))` by ( 43 fs[isValidAlterA_def] >> simp[SUBSET_DEF] >> rpt strip_tac 44 >- (Cases_on `x` >> metis_tac[IN_POW,FST]) 45 >- (Cases_on `x` >> metis_tac[IN_POW,SND]) 46 ) 47 >> metis_tac[FINITE_CROSS, FINITE_POW,PSUBSET_DEF,PSUBSET_FINITE] 48 ); 49 50(* 51 RUNs over the alternating automaton 52*) 53 54val _ = Hol_datatype 55 `ALTERA_RUN = <| V : num -> 's set; 56 E : (num # 's) -> 's set 57 |>`; 58 59(* 60 validity condition for runs over a given word 61*) 62 63val validAARunFor_def = Define 64`validAARunFor aut run word = 65 (run.V 0 ��� aut.initial) 66 /\ (!i. run.V i ��� aut.states) 67 /\ (!i q. (q ��� run.V i) 68 ==> ?a. (a,run.E (i,q)) ��� aut.trans q /\ (at word i ��� a)) 69 /\ (!i q. run.E (i,q) ��� run.V (i+1)) 70 /\ (!i q. (q ��� run.V i) 71 ==> ((i = 0) \/ ?q'. (q ��� run.E (i-1,q')) /\ (q' ��� run.V (i-1))))`; 72 73 74(* 75 infinite branches of the run 76*) 77 78val infBranchOf_def = Define 79 `infBranchOf run b = (b 0 ��� run.V 0) /\ !i. (b (i+1) ��� run.E (i, b i))`; 80 81val branchFixP_def = Define 82`branchFixP b x = ?i. (b i = x) /\ !m. (m >= i) ==> (b m = x)`; 83 84val branchRange_def = Define 85`branchRange b = { x | ?i. b i = x }` 86 87val BRANCH_V_LEMM = store_thm 88 ("BRANCH_V_LEMM", 89 ``!run b aut w. validAARunFor aut run w /\ infBranchOf run b 90 ==> !i. (b i ��� run.V i)``, 91 rpt gen_tac >> strip_tac >> Induct_on `i` >> fs[infBranchOf_def] 92 >> `SUC i = (i+1)` by simp[] 93 >> `b (i+1) ��� run.E (i, b i)` by metis_tac[] 94 >> fs[validAARunFor_def] 95 >> `run.E (i, b i) ��� run.V (i+1)` by metis_tac[] 96 >> `SUC i = (i+1)` by simp[] >> metis_tac[SUBSET_DEF] 97 ); 98 99val BRANCHRANGE_LEMM = store_thm 100 ("BRANCHRANGE_LEMM", 101 ``!b aut run w. validAARunFor aut run w /\ infBranchOf run b 102 ==> (branchRange b ��� aut.states)``, 103 rpt strip_tac 104 >> `!i. (b i ��� run.V i)` by metis_tac[BRANCH_V_LEMM] 105 >> fs[validAARunFor_def, branchRange_def, SUBSET_DEF] >> rpt strip_tac 106 >> metis_tac[] 107 ); 108 109val BRANCHRANGE_NONEMPTY = store_thm 110 ("BRANCHRANGE_NONEMPTY", 111 ``!b run. infBranchOf run b ==> ~(branchRange b = {})``, 112 rpt strip_tac 113 >> `~(?x. x ��� branchRange b)` by metis_tac[MEMBER_NOT_EMPTY] 114 >> fs[] 115 >> `?x. x ��� branchRange b` suffices_by metis_tac[] 116 >> qexists_tac `b 0` >> fs[branchRange_def] 117 ); 118 119(* 120 acceptance condition for a run over a given automaton (CO-B��CHI condition) 121*) 122 123val acceptingAARun_def = Define 124`acceptingAARun aut run = 125 !b. infBranchOf run b ==> FINITE {i | b i ��� aut.final }` 126 127(* 128 the language of the automaton 129*) 130 131val runForAA_def = Define 132`runForAA aut run word = 133 validAARunFor aut run word /\ acceptingAARun aut run`; 134 135val alterA_lang_def = Define 136`alterA_lang aut = { w | ?run. runForAA aut run w 137 /\ (word_range w ��� aut.alphabet) }`; 138 139(* 140 Some properties of weak alternating automata 141*) 142 143val BRANCH_WAA_LEMM = store_thm 144 ("BRANCH_WAA_LEMM", 145 ``!b run aut w ord. validAARunFor aut run w /\ infBranchOf run b 146 /\ isVeryWeakWithOrder aut ord 147 ==> !i. (b (i+1), b i) ��� ord``, 148 rpt strip_tac 149 >> `!i. b i ��� run.V i` by metis_tac[BRANCH_V_LEMM] 150 >> fs[isVeryWeakWithOrder_def, infBranchOf_def, validAARunFor_def] 151 >> `(b (i + 1) ��� run.V (i+1)) /\ (b i ��� run.V i)` by metis_tac[] 152 >> `b (i + 1) ��� run.E(i, b i)` by metis_tac[] 153 >> `���a. (a,run.E (i,b i)) ��� aut.trans (b i)` by metis_tac[] 154 >> `b i ��� aut.states` by metis_tac[SUBSET_DEF] 155 >> `���s'. (s' ��� run.E (i, b i)) ��� (s',b i) ��� ord` by metis_tac[] 156 >> metis_tac[] 157 ); 158 159val BRANCH_LIN_ORD = store_thm 160 ("BRANCH_LIN_ORD", 161 ``!b run aut w ord. infBranchOf run b /\ validAARunFor aut run w 162 /\ isVeryWeakWithOrder aut ord 163 ==> linear_order (rrestrict ord (branchRange b)) (branchRange b)``, 164 rpt strip_tac 165 >> `!i. b i ��� run.V i` by metis_tac[BRANCH_V_LEMM] 166 >> `!i. (b (i+1), b i) ��� ord` by metis_tac[BRANCH_WAA_LEMM] 167 >> fs[linear_order_def, branchRange_def, infBranchOf_def, validAARunFor_def] 168 >> fs[isVeryWeakWithOrder_def] 169 >> fs[domain_def, partial_order_def,range_def, in_rrestrict,SUBSET_DEF,branchRange_def] 170 >> rpt strip_tac 171 >- (qexists_tac `i` >> fs[]) 172 >- (qexists_tac `i'` >> fs[]) 173 >- metis_tac[RRESTRICT_TRANS] 174 >- metis_tac[RRESTRICT_ANTISYM] 175 >- (`(x,y) ��� ord \/ (y,x) ��� ord` suffices_by metis_tac[] 176 >> Cases_on `i > i'` 177 >- (`!n. (n > i') ==> ((b n,y) ��� ord)` suffices_by metis_tac[] 178 >> Induct_on `n` >> fs[] >> rpt strip_tac 179 >> Cases_on `n = i'` >> fs[reflexive_def] 180 >- (`SUC i' = i' + 1` by simp[] 181 >> `(b (i'+1), b i') ��� ord` suffices_by metis_tac[] 182 >> metis_tac[] 183 ) 184 >- (`(b (SUC n), b n) ��� ord` suffices_by metis_tac[transitive_def] 185 >> `SUC n = n + 1` by simp[] 186 >> `(b (n+1), b n) ��� ord` suffices_by metis_tac[] >> metis_tac[]) 187 ) 188 >- (Cases_on `i = i'` >> fs[reflexive_def] 189 >- (`b i' ��� run.V i'` by metis_tac[] 190 >> `b i' ��� aut.states` by metis_tac[] >> metis_tac[]) 191 >- (`i' > i` by simp[] 192 >> `!n. (n > i) ==> ((b n,x) ��� ord)` suffices_by metis_tac[] 193 >> Induct_on `n` >> fs[] >> rpt strip_tac 194 >> Cases_on `n = i` >> fs[reflexive_def] 195 >- (`SUC i = i + 1` by simp[] 196 >> `(b (i+1), b i) ��� ord` suffices_by metis_tac[] >> metis_tac[] 197 ) 198 >- (`(b (SUC n), b n) ��� ord` suffices_by metis_tac[transitive_def] 199 >> `SUC n = n + 1` by simp[] 200 >> `(b (n + 1), b n) ��� ord` suffices_by metis_tac[] >> metis_tac[]) 201 ) 202 ) 203 ) 204 ); 205 206val BRANCH_FIXP = store_thm 207 ("BRANCH_FIXP", 208 ``���b run aut w ord. 209 infBranchOf run b ��� validAARunFor aut run w ��� isVeryWeakAlterA aut /\ FINITE aut.states ��� 210 ���x. branchFixP b x``, 211 `���b run aut w ord. 212 infBranchOf run b ��� validAARunFor aut run w ��� isVeryWeakWithOrder aut ord 213 /\ FINITE aut.states ��� 214 ���x. branchFixP b x` suffices_by metis_tac[isVeryWeakAlterA_def] 215 >> rpt strip_tac 216 >> `linear_order (rrestrict ord (branchRange b)) (branchRange b)` 217 by metis_tac[BRANCH_LIN_ORD] 218 >> qabbrev_tac `ord' = rrestrict ord (branchRange b)` 219 >> `FINITE (branchRange b)` by metis_tac[BRANCHRANGE_LEMM,SUBSET_FINITE] 220 >> `~(branchRange b = {})` by metis_tac[BRANCHRANGE_NONEMPTY] 221 >> `���x. x ��� minimal_elements (branchRange b) ord'` 222 by metis_tac[finite_linear_order_has_minimal] 223 >> qexists_tac `x` 224 >> fs[minimal_elements_def, branchFixP_def, branchRange_def] 225 >> qexists_tac `i` >> fs[] >> rpt strip_tac 226 >> fs[linear_order_def] 227 >> `!n. (n >= i) ==> (b n = x)` suffices_by metis_tac[] 228 >> Induct_on `n` 229 >- (Cases_on `i = 0` >> fs[]) 230 >- (rpt strip_tac 231 >> Cases_on `SUC n = i` >> fs[] 232 >> `n >= i` by simp[] >> fs[] 233 >> `b (SUC n) = b n` suffices_by metis_tac[] 234 >> `(b (SUC n),b n) ��� ord' ��� (b n,b (SUC n)) ��� ord'` by metis_tac[] 235 >- metis_tac[] 236 >- (`SUC n = n + 1` by simp[] 237 >> `(b n, b (n+1)) ��� ord'` by metis_tac[] 238 >> `(b (n+1), b n) ��� ord` by metis_tac[BRANCH_WAA_LEMM] 239 >> `(b (n+1),b n) ��� ord'` suffices_by metis_tac[antisym_def] 240 >> metis_tac[in_rrestrict] 241 ) 242 ) 243 ); 244 245val BRANCH_ACC_LEMM = store_thm 246 ("BRANCH_ACC_LEMM", 247 ``!run w aut. validAARunFor aut run w /\ isVeryWeakAlterA aut 248 /\ FINITE aut.states 249 ==> (acceptingAARun aut run = 250 (!b x. infBranchOf run b /\ branchFixP b x ==> ~(x ��� aut.final)))``, 251 rpt strip_tac >> rw[EQ_IMP_THM] 252 >- (CCONTR_TAC >> fs[acceptingAARun_def, branchFixP_def] 253 >> `FINITE {i | b i ��� aut.final}` by metis_tac[] 254 >> `INFINITE ����(:num)` by metis_tac[INFINITE_NUM_UNIV] 255 >> `!x y. ((\x. x+i) x = (\x. x+i) y) ==> (x = y)` 256 by metis_tac[ADD_N_INJ_LEMM] 257 >> `INFINITE (IMAGE (\x. x+i) ����(:num))` by rw[IMAGE_11_INFINITE] 258 >> `INFINITE { x | x >= i }` by metis_tac[ADD_N_IMAGE_LEMM] 259 >> `!m. (m ��� { x | x >= i }) ==> (b m = x)` by simp[] 260 >> `{ x | x >= i } ��� { m | b m = x }` by simp[SUBSET_DEF] 261 >> `{ x | x >= i } ��� { i | b i ��� aut.final }` by simp[SUBSET_DEF] 262 >> `{ x | x >= i } ��� { i | b i ��� aut.final }` by simp[] 263 >> metis_tac[IN_INFINITE_NOT_FINITE,SUBSET_DEF] 264 ) 265 >- (simp[acceptingAARun_def] >> rpt strip_tac 266 >> `���x. branchFixP b x` by metis_tac[BRANCH_FIXP] 267 >> `~(x ��� aut.final)` by metis_tac[] 268 >> fs[branchFixP_def] 269 >> `{i | b i ��� aut.final} ��� (count i)` 270 suffices_by metis_tac[FINITE_COUNT,SUBSET_FINITE] 271 >> fs[SUBSET_DEF] >> rpt strip_tac 272 >> CCONTR_TAC >> `x' >= i` by simp[] >> metis_tac[] 273 ) 274 ); 275 276(* 277 infinite run suffixes 278*) 279 280val infBranchSuffOf_def = Define 281 `infBranchSuffOf run i b = 282 (b 0 ��� run.V i) /\ !j. (b (j+1) ��� run.E (j + i, b j))`; 283 284val appendToBranchSuff_def = Define 285 `appendToBranchSuff b q = \n. if n = 0 then q else b (n-1)`; 286 287val APPEND_LEMMA = store_thm 288 ("APPEND_LEMMA", 289 ``!r b q i aut w. infBranchSuffOf r i b /\ validAARunFor aut r w /\ ~(i=0) 290 /\ q ��� r.V (i-1) /\ (b 0 ��� r.E (i-1,q)) 291 ==> infBranchSuffOf r (i-1) (appendToBranchSuff b q)``, 292 rpt strip_tac >> fs[appendToBranchSuff_def, infBranchSuffOf_def, validAARunFor_def] 293 >> rpt strip_tac 294 >> Induct_on `j` >> fs[] 295 >> `b (j + 1) ��� r.E (i + j,b j)` by metis_tac[] 296 >> `SUC j = j + 1` by simp[] >> rw[] 297 ); 298 299val BRANCH_SUFF_LEMM = store_thm 300 ("BRANCH_SUFF_LEMM", 301 ``!i q run aut w b. validAARunFor aut run w /\ infBranchSuffOf run i b 302 ==> ?b'. infBranchOf run b' /\ !j. (b j = b' (j+i))``, 303 Induct_on `i` >> rpt strip_tac 304 >- (qexists_tac `b` 305 >> fs[infBranchSuffOf_def, infBranchOf_def]) 306 >- (`!q. ~(SUC i = 0) /\ q ��� run.V ((SUC i) ��� 1) ��� b 0 ��� run.E ((SUC i) ��� 1,q) ��� 307 infBranchSuffOf run ((SUC i) ��� 1) (appendToBranchSuff b q)` 308 by metis_tac[APPEND_LEMMA] 309 >> `!b. infBranchSuffOf run i b 310 ��� ���b'. infBranchOf run b' ��� ���j. (b j = b' (j + i))` 311 by metis_tac[] 312 >> fs[validAARunFor_def, infBranchSuffOf_def] >> rpt strip_tac 313 >> `((SUC i) = 0) ��� ���q'. b 0 ��� run.E ((SUC i) ��� 1,q') 314 ��� (q' ��� run.V ((SUC i) ��� 1))` 315 by metis_tac[] 316 >> fs[] 317 >> `appendToBranchSuff b q' 0 ��� run.V i ��� 318 ���j. 319 appendToBranchSuff b q' (j + 1) ��� 320 run.E (i + j,appendToBranchSuff b q' j)` 321 by metis_tac[] 322 >> qabbrev_tac `b_new = appendToBranchSuff b q'` 323 >> `���b'. infBranchOf run b' ��� ���j. (b_new j = b' (i + j))` 324 by metis_tac[] 325 >> qexists_tac `b'` >> fs[appendToBranchSuff_def] 326 >> rpt strip_tac 327 >> `SUC i <= j ==> i <= (SUC j)` by simp[] 328 >> `(b_new (SUC j) = b' (i + (SUC j)))` by metis_tac[] 329 >> fs[] 330 >> `~(SUC j = 0) ==> (b_new (SUC j) = b (SUC j - 1))` by metis_tac[] 331 >> fs[] 332 >> `(i + SUC j) = (j + SUC i)` by simp[] 333 >> metis_tac[] 334 ) 335 ); 336 337(* reachable states *) 338 339val oneStep_def = Define` 340 oneStep aut = \x y. ?a qs. (a,qs) ��� aut.trans x ��� y ��� qs ��� x ��� aut.states`; 341 342val reachRel_def = Define` 343 reachRel aut = (oneStep aut)^*`; 344 345val reachRelFromSet_def = Define` 346 reachRelFromSet aut s = { y | ?x. reachRel aut x y ��� x ��� s }`; 347 348(*TODO rewrite using different reach rel*) 349 350(* val nStepReachable_def = Define` *) 351(* (nStepReachable trans init 0 = init) *) 352(* ��� (nStepReachable trans init (SUC i) = *) 353(* {s | ?a qs s'. (a, qs) ��� trans s' ��� s' ��� nStepReachable trans init i *) 354(* ��� s ��� qs})`; *) 355 356(* val reachable_def = Define` *) 357(* (reachable trans init = {s | ?n. s ��� nStepReachable trans init n })`; *) 358 359(* val reachableRel_def = Define` *) 360(* reachableRel aut = *) 361(* { (s, s') | s ��� reachable aut.trans {s'} *) 362(* ��� s ��� aut.states ��� s' ��� aut.states}`; *) 363 364(* val REACHABLE_LEMM = store_thm *) 365(* ("REACHABLE_LEMM", *) 366(* ``!aut x. isValidAlterA aut ��� (x ��� aut.states) *) 367(* ==> (reachable aut.trans {x} ��� aut.states)``, *) 368(* rpt strip_tac *) 369(* >> `!n. nStepReachable aut.trans {x} n ��� aut.states` by ( *) 370(* Induct_on `n` >> fs[nStepReachable_def] *) 371(* >> simp[SUBSET_DEF] >> rpt strip_tac *) 372(* >> metis_tac[isValidAlterA_def,SUBSET_DEF] *) 373(* ) *) 374(* >> simp[reachable_def,SUBSET_DEF] >> rpt strip_tac *) 375(* >> metis_tac[SUBSET_DEF] *) 376(* ); *) 377 378(* val WAA_REACH_IS_PO = store_thm *) 379(* ("WAA_REACH_IS_PO", *) 380(* ``!aut. isWeakAlterA aut ��� isValidAlterA aut *) 381(* ==> isWeakWithOrder aut (reachableRel aut)``, *) 382(* fs[isWeakAlterA_def] >> simp[isWeakWithOrder_def] >> rpt strip_tac *) 383(* >- (fs[partial_order_def] >> rpt strip_tac *) 384(* >- (simp[reachableRel_def,domain_def,SUBSET_DEF] >> rpt strip_tac) *) 385(* >- (simp[reachableRel_def,range_def,SUBSET_DEF] >> rpt strip_tac) *) 386(* >- (simp[reachableRel_def,transitive_def] >> rpt strip_tac *) 387(* >> fs[reachable_def] >> qexists_tac `n + n'` *) 388(* >> `!j1 j2 p q r. *) 389(* p ��� nStepReachable aut.trans {q} j1 ��� *) 390(* r ��� nStepReachable aut.trans {p} j2 *) 391(* ==> r ��� nStepReachable aut.trans {q} (j1 + j2)` by ( *) 392(* Induct_on `j2` >> rpt strip_tac >> fs[nStepReachable_def] *) 393(* >> `r ��� nStepReachable aut.trans {q} (SUC (j1 + j2))` *) 394(* suffices_by metis_tac[SUC_ADD_SYM,ADD_COMM] *) 395(* >> simp[nStepReachable_def] >> metis_tac[] *) 396(* ) *) 397(* >> metis_tac[ADD_COMM] *) 398(* ) *) 399(* >- (fs[reflexive_def,reachableRel_def,reachable_def] >> rpt strip_tac *) 400(* >> qexists_tac `0` >> fs[nStepReachable_def] *) 401(* ) *) 402(* >- (fs[antisym_def,reachableRel_def,reachable_def] >> rpt strip_tac *) 403(* >> `!i p q. p ��� aut.states ��� q ��� aut.states *) 404(* ��� p ��� nStepReachable aut.trans {q} i ==> (p,q) ��� ord` by ( *) 405(* Induct_on `i` >> rpt strip_tac *) 406(* >- fs[reflexive_def,nStepReachable_def] *) 407(* >- (fs[nStepReachable_def] *) 408(* >> `s' ��� aut.states` by ( *) 409(* `s' ��� reachable aut.trans {q}` *) 410(* by (simp[reachable_def] >> metis_tac[]) *) 411(* >> metis_tac[SUBSET_DEF,REACHABLE_LEMM]) *) 412(* >> `(s',q) ��� ord` by metis_tac[] *) 413(* >> fs[transitive_def] >> metis_tac[] *) 414(* ) *) 415(* ) *) 416(* >> metis_tac[] *) 417(* ) *) 418(* ) *) 419(* >- (fs[reachableRel_def,reachable_def] >> strip_tac *) 420(* >- (qexists_tac `SUC 0` >> simp[nStepReachable_def] >> metis_tac[]) *) 421(* >- (fs[isValidAlterA_def] >> metis_tac[SUBSET_DEF]) *) 422(* ) *) 423(* ); *) 424 425 426(* 427 restricting a run to a subset of its initial states 428*) 429 430val run_restr_V_def = Define ` 431 (run_restr_V init r_old (SUC i) = 432 BIGUNION { e | ?q. (e = r_old.E (i,q)) /\ (q ��� run_restr_V init r_old i) }) 433 /\ (run_restr_V init r_old 0 = init)`; 434 435val run_restr_E_def = Define ` 436 (run_restr_E init r_old (i,q) = 437 if q ��� run_restr_V init r_old i then r_old.E (i,q) else {})`; 438 439val run_restr_def = Define ` 440 (run_restr init r_old = ALTERA_RUN (run_restr_V init r_old) (run_restr_E init r_old))`; 441 442val RUN_RESTR_LEMM = store_thm 443 ("RUN_RESTR_LEMM", 444 ``!r init aut w. (validAARunFor aut r w) /\ (init ��� r.V 0) 445 ==> !i. run_restr_V init r i ��� r.V i``, 446 rpt strip_tac >> Induct_on `i` >> fs[run_restr_V_def] 447 >> fs[validAARunFor_def, SUBSET_DEF] >> rpt strip_tac 448 >> `(s = r.E (i,q)) ��� q ��� run_restr_V init r i` by metis_tac[] 449 >> `x ��� r.E (i,q)` by metis_tac[] 450 >> `x ��� r.V (i + 1)` by metis_tac[] 451 >> `x ��� r.V (i + 1)` suffices_by simp[SUC_ONE_ADD] >> fs[] 452 ); 453 454val RUN_RESTR_FIXP_LEMM = store_thm 455 ("RUN_RESTR_FIXP_LEMM", 456 ``!r init aut w b. (validAARunFor aut r w) /\ (init ��� r.V 0) 457 /\ (infBranchOf (run_restr init r) b) 458 ==> infBranchOf r b``, 459 rpt strip_tac >> fs[infBranchOf_def] >> rpt strip_tac 460 >> fs[run_restr_def, run_restr_V_def] 461 >- (metis_tac[SUBSET_DEF]) 462 >- (fs[run_restr_E_def] >> Cases_on `b i ��� (run_restr_V init r i)` >> fs[] 463 >- metis_tac[] 464 >- (metis_tac[NOT_IN_EMPTY]) 465 ) 466 ); 467 468(* 469 conjoining two runs 470*) 471 472val conj_run_branch_cond_def = Define ` 473 conj_run_branch_cond r1 r2 s q i = 474 if q ��� s 475 then (if q ��� r1.V i 476 then r1.E (i,q) 477 else if q ��� r2.V i 478 then r2.E (i,q) 479 else {}) 480 else {}`; 481 482val conj_run_V_def = Define ` 483 (conj_run_V r1 r2 (SUC i) = 484 BIGUNION { e | ?q. (e = conj_run_branch_cond r1 r2 (conj_run_V r1 r2 i) q i) 485 /\ (q ��� conj_run_V r1 r2 i)}) 486 /\ (conj_run_V r1 r2 0 = r1.V 0 ��� r2.V 0)`; 487 488val conj_run_E_def = Define ` 489 (conj_run_E r1 r2 (i,q) = 490 conj_run_branch_cond r1 r2 (conj_run_V r1 r2 i) q i)`; 491 492val conj_run_def = Define ` 493 conj_run r1 r2 = ALTERA_RUN (conj_run_V r1 r2) (conj_run_E r1 r2)`; 494 495val CONJ_RUN_V_LEMM = store_thm 496 ("CONJ_RUN_V_LEMM", 497 ``!r1 r2 i w1 w2 a1 a2. validAARunFor a1 r1 w1 /\ validAARunFor a2 r2 w2 498 ==> conj_run_V r1 r2 i ��� (r1.V i ��� r2.V i)``, 499 rpt strip_tac >> Induct_on `i` >> fs[conj_run_V_def] 500 >> fs[SUBSET_DEF, BIGUNION, conj_run_V_def] 501 >> rpt strip_tac >> fs[conj_run_E_def, conj_run_branch_cond_def] 502 >> Cases_on `q ��� r1.V i` 503 >- (fs[validAARunFor_def] >> `SUC i = i +1` by simp[] 504 >> metis_tac[SUBSET_DEF]) 505 >- (Cases_on `q ��� r2.V i` 506 >- (fs[validAARunFor_def] >> `SUC i = i +1` by simp[] 507 >> metis_tac[SUBSET_DEF]) 508 >- (fs[]) 509 ) 510 ); 511 512val CONJ_RUN_FIXP_LEMM = store_thm 513 ("CONJ_RUN_FIXP_LEMM", 514 ``!r1 r2 b x a1 a2 w. (validAARunFor a1 r1 w) /\ (validAARunFor a2 r2 w) 515 /\ (infBranchOf (conj_run r1 r2) b) /\ (branchFixP b x) 516 ==> (?b'. (infBranchOf r1 b' \/ infBranchOf r2 b') /\ branchFixP b' x)``, 517 rpt strip_tac 518 >> `!i. conj_run_V r1 r2 i ��� (r1.V i ��� r2.V i)` by metis_tac[CONJ_RUN_V_LEMM] 519 >> fs[infBranchOf_def] 520 >> `!i. b (i+1) ��� (conj_run r1 r2).E (i, b i)` by metis_tac[] 521 >> fs[conj_run_def, conj_run_E_def, conj_run_branch_cond_def] 522 >> `!i. b i ��� conj_run_V r1 r2 i` by metis_tac[NOT_IN_EMPTY] 523 >> `!i. b i ��� r1.V i \/ b i ��� r2.V i` by fs[SUBSET_DEF, UNION_DEF] 524 >> fs[branchFixP_def] 525 >> `(?a. a >= i /\ b a ��� r1.V a) \/ (!a. (a >= i) ==> ~(b a ��� r1.V a) /\ (b a ��� r2.V a))` 526 by metis_tac[] 527 >- (dsimp[] 528 >> `(���b' i. 529 (b' 0 ��� r1.V 0 ��� ���i. b' (i + 1) ��� r1.E (i,b' i)) 530 ��� (b' i = x) /\ !m. (m >= i) ==> (b' m = x))` 531 suffices_by metis_tac[] 532 >> qabbrev_tac `b_suff = \j. b (a + j)` 533 >> SUBGOAL_THEN ``infBranchSuffOf r1 a b_suff`` mp_tac 534 >- (fs[infBranchSuffOf_def] >> rpt strip_tac >> fs[] 535 >- (`b_suff 0 = b (a+0)` by simp[] 536 >> `a + 0 = a` by simp[] >> metis_tac[] 537 ) 538 >- (`!j. (a+j) >= i` by simp[] 539 >> `b_suff (j+1) = b (a + j)` by metis_tac[] 540 >> `b (a + j) = x` by metis_tac[] 541 >> fs[conj_run_V_def, conj_run_branch_cond_def] 542 >> SUBGOAL_THEN ``!n. (b (a + n) ��� r1.V (a+n))`` mp_tac 543 >- (Induct_on `n` >> fs[] 544 >- (`b_suff 0 = b (a + 0)` by metis_tac[] 545 >> fs[] >> `b a = x` by simp[] >> metis_tac[]) 546 >- (`b (a + n + 1) ��� r1.E (a+n, b (a+n))` by metis_tac[] 547 >> fs[validAARunFor_def] 548 >> `b (a + n + 1) ��� r1.V (a + n + 1)` 549 by metis_tac[SUBSET_DEF] 550 >> fs[] 551 >> `b (a + (n + 1)) = b_suff (n + 1)` by metis_tac[] 552 >> `b_suff (SUC n) ��� r1.V (a + (SUC n))` 553 by metis_tac[SUC_ONE_ADD, ADD_SYM] 554 ) 555 ) 556 >- (rpt strip_tac 557 >> `b (a + j) ��� r1.V (a + j)` by metis_tac[] 558 >> `b ((a + j) + 1) ��� r1.E (a + j, b (a + j))` by metis_tac[] 559 >> `b (a + j + 1) = x` by simp[] 560 >> fs[] 561 >> `b_suff j = b (a + j)` by metis_tac[] >> metis_tac[] 562 ) 563 ) 564 ) 565 >- (rpt strip_tac 566 >> `���b'. infBranchOf r1 b' ��� ���j. (b_suff j = b' (j + a))` 567 by metis_tac[BRANCH_SUFF_LEMM] 568 >> qexists_tac `b'` >> qexists_tac `a` >> rpt strip_tac >> fs[infBranchOf_def] 569 >- (`a + 0 = a` by simp[] 570 >> `b_suff 0 = x` suffices_by metis_tac[] 571 >> `b_suff 0 = b a` by metis_tac[] 572 >> fs[] 573 ) 574 >- (`a <= m` by simp[] 575 >> `?p. p + a = m` by metis_tac[LESS_EQ_ADD_EXISTS] 576 >> `b_suff p = b' m` by metis_tac[ADD_COMM] 577 >> `b_suff p = b (a + p)` by metis_tac[ADD_COMM] 578 >> `a + p >= i` by simp[] >> metis_tac[] 579 ) 580 ) 581 ) 582 >- (dsimp[] 583 >> `(���b' i. 584 (b' 0 ��� r2.V 0 ��� ���i. b' (i + 1) ��� r2.E (i,b' i)) 585 ��� (b' i = x) /\ !m. (m >= i) ==> (b' m = x))` 586 suffices_by metis_tac[] 587 >> `i >= i` by simp[] >> `b i ��� r2.V i` by metis_tac[] 588 >> qabbrev_tac `b_suff = \j. b (i + j)` 589 >> SUBGOAL_THEN ``infBranchSuffOf r2 i b_suff`` mp_tac 590 >- (fs[infBranchSuffOf_def] >> rpt strip_tac >> fs[] 591 >- (`b_suff 0 = b (i+0)` by simp[] 592 >> `i + 0 = i` by simp[] >> metis_tac[] 593 ) 594 >- (`!j. (i+j) >= i` by simp[] 595 >> `b_suff (j+1) = b (i + j)` by metis_tac[] 596 >> `b (i + j) = x` by metis_tac[] 597 >> fs[conj_run_V_def, conj_run_branch_cond_def] 598 >> rpt strip_tac 599 >> `i + j >= i` by simp[] 600 >> `b (i + j) ��� r2.V (i + j)` by metis_tac[] 601 >> `b ((i + j) + 1) ��� r2.E (i + j, b (i + j))` by metis_tac[] 602 >> `b (i + j + 1) = x` by simp[] 603 >> fs[] 604 >> `b_suff j = b (i + j)` by metis_tac[] >> metis_tac[] 605 ) 606 ) 607 >- (rpt strip_tac 608 >> `���b'. infBranchOf r2 b' ��� ���j. (b_suff j = b' (j + i))` 609 by metis_tac[BRANCH_SUFF_LEMM] 610 >> qexists_tac `b'` >> qexists_tac `i` >> rpt strip_tac 611 >> fs[infBranchOf_def] 612 >- (`i + 0 = i` by simp[] 613 >> `b_suff 0 = x` suffices_by metis_tac[] 614 >> `b_suff 0 = b i` by metis_tac[] 615 >> fs[] 616 ) 617 >- (`i <= m` by simp[] 618 >> `?p. p + i = m` by metis_tac[LESS_EQ_ADD_EXISTS] 619 >> `b_suff p = b' m` by metis_tac[ADD_COMM] 620 >> `b_suff p = b (i + p)` by metis_tac[ADD_COMM] 621 >> `i + p >= i` by simp[] >> metis_tac[] 622 ) 623 ) 624 ) 625 ); 626 627(* 628 suffix run with replaced initial states 629*) 630 631val REPL_RUN_CONSTR_LEMM = store_thm 632 ("REPL_RUN_CONSTR_LEMM", 633 ``!aut run w e h j. 634 let run_int = 635 ALTERA_RUN (\i. if i = 0 then e else run.V (i + j)) 636 (��(i,q). if i = 0 then h q else run.E (i + j,q)) 637 in 638 validAARunFor aut run w /\ (!q. q ��� e ==> h q ��� run.V (j + 1)) 639 ==> !i. (run_restr e run_int).V (i+1) ��� run.V (i+j+1)``, 640 fs[] >> rpt gen_tac >> rpt conj_tac >> strip_tac 641 >> Induct_on `i` >> fs[run_restr_def, run_restr_V_def, run_restr_E_def, validAARunFor_def] 642 >- (fs[SUBSET_DEF] >> rpt strip_tac 643 >> `1 = SUC 0` by simp[] 644 >> `x ��� 645 run_restr_V e 646 (ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 647 (��(i,q). if i = 0 then h q else run.E (i + j,q))) (SUC 0)` by fs[] 648 >> fs[run_restr_V_def] 649 >> metis_tac[] 650 ) 651 >- (fs[SUBSET_DEF] >> rpt strip_tac 652 >> `SUC i + 1 = SUC (i + 1)` by simp[] 653 >> `x ��� 654 run_restr_V e 655 (ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 656 (��(i,q). if i = 0 then h q else run.E (i + j,q))) (SUC (i + 1))` 657 by metis_tac[] 658 >> fs[run_restr_V_def] 659 >> `x ��� run.V ((i + (j + 1)) + 1)` by metis_tac[] 660 >> `j + (SUC i + 1) = i + (j + 1) + 1` by simp[] 661 >> metis_tac[] 662 ) 663 ); 664 665val REPL_LEMM_1 = store_thm 666 ("REPL_LEMM_1", 667 ``!aut run w e h b x j. 668 let run_int = 669 ALTERA_RUN (\i. if i = 0 then e else run.V (i + j)) 670 (��(i,q). if i = 0 then h q else run.E (i + j,q)) 671 in 672 validAARunFor aut run w /\ (!q. q ��� e ==> h q ��� run.V (1 + j)) 673 /\ infBranchOf (run_restr e run_int) b /\ branchFixP b x 674 ==> infBranchSuffOf run (1 + j) (\i. b (i + 1))``, 675 fs[infBranchSuffOf_def] >> rpt strip_tac 676 >- (fs[infBranchOf_def, run_restr_def] 677 >> fs[run_restr_E_def] 678 >> `b 0 ��� e` by metis_tac[run_restr_V_def] 679 >> `b (0 + 1) ��� h (b 0)` by metis_tac[run_restr_E_def, run_restr_V_def] 680 >> fs[] 681 >> `h (b 0) ��� run.V (1+j)` by fs[] 682 >> metis_tac[SUBSET_DEF] 683 ) 684 >- (rename [���b (i + 2) ��� run.E _���] >> Induct_on `i` >> fs[] 685 >- (fs[infBranchOf_def, run_restr_def, run_restr_E_def, run_restr_V_def] 686 >> `b (1 + 1) ��� run.E (j + 1, b 1)` suffices_by simp[] 687 >> `b (1 + 1) ��� 688 if 689 b 1 ��� 690 run_restr_V e 691 (ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 692 (��(i,q). if i = 0 then h q else run.E (i + j,q))) 1 693 then 694 if 1 = 0 then h (b 0) else run.E (1+j,b 1) 695 else ���` by fs[] 696 >> fs[] 697 >> Cases_on `b 1 ��� 698 run_restr_V e 699 (ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 700 (��(i,q). if i = 0 then h q else run.E (i + j,q))) 1` 701 >> fs[]) 702 >- (fs[infBranchOf_def, run_restr_def, run_restr_E_def, run_restr_V_def] 703 >> `SUC i + 2 = (i + 2) + 1` by simp[] 704 >> `b (i + 2 + 1) ��� run.E (j + (SUC i + 1),b (SUC i + 1))` 705 suffices_by metis_tac[] 706 >> `b ((i + 2) + 1) ��� 707 if 708 b (i + 2) ��� 709 run_restr_V e 710 (ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 711 (��(i,q). if i = 0 then h q else run.E (i + j,q))) (i + 2) 712 then 713 if (i + 2) = 0 then h (b 0) else run.E ((i + 2) + j,b (i + 2)) 714 else ���` by fs[] 715 >> qabbrev_tac `r' = (ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 716 (��(i,q). if i = 0 then h q else run.E (i+j,q)))` 717 >> Cases_on `b (i + 2) ��� run_restr_V e r' (i + 2)` 718 >- (fs[] >> `SUC (i + 1) = i + 2` by simp[] >> fs[] 719 >> `b (i + 3) ��� run.E (j + (1 + i) + 1, b ((1 + i) + 1))` 720 suffices_by simp[SUC_ONE_ADD] 721 >> simp[]) 722 >- metis_tac[NOT_IN_EMPTY] 723 ) 724 ) 725 ); 726 727val REPL_RUN_CONSTR_LEMM2 = store_thm 728 ("REPL_RUN_CONSTR_LEMM2", 729 ``!aut run w e h b x j. 730 let run_int = 731 ALTERA_RUN (\i. if i = 0 then e else run.V (i + j)) 732 (��(i,q). if i = 0 then h q else run.E (i + j,q)) 733 in 734 validAARunFor aut run w /\ (!q. q ��� e ==> h q ��� run.V (1 + j)) 735 /\ infBranchOf (run_restr e run_int) b /\ branchFixP b x 736 ==> ?b'. infBranchOf run b' /\ branchFixP b' x``, 737 fs[] >> rpt strip_tac 738 >> `(let run_int = 739 ALTERA_RUN (��i. if i = 0 then e else run.V (i + j)) 740 (��(i,q). if i = 0 then h q else run.E (i + j,q)) 741 in 742 validAARunFor aut run w ��� (���q. q ��� e ��� h q ��� run.V (1+j)) ��� 743 infBranchOf (run_restr e run_int) b ��� branchFixP b x ��� 744 infBranchSuffOf run (1+j) (��i. b (i + 1)))` 745 by metis_tac[REPL_LEMM_1] 746 >> fs[] >> `infBranchSuffOf run (j + 1) (��i. b (i + 1))` by metis_tac[] 747 >> qabbrev_tac `b_new = \i. b (i + 1)` 748 >> `���b'. infBranchOf run b' ��� ���n. b_new n = b' (n + (j + 1))` 749 by metis_tac[BRANCH_SUFF_LEMM] 750 >> qexists_tac `b'` >> fs[] 751 >> fs[branchFixP_def] 752 >> qunabbrev_tac `b_new` 753 >> qexists_tac `j + (i+1)` >> rpt strip_tac 754 >- (`(i + 1) >= i` by simp[] 755 >> `b (i + 1) = x` by metis_tac[] 756 >> fs[] >> metis_tac[ADD_ASSOC, ADD_COMM] 757 ) 758 >- (`m >= i` by simp[] 759 >> `b m = x` by simp[] 760 >> `m >= j + 1` by simp[] 761 >> `?k. m = j + k + 1` by 762 (`?p. p + (j + 1) = m` by simp[LESS_EQ_ADD_EXISTS] 763 >> qexists_tac `p` >> fs[]) 764 >> `k + 1 >= i` by simp[] 765 >> `b (k + 1) = x` by metis_tac[] 766 >> rw[] >> metis_tac[] 767 ) 768 ); 769 770 771(* 772 step function of a run 773*) 774 775val step_def = Define 776 `step run (v,i) = (BIGUNION {run.E (i,q) | q ��� v }, i+1)`; 777 778val STEP_THM = store_thm 779 ("STEP_THM", 780 ``!aut run. (?w. validAARunFor aut run w) 781 ==> !i. (FUNPOW (step run) i (run.V 0,0) = (run.V i,i))``, 782 strip_tac >> strip_tac >> strip_tac 783 >> Induct_on `i` >> fs[FUNPOW] 784 >> fs[validAARunFor_def] 785 >> `FUNPOW (step run) (SUC i) (run.V 0, 0) 786 = FUNPOW (step run) i (step run (run.V 0, 0))` by metis_tac[FUNPOW] 787 >> `FUNPOW (step run) (SUC i) (run.V 0,0) = step run (FUNPOW (step run) i (run.V 0,0))` 788 by metis_tac[FUNPOW_SUC] 789 >> `FUNPOW (step run) (SUC i) (run.V 0,0) = step run (run.V i,i)` by metis_tac[] 790 >> `step run (run.V i, i) = (run.V (SUC i), SUC i)` suffices_by metis_tac[] 791 >> rw[step_def] >> fs[validAARunFor_def] 792 >> `(BIGUNION {run.E (i,q) | q | q ��� run.V i} ��� run.V (SUC i)) 793 /\ (run.V (SUC i) ��� BIGUNION {run.E (i,q) | q | q ��� run.V i})` 794 suffices_by metis_tac[SET_EQ_SUBSET] 795 >> rpt strip_tac 796 >- (simp[SUBSET_DEF, BIGUNION] >> rpt strip_tac 797 >> `run.E (i,q) ��� run.V (i + 1)` by metis_tac[] 798 >> fs[SUBSET_DEF] >> `x ��� run.V (i+1)` by metis_tac[] 799 >> `(SUC i) = (i + 1)` suffices_by metis_tac[] >> simp[] 800 ) 801 >- (simp[SUBSET_DEF, BIGUNION] >> rpt strip_tac 802 >> `((SUC i) = 0) ��� ���q'. x ��� run.E ((SUC i) ��� 1,q') ��� q' ��� run.V ((SUC i) ��� 1)` 803 by metis_tac[] >> fs[] 804 >> qexists_tac `run.E (i,q')` >> rpt strip_tac >> fs[] 805 >> qexists_tac `q'` >> simp[] 806 ) 807 ); 808 809 810(* An example alternating automata *) 811 812val A1_def = Define `A1 = ALTER_A {1;2} {T;F} (\_. {({T;F}, {1;2})}) {{1}} {2}`; 813 814val AUT_EX_1 = store_thm 815 ("AUT_EX_1", 816 ``isValidAlterA A1``, 817 simp[isValidAlterA_def, A1_def, POW_DEF] 818 ); 819 820val AUT_EX_2 = store_thm 821 ("AUT_EX_2", 822 ``~(isVeryWeakAlterA A1)``, 823 simp[A1_def, isVeryWeakAlterA_def, isVeryWeakWithOrder_def] >> rw[] >> 824 `partial_order ord {1;2} 825 ==> (?s. ((s = 1) \/ (s = 2)) /\ ?s'. ((s' = 1) \/ (s' = 2)) /\ ~((s, s') ��� ord))` 826 suffices_by metis_tac[] 827 >> rw[] >> CCONTR_TAC >> fs[] >> `((1,2) ��� ord) /\ ((2,1) ��� ord)` by metis_tac[] 828 >> `1 <> 2 /\ {1;2} 1 /\ {1;2} 2` 829 suffices_by metis_tac[partial_order_def, antisym_def] >> simp[] 830 ); 831 832val _ = export_theory(); 833