1open HolKernel Parse bossLib boolLib pairTheory pred_setTheory relationTheory set_relationTheory arithmeticTheory 2 3open buechiATheory 4 5val _ = new_theory "gbaSimpl" 6 7(* 8 Reducing the amount of transitions 9*) 10 11val trans_implies_def = Define` 12 trans_implies accTrans q (a1,q1) (a2,q2) 13 = (q1 = q2) ��� a2 ��� a1 14 ��� !t. t ��� accTrans ==> ((q,a2,q2) ��� t ==> (q,a1,q1) ��� t)`; 15 16val TRANS_IMPLIES_PO = store_thm 17 ("TRANS_IMPLIES_PO", 18 ``!aT q d. 19 partial_order (rrestrict (rel_to_reln (trans_implies aT q)) d) d``, 20 fs[partial_order_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac 21 >- (fs[domain_def,SUBSET_DEF] >> rpt strip_tac) 22 >- (fs[range_def, SUBSET_DEF] >> rpt strip_tac) 23 >- (fs[transitive_def,SUBSET_DEF] >> rpt strip_tac 24 >> Cases_on `x` >> Cases_on `y` >> Cases_on `z` >> fs[trans_implies_def] 25 >> metis_tac[SUBSET_TRANS]) 26 >- (fs[reflexive_def,SUBSET_DEF] >> rpt strip_tac >> Cases_on `x` 27 >> fs[trans_implies_def]) 28 >- (fs[antisym_def,SUBSET_DEF] >> rpt strip_tac >> Cases_on `x` 29 >> Cases_on `y` >> fs[trans_implies_def] 30 >> metis_tac[SUBSET_ANTISYM] 31 ) 32 ); 33 34val TRANS_IMPLIES_FINITE = store_thm 35 ("TRANS_IMPLIES_FINITE", 36 ``!aT q d. FINITE d ==> 37 finite_prefixes (rrestrict (rel_to_reln (trans_implies aT q)) d) d``, 38 fs[finite_prefixes_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac 39 >> `FINITE {e' | e' ��� (\x. trans_implies aT q x e) ��� e' ��� d }` 40 suffices_by fs[IN_DEF] 41 >> metis_tac[INTER_DEF,INTER_FINITE,INTER_COMM] 42 ); 43 44val TRANS_IMPLIES_MIN = store_thm 45 ("TRANS_IMPLIES_MIN", 46 ``!aut q1 q2 w i a. FINITE aut.states ��� FINITE aut.alphabet ��� isValidGBA aut 47 ��� q1 ��� aut.states ��� (a,q2) ��� aut.trans q1 48 ==> let rel = rrestrict 49 (rel_to_reln (trans_implies aut.accTrans q1)) 50 (aut.trans q1) 51 in ?t. t ��� minimal_elements (aut.trans q1) rel 52 ��� (t,(a, q2)) ��� rel``, 53 rpt strip_tac >> simp[] 54 >> qabbrev_tac `rel = rrestrict 55 (rel_to_reln (trans_implies aut.accTrans q1)) 56 (aut.trans q1)` 57 >> Cases_on `(a, q2) ��� minimal_elements (aut.trans q1) rel` 58 >- (qexists_tac `(a, q2)` >> fs[] >> qunabbrev_tac `rel` 59 >> fs[rrestrict_def,rel_to_reln_def,trans_implies_def]) 60 >- (HO_MATCH_MP_TAC finite_prefix_po_has_minimal_path 61 >> qexists_tac `aut.trans q1` 62 >> `FINITE (aut.trans q1)` by (imp_res_tac GBA_FINITE_LEMM >> fs[]) 63 >> rpt strip_tac >> fs[] >> qunabbrev_tac `rel` 64 >- metis_tac[TRANS_IMPLIES_PO] 65 >- metis_tac[TRANS_IMPLIES_FINITE] 66 ) 67 ); 68 69val removeImplied_def = Define` 70 removeImplied accTrans trans q = 71 (trans q) DIFF {t | ?t'. ~(t = t') ��� t' ��� (trans q) 72 ��� trans_implies accTrans q t' t}`; 73 74val reduceTransSimpl_def = Define` 75 reduceTransSimpl (GBA s i t aT a) = 76 GBA s i (removeImplied aT t) 77 (IMAGE 78 (\s. {(e,a,e') | (e,a,e') ��� s ��� (a,e') ��� (removeImplied aT t) e }) 79 aT) 80 a`; 81 82val REDUCE_IS_VALID = store_thm 83 ("REDUCE_IS_VALID", 84 ``!aut. isValidGBA aut ==> isValidGBA (reduceTransSimpl aut)``, 85 fs[isValidGBA_def] >> rpt strip_tac >> Cases_on `aut` 86 >> fs[reduceTransSimpl_def] >> fs[removeImplied_def] >> metis_tac[] 87 ); 88 89val REDUCE_IS_CORRECT = store_thm 90 ("REDUCE_IS_CORRECT", 91 ``!aut. FINITE aut.states ��� FINITE aut.alphabet ��� isValidGBA aut 92 ==> (GBA_lang aut = GBA_lang (reduceTransSimpl aut))``, 93 fs[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 94 >> fs[GBA_lang_def, reduceTransSimpl_def] 95 >- (rename [���isGBARunFor aut r x���] >> qexists_tac `r` 96 >> `word_range x ��� (reduceTransSimpl aut).alphabet` 97 by (Cases_on `aut` >> fs[reduceTransSimpl_def]) 98 >> fs[isGBARunFor_def] >> Cases_on `r` 99 >> rename [`GBA_RUN f`] 100 >> `!i. f i ��� aut.states` by metis_tac[GBA_RUN_LEMM] 101 >> rpt strip_tac 102 >- (fs[isValidGBARunFor_def] >> rpt strip_tac 103 >> Cases_on `aut` >> fs[reduceTransSimpl_def] 104 >> rename [`GBA states init trans aT alph`] 105 >> imp_res_tac TRANS_IMPLIES_MIN >> fs[] 106 >> `���a. (a,f (i + 1)) ��� trans (f i) ��� at x i ��� a` by fs[] 107 >> first_x_assum (qspec_then `f (i+1)` mp_tac) >> rpt strip_tac 108 >> first_x_assum (qspec_then `f i` mp_tac) >> rpt strip_tac 109 >> first_x_assum (qspec_then `a` mp_tac) >> rpt strip_tac 110 >> POP_ASSUM mp_tac >> simp[] >> rpt strip_tac >> Cases_on `t` 111 >> rename[`(a_new,_) ��� minimal_elements (trans (f i)) _`] 112 >> qexists_tac `a_new` >> simp[removeImplied_def] 113 >> fs[minimal_elements_def,rrestrict_def,rel_to_reln_def] 114 >> fs[trans_implies_def] >> rw[] >> metis_tac[SUBSET_DEF] 115 ) 116 >- (`!TT. TT ��� (reduceTransSimpl aut).accTrans 117 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� TT 118 ��� (a, f (j+1)) ��� (reduceTransSimpl aut).trans (f j) 119 ��� at x j ��� a)` suffices_by metis_tac[GBA_ACC_LEMM] 120 >> `!TT. TT ��� aut.accTrans 121 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� TT 122 ��� (a, f (j+1)) ��� aut.trans (f j) 123 ��� at x j ��� a)` by metis_tac[GBA_ACC_LEMM] 124 >> rpt strip_tac 125 >> rpt strip_tac >> Cases_on `aut` >> fs[reduceTransSimpl_def] 126 >> rename [`GBA states init trans aT alph`, ���s ��� aT���] 127 >> first_x_assum (qspec_then `s` mp_tac) 128 >> simp[] >> rpt strip_tac 129 >> first_x_assum (qspec_then `i` mp_tac) >> rpt strip_tac 130 >> imp_res_tac TRANS_IMPLIES_MIN >> fs[] 131 >> first_x_assum (qspec_then `f (j+1)` mp_tac) >> rpt strip_tac 132 >> first_x_assum (qspec_then `f j` mp_tac) >> rpt strip_tac 133 >> first_x_assum (qspec_then `a` mp_tac) >> rpt strip_tac 134 >> POP_ASSUM mp_tac >> simp[] >> rpt strip_tac 135 >> rename [���(t, _, _) ��� rrestrict (rel_to_reln _) _���] 136 >> Cases_on `t` >> rename[`(a_new,r) ��� minimal_elements _ _`] 137 >> qexists_tac `a_new` >> qexists_tac `j` >> fs[removeImplied_def] 138 >> rpt strip_tac >> fs[minimal_elements_def,rrestrict_def] 139 >> fs[rel_to_reln_def,trans_implies_def] 140 >- (first_x_assum (qspec_then `(a,f(j+1))` mp_tac) >> fs[] 141 >> rpt strip_tac >> metis_tac[]) 142 >- metis_tac[] 143 >- metis_tac[] 144 >- metis_tac[SUBSET_DEF] 145 >- metis_tac[] 146 >- metis_tac[SUBSET_DEF] 147 ) 148 ) 149 >- (rename [���isGBARunFor (reduceTransSimpl aut) r x���] >> qexists_tac `r` 150 >> `word_range x ��� aut.alphabet` 151 by (Cases_on `aut` >> fs[reduceTransSimpl_def]) 152 >> fs[isGBARunFor_def] >> rpt strip_tac 153 >- (Cases_on `r` >> simp[isValidGBARunFor_def] >> rpt strip_tac 154 >> Cases_on `aut` >> fs[reduceTransSimpl_def,isValidGBARunFor_def] 155 >> first_x_assum (qspec_then `i` mp_tac) >> rpt strip_tac 156 >> fs[removeImplied_def] >> metis_tac[] 157 ) 158 >- (Cases_on `r` 159 >> `!TT. TT ��� (reduceTransSimpl aut).accTrans 160 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� TT 161 ��� (a, f (j+1)) ��� (reduceTransSimpl aut).trans (f j) 162 ��� at x j ��� a)` by metis_tac[GBA_ACC_LEMM] 163 >> `!TT. TT ��� aut.accTrans 164 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� TT 165 ��� (a, f (j+1)) ��� aut.trans (f j) 166 ��� at x j ��� a)` suffices_by metis_tac[GBA_ACC_LEMM] 167 >> rpt strip_tac 168 >> qabbrev_tac 169 `realTrans = {(e,a,e') | (a,e') ��� 170 (reduceTransSimpl aut).trans e }` 171 >> first_x_assum (qspec_then `TT ��� realTrans` mp_tac) 172 >> Cases_on `aut` >> fs[reduceTransSimpl_def] 173 >> qunabbrev_tac `realTrans` 174 >> simp[] >> rpt strip_tac >> fs[] 175 >> rename [���GBA states init trans aT alph���, 176 ���removeImplied aT trans���] 177 >> `���i. 178 ���a j. i ��� j ��� 179 ((f j,a,f (j + 1)) ��� TT 180 ��� (a,f (j + 1)) ��� removeImplied aT trans (f j)) 181 ��� (a,f (j + 1)) ��� removeImplied aT trans (f j) ��� at x j ��� a` 182 by ( 183 `���s. 184 (TT ��� {(e,a,e') | (a,e') ��� removeImplied aT trans e} = 185 {(e,a,e') | 186 (e,a,e') ��� s ��� (a,e') ��� removeImplied aT trans e}) ��� 187 s ��� aT` suffices_by fs[] 188 >> qexists_tac `TT` >> simp[SET_EQ_SUBSET,SUBSET_DEF] 189 >> rpt strip_tac >> metis_tac[] 190 ) 191 >> first_x_assum (qspec_then `i` mp_tac) >> rpt strip_tac 192 >> fs[removeImplied_def] >> metis_tac[] 193 ) 194 ) 195 ); 196 197(* 198 Remove unreachable states 199*) 200 201val removeStatesSimpl_def = Define` 202 removeStatesSimpl (GBA s i t aT alph) = 203 GBA 204 (s ��� reachableFromSetGBA (GBA s i t aT alph) i) 205 i 206 (��q. if q ��� (s ��� reachableFromSetGBA (GBA s i t aT alph) i) 207 then t q 208 else {} 209 ) 210 (IMAGE 211 (\T. {(e,a,e') | (e,a,e') ��� T 212 ��� e ��� (reachableFromSetGBA (GBA s i t aT alph) i)}) 213 aT) 214 alph`; 215 216val REDUCE_STATE_VALID = store_thm 217 ("REDUCE_STATE_VALID", 218 ``!aut. isValidGBA aut ==> isValidGBA (removeStatesSimpl aut)``, 219 fs[isValidGBA_def] >> rpt strip_tac >> Cases_on `aut` 220 >> fs[removeStatesSimpl_def,reachableFromSetGBA_def] 221 >> fs[SUBSET_DEF] >> rpt strip_tac 222 >- (simp[reachableFromGBA_def] >> metis_tac[RTC_REFL]) 223 >- metis_tac[] 224 >- (rename [���reachableFromGBA (GBA f f0 f1 f2 f3) x s���, ���x ��� f0���] 225 >> qexists_tac `x` >> fs[reachableFromGBA_def] 226 >> `stepGBA (GBA f f0 f1 f2 f3) s d` suffices_by metis_tac[RTC_CASES2] 227 >> simp[stepGBA_def] >> metis_tac[]) 228 >- metis_tac[] 229 >- metis_tac[] 230 >- metis_tac[] 231 >- metis_tac[] 232 ); 233 234(* val REACHABLE_LEMM = store_thm *) 235(* ("REACHABLE_LEMM", *) 236(* ``!gba. isValidGBA gba ==> *) 237(* (!q. q ��� gba.states ==>) *) 238(* ) *) 239 240val REDUCE_STATE_CORRECT = store_thm 241 ("REDUCE_STATE_CORRECT", 242 ``!aut. isValidGBA aut ==> 243 (GBA_lang aut = GBA_lang (removeStatesSimpl aut))``, 244 fs[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 245 >> fs[GBA_lang_def, removeStatesSimpl_def] 246 >- (qexists_tac `r` >> Cases_on `r` >> fs[isGBARunFor_def] 247 >> `!i. f i ��� reachableFromSetGBA aut aut.initial 248 ��� f i ��� aut.states` by ( 249 Induct_on `i` >> fs[reachableFromSetGBA_def] >> rpt strip_tac 250 >- (fs[isValidGBARunFor_def,reachableFromGBA_def] 251 >> qexists_tac `f 0` >> metis_tac[RTC_REFL]) 252 >- (fs[isValidGBA_def,isValidGBARunFor_def] 253 >> metis_tac[SUBSET_DEF]) 254 >- (fs[reachableFromGBA_def, isValidGBARunFor_def] 255 >> rename[`init ��� aut.initial`] 256 >> qexists_tac `init` >> fs[] 257 >> `(stepGBA aut) (f i) (f (SUC i))` suffices_by ( 258 rpt strip_tac >> metis_tac[RTC_CASES2] 259 ) 260 >> simp[stepGBA_def] >> metis_tac[SUC_ONE_ADD,ADD_COMM] 261 ) 262 >- (fs[isValidGBARunFor_def,isValidGBA_def] 263 >> metis_tac[SUBSET_DEF,SUC_ONE_ADD,ADD_COMM] 264 ) 265 ) 266 >> `word_range x ��� (removeStatesSimpl aut).alphabet` 267 by (Cases_on `aut` >> fs[removeStatesSimpl_def]) 268 >> rpt strip_tac >> fs[] 269 >- (fs[isValidGBARunFor_def] 270 >> Cases_on `aut` >> fs[removeStatesSimpl_def] 271 ) 272 >- (`!T. T ��� (removeStatesSimpl aut).accTrans 273 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� T 274 ��� (a, f (j+1)) ��� (removeStatesSimpl aut).trans (f j) 275 ��� at x j ��� a)` suffices_by metis_tac[GBA_ACC_LEMM] 276 >> `!T. T ��� aut.accTrans 277 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� T 278 ��� (a, f (j+1)) ��� aut.trans (f j) 279 ��� at x j ��� a)` by metis_tac[GBA_ACC_LEMM] 280 >> rpt strip_tac >> Cases_on `aut` 281 >> fs[removeStatesSimpl_def]) 282 ) 283 >- (`word_range x ��� aut.alphabet` 284 by (Cases_on `aut` >> fs[removeStatesSimpl_def]) 285 >> qexists_tac `r` >> fs[isGBARunFor_def] >> rpt strip_tac 286 >- (Cases_on `r` >> fs[isValidGBARunFor_def] >> rpt strip_tac 287 >> Cases_on `aut` >> fs[removeStatesSimpl_def] 288 >> metis_tac[MEMBER_NOT_EMPTY] 289 ) 290 >- (Cases_on `r` 291 >> `!i. f i ��� reachableFromSetGBA aut aut.initial 292 ��� f i ��� aut.states` by ( 293 Induct_on `i` >> fs[reachableFromSetGBA_def] >> rpt strip_tac 294 >- (fs[isValidGBARunFor_def,reachableFromGBA_def] 295 >> qexists_tac `f 0` >> Cases_on `aut` 296 >> fs[removeStatesSimpl_def] 297 ) 298 >- (Cases_on `aut` >> fs[removeStatesSimpl_def] 299 >> fs[isValidGBARunFor_def,isValidGBA_def] 300 >> fs[SUBSET_DEF] 301 ) 302 >- (fs[isValidGBARunFor_def,reachableFromGBA_def] 303 >> rename[`init ��� aut.initial`] 304 >> qexists_tac `init` >> fs[] 305 >> `(stepGBA aut) (f i) (f (SUC i))` suffices_by ( 306 rpt strip_tac >> metis_tac[RTC_CASES2] 307 ) 308 >> Cases_on `aut` >> fs[removeStatesSimpl_def] 309 >> simp[stepGBA_def] 310 >> metis_tac[SUC_ONE_ADD,ADD_COMM,MEMBER_NOT_EMPTY] 311 ) 312 >- (fs[isValidGBARunFor_def,isValidGBA_def] 313 >> Cases_on `aut` >> fs[removeStatesSimpl_def] 314 >> metis_tac[SUBSET_DEF,SUC_ONE_ADD,ADD_COMM, 315 MEMBER_NOT_EMPTY] 316 ) 317 ) 318 >> `!T. T ��� (removeStatesSimpl aut).accTrans 319 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� T 320 ��� (a, f (j+1)) ��� (removeStatesSimpl aut).trans (f j) 321 ��� at x j ��� a)` by metis_tac[GBA_ACC_LEMM] 322 >> `!T. T ��� aut.accTrans 323 ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� T 324 ��� (a, f (j+1)) ��� aut.trans (f j) 325 ��� at x j ��� a)` suffices_by metis_tac[GBA_ACC_LEMM] 326 >> rpt strip_tac >> fs[] 327 >> qabbrev_tac `realTrans = 328 {(e,a,e') | e ��� (reachableFromSetGBA aut aut.initial) 329 ��� (e,a,e') ��� T'}` 330 >> first_x_assum (qspec_then `realTrans` mp_tac) 331 >> Cases_on `aut` >> fs[removeStatesSimpl_def] 332 >> rpt strip_tac 333 >> `���i. 334 ���a j. i ��� j ��� 335 (f j,a,f (j + 1)) ��� realTrans ��� 336 (a,f (j + 1)) ��� f1 (f j) ��� at x j ��� a` by ( 337 `(realTrans = 338 {(e,a,e') | 339 (e,a,e') ��� T' ��� 340 e ��� reachableFromSetGBA (GBA f' f0 f1 f2 f3) f0}) 341 ��� T' ��� f2` suffices_by metis_tac[] 342 >> qunabbrev_tac `realTrans` >> simp[SET_EQ_SUBSET,SUBSET_DEF] 343 >> rpt strip_tac >> fs[] 344 ) 345 >> first_x_assum (qspec_then `i` mp_tac) >> rpt strip_tac 346 >> qexists_tac `a` >> qexists_tac `j` >> simp[] 347 >> qunabbrev_tac `realTrans` >> fs[] 348 ) 349 ) 350 ); 351 352(* 353 Merge equivalent states 354*) 355 356val replaceState_def = Define` 357 replaceState x_old x_new s = 358 if s = x_old then x_new else s`; 359 360val replaceStateSet_def = Define` 361 replaceStateSet x_old x_new set = 362 if x_old ��� set 363 then (set DIFF {x_old}) ��� {x_new} 364 else set`; 365 366val replaceAccTrans_def = Define` 367 replaceAccTrans x_old x_new aT = 368 IMAGE (\s. {(replaceState x_old x_new q1, a, replaceState x_old x_new q2) | 369 (q1,a,q2) ��� s}) aT`; 370 371val REPL_AT_LEMM = store_thm 372 ("REPL_AT_LEMM", 373 ``!aT t x y. 374 t ��� replaceAccTrans x y aT ==> 375 ?t2. t2 ��� aT ��� 376 !q1 a q2. (q1,a,q2) ��� t2 377 ==> (replaceState x y q1, a, replaceState x y q2) ��� t``, 378 rpt strip_tac >> fs[replaceAccTrans_def] >> metis_tac[] 379 ); 380 381val REPL_AT_LEMM2 = store_thm 382 ("REPL_AT_LEMM2", 383 ``!aT t x y. t ��� aT 384 ==> ?t2. t2 ��� (replaceAccTrans x y aT) 385 ��� !q1 a q2. (q1,a,q2) ��� t2 386 ==> ?q3 q4. (q1 = replaceState x y q3) ��� (q2 = replaceState x y q4) 387 ��� (q3,a,q4) ��� t``, 388 rpt strip_tac >> fs[replaceAccTrans_def] 389 >> qexists_tac 390 `{(replaceState x y q1, a, replaceState x y q2) | (q1,a,q2) ��� t}` 391 >> rpt strip_tac >> fs[] >> metis_tac[] 392 ); 393 394val equivalentStates_def = Define` 395 equivalentStates aT trans q1 q2 = 396 (trans q1 = trans q2) 397 ��� !a q3 T. ((a,q3) ��� trans q1) ��� T ��� aT 398 ==> ((q1,a,q3) ��� T = (q2,a,q3) ��� T)`; 399 400val mergeState_def = Define` 401 mergeState x y (GBA s i t aT alph) = 402 if equivalentStates aT t x y 403 then GBA 404 (s DIFF {x}) 405 (replaceStateSet x y i) 406 (\m. {(a,replaceState x y n) | (a,n) ��� t m}) 407 (replaceAccTrans x y aT) 408 alph 409 else (GBA s i t aT alph)`; 410 411val _ = export_theory(); 412 413(* (* val un_merged_run_def = Define` *) *) 414(* (* (un_merged_run word aT x_old x_new init trans f switch 0 = *) *) 415(* (* ((switch,if f 0 ��� init then f 0 else x_old))) *) *) 416(* (* ��� (un_merged_run word aT x_old x_new init trans f s (SUC i) = *) *) 417(* (* if ?a. (a, f (SUC i)) ��� trans (f i) ��� at word i ��� a *) *) 418(* (* ��� (!a2. (f i = x_new) ��� (a2,x_old) ��� trans (f i) *) *) 419(* (* ��� (at word i ��� a2) ==> switch ((f i), a2)) *) *) 420(* (* then (switch, f (SUC i)) *) *) 421(* (* else let a2 = @a. (a,x_old) ��� trans (f i) ��� (at word i ��� a) *) *) 422(* (* in ((��(q,a). if (q,a) = (f i, a2) *) *) 423(* (* then false else switch (q,a,q2)),x_old))`; *) *) 424 425(* (* val un_merged_run_def = Define` *) *) 426(* (* un_merged_run word aT x_old x_new init trans f i = *) *) 427(* (* if i = 0 *) *) 428(* (* then (if f 0 ��� init then f 0 else x_old) *) *) 429(* (* else (if ?a. (a,f i) ��� trans (f (i - 1)) ��� at word (i-1) ��� a *) *) 430(* (* ��� (!a2. (f i = x_new) ��� (a2,x_old) ��� trans (f (i-1)) *) *) 431(* (* ��� (at word (i-1) ��� a2) ==> *) *) 432(* (* !T. T ��� aT ==> *) *) 433(* (* ((f (i-1),a2,x_old) ��� T ==> (f (i-1),a,f i) ��� T)) *) *) 434(* (* then f i else x_old)`; *) *) 435 436(* val un_merged_run_def = Define` *) 437(* (un_merged_run_def w x y init trans f toggle 0 = *) 438(* if f 0 ��� init then f 0 else y *) 439(* ) *) 440(* ��� (un_merged_run_def w �� x y init trans f toogle i = *) 441(* if (�� i, f i) ��� trans (f (i-1)) *) 442(* then y *) 443 444(* then *) 445 446(* ) *) 447 448(* val MERGE_IS_CORRECT = store_thm *) 449(* ("MERGE_IS_CORRECT", *) 450(* ``!aut x y. isValidGBA aut ��� x ��� aut.states ��� y ��� aut.states *) 451(* ��� ~(x = y) ��� equivalentStates aut.accTrans aut.trans x y *) 452(* ==> (GBA_lang aut = GBA_lang (mergeState x y aut))``, *) 453(* fs[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac *) 454(* >> fs[GBA_lang_def,mergeState_def] *) 455(* >- (rename[`word_range w ��� _`] *) 456(* >> `word_range w ��� (mergeState x y aut).alphabet` *) 457(* by (Cases_on `aut` >> fs[mergeState_def] *) 458(* >> Cases_on `equivalentStates f2 f1 x y` *) 459(* >> simp[]) *) 460(* (* >> Cases_on `equivalentStates aut.accTrans aut.trans x y` *) *) 461(* (* >- ( *) *) 462(* Cases_on `aut` >> rename[`GBA states init t aT alph`] *) 463(* >> fs[] *) 464(* (* >> qabbrev_tac `s_new = *) *) 465(* (* @p. p ��� states ��� ~(p = q) ��� equivalentStates aT t p q` *) *) 466(* (* >> `s_new ��� states ��� ~(s_new = q) ��� equivalentStates aT t s_new q` *) *) 467(* (* by (qunabbrev_tac `s_new` >> metis_tac[]) *) *) 468(* >> Cases_on `r` *) 469(* >> qexists_tac `GBA_RUN (\i. replaceState x y (f i))` *) 470(* >> fs[isGBARunFor_def,mergeState_def] >> rpt strip_tac *) 471(* >> qabbrev_tac `newGBA = *) 472(* GBA (states DIFF {x}) (replaceStateSet x y init) *) 473(* (��m. {(a,replaceState x y n) | (a,n) ��� t m}) *) 474(* (replaceAccTrans x y aT) alph` *) 475(* >- ((* `isValidGBARunFor newGBA *) *) 476(* (* (GBA_RUN (��i. replaceState q s_new (f i))) x` *) *) 477(* (* suffices_by metis_tac[] *) *) 478(* simp[isValidGBARunFor_def] >> rpt strip_tac *) 479(* >- (qunabbrev_tac `newGBA` *) 480(* >> simp[replaceState_def,replaceStateSet_def] *) 481(* >> Cases_on `f 0 = x` >> simp[] *) 482(* >- fs[isValidGBARunFor_def] *) 483(* >- (Cases_on `x ��� init` >> fs[isValidGBARunFor_def]) *) 484(* ) *) 485(* >- (fs[isValidGBARunFor_def] *) 486(* >> `���a. (a,f (i + 1)) ��� t (f i) ��� at w i ��� a` *) 487(* by metis_tac[] *) 488(* >> qexists_tac `a` >> simp[replaceState_def] *) 489(* >> qunabbrev_tac `newGBA` >> simp[replaceState_def] *) 490(* >> qexists_tac `f (i + 1)` >> simp[] *) 491(* >> Cases_on `f i = x` >> fs[equivalentStates_def] *) 492(* >> metis_tac[] *) 493(* ) *) 494(* ) *) 495(* >- (qabbrev_tac `newRun = ��i. replaceState x y (f i)` *) 496(* (* >> `isAcceptingGBARunFor newGBA (GBA_RUN newRun) x` *) *) 497(* (* suffices_by metis_tac[] *) *) 498(* >> `!T. T ��� newGBA.accTrans *) 499(* ==> (!i. ?a j. i <= j ��� (newRun j, a, newRun (j+1)) ��� T *) 500(* ��� (a, newRun (j+1)) ��� newGBA.trans (newRun j) *) 501(* ��� at w j ��� a)` suffices_by metis_tac[GBA_ACC_LEMM] *) 502(* >> qabbrev_tac `aut = GBA states init t aT alph` *) 503(* >> `!T. T ��� aut.accTrans *) 504(* ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� T *) 505(* ��� (a, f (j+1)) ��� aut.trans (f j) *) 506(* ��� at w j ��� a)` by metis_tac[GBA_ACC_LEMM] *) 507(* >> rpt strip_tac *) 508(* >> `?t2. t2 ��� aut.accTrans *) 509(* ��� !q1 a q2. (q1,a,q2) ��� t2 ==> *) 510(* (replaceState x y q1, a, replaceState x y q2) ��� T'` *) 511(* by (qunabbrev_tac `newGBA` >> fs[] *) 512(* >> imp_res_tac REPL_AT_LEMM >> qunabbrev_tac `aut` *) 513(* >> simp[] >> metis_tac[]) *) 514(* >> first_x_assum (qspec_then `t2` mp_tac) *) 515(* >> simp[] >> rpt strip_tac *) 516(* >> first_x_assum (qspec_then `i` mp_tac) >> rpt strip_tac *) 517(* >> qexists_tac `a` >> qexists_tac `j` >> fs[] *) 518(* >> qunabbrev_tac `newRun` >> simp[replaceState_def] *) 519(* >> Cases_on `f j = x` >> Cases_on `f (j + 1) = x` *) 520(* >> qunabbrev_tac `aut` >> fs[equivalentStates_def] *) 521(* >> rpt strip_tac >> qunabbrev_tac `newGBA` >> simp[] *) 522(* >> metis_tac[replaceState_def] *) 523(* ) *) 524(* ) *) 525(* >- (qexists_tac `r` >> simp[isGBARunFor_def] >> strip_tac *) 526(* >> Cases_on `aut` >> simp[mergeState_def] *) 527(* >- (qabbrev_tac `aut = GBA f f0 f1 f2 f3` *) 528(* >> `isValidGBARunFor aut r x` suffices_by ( *) 529(* qunabbrev_tac `aut` >> fs[] >> metis_tac[] *) 530(* ) *) 531(* >> fs[isGBARunFor_def] *) 532(* ) *) 533(* >- (qabbrev_tac `aut = GBA f f0 f1 f2 f3` *) 534(* >> `isAcceptingGBARunFor aut r x` suffices_by ( *) 535(* qunabbrev_tac `aut` >> fs[] >> metis_tac[] *) 536(* ) *) 537(* >> fs[isGBARunFor_def] *) 538(* ) *) 539(* ) *) 540(* ) *) 541(* >- (`word_range x ��� aut.alphabet` by ( *) 542(* Cases_on `aut` >> fs[mergeState_def] >> POP_ASSUM mp_tac *) 543(* >> Cases_on `���q'. q' ��� f ��� q' ��� q ��� equivalentStates f2 f1 q' q` *) 544(* >> simp[]) *) 545(* >> Cases_on `���q'. q' ��� aut.states ��� q' ��� q *) 546(* ��� equivalentStates aut.accTrans aut.trans q' q` *) 547(* >> rpt strip_tac *) 548(* >- (fs[isGBARunFor_def,isValidGBARunFor_def] >> Cases_on `aut` *) 549(* >> rename[`GBA states i t aT alph`] *) 550(* >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 551(* >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 552(* >> RULE_ASSUM_TAC(SIMP_RULE (srw_ss())[mergeState_def]) *) 553(* >> rpt strip_tac *) 554(* >> qabbrev_tac *) 555(* `s_new = @p. p ��� states ��� p ��� q ��� equivalentStates aT t p q` *) 556(* >> `s_new ��� states ��� ~(s_new = q) ��� equivalentStates aT t s_new q` *) 557(* by (qunabbrev_tac `s_new` >> fs[] >> metis_tac[]) *) 558(* >> fs[] *) 559(* >> qabbrev_tac *) 560(* `newGBA = GBA (states DIFF {q}) (replaceStateSet q s_new i) *) 561(* (��m. {(a,replaceState q s_new n) | (a,n) ��� t m}) *) 562(* (replaceAccTrans q s_new aT) alph` *) 563(* >> `isValidGBARunFor newGBA r x` by metis_tac[] *) 564(* >> POP_ASSUM mp_tac >> Cases_on `r` >> simp[isValidGBARunFor_def] *) 565(* >> rpt strip_tac *) 566(* >> qexists_tac `GBA_RUN (un_merged_run x aT q s_new i t f)` *) 567(* >> rpt strip_tac *) 568(* >- (simp[isValidGBARunFor_def,un_merged_run_def] >> rpt strip_tac *) 569(* >- (Cases_on `f 0 ��� i` >> fs[] >> qunabbrev_tac `newGBA` *) 570(* >> fs[replaceStateSet_def] >> metis_tac[] *) 571(* ) *) 572(* >- (rename[`n = 0`] *) 573(* >> `���a. (a,f (n + 1)) ��� newGBA.trans (f n) ��� at x n ��� a` *) 574(* by metis_tac[] *) 575(* >> rpt strip_tac *) 576(* >> Cases_on ` *) 577(* ���a. (a,f (n + 1)) ��� t (f n) ��� at x n ��� a ��� *) 578(* ���a2. *) 579(* (f (n + 1) = s_new) ��� (a2,q) ��� t (f n) *) 580(* ��� at x n ��� a2 ��� *) 581(* ���T. T ��� aT ��� (f n,a2,q) ��� T ��� (f n,a,s_new) ��� T` *) 582(* >> Cases_on `n = 0` >> simp[] *) 583(* >- (Cases_on `f 0 ��� i` >> fs[] *) 584(* >- metis_tac[] *) 585(* >- (qunabbrev_tac `newGBA` >> fs[replaceStateSet_def] *) 586(* >> `f 0 = s_new` by (Cases_on `q ��� i` >> fs[]) *) 587(* >> fs[equivalentStates_def] >> metis_tac[]) *) 588(* ) *) 589(* >- (Cases_on *) 590(* `���a. (a,f n) ��� t (f (n ��� 1)) ��� at x (n ��� 1) ��� a ��� *) 591(* ���a2. *) 592(* (f n = s_new) ��� (a2,q) ��� t (f (n ��� 1)) *) 593(* ��� at x (n ��� 1) ��� a2 ��� ���T. T ��� aT ��� *) 594(* (f (n ��� 1),a2,q) ��� T ��� (f (n ��� 1),a,s_new) ��� T` *) 595(* >- metis_tac[] *) 596(* >- (simp[] >> qunabbrev_tac `newGBA` *) 597(* >> fs[replaceStateSet_def,replaceState_def] *) 598(* >> `f n = s_new` by ( *) 599(* first_x_assum (qspec_then `n-1` mp_tac) >> simp[] *) 600(* >> rpt strip_tac >> metis_tac[]) *) 601(* >> fs[equivalentStates_def] >> rw[] *) 602(* >> metis_tac[]) *) 603(* ) *) 604(* >- (Cases_on `f 0 ��� i` >> fs[] *) 605(* >- (qunabbrev_tac `newGBA` >> fs[replaceStateSet_def] *) 606(* >> fs[replaceState_def] >> Cases_on `n' = q` *) 607(* >> metis_tac[]) *) 608(* >- (qunabbrev_tac `newGBA` >> fs[replaceStateSet_def] *) 609(* >> fs[replaceState_def,equivalentStates_def] *) 610(* >> `f 0 = s_new` by (Cases_on `q ��� i` >> fs[]) *) 611(* >> Cases_on `n' = q` *) 612(* >> metis_tac[]) *) 613(* ) *) 614(* >- (Cases_on *) 615(* `���a. (a,f n) ��� t (f (n ��� 1)) ��� at x (n ��� 1) ��� a ��� *) 616(* ���a2. *) 617(* (f n = s_new) ��� (a2,q) ��� t (f (n ��� 1)) *) 618(* ��� at x (n ��� 1) ��� a2 ��� ���T. T ��� aT ��� *) 619(* (f (n ��� 1),a2,q) ��� T ��� (f (n ��� 1),a,s_new) ��� T` *) 620(* >- (simp[] >> qunabbrev_tac `newGBA` *) 621(* >> fs[replaceStateSet_def,replaceState_def] *) 622(* >> Cases_on `n' = q` >> fs[] >> metis_tac[] *) 623(* ) *) 624(* >- (simp[] >> fs[] >> qunabbrev_tac `newGBA` *) 625(* >> fs[replaceStateSet_def,replaceState_def] *) 626(* >> `f n = s_new` by ( *) 627(* first_x_assum (qspec_then `n-1` mp_tac) *) 628(* >> simp[] >> rpt strip_tac >> metis_tac[]) *) 629(* >> fs[equivalentStates_def] >> rw[] *) 630(* >> metis_tac[]) *) 631(* ) *) 632(* ) *) 633(* ) *) 634(* >- (qabbrev_tac `newRun = un_merged_run x aT q s_new i t f` *) 635(* >> qabbrev_tac `aut = GBA states i t aT alph` *) 636(* >> `!T. T ��� aut.accTrans *) 637(* ==> (!i. ?a j. i <= j ��� (newRun j, a, newRun (j+1)) ��� T *) 638(* ��� (a, newRun (j+1)) ��� aut.trans (newRun j) *) 639(* ��� at x j ��� a)` suffices_by metis_tac[GBA_ACC_LEMM] *) 640(* >> `isAcceptingGBARunFor newGBA (GBA_RUN f) x` by ( *) 641(* qunabbrev_tac `aut` >> fs[mergeState_def] *) 642(* >> metis_tac[]) *) 643(* >> `!T. T ��� newGBA.accTrans *) 644(* ==> (!i. ?a j. i <= j ��� (f j, a, f (j+1)) ��� T *) 645(* ��� (a, f (j+1)) ��� newGBA.trans (f j) *) 646(* ��� at x j ��� a)` by metis_tac[GBA_ACC_LEMM] *) 647(* >> rpt strip_tac *) 648(* >> `���t2. t2 ��� replaceAccTrans q s_new aT ��� *) 649(* ���q1 a q2. *) 650(* (q1,a,q2) ��� t2 ��� *) 651(* ?q3 q4. (q1 = replaceState q s_new q3) *) 652(* ��� (q2 = replaceState q s_new q4) *) 653(* ��� ((q3,a,q4) ��� T')` by ( *) 654(* imp_res_tac REPL_AT_LEMM2 >> qunabbrev_tac `aut` *) 655(* >> fs[] >> metis_tac[]) *) 656(* >> first_x_assum (qspec_then `t2` mp_tac) *) 657(* >> `t2 ��� newGBA.accTrans` *) 658(* by (qunabbrev_tac `newGBA` >> fs[]) *) 659(* >> simp[] >> rpt strip_tac *) 660(* >> first_x_assum (qspec_then `i'` mp_tac) >> rpt strip_tac *) 661(* >> rename[`n <= j`] >> qexists_tac `a` >> qexists_tac `j` *) 662(* >> fs[] >> strip_tac *) 663(* >- (`!p. (f p, a, f (p+1)) ��� t2 *) 664(* ==> (newRun p,a,newRun (p+1)) ��� T'` by ( *) 665(* Induct_on `p` >> fs[] >> rpt strip_tac *) 666(* >> qunabbrev_tac `newRun` >> fs[un_merged_run_def] *) 667(* >- (Cases_on `f 0 ��� i` >> simp[] *) 668(* >- (Cases_on `���a'. (a',f 1) ��� t (f 0) ��� at x 0 ��� a' *) 669(* ��� ���a2. (f 1 = s_new) ��� (a2,q) ��� t (f 0) *) 670(* ��� at x 0 ��� a2 ��� ���T. T ��� aT ��� *) 671(* (f 0,a2,q) ��� T ��� (f 0,a',s_new) ��� T` *) 672(* >- (simp[] >> fs[] >> ) *) 673 674(* (* ) *) *) 675 676 677(* (* ) *) *) 678 679 680(* (* qunabbrev_tac `newRun` >> simp[un_merged_run_def] *) *) 681(* (* >> *) *) 682 683 684 685(* (* ) *) *) 686 687 688 689 690 691(* (* >> `!j. (newRun j = f j) \/ (newRun j = q)` by ( *) *) 692(* (* strip_tac >> qunabbrev_tac `newRun` *) *) 693(* (* >> fs[un_merged_run_def] >> metis_tac[] *) *) 694(* (* ) *) *) 695(* (* >> strip_tac *) *) 696(* (* >- (first_x_assum (qspec_then `f j` mp_tac) *) *) 697(* (* >> strip_tac >> first_x_assum (qspec_then `a` mp_tac) *) *) 698(* (* >> strip_tac *) *) 699(* (* >> first_x_assum (qspec_then `f (j+1)` mp_tac) *) *) 700(* (* >> simp[] >> strip_tac *) *) 701(* (* >> `q3 = newRun j` by ( *) *) 702(* (* qunabbrev_tac `newRun` >> fs[un_merged_run_def] *) *) 703(* (* >> fs[replaceState_def] >> Cases_on `q3=q` >> fs[] *) *) 704(* (* >> Cases_on `j=0` >> simp[] *) *) 705 706(* (* ) *) *) 707 708(* (* >> Cases_on `q3 = q` *) *) 709(* (* >> Cases_on `q4 = q` >> fs[replaceState_def] *) *) 710(* (* >- (`(s_new,a,s_new) ��� T'` suffices_by ( *) *) 711(* (* qunabbrev_tac `newRun` >> fs[un_merged_run_def] *) *) 712(* (* >> simp[] >> strip_tac >> *) *) 713 714(* (* )) *) *) 715 716 717(* (* >- (qunabbrev_tac `newRun` >> qunabbrev_tac `aut` *) *) 718(* (* >> simp[un_merged_run_def] >> fs[replaceState_def] *) *) 719(* (* >> fs[equivalentStates_def] *) *) 720(* (* >> Cases_on `~(f j = s_new)` >> simp[] *) *) 721(* (* >- (qunabbrev_tac `newGBA` >> fs[] *) *) 722(* (* >> first_x_assum (qspec_then `f j` mp_tac) *) *) 723(* (* >> strip_tac >> first_x_assum (qspec_then `a` mp_tac) *) *) 724(* (* >> strip_tac >> first_x_assum (qspec_then `f (j+1)` mp_tac) *) *) 725(* (* >> simp[] >> rpt strip_tac >> Cases_on `q3 = q` *) *) 726(* (* >> fs[] >> rw[] *) *) 727(* (* >- (Cases_on `n' = q` >> fs[] *) *) 728(* (* >- (fs[replaceAccTrans_def,replaceState_def] *) *) 729(* (* >> *) *) 730 731(* (* ) *) *) 732(* (* ) *) *) 733 734(* (* >> Cases_on `j = 0` >> simp[] *) *) 735(* (* >- (Cases_on `f 0 ��� i` >> fs[] *) *) 736(* (* >- (Cases_on `q3 = q` >> Cases_on `q4 = q` *) *) 737(* (* >> simp[] >> rw[] *) *) 738(* (* >- (Cases_on `n' = q` >> rw[] *) *) 739(* (* >- (`(f 0,a,n') ��� T'` by metis_tac[] *) *) 740(* (* >> metis_tac[] *) *) 741(* (* ) *) *) 742(* (* ) *) *) 743(* (* ) *) *) 744(* (* ) *) *) 745(* (* >- (simp[] >> Cases_on `f 0 ��� i` >> simp[] *) *) 746(* (* >- ( *) *) 747 748(* (* ) *) *) 749(* (* ) *) *) 750(* (* ) *) *) 751 752(* (* >> simp[] >> first_x_assum (qspec_then `f j` mp_tac) *) *) 753(* (* >> strip_tac >> first_x_assum (qspec_then `a` mp_tac) *) *) 754(* (* >> strip_tac >> first_x_assum (qspec_then `f (j+1)` mp_tac) *) *) 755(* (* >> simp[] >> strip_tac >> fs[replaceState_def] *) *) 756(* (* >> fs[equivalentStates_def] *) *) 757(* (* >> Cases_on `~(f j = q)` >> simp[] *) *) 758(* (* >- (Cases_on `j = 0` >> simp[] >> *) *) 759 760 761(* (* ) *) *) 762 763 764(* (* >> Cases_on `q3 = q` >> Cases_on `q4 = q` >> simp[] *) *) 765(* (* >- (`(a,q) ��� t s_new` by ( *) *) 766(* (* fs[isValidGBA_def] *) *) 767 768(* (* ) *) *) 769 770 771 772 773(* (* fs[equivalentStates_def] *) *) 774(* (* >> Cases_on ) *) *) 775 776 777(* (* >> Cases_on `j = 0` *) *) 778(* (* >> Cases_on `���a. (a,f j) ��� t (f (j ��� 1)) ��� at x (j ��� 1) ��� a` *) *) 779(* (* >> Cases_on `���a'. (a',f (j+1)) ��� t (f j) ��� at x j ��� a'` *) *) 780(* (* >> rw[] >> fs[replaceState_def] >> *) *) 781(* (* >- () *) *) 782(* (* ) *) *) 783(* (* ) *) *) 784(* (* ) *) *) 785