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