1open HolKernel Parse bossLib boolLib pairTheory relationTheory set_relationTheory pred_setTheory arithmeticTheory whileTheory 2 3open alterATheory ltlTheory ltl2waaTheory 4 5val _ = new_theory "waaSimpl" 6 7(* 8 Reducing the amount of transitions 9*) 10 11val trans_implies_def = Define` 12 trans_implies (a1,q1) (a2,q2) = a2 ��� a1 ��� q1 ��� q2`; 13 14val TRANS_IMPL_PO = store_thm 15 ("TRANS_IMPL_PO", 16 ``!d. partial_order (rrestrict (rel_to_reln trans_implies) d) d``, 17 fs[partial_order_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac 18 >- (fs[domain_def,SUBSET_DEF] >> rpt strip_tac) 19 >- (fs[range_def, SUBSET_DEF] >> rpt strip_tac) 20 >- (fs[transitive_def,SUBSET_DEF,trans_implies_def] >> rpt strip_tac 21 >> Cases_on `x` >> Cases_on `y` >> Cases_on `z` 22 >> fs[trans_implies_def] >> metis_tac[SUBSET_TRANS]) 23 >- (fs[reflexive_def,SUBSET_DEF,trans_implies_def] >> rpt strip_tac 24 >> Cases_on `x` >> fs[trans_implies_def] >> metis_tac[SUBSET_REFL]) 25 >- (fs[antisym_def,SUBSET_DEF,trans_implies_def] >> rpt strip_tac 26 >> Cases_on `x` >> Cases_on `y` 27 >> fs[trans_implies_def] >> metis_tac[SUBSET_ANTISYM]) 28 ); 29 30val TRANS_IMPL_FINITE = store_thm 31 ("TRANS_IMPL_FINITE", 32 ``!d. FINITE d ==> finite_prefixes (rrestrict (rel_to_reln trans_implies) d) d``, 33 fs[finite_prefixes_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac 34 >> `FINITE {e' | e' ��� (\x. trans_implies x e) ��� e' ��� d }` suffices_by fs[IN_DEF] 35 >> metis_tac[INTER_DEF, INTER_FINITE,INTER_COMM] 36 ); 37 38val TRANS_IMPL_MIN_LEMM = store_thm 39 ("TRANS_IMPL_MIN_LEMM", 40 ``!run q aut w i. validAARunFor aut run w ��� q ��� run.V i ��� isValidAlterA aut 41 ��� FINITE aut.states ��� FINITE aut.alphabet 42 ==> ?t. t ��� minimal_elements (aut.trans q) 43 (rrestrict (rel_to_reln trans_implies) (aut.trans q)) ��� 44 trans_implies t 45 ((@a. (a,run.E (i,q)) ��� aut.trans q ��� at w i ��� a), 46 run.E (i,q))``, 47 rpt strip_tac 48 >> `FINITE (aut.trans q)` 49 by metis_tac[FINITE_LEMM,SUBSET_DEF,validAARunFor_def] 50 >> qabbrev_tac `a' = (@a. (a,run.E (i,q)) ��� aut.trans q ��� at w i ��� a)` 51 >> qabbrev_tac `trans_impl_r = (rrestrict (rel_to_reln trans_implies) (aut.trans q))` 52 >> `?t. t ��� minimal_elements (aut.trans q) trans_impl_r ��� 53 (t, (a',run.E (i,q))) ��� trans_impl_r` suffices_by ( 54 qunabbrev_tac `trans_impl_r` >> qunabbrev_tac `a'` 55 >> fs[rrestrict_def, rel_to_reln_def] >> rpt strip_tac 56 >> metis_tac[] 57 ) 58 >> Cases_on `(a', run.E (i,q)) ��� minimal_elements (aut.trans q) trans_impl_r` 59 >- (qexists_tac `(a', run.E (i,q))` >> qunabbrev_tac `trans_impl_r` 60 >> fs[rrestrict_def, rel_to_reln_def, trans_implies_def] 61 >> qunabbrev_tac `a'` 62 >> fs[validAARunFor_def] 63 >> metis_tac[SELECT_THM,SUBSET_DEF] 64 ) 65 >-(HO_MATCH_MP_TAC finite_prefix_po_has_minimal_path 66 >> qexists_tac `aut.trans q` 67 >> fs[validAARunFor_def] >> qunabbrev_tac `a'` 68 >> qunabbrev_tac `trans_impl_r` 69 >> metis_tac[SUBSET_DEF,SELECT_THM,TRANS_IMPL_FINITE,TRANS_IMPL_PO] 70 ) 71 ); 72 73val removeImplied_def = Define` 74 removeImplied trans x = 75 (trans x) DIFF {t | ?t'. ~(t = t') ��� t' ��� (trans x) ��� trans_implies t' t}`; 76 77val reduceTransSimpl_def = Define` 78 reduceTransSimpl (ALTER_A s a trans i f) = 79 ALTER_A s a (removeImplied trans) i f`; 80 81val REDUCE_IS_WEAK = store_thm 82 ("REDUCE_IS_WEAK", 83 ``!aut. isVeryWeakAlterA aut ==> isVeryWeakAlterA (reduceTransSimpl aut)``, 84 rpt strip_tac >> fs[isVeryWeakAlterA_def] >> qexists_tac `ord` 85 >> fs[isVeryWeakWithOrder_def] >> Cases_on `aut` >> fs[reduceTransSimpl_def] 86 >> fs[removeImplied_def] >> metis_tac[] 87 ); 88 89val reduced_E_def = Define` 90 reduced_E run trans word (i,q) = 91 let a = $@ (\a. (a,run.E (i,q)) ��� trans q ��� at word i ��� a) 92 in if ?a' q'. (a',q') ��� trans q ��� trans_implies (a',q') (a,run.E (i,q)) 93 then SND 94 ($@ \t. (t ��� minimal_elements 95 (trans q) 96 (rrestrict (rel_to_reln trans_implies) (trans q))) 97 ��� trans_implies t (a,run.E (i,q))) 98 else run.E(i,q)`; 99 100val reduced_run_def = Define` 101 reduced_run run w trans = 102 run_restr (run.V 0) (ALTERA_RUN run.V (reduced_E run trans w))`; 103 104val REDUCE_TRANS_CORRECT = store_thm 105 ("REDUCE_TRANS_CORRECT", 106 ``!aut. FINITE aut.states ��� FINITE aut.alphabet ��� isValidAlterA aut 107 ��� isVeryWeakAlterA aut 108 ==> (alterA_lang aut = alterA_lang (reduceTransSimpl aut))``, 109 rw[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 110 >- (qexists_tac `reduced_run run x aut.trans` >> fs[runForAA_def] 111 >> `(validAARunFor (reduceTransSimpl aut) (reduced_run run x aut.trans) x ��� 112 (validAARunFor (reduceTransSimpl aut) (reduced_run run x aut.trans) x 113 ==> acceptingAARun (reduceTransSimpl aut) (reduced_run run x aut.trans))) ��� 114 word_range x ��� (reduceTransSimpl aut).alphabet` suffices_by fs[] 115 >> rpt strip_tac 116 >> `!i. (reduced_run run x aut.trans).V i ��� run.V i` by ( 117 Induct_on `i` >> simp[SUBSET_DEF] >> rpt strip_tac 118 >> fs[reduced_run_def, run_restr_def, run_restr_V_def,reduced_E_def] 119 >> Cases_on `���a' q'. 120 (a',q') ��� aut.trans q ��� 121 trans_implies (a',q') 122 ((@a. (a,run.E (i,q)) ��� aut.trans q ��� at x i ��� a), 123 run.E (i,q))` 124 >> fs[] 125 >> qabbrev_tac `minE = \t. t ��� minimal_elements (aut.trans q) 126 (rrestrict (rel_to_reln trans_implies) (aut.trans q)) ��� 127 trans_implies t 128 ((@a. (a,run.E (i,q)) ��� aut.trans q ��� at x i ��� a), 129 run.E (i,q))` 130 >- (`?t. minE t` by ( 131 qunabbrev_tac `minE` 132 >> `q ��� run.V i` by fs[SUBSET_DEF] >> fs[] 133 >> HO_MATCH_MP_TAC TRANS_IMPL_MIN_LEMM >> fs[] 134 ) 135 >> Cases_on `$@ minE` 136 >> `minE (q'',r)` by metis_tac[SELECT_THM] 137 >> qunabbrev_tac `minE` 138 >> fs[minimal_elements_def, rrestrict_def, rel_to_reln_def] 139 >> fs[validAARunFor_def,trans_implies_def] 140 >> metis_tac[SUC_ONE_ADD,ADD_COMM,SUBSET_TRANS,SUBSET_DEF] 141 ) 142 >- (fs[validAARunFor_def] >> metis_tac[SUC_ONE_ADD,ADD_COMM,SUBSET_DEF]) 143 ) 144 >- (simp[validAARunFor_def] >> rpt strip_tac 145 >- (Cases_on `aut` 146 >> fs[validAARunFor_def,reduced_run_def,run_restr_def,run_restr_V_def] 147 >> fs[reduceTransSimpl_def]) 148 >- (`run.V i ��� (reduceTransSimpl aut).states` 149 suffices_by metis_tac[SUBSET_TRANS] 150 >> Cases_on `aut` >> simp[reduceTransSimpl_def] 151 >> fs[validAARunFor_def] 152 ) 153 >- (simp[reduced_run_def, reduced_E_def,run_restr_def,run_restr_E_def] 154 >> fs[reduced_run_def] 155 >> Cases_on `���a' q'. 156 (a',q') ��� aut.trans q ��� 157 trans_implies (a',q') 158 ((@a. (a,run.E (i,q)) ��� aut.trans q ��� at x i ��� a), 159 run.E (i,q))` 160 >- (fs[] >> rw[] 161 >> qabbrev_tac `minE = 162 \t. (t ��� minimal_elements (aut.trans q) 163 (rrestrict (rel_to_reln trans_implies) (aut.trans q))) ��� 164 trans_implies t 165 ((@a. (a,run.E (i,q)) ��� aut.trans q ��� at x i ��� a), 166 run.E (i,q))` 167 >> `?t. minE t` by ( 168 qunabbrev_tac `minE` 169 >> `q ��� run.V i` by fs[SUBSET_DEF] >> fs[] 170 >> HO_MATCH_MP_TAC TRANS_IMPL_MIN_LEMM >> fs[] 171 ) 172 >> fs[run_restr_def] 173 >> Cases_on `$@ minE` >> fs[SND] 174 >> `minE (q''',r)` by metis_tac[SELECT_THM] 175 >> qunabbrev_tac `minE` >> fs[minimal_elements_def,rrestrict_def] 176 >> fs[rel_to_reln_def, trans_implies_def] 177 >> qabbrev_tac `a''' = 178 (@a. (a,run.E (i,q)) ��� aut.trans q ��� at x i ��� a)` 179 >> `(a''', run.E (i,q)) ��� aut.trans q ��� at x i ��� a'''` by ( 180 fs[validAARunFor_def] 181 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 182 >> metis_tac[SELECT_THM,IN_DEF] 183 ) 184 >- (qexists_tac `q'''` >> Cases_on `aut` >> fs[reduceTransSimpl_def] 185 >> fs[removeImplied_def] 186 >> rpt strip_tac 187 >- (CCONTR_TAC >> fs[] >> metis_tac[]) 188 >- metis_tac[SUBSET_TRANS,SUBSET_DEF]) 189 >- metis_tac[] 190 ) 191 >- (simp[] >> fs[run_restr_def] >> simp[] 192 >> Cases_on `aut` >> simp[reduceTransSimpl_def, removeImplied_def] 193 >> `?a. (a, run.E (i,q)) ��� f1 q ��� at x i ��� a` by ( 194 fs[validAARunFor_def] >> metis_tac[SUBSET_DEF] 195 ) 196 >> qabbrev_tac `a' = (@a. (a,run.E (i,q)) ��� f1 q ��� at x i ��� a)` 197 >> `(a', run.E (i,q)) ��� f1 q ��� at x i ��� a'` by metis_tac[SELECT_THM] 198 >> qexists_tac `a'` >> rpt strip_tac >> fs[] 199 >> Cases_on `t'` >> metis_tac[] 200 ) 201 ) 202 >- (simp[SUBSET_DEF, reduced_run_def] >> rpt strip_tac 203 >> fs[run_restr_def, run_restr_E_def] 204 >> rw[run_restr_V_def, DECIDE ``i + 1 = SUC i``] 205 >> metis_tac[MEMBER_NOT_EMPTY] 206 ) 207 >- (Cases_on `i = 0` >> fs[] 208 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 209 >> fs[reduced_run_def, run_restr_def, run_restr_V_def] 210 >> simp[run_restr_E_def] 211 >> metis_tac[] 212 ) 213 ) 214 >- (`���b f. infBranchOf (reduced_run run x aut.trans) b 215 ��� branchFixP b f ��� f ��� (reduceTransSimpl aut).final` suffices_by ( 216 `isVeryWeakAlterA (reduceTransSimpl aut)` by metis_tac[REDUCE_IS_WEAK] 217 >> `FINITE (reduceTransSimpl aut).states` by 218 (Cases_on `aut` >> fs[reduceTransSimpl_def]) 219 >> metis_tac[BRANCH_ACC_LEMM] 220 ) 221 >> `���b f. infBranchOf run b ��� branchFixP b f ��� f ��� aut.final` 222 by metis_tac[BRANCH_ACC_LEMM] 223 >> `!b. infBranchOf (reduced_run run x aut.trans) b 224 ==> infBranchOf run b` by ( 225 rpt strip_tac >> simp[infBranchOf_def] >> rpt strip_tac 226 >- metis_tac[infBranchOf_def,SUBSET_DEF] 227 >- (`!i. b i ��� run.V i` by ( 228 rpt strip_tac >> fs[infBranchOf_def,validAARunFor_def] 229 >> Cases_on `i = 0` >> fs[SUBSET_DEF] 230 >> `?j. i = j + 1` by ( 231 Cases_on `i` >> metis_tac[SUC_ONE_ADD, ADD_COMM] 232 ) 233 >> metis_tac[] 234 ) 235 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 236 >> simp[infBranchOf_def, reduced_run_def] 237 >> simp[run_restr_def, run_restr_E_def] >> rpt strip_tac 238 >> POP_ASSUM mp_tac 239 >> first_x_assum (qspec_then `i` mp_tac) >> rpt strip_tac 240 >> `b (i+1) ��� reduced_E run aut.trans x (i, b i)` 241 by metis_tac[MEMBER_NOT_EMPTY] 242 >> POP_ASSUM mp_tac >> simp[reduced_E_def] >> rpt strip_tac 243 >> Cases_on `���a' q'. 244 (a',q') ��� aut.trans (b i) ��� 245 trans_implies (a',q') 246 ((@a. (a,run.E (i,b i)) ��� aut.trans (b i) 247 ��� at x i ��� a), 248 run.E (i,b i))` 249 >- (fs[] 250 >> qabbrev_tac `minE = \t. 251 t ��� 252 minimal_elements (aut.trans (b i)) 253 (rrestrict (rel_to_reln trans_implies) 254 (aut.trans (b i))) ��� 255 trans_implies t 256 ((@a. (a,run.E (i,b i)) ��� aut.trans (b i) 257 ��� at x i ��� a), 258 run.E (i,b i))` 259 >> `?t. minE t` by ( 260 qunabbrev_tac `minE` >> fs[] 261 >> HO_MATCH_MP_TAC TRANS_IMPL_MIN_LEMM >> fs[] 262 ) 263 >> `minE ($@ minE)` by metis_tac[SELECT_THM] 264 >> Cases_on `$@ minE` 265 >> `r ��� run.E (i,b i)` suffices_by metis_tac[SUBSET_DEF,SND] 266 >> qunabbrev_tac `minE` >> fs[minimal_elements_def] 267 >> fs[rrestrict_def, rel_to_reln_def,trans_implies_def] 268 ) 269 >- metis_tac[] 270 ) 271 ) 272 >> rpt strip_tac >> `f ��� aut.final` suffices_by metis_tac[] 273 >> Cases_on `aut` >> fs[reduceTransSimpl_def] 274 ) 275 >- (Cases_on `aut` >> fs[reduceTransSimpl_def]) 276 ) 277 >- (qexists_tac `run` >> fs[runForAA_def] 278 >> `(validAARunFor aut run x ��� (validAARunFor aut run x ==> acceptingAARun aut run)) 279 ��� word_range x ��� aut.alphabet` suffices_by fs[] 280 >> rpt strip_tac 281 >- (simp[validAARunFor_def] >> rpt strip_tac 282 >- (Cases_on `aut` >> fs[validAARunFor_def, reduceTransSimpl_def]) 283 >- (Cases_on `aut` >> fs[validAARunFor_def, reduceTransSimpl_def]) 284 >- (Cases_on `aut` >> fs[validAARunFor_def, reduceTransSimpl_def] 285 >> metis_tac[removeImplied_def,IN_DIFF]) 286 >- (Cases_on `aut` >> fs[validAARunFor_def, reduceTransSimpl_def]) 287 >- (Cases_on `aut` >> fs[validAARunFor_def, reduceTransSimpl_def]) 288 ) 289 >- (`���b x. infBranchOf run b ��� branchFixP b x ��� x ��� aut.final` 290 suffices_by metis_tac[BRANCH_ACC_LEMM] 291 >> `FINITE (reduceTransSimpl aut).states` by 292 (Cases_on `aut` >> fs[reduceTransSimpl_def]) 293 >> `aut.final = (reduceTransSimpl aut).final` by 294 (Cases_on `aut` >> fs[reduceTransSimpl_def]) 295 >> metis_tac[BRANCH_ACC_LEMM,REDUCE_IS_WEAK] 296 ) 297 >- (Cases_on `aut` >> fs[reduceTransSimpl_def]) 298 ) 299 ); 300 301(* 302 Remove unreachable states 303*) 304 305val removeStatesSimpl_def = Define` 306 removeStatesSimpl (ALTER_A s a t i f) = 307 (ALTER_A 308 (s ��� reachRelFromSet (ALTER_A s a t i f) (BIGUNION i)) 309 a 310 (��q. if q ��� (s ��� reachRelFromSet (ALTER_A s a t i f) (BIGUNION i)) 311 then t q 312 else {}) 313 i 314 (f ��� reachRelFromSet (ALTER_A s a t i f) (BIGUNION i)) 315 )`; 316 317val REACHREL_LEMM = store_thm 318 ("REACHREL_LEMM", 319 ``!x f qs. (x ��� reachRelFromSet (ltl2vwaa f) qs) ��� (qs ��� tempSubForms f) 320 ==> (x ��� tempSubForms f)``, 321 simp[reachRelFromSet_def,reachRel_def] 322 >> `!f x y. (oneStep (ltl2vwaa f))^* x y 323 ==> (!qs. x ��� qs ��� (qs ��� tempSubForms f) 324 ==> y ��� tempSubForms f)` suffices_by metis_tac[] 325 >> gen_tac >> HO_MATCH_MP_TAC RTC_INDUCT >> rpt strip_tac >> fs[] 326 >- metis_tac[SUBSET_DEF] 327 >- (first_x_assum (qspec_then `tempSubForms f` mp_tac) >> simp[] 328 >> rpt strip_tac >> fs[oneStep_def,ltl2vwaa_def,ltl2vwaa_free_alph_def] 329 >> `(x',x) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 330 >> metis_tac[TSF_def,TSF_TRANS_LEMM,transitive_def,IN_DEF] 331 ) 332 ); 333 334val REDUCE_STATE_IS_WEAK = store_thm 335 ("REDUCE_STATE_IS_WEAK", 336 ``!aut. (isVeryWeakAlterA aut ��� isValidAlterA aut) 337 ==> isVeryWeakAlterA (removeStatesSimpl aut)``, 338 simp[isVeryWeakAlterA_def,isVeryWeakWithOrder_def] >> rpt strip_tac 339 >> Cases_on `aut` 340 >> simp[removeStatesSimpl_def,ALTER_A_component_equality] 341 >> qabbrev_tac `reachable = 342 reachRelFromSet (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)` 343 >> qexists_tac `rrestrict ord (f ��� reachable)` 344 >> fs[ALTER_A_component_equality] 345 >> strip_tac 346 >- metis_tac[INTER_SUBSET,partial_order_subset] 347 >- (rpt strip_tac >> `(a,d) ��� f1 s` by metis_tac[] 348 >> simp[rrestrict_def] >> rpt strip_tac 349 >- metis_tac[] 350 >- (fs[isValidAlterA_def] >> metis_tac[SUBSET_DEF]) 351 >- (qunabbrev_tac `reachable` >> fs[reachRelFromSet_def,reachRel_def] 352 >> `���x. (oneStep (ALTER_A f f0 f1 f2 f3))^* x s ��� ���s. x ��� s ��� s ��� f2` 353 by metis_tac[] 354 >> fs[] >> qexists_tac `x'` >> rpt strip_tac 355 >- (`oneStep (ALTER_A f f0 f1 f2 f3) s s'` by ( 356 simp[oneStep_def,ALTER_A_component_equality] 357 >> metis_tac[] 358 ) 359 >> metis_tac[RTC_RTC,RTC_SUBSET] 360 ) 361 >- metis_tac[] 362 ) 363 ) 364 ); 365 366val REDUCE_STATE_IS_VALID = store_thm 367 ("REDUCE_STATE_IS_VALID", 368 ``!aut. isValidAlterA aut ==> isValidAlterA (removeStatesSimpl aut)``, 369 rpt strip_tac >> simp[isValidAlterA_def] >> rpt strip_tac 370 >> fs[isValidAlterA_def,removeStatesSimpl_def] 371 >- (Cases_on `aut` >> simp[removeStatesSimpl_def] >> fs[] 372 >> `!init a. init ��� reachRelFromSet a init` by ( 373 rpt strip_tac >> simp[reachRelFromSet_def,reachRel_def] 374 >> simp[SUBSET_DEF] >> rpt strip_tac 375 >> qexists_tac `x` >> fs[] 376 ) 377 >> simp[SUBSET_DEF,IN_POW] >> rpt strip_tac 378 >- metis_tac[SUBSET_DEF,IN_POW] 379 >- (simp[reachRelFromSet_def,reachRel_def] >> qexists_tac `x'` 380 >> simp[RTC_SUBSET] >> metis_tac[] 381 ) 382 ) 383 >- (Cases_on `aut` >> simp[removeStatesSimpl_def] >> fs[] 384 >> simp[SUBSET_DEF,IN_INTER] >> rpt strip_tac 385 >> metis_tac[SUBSET_DEF] 386 ) 387 >- (Cases_on `aut` >> fs[removeStatesSimpl_def] 388 >> rfs[] 389 >> `d ��� f` by metis_tac[] >> fs[] 390 >> fs[reachRelFromSet_def] >> simp[SUBSET_DEF] >> rpt strip_tac 391 >> fs[] 392 >> rename [���reachRel (ALTER_A f f0 f1 f2 f3) b s���, ���b ��� s1���, ���s1 ��� f2���, 393 ���d ��� f���, ���x ��� d���] 394 >> qexists_tac `b` >> simp[reachRel_def] >> conj_tac 395 >- (`oneStep (ALTER_A f f0 f1 f2 f3) s x` by ( 396 simp[oneStep_def] >> metis_tac[] 397 ) 398 >> metis_tac[RTC_TRANSITIVE,relationTheory.transitive_def, 399 RTC_SUBSET,reachRel_def] 400 ) 401 >- metis_tac[] 402 ) 403 >- (Cases_on `aut` >> fs[removeStatesSimpl_def] 404 >> rfs[] >> metis_tac[]) 405 ); 406 407val REDUCE_STATE_CORRECT = store_thm 408 ("REDUCE_STATE_CORRECT", 409 ``!aut. alterA_lang aut = alterA_lang (removeStatesSimpl aut)``, 410 rw[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 411 >- (qexists_tac `run` >> fs[runForAA_def] >> rpt strip_tac 412 >- (simp[validAARunFor_def] 413 >> Q.HO_MATCH_ABBREV_TAC `B1 ��� B2 ��� B3 ��� B4 ��� B5` 414 >> `B1 ��� B2 ��� (B2 ==> (B3 ��� B4 ��� B5))` suffices_by metis_tac[] 415 >> rpt strip_tac >> qunabbrev_tac `B1` >> qunabbrev_tac `B2` 416 >> qunabbrev_tac `B3` >> qunabbrev_tac `B4` >> qunabbrev_tac `B5` 417 >- (Cases_on `aut` >> fs[validAARunFor_def, removeStatesSimpl_def]) 418 >- ((* Cases_on `aut` >> fs[validAARunFor_def, removeStatesSimpl_def] *) 419 `!n. run.V n ��� reachRelFromSet aut (BIGUNION aut.initial)` 420 by ( 421 Induct_on `n` 422 >- (fs[reachRel_def,reachRelFromSet_def] 423 >> simp[SUBSET_DEF] >> rpt strip_tac 424 >> qexists_tac `x'` >> fs[RTC_REFL] 425 >> fs[validAARunFor_def] >> metis_tac[] 426 ) 427 >- (fs[validAARunFor_def] 428 >> fs[SUBSET_DEF,reachRelFromSet_def] 429 >> rpt strip_tac >> fs[reachRel_def] 430 >> `���q'. x' ��� run.E (n,q') ��� q' ��� run.V n` 431 by metis_tac[DECIDE ``~(SUC n = 0)`` 432 ,DECIDE ``SUC n -1 = n``] 433 >> first_x_assum (qspec_then `q'` mp_tac) >> simp[] 434 >> rpt strip_tac >> qexists_tac `x''` >> simp[] 435 >> `oneStep aut q' x'` 436 suffices_by metis_tac[RTC_CASES2] 437 >> simp[oneStep_def] 438 >> `���a. (a,run.E (n,q')) ��� aut.trans q' ��� at x n ��� a` 439 by metis_tac[] 440 >> qexists_tac `a` >> qexists_tac `run.E (n,q')` 441 >> simp[] >> metis_tac[SUBSET_DEF] 442 ) 443 ) 444 >> Cases_on `aut` 445 >> fs[validAARunFor_def,removeStatesSimpl_def] 446 ) 447 >- (Cases_on `aut` >> fs[validAARunFor_def, removeStatesSimpl_def] 448 >> rpt strip_tac 449 >> `q ��� f 450 ��� q ��� reachRelFromSet (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)` 451 by metis_tac[SUBSET_DEF] >> fs[] 452 ) 453 >- (Cases_on `aut` >> fs[validAARunFor_def, removeStatesSimpl_def]) 454 >- (Cases_on `aut` >> fs[validAARunFor_def, removeStatesSimpl_def]) 455 ) 456 >- (Cases_on `aut` >> fs[acceptingAARun_def, removeStatesSimpl_def] 457 >> rpt strip_tac 458 >> Q.HO_MATCH_ABBREV_TAC `FINITE {i | b i ��� A ��� b i ��� B }` 459 >> `{i | b i ��� A ��� b i ��� B } ��� {i | b i ��� A }` by ( 460 simp[SUBSET_DEF] >> rpt strip_tac >> metis_tac[] 461 ) 462 >> metis_tac[PSUBSET_DEF,PSUBSET_FINITE] 463 ) 464 >- (Cases_on `aut` >> fs[removeStatesSimpl_def]) 465 ) 466 >- (qexists_tac `run` >> fs[runForAA_def] >> rpt strip_tac 467 >- (simp[validAARunFor_def] >> rpt strip_tac 468 >> Cases_on `aut` 469 >> fs[validAARunFor_def, removeStatesSimpl_def] 470 >> metis_tac[SUBSET_DEF]) 471 >- (Cases_on `aut` >> fs[acceptingAARun_def,removeStatesSimpl_def] 472 >> rpt strip_tac 473 >> `���i. b i ��� run.V i` by metis_tac[BRANCH_V_LEMM] 474 >> fs[validAARunFor_def] >> first_x_assum (qspec_then `b` mp_tac) 475 >> simp[] >> rpt strip_tac 476 >> `{i | b i ��� f3} 477 ��� {i | b i ��� f3 ��� 478 b i ��� reachRelFromSet 479 (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)}` by ( 480 simp[SUBSET_DEF] >> rpt strip_tac 481 >> metis_tac[SUBSET_DEF] 482 ) 483 >> metis_tac[PSUBSET_DEF,PSUBSET_FINITE] 484 ) 485 >- (Cases_on `aut` >> fs[removeStatesSimpl_def]) 486 ) 487 ); 488 489(* 490 Merge equivalent states 491*) 492 493val equivalentStates_def = Define` 494 equivalentStates final trans s s' = 495 (trans s = trans s') ��� (s ��� final = s' ��� final)`; 496 497val EQUIV_STATES_SYMM = store_thm 498 ("EQUIV_STATES_SYMM", 499 ``!f t x y. equivalentStates f t x y = equivalentStates f t y x``, 500 metis_tac[equivalentStates_def] 501 ); 502 503val EQUIV_STATES_REFL = store_thm 504 ("EQUIV_STATES_SYMM", 505 ``!f t x. equivalentStates f t x x``, 506 metis_tac[equivalentStates_def] 507 ); 508 509val replaceSingleTrans_def = Define` 510 replaceSingleTrans s s' (a,e) = 511 if s ��� e 512 then (a, (e DIFF {s}) ��� {s'}) 513 else (a,e)`; 514 515val replaceState_def = Define` 516 replaceState s s' qs = 517 if s ��� qs 518 then qs DIFF {s} ��� {s'} 519 else qs`; 520 521val REPL_STATE_LEMM = store_thm 522 ("REPL_STATE_LEMM", 523 ``!x s d1 d2. d1 ��� d2 ==> replaceState x s d1 ��� replaceState x s d2``, 524 rpt strip_tac >> fs[replaceState_def] >> Cases_on `x ��� d1` 525 >> Cases_on `x ��� d2` >> fs[SUBSET_DEF, IN_DIFF, IN_UNION] >> rpt strip_tac 526 >> metis_tac[] 527 ); 528 529val replaceBy_def = Define` 530 replaceBy trans s s' q = IMAGE (replaceSingleTrans s s') (trans q)`; 531 532(* val REPLACE_TRANS_REACHABLE_LEMM = store_thm *) 533(* ("REPLACE_TRANS_LEMM", *) 534(* ``!f trans a b s. equivalentStates f trans a b ��� ~(a ��� s) *) 535(* ==> ((reachable (replaceBy trans a b) s) = *) 536(* replaceState a b (reachable trans s))`` *) 537(* rpt strip_tac *) 538(* >> `!n. (replaceState a b (nStepReachable trans s n) *) 539(* = nStepReachable (replaceBy trans a b) s n)` by ( *) 540(* Induct_on `n` >> rw[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac *) 541(* >> fs[nStepReachable_def,replaceState_def] *) 542(* >- metis_tac[] *) 543(* >- (Cases_on `���a' qs s'. *) 544(* (a',qs) ��� trans s' ��� s' ��� nStepReachable trans s n ��� a ��� qs` *) 545(* >> fs[] >> metis_tac[] *) 546(* >- (qexists_tac `a'` >> qexists_tac `qs` *) 547(* >> qexists_tac `b` >> fs[] >> fs[replaceBy_def,EXISTS_PROD] *) 548 549(* >> fs[replaceSingleTrans_def] > *) 550(* ) *) 551(* `s' ��� nStepReachable (replaceBy trans a b) s n` by metis_tac[] *) 552(* >> qexists_tac `a'` >> qexists_tac `qs` >> qexists_tac `s'` *) 553(* >> simp[replaceBy_def] *) 554(* >> fs[EXISTS_PROD] >> qexists_tac `a'` >> qexists_tac `qs` *) 555(* >> simp[replaceSingleTrans_def] >> *) 556(* ) *) 557 558(* ) *) 559 560(* rw[SET_EQ_SUBSET] >> rpt strip_tac >> fs[reachable_def, replaceBy_def] *) 561(* >> fs[equivalentStates_def,SUBSET_DEF] >> rpt strip_tac *) 562(* >> qexists_tac `n` *) 563(* >- (Induct_on `n`) *) 564 565(* ) *) 566 567 568val mergeState_def = Define` 569 mergeState x (ALTER_A states a trans i f) = 570 if ?s. s ��� states ��� ~(s = x) ��� equivalentStates f trans s x 571 then 572 let s' = $@ (\s. s ��� states ��� ~(s = x) 573 ��� equivalentStates f trans s x) 574 in ALTER_A 575 (states DIFF {x}) 576 a 577 (replaceBy trans x s') 578 (IMAGE (replaceState x s') i) 579 (replaceState x s' f) 580 else (ALTER_A states a trans i f)`; 581 582val mergeStatesSimpl = Define` 583 mergeStatesSimpl aut = ITSET mergeState aut.states aut`; 584 585(* val MERGE_STATE_COMMUTES = store_thm *) 586(* ("MERGE_STATE_COMMUTES", *) 587(* ``!f x y z. mergeState f x (mergeStates f y z) = *) 588(* mergeState f y (mergeState f x z)``, *) 589 590 591(* val ITSET_IND_SPEC_MERGE = store_thm *) 592(* ("ITSET_IND_SPEC_MERGE", *) 593(* ``���P. *) 594(* (���s b. *) 595(* (FINITE s ��� s ��� ��� ��� P (REST s) ((mergeState final) (CHOICE s) b)) ��� P s b) ��� *) 596(* ���v v1. P v v1``, *) 597(* metis_tac[ITSET_IND] *) 598(* ); *) 599 600(* val EQUIV_EXISTS_IN_MERGESET = store_thm *) 601(* ("EQUIV_EXISTS_IN_MERGESET", *) 602(* ``!final states trans x. FINITE states ��� (x ��� states) *) 603(* ==> ?x'. (x' ��� FST (mergeStates final states trans)) *) 604(* ��� (equivalentStates final trans x x')``, *) 605(* simp[mergeStates_def] >> gen_tac *) 606(* >> `!v v1 trans. FINITE v ==> *) 607(* !x. x ��� v ==> *) 608(* ?x'. x' ��� FST (ITSET (mergeState final) v v1) ��� *) 609(* equivalentStates final trans x x'` by ( *) 610(* HO_MATCH_MP_TAC ITSET_IND_SPEC_MERGE >> rpt strip_tac *) 611(* >> `���trans x. *) 612(* x ��� REST v ��� *) 613(* ���x'. x' ��� FST *) 614(* (ITSET (mergeState final) (REST v) *) 615(* (mergeState final (CHOICE v) v1)) ��� *) 616(* equivalentStates final trans x x'` *) 617(* by metis_tac[MEMBER_NOT_EMPTY] *) 618(* >> Cases_on `x ��� REST v` *) 619(* >- metis_tac[ITSET_THM,MEMBER_NOT_EMPTY] *) 620(* >- (rw[ITSET_THM] >> fs[MEMBER_NOT_EMPTY] *) 621(* >- (Cases_on `v1` >> simp[mergeState_def] *) 622(* >> Cases_on `���s. *) 623(* s ��� q ��� (s ��� CHOICE v) *) 624(* ��� equivalentStates final r s (CHOICE v)` *) 625(* >- (rw[] >> metis_tac[]) *) 626(* ) *) 627 628(* ) *) 629(* >> HO_MATCH_MP_TAC ITSET_IND_SPEC_MERGE >> rpt strip_tac *) 630(* >> Cases_on `(states = {})` *) 631(* >- (simp[ITSET_THM] >> metis_tac[MEMBER_NOT_EMPTY]) *) 632(* >- (fs[] *) 633(* >> *) 634(* >> *) 635 636(* ) *) 637 638(* `!states. FINITE states ==> *) 639(* !final trans x. (x ��� states) *) 640(* ==> ?x'. (x' ��� FST (mergeStates final states trans)) *) 641(* ��� (equivalentStates final trans x x')` suffices_by metis_tac[] *) 642(* >> Induct_on `states` >> rpt strip_tac >> fs[mergeStates_def] *) 643(* >- () *) 644 645 646(* ) *) 647 648val replace_run_def = Define` 649 replace_run old_run x_old x_new = 650 ALTERA_RUN 651 (replaceState x_old x_new o old_run.V) 652 (��(i,q). if (q = x_new) ��� ~(x_new ��� old_run.V i) 653 then replaceState x_old x_new (old_run.E (i,x_old)) 654 else replaceState x_old x_new (old_run.E (i,q)))`; 655 656 657 658(* val replace_ord_def = Define` *) 659(* replace_ord old_ord x x' = *) 660(* { (s,s') | ~(s = x) ��� ~(s' = x) ��� (s,s') ��� old_ord } *) 661(* ��� { (x',s) | ~(s = x) ��� (x,s) ��� old_ord } *) 662(* ��� { (s,x') | ~(s = x) ��� (s,x) ��� old_ord } *) 663(* ��� if (x,x) ��� old_ord then { (x',x') } else {}`; *) 664 665 666(* val REPL_ORD_TRANS_LEMM = store_thm *) 667(* ("REPL_ORD_TRANS_LEMM", *) 668(* ``!ord a b. transitive ord ==> transitive (replace_ord ord a b)``, *) 669(* fs[transitive_def] >> rpt strip_tac *) 670(* >> Cases_on `(x = a) \/ (y = a) \/ (z = a)` *) 671(* >- (fs[replace_ord_def] >> rw[] >> fs[] *) 672(* >> metis_tac[MEMBER_NOT_EMPTY,IN_SING]) *) 673(* >- (fs[replace_ord_def] *) 674(* >- metis_tac[] *) 675(* >- dsimp[] *) 676 677 678(* ) *) 679(* ) *) 680 681 682(*change to new reach relation*) 683 684(* val EQUIV_REACH_LEMM = store_thm *) 685(* ("EQUIV_REACH_LEMM", *) 686(* ``!aut x y. x ��� aut.states ��� y ��� aut.states *) 687(* ��� equivalentStates aut.final aut.trans x y ==> *) 688(* (!v. ~(x = v) ��� ~(y = v) *) 689(* ==> ((reachRel aut) v x = (reachRel aut) v y))``, *) 690(* `!aut x y. x ��� aut.states ��� y ��� aut.states *) 691(* ��� equivalentStates aut.final aut.trans x y ==> *) 692(* (!v. ~(x = v) ��� ~(y = v) *) 693(* ==> ((reachRel aut) v x ==> (reachRel aut) v y))` *) 694(* suffices_by metis_tac[EQUIV_STATES_SYMM] *) 695(* >> gen_tac >> fs[reachRel_def] *) 696(* >> simp[RTC_eq_NRC] *) 697(* >> `���n x y. *) 698(* x ��� aut.states ��� y ��� aut.states *) 699(* ��� equivalentStates aut.final aut.trans x y ��� *) 700(* ���v. *) 701(* x ��� v ��� y ��� v ��� *) 702(* NRC (oneStep aut) n v x ��� NRC (oneStep aut) n v y` suffices_by metis_tac[] *) 703(* >> Induct_on `n` *) 704(* >- (rpt strip_tac >> fs[NRC]) *) 705(* >- (rpt strip_tac >> fs[NRC_SUC_RECURSE_LEFT] *) 706(* >> `oneStep aut z y` by ( *) 707(* fs[oneStep_def,equivalentStates_def] *) 708(* >> qexists_tac `a` >> qexists_tac `qs` *) 709(* >> fs[] >> metis_tac[] *) 710(* ) *) 711(* >> metis_tac[] *) 712(* ) *) 713(* ); *) 714 715(* val MERGE_REACH_LEMM = store_thm *) 716(* ("MERGE_REACH_LEMM", *) 717(* ``!aut x y. isValidAlterA aut ��� equivalentStates aut.final aut.trans y x *) 718(* ��� x ��� aut.states ��� y ��� aut.states ��� ~(x = y) *) 719(* ==> let mergedAut = mergeState x aut *) 720(* in !q1 q2. (reachRel mergedAut) q1 q2 *) 721(* ==> *) 722(* ((q1 = @s. s ��� aut.states ��� ~(s = x) *) 723(* ��� equivalentStates aut.final aut.trans s x) *) 724(* \/ (reachRel aut) q1 q2)``, *) 725(* rpt strip_tac >> fs[reachRel_def] *) 726(* >> HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 >> rpt strip_tac *) 727(* >> fs[rel_to_reln_def] *) 728(* >> qabbrev_tac `s_new = @s. *) 729(* s ��� aut.states ��� s ��� x ��� equivalentStates aut.final aut.trans s x` *) 730(* >> Cases_on `q1 = s_new` >> fs[] *) 731(* >> `?q3. (oneStep aut) q3 q2' ��� equivalentStates aut.final aut.trans q2 q3` *) 732(* suffices_by ( *) 733(* rpt strip_tac >> Cases_on `q1 = q2` >> Cases_on `q1 = q3` *) 734(* >> rw[] *) 735(* >- (`(oneStep aut) q1 q2'` suffices_by metis_tac[RTC_SUBSET] *) 736(* >> fs[] >> Cases_on `aut` >> fs[mergeState_def,oneStep_def] >> fs[] *) 737(* >> rpt (POP_ASSUM mp_tac) >> rw[] >> fs[] >> rw[] *) 738(* >- (fs[replaceBy_def] >> Cases_on `x'` >> fs[replaceSingleTrans_def] *) 739(* >> rw[] >> Cases_on `x ��� r` >> fs[] >> rw[] *) 740(* >- (qexists_tac `a` >> qexists_tac `r` >> fs[]) *) 741(* >- metis_tac[] *) 742(* ) *) 743(* >- metis_tac[] *) 744(* ) *) 745(* >- (`q2 ��� aut.states ��� q3 ��� aut.states` by ( *) 746(* fs[oneStep_def,isValidAlterA_def] >> Cases_on `aut` *) 747(* >> fs[mergeState_def] >> rw[] *) 748(* >> Cases_on `���s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x` *) 749(* >> fs[replaceBy_def] *) 750(* >- (Cases_on `x'` >> fs[replaceSingleTrans_def] *) 751(* >> Cases_on `x ��� r` >> fs[] >> rw[IN_DIFF, IN_UNION] *) 752(* >> `s_new ��� f` by metis_tac[] *) 753(* >> metis_tac[IN_DIFF,IN_UNION,IN_SING,SUBSET_DEF] *) 754(* ) *) 755(* >- metis_tac[IN_DIFF,IN_UNION,IN_SING,SUBSET_DEF] *) 756(* >- metis_tac[IN_DIFF,IN_UNION,IN_SING,SUBSET_DEF] *) 757(* >- metis_tac[IN_DIFF,IN_UNION,IN_SING,SUBSET_DEF] *) 758(* ) *) 759(* >> `(oneStep aut)^* q1 q3` by metis_tac[EQUIV_REACH_LEMM,reachRel_def] *) 760(* >> metis_tac[RTC_CASES_RTC_TWICE,RTC_SUBSET] *) 761(* ) *) 762(* ) *) 763(* >> fs[] >> Cases_on `aut` >> fs[mergeState_def,oneStep_def] >> fs[] *) 764(* >> rpt (POP_ASSUM mp_tac) >> rw[] >> fs[] *) 765(* >- (fs[replaceBy_def] >> Cases_on `x'` >> fs[replaceSingleTrans_def] *) 766(* >> Cases_on `x ��� r` >> fs[] *) 767(* >> rw[] >> fs[IN_UNION] >> metis_tac[EQUIV_STATES_REFL] *) 768(* ) *) 769(* >- metis_tac[] *) 770(* ); *) 771 772(* val MERGE_REACH_LEMM2 = store_thm *) 773(* ("MERGE_REACH_LEMM2", *) 774(* ``!aut v x y. isValidAlterA aut ��� equivalentStates aut.final aut.trans x y *) 775(* ��� x ��� aut.states ��� y ��� aut.states ��� ~(y = x) *) 776(* ==> let mergedAut = mergeState x aut *) 777(* and s_new = @s. s ��� aut.states ��� s ��� x ��� *) 778(* equivalentStates aut.final aut.trans s x *) 779(* in !v. reachRel mergedAut s_new v *) 780(* ==> reachRel aut s_new v \/ reachRel aut x v``, *) 781(* rpt strip_tac >> fs[] *) 782(* >> qabbrev_tac `s_new = @s. *) 783(* s ��� aut.states ��� s ��� x ��� *) 784(* equivalentStates aut.final aut.trans s x` *) 785(* >> fs[reachRel_def] >> gen_tac *) 786(* >> `!m n. (oneStep (mergeState x aut))^* m n ��� (m = s_new) *) 787(* ==> (oneStep aut)^* m n ��� (oneStep aut)^* x n` *) 788(* suffices_by metis_tac[] *) 789(* >> HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 >> rpt strip_tac >> rw[] *) 790(* >> (Cases_on `n = m` *) 791(* >- (`(oneStep aut) m n' ��� (oneStep aut) x n'` *) 792(* suffices_by metis_tac[RTC_SUBSET] *) 793(* >> fs[] >> Cases_on `aut` >> fs[mergeState_def,oneStep_def] *) 794(* >> fs[] >> rpt (POP_ASSUM mp_tac) >> rw[] >> fs[] *) 795(* >- (fs[replaceBy_def] >> Cases_on `x'` >> fs[replaceSingleTrans_def] *) 796(* >> Cases_on `x ��� r` >> fs[] *) 797(* >> rw[] >> fs[IN_UNION] >> metis_tac[] *) 798(* ) *) 799(* >- metis_tac[] *) 800(* ) *) 801(* >- (`reachRel aut n n'` by ( *) 802(* fs[reachRel_def] *) 803(* >> `reachRel (mergeState x aut) n n'` by *) 804(* (fs[reachRel_def] >> metis_tac[RTC_SUBSET]) *) 805(* >> qunabbrev_tac `m` *) 806(* >> `reachRel aut n n'` suffices_by metis_tac[reachRel_def] *) 807(* >> `(let mergedAut = mergeState x aut *) 808(* in *) 809(* ���q1 q2. *) 810(* reachRel mergedAut q1 q2 ��� *) 811(* (q1 = *) 812(* @s. *) 813(* s ��� aut.states ��� s ��� x ��� *) 814(* equivalentStates aut.final aut.trans s x) ��� *) 815(* reachRel aut q1 q2)` *) 816(* by (HO_MATCH_MP_TAC MERGE_REACH_LEMM *) 817(* >> metis_tac[EQUIV_STATES_SYMM]) *) 818(* >> fs[] >> metis_tac[] *) 819(* ) *) 820(* >> fs[reachRel_def] >> metis_tac[RTC_CASES_RTC_TWICE] *) 821(* ) *) 822(* ) *) 823(* ); *) 824 825(* val MERGE_PO_LEMM = store_thm *) 826(* ("MERGE_PO_LEMM", *) 827(* ``!aut x y. isValidAlterA aut ��� equivalentStates aut.final aut.trans x y *) 828(* ��� x ��� aut.states ��� y ��� aut.states ��� ~(y = x) *) 829(* ��� partial_order (rrestrict (rel_to_reln (reachRel aut)) aut.states) *) 830(* aut.states *) 831(* ==> (let mergedAut = mergeState x aut *) 832(* in partial_order (rrestrict (rel_to_reln (reachRel mergedAut)) *) 833(* mergedAut.states) *) 834(* mergedAut.states)``, *) 835(* rpt strip_tac >> fs[] *) 836(* >> simp[partial_order_def,reachableRel_def,mergeState_def] >> rpt strip_tac *) 837(* >- (fs[domain_def,SUBSET_DEF,rel_to_reln_def,rrestrict_def] >> rpt strip_tac) *) 838(* >- (fs[range_def,SUBSET_DEF,rel_to_reln_def,rrestrict_def] >> rpt strip_tac) *) 839(* >- (fs[reachRel_def,rrestrict_def,transitive_def] *) 840(* >> rpt strip_tac >> fs[rel_to_reln_def] *) 841(* >> metis_tac[RTC_TRANSITIVE]) *) 842(* >- (fs[reflexive_def, rrestrict_def, rel_to_reln_def, reachRel_def]) *) 843(* >- (fs[antisym_def,rel_to_reln_def,rrestrict_def] >> rpt strip_tac *) 844(* >> qabbrev_tac `s_new = *) 845(* @s. s ��� aut.states ��� s ��� x ��� *) 846(* equivalentStates aut.final aut.trans s x` *) 847(* >> Cases_on `x' = s_new` >> Cases_on `y' = s_new` >> fs[] *) 848(* >- (`reachRel aut y' s_new` by ( *) 849(* `let mergedAut = mergeState x aut *) 850(* in *) 851(* ���q1 q2. *) 852(* reachRel mergedAut q1 q2 ��� *) 853(* (q1 = *) 854(* @s. *) 855(* s ��� aut.states ��� s ��� x ��� *) 856(* equivalentStates aut.final aut.trans s x) ��� *) 857(* reachRel aut q1 q2` *) 858(* by (HO_MATCH_MP_TAC MERGE_REACH_LEMM *) 859(* >> metis_tac[EQUIV_STATES_SYMM]) *) 860(* >> fs[] >> metis_tac[] *) 861(* ) *) 862(* >> `s_new ��� aut.states` by metis_tac[EQUIV_STATES_SYMM] *) 863(* >> `y' ��� aut.states` by ( *) 864(* Cases_on `aut` >> fs[mergeState_def] *) 865(* >> `y' ��� *) 866(* (ALTER_A (f DIFF {x}) (IMAGE (replaceState x s_new) f0) *) 867(* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *) 868(* by metis_tac[EQUIV_STATES_SYMM] *) 869(* >> fs[] *) 870(* ) *) 871(* >> `reachRel aut s_new y' \/ reachRel aut x y'` by ( *) 872(* `let *) 873(* mergedAut = mergeState x aut and *) 874(* s_new = *) 875(* @s. *) 876(* s ��� aut.states ��� s ��� x ��� *) 877(* equivalentStates aut.final aut.trans s x *) 878(* in *) 879(* ���v. *) 880(* reachRel mergedAut s_new v ��� *) 881(* reachRel aut s_new v ��� reachRel aut x v` *) 882(* by (HO_MATCH_MP_TAC MERGE_REACH_LEMM2 >> metis_tac[]) *) 883(* >> fs[] >> metis_tac[]) *) 884(* >- (fs[partial_order_def, antisym_def] >> metis_tac[]) *) 885(* >- (Cases_on `x = y'` *) 886(* >- (rw[] >> Cases_on `aut` >> fs[mergeState_def] *) 887(* >> `x ��� *) 888(* (ALTER_A (f DIFF {x}) (IMAGE (replaceState x s_new) f0) *) 889(* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *) 890(* by metis_tac[EQUIV_STATES_SYMM] *) 891(* >> fs[]) *) 892(* >- (rw[] >> `reachRel aut y' x ��� reachRel aut y' s_new` by ( *) 893(* metis_tac[EQUIV_REACH_LEMM,EQUIV_STATES_SYMM] *) 894(* ) *) 895(* >> fs[partial_order_def,antisym_def] *) 896(* >> metis_tac[] *) 897(* ) *) 898(* ) *) 899(* ) *) 900(* >- (`reachRel aut x' s_new` by ( *) 901(* `let mergedAut = mergeState x aut *) 902(* in *) 903(* ���q1 q2. *) 904(* reachRel mergedAut q1 q2 ��� *) 905(* (q1 = *) 906(* @s. *) 907(* s ��� aut.states ��� s ��� x ��� *) 908(* equivalentStates aut.final aut.trans s x) ��� *) 909(* reachRel aut q1 q2` *) 910(* by (HO_MATCH_MP_TAC MERGE_REACH_LEMM *) 911(* >> metis_tac[EQUIV_STATES_SYMM]) *) 912(* >> fs[] >> metis_tac[] *) 913(* ) *) 914(* >> `s_new ��� aut.states` by metis_tac[EQUIV_STATES_SYMM] *) 915(* >> `x' ��� aut.states` by ( *) 916(* Cases_on `aut` >> fs[mergeState_def] *) 917(* >> `x' ��� *) 918(* (ALTER_A (f DIFF {x}) (IMAGE (replaceState x s_new) f0) *) 919(* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *) 920(* by metis_tac[EQUIV_STATES_SYMM] *) 921(* >> fs[] *) 922(* ) *) 923(* >> `reachRel aut s_new x' \/ reachRel aut x x'` by ( *) 924(* `let *) 925(* mergedAut = mergeState x aut and *) 926(* s_new = *) 927(* @s. *) 928(* s ��� aut.states ��� s ��� x ��� *) 929(* equivalentStates aut.final aut.trans s x *) 930(* in *) 931(* ���v. *) 932(* reachRel mergedAut s_new v ��� *) 933(* reachRel aut s_new v ��� reachRel aut x v` *) 934(* by (HO_MATCH_MP_TAC MERGE_REACH_LEMM2 >> metis_tac[]) *) 935(* >> fs[] >> metis_tac[]) *) 936(* >- (fs[partial_order_def, antisym_def] >> metis_tac[]) *) 937(* >- (Cases_on `x = x'` *) 938(* >- (rw[] >> Cases_on `aut` >> fs[mergeState_def] *) 939(* >> `x ��� *) 940(* (ALTER_A (f DIFF {x}) (IMAGE (replaceState x s_new) f0) *) 941(* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *) 942(* by metis_tac[EQUIV_STATES_SYMM] *) 943(* >> fs[]) *) 944(* >- (rw[] >> `reachRel aut x' x ��� reachRel aut x' s_new` by ( *) 945(* metis_tac[EQUIV_REACH_LEMM,EQUIV_STATES_SYMM] *) 946(* ) *) 947(* >> fs[partial_order_def,antisym_def] *) 948(* >> metis_tac[] *) 949(* ) *) 950(* ) *) 951(* ) *) 952(* >- (`reachRel aut x' y' *) 953(* ��� reachRel aut y' x'` by ( *) 954(* `let mergedAut = mergeState x aut *) 955(* in *) 956(* ���q1 q2. *) 957(* reachRel mergedAut q1 q2 ��� *) 958(* (q1 = *) 959(* @s. *) 960(* s ��� aut.states ��� s ��� x ��� *) 961(* equivalentStates aut.final aut.trans s x) ��� *) 962(* reachRel aut q1 q2` by *) 963(* (HO_MATCH_MP_TAC MERGE_REACH_LEMM >> metis_tac[EQUIV_STATES_SYMM]) *) 964(* >> fs[] >> metis_tac[]) *) 965(* >> fs[partial_order_def,antisym_def] *) 966(* >> `x' ��� aut.states ��� y' ��� aut.states` by ( *) 967(* Cases_on `aut` >> fs[mergeState_def] *) 968(* >> strip_tac *) 969(* >- (`x' ��� *) 970(* (ALTER_A (f DIFF {x}) (IMAGE (replaceState x s_new) f0) *) 971(* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *) 972(* by metis_tac[EQUIV_STATES_SYMM] *) 973(* >> fs[]) *) 974(* >- (`y' ��� *) 975(* (ALTER_A (f DIFF {x}) (IMAGE (replaceState x s_new) f0) *) 976(* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *) 977(* by metis_tac[EQUIV_STATES_SYMM] >> fs[]) *) 978(* ) *) 979(* >> metis_tac[] *) 980(* ) *) 981(* ) *) 982(* ); *) 983 984(* val WAA_REACH_IS_PO__ = store_thm *) 985(* ("WAA_REACH_IS_PO__", *) 986(* ``!aut. isWeakAlterA aut ��� isValidAlterA aut *) 987(* ==> isWeakWithOrder aut *) 988(* (rrestrict (rel_to_reln (reachRel aut)) aut.states)``, *) 989(* fs[isWeakAlterA_def] >> simp[isWeakWithOrder_def] >> rpt strip_tac *) 990(* >- (fs[partial_order_def,rrestrict_def,rel_to_reln_def] >> rpt strip_tac *) 991(* >- (simp[domain_def,SUBSET_DEF] >> rpt strip_tac) *) 992(* >- (simp[range_def,SUBSET_DEF] >> rpt strip_tac) *) 993(* >- (simp[transitive_def,reachRel_def] >> rpt strip_tac *) 994(* >> metis_tac[RTC_TRANSITIVE]) *) 995(* >- fs[reflexive_def,reachRel_def] *) 996(* >- (fs[antisym_def] *) 997(* >> `!m n. m ��� aut.states ��� reachRel aut m n ==> n ��� aut.states` by ( *) 998(* fs[reachRel_def] >> HO_MATCH_MP_TAC RTC_lifts_invariants *) 999(* >> rpt strip_tac >> fs[oneStep_def] *) 1000(* ) *) 1001(* >> `!m n. reachRel aut m n ==> *) 1002(* m ��� aut.states ==> (m,n) ��� ord` by ( *) 1003(* fs[reachRel_def] >> HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 *) 1004(* >> strip_tac *) 1005(* >- (rpt strip_tac >> fs[reflexive_def]) *) 1006(* >- (rpt strip_tac >> fs[] >> fs[oneStep_def] *) 1007(* >> fs[transitive_def] >> metis_tac[]) *) 1008(* ) *) 1009(* >> rpt strip_tac *) 1010(* >> metis_tac[] *) 1011(* ) *) 1012(* ) *) 1013(* >- (simp[rrestrict_def,rel_to_reln_def,reachRel_def] *) 1014(* >> fs[isValidAlterA_def] >> strip_tac *) 1015(* >- (`(oneStep aut) s' s` suffices_by metis_tac[RTC_SUBSET] *) 1016(* >> simp[oneStep_def] >> metis_tac[] *) 1017(* ) *) 1018(* >- (fs[isValidAlterA_def] >> metis_tac[SUBSET_DEF]) *) 1019(* ) *) 1020(* ); *) 1021 1022(* val MERGE_IS_VALID = store_thm *) 1023(* ("MERGE_IS_VALID", *) 1024(* ``!aut x. isValidAlterA aut ��� x ��� aut.states *) 1025(* ==> isValidAlterA (mergeState x aut)``, *) 1026(* rpt strip_tac *) 1027(* >> Cases_on `���s. s ��� aut.states ��� s ��� x *) 1028(* ��� equivalentStates aut.final aut.trans s x` *) 1029(* >- (Cases_on `aut` >> simp[mergeState_def] >> rpt strip_tac *) 1030(* >> qabbrev_tac `fullAuto = *) 1031(* ALTER_A (f DIFF {x}) *) 1032(* (IMAGE *) 1033(* (replaceState x *) 1034(* (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x)) f0) *) 1035(* (replaceState x (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x) *) 1036(* f1) f2 *) 1037(* (replaceBy f3 x (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x))` *) 1038(* >> fs[] >> `isValidAlterA fullAuto` suffices_by metis_tac[] *) 1039(* >> simp[isValidAlterA_def] >> rpt strip_tac *) 1040(* >- (qunabbrev_tac `fullAuto` >> fs[IMAGE_DEF,replaceState_def] *) 1041(* >> fs[SUBSET_DEF] >> rpt strip_tac *) 1042(* >> `f0 ��� POW f` by fs[isValidAlterA_def] *) 1043(* >> Cases_on `x ��� x''` >> fs[] *) 1044(* >- (rw[] >> fs[DIFF_DEF,UNION_DEF,IN_POW] >> rpt strip_tac *) 1045(* >- (fs[SUBSET_DEF] >> rpt strip_tac *) 1046(* >> metis_tac[IN_POW,SUBSET_DEF]) *) 1047(* >- metis_tac[] *) 1048(* >- metis_tac[] *) 1049(* ) *) 1050(* >- (`f0 ��� POW f` by fs[isValidAlterA_def] *) 1051(* >> fs[IN_POW,IN_DIFF,SUBSET_DEF] >> rpt strip_tac *) 1052(* >> metis_tac[] *) 1053(* ) *) 1054(* ) *) 1055(* >- (qunabbrev_tac `fullAuto` >> fs[IMAGE_DEF,replaceState_def] *) 1056(* >> fs[SUBSET_DEF] >> rpt strip_tac *) 1057(* >> `f1 ��� f` by fs[isValidAlterA_def] *) 1058(* >> Cases_on `x ��� f1` >> fs[] *) 1059(* >> metis_tac[SUBSET_DEF] *) 1060(* ) *) 1061(* >- (qunabbrev_tac `fullAuto` >> fs[IMAGE_DEF,replaceState_def] *) 1062(* >> fs[SUBSET_DEF,replaceBy_def] >> rpt strip_tac *) 1063(* >> Cases_on `x'` >> fs[replaceSingleTrans_def] *) 1064(* >> Cases_on `x ��� r` >> fs[] >> rw[] *) 1065(* >- (`r ��� f` by (fs[isValidAlterA_def] >> metis_tac[]) *) 1066(* >> Cases_on `x'' = x` *) 1067(* >> fs[IN_DIFF,IN_UNION] *) 1068(* >> metis_tac[SUBSET_DEF] *) 1069(* ) *) 1070(* >- (`d ��� f` by (fs[isValidAlterA_def] >> metis_tac[]) *) 1071(* >> metis_tac[SUBSET_DEF] *) 1072(* ) *) 1073(* >- (fs[IN_DIFF,IN_UNION] >> metis_tac[]) *) 1074(* >- metis_tac[] *) 1075(* ) *) 1076(* >- (qunabbrev_tac `fullAuto` >> fs[isValidAlterA_def,replaceBy_def] *) 1077(* >> Cases_on `x'` >> fs[replaceSingleTrans_def] *) 1078(* >> `a = q` by (Cases_on `x ��� r` >> fs[]) *) 1079(* >> metis_tac[] *) 1080(* ) *) 1081(* ) *) 1082(* >- (`mergeState x aut = aut` by ( *) 1083(* Cases_on `aut` >> simp[mergeState_def,COND_EXPAND] *) 1084(* >> fs[COND_EXPAND] >> metis_tac[] *) 1085(* ) >> metis_tac[] *) 1086(* ) *) 1087(* ); *) 1088 1089(* val MERGE_IS_WEAK = store_thm *) 1090(* ("MERGE_IS_WEAK", *) 1091(* ``!aut x. isWeakAlterA aut ��� x ��� aut.states ��� isValidAlterA aut *) 1092(* ��� isValidAlterA (mergeState x aut) *) 1093(* ==> isWeakAlterA (mergeState x aut)``, *) 1094(* rpt strip_tac *) 1095(* >> `isWeakWithOrder aut (rrestrict (rel_to_reln (reachRel aut)) aut.states)` *) 1096(* by metis_tac[WAA_REACH_IS_PO__] *) 1097(* >> fs[isWeakWithOrder_def] *) 1098(* >> qabbrev_tac *) 1099(* `s_new = @s. s ��� aut.states ��� s ��� x *) 1100(* ��� equivalentStates aut.final aut.trans s x` *) 1101(* >> Cases_on `���s. s ��� aut.states ��� s ��� x *) 1102(* ��� equivalentStates aut.final aut.trans s x` *) 1103(* >- (`s_new ��� aut.states ��� ~(s_new = x) *) 1104(* ��� equivalentStates aut.final aut.trans s_new x` by metis_tac[] *) 1105(* >> `(let mergedAut = mergeState x aut *) 1106(* in partial_order *) 1107(* (rrestrict (rel_to_reln (reachRel mergedAut)) *) 1108(* mergedAut.states) mergedAut.states)` by ( *) 1109(* HO_MATCH_MP_TAC MERGE_PO_LEMM >> metis_tac[EQUIV_STATES_SYMM]) *) 1110(* >> fs[] >> simp[isWeakAlterA_def,isWeakWithOrder_def] *) 1111(* >> qexists_tac `(rrestrict (rel_to_reln (reachRel (mergeState x aut))) *) 1112(* (mergeState x aut).states)` *) 1113(* >> simp[] >> rpt strip_tac >> fs[rrestrict_def,rel_to_reln_def] *) 1114(* >> fs[reachRel_def] >> strip_tac *) 1115(* >- (`oneStep (mergeState x aut) s'' s'` *) 1116(* suffices_by metis_tac[RTC_SUBSET] *) 1117(* >> fs[oneStep_def] >> metis_tac[] *) 1118(* ) *) 1119(* >- (fs[isValidAlterA_def] >> metis_tac[SUBSET_DEF]) *) 1120(* ) *) 1121(* >- (`mergeState x aut = aut` by ( *) 1122(* Cases_on `aut` >> simp[mergeState_def,COND_EXPAND] *) 1123(* >> fs[COND_EXPAND] >> metis_tac[] *) 1124(* ) >> metis_tac[] *) 1125(* ) *) 1126(* ); *) 1127 1128(* val RUN_WELLBEHAVED_MERGE = store_thm *) 1129(* ("RUN_WELLBEHAVED_MERGE", *) 1130(* ``!aut r w s x. runForAA aut r w ��� s ��� aut.states ��� ~(s = x) ��� *) 1131(* equivalentStates aut.final aut.trans s x ��� x ��� aut.states *) 1132(* ��� isWeakAlterA aut ��� isValidAlterA aut ��� FINITE aut.states *) 1133(* ==> ?r2. runForAA aut r2 w *) 1134(* ��� !i. (s ��� r2.V i) ��� (x ��� r2.V i) ==> (r2.E (i,s) = r2.E (i,x))``, *) 1135(* gen_tac >> gen_tac >> gen_tac *) 1136(* >> `���ord s x. runForAA aut r w ��� s ��� aut.states ��� s ��� x ��� *) 1137(* equivalentStates aut.final aut.trans s x ��� x ��� aut.states ��� *) 1138(* isWeakWithOrder aut ord ��� isValidAlterA aut ��� *) 1139(* FINITE aut.states *) 1140(* ��� ((s,x) ��� ord \/ (~((x,s) ��� ord) ��� ~((s,x) ��� ord))) ��� *) 1141(* ���r2. *) 1142(* runForAA aut r2 w ��� *) 1143(* ���i. s ��� r2.V i ��� x ��� r2.V i ��� (r2.E (i,s) = r2.E (i,x))` *) 1144(* suffices_by (rpt strip_tac >> fs[isWeakAlterA_def] *) 1145(* >> first_x_assum (qspec_then `ord` mp_tac) *) 1146(* >> rpt strip_tac *) 1147(* >> `(s,x) ��� ord \/ (x,s) ��� ord *) 1148(* \/ (~((x,s) ��� ord) ��� ~((s,x) ��� ord))` by metis_tac[] *) 1149(* >> metis_tac[EQUIV_STATES_SYMM] *) 1150(* ) *) 1151(* >> rpt strip_tac *) 1152(* >> (`~((x,s) ��� ord)` by *) 1153(* (fs[isWeakWithOrder_def,partial_order_def,antisym_def] *) 1154(* >> metis_tac[]) *) 1155(* >> qabbrev_tac `new_run = *) 1156(* run_restr (r.V 0) (ALTERA_RUN r.V *) 1157(* (��(i,q). if (q = x) ��� (s ��� r.V i) *) 1158(* then r.E (i,s) else r.E (i,q)))` *) 1159(* >> `!i. new_run.V i ��� r.V i` by ( *) 1160(* Induct_on `i` *) 1161(* >- (qunabbrev_tac `new_run` >> fs[run_restr_def,validAARunFor_def] *) 1162(* >> fs[run_restr_V_def]) *) 1163(* >- (simp[SUBSET_DEF] >> rpt strip_tac >> qunabbrev_tac `new_run` *) 1164(* >> fs[run_restr_V_def,run_restr_def] *) 1165(* >> Cases_on `(q = x) ��� (s ��� r.V i)` >> fs[] *) 1166(* >> `s' ��� r.V (i + 1)` *) 1167(* by metis_tac[runForAA_def,validAARunFor_def] *) 1168(* >> metis_tac[SUC_ONE_ADD,ADD_COMM,SUBSET_DEF] *) 1169(* ) *) 1170(* ) *) 1171(* >> qexists_tac `new_run` >> fs[runForAA_def] *) 1172(* >> `(validAARunFor aut new_run w *) 1173(* ��� ((validAARunFor aut new_run w ==> acceptingAARun aut new_run))) ��� *) 1174(* ���i. s ��� new_run.V i ��� x ��� new_run.V i ==> *) 1175(* (new_run.E (i,s) = new_run.E (i,x))` suffices_by fs[] *) 1176(* >> rpt strip_tac *) 1177(* >- (simp[validAARunFor_def] >> rpt strip_tac *) 1178(* >- (qunabbrev_tac `new_run` >> fs[run_restr_def,run_restr_V_def] *) 1179(* >> metis_tac[validAARunFor_def]) *) 1180(* >- metis_tac[SUBSET_TRANS,validAARunFor_def] *) 1181(* >- (`q ��� r.V i` by metis_tac[SUBSET_DEF] *) 1182(* >> qunabbrev_tac `new_run` >> simp[run_restr_def,run_restr_E_def] *) 1183(* >> Cases_on `(q = x) ��� (s ��� r.V i)` *) 1184(* >- (fs[validAARunFor_def] *) 1185(* >> `���a. (a,r.E (i,s)) ��� aut.trans s ��� at w i ��� a` *) 1186(* by metis_tac[] *) 1187(* >> qexists_tac `a` >> fs[] *) 1188(* >> `(a,r.E (i,s)) ��� aut.trans x` *) 1189(* suffices_by fs[run_restr_def] *) 1190(* >> metis_tac[equivalentStates_def] *) 1191(* ) *) 1192(* >- (fs[validAARunFor_def] *) 1193(* >> `���a. (a,r.E (i,q)) ��� aut.trans q ��� at w i ��� a` *) 1194(* by metis_tac[] *) 1195(* >> qexists_tac `a` >> fs[] *) 1196(* >> `(a,r.E(i,q)) ��� aut.trans q` suffices_by fs[run_restr_def] *) 1197(* >> metis_tac[] *) 1198(* ) *) 1199(* ) *) 1200(* >- (simp[SUBSET_DEF] >> rpt strip_tac >> qunabbrev_tac `new_run` *) 1201(* >> fs[run_restr_def,run_restr_V_def,run_restr_E_def] *) 1202(* >> qabbrev_tac `fullRunV = \i. *) 1203(* run_restr_V (r.V 0) *) 1204(* (ALTERA_RUN r.V *) 1205(* (��(i,q). *) 1206(* if (q = x) ��� s ��� r.V i *) 1207(* then r.E (i,s) else r.E (i,q))) i` *) 1208(* >> fs[] *) 1209(* >> `q ��� fullRunV i` by metis_tac[MEMBER_NOT_EMPTY] >> fs[] *) 1210(* >> `x' ��� fullRunV (SUC i)` *) 1211(* suffices_by metis_tac[SUC_ONE_ADD,ADD_COMM] *) 1212(* >> qunabbrev_tac `fullRunV` >> simp[run_restr_V_def] *) 1213(* >> Cases_on `(q = x) ��� s ��� r.V i` >> fs[] *) 1214(* >> metis_tac[] *) 1215(* ) *) 1216(* >- (Cases_on `i=0` >> fs[] >> `q ��� r.V i` by metis_tac[SUBSET_DEF] *) 1217(* >> qunabbrev_tac `new_run` *) 1218(* >> simp[] *) 1219(* >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) *) 1220(* >> rw[] >> fs[] *) 1221(* >> fs[run_restr_V_def,run_restr_def,run_restr_E_def] *) 1222(* >> metis_tac[] *) 1223(* ) *) 1224(* ) *) 1225(* >- (`���b f. infBranchOf new_run b ��� branchFixP b f *) 1226(* ��� f ��� aut.final` *) 1227(* suffices_by metis_tac[BRANCH_ACC_LEMM,isWeakAlterA_def] *) 1228(* >> `���b1 f1. infBranchOf r b1 ��� branchFixP b1 f1 *) 1229(* ��� f1 ��� aut.final` by metis_tac[BRANCH_ACC_LEMM,isWeakAlterA_def] *) 1230(* >> rpt strip_tac >> fs[branchFixP_def] *) 1231(* >> Cases_on `(f = x) ��� ((f = x) ==> ?j. i <= j ��� s ��� r.V j)` *) 1232(* >> fs[] *) 1233(* >- (`?j. i <= j ��� s ��� r.V j` by fs[] *) 1234(* >> `!j. b j ��� new_run.V j` by metis_tac[BRANCH_V_LEMM] *) 1235(* >> fs[infBranchOf_def] *) 1236(* >> `x ��� new_run.E (j, x)` by ( *) 1237(* `b (j + 1) = x` by simp[] *) 1238(* >> `b j = x` by simp[] *) 1239(* >> `b (j + 1) ��� new_run.E (j, b j)` by metis_tac[] *) 1240(* >> metis_tac[] *) 1241(* ) *) 1242(* >> qunabbrev_tac `new_run` >> POP_ASSUM mp_tac *) 1243(* >> simp[run_restr_def, run_restr_E_def] *) 1244(* >> `b j = x` by simp[] *) 1245(* >> first_x_assum (qspec_then `j` mp_tac) *) 1246(* >> simp[run_restr_def] >> rpt strip_tac *) 1247(* >> fs[validAARunFor_def] *) 1248(* >> `���a. (a,r.E (j,s)) ��� aut.trans s ��� at w j ��� a` *) 1249(* by metis_tac[] *) 1250(* >> metis_tac[isWeakWithOrder_def] *) 1251(* ) *) 1252(* >- (`infBranchSuffOf r i (\p. f)` by ( *) 1253(* simp[infBranchSuffOf_def] >> rpt strip_tac *) 1254(* >- (`f ��� new_run.V i` *) 1255(* by metis_tac[BRANCH_V_LEMM, DECIDE ``i >= i``] *) 1256(* >> metis_tac[SUBSET_DEF] *) 1257(* ) *) 1258(* >- (fs[infBranchOf_def] *) 1259(* >> `f ��� new_run.E (i + p, f)` by ( *) 1260(* `b (i + p + 1) = f` by fs[] *) 1261(* >> `b (i + p) = f` by fs[] *) 1262(* >> metis_tac[]) *) 1263(* >> qunabbrev_tac `new_run` *) 1264(* >> fs[run_restr_def, run_restr_E_def] *) 1265(* >> metis_tac[MEMBER_NOT_EMPTY] *) 1266(* ) *) 1267(* ) *) 1268(* >> qabbrev_tac `new_branch = \p:num. f` *) 1269(* >> `���b'. infBranchOf r b' ��� ���a. new_branch a = b' (a + i)` *) 1270(* by metis_tac[BRANCH_SUFF_LEMM] *) 1271(* >> rename[`infBranchOf r b'`] *) 1272(* >> first_x_assum (qspec_then `b'` mp_tac) >> rpt strip_tac *) 1273(* >> first_x_assum (qspec_then `f` mp_tac) >> simp[] *) 1274(* >> qexists_tac `i` >> qunabbrev_tac `new_branch` *) 1275(* >> rpt strip_tac >> fs[] *) 1276(* >- metis_tac[DECIDE ``0 + i = i``] *) 1277(* >- (`i <= m` by simp[] *) 1278(* >> `?p. m = i + p` by metis_tac[LESS_EQ_EXISTS] *) 1279(* >> metis_tac[ADD_COMM] *) 1280(* ) *) 1281(* ) *) 1282(* >- (`infBranchSuffOf r i (\p. f)` by ( *) 1283(* simp[infBranchSuffOf_def] >> rpt strip_tac *) 1284(* >- (`f ��� new_run.V i` *) 1285(* by metis_tac[BRANCH_V_LEMM, DECIDE ``i >= i``] *) 1286(* >> metis_tac[SUBSET_DEF] *) 1287(* ) *) 1288(* >- (fs[infBranchOf_def] >> rw[] *) 1289(* >> `f ��� new_run.E (i + p, f)` by ( *) 1290(* `b (i + p + 1) = f` by fs[] *) 1291(* >> `b (i + p) = f` by fs[] *) 1292(* >> metis_tac[]) *) 1293(* >> qunabbrev_tac `new_run` *) 1294(* >> fs[run_restr_def, run_restr_E_def] *) 1295(* >> metis_tac[MEMBER_NOT_EMPTY,DECIDE ``i <= i + p``] *) 1296(* ) *) 1297(* ) *) 1298(* >> qabbrev_tac `new_branch = \p:num. f` *) 1299(* >> `���b'. infBranchOf r b' ��� ���j. new_branch j = b' (j + i)` *) 1300(* by metis_tac[BRANCH_SUFF_LEMM] *) 1301(* >> rename[`infBranchOf r b'`] *) 1302(* >> first_x_assum (qspec_then `b'` mp_tac) >> rpt strip_tac *) 1303(* >> first_x_assum (qspec_then `f` mp_tac) >> simp[] *) 1304(* >> qexists_tac `i` >> qunabbrev_tac `new_branch` *) 1305(* >> rpt strip_tac >> fs[] *) 1306(* >- metis_tac[DECIDE ``i + 0 = i``] *) 1307(* >- (`i <= m` by simp[] *) 1308(* >> `?p. m = i + p` by metis_tac[LESS_EQ_EXISTS] *) 1309(* >> metis_tac[] *) 1310(* ) *) 1311(* ) *) 1312(* ) *) 1313(* >- (`s ��� r.V i ��� x ��� r.V i` by metis_tac[SUBSET_DEF] *) 1314(* >> qunabbrev_tac `new_run` >> simp[SET_EQ_SUBSET,SUBSET_DEF] *) 1315(* >> rpt strip_tac >> fs[run_restr_def, run_restr_E_def] *) 1316(* >> metis_tac[MEMBER_NOT_EMPTY] *) 1317(* ) *) 1318(* ) *) 1319(* ); *) 1320 1321(*up to here should work with new reach rel*) 1322 1323 1324(* val MERGE_STATE_CORRECT = store_thm *) 1325(* ("MERGE_STATE_CORRECT", *) 1326(* ``!aut x. x ��� aut.states ��� isWeakAlterA aut ��� isValidAlterA aut *) 1327(* ��� FINITE aut.states ==> *) 1328(* (alterA_lang aut = alterA_lang (mergeState x aut))``, *) 1329(* rw[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] *) 1330(* >> rename[`word_range x'`] *) 1331(* >- (`word_range x' ��� (mergeState x aut).alphabet` by *) 1332(* (Cases_on `aut` >> fs[mergeState_def] >> rw[COND_EXPAND_OR]) *) 1333(* >> fs[] *) 1334(* >> Cases_on `���s. s ��� aut.states *) 1335(* ��� s ��� x ��� equivalentStates aut.final aut.trans s x` *) 1336(* >- (qabbrev_tac `s' = *) 1337(* $@ (\s. s ��� aut.states ��� s ��� x *) 1338(* ��� equivalentStates aut.final aut.trans s x)` *) 1339(* >> `���r2. *) 1340(* runForAA aut r2 x' ��� *) 1341(* ���i. s' ��� r2.V i ��� x ��� r2.V i ��� (r2.E (i,s') = r2.E (i,x))` *) 1342(* by metis_tac[RUN_WELLBEHAVED_MERGE] *) 1343(* >> qabbrev_tac `repl_run = replace_run r2 x s'` *) 1344(* >> qabbrev_tac `new_run = run_restr (repl_run.V 0) repl_run` *) 1345(* >> qexists_tac `new_run` *) 1346(* >> fs[runForAA_def] *) 1347(* >> `validAARunFor (mergeState x aut) new_run x' ��� *) 1348(* (validAARunFor (mergeState x aut) new_run x' *) 1349(* ==> acceptingAARun (mergeState x aut) new_run)` *) 1350(* suffices_by fs[] *) 1351(* >> rpt strip_tac *) 1352(* >> `!i q. ((q ��� new_run.V i) ��� ~(q = s') *) 1353(* ==> (q ��� r2.V i) ��� ~(q = x))` by ( *) 1354(* Induct_on `i` >> fs[] >> rpt strip_tac *) 1355(* >- (qunabbrev_tac `new_run` >> qunabbrev_tac `repl_run` *) 1356(* >> fs[replace_run_def,replaceState_def,run_restr_def] *) 1357(* >> fs[run_restr_V_def] *) 1358(* >> Cases_on `x ��� r2.V 0` >> fs[] *) 1359(* ) *) 1360(* >- (qunabbrev_tac `new_run` >> qunabbrev_tac `repl_run` *) 1361(* >> fs[replace_run_def,replaceState_def,run_restr_def] *) 1362(* >> fs[run_restr_V_def] *) 1363(* >> Cases_on `x ��� r2.V 0` >> fs[] *) 1364(* ) *) 1365(* >- (qunabbrev_tac `new_run` >> qunabbrev_tac `repl_run` *) 1366(* >> fs[run_restr_def, run_restr_V_def] *) 1367(* >> rename [`q' ��� _`] *) 1368(* >> Cases_on `q'' = s'` *) 1369(* >> fs[replace_run_def, replaceState_def] *) 1370(* >- (Cases_on `s' ��� r2.V i` >> fs[validAARunFor_def] *) 1371(* >> Cases_on `(q' = x)` >> Cases_on `x ��� r2.E (i,x)` *) 1372(* >> Cases_on `x ��� r2.E (i,s')` *) 1373(* >> rw[] >> fs[] *) 1374(* >> metis_tac[SUC_ONE_ADD,ADD_COMM,SUBSET_DEF] *) 1375(* ) *) 1376(* >- (`q'' ��� r2.V i` by metis_tac[] *) 1377(* >> fs[validAARunFor_def] *) 1378(* >> Cases_on `x ��� r2.E (i,q'')` >> fs[] *) 1379(* >> metis_tac[SUC_ONE_ADD,ADD_COMM,SUBSET_DEF] *) 1380(* ) *) 1381(* ) *) 1382(* >- (qunabbrev_tac `new_run` >> qunabbrev_tac `repl_run` *) 1383(* >> fs[run_restr_def, replace_run_def, replaceState_def] *) 1384(* >> fs[run_restr_V_def] *) 1385(* >> Cases_on `(q' = s') ��� (s' ��� r2.V i)` *) 1386(* >> Cases_on `x ��� r2.E (i,x)` *) 1387(* >> Cases_on `x ��� r2.E (i,q')` *) 1388(* >> rpt (fs[]) *) 1389(* ) *) 1390(* ) *) 1391(* >> `!i. (s' ��� new_run.V i) ��� ~(s' ��� r2.V i) ==> (x ��� r2.V i)` by ( *) 1392(* Cases_on `i` >> qunabbrev_tac `new_run` *) 1393(* >> qunabbrev_tac `repl_run` >> fs[] >> rpt strip_tac *) 1394(* >> fs[run_restr_def,run_restr_V_def,replace_run_def] *) 1395(* >> fs[replaceState_def] *) 1396(* >- (Cases_on `x ��� r2.V 0` >> metis_tac[]) *) 1397(* >- (rw[] >> Cases_on `(q = s') ��� s' ��� r2.V i` *) 1398(* >> Cases_on `x ��� r2.E (i,x)` *) 1399(* >> Cases_on `x ��� r2.E (i,q)` *) 1400(* >> fs[validAARunFor_def] *) 1401(* >> metis_tac[SUC_ONE_ADD,ADD_COMM,SUBSET_DEF] *) 1402(* ) *) 1403(* ) *) 1404(* >> simp[validAARunFor_def] *) 1405(* >> rpt strip_tac *) 1406(* >- (Cases_on `x ��� r2.V 0` >> fs[] *) 1407(* >> qunabbrev_tac `new_run` >> qunabbrev_tac `repl_run` *) 1408(* >> fs[run_restr_def, run_restr_V_def] *) 1409(* >> fs[replace_run_def, replaceState_def] *) 1410(* >- (`s' ��� aut.states ��� ~(s' = x) *) 1411(* ��� equivalentStates aut.final aut.trans s' x` *) 1412(* by metis_tac[SELECT_THM] *) 1413(* >> Cases_on `aut` >> fs[mergeState_def] *) 1414(* >> simp[] >> rw[] *) 1415(* >- (qexists_tac `r2.V 0` >> fs[validAARunFor_def] *) 1416(* >> fs[replaceState_def] *) 1417(* ) *) 1418(* >- metis_tac[] *) 1419(* ) *) 1420(* >- (Cases_on `aut` >> fs[mergeState_def] >> rw[] *) 1421(* >- (qexists_tac `r2.V 0` >> fs[validAARunFor_def] *) 1422(* >> fs[replaceState_def] *) 1423(* ) *) 1424(* >- metis_tac[] *) 1425(* ) *) 1426(* ) *) 1427(* >- (qunabbrev_tac `new_run` >> qunabbrev_tac `repl_run` *) 1428(* >> simp[SUBSET_DEF, replace_run_def] >> rpt strip_tac *) 1429(* >> fs[replaceState_def] >> Cases_on `x ��� r2.V i` *) 1430(* >> rename[`x'' ��� _`] *) 1431(* >> (fs[] >> Cases_on `~(x'' = s')` *) 1432(* >- (Cases_on `aut` >> fs[mergeState_def] *) 1433(* >> rw[] >> fs[validAARunFor_def] *) 1434(* >> fs[run_restr_def,replace_run_def] *) 1435(* >> fs[replaceState_def] *) 1436(* >> `x'' ��� r2.V i` by metis_tac[] *) 1437(* >> metis_tac[SUBSET_DEF]) *) 1438(* >- (Cases_on `aut` >> fs[mergeState_def] *) 1439(* >> rw[] >> metis_tac[SELECT_THM]) *) 1440(* ) *) 1441(* ) *) 1442(* >- (Cases_on `(q = s') ��� ~(s' ��� r2.V i)` >> fs[] *) 1443(* >- (`x ��� r2.V i` by fs[] *) 1444(* >> `?a. (a, r2.E (i,x)) ��� aut.trans x ��� at x' i ��� a` *) 1445(* by metis_tac[validAARunFor_def] *) 1446(* >> qexists_tac `a` >> fs[] *) 1447(* >> Cases_on `aut` >> fs[mergeState_def] >> rw[] *) 1448(* >- (simp[replaceBy_def] *) 1449(* >> qexists_tac `(a,r2.E (i,x))` *) 1450(* >> fs[replaceSingleTrans_def] *) 1451(* >> `equivalentStates f1 f3 q x` *) 1452(* by metis_tac[SELECT_THM] *) 1453(* >> simp[run_restr_E_def,run_restr_def] *) 1454(* >> qunabbrev_tac `new_run` >> rw[] *) 1455(* >> qunabbrev_tac `repl_run` *) 1456(* >> fs[run_restr_def,run_restr_E_def] *) 1457(* >> fs[replace_run_def,replaceState_def] *) 1458(* >> fs[validAARunFor_def,equivalentStates_def] *) 1459(* ) *) 1460(* >- metis_tac[] *) 1461(* ) *) 1462(* >- (rw[] >> fs[replace_run_def, replaceState_def] *) 1463(* >> `q ��� r2.V i` by metis_tac[IN_UNION,IN_DIFF] *) 1464(* >> `?a. (a, r2.E (i,q)) ��� aut.trans q ��� at x' i ��� a` *) 1465(* by metis_tac[validAARunFor_def] *) 1466(* >> qexists_tac `a` >> fs[] >> Cases_on `aut` *) 1467(* >> fs[mergeState_def] >> rw[] *) 1468(* >- (simp[replaceBy_def] *) 1469(* >> qexists_tac `(a,r2.E (i,q))` *) 1470(* >> fs[replaceSingleTrans_def] *) 1471(* >> qunabbrev_tac `new_run` *) 1472(* >> fs[run_restr_def, run_restr_E_def] *) 1473(* >> qunabbrev_tac `repl_run` >> rw[] *) 1474(* ) *) 1475(* >- (qunabbrev_tac `new_run` *) 1476(* >> simp[run_restr_def,run_restr_E_def] *) 1477(* >> fs[run_restr_def] *) 1478(* >> qunabbrev_tac `repl_run` *) 1479(* >> fs[] >> metis_tac[] *) 1480(* ) *) 1481(* ) *) 1482(* >- (rw[] >> fs[replace_run_def, replaceState_def] *) 1483(* >> rw[] >> `?a. (a, r2.E (i,q)) ��� aut.trans q *) 1484(* ��� at x' i ��� a` *) 1485(* by metis_tac[validAARunFor_def] *) 1486(* >> qexists_tac `a` >> fs[] >> Cases_on `aut` *) 1487(* >> fs[mergeState_def] >> rw[] *) 1488(* >- (simp[replaceBy_def] *) 1489(* >> qexists_tac `(a,r2.E (i,q))` *) 1490(* >> fs[replaceSingleTrans_def] *) 1491(* >> qunabbrev_tac `new_run` *) 1492(* >> fs[run_restr_def, run_restr_E_def] *) 1493(* >> qunabbrev_tac `repl_run` >> rw[] *) 1494(* ) *) 1495(* >- metis_tac[] *) 1496(* ) *) 1497(* ) *) 1498(* >- (qunabbrev_tac `new_run` >> simp[run_restr_def,run_restr_E_def] *) 1499(* >> simp[run_restr_V_def, DECIDE ``i + 1 = SUC i``] *) 1500(* >> Cases_on `q ��� run_restr_V (repl_run.V 0) repl_run i` *) 1501(* >> fs[EMPTY_SUBSET] *) 1502(* >> simp[BIGUNION,SUBSET_DEF] >> rpt strip_tac *) 1503(* >> metis_tac[] *) 1504(* ) *) 1505(* >- (Cases_on `i = 0` >> fs[replace_run_def, replaceState_def] *) 1506(* >> qunabbrev_tac `new_run` *) 1507(* >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) *) 1508(* >> rw[] >> fs[run_restr_def, run_restr_V_def] *) 1509(* >> metis_tac[run_restr_E_def] *) 1510(* ) *) 1511(* >- (`FINITE (mergeState x aut).states` by ( *) 1512(* Cases_on `aut` >> simp[mergeState_def] *) 1513(* >> Cases_on `���s. s ��� f ��� s ��� x *) 1514(* ��� equivalentStates f1 f3 s x` >> simp[] *) 1515(* >> fs[] >> metis_tac[FINITE_DIFF] *) 1516(* ) *) 1517(* >> `isWeakAlterA (mergeState x aut)` *) 1518(* by metis_tac[MERGE_IS_WEAK,MERGE_IS_VALID] *) 1519(* >> `���b q. infBranchOf new_run b ��� branchFixP b q *) 1520(* ��� q ��� (mergeState x aut).final` *) 1521(* suffices_by metis_tac[BRANCH_ACC_LEMM] *) 1522(* >> `���b1 q1. infBranchOf r2 b1 ��� branchFixP b1 q1 *) 1523(* ��� q1 ��� aut.final` by metis_tac[BRANCH_ACC_LEMM] *) 1524(* >> rpt strip_tac *) 1525(* >> `?b2. infBranchOf r2 b2 *) 1526(* ��� (branchFixP b2 q \/ ((q = s') ��� branchFixP b2 x))` *) 1527(* suffices_by ( *) 1528(* Cases_on `aut` >> fs[mergeState_def] *) 1529(* >> `q ��� *) 1530(* (ALTER_A (f DIFF {x}) (IMAGE *) 1531(* (replaceState x *) 1532(* (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x)) f0) *) 1533(* (replaceState x *) 1534(* (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x) f1) f2 *) 1535(* (replaceBy f3 x *) 1536(* (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x))).final` *) 1537(* by metis_tac[] >> fs[replaceState_def] *) 1538(* >> Cases_on `x ��� f1` >> fs[] *) 1539(* >- metis_tac[] *) 1540(* >- (`q ��� f1` by metis_tac[equivalentStates_def] *) 1541(* >> metis_tac[]) *) 1542(* >- (rpt strip_tac >> Cases_on `infBranchOf r2 b2` *) 1543(* >- (fs[] >> strip_tac *) 1544(* >- metis_tac[] *) 1545(* >- (Cases_on `q= s'` >> fs[] *) 1546(* >> metis_tac[equivalentStates_def] *) 1547(* ) *) 1548(* ) *) 1549(* >- fs[] *) 1550(* ) *) 1551(* ) *) 1552(* >> Cases_on `~(q = s')` *) 1553(* >- (fs[branchFixP_def] *) 1554(* >> `infBranchSuffOf r2 i (\a. q)` by ( *) 1555(* simp[infBranchSuffOf_def] >> rpt strip_tac *) 1556(* >- (`q ��� new_run.V i` by ( *) 1557(* fs[infBranchOf_def,validAARunFor_def] *) 1558(* >> `b i = q` by fs[] *) 1559(* >> Cases_on `i = 0` >> fs[] *) 1560(* >> `?j. SUC j = i` by *) 1561(* (Cases_on `i` >> fs[]) *) 1562(* >> `j + 1 = i` by simp[] *) 1563(* >> metis_tac[SUBSET_DEF] *) 1564(* ) *) 1565(* >> metis_tac[] *) 1566(* ) *) 1567(* >- (`(a + i) + 1 >= i` by simp[] *) 1568(* >> `b (a + i + 1) = q` by fs[] *) 1569(* >> `b (a + i) = q` by fs[] *) 1570(* >> `q ��� new_run.E (a + i,q)` *) 1571(* by metis_tac[infBranchOf_def] *) 1572(* >> qunabbrev_tac `new_run` *) 1573(* >> qunabbrev_tac `repl_run` *) 1574(* >> fs[run_restr_def,run_restr_E_def] *) 1575(* >> `q ��� (replace_run r2 x s').E (a + i,q)` *) 1576(* by metis_tac[MEMBER_NOT_EMPTY] *) 1577(* >> fs[replace_run_def] *) 1578(* >> `q ��� replaceState x s' (r2.E (a + i,q))` *) 1579(* by metis_tac[] >> POP_ASSUM mp_tac *) 1580(* >> simp[replaceState_def] >> rpt strip_tac *) 1581(* >> Cases_on `x ��� r2.E (a + i,q)` >> fs[] *) 1582(* >> rw[] *) 1583(* ) *) 1584(* ) *) 1585(* >> qabbrev_tac `infSuff = (\a:num. q)` *) 1586(* >> `���b'. infBranchOf r2 b' ��� ���j. infSuff j = b' (j + i)` *) 1587(* by metis_tac[BRANCH_SUFF_LEMM] *) 1588(* >> qexists_tac `b'` >> fs[] >> qexists_tac `i` >> fs[] *) 1589(* >> qunabbrev_tac `infSuff` >> rw[] *) 1590(* >- (fs[] >> metis_tac[DECIDE ``i + 0 = i``]) *) 1591(* >- (fs[] >> `i <= m` by simp[] *) 1592(* >> `?p. p + i = m` by metis_tac[LESS_EQ_ADD_EXISTS] *) 1593(* >> metis_tac[ADD_COMM] *) 1594(* ) *) 1595(* ) *) 1596(* >- (fs[branchFixP_def] *) 1597(* >> Cases_on `?a. ~(s' ��� r2.E (a + i,s'))` *) 1598(* (* >- (fs[] >> rw[] *) *) 1599(* (* >> `q ��� new_run.E (a + i,q)` by ( *) *) 1600(* (* fs[infBranchOf_def] >> `a + i >= i` by simp[] *) *) 1601(* (* >> `a + i + 1 >= i` by simp[] *) *) 1602(* (* >> `b (a + i) = q` by fs[] *) *) 1603(* (* >> `b (a + i + 1) = q` by simp[] *) *) 1604(* (* >> fs[] >> rw[] >> metis_tac[ADD_ASSOC] *) *) 1605(* (* ) *) *) 1606(* (* >> Cases_on `q ��� r2.V (a+i)` *) *) 1607(* (* >- (`x ��� r2.E (a + i, q)` by ( *) *) 1608(* (* qunabbrev_tac `new_run` >> fs[run_restr_def] *) *) 1609(* (* >> fs[run_restr_E_def] *) *) 1610(* (* >> `q ��� repl_run.E (a + i,q)` *) *) 1611(* (* by metis_tac[MEMBER_NOT_EMPTY] *) *) 1612(* (* >> qunabbrev_tac `repl_run` >> fs[replace_run_def] *) *) 1613(* (* >> `q ��� replaceState x q (r2.E (a + i,q))` *) *) 1614(* (* by metis_tac[] *) *) 1615(* (* >> fs[replaceState_def] >> metis_tac[] *) *) 1616(* (* ) *) *) 1617(* (* >> `infBranchSuffOf r2 (a+i+1) (\p. x)` by ( *) *) 1618(* (* simp[infBranchSuffOf_def] >> strip_tac *) *) 1619(* (* >- (fs[validAARunFor_def] *) *) 1620(* (* >> metis_tac[SUBSET_DEF,ADD_ASSOC]) *) *) 1621(* (* >- (`!p. (x ��� r2.E (a+i+p+1,x)) *) *) 1622(* (* ��� (x ��� r2.V (a+i+p+1))` *) *) 1623(* (* suffices_by fs[] *) *) 1624(* (* >> Induct_on `p` >> fs[] *) *) 1625(* (* >- (rpt strip_tac >> fs[validAARunFor_def] *) *) 1626(* (* >> `x ��� r2.V(a+i+1)` *) *) 1627(* (* by metis_tac[SUBSET_DEF] *) *) 1628(* (* >> `q ��� new_run.E (a+i+1,q)` by ( *) *) 1629(* (* fs[infBranchOf_def] *) *) 1630(* (* >> `b (a+i+1) = q` by simp[] *) *) 1631(* (* >> `b (a+i+1+1) = q` by simp[] *) *) 1632(* (* >> metis_tac[ADD_ASSOC]) *) *) 1633(* (* >> qunabbrev_tac `new_run` *) *) 1634(* (* >> fs[run_restr_def,run_restr_E_def] *) *) 1635(* (* >> `q ��� repl_run.E (a+i+1,q)` *) *) 1636(* (* by metis_tac[MEMBER_NOT_EMPTY,ADD_ASSOC] *) *) 1637(* (* >> qunabbrev_tac `repl_run` *) *) 1638(* (* >> fs[replace_run_def,replaceState_def] *) *) 1639(* (* >> Cases_on `x ��� r2.E(a+i+1,q)` *) *) 1640(* (* >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) *) 1641(* (* >> simp[] *) *) 1642(* (* >> metis_tac[] *) *) 1643(* (* ) *) *) 1644(* (* ) *) *) 1645(* (* ) *) *) 1646(* >- (fs[] *) 1647(* >> qabbrev_tac `P = \n. ~(s' ��� r2.E (n + i, s'))` *) 1648(* >> qabbrev_tac `N = $LEAST P` *) 1649(* >> `(!n. n < N ==> ~ P n) ��� P ($LEAST P)` by ( *) 1650(* qunabbrev_tac `N` *) 1651(* >> metis_tac[LEAST_EXISTS_IMP,EXISTS_THM] *) 1652(* ) *) 1653(* >> rw[] *) 1654(* >> `q ��� new_run.E (N + i,q)` by ( *) 1655(* fs[infBranchOf_def] >> `N + i >= i` by simp[] *) 1656(* >> `N + i + 1 >= i` by simp[] *) 1657(* >> `b (N + i) = q` by metis_tac[] *) 1658(* >> `b (N + i + 1) = q` by simp[] *) 1659(* >> fs[] >> metis_tac[ADD_ASSOC] *) 1660(* ) *) 1661(* >> Cases_on `q ��� r2.V i` *) 1662(* >- (`!n. n <= N ==> q ��� r2.V (n + i)` *) 1663(* by ( *) 1664(* Induct_on `n` >> rpt strip_tac >> fs[] *) 1665(* >> `n < N` by simp[] *) 1666(* >> `~P n` by fs[] >> qunabbrev_tac `P` *) 1667(* >> fs[] >> fs[validAARunFor_def] *) 1668(* >> `q ��� r2.V (i + n + 1)` suffices_by *) 1669(* metis_tac[ADD_SUC,ADD_COMM,SUC_ONE_ADD] *) 1670(* >> metis_tac[SUBSET_DEF] *) 1671(* ) *) 1672(* >> `q ��� r2.V (N + i)` *) 1673(* by metis_tac[DECIDE ``N <= N``] *) 1674(* >> `x ��� r2.E (i + N, q)` by ( *) 1675(* `q ��� r2.V (i + N)` by fs[] *) 1676(* >> `~(q ��� r2.E (N + i, q))` by ( *) 1677(* qunabbrev_tac `P` >> qunabbrev_tac `N` *) 1678(* >> fs[] >> metis_tac[ADD_COMM] *) 1679(* ) *) 1680(* >> qunabbrev_tac `new_run` *) 1681(* >> qunabbrev_tac `repl_run` *) 1682(* >> fs[run_restr_def, run_restr_E_def] *) 1683(* >> `q *) 1684(* ��� (replace_run r2 x (q)).E (N + i,q)` *) 1685(* by metis_tac[MEMBER_NOT_EMPTY] *) 1686(* >> fs[replace_run_def] *) 1687(* >> `q ��� *) 1688(* replaceState x (q) (r2.E (N + i,q))` *) 1689(* by metis_tac[] *) 1690(* >> POP_ASSUM mp_tac >> simp[replaceState_def] *) 1691(* >> rpt strip_tac >> metis_tac[] *) 1692(* ) *) 1693(* >> `infBranchSuffOf r2 (N+i+1) (\p. x)` by ( *) 1694(* >> fs[infBranchSuffOf_def] >> strip_tac *) 1695(* >- (fs[validAARunFor_def] *) 1696(* >> metis_tac[ADD_ASSOC,SUBSET_DEF]) *) 1697(* >- ( *) 1698 1699 1700(* `q ��� r2.E (N+i+1,q)` by ( *) 1701(* `q ��� new_run.E (N+i+1,q)` by ( *) 1702(* fs[infBranchOf_def] *) 1703(* >> `b (N+i+1+1) = q` by simp[] *) 1704(* >> `b (N+i+1) = q` by simp[] *) 1705(* >> metis_tac[ADD_ASSOC] *) 1706(* ) *) 1707(* >> qunabbrev_tac `new_run` *) 1708(* >> fs[run_restr_def, run_restr_E_def] *) 1709(* >> `q ��� repl_run.E (N+i+1,q)` *) 1710(* by metis_tac[MEMBER_NOT_EMPTY,ADD_ASSOC] *) 1711(* >> qunabbrev_tac `repl_run` *) 1712(* >> fs[replace_run_def,replaceState_def] *) 1713(* >> `~(q ��� r2.E (N+i+1,x))` by ( *) 1714(* fs[isWeakAlterA_def] *) 1715(* >> `(x,q) ��� ord` by ( *) 1716(* fs[isWeakWithOrder_def,validAARunFor_def] *) 1717(* >> metis_tac[SUBSET_DEF] *) 1718(* ) *) 1719(* >> CCONTR_TAC >> fs[] *) 1720(* >> `(q,x) ��� ord` by ( *) 1721(* fs[isWeakWithOrder_def,validAARunFor_def] *) 1722(* >> `x ��� r2.V (N+i+1)` by *) 1723(* metis_tac[ADD_ASSOC,SUBSET_DEF] *) 1724(* >> metis_tac[SUBSET_DEF,ADD_ASSOC]) *) 1725(* ) *) 1726(* >> fs[isWeakWithOrder_def,partial_order_def] *) 1727(* >> metis_tac[antisym_def] *) 1728(* ) *) 1729(* ) *) 1730(* >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 1731(* >> simp[] >> Cases_on `x ��� r2.E *) 1732 1733(* >> `!n. x ��� r2.E (i + N + n + 1,x)` by ( *) 1734(* Induct_on `n` >> rpt strip_tac >> fs[] *) 1735(* >- (`x ��� r2.V (N + i + 1)` *) 1736(* by metis_tac[validAARunFor_def,SUBSET_DEF] *) 1737(* >> `b (N + i + 1) ��� new_run.V (N + i + 1)` *) 1738(* by metis_tac[BRANCH_V_LEMM] *) 1739(* >> `b i ��� new_run.V (N + i + 1)` by ( *) 1740(* metis_tac[DECIDE ``N + i + 1 >= i``] *) 1741(* ) *) 1742(* >> `((b i ��� r2.V (N + i + 1)) *) 1743(* \/ (x ��� r2.V (N + i + 1)))` *) 1744(* by metis_tac[] *) 1745(* >- (`r2.E (N + i + 1,b i) *) 1746(* ��� r2.E (N + i + 1,x)` by ( *) 1747(* `x ��� r2.V (N + i + 1)` by *) 1748(* metis_tac[validAARunFor_def] *) 1749(* >> metis_tac[SET_EQ_SUBSET] *) 1750(* ) *) 1751(* >> `x ��� r2.E (N + i + 1,b i)` by ( *) 1752(* `b i ��� new_run.E (N + i + 1, b i)` *) 1753(* by (fs[infBranchOf_def] *) 1754(* >> `b (N + i + 1 + 1) = b i` *) 1755(* by fs[] *) 1756(* >> `b (N + i + 1) = b i` *) 1757(* by fs[] *) 1758(* >> metis_tac[ADD_ASSOC] *) 1759(* ) *) 1760(* >> `b i ��� r2.E (N + i + 1,b i)` *) 1761(* by (qunabbrev_tac `P` >> fs[] *) 1762(* >> *) 1763(* ) *) 1764 1765 1766 1767 1768(* ) *) 1769(* ) *) 1770 1771 1772(* ) *) 1773 1774 1775 1776 1777(* >> `infBranchSuffOf run (a + i + 1) (\n. x)` by ( *) 1778(* simp[infBranchSuffOf_def] >> rpt strip_tac *) 1779(* >- (fs[validAARunFor_def] *) 1780(* >> metis_tac[SUBSET_DEF,ADD_ASSOC]) *) 1781(* >- (`q ��� new_run.E (a + i + n + 1, q)` by ( *) 1782(* fs[infBranchOf_def] *) 1783(* >> `a + i + n + 1 >= i` by simp[] *) 1784(* >> `a + i + n + 1 + 1 >= i` by simp[] *) 1785(* >> `b (a + i + n + 1) = q` by metis_tac[] *) 1786(* >> `b (a + i + n + 1 + 1) = q` *) 1787(* by metis_tac[] *) 1788(* >> metis_tac[ADD_ASSOC] *) 1789(* ) *) 1790(* >> qunabbrev_tac `new_run` *) 1791(* >> qunabbrev_tac `repl_run` *) 1792(* >> fs[run_restr_def, run_restr_E_def] *) 1793(* >> `q ��� (replace_run run x q).E *) 1794(* (a + (i + (n + 1)),q)` *) 1795(* by metis_tac[MEMBER_NOT_EMPTY] *) 1796(* >> fs[replace_run_def] *) 1797(* >> `!n. a + i <= n ==> ~(q ��� run.V n)` by ( *) 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808(* ) *) 1809 1810 1811(* ) *) 1812 1813 1814 1815(* )) *) 1816 1817 1818 1819(* ) *) 1820 1821 1822(* ) *) 1823 1824 1825 1826(* ) *) 1827(* ) *) 1828 1829 1830val _ = export_theory(); 1831