1open HolKernel Parse bossLib boolLib pred_setTheory relationTheory arithmeticTheory prim_recTheory pairTheory set_relationTheory whileTheory 2 3open generalHelpersTheory ltlTheory wordTheory alterATheory 4 5val _ = new_theory "ltl2waa" 6 7(* 8 Defining the translation from LTL to WAA 9 *) 10 11val initForms_def = Define `(initForms f = tempDNF f)`; 12 13val finalForms_def = Define 14 `finalForms f = {U f1 f2 | (U f1 f2) ��� tempSubForms f}`; 15 16(* 17 transition function of the automaton 18*) 19 20val trans_def = Define 21 `(trans �� (VAR a) = {((char �� a), {})}) 22 /\ (trans �� (N_VAR a) = {�� DIFF (char �� a), {}}) 23 /\ (trans �� (CONJ f1 f2) = d_conj (trans �� f1) (trans �� f2)) 24 /\ (trans �� (DISJ f1 f2) = (trans �� f1) ��� (trans �� f2)) 25 /\ (trans �� (X f) = \s. ?e. (s = (��, e)) /\ (e ��� tempDNF f)) 26 /\ (trans �� (U f1 f2) = (trans �� f2) ��� (d_conj (trans �� f1) {(��,{U f1 f2})})) 27 /\ (trans �� (R f1 f2) = d_conj (trans �� f2) ((trans �� f1) ��� {(��,{R f1 f2})}))`; 28 29val TRANS_ALPH_LEMM = store_thm 30 ("TRANS_ALPH_LEMM", 31 ``!a e f ��. (a,e) ��� trans �� f ==> a ��� ��``, 32 Induct_on `f` >> fs[trans_def, char_def, SUBSET_DEF,d_conj_def] 33 >> rpt strip_tac >> metis_tac[IN_INTER] 34 ); 35 36val TRANS_TEMPDNF_LEMM = store_thm 37 ("TRANS_TEMPDNF_LEMM", 38 ���!a s �� f. 39 ((a,s) ��� trans �� f) ==> 40 ?e t a'. (s = BIGUNION t) /\ (e ��� tempDNF f) 41 /\ (a = BIGINTER a') 42 /\ (!t'. t' ��� t ==> 43 ?q a''. a'' ��� a' /\ q ��� e /\ (a'',t') ��� trans �� q) 44 /\ !q. q ��� e ==> 45 ?t' a''. a'' ��� a' /\ (t' ��� t) /\ (a'',t') ��� trans �� q���, 46 Induct_on `f` >> fs[trans_def, tempDNF_def,BIGUNION,SUBSET_DEF] >> rpt strip_tac 47 >- (qexists_tac `{{}}` >> qexists_tac `{char �� a}` >> fs[]) 48 >- (qexists_tac `{{}}` >> qexists_tac `{�� DIFF char �� a}` >> fs[]) 49 >- (dsimp[] >> metis_tac[]) 50 >- (dsimp[] >> metis_tac[]) 51 >- (fs[d_conj_def] >> 52 rename [���(a1,e1) ��� trans �� f1���, ���a = a1 ��� a2���, ���(a2,e2) ��� trans �� f2���] 53 >> `���e t a'. 54 (e1 = {x | ���s. s ��� t ��� x ��� s}) ��� e ��� tempDNF f1 ��� 55 (a1 = BIGINTER a') ��� 56 (���t'. 57 t' ��� t ��� ���q a''. a'' ��� a' ��� q ��� e ��� (a'',t') ��� trans �� q) ��� 58 ���q. q ��� e ��� ���t' a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans �� q` 59 by metis_tac[] 60 >> `���e' t' a''. 61 (e2 = {x | ���s. s ��� t' ��� x ��� s}) ��� e' ��� tempDNF f2 ��� 62 (a2 = BIGINTER a'') ��� 63 (���tt. 64 tt ��� t' ��� ���q aa. aa ��� a'' ��� q ��� e' ��� (aa,tt) ��� trans �� q) ��� 65 ���q. q ��� e' ��� ���tt aa. aa ��� a'' ��� tt ��� t' ��� (aa,tt) ��� trans �� q` 66 by metis_tac[] 67 >> qexists_tac `e ��� e'` >> fs[] >> qexists_tac `t ��� t'` 68 >> dsimp[] >> fs[] >> rpt strip_tac 69 >> qexists_tac `a' ��� a''` 70 >> qexists_tac `e` >> qexists_tac `e'` >> fs[] 71 >> fs[UNION_DEF] >> rpt strip_tac 72 >- (rename1 ���t'' ��� t��� >> 73 `���q a''. a'' ��� a' ��� q ��� e ��� (a'',t'') ��� trans �� q` 74 by metis_tac[] >> 75 `���q a'''. 76 ((a''' ��� a') ��� (a''' ��� a'')) ��� q ��� e ��� 77 (a''',t'') ��� trans �� q` suffices_by metis_tac[] 78 >> qexists_tac `q` >> qexists_tac `a'''` >> fs[]) 79 >- (rename1 ���t'' ��� t'��� >> 80 `���q a'''. a''' ��� a'' ��� q ��� e' ��� (a''',t'') ��� trans �� q` 81 by metis_tac[] 82 >> `���q a'''. 83 ((a''' ��� a') ��� (a''' ��� a'')) ��� q ��� e' ��� 84 (a''',t'') ��� trans �� q` suffices_by metis_tac[] 85 >> qexists_tac `q` >> qexists_tac `a'''` >> fs[] 86 ) 87 >- (`���t' a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans �� q` by metis_tac[] 88 >> `(���t'' a'''. 89 (a''' ��� a' ��� a''' ��� a'') ��� t'' ��� t ��� (a''',t'') ��� trans �� q)` 90 suffices_by metis_tac[] 91 >> qexists_tac `t''` >> qexists_tac `a'''` >> fs[] 92 ) 93 >- (`���t'' a'''. a''' ��� a'' ��� t'' ��� t' ��� (a''',t'') ��� trans �� q` by metis_tac[] 94 >> `(���t'' a'''. 95 (a''' ��� a' ��� a''' ��� a'') ��� t'' ��� t' ��� (a''',t'') ��� trans �� q)` 96 suffices_by metis_tac[] 97 >> qexists_tac `t''` >> qexists_tac `a'''` >> fs[]) 98 ) 99 >- (qexists_tac `{s}` >> qexists_tac `{a}` >> fs[]) 100 >- (qexists_tac `{s}` >> qexists_tac `{a}` >> fs[]) 101 >- (fs[d_conj_def] >> qexists_tac `{s}` >> qexists_tac `{a1 ��� ��}` 102 >> fs[] >> rpt strip_tac 103 >- (fs[UNION_DEF]) 104 >- (`���a1' e1'. 105 ((a1 ��� �� = a1' ��� ��) ��� (e1 ��� {U f f'} = e1' ��� {U f f'})) ��� 106 (a1',e1') ��� trans �� f` suffices_by metis_tac[] 107 >> qexists_tac `a1` >> qexists_tac `e1` >> fs[]) 108 ) 109 >- (fs[d_conj_def] 110 >> qexists_tac `{s}` >> qexists_tac `{a1 ��� a2}` 111 >> fs[] >> rpt strip_tac 112 >- (fs[UNION_DEF]) 113 >- (qexists_tac `a1` >> qexists_tac `a2` >> qexists_tac `e1` 114 >> qexists_tac `e2` >> fs[]) 115 >- (fs[UNION_DEF]) 116 >- (qexists_tac `a1` >> qexists_tac `a2` >> qexists_tac `e1` 117 >> qexists_tac `e2` >> fs[] 118 ) 119 ) 120 ); 121 122val TRANS_REACHES_SUBFORMS = store_thm 123 ("TRANS_REACHES_SUBFORMS", 124 ``!s a d ��. ((a,d) ��� trans �� s) 125 ==> !q. (q ��� d) ==> ((q,s) ��� TSF)``, 126 `!s a d ��. ((a,d) ��� trans �� s) 127 ==> (d ��� tempSubForms s)` suffices_by metis_tac[SUBSET_DEF,TSF_def,IN_DEF] 128 >> Induct_on `s` >> (rpt strip_tac >> fs[trans_def]) 129 >- (`!s s'. tempSubForms s ��� tempSubForms (DISJ s s')` 130 by metis_tac[tempSubForms_def,SUBSET_UNION] 131 >> `d ��� (tempSubForms s)` by metis_tac[] 132 >> fs[SUBSET_DEF] >> rpt strip_tac) 133 >- (`!s s'. tempSubForms s ��� tempSubForms (DISJ s' s)` 134 by metis_tac[tempSubForms_def,SUBSET_UNION] 135 >> `d ��� (tempSubForms s')` by metis_tac[] 136 >> fs[SUBSET_DEF] >> rpt strip_tac 137 ) 138 >- (fs[d_conj_def] 139 >> `e1 ��� tempSubForms s` by metis_tac[] 140 >> `e2 ��� tempSubForms s'` by metis_tac[] 141 >> `!s s'. tempSubForms s ��� tempSubForms (CONJ s' s)` 142 by metis_tac[tempSubForms_def, SUBSET_UNION] 143 >> `!s s'. tempSubForms s' ��� tempSubForms (CONJ s' s)` 144 by metis_tac[tempSubForms_def, SUBSET_UNION] 145 >> fs[SUBSET_DEF] >> rpt strip_tac 146 ) 147 >- (`d ��� tempSubForms s` by metis_tac[TEMPDNF_TEMPSUBF] 148 >> `d ��� tempSubForms (X s)` 149 suffices_by metis_tac[SUBSET_UNION, SUBSET_TRANS] 150 >> `!s. tempSubForms s ��� tempSubForms (X s)` by rw[tempSubForms_def] 151 >> metis_tac[SUBSET_TRANS]) 152 >- (`!s s'. tempSubForms s' ��� tempSubForms (U s s')` 153 by metis_tac[tempSubForms_def,SUBSET_UNION] 154 >> `tempSubForms s' ��� tempSubForms (U s s')` by metis_tac[] 155 >> `d ��� (tempSubForms s')` by metis_tac[] 156 >> fs[SUBSET_DEF] >> rpt strip_tac 157 ) 158 >- (fs[d_conj_def] >> `e1 ��� (tempSubForms s)` by metis_tac[] 159 >> `!s s'. tempSubForms (U s s') = {U s s'} ��� tempSubForms s ��� tempSubForms s'` 160 by rw[tempSubForms_def] 161 >> `tempSubForms (U s s') = {U s s'} ��� tempSubForms s ��� tempSubForms s'` 162 by metis_tac[] 163 >> fs[SUBSET_DEF] >> rpt strip_tac 164 ) 165 >- (fs[d_conj_def] >> `e1 ��� (tempSubForms s')` by metis_tac[] 166 >> `!s s'. tempSubForms (R s s') = {R s s'} ��� tempSubForms s ��� tempSubForms s'` 167 by rw[tempSubForms_def] 168 >- (`e2 ��� (tempSubForms s)` by metis_tac[] 169 >> `tempSubForms (R s s') = {R s s'} ��� tempSubForms s ��� tempSubForms s'` 170 by metis_tac[] 171 >> fs[SUBSET_DEF] >> rpt strip_tac 172 ) 173 >- (fs[SUBSET_DEF] >> rpt strip_tac) 174 ) 175 ); 176 177 178(* 179 Defining the automaton 180*) 181 182val ltl2vwaa_free_alph_def = Define 183 `ltl2vwaa_free_alph �� f = 184 ALTER_A 185 (tempSubForms f) 186 �� 187 (trans ��) 188 (initForms f) 189 (finalForms f)`; 190 191val ltl2vwaa_def = Define `ltl2vwaa f = ltl2vwaa_free_alph (POW (props f)) f`; 192 193val LTL2WAA_ISVALID = store_thm 194 ("LTL2WAA_ISVALID", 195 ``!f. isValidAlterA (ltl2vwaa f)``, 196 strip_tac >> fs[isValidAlterA_def, ltl2vwaa_def, ltl2vwaa_free_alph_def] 197 >> rpt strip_tac 198 >- (fs[initForms_def, tempSubForms_def, POW_DEF, SUBSET_DEF] 199 >> rpt strip_tac >> `x ��� tempSubForms f` by metis_tac[TEMPDNF_TEMPSUBF] 200 >> fs[SUBSET_DEF]) 201 >- (fs[finalForms_def, tempSubForms_def, POW_DEF, SUBSET_DEF] 202 >> rpt strip_tac >> fs[]) 203 >- (`!q. (q ��� d) ==> ((q,s) ��� TSF)` by metis_tac[TRANS_REACHES_SUBFORMS] 204 >> `!q. (q ��� d) ==> ((q,f) ��� TSF)` suffices_by metis_tac[SUBSET_DEF,TSF_def,IN_DEF] 205 >> `(s,f) ��� TSF` by metis_tac[TSF_def,IN_DEF] 206 >> rpt strip_tac 207 >> `(q,s) ��� TSF` by metis_tac[] 208 >> metis_tac[TSF_TRANS_LEMM,transitive_def,IN_DEF] 209 ) 210 >- (`!s' a' d'. s' ��� subForms f ��� (a',d') ��� trans (POW (props f)) s' 211 ==> a' ��� (POW (props f))` suffices_by metis_tac[TSF_IMPL_SF] 212 >> Induct_on `s'` >> fs[trans_def,char_def,SUBSET_DEF] >> rpt strip_tac 213 >> fs[d_conj_def] 214 >> metis_tac[subForms_def, IN_UNION, SUBFORMS_REFL, SUBFORMS_TRANS,IN_INTER] 215 ) 216 ); 217 218val LTL2WAA_ISWEAK_LEMM = store_thm 219 ("LTL2WAA_ISWEAK_LEMM", 220 ``!f g. isVeryWeakAlterA (ltl2vwaa_free_alph (POW (props f)) g)``, 221 rpt strip_tac 222 >> fs[isVeryWeakAlterA_def, isVeryWeakWithOrder_def, ltl2vwaa_def, ltl2vwaa_free_alph_def] 223 >> exists_tac ``rrestrict TSF (tempSubForms g)`` 224 >> rpt strip_tac >> fs[TSF_PO] 225 >> `!q. (q ��� d) ==> ((q,s) ��� TSF)` 226 by metis_tac[TRANS_REACHES_SUBFORMS] 227 >> `(s',s) ��� TSF` by metis_tac[] 228 >> fs[in_rrestrict] 229 >> `(s,g) ��� TSF` by metis_tac[TSF_def,IN_DEF] 230 >> metis_tac[TSF_TRANS_LEMM, transitive_def,TSF_def,IN_DEF] 231 ); 232 233val LTL2WAA_ISWEAK = store_thm 234 ("LTL2WAA_ISWEAK", 235 ``!f. isVeryWeakAlterA (ltl2vwaa f)``, 236 strip_tac >> fs[ltl2vwaa_def] >> metis_tac[LTL2WAA_ISWEAK_LEMM] 237 ); 238 239val LTL2WAA_ISFINITE = store_thm 240 ("LTL2WAA_ISFINITE", 241 ``!f g. FINITE (ltl2vwaa_free_alph (POW (props f)) g).states``, 242 fs[ltl2vwaa_free_alph_def] >> metis_tac[TSF_FINITE] 243 ); 244 245(* 246 run constructions that are needed for the correctness proof 247*) 248 249val REPL_F2_LEMM = store_thm 250 ("REPL_F2_LEMM", 251 ``!a r f f' f1 f2 w l qs.(runForAA (ltl2vwaa_free_alph (POW (props f')) f2) r w 252 /\ (a,qs) ��� trans (POW (props f')) f 253 /\ at w l ��� a 254 /\ qs ��� r.E (l, f1) 255 ) 256 ==> ?r'. runForAA (ltl2vwaa_free_alph (POW (props f')) f) r' (suff w l)``, 257 rpt strip_tac 258 >> `���e t a'. 259 (qs = BIGUNION t) ��� e ��� tempDNF f ��� (a = BIGINTER a') ��� 260 (���t'. t' ��� t ��� ���q a''. a'' ��� a' ��� q ��� e ��� (a'',t') ��� trans (POW (props f')) q) ��� 261 ���q. q ��� e ��� ���t' a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans (POW (props f')) q` 262 by fs[TRANS_TEMPDNF_LEMM] 263 >> `���q. ?t'. 264 q ��� e ��� 265 ���a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans (POW (props f')) q` 266 by metis_tac[] 267 >> `?h. !q. q ��� e ��� 268 ���a''. a'' ��� a' ��� (h q) ��� t ��� (a'',(h q)) ��� trans (POW (props f')) q` 269 by metis_tac[SKOLEM_THM] 270 >> `!q. q ��� e ==> h q ��� t` by metis_tac[] 271 >> `!q. q ��� e ==> h q ��� qs` by metis_tac[SUBSET_BIGUNION_I] 272 >> `!q. q ��� e ==> h q ��� r.V (l + 1)` 273 by metis_tac[SUBSET_TRANS, runForAA_def, validAARunFor_def] 274 >> fs[] >> fs[runForAA_def] 275 >> qabbrev_tac `r_int = 276 ALTERA_RUN (\i. if i = 0 then e else r.V (i + l)) 277 (��(i,q). if i = 0 then h q else r.E (i + l,q))` 278 >> qabbrev_tac `r_new = run_restr e r_int` 279 >> qexists_tac `r_new` 280 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f')) f) r_new (suff w l) ��� 281 (���b x. infBranchOf r_new b ��� branchFixP b x 282 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) f).final)` 283 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 284 >> strip_tac 285 >- (fs[validAARunFor_def] 286 >> `!n. r_new.V (n + 1) ��� tempSubForms f ��� r.V (n + 1 + l)` by 287 (qunabbrev_tac `r_new` >> qunabbrev_tac `r_int` >> fs[ltl2vwaa_free_alph_def] 288 >> Induct_on `n` >> fs[] >> rpt strip_tac 289 >- (fs[SUBSET_DEF, run_restr_def, run_restr_V_def] >> rpt strip_tac 290 >> `e ��� tempSubForms f` by metis_tac[TEMPDNF_TEMPSUBF] 291 >> `SUC 0 = 1` by simp[] 292 >> `x ��� run_restr_V e 293 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 294 (��(i,q). if i = 0 then h q else r.E (i + l,q))) (SUC 0)` 295 by fs[] 296 >> fs[run_restr_V_def] 297 >> `���a''. a'' ��� a' ��� (a'',h q) ��� trans (POW (props f')) q` 298 by metis_tac[] 299 >> `(x,q) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 300 >> metis_tac[TSF_def,IN_DEF,TSF_TRANS_LEMM, transitive_def,SUBSET_DEF] 301 ) 302 >- (fs[SUBSET_DEF, run_restr_def, run_restr_V_def] >> rpt strip_tac 303 >> `SUC 0 = 1` by simp[] 304 >> `x ��� run_restr_V e 305 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 306 (��(i,q). if i = 0 then h q else r.E (i + l,q))) (SUC 0)` 307 by fs[] 308 >> fs[run_restr_V_def] 309 >> metis_tac[] 310 ) 311 >- (fs[SUBSET_DEF, run_restr_def, run_restr_V_def] >> rpt strip_tac 312 >> `SUC n + 1 = SUC (n + 1)` by simp[] 313 >> `x ��� 314 run_restr_V e 315 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 316 (��(i,q). if i = 0 then h q else r.E (i + l,q))) (SUC (n + 1))` 317 by metis_tac[] 318 >> fs[run_restr_V_def] 319 >> `q ��� r.V (l + (n + 1)) /\ q ��� tempSubForms f` by metis_tac[] 320 >> `?a''. (a'',r.E(l + (n + 1),q)) ��� trans (POW (props f')) q` 321 by metis_tac[] 322 >> `(x,q) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 323 >> metis_tac[TSF_def, IN_DEF, TSF_TRANS_LEMM, transitive_def] 324 ) 325 >- (fs[SUBSET_DEF, run_restr_def, run_restr_V_def] >> rpt strip_tac 326 >> `SUC n + 1 = SUC (n + 1)` by simp[] 327 >> `x ��� 328 run_restr_V e 329 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 330 (��(i,q). if i = 0 then h q else r.E (i + l,q))) (SUC (n + 1))` 331 by metis_tac[] 332 >> fs[run_restr_V_def] 333 >> `x ��� r.V ((l + (n + 1)) + 1)` by metis_tac[] 334 >> rw[SUC_ONE_ADD] >> fs[] 335 ) 336 ) 337 >> rpt strip_tac 338 >- (qunabbrev_tac `r_new` >> qunabbrev_tac `r_int` 339 >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def, run_restr_def] 340 >> fs[run_restr_V_def]) 341 >- (Cases_on `i = 0` 342 >- (qunabbrev_tac `r_new` >> qunabbrev_tac `r_int` 343 >> fs[ltl2vwaa_free_alph_def, run_restr_def, run_restr_V_def] 344 >> metis_tac[TEMPDNF_TEMPSUBF] 345 ) 346 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 347 >> `i = j + 1` by simp[] 348 >> `r_new.V (j + 1) ��� tempSubForms f` by metis_tac[SUBSET_INTER] 349 >> fs[ltl2vwaa_free_alph_def] >> metis_tac[] 350 ) 351 ) 352 >- (Cases_on `i = 0` >> fs[ltl2vwaa_free_alph_def] 353 >- (qunabbrev_tac `r_int` >> qunabbrev_tac `r_new` 354 >> fs[run_restr_def, run_restr_E_def, run_restr_V_def] 355 >> `���a''. a'' ��� a' ��� (a'',h q) ��� trans (POW (props f')) q` 356 by metis_tac[] >> qexists_tac `a''` 357 >> fs[AT_SUFF_LEMM] 358 ) 359 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 360 >> `i = j + 1` by simp[] 361 >> `r_new.V (j + 1) ��� r.V (l + (j + 1))` by metis_tac[] 362 >> `q ��� r.V (l + (j + 1))` by metis_tac[SUBSET_DEF] 363 >> qunabbrev_tac `r_int` >> qunabbrev_tac `r_new` 364 >> fs[run_restr_def, run_restr_E_def, run_restr_V_def] 365 >> `?a''. (a'',r.E((j + l + 1),q)) ��� trans (POW (props f')) q 366 ��� at w (j + l + 1) ��� a''` by fs[] 367 >> qexists_tac `a''` >> fs[AT_SUFF_LEMM] 368 ) 369 ) 370 >- (Cases_on `i = 0` >> fs[ltl2vwaa_free_alph_def] 371 >- (qunabbrev_tac `r_int` >> qunabbrev_tac `r_new` 372 >> fs[run_restr_def, run_restr_E_def, run_restr_V_def] 373 >> fs[SUBSET_DEF] >> rpt strip_tac 374 >> Cases_on `q ��� e` >> fs[] 375 >> `1 = SUC 0` by simp[] 376 >> `x ��� 377 run_restr_V e 378 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 379 (��(i,q). if i = 0 then h q else r.E (i + l,q))) (SUC 0)` 380 suffices_by metis_tac[] 381 >> fs[run_restr_V_def] 382 >> qexists_tac `h q` >> strip_tac >> fs[] 383 >> qexists_tac `q` >> fs[] 384 ) 385 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 386 >> `i = j + 1` by simp[] 387 >> `r_new.V (j + 1) ��� r.V (l + (j + 1))` by metis_tac[] 388 >> fs[SUBSET_DEF] >> rpt strip_tac 389 >> qunabbrev_tac `r_int` >> qunabbrev_tac `r_new` 390 >> fs[run_restr_def, run_restr_E_def, run_restr_V_def] 391 >> Cases_on 392 `q ��� 393 run_restr_V e 394 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 395 (��(i,q). if i = 0 then h q else r.E (i + l,q))) (j + 1)` 396 >> fs[] 397 >> `q ��� r.V (j + (l + 1))` by fs[] 398 >> `j + 2 = SUC (j + 1)` by simp[] 399 >> `x ��� 400 run_restr_V e 401 (ALTERA_RUN (��i. if i = 0 then e else r.V (i + l)) 402 (��(i,q). if i = 0 then h q else r.E (i + l,q))) 403 (SUC (j + 1))` 404 suffices_by metis_tac[] 405 >> fs[run_restr_V_def] >> qexists_tac `r.E (j + (l + 1),q)` 406 >> rpt strip_tac >> fs[] >> qexists_tac `q` >> fs[] 407 ) 408 ) 409 >- (Cases_on `i = 0` >> fs[] 410 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 411 >> `i = j + 1` by simp[] 412 >> `r_new.V (j + 1) ��� r.V (l + (j + 1))` by metis_tac[] 413 >> fs[run_restr_def] 414 >> qunabbrev_tac `r_new` 415 >> fs[run_restr_V_def] 416 >> `j + 1 = SUC j` by simp[] >> rw[] 417 >> `q ��� run_restr_V e r_int (SUC j)` by metis_tac[] 418 >> fs[run_restr_V_def] 419 >> qexists_tac `q'` >> fs[run_restr_E_def, run_restr_V_def] 420 ) 421 ) 422 >- (`���b x. infBranchOf r b ��� branchFixP b x 423 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) f2).final` 424 by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 425 >> rpt strip_tac >> fs[ltl2vwaa_free_alph_def, finalForms_def] 426 >> `!aut. (let run_int = 427 ALTERA_RUN (��i. if i = 0 then e else r.V (i+l)) 428 (��(i,q). if i = 0 then h q else r.E (i+l,q)) 429 in 430 validAARunFor aut r w ��� (���q. q ��� e ��� h q ��� r.V (1 + l)) ��� 431 infBranchOf (run_restr e run_int) b ��� branchFixP b x ��� 432 ���b'. infBranchOf r b' ��� branchFixP b' x)` 433 by metis_tac[REPL_RUN_CONSTR_LEMM2] 434 >> `���b'. infBranchOf r b' ��� branchFixP b' x` by metis_tac[ADD_COMM] 435 >> `���i. b' i ��� r.V i` by metis_tac[BRANCH_V_LEMM] 436 >> `?i. b' i = x` by metis_tac[branchFixP_def] 437 >> `x ��� r.V i` by metis_tac[] 438 >> `r.V i ��� tempSubForms f2` by fs[validAARunFor_def] 439 >> metis_tac[SUBSET_DEF] 440 ) 441 ); 442 443val U_REPL_F1_LEMM = store_thm 444 ("U_REPL_F1_LEMM", 445 ``!a r f f1 f2 w l.(runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w 446 /\ (a,r.E (l,U f1 f2)) ��� 447 d_conj (trans (POW (props f)) f1) {(POW (props f), {U f1 f2})} 448 /\ at w l ��� a) 449 ==> ?r'. 450 runForAA 451 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) 452 r' (suff w l)``, 453 rpt strip_tac >> fs[d_conj_def] 454 >> `���e t a'. 455 (e1 = BIGUNION t) ��� e ��� tempDNF f1 ��� (a1 = BIGINTER a') ��� 456 (���t'. t' ��� t ��� ���q a''. a'' ��� a' ��� q ��� e ��� (a'',t') ��� trans (POW (props f)) q) ��� 457 ���q. q ��� e ��� ���t' a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans (POW (props f)) q` 458 by fs[TRANS_TEMPDNF_LEMM] 459 >> `���q. ?t'. 460 q ��� e ��� 461 ���a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans (POW (props f)) q` 462 by metis_tac[] 463 >> `?h. !q. q ��� e ��� 464 ���a''. a'' ��� a' ��� (h q) ��� t ��� (a'',(h q)) ��� trans (POW (props f)) q` 465 by metis_tac[SKOLEM_THM] 466 >> `!q. q ��� e ==> h q ��� t` by metis_tac[] 467 >> `!q. q ��� e ==> h q ��� e1` by metis_tac[SUBSET_BIGUNION_I] 468 >> qabbrev_tac `h' = (\q. if (q = X (U f1 f2)) then {U f1 f2} else h q)` 469 >> qabbrev_tac `e' = e ��� {X (U f1 f2)}` 470 >> `!q. q ��� e' ==> ((h' q = h q) \/ (h' q = {U f1 f2}))` 471 by metis_tac[] 472 >> `!q. q ��� e' ==> h' q ��� (h q ��� {U f1 f2})` 473 by metis_tac[SUBS_UNION_LEMM] 474 >> `!q. e ��� e'` by metis_tac[SUBSET_UNION] 475 >> `!q. q ��� e ==> h' q ��� h q ��� {U f1 f2}` 476 by metis_tac[SUBSET_DEF] 477 >> `!q. q ��� e ==> h' q ��� e1 ��� {U f1 f2}` by metis_tac[SUBS_UNION_LEMM2] 478 >> `!q. q ��� e' ==> q ��� e \/ (q = X (U f1 f2))` by metis_tac[IN_UNION, IN_SING] 479 >> `!q. q ��� e' ==> h' q ��� e1 ��� {U f1 f2}` by 480 (Cases_on `q ��� e` >> metis_tac[SUBSET_UNION]) 481 >> `!q. q ��� e' ==> h' q ��� r.V (l + 1)` 482 by metis_tac[SUBSET_TRANS, runForAA_def, validAARunFor_def] 483 >> fs[] >> fs[runForAA_def] 484 >> `?r'. validAARunFor 485 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) r' (suff w l) 486 /\ ���b x. infBranchOf r' b ��� branchFixP b x 487 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))).final` 488 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 489 >> `���b x. infBranchOf r b ��� branchFixP b x 490 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)).final` 491 by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 492 >> `(let run_int = 493 ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 494 (��(i,q). if i = 0 then h' q else r.E (i + l,q)) 495 in 496 validAARunFor (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w 497 ��� (���q. q ��� e' ��� h' q ��� r.V (l + 1)) ��� 498 ���i. (run_restr e' run_int).V (i + 1) ��� r.V (i + l + 1))` 499 by metis_tac[REPL_RUN_CONSTR_LEMM] 500 >> fs[] 501 >> qabbrev_tac `r_int = 502 (ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 503 (��(i,q). if i = 0 then h' q else r.E (i + l,q)))` 504 >> `���i. (run_restr e' r_int).V (i + 1) ��� r.V (i + (l + 1))` by metis_tac[] 505 >> qexists_tac `run_restr e' r_int` >> strip_tac 506 >- (fs[validAARunFor_def, ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 507 >> rpt strip_tac 508 >- (fs[] >> qexists_tac `e` >> rpt strip_tac >> fs[] 509 >> simp[run_restr_def, run_restr_V_def] >> fs[] 510 ) 511 >- (Cases_on `i = 0` 512 >> simp[SUBSET_DEF] 513 >> simp[run_restr_def, run_restr_V_def, tempSubForms_def, UNION_DEF] 514 >> rpt strip_tac 515 >- (`x ��� e \/ (x = (X (U f1 f2)))` by metis_tac[] >> fs[] 516 >> `e ��� tempSubForms f1` by metis_tac[TEMPDNF_TEMPSUBF] 517 >> metis_tac[SUBSET_DEF]) 518 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 519 >> `i = j + 1` by simp[] 520 >> fs[run_restr_def] 521 >> `x ��� r.V (j + (l + 1))` by metis_tac[SUBSET_DEF] 522 >> `x ��� tempSubForms (U f1 f2)` by metis_tac[SUBSET_DEF] 523 >> fs[tempSubForms_def, SUBSET_DEF, UNION_DEF] 524 ) 525 ) 526 >- (Cases_on `i = 0` >> simp[run_restr_def, run_restr_E_def] 527 >- (fs[run_restr_def, run_restr_V_def] 528 >> Cases_on `q = X (U f1 f2)` 529 >- (qexists_tac `POW (props f)` >> strip_tac 530 >- (simp[trans_def] >> qunabbrev_tac `r_int` 531 >> qunabbrev_tac `h'` >> fs[] 532 >> fs[tempDNF_def] 533 ) 534 >- (`at w l ��� POW (props f)` suffices_by fs[AT_SUFF_LEMM] 535 >> metis_tac[IN_INTER]) 536 ) 537 >- (`q ��� e` by metis_tac[] 538 >> `���a''. a'' ��� a' ��� (a'',h q) ��� trans (POW (props f)) q` 539 by metis_tac[] 540 >> qexists_tac `a''` >> strip_tac 541 >- (simp[trans_def] >> qunabbrev_tac `r_int` 542 >> qunabbrev_tac `h'` >> fs[]) 543 >- (`at w l ��� a''` suffices_by fs[AT_SUFF_LEMM] 544 >> metis_tac[IN_INTER, IN_BIGINTER]) 545 ) 546 ) 547 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 548 >> `i = j + 1` by simp[] 549 >> `q ��� r.V (j + (l + 1))` by metis_tac[SUBSET_DEF] 550 >> `���a''. (a'',r.E ((j + (l + 1)) ,q)) ��� trans (POW (props f)) q 551 ��� at w (j + (l + 1)) ��� a''` 552 by metis_tac[] 553 >> qexists_tac `a''` 554 >> `at w (i + l) ��� a''` by metis_tac[ADD_COMM, ADD_ASSOC] 555 >> fs[run_restr_def] 556 >> qunabbrev_tac `r_int` >> simp[run_restr_V_def, trans_def] 557 >> metis_tac[AT_SUFF_LEMM] 558 ) 559 ) 560 >- (simp[run_restr_def, run_restr_E_def, run_restr_V_def] 561 >> Cases_on `q ��� run_restr_V e' r_int i` >> fs[EMPTY_SUBSET] 562 >> Cases_on `i = 0` 563 >- (simp[run_restr_V_def] 564 >> qunabbrev_tac `r_int` >> simp[run_restr_V_def] >> fs[] 565 >> `h' q ��� 566 run_restr_V e' 567 (ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 568 (��(i,q). if i = 0 then h' q else r.E (i + l,q))) (SUC 0)` 569 suffices_by simp[] 570 >> simp[run_restr_V_def] >> simp[SUBSET_DEF, BIGUNION] 571 >> rpt strip_tac >> qexists_tac `h' q` >> fs[] 572 >> qexists_tac `q` >> fs[] 573 >> metis_tac[run_restr_V_def] 574 ) 575 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 576 >> `i = j + 1` by simp[] 577 >> fs[run_restr_def] 578 >> `q ��� r.V (j + (l + 1))` by metis_tac [SUBSET_DEF] 579 >> qunabbrev_tac `r_int` 580 >> simp[run_restr_V_def, run_restr_E_def] >> fs[] 581 >> simp[SUBSET_DEF] >> rpt strip_tac 582 >> `j + 2 = SUC (j + 1)` by simp[] 583 >> `x ��� 584 run_restr_V e' 585 (ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 586 (��(i,q). if i = 0 then h' q else r.E (i + l,q))) (SUC (j + 1))` 587 suffices_by metis_tac[] 588 >> fs[run_restr_V_def] 589 >> qexists_tac `r.E (j+(l+1),q)` >> strip_tac >> fs[] 590 >> qexists_tac `q` >> fs[] 591 ) 592 ) 593 >- (Cases_on `i = 0` >> fs[] 594 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 595 >> `i = j + 1` by simp[] 596 >> fs[run_restr_def] 597 >> `j + 1 = SUC j` by simp[] 598 >> `q ��� run_restr_V e' r_int (SUC j)` by metis_tac[] 599 >> fs[run_restr_V_def] 600 >> qexists_tac `q'` >> fs[] 601 >> fs[run_restr_E_def] 602 )) 603 >- (rpt strip_tac 604 >> `!aut. (let run_int = 605 ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 606 (��(i,q). if i = 0 then h' q else r.E (i + l,q)) 607 in 608 validAARunFor aut r w ��� (���q. q ��� e' ��� h' q ��� r.V (1 + l)) ��� 609 infBranchOf (run_restr e' run_int) b ��� branchFixP b x ��� 610 ���b'. infBranchOf r b' ��� branchFixP b' x)` 611 by metis_tac[REPL_RUN_CONSTR_LEMM2] 612 >> fs[] 613 >> `���b'. infBranchOf r b' ��� branchFixP b' x` by metis_tac[] 614 >> fs[ltl2vwaa_free_alph_def, finalForms_def] 615 >> `tempSubForms (CONJ f1 (X (U f1 f2))) 616 = {X (U f1 f2)} ��� tempSubForms (U f1 f2)` by 617 (fs[tempSubForms_def] >> metis_tac[UNION_DEF]) 618 >> `U f1' f2' ��� {X (U f1 f2)} ��� tempSubForms (U f1 f2)` by fs[] 619 >> `~(X (U f1 f2) = U f1' f2')` by rw[] 620 >> `U f1' f2' ��� tempSubForms (U f1 f2)` by metis_tac[IN_UNION,IN_SING] 621 >> metis_tac[] 622 ) 623 ); 624 625val R_REPL_F1_LEMM = store_thm 626 ("R_REPL_F1_LEMM", 627 ``!a r f f1 f2 w l.(runForAA (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) r w 628 /\ (a,r.E (l,R f1 f2)) ��� 629 d_conj (trans (POW (props f)) f2) {(POW (props f), {R f1 f2})} 630 /\ at w l ��� a) 631 ==> ?r'. 632 runForAA 633 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) 634 r' (suff w l)``, 635 rpt strip_tac >> fs[d_conj_def] 636 >> `���e t a'. 637 (e1 = BIGUNION t) ��� e ��� tempDNF f2 ��� (a1 = BIGINTER a') ��� 638 (���t'. t' ��� t ��� ���q a''. a'' ��� a' ��� q ��� e ��� (a'',t') ��� trans (POW (props f)) q) ��� 639 ���q. q ��� e ��� ���t' a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans (POW (props f)) q` 640 by fs[TRANS_TEMPDNF_LEMM] 641 >> `���q. ?t'. 642 q ��� e ��� 643 ���a''. a'' ��� a' ��� t' ��� t ��� (a'',t') ��� trans (POW (props f)) q` 644 by metis_tac[] 645 >> `?h. !q. q ��� e ��� 646 ���a''. a'' ��� a' ��� (h q) ��� t ��� (a'',(h q)) ��� trans (POW (props f)) q` 647 by metis_tac[SKOLEM_THM] 648 >> `!q. q ��� e ==> h q ��� t` by metis_tac[] 649 >> `!q. q ��� e ==> h q ��� e1` by metis_tac[SUBSET_BIGUNION_I] 650 >> qabbrev_tac `h' = (\q. if (q = X (R f1 f2)) then {R f1 f2} else h q)` 651 >> qabbrev_tac `e' = e ��� {X (R f1 f2)}` 652 >> `!q. q ��� e' ==> ((h' q = h q) \/ (h' q = {R f1 f2}))` 653 by metis_tac[] 654 >> `!q. q ��� e' ==> h' q ��� (h q ��� {R f1 f2})` 655 by metis_tac[SUBS_UNION_LEMM] 656 >> `!q. e ��� e'` by metis_tac[SUBSET_UNION] 657 >> `!q. q ��� e ==> h' q ��� h q ��� {R f1 f2}` 658 by metis_tac[SUBSET_DEF] 659 >> `!q. q ��� e ==> h' q ��� e1 ��� {R f1 f2}` by metis_tac[SUBS_UNION_LEMM2] 660 >> `!q. q ��� e' ==> q ��� e \/ (q = X (R f1 f2))` by metis_tac[IN_UNION, IN_SING] 661 >> `!q. q ��� e' ==> h' q ��� e1 ��� {R f1 f2}` by 662 (Cases_on `q ��� e` >> metis_tac[SUBSET_UNION]) 663 >> `!q. q ��� e' ==> h' q ��� r.V (l + 1)` 664 by metis_tac[SUBSET_TRANS, runForAA_def, validAARunFor_def] 665 >> fs[] >> fs[runForAA_def] 666 >> `?r'. validAARunFor 667 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) r' (suff w l) 668 /\ ���b x. infBranchOf r' b ��� branchFixP b x 669 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))).final` 670 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 671 >> `���b x. infBranchOf r b ��� branchFixP b x 672 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)).final` 673 by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 674 >> `(let run_int = 675 ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 676 (��(i,q). if i = 0 then h' q else r.E (i + l,q)) 677 in 678 validAARunFor (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) r w 679 ��� (���q. q ��� e' ��� h' q ��� r.V (l + 1)) ��� 680 ���i. (run_restr e' run_int).V (i + 1) ��� r.V (i + l + 1))` 681 by metis_tac[REPL_RUN_CONSTR_LEMM] 682 >> fs[] 683 >> qabbrev_tac `r_int = 684 (ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 685 (��(i,q). if i = 0 then h' q else r.E (i + l,q)))` 686 >> `���i. (run_restr e' r_int).V (i + 1) ��� r.V (i + (l + 1))` by metis_tac[] 687 >> qexists_tac `run_restr e' r_int` >> strip_tac 688 >- (fs[validAARunFor_def, ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 689 >> rpt strip_tac 690 >- (fs[] >> qexists_tac `e` >> rpt strip_tac >> fs[] 691 >> simp[run_restr_def, run_restr_V_def] >> fs[] 692 ) 693 >- (Cases_on `i = 0` 694 >> simp[SUBSET_DEF] 695 >> simp[run_restr_def, run_restr_V_def, tempSubForms_def, UNION_DEF] 696 >> rpt strip_tac 697 >- (`x ��� e \/ (x = (X (R f1 f2)))` by metis_tac[] >> fs[] 698 >> `e ��� tempSubForms f2` by metis_tac[TEMPDNF_TEMPSUBF] 699 >> metis_tac[SUBSET_DEF]) 700 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 701 >> `i = j + 1` by simp[] 702 >> fs[run_restr_def] 703 >> `x ��� r.V (j + (l + 1))` by metis_tac[SUBSET_DEF] 704 >> `x ��� tempSubForms (R f1 f2)` by metis_tac[SUBSET_DEF] 705 >> fs[tempSubForms_def, SUBSET_DEF, UNION_DEF] 706 ) 707 ) 708 >- (Cases_on `i = 0` >> simp[run_restr_def, run_restr_E_def] 709 >- (fs[run_restr_def, run_restr_V_def] 710 >> Cases_on `q = X (R f1 f2)` 711 >- (qexists_tac `POW (props f)` >> strip_tac 712 >- (simp[trans_def] >> qunabbrev_tac `r_int` 713 >> qunabbrev_tac `h'` >> fs[] 714 >> fs[tempDNF_def] 715 ) 716 >- (`at w l ��� POW (props f)` suffices_by fs[AT_SUFF_LEMM] 717 >> metis_tac[IN_INTER]) 718 ) 719 >- (`q ��� e` by metis_tac[] 720 >> `���a''. a'' ��� a' ��� (a'',h q) ��� trans (POW (props f)) q` 721 by metis_tac[] 722 >> qexists_tac `a''` >> strip_tac 723 >- (simp[trans_def] >> qunabbrev_tac `r_int` 724 >> qunabbrev_tac `h'` >> fs[]) 725 >- (`at w l ��� a''` suffices_by fs[AT_SUFF_LEMM] 726 >> metis_tac[IN_INTER, IN_BIGINTER]) 727 ) 728 ) 729 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 730 >> `i = j + 1` by simp[] 731 >> `q ��� r.V (j + (l + 1))` by metis_tac[SUBSET_DEF] 732 >> `���a''. (a'',r.E ((j + (l + 1)) ,q)) ��� trans (POW (props f)) q 733 ��� at w (j + (l + 1)) ��� a''` 734 by metis_tac[] 735 >> qexists_tac `a''` 736 >> `at w (i + l) ��� a''` by metis_tac[ADD_COMM, ADD_ASSOC] 737 >> fs[run_restr_def] 738 >> qunabbrev_tac `r_int` >> simp[run_restr_V_def, trans_def] 739 >> metis_tac[AT_SUFF_LEMM] 740 ) 741 ) 742 >- (simp[run_restr_def, run_restr_E_def, run_restr_V_def] 743 >> Cases_on `q ��� run_restr_V e' r_int i` >> fs[EMPTY_SUBSET] 744 >> Cases_on `i = 0` 745 >- (simp[run_restr_V_def] 746 >> qunabbrev_tac `r_int` >> simp[run_restr_V_def] >> fs[] 747 >> `h' q ��� 748 run_restr_V e' 749 (ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 750 (��(i,q). if i = 0 then h' q else r.E (i + l,q))) (SUC 0)` 751 suffices_by simp[] 752 >> simp[run_restr_V_def] >> simp[SUBSET_DEF, BIGUNION] 753 >> rpt strip_tac >> qexists_tac `h' q` >> fs[] 754 >> qexists_tac `q` >> fs[] 755 >> metis_tac[run_restr_V_def] 756 ) 757 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 758 >> `i = j + 1` by simp[] 759 >> fs[run_restr_def] 760 >> `q ��� r.V (j + (l + 1))` by metis_tac [SUBSET_DEF] 761 >> qunabbrev_tac `r_int` 762 >> simp[run_restr_V_def, run_restr_E_def] >> fs[] 763 >> simp[SUBSET_DEF] >> rpt strip_tac 764 >> `j + 2 = SUC (j + 1)` by simp[] 765 >> `x ��� 766 run_restr_V e' 767 (ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 768 (��(i,q). if i = 0 then h' q else r.E (i + l,q))) (SUC (j + 1))` 769 suffices_by metis_tac[] 770 >> fs[run_restr_V_def] 771 >> qexists_tac `r.E (j+(l+1),q)` >> strip_tac >> fs[] 772 >> qexists_tac `q` >> fs[] 773 ) 774 ) 775 >- (Cases_on `i = 0` >> fs[] 776 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 777 >> `i = j + 1` by simp[] 778 >> fs[run_restr_def] 779 >> `j + 1 = SUC j` by simp[] 780 >> `q ��� run_restr_V e' r_int (SUC j)` by metis_tac[] 781 >> fs[run_restr_V_def] 782 >> qexists_tac `q'` >> fs[] 783 >> fs[run_restr_E_def] 784 )) 785 >- (rpt strip_tac 786 >> `!aut. (let run_int = 787 ALTERA_RUN (��i. if i = 0 then e' else r.V (i + l)) 788 (��(i,q). if i = 0 then h' q else r.E (i + l,q)) 789 in 790 validAARunFor aut r w ��� (���q. q ��� e' ��� h' q ��� r.V (1 + l)) ��� 791 infBranchOf (run_restr e' run_int) b ��� branchFixP b x ��� 792 ���b'. infBranchOf r b' ��� branchFixP b' x)` 793 by metis_tac[REPL_RUN_CONSTR_LEMM2] 794 >> fs[] 795 >> `���b'. infBranchOf r b' ��� branchFixP b' x` by metis_tac[] 796 >> fs[ltl2vwaa_free_alph_def, finalForms_def] 797 >> `tempSubForms (CONJ f2 (X (R f1 f2))) 798 = {X (R f1 f2)} ��� tempSubForms (R f1 f2)` by 799 (fs[tempSubForms_def] >> metis_tac[UNION_DEF]) 800 >> `U f1' f2' ��� {X (R f1 f2)} ��� tempSubForms (R f1 f2)` by fs[] 801 >> `~(X (R f1 f2) = U f1' f2')` by rw[] 802 >> `U f1' f2' ��� tempSubForms (R f1 f2)` by metis_tac[IN_UNION,IN_SING] 803 >> metis_tac[] 804 ) 805 ); 806 807val RUN_FOR_DISJ_LEMM = store_thm 808 ("RUN_FOR_DISJ_LEMM", 809 ``!f1 f2 f w run. 810 (runForAA (ltl2vwaa_free_alph (POW (props f)) f1) run w 811 \/ runForAA (ltl2vwaa_free_alph (POW (props f)) f2) run w 812 ) 813 ==> runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w``, 814 fs[runForAA_def] >> rpt strip_tac 815 >- (fs[ltl2vwaa_free_alph_def, initForms_def, tempSubForms_def, finalForms_def] 816 >> fs[tempDNF_def, tempSubForms_def, SUBSET_DEF, UNION_DEF] >> rpt strip_tac 817 >> fs[validAARunFor_def,SUBSET_DEF] >> rpt strip_tac 818 >> metis_tac[]) 819 >- (`!b x. infBranchOf run b ��� branchFixP b x ��� 820 x ��� (ltl2vwaa_free_alph (POW (props f)) f1).final` 821 by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 822 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w 823 /\ (���b x. (infBranchOf run b ��� branchFixP b x) 824 ==> (x ��� (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)).final))` 825 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 826 >> rpt strip_tac 827 >- (fs[validAARunFor_def] >> rpt strip_tac 828 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 829 >> rpt strip_tac >> fs[tempSubForms_def] >> metis_tac[] 830 ) 831 >- (fs[ltl2vwaa_free_alph_def, finalForms_def] 832 >> `���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[] 833 >> `x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[] 834 >> `���i. b i ��� run.V i` by metis_tac[BRANCH_V_LEMM] 835 >> fs[validAARunFor_def, branchFixP_def] 836 >> `b i ��� tempSubForms f1` by metis_tac[SUBSET_DEF] 837 >> metis_tac[] 838 ) 839 ) 840 >- (fs[ltl2vwaa_free_alph_def, initForms_def, tempSubForms_def, finalForms_def] 841 >> fs[tempDNF_def, tempSubForms_def, SUBSET_DEF, UNION_DEF] >> rpt strip_tac 842 >> fs[validAARunFor_def,SUBSET_DEF] >> rpt strip_tac 843 >> metis_tac[]) 844 >- (`!b x. infBranchOf run b ��� branchFixP b x ��� 845 x ��� (ltl2vwaa_free_alph (POW (props f)) f2).final` 846 by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 847 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w 848 /\ (���b x. (infBranchOf run b ��� branchFixP b x) 849 ==> (x ��� (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)).final))` 850 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 851 >> rpt strip_tac 852 >- (fs[validAARunFor_def] >> rpt strip_tac 853 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 854 >> rpt strip_tac >> fs[tempSubForms_def] >> metis_tac[] 855 ) 856 >- (fs[ltl2vwaa_free_alph_def, finalForms_def] 857 >> `���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2` by metis_tac[] 858 >> `x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2` by metis_tac[] 859 >> `���i. b i ��� run.V i` by metis_tac[BRANCH_V_LEMM] 860 >> fs[validAARunFor_def, branchFixP_def] 861 >> `b i ��� tempSubForms f2` by metis_tac[SUBSET_DEF] 862 >> metis_tac[] 863 ) 864 ) 865 ); 866 867val RUN_FOR_DISJ_LEMM2 = store_thm 868 ("RUN_FOR_DISJ_LEMM2", 869 ``!f f1 f2 run w. 870 runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w 871 ==> (runForAA (ltl2vwaa_free_alph (POW (props f)) f1) run w 872 \/ runForAA (ltl2vwaa_free_alph (POW (props f)) f2) run w 873 )``, 874 rpt strip_tac >> fs[runForAA_def] 875 >> `���b x. infBranchOf run b ��� branchFixP b x 876 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)).final` 877 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 878 >> asm_simp_tac(srw_ss() ++ SatisfySimps.SATISFY_ss ++ boolSimps.CONJ_ss) 879 [BRANCH_ACC_LEMM,LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 880 >> fs[ltl2vwaa_free_alph_def,validAARunFor_def] 881 >> rpt strip_tac >> fs[initForms_def, tempDNF_def, tempSubForms_def, finalForms_def] 882 >- (`(���i. run.V i ��� tempSubForms f1) ��� 883 (���b x. 884 infBranchOf run b ��� branchFixP b x ��� 885 ���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1) ` 886 suffices_by metis_tac[] 887 >> conj_tac 888 >- (Induct_on `i` >> fs[tempSubForms_def, tempDNF_def,TEMPDNF_TEMPSUBF] 889 >> fs[SUBSET_DEF] >> rpt strip_tac 890 >> `(SUC i = 0) ��� ���q'. x ��� run.E ((SUC i) ��� 1,q') ��� q' ��� run.V ((SUC i) ��� 1)` 891 by metis_tac[] >> fs[] 892 >> `���a. (a,run.E (i,q')) ��� trans (POW (props f)) q'` 893 by metis_tac[] 894 >> `(x,q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 895 >> `(q',f1) ��� TSF` by metis_tac[TSF_def, IN_DEF] 896 >> metis_tac[TSF_TRANS_LEMM, transitive_def, TSF_def, IN_DEF] 897 ) 898 >- metis_tac[] 899 ) 900 >- (`(���i. run.V i ��� tempSubForms f2) ��� 901 (���b x. 902 infBranchOf run b ��� branchFixP b x ��� 903 ���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2) ` 904 suffices_by metis_tac[] 905 >> conj_tac 906 >- (Induct_on `i` >> fs[tempSubForms_def, tempDNF_def,TEMPDNF_TEMPSUBF] 907 >> fs[SUBSET_DEF] >> rpt strip_tac 908 >> `(SUC i = 0) ��� ���q'. x ��� run.E ((SUC i) ��� 1,q') ��� q' ��� run.V ((SUC i) ��� 1)` 909 by metis_tac[] >> fs[] 910 >> `���a. (a,run.E (i,q')) ��� trans (POW (props f)) q'` 911 by metis_tac[] 912 >> `(x,q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 913 >> `(q',f2) ��� TSF` by metis_tac[TSF_def, IN_DEF] 914 >> metis_tac[TSF_TRANS_LEMM, transitive_def, TSF_def, IN_DEF] 915 ) 916 >- metis_tac[] 917 ) 918 ); 919 920val REPL_IN_0 = store_thm 921 ("REPL_IN_0", 922 ``!r w f f' f1 f2 a p. 923 runForAA (ltl2vwaa_free_alph (POW (props f')) f) r w 924 /\ (a, r.V 1) ��� trans (POW (props f')) (p) 925 /\ at w 0 ��� a 926 /\ {p} ��� tempDNF p 927 ==> 928 ?r'. runForAA (ltl2vwaa_free_alph (POW (props f')) (p)) r' w``, 929 rpt strip_tac >> fs[runForAA_def] 930 >> `?r'. validAARunFor (ltl2vwaa_free_alph (POW (props f')) (p)) r' w 931 /\ (���b x. infBranchOf r' b ��� branchFixP b x 932 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) (p)).final)` 933 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 934 >> `(���b x. infBranchOf r b ��� branchFixP b x 935 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) f).final)` 936 by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 937 >> SUBGOAL_THEN ``!n. r.V (n + 1) ��� tempSubForms (p)`` mp_tac 938 >- (Induct_on `n` 939 >- (`!q. q ��� r.V 1 ==> (q,p) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 940 >> fs[SUBSET_DEF] >> rpt strip_tac 941 >> metis_tac[TSF_def, IN_DEF] 942 ) 943 >- (fs[SUBSET_DEF] >> rpt strip_tac 944 >> `(((SUC n) + 1) = 0) 945 \/ ���q'. x ��� r.E (((SUC n) + 1) ��� 1,q') ��� q' ��� r.V (((SUC n) + 1) ��� 1)` 946 by metis_tac[validAARunFor_def] 947 >> fs[validAARunFor_def, ltl2vwaa_free_alph_def] 948 >> `���a'. (a',r.E(SUC n, q')) ��� trans (POW (props f')) q'` by metis_tac[] 949 >> `(x, q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 950 >> `q' ��� tempSubForms (p)` by metis_tac[SUC_ONE_ADD, ADD_COMM] 951 >> metis_tac[TSF_def, IN_DEF, TSF_TRANS_LEMM, transitive_def] 952 ) 953 ) 954 >- (rpt strip_tac 955 >> qexists_tac `ALTERA_RUN (\i. if i = 0 then {p} else r.V i) 956 (��(i,q). if i = 0 then r.V 1 else r.E (i,q))` 957 >> `!b. infBranchSuffOf r 1 b ��� 958 ���b'. infBranchOf r b' ��� ���j. b j = b' (j + 1)` 959 by metis_tac[BRANCH_SUFF_LEMM] 960 >> `!b. infBranchOf r b ��� ���i. b i ��� r.V i` by metis_tac[BRANCH_V_LEMM] 961 >> fs[validAARunFor_def] >> rpt strip_tac 962 >- (fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def]) 963 >- (Cases_on `i = 0` >> fs[tempSubForms_def, ltl2vwaa_free_alph_def] 964 >- (`{p} ��� tempSubForms p` by metis_tac[TEMPDNF_TEMPSUBF] 965 >> fs[SUBSET_DEF] 966 ) 967 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 968 >> `i = j + 1` by simp[] 969 >> metis_tac[] 970 ) 971 ) 972 >- (Cases_on `i = 0` >> fs[tempSubForms_def, ltl2vwaa_free_alph_def] 973 >> qexists_tac `a` >> fs[]) 974 >- (Cases_on `i = 0` >> fs[]) 975 >- (Cases_on `i = 0` >> fs[] 976 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 977 >> `i = j + 1` by simp[] 978 >> Cases_on `j = 0` >> fs[] 979 >> `((j + 1) = 0) ��� ���q'. q ��� r.E ((j + 1) ��� 1,q') ��� q' ��� r.V ((j + 1) ��� 1)` 980 by metis_tac[] >> fs[] 981 >> qexists_tac `q'` >> fs[] 982 ) 983 >- (fs[ltl2vwaa_free_alph_def, finalForms_def] 984 >> `infBranchSuffOf r 1 (\i. b (i + 1))` by 985 (simp[infBranchSuffOf_def] >> fs[] >> rpt strip_tac 986 >- (fs[infBranchOf_def] >> fs[] 987 >> `0 + 1 = 1` by simp[] 988 >> `b (0 + 1) ��� r.V 1` by metis_tac[] 989 >> fs[]) 990 >- (fs[infBranchOf_def] >> rename [���b (i + 2) ��� r.E _���] 991 >> `b (i + 1 + 1) ��� r.E(i+1, b (i+1))` suffices_by simp[] 992 >> `~(i + 1 = 0)` by simp[] >> metis_tac[] 993 ) 994 ) 995 >> qabbrev_tac `b' = (\i. b (i+1))` 996 >> `���b''. infBranchOf r b'' ��� ���j. b' j = b'' (j + 1)` 997 by metis_tac[] 998 >> `branchFixP b'' x` by 999 (fs[branchFixP_def] >> rpt strip_tac 1000 >> qexists_tac `i + 1` 1001 >> qunabbrev_tac `b'` 1002 >> rpt strip_tac >> fs[] 1003 >- (`i + 1 >= i` by simp[] 1004 >> `b (i+1) = b'' (i + 1)` by metis_tac[] 1005 >> metis_tac[]) 1006 >- (`m >= i` by simp[] 1007 >> `b m = x` by simp[] 1008 >> `m >= 1` by simp[] 1009 >> `~ (m = 0)` by simp[] 1010 >> `?k. m = SUC k` by (Cases_on `m` >> fs[]) 1011 >> `b (k + 1) = b'' (k + 1)` by metis_tac[] 1012 >> `SUC k = k + 1` by simp[] 1013 >> `b (SUC k) = x` by metis_tac[] 1014 >> `b (k + 1) = b'' (k + 1)` by metis_tac[] 1015 >> metis_tac[SUC_ONE_ADD,ADD_COMM] 1016 ) 1017 ) 1018 >> `x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f` 1019 by metis_tac[] 1020 >> `���i. b'' i ��� r.V i` by metis_tac[] 1021 >> `!i. b'' i ��� tempSubForms f` by metis_tac[SUBSET_DEF] 1022 >> fs[branchFixP_def] 1023 >> metis_tac[] 1024 ) 1025 ) 1026 ); 1027 1028val RUN_FOR_CONJ_LEMM = store_thm 1029 ("RUN_FOR_DISJ_LEMM", 1030 ``!f1 f2 f w. 1031 (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) f1) r w) 1032 /\ (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r w) 1033 ==> (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r w)``, 1034 fs[runForAA_def] >> rpt gen_tac >> strip_tac 1035 >> `?r. validAARunFor (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r w 1036 /\ (���b x. infBranchOf r b ��� branchFixP b x 1037 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)).final)` 1038 suffices_by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1039 >> qexists_tac `conj_run r r'` 1040 >> conj_tac 1041 >- (`!i. conj_run_V r r' i ��� (r.V i ��� r'.V i)` by metis_tac[CONJ_RUN_V_LEMM] 1042 >> fs[validAARunFor_def] >> rpt strip_tac 1043 >> fs[ltl2vwaa_free_alph_def, initForms_def, finalForms_def, tempSubForms_def] 1044 >> fs[tempDNF_def, conj_run_def, conj_run_V_def, conj_run_E_def] 1045 >- (qexists_tac `r.V 0` >> qexists_tac `r'.V 0` >> fs[]) 1046 >- (`conj_run_V r r' i ��� r.V i ��� r'.V i` by metis_tac[] 1047 >> `r.V i ��� (tempSubForms f1 ��� tempSubForms f2)` 1048 by metis_tac[SUBSET_UNION, SUBSET_TRANS] 1049 >> `r'.V i ��� (tempSubForms f1 ��� tempSubForms f2)` 1050 by metis_tac[SUBSET_UNION, SUBSET_TRANS] 1051 >> `r.V i ��� r'.V i ��� (tempSubForms f1 ��� tempSubForms f2)` 1052 by metis_tac[UNION_SUBSET] 1053 >> metis_tac[SUBSET_TRANS] 1054 ) 1055 >- (Cases_on `q ��� r.V i` 1056 >- (metis_tac[conj_run_branch_cond_def]) 1057 >- (Cases_on `q ��� r'.V i` 1058 >- (metis_tac[conj_run_branch_cond_def]) 1059 >- (`conj_run_V r r' i ��� r.V i ��� r'.V i` 1060 by metis_tac[] >> fs[SUBSET_DEF] 1061 >> metis_tac[] 1062 ) 1063 ) 1064 ) 1065 >- (fs[SUBSET_DEF, conj_run_V_def] >> rpt strip_tac 1066 >> `i + 1 = SUC i` by simp[] 1067 >> `x ��� conj_run_V r r' (SUC i)` suffices_by metis_tac[] 1068 >> fs[conj_run_V_def, conj_run_branch_cond_def] 1069 >> Cases_on `q ��� conj_run_V r r' i` >> fs[] 1070 >> Cases_on `q ��� r.V i` 1071 >- (qexists_tac `r.E (i,q)` >> fs[] 1072 >> qexists_tac `q` >> fs[conj_run_E_def]) 1073 >- (Cases_on `q ��� r'.V i` 1074 >- (qexists_tac `r'.E (i,q)` >> fs[] 1075 >> qexists_tac `q` >> fs[conj_run_E_def]) 1076 >- (metis_tac[NOT_IN_EMPTY]) 1077 ) 1078 ) 1079 >- (Cases_on `i=0` >> fs[] 1080 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 1081 >> rw[] 1082 >> fs[conj_run_V_def] 1083 >> qexists_tac `q'` >> rpt strip_tac >> fs[] 1084 ) 1085 ) 1086 >- (CCONTR_TAC 1087 >> fs[] 1088 >> `���b x. infBranchOf r b ��� branchFixP b x 1089 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) f1).final` 1090 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1091 >> `���b x. infBranchOf r' b ��� branchFixP b x 1092 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) f2).final` 1093 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1094 >> `���b'. (infBranchOf r b' ��� infBranchOf r' b') ��� branchFixP b' x` 1095 by metis_tac[CONJ_RUN_FIXP_LEMM] 1096 >- (fs[ltl2vwaa_free_alph_def, finalForms_def,acceptingAARun_def, tempSubForms_def] 1097 >- (`���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[] 1098 >> metis_tac[]) 1099 >- (`���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[] 1100 >> `U f1' f2' ��� tempSubForms f1` by metis_tac[] 1101 >> `!i. b' i ��� r.V i` by metis_tac[BRANCH_V_LEMM] 1102 >> `(���i. r.V i ��� (ALTER_A (tempSubForms f1) (POW (props f)) 1103 (trans (POW (props f))) (initForms f1) 1104 {U f1' f2 | U f1' f2 ��� tempSubForms f1} 1105 ).states)` 1106 by metis_tac[validAARunFor_def] 1107 >> fs[SUBSET_DEF, branchFixP_def] >> metis_tac[] 1108 ) 1109 ) 1110 >- (fs[ltl2vwaa_free_alph_def, finalForms_def,acceptingAARun_def, tempSubForms_def] 1111 >- (`���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2` by metis_tac[] 1112 >> `U f1' f2' ��� tempSubForms f2` by metis_tac[] 1113 >> `!i. b' i ��� r'.V i` by metis_tac[BRANCH_V_LEMM] 1114 >> `(���i. r'.V i ��� (ALTER_A (tempSubForms f2) (POW (props f)) 1115 (trans (POW (props f))) 1116 (initForms f2) 1117 {U f1 f2' | U f1 f2' ��� tempSubForms f2} 1118 ).states)` 1119 by metis_tac[validAARunFor_def] 1120 >> fs[SUBSET_DEF, branchFixP_def] >> metis_tac[] 1121 ) 1122 >- (`���f1 f2'. x ��� U f1 f2' ��� U f1 f2' ��� tempSubForms f2` by metis_tac[] 1123 >> metis_tac[]) 1124 ) 1125 ) 1126 ); 1127 1128val RUN_FOR_CONJ_LEMM2_UNION = store_thm 1129 ("RUN_FOR_CONJ_LEMM2_UNION", 1130 ``!f1 f2 f w run. 1131 runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) run w 1132 ==> (?r1. runForAA (ltl2vwaa_free_alph (POW (props f)) f1) r1 w 1133 /\ (?r2. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r2 w 1134 /\ !i. run.V i = r1.V i ��� r2.V i))``, 1135 fs[runForAA_def] >> rpt gen_tac >> rpt strip_tac 1136 >> `(!b x. infBranchOf run b ��� branchFixP b x 1137 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)).final)` 1138 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1139 >> `!init. init ��� run.V 0 ==> !i. run_restr_V init run i ��� run.V i` 1140 by metis_tac[RUN_RESTR_LEMM] 1141 >> `!init b. (init ��� run.V 0) /\ (infBranchOf (run_restr init run) b) 1142 ==> infBranchOf run b` 1143 by metis_tac[RUN_RESTR_FIXP_LEMM] 1144 >- (`?r1. validAARunFor (ltl2vwaa_free_alph (POW (props f)) f1) r1 w 1145 /\ (���b x. infBranchOf r1 b ��� branchFixP b x 1146 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) f1).final) /\ 1147 ���r2. 1148 (validAARunFor (ltl2vwaa_free_alph (POW (props f)) f2) r2 w ��� 1149 (���b x. infBranchOf r2 b ��� branchFixP b x 1150 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) f2).final)) ��� 1151 ���i. run.V i = r1.V i ��� r2.V i` 1152 suffices_by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1153 >> rpt strip_tac >> fs[validAARunFor_def, ltl2vwaa_free_alph_def, finalForms_def] 1154 >> rpt strip_tac >> fs[initForms_def, tempSubForms_def, tempDNF_def] 1155 >> qexists_tac `run_restr f' run` 1156 >> rpt strip_tac >> fs[run_restr_def, run_restr_V_def] 1157 >- (Induct_on `i` 1158 >- metis_tac[run_restr_V_def, TEMPDNF_TEMPSUBF] 1159 >- (`���i. run_restr_V f' run i ��� run.V i` by metis_tac[SUBSET_UNION] 1160 >> simp[run_restr_V_def, SUBSET_DEF] >> rpt strip_tac 1161 >> `(s = run.E (i,q)) ��� q ��� run_restr_V f' run i` by metis_tac[] 1162 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 1163 >> `���a. (a,run.E (i,q)) ��� trans (POW (props f)) q` by metis_tac[] 1164 >> `���q'. (q' ��� run.E (i,q)) ��� (q',q) ��� TSF` 1165 by metis_tac[TRANS_REACHES_SUBFORMS] 1166 >> `(x,q) ��� TSF` by metis_tac[] 1167 >> `(q,f1) ��� TSF` by metis_tac[TSF_def,IN_DEF,SUBSET_DEF] 1168 >> metis_tac[TSF_TRANS_LEMM, transitive_def, TSF_def, IN_DEF] 1169 ) 1170 ) 1171 >- (`���i. run_restr_V f' run i ��� run.V i` by metis_tac[SUBSET_UNION] 1172 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 1173 >> fs[run_restr_E_def] 1174 ) 1175 >- (fs[SUBSET_DEF, run_restr_V_def, run_restr_E_def] >> rpt strip_tac 1176 >> Cases_on `q ��� run_restr_V f' run i` >> fs[] 1177 >> `x ��� run_restr_V f' run (SUC i)` suffices_by simp[SUC_ONE_ADD] 1178 >> fs[run_restr_V_def] 1179 >> qexists_tac `run.E (i,q)` >> rpt strip_tac >> fs[] 1180 >> qexists_tac `q` >> fs[] 1181 ) 1182 >- (`run_restr_V f' run i ��� run.V i` by metis_tac[SUBSET_UNION] 1183 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 1184 >> Cases_on `i=0` >> fs[] 1185 >> `(i = 0) ��� ���q'. q ��� run.E (i ��� 1,q') ��� q' ��� run.V (i ��� 1)` 1186 by metis_tac[] >> fs[] 1187 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 1188 >> rw[] >> fs[run_restr_V_def] 1189 >> qexists_tac `q''` >> strip_tac >> fs[] 1190 >> simp[run_restr_E_def] 1191 ) 1192 >- (`infBranchOf run b` by metis_tac[SUBSET_UNION] 1193 >> metis_tac[] 1194 ) 1195 >- (qexists_tac `run_restr f'' run` 1196 >> rpt strip_tac >> fs[run_restr_def, run_restr_V_def] 1197 >- (Induct_on `i` 1198 >- metis_tac[run_restr_V_def, TEMPDNF_TEMPSUBF] 1199 >- (`���i. run_restr_V f'' run i ��� run.V i` by metis_tac[SUBSET_UNION] 1200 >> simp[run_restr_V_def, SUBSET_DEF] >> rpt strip_tac 1201 >> `(s = run.E (i,q)) ��� q ��� run_restr_V f'' run i` by metis_tac[] 1202 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 1203 >> `���a. (a,run.E (i,q)) ��� trans (POW (props f)) q` by metis_tac[] 1204 >> `���q'. (q' ��� run.E (i,q)) ��� (q',q) ��� TSF` 1205 by metis_tac[TRANS_REACHES_SUBFORMS] 1206 >> `(x,q) ��� TSF` by metis_tac[] 1207 >> `(q,f2) ��� TSF` by metis_tac[TSF_def,IN_DEF,SUBSET_DEF] 1208 >> metis_tac[TSF_TRANS_LEMM, transitive_def, TSF_def, IN_DEF] 1209 ) 1210 ) 1211 >- (`���i. run_restr_V f'' run i ��� run.V i` by metis_tac[SUBSET_UNION] 1212 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 1213 >> fs[run_restr_E_def] 1214 ) 1215 >- (fs[SUBSET_DEF, run_restr_V_def, run_restr_E_def] >> rpt strip_tac 1216 >> Cases_on `q ��� run_restr_V f'' run i` >> fs[] 1217 >> `x ��� run_restr_V f'' run (SUC i)` suffices_by simp[SUC_ONE_ADD] 1218 >> fs[run_restr_V_def] 1219 >> qexists_tac `run.E (i,q)` >> rpt strip_tac >> fs[] 1220 >> qexists_tac `q` >> fs[] 1221 ) 1222 >- (`run_restr_V f'' run i ��� run.V i` by metis_tac[SUBSET_UNION] 1223 >> `q ��� run.V i` by metis_tac[SUBSET_DEF] 1224 >> Cases_on `i=0` >> fs[] 1225 >> `(i = 0) ��� ���q'. q ��� run.E (i ��� 1,q') ��� q' ��� run.V (i ��� 1)` 1226 by metis_tac[] >> fs[] 1227 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 1228 >> rw[] >> fs[run_restr_V_def] 1229 >> qexists_tac `q''` >> strip_tac >> fs[] 1230 >> simp[run_restr_E_def] 1231 ) 1232 >- (`infBranchOf run b` by metis_tac[SUBSET_UNION] 1233 >> metis_tac[] 1234 ) 1235 >- (Induct_on `i` 1236 >> fs[run_restr_V_def] 1237 >> fs[SET_EQ_SUBSET] >> rpt strip_tac 1238 >- (simp[SUBSET_DEF] >> rpt strip_tac 1239 >> `((SUC i) = 0) ��� ���q'. x ��� run.E ((SUC i) ��� 1,q') 1240 ��� q' ��� run.V ((SUC i) ��� 1)` by metis_tac[] 1241 >> fs[] 1242 >> `q' ��� run_restr_V f' run i \/ q' ��� run_restr_V f'' run i` 1243 by fs[UNION_DEF, SUBSET_DEF] 1244 >- (`(���s. 1245 x ��� s ��� 1246 ���q. 1247 ((���x. x ��� s ��� x ��� run.E (i,q)) 1248 ��� ���x. x ��� run.E (i,q) ��� x ��� s) ��� 1249 q ��� run_restr_V f' run i)` 1250 suffices_by metis_tac[] 1251 >> qexists_tac `run.E (i,q')` >> fs[] 1252 >> qexists_tac `q'` >> fs[]) 1253 >- (`���s. 1254 x ��� s ��� 1255 ���q. 1256 ((���x. x ��� s ��� x ��� run.E (i,q)) 1257 ��� ���x. x ��� run.E (i,q) ��� x ��� s) ��� 1258 q ��� run_restr_V f'' run i` 1259 suffices_by metis_tac[] 1260 >> qexists_tac `run.E (i,q')` >> fs[] 1261 >> qexists_tac `q'` >> fs[] 1262 ) 1263 ) 1264 >- (simp[BIGUNION, SUBSET_DEF] >> rpt strip_tac 1265 >> (`x ��� run.V (i + 1)` by metis_tac[SUBSET_DEF] 1266 >> metis_tac[SUC_ONE_ADD,ADD_COMM] 1267 )) 1268 >- (simp[BIGUNION, SUBSET_DEF] >> rpt strip_tac 1269 >> `x ��� run.V (i + 1)` by metis_tac[SUBSET_DEF] 1270 >> metis_tac[SUC_ONE_ADD,ADD_COMM]) 1271 ) 1272 ) 1273 ) 1274 ); 1275 1276val TRANS_LEMM1 = store_thm 1277 ("TRANS_LEMM1", 1278 ``!w f' f r. runForAA (ltl2vwaa_free_alph (POW (props f')) f) r w 1279 /\ r.V 0 ��� tempDNF f 1280 ==> (?a. (a, r.V 1) ��� trans (POW (props f')) f 1281 /\ at w 0 ��� a)``, 1282 gen_tac >> gen_tac >> Induct_on `f` 1283 >- (fs[ltl2vwaa_free_alph_def, initForms_def, trans_def, tempDNF_def] 1284 >> fs[trans_def, runForAA_def, validAARunFor_def] 1285 >> rpt strip_tac 1286 >> `���a'. (a',r.E (0,VAR a)) ��� (trans (POW (props f')) (VAR a)) 1287 /\ at w 0 ��� a'` 1288 by metis_tac[IN_SING] >> fs[trans_def] 1289 >- (CCONTR_TAC >> `CHOICE (r.V 1) ��� r.V 1` by metis_tac[CHOICE_DEF] 1290 >> `(1 = 0) ��� ���q'. (CHOICE (r.V 1)) ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1291 by metis_tac[] >> fs[] 1292 >> `q' = VAR a` by metis_tac[IN_SING] 1293 >> fs[] >> metis_tac[NOT_IN_EMPTY]) 1294 >- (metis_tac[]) 1295 ) 1296 >- (fs[ltl2vwaa_free_alph_def, initForms_def, trans_def, tempDNF_def] 1297 >> fs[trans_def, runForAA_def, validAARunFor_def] 1298 >> rpt strip_tac 1299 >> `���a'. (a',r.E (0,N_VAR a)) ��� (trans (POW (props f')) (N_VAR a)) 1300 /\ at w 0 ��� a'` 1301 by metis_tac[IN_SING] >> fs[trans_def] 1302 >- (CCONTR_TAC >> `CHOICE (r.V 1) ��� r.V 1` by metis_tac[CHOICE_DEF] 1303 >> `(1 = 0) ��� ���q'. (CHOICE (r.V 1)) ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1304 by metis_tac[] >> fs[] 1305 >> `q' = N_VAR a` by metis_tac[IN_SING] >> fs[] >> metis_tac[NOT_IN_EMPTY]) 1306 >- (fs[IN_DIFF] >> metis_tac[IN_DIFF]) 1307 >- (metis_tac[IN_DIFF]) 1308 ) 1309 >- (rpt strip_tac 1310 >> `runForAA (ltl2vwaa_free_alph (POW (props f')) f) r w ��� 1311 runForAA (ltl2vwaa_free_alph (POW (props f')) f'') r w` 1312 by metis_tac[RUN_FOR_DISJ_LEMM2] 1313 >- (`r.V 0 ��� tempDNF f` by 1314 (POP_ASSUM mp_tac 1315 >> simp[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 1316 >> rpt strip_tac >> fs[initForms_def] 1317 ) 1318 >> `���a. (a,r.V 1) ��� trans (POW (props f')) f ��� at w 0 ��� a` by metis_tac[] 1319 >> qexists_tac `a` >> fs[trans_def] 1320 ) 1321 >- (`r.V 0 ��� tempDNF f''` by 1322 (POP_ASSUM mp_tac 1323 >> simp[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 1324 >> rpt strip_tac >> fs[initForms_def] 1325 ) 1326 >> `���a. (a,r.V 1) ��� trans (POW (props f')) f'' ��� at w 0 ��� a` by metis_tac[] 1327 >> qexists_tac `a` >> fs[trans_def] 1328 ) 1329 ) 1330 >- (rpt strip_tac 1331 >> `���r1. 1332 runForAA (ltl2vwaa_free_alph (POW (props f')) f) r1 w ��� 1333 ���r2. 1334 runForAA (ltl2vwaa_free_alph (POW (props f')) f'') r2 w ��� 1335 ���i. r.V i = r1.V i ��� r2.V i` 1336 by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 1337 >> simp[trans_def, d_conj_def] 1338 >> `r1.V 0 ��� tempDNF f` by 1339 fs[ltl2vwaa_free_alph_def, runForAA_def, validAARunFor_def, initForms_def] 1340 >> `r2.V 0 ��� tempDNF f''` by 1341 fs[ltl2vwaa_free_alph_def, runForAA_def, validAARunFor_def, initForms_def] 1342 >> `���a. (a,r1.V 1) ��� trans (POW (props f')) f ��� at w 0 ��� a` by metis_tac[] 1343 >> `���a. (a,r2.V 1) ��� trans (POW (props f')) f'' ��� at w 0 ��� a` by metis_tac[] 1344 >> qexists_tac `a ��� a'` >> fs[] 1345 >> qexists_tac `a` >> qexists_tac `a'` 1346 >> qexists_tac `r1.V 1` >> qexists_tac `r2.V 1` 1347 >> fs[] >> strip_tac 1348 ) 1349 >- (rpt strip_tac 1350 >> fs[trans_def, runForAA_def, validAARunFor_def] 1351 >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 1352 >> `���a. (a,r.E (0,X f)) ��� trans (POW (props f')) (X f) ��� at w 0 ��� a` 1353 by metis_tac[IN_SING] 1354 >> fs[trans_def] >> CCONTR_TAC 1355 >> `r.V 1 ��� r.E (0, X f)` by 1356 (simp[SUBSET_DEF] >> rpt strip_tac 1357 >> CCONTR_TAC 1358 >> `(1 = 0) ��� ���q'. x ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1359 by metis_tac[] >> fs[] 1360 >> `q' = X f` by metis_tac[IN_SING] >> fs[] 1361 ) 1362 >> `r.E (0, X f) ��� r.V (0 + 1)` by metis_tac[] >> fs[] 1363 >> `r.E (0, X f) = r.V 1` by metis_tac[SET_EQ_SUBSET] 1364 >> fs[] >> metis_tac[] 1365 ) 1366 >- (rpt strip_tac 1367 >> fs[trans_def, runForAA_def, validAARunFor_def] 1368 >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 1369 >> `���a. (a,r.E (0,U f f'')) ��� trans (POW (props f')) (U f f'') ��� at w 0 ��� a` 1370 by metis_tac[IN_SING] 1371 >> qexists_tac `a` 1372 >> `r.V 1 ��� r.E (0, U f f'')` by 1373 (simp[SUBSET_DEF] >> rpt strip_tac >> fs[] 1374 >> CCONTR_TAC 1375 >> `(1 = 0) ��� ���q'. x ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1376 by metis_tac[] >> fs[] 1377 >> `q' = U f f''` by metis_tac[IN_SING] 1378 >> fs[] 1379 ) 1380 >> `r.E (0, U f f'') ��� r.V (0 + 1)` by metis_tac[] >> fs[] 1381 >> `r.V 1 = r.E (0, U f f'')` by metis_tac[SET_EQ_SUBSET] 1382 >> fs[trans_def] >> metis_tac[] 1383 ) 1384 >- (rpt strip_tac 1385 >> fs[runForAA_def, validAARunFor_def] 1386 >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 1387 >> `���a. (a,r.E (0,R f f'')) ��� trans (POW (props f')) (R f f'') ��� at w 0 ��� a` 1388 by metis_tac[IN_SING] 1389 >> qexists_tac `a` 1390 >> `r.V 1 ��� r.E (0, R f f'')` by 1391 (simp[SUBSET_DEF] >> rpt strip_tac >> fs[] 1392 >> CCONTR_TAC 1393 >> `(1 = 0) ��� ���q'. x ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1394 by metis_tac[] >> fs[] 1395 >> `q' = R f f''` by metis_tac[IN_SING] 1396 >> fs[] 1397 ) 1398 >> `r.E (0, R f f'') ��� r.V (0 + 1)` by metis_tac[] >> fs[] 1399 >> `r.V 1 = r.E (0, R f f'')` by metis_tac[SET_EQ_SUBSET] 1400 >> fs[trans_def] >> metis_tac[] 1401 ) 1402 ); 1403 1404val CONJ_DISJ_DISTRIB = store_thm 1405 ("CONJ_DISJ_DISTRIB", 1406 ``!x f f1 f2 f3. 1407 (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (DISJ f2 f3))) r x) 1408 = ((?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r x) 1409 \/ ?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f3)) r x)``, 1410 rpt strip_tac >> fs[EQ_IMP_THM] >> rpt strip_tac 1411 >- (imp_res_tac RUN_FOR_CONJ_LEMM2_UNION 1412 >> imp_res_tac RUN_FOR_DISJ_LEMM2 1413 >- (`���r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r x` 1414 by metis_tac[RUN_FOR_CONJ_LEMM] >> metis_tac[]) 1415 >- (`���r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f3)) r x` 1416 by metis_tac[RUN_FOR_CONJ_LEMM] >> metis_tac[]) 1417 ) 1418 >- (imp_res_tac RUN_FOR_CONJ_LEMM2_UNION 1419 >> `?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f2 f3)) r x` 1420 by metis_tac[RUN_FOR_DISJ_LEMM] 1421 >> metis_tac[RUN_FOR_CONJ_LEMM] 1422 ) 1423 >- (imp_res_tac RUN_FOR_CONJ_LEMM2_UNION 1424 >> `?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f2 f3)) r x` 1425 by metis_tac[RUN_FOR_DISJ_LEMM] 1426 >> metis_tac[RUN_FOR_CONJ_LEMM] 1427 ) 1428 ); 1429 1430 1431val U_AUTO_CHARACTERISATION = store_thm 1432 ("U_AUTO_CHARACTERISATION", 1433 ``!f f1 f2. 1434 (alterA_lang (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) 1435 = alterA_lang (ltl2vwaa_free_alph (POW (props f)) 1436 (DISJ f2 (CONJ f1 (X (U f1 f2))))))``, 1437 rpt strip_tac >> rw[SET_EQ_SUBSET] >> fs[SUBSET_DEF, alterA_lang_def] 1438 >> rpt strip_tac 1439 >- (`(���run. 1440 runForAA 1441 (ltl2vwaa_free_alph (POW (props f)) 1442 (DISJ f2 (CONJ f1 (X (U f1 f2))))) run x) ��� 1443 ���x'. 1444 x' ��� word_range x ��� 1445 x' ��� 1446 (ltl2vwaa_free_alph (POW (props f)) 1447 (DISJ f2 (CONJ f1 (X (U f1 f2))))).alphabet` 1448 suffices_by metis_tac[] 1449 >> strip_tac 1450 >- (`suff x 0 = x` by (Cases_on `x` >> fs[suff_def] >> metis_tac[]) 1451 >> `!a. (a,run.E (0,U f1 f2)) ��� trans (POW (props f)) f2 ��� at x 0 ��� a ��� 1452 ���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' x` 1453 by metis_tac[REPL_F2_LEMM, SUBSET_REFL] 1454 >> `!a. (a,run.E (0,U f1 f2)) ��� 1455 d_conj (trans (POW (props f)) f1) {(POW (props f),{U f1 f2})} 1456 ��� at x 0 ��� a ��� 1457 ���r'. runForAA 1458 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) r' x` 1459 by metis_tac[U_REPL_F1_LEMM] 1460 >> POP_ASSUM mp_tac 1461 >> POP_ASSUM mp_tac 1462 >> RULE_ASSUM_TAC( 1463 SIMP_RULE (srw_ss())[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def]) 1464 >> fs[initForms_def, tempSubForms_def, tempDNF_def] 1465 >> rpt strip_tac 1466 >> `(U f1 f2) ��� run.V 0` by simp[] 1467 >> `���a. ((a,run.E (0,U f1 f2)) ��� trans (POW (props f)) (U f1 f2)) ��� (at x 0 ��� a)` 1468 by metis_tac[] 1469 >> fs[trans_def] 1470 >- (`���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' x` 1471 by metis_tac[] 1472 >> qexists_tac `r'` 1473 >> metis_tac[RUN_FOR_DISJ_LEMM] 1474 ) 1475 >- (`���r'. runForAA 1476 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) 1477 r' x` 1478 by metis_tac[] 1479 >> qexists_tac `r'` 1480 >> metis_tac[RUN_FOR_DISJ_LEMM] 1481 ) 1482 ) 1483 >- (rpt strip_tac >> fs[ltl2vwaa_free_alph_def]) 1484 ) 1485 >- (`(���run. 1486 runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) run x) ��� 1487 ���x'. 1488 x' ��� word_range x ��� 1489 x' ��� (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)).alphabet` suffices_by metis_tac[] 1490 >> rpt strip_tac 1491 >> `runForAA (ltl2vwaa_free_alph (POW (props f)) f2) run x 1492 \/ runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) run x` 1493 by metis_tac[RUN_FOR_DISJ_LEMM2] 1494 >> `{U f1 f2} ��� tempDNF (U f1 f2)` by fs[tempDNF_def] 1495 >- (`?a. (a,run.V 1) ��� trans (POW (props f)) (U f1 f2) ��� at x 0 ��� a` 1496 suffices_by metis_tac[REPL_IN_0] 1497 >> `run.V 0 ��� tempDNF f2 ��� 1498 ���a. (a,run.V 1) ��� trans (POW (props f)) f2 ��� at x 0 ��� a` 1499 by metis_tac[TRANS_LEMM1] 1500 >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 1501 >> fs[trans_def] 1502 >> `?a. (a,run.V 1) ��� trans (POW (props f)) f2 /\ (at x 0 ��� a)` 1503 suffices_by metis_tac[] 1504 >> `���a. (a,run.V 1) ��� trans (POW (props f)) f2 ��� (at x 0 ��� a)` 1505 by metis_tac[initForms_def] 1506 >> qexists_tac `a` >> fs[]) 1507 >- (`?a. (a,run.V 1) ��� trans (POW (props f)) (U f1 f2) ��� at x 0 ��� a` 1508 suffices_by metis_tac[REPL_IN_0] 1509 >> `run.V 0 ��� tempDNF (CONJ f1 (X (U f1 f2))) ��� 1510 ���a. (a,run.V 1) ��� trans (POW (props f)) (CONJ f1 (X (U f1 f2))) 1511 ��� at x 0 ��� a` 1512 by metis_tac[TRANS_LEMM1] 1513 >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 1514 >> fs[trans_def] 1515 >> `?a. (a,run.V 1) ��� 1516 d_conj (trans (POW (props f)) f1) {(POW (props f),{U f1 f2})} 1517 ��� at x 0 ��� a` suffices_by metis_tac[] 1518 >> `���a. 1519 (a,run.V 1) ��� 1520 d_conj (trans (POW (props f)) f1) 1521 (��s. ���e. (s = (POW (props f),e)) ��� e ��� tempDNF (U f1 f2)) ��� 1522 at x 0 ��� a` by metis_tac[initForms_def] 1523 >> qexists_tac `a` >> fs[tempDNF_def] 1524 >> `(��s. (s = (POW (props f),{U f1 f2}))) 1525 = {(POW (props f), {U f1 f2})}` by 1526 (CCONTR_TAC >> fs[NOT_EQUAL_SETS] >> metis_tac[]) 1527 >> fs[] 1528 ) 1529 >- (fs[ltl2vwaa_free_alph_def]) 1530 >- (fs[ltl2vwaa_free_alph_def]) 1531 ) 1532 ); 1533 1534val R_AUTO_CHARACTERISATION = store_thm 1535 ("R_AUTO_CHARACTERISATION", 1536 ``!f f1 f2. alterA_lang (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) = 1537 alterA_lang (ltl2vwaa_free_alph (POW (props f)) 1538 (CONJ f2 (DISJ f1 (X (R f1 f2)))))``, 1539 rpt strip_tac >> rw[SET_EQ_SUBSET] >> fs[SUBSET_DEF, alterA_lang_def] 1540 >> rpt strip_tac 1541 >- (`(���run. 1542 runForAA 1543 (ltl2vwaa_free_alph (POW (props f)) 1544 (CONJ f2 (DISJ f1 (X (R f1 f2))))) run x) ��� 1545 ���x'. 1546 x' ��� word_range x ��� 1547 x' ��� 1548 (ltl2vwaa_free_alph (POW (props f)) 1549 (CONJ f2 (DISJ f1 (X (R f1 f2))))).alphabet` 1550 suffices_by metis_tac[] 1551 >> strip_tac 1552 >> `!a qs f1 f2. 1553 (a,qs) ��� trans (POW (props f)) f1 ��� at x 0 ��� a ��� qs ��� run.E (0,f2) ��� 1554 ���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f1) r' (suff x 0)` 1555 by metis_tac[REPL_F2_LEMM] 1556 >> `!a. (a,run.E (0,R f1 f2)) ��� 1557 d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})} ��� 1558 at x 0 ��� a ��� 1559 ���r'. 1560 runForAA 1561 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) r' 1562 (suff x 0)` 1563 by metis_tac[R_REPL_F1_LEMM] 1564 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 1565 >> RULE_ASSUM_TAC( 1566 SIMP_RULE 1567 (srw_ss())[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def]) 1568 >> rpt strip_tac 1569 >> fs[trans_def] 1570 >- (`?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 f1)) r x 1571 \/ ?r. runForAA 1572 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) r x` 1573 suffices_by metis_tac[CONJ_DISJ_DISTRIB] 1574 >> fs[initForms_def, tempDNF_def] 1575 >> `R f1 f2 ��� run.V 0` by metis_tac[IN_SING] 1576 >> `���a. (a,run.E (0,R f1 f2)) ��� trans (POW (props f)) (R f1 f2) 1577 ��� at x 0 ��� a` 1578 by metis_tac[] 1579 >> fs[trans_def] 1580 >> `((a,run.E (0,R f1 f2)) ��� 1581 d_conj (trans (POW (props f)) f2) (trans (POW (props f)) f1)) 1582 \/ (a,run.E (0,R f1 f2)) ��� 1583 d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})}` 1584 by metis_tac[D_CONJ_UNION_DISTR, IN_UNION] 1585 >- (POP_ASSUM mp_tac >> simp[d_conj_def] 1586 >> rpt strip_tac 1587 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f1) r' (suff x 0)` 1588 by metis_tac[IN_INTER,SUBSET_UNION] 1589 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' (suff x 0)` 1590 by metis_tac[IN_INTER,SUBSET_UNION] 1591 >> `suff x 0 = x` 1592 by (Cases_on `x` >> fs[suff_def] >> metis_tac[]) 1593 >> `?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 f1)) r x` 1594 by metis_tac[RUN_FOR_CONJ_LEMM] 1595 >> dsimp[] >> metis_tac[] 1596 ) 1597 >- (`suff x 0 = x` 1598 by (Cases_on `x` >> fs[suff_def] >> metis_tac[]) 1599 >> dsimp[] >> metis_tac[]) 1600 ) 1601 >- fs[ltl2vwaa_free_alph_def] 1602 ) 1603 >- (`(���run. 1604 runForAA 1605 (ltl2vwaa_free_alph (POW (props f)) 1606 (R f1 f2)) run x) ��� 1607 ���x'. 1608 x' ��� word_range x ��� 1609 x' ��� 1610 (ltl2vwaa_free_alph (POW (props f)) 1611 (R f1 f2)).alphabet` 1612 suffices_by metis_tac[] >> rpt strip_tac 1613 >- (`{R f1 f2} ��� tempDNF (R f1 f2)` by fs[tempDNF_def] 1614 >> `run.V 0 ��� tempDNF (CONJ f2 (DISJ f1 (X (R f1 f2)))) ��� 1615 ���a. (a,run.V 1) ��� trans (POW (props f)) 1616 (CONJ f2 (DISJ f1 (X (R f1 f2)))) 1617 ��� at x 0 ��� a` by metis_tac[TRANS_LEMM1] 1618 >> `?a.(a,run.V 1) ��� trans (POW (props f)) (R f1 f2) ��� at x 0 ��� a` 1619 suffices_by metis_tac[REPL_IN_0] 1620 >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def, initForms_def] 1621 >> `���a. 1622 (a,run.V 1) ��� 1623 trans (POW (props f)) (CONJ f2 (DISJ f1 (X (R f1 f2)))) 1624 ��� at x 0 ��� a` by fs[] 1625 >> fs[trans_def, tempDNF_def] 1626 >> qexists_tac `a` >> fs[] 1627 >> `(��s. s = (POW (props f),{R f1 f2})) 1628 = {(POW (props f),{R f1 f2})}` suffices_by (rpt strip_tac >> fs[]) 1629 >> fs[SET_EQ_SUBSET, SUBSET_DEF] 1630 ) 1631 >- fs[ltl2vwaa_free_alph_def] 1632 ) 1633 ); 1634 1635 1636 1637val RUN_FOR_X_LEMM = store_thm 1638 ("RUN_FOR_X_LEMM", 1639 ``!r f g x. runForAA (ltl2vwaa_free_alph (POW (props f)) g) r (suff x 1) 1640 /\ word_range x ��� POW (props f) 1641 ==> ?r'. runForAA (ltl2vwaa_free_alph (POW (props f)) (X g)) r' x``, 1642 rpt strip_tac >> fs[runForAA_def] 1643 >> qabbrev_tac `r_new = ALTERA_RUN 1644 (\i. if i = 0 then {X g} else r.V (i-1)) 1645 (��(i,q). if i = 0 then r.V 0 else r.E (i-1,q))` 1646 >> qexists_tac `r_new` 1647 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f)) (X g)) r_new x ��� 1648 (validAARunFor (ltl2vwaa_free_alph (POW (props f)) (X g)) r_new x 1649 ==> acceptingAARun (ltl2vwaa_free_alph (POW (props f)) (X g)) r_new)` 1650 suffices_by metis_tac[] 1651 >> conj_tac 1652 >- (fs[validAARunFor_def] >> rpt strip_tac >> fs[ltl2vwaa_free_alph_def] 1653 >> fs[tempDNF_def, initForms_def, tempSubForms_def] 1654 >- (qunabbrev_tac `r_new` >> fs[]) 1655 >- (Cases_on `i` >> qunabbrev_tac `r_new` >> fs[SUBSET_DEF] >> rpt strip_tac 1656 >> metis_tac[]) 1657 >- (Cases_on `i` >> qunabbrev_tac `r_new` >> fs[] 1658 >- (qexists_tac `POW (props f)` >> strip_tac 1659 >- (fs[trans_def]) 1660 >- (metis_tac[AT_WORD_RANGE, SUBSET_DEF]) 1661 ) 1662 >- (`?a. (a,r.E (n,q)) ��� trans (POW (props f)) q ��� at (suff x 1) n ��� a` 1663 by metis_tac[] 1664 >> qexists_tac `a` >> strip_tac >> fs[] 1665 >> `SUC n = n + 1` by simp[] 1666 >> metis_tac[AT_SUFF_LEMM] 1667 ) 1668 ) 1669 >- (Cases_on `i` >> qunabbrev_tac `r_new` >> fs[SUBSET_DEF] 1670 >> rpt strip_tac 1671 >> `x' ��� r.V (n + 1)` by metis_tac[] 1672 >> `SUC n = n + 1` by simp[] >> rw[] 1673 ) 1674 >- (Cases_on `i = 0` >> fs[] >> qunabbrev_tac `r_new` 1675 >> fs[] 1676 >> Cases_on `i = 1` 1677 >- (qexists_tac `X g` >> fs[]) 1678 >- (`~(0 = 1)` by simp[] 1679 >> `((i - 1) = 0) \/ ���q'. q ��� r.E (((i - 1) - 1),q') 1680 ��� q' ��� r.V ((i - 1) - 1)` 1681 by metis_tac[] 1682 >> fs[] 1683 >> `((i - 1) = 0) ��� ���q'. q ��� r.E ((i - 1) ��� 1,q') 1684 ��� q' ��� r.V ((i - 1) ��� 1)` 1685 by metis_tac[] >> fs[] 1686 >> `~(i <= 1)` by simp[] 1687 >> qexists_tac `q''` >> fs[]) 1688 ) 1689 ) 1690 >- (strip_tac 1691 >> `���b x'. infBranchOf r_new b ��� branchFixP b x' 1692 ��� x' ��� (ltl2vwaa_free_alph (POW (props f)) (X g)).final` 1693 suffices_by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1694 >> rpt strip_tac 1695 >> `���b x'. infBranchOf r b ��� branchFixP b x' 1696 ��� x' ��� (ltl2vwaa_free_alph (POW (props f)) g).final` 1697 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1698 >> qabbrev_tac `b' = \i. b (i + 1)` 1699 >> `x' ��� {U f1 f2 | U f1 f2 ��� tempSubForms (X g)}` 1700 by fs[ltl2vwaa_free_alph_def, finalForms_def] 1701 >> `x' ��� {U f1 f2 | U f1 f2 ��� tempSubForms g}` by fs[tempSubForms_def] 1702 >> `x' ��� (ltl2vwaa_free_alph (POW (props f)) g).final` 1703 by fs[ltl2vwaa_free_alph_def, finalForms_def] 1704 >> `infBranchOf r b' /\ branchFixP b' x'` 1705 suffices_by metis_tac[ltl2vwaa_free_alph_def, finalForms_def, tempSubForms_def] 1706 >> strip_tac 1707 >- (fs[infBranchOf_def] >> rpt strip_tac >> fs[] 1708 >- (qunabbrev_tac `b'` >> qunabbrev_tac `r_new` >> fs[] 1709 >> `0 + 1 = 1` by simp[] >> metis_tac[]) 1710 >- (qunabbrev_tac `b'` >> qunabbrev_tac `r_new` >> fs[] 1711 >> `b ((i + 1) + 1) ��� 1712 if (i + 1) = 0 then r.V 0 else r.E ((i + 1) ��� 1,b (i +1))` 1713 by metis_tac[] >> fs[]) 1714 ) 1715 >- (fs[branchFixP_def] >> qexists_tac `i-1` 1716 >> fs[] >> qunabbrev_tac `b'` >> fs[] 1717 ) 1718 ) 1719 ); 1720 1721val RUN_FOR_X_LEMM2 = store_thm 1722 ("RUN_FOR_X_LEMM2", 1723 ``!r x f g. runForAA (ltl2vwaa_free_alph (POW (props f)) (X g)) r x 1724 ==> ���run. runForAA (ltl2vwaa_free_alph (POW (props f)) g) run (suff x 1)``, 1725 rpt strip_tac >> fs[runForAA_def] 1726 >> qabbrev_tac `r_new = ALTERA_RUN (\i. r.V (i + 1)) (��(i,q). r.E(i+1,q))` 1727 >> qexists_tac `r_new` 1728 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f)) g) r_new (suff x 1) ��� 1729 (validAARunFor (ltl2vwaa_free_alph (POW (props f)) g) r_new (suff x 1) 1730 ==> acceptingAARun (ltl2vwaa_free_alph (POW (props f)) g) r_new)` 1731 suffices_by metis_tac[] 1732 >> conj_tac 1733 >- (fs[validAARunFor_def, ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 1734 >> `X g ��� r.V 0` by simp[] 1735 >> `���a. (a,r.E (0,X g)) ��� trans (POW (props f)) (X g)` by metis_tac[] 1736 >> fs[trans_def] 1737 >> qunabbrev_tac `r_new` >> fs[] 1738 >> `!q. q ��� r.V 1 ==> (1 = 0) \/ 1739 ���q'. q ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1740 by metis_tac[] >> fs[] 1741 >> `!q. (q ��� r.V 1) ==> (q ��� r.E(0,X g))` by metis_tac[IN_SING] 1742 >> `r.V 1 ��� r.E (0, X g)` by metis_tac[SUBSET_DEF] 1743 >> `0 + 1 = 1` by simp[] 1744 >> `r.V 1 = r.E (0, X g)` by metis_tac[SUBSET_ANTISYM] 1745 >> rpt strip_tac >> fs[] 1746 >- (Induct_on `i` >> fs[tempSubForms_def, tempDNF_def] 1747 >- metis_tac[TEMPDNF_TEMPSUBF] 1748 >- (fs[SUBSET_DEF] >> rpt strip_tac 1749 >> `(((SUC i) + 1) = 0) ��� ���q'. x' ��� r.E (((SUC i) + 1) ��� 1,q') 1750 ��� q' ��� r.V (((SUC i) + 1) ��� 1)` 1751 by metis_tac[] >> fs[] 1752 >> `���a. (a,r.E ((SUC i),q')) ��� trans (POW (props f)) q'` 1753 by metis_tac[] 1754 >> `(x',q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 1755 >> `SUC i = i + 1` by simp[] 1756 >> `(q',g) ��� TSF` by metis_tac[TSF_def, IN_DEF] 1757 >> `(x',g) ��� TSF` by metis_tac[TSF_TRANS_LEMM, IN_DEF, transitive_def] 1758 >> metis_tac[TSF_def, IN_DEF] 1759 ) 1760 ) 1761 >- (`���a. (a,r.E ((i + 1),q)) ��� trans (POW (props f)) q ��� at x (i + 1) ��� a` 1762 by metis_tac[] 1763 >> qexists_tac `a'` >> fs[] >> metis_tac[AT_SUFF_LEMM] 1764 ) 1765 >- (`r.E (i + 1,q) ��� r.V ((i + 1) + 1)` by metis_tac[] >> fs[]) 1766 >- (Cases_on `i = 0` >> fs[] 1767 >> `(i + 1) - 1 = i` by simp[] 1768 >> `~(i + 1 = 0)` by simp[] >> metis_tac[] 1769 ) 1770 ) 1771 >- (strip_tac 1772 >> `���b x. infBranchOf r_new b ��� branchFixP b x 1773 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) g).final` 1774 suffices_by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1775 >> rpt strip_tac 1776 >> `���b x. infBranchOf r b ��� branchFixP b x 1777 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (X g)).final` 1778 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1779 >> `!i. b i ��� r_new.V i` by metis_tac[BRANCH_V_LEMM] 1780 >> fs[ltl2vwaa_free_alph_def, finalForms_def, tempSubForms_def] 1781 >> qabbrev_tac `b' = \i. if i = 0 then X g else b (i - 1)` 1782 >> `infBranchOf r b' ��� branchFixP b' x'` suffices_by metis_tac[] 1783 >> strip_tac 1784 >- (fs[infBranchOf_def] >> qunabbrev_tac `b'` >> qunabbrev_tac `r_new` 1785 >> rpt strip_tac >> fs[validAARunFor_def, initForms_def, tempDNF_def] 1786 >> Cases_on `i = 0` >> fs[] 1787 >- (`b 0 ��� r.V (0 + 1)` by metis_tac[] >> fs[] 1788 >> `(1 = 0) ��� ���q'. b 0 ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1789 by metis_tac[] >> fs[] 1790 >> metis_tac[IN_SING] 1791 ) 1792 >- (`?j. i = SUC j` by (Cases_on `i` >> fs[]) 1793 >> `i = j +1` by simp[] 1794 >> `b i ��� r.E (i,b j)` by metis_tac[] 1795 >> fs[] 1796 ) 1797 ) 1798 >- (fs[branchFixP_def] >> qexists_tac `i+1` 1799 >> qunabbrev_tac `b'` >> fs[] 1800 ) 1801 ) 1802 ); 1803 1804val EVTL_F2_TRANS_LEMM = store_thm 1805 ("EVTL_F2_TRANS_LEMM", 1806 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w 1807 ==> (?n a. (a, r.E (n, U f1 f2)) ��� trans (POW (props f)) f2 1808 ��� at w n ��� a)``, 1809 rpt strip_tac >> fs[runForAA_def] 1810 >> `���b x. infBranchOf r b ��� branchFixP b x 1811 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)).final` 1812 by metis_tac[LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM, BRANCH_ACC_LEMM] 1813 >> CCONTR_TAC 1814 >> fs[validAARunFor_def] 1815 >> `!i. U f1 f2 ��� r.V i` by ( 1816 Induct_on `i` >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 1817 >> `���a. (a,r.E (i,U f1 f2)) ��� trans (POW (props f)) (U f1 f2) 1818 ��� (at w i ��� a)` by metis_tac[] 1819 >> fs[trans_def] 1820 >- (metis_tac[]) 1821 >- (fs[d_conj_def] 1822 >> `U f1 f2 ��� r.E (i, U f1 f2)` by metis_tac[IN_UNION, IN_SING] 1823 >> `U f1 f2 ��� r.V (i + 1)` by metis_tac[SUBSET_DEF] 1824 >> metis_tac[SUC_ONE_ADD,ADD_COMM] 1825 ) 1826 ) 1827 >> `!i. U f1 f2 ��� r.E (i, U f1 f2)` by ( 1828 CCONTR_TAC >> fs[] 1829 >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 1830 >> `(i = 0) ��� ���q'. (U f1 f2) ��� r.E (i ��� 1,q') ��� q' ��� r.V (i ��� 1)` 1831 by metis_tac[] 1832 >- (rw[] 1833 >> `U f1 f2 ��� r.V 0` by metis_tac[IN_SING] 1834 >> `(1 = 0) ��� ���q'. (U f1 f2) ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)` 1835 by metis_tac[] >> fs[] 1836 >> `q' = U f1 f2` by metis_tac[IN_SING] >> fs[] 1837 ) 1838 >- (`U f1 f2 ��� r.V i` by fs[] 1839 >> `���a. (a,r.E (i,(U f1 f2))) ��� trans (POW (props f)) (U f1 f2) 1840 ��� at w i ��� a` by metis_tac[] 1841 >> fs[trans_def] 1842 >- (metis_tac[]) 1843 >- (fs[d_conj_def] 1844 >> `U f1 f2 ��� r.E (i, U f1 f2)` by metis_tac[IN_UNION, IN_SING] 1845 >> `U f1 f2 ��� r.V (i + 1)` by metis_tac[SUBSET_DEF] 1846 >> metis_tac[SUC_ONE_ADD,ADD_COMM] 1847 ) 1848 ) 1849 ) 1850 >> `infBranchOf r (\_. U f1 f2)` by fs[infBranchOf_def] 1851 >> `branchFixP (\_. U f1 f2) (U f1 f2)` by fs[branchFixP_def] 1852 >> fs[ltl2vwaa_free_alph_def, finalForms_def] 1853 >> `U f1 f2 ��� U f1 f2 ��� U f1 f2 ��� tempSubForms (U f1 f2)` 1854 by metis_tac[] 1855 >> fs[tempSubForms_def] 1856 ); 1857 1858val ALL_F1_BEFORE_F2 = store_thm 1859 ("ALL_F1_BEFORE_F2", 1860 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w 1861 ==> ?n a. (a, r.E (n, U f1 f2)) ��� trans (POW (props f)) f2 1862 ��� at w n ��� a 1863 ��� (!i. i < n ==> ?a'. (a', r.E (i, U f1 f2)) ��� 1864 d_conj (trans (POW (props f)) f1) {(POW (props f), {U f1 f2})} 1865 ��� at w i ��� a')``, 1866 rpt strip_tac 1867 >> imp_res_tac (SIMP_RULE bool_ss [LEAST_EXISTS] EVTL_F2_TRANS_LEMM) 1868 >> qabbrev_tac `N = LEAST n. (���a. 1869 (a,r.E (n,U f1 f2)) ��� trans (POW (props f)) f2 ��� 1870 at w n ��� a)` 1871 >> qexists_tac `N` >> qexists_tac `a` 1872 >> simp[] 1873 >> CCONTR_TAC >> fs[] 1874 >> `!j. j < N ==> U f1 f2 ��� r.V j` by ( 1875 Induct_on `j` 1876 >- (fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def, initForms_def] 1877 >> metis_tac[tempDNF_def, IN_SING] 1878 ) 1879 >- (strip_tac >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def, trans_def] 1880 >> `���a'. (a',r.E (j,U f1 f2)) ��� trans (POW (props f)) (U f1 f2) ��� at w j ��� a'` 1881 by metis_tac[] 1882 >> fs[trans_def] 1883 >- metis_tac[DECIDE ``SUC j < N ==> j < N``] 1884 >- (fs[d_conj_def] 1885 >> metis_tac[DECIDE ``SUC j = j + 1``, SUBSET_DEF,IN_UNION,IN_SING]) 1886 ) 1887 ) 1888 >> `U f1 f2 ��� r.V i` by fs[] 1889 >> fs[runForAA_def,validAARunFor_def,ltl2vwaa_free_alph_def,trans_def] 1890 >> `���a'. (a',r.E (i,(U f1 f2))) ��� trans (POW (props f)) (U f1 f2) ��� at w i ��� a'` 1891 by metis_tac[] 1892 >> fs[trans_def] 1893 >> metis_tac[] 1894 ); 1895 1896val EVTL_F2_RUN_LEMM = store_thm 1897 ("EVTL_F2_RUN_LEMM", 1898 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w 1899 ==> ?r' n. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' (suff w n) 1900 ��� !i. i < n ==> ?r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f1) r' (suff w i)``, 1901 rpt strip_tac 1902 >> `���n a. (a,r.E (n,U f1 f2)) ��� trans (POW (props f)) f2 ��� at w n ��� a 1903 ��� (!i. i < n ==> ?a'. (a', r.E (i, U f1 f2)) ��� 1904 d_conj (trans (POW (props f)) f1) {(POW (props f), {U f1 f2})} 1905 ��� at w i ��� a')` 1906 by metis_tac[ALL_F1_BEFORE_F2] 1907 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' (suff w n)` 1908 by metis_tac[REPL_F2_LEMM, SUBSET_REFL] 1909 >> qexists_tac `r'` >> qexists_tac `n` >> simp[] 1910 >> rpt strip_tac 1911 >> `���a'. 1912 (a',r.E (i,U f1 f2)) ��� 1913 d_conj (trans (POW (props f)) f1) 1914 {(POW (props f),{U f1 f2})} ��� at w i ��� a'` 1915 by fs[] 1916 >> imp_res_tac U_REPL_F1_LEMM 1917 >> metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 1918 ); 1919 1920val always_run_cond_def = Define ` 1921 always_run_cond f1 f2 rs s i q = 1922 if q ��� s 1923 then (if q = R f1 f2 1924 then {R f1 f2} ��� ((rs i).V 1) 1925 else let j = (LEAST j. q ��� (rs j).V (i-j)) in 1926 (rs j).E (i-j,q)) 1927 else {}` 1928 1929val always_run_V_def = Define ` 1930 (always_run_V f1 f2 rs 0 = {R f1 f2}) 1931 ��� (always_run_V f1 f2 rs (SUC i) = 1932 {R f1 f2} ��� {q | ?q'. q' ��� always_run_V f1 f2 rs i 1933 ��� q ��� always_run_cond f1 f2 rs (always_run_V f1 f2 rs i) i q'} 1934 )` 1935 1936val always_run_E_def = Define ` 1937 always_run_E f1 f2 rs (i,q) = 1938 always_run_cond f1 f2 rs (always_run_V f1 f2 rs i) i q` 1939 1940val always_run_def = Define ` 1941 always_run f1 f2 rs = ALTERA_RUN (always_run_V f1 f2 rs) (always_run_E f1 f2 rs)` 1942 1943val ALWAYS_RUN_LEMM1 = store_thm 1944 ("ALWAYS_RUN_LEMM1", 1945 ``���f' f1 f2 w rs. 1946 (!n. runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n)) 1947 ==> (!i q. q ��� always_run_V f1 f2 rs i /\ ~(q = R f1 f2) 1948 ==> (LEAST j. q ��� (rs j).V (i ��� j)) < i)``, 1949 rpt gen_tac >> strip_tac >> Induct_on `i` 1950 >> rpt strip_tac >> fs[always_run_V_def] >> rpt strip_tac 1951 >> Cases_on `q' = R f1 f2` 1952 >- (`q ��� {R f1 f2} ��� (rs i).V 1` by metis_tac[always_run_cond_def] 1953 >> `q ��� (rs i).V 1` by metis_tac[IN_UNION,IN_SING] 1954 >> fs[] >> numLib.LEAST_ELIM_TAC >> rpt strip_tac 1955 >- (qexists_tac `i` >> simp[]) 1956 >- (CCONTR_TAC >> fs[SUC_ONE_ADD] 1957 >> `i < n` by simp[] 1958 >> `q ��� (rs i).V (i + 1 - i)` by metis_tac[] 1959 >> fs[] 1960 ) 1961 ) 1962 >- (`q ��� (rs (LEAST j. q' ��� (rs j).V (i ��� j))).E 1963 (i ��� (LEAST j. q' ��� (rs j).V (i ��� j)),q')` 1964 by metis_tac[always_run_cond_def] 1965 >> qabbrev_tac `N' = (LEAST j. q' ��� (rs j).V (i ��� j))` 1966 >> `N' < i` by metis_tac[] 1967 >> numLib.LEAST_ELIM_TAC >> rpt strip_tac 1968 >- (fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 1969 >> `(rs N').E (i-N',q') ��� (rs N').V ((i-N') + 1)` 1970 by metis_tac[] 1971 >> qexists_tac `N'` >> fs[SUB] 1972 >> `q ��� (rs N').V (i ��� N' + 1)` by metis_tac[SUBSET_DEF] 1973 >> fs[SUC_ONE_ADD] 1974 >> `i - N' + 1 = i + 1 - N'` by simp[] >> metis_tac[] 1975 ) 1976 >- (CCONTR_TAC >> `N' < n` by simp[] 1977 >> `q ��� (rs N').V (SUC i ��� N')` by metis_tac[] 1978 >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 1979 >> `(rs N').E (i - N',q') ��� (rs N').V (i - N' + 1)` by fs[] 1980 >> `q ��� (rs N').V (i - N' + 1)` by metis_tac[SUBSET_DEF] 1981 >> `SUC i - N' = i - N' + 1` by simp[] 1982 >> metis_tac[] 1983 ) 1984 ) 1985 ); 1986 1987val ALWAYS_RUN_LEMM2 = store_thm 1988 ("ALWAYS_RUN_LEMM2", 1989 ``���f' f1 f2 w rs. 1990 (!n .runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n)) 1991 ==> (!i q. q ��� always_run_V f1 f2 rs i /\ ~(q = R f1 f2) 1992 ==> 1993 let N = LEAST j. q ��� (rs j).V (i - j) 1994 in q ��� (rs N).V (i - N))``, 1995 rpt gen_tac >> strip_tac >> Induct_on `i` 1996 >- (rpt strip_tac >> fs[] >> fs[always_run_V_def]) 1997 >- (rpt strip_tac >> fs[always_run_V_def] >> Cases_on `q' = R f1 f2` 1998 >- (`q ��� {R f1 f2} ��� (rs i).V 1` 1999 by metis_tac[always_run_cond_def] 2000 >> numLib.LEAST_ELIM_TAC >> rpt strip_tac 2001 >> qexists_tac `i` >> fs[] >> fs[] 2002 ) 2003 >- (fs[always_run_V_def] 2004 >> qabbrev_tac `N = LEAST j. q' ��� (rs j).V (i ��� j)` 2005 >> `q ��� (rs N).E (i-N,q')` by metis_tac[always_run_cond_def] 2006 >> numLib.LEAST_ELIM_TAC >> rpt strip_tac 2007 >> qexists_tac `N` 2008 >> `N < i` by metis_tac[ALWAYS_RUN_LEMM1] 2009 >> fs[runForAA_def, validAARunFor_def] 2010 >> `(rs N).E (i - N,q') ��� (rs N).V ((i - N) + 1)` by metis_tac[] 2011 >> `i - N + 1 = SUC i - N` by simp[] 2012 >> metis_tac[SUBSET_DEF] 2013 ) 2014 ) 2015 ); 2016 2017val LEQ_CHAIN_FIXP = store_thm 2018 ("LEQ_CHAIN_FIXP", 2019 ``!f n. (!i. i >= n ==> f (i + 1) <= f i) 2020 ==> (?k. k ��� minimal_elements { f l | n <= l } 2021 (rrestrict (rel_to_reln $<=) { f l | n <= l }))``, 2022 rpt strip_tac 2023 >> `linear_order (rrestrict (rel_to_reln $<=) {f l | n <= l}) {f l | n <= l}` by ( 2024 fs[linear_order_def] >> rpt strip_tac 2025 >- (fs[SUBSET_DEF, domain_def, rrestrict_def] >> rpt strip_tac 2026 >> metis_tac[]) 2027 >- (fs[SUBSET_DEF, range_def, rrestrict_def] >> rpt strip_tac 2028 >> metis_tac[]) 2029 >- (fs[transitive_def, rrestrict_def, rel_to_reln_def] >> rpt strip_tac) 2030 >- (fs[antisym_def, rrestrict_def, rel_to_reln_def]) 2031 >- (fs[rrestrict_def, rel_to_reln_def] >> Cases_on `f l <= f l'` 2032 >- (disj1_tac >> strip_tac >> fs[] >> metis_tac[]) 2033 >- (fs[] >> metis_tac[]) 2034 ) 2035 ) 2036 >> `!k l. k >= l ��� l >= n ==> f k <= f l` by ( 2037 Induct_on `k` 2038 >- (rpt strip_tac >> fs[] >> `l = 0` by simp[] >> fs[]) 2039 >- (rpt strip_tac >> Cases_on `SUC k = l` >> fs[] 2040 >> `k >= l` by simp[] >> `f k <= f l` by simp[] 2041 >> `f (SUC k) <= f k` suffices_by simp[] 2042 >> `k >= n` by simp[] 2043 >> metis_tac[DECIDE ``SUC k = k + 1``] 2044 ) 2045 ) 2046 >> `FINITE { f l | n <= l }` by ( 2047 `{ f l | n <= l } ��� count (f n + 1)` by ( 2048 fs[SUBSET_DEF, count_def] >> rpt strip_tac 2049 >> `x <= f n` suffices_by (rpt strip_tac >> fs[LESS_OR_EQ]) 2050 >> rw[] 2051 ) 2052 >> metis_tac[SUBSET_FINITE,FINITE_COUNT] 2053 ) 2054 >> `~({ f l | n <= l } = {})` by ( 2055 `f n ��� { f l | n <= l }` by ( 2056 fs[] >> qexists_tac `n` >> fs[] 2057 ) >> metis_tac[NOT_IN_EMPTY] 2058 ) 2059 >> metis_tac[finite_linear_order_has_minimal] 2060 ); 2061 2062val ALWAYS_RUN_ACC_LEMM = store_thm 2063 ("ALWAYS_RUN_ACC_LEMM", 2064 ``���f' f1 f2 w rs. 2065 (!n .runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n)) 2066 ��� validAARunFor (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) (always_run f1 f2 rs) w 2067 ==> (!b x. infBranchOf (always_run f1 f2 rs) b ��� branchFixP b x 2068 ��� ~(x = R f1 f2) 2069 ==> ?b' i. infBranchOf (rs i) b' ��� branchFixP b' x)``, 2070 rpt strip_tac 2071 >> imp_res_tac BRANCH_V_LEMM 2072 >> fs[branchFixP_def] 2073 >> `!m. m >= i ==> x ��� (always_run f1 f2 rs).V m` by metis_tac[] 2074 >> fs[always_run_def] 2075 >> `!m. m >= i ==> (let N = LEAST j. x ��� (rs j).V (m - j) 2076 in x ��� (rs N).V (m - N))` 2077 by metis_tac[ALWAYS_RUN_LEMM2] 2078 >> fs[] 2079 >> qabbrev_tac `N = \m. LEAST j. x ��� (rs j).V (m - j)` 2080 >> `!k. k >= i ==> N (k + 1) <= N k` by ( 2081 rpt strip_tac 2082 >> `x ��� (rs (N k)).V (k - (N k))` by fs[] 2083 >> `x ��� (always_run f1 f2 rs).E (k, x)` by ( 2084 fs[infBranchOf_def, always_run_def] 2085 >> `b (k+1) = x` by simp[] >> metis_tac[] 2086 ) 2087 >> `x ��� (rs (N k)).E (k - N k, x)` by ( 2088 fs[always_run_def, always_run_E_def, always_run_cond_def] 2089 >> metis_tac[] 2090 ) 2091 >> `x ��� (rs (N k)).V ((k - N k) + 1)` 2092 by metis_tac[runForAA_def,validAARunFor_def,SUBSET_DEF] 2093 >> `N k < k` by metis_tac[ALWAYS_RUN_LEMM1] 2094 >> `(k - N k) + 1 = (k + 1) - N k` by fs[SUB_LEFT_ADD, ADD_COMM] 2095 >> `x ��� (rs (N k)).V ((k + 1) - N k)` by fs[] 2096 >> CCONTR_TAC >> `N k < N (k + 1)` by simp[] 2097 >> qunabbrev_tac `N` >> POP_ASSUM mp_tac 2098 >> simp[] >> strip_tac 2099 >> imp_res_tac LESS_LEAST 2100 >> POP_ASSUM mp_tac >> simp[] >> metis_tac[] 2101 ) 2102 >> `���k. 2103 k ��� 2104 minimal_elements {N l | i <= l} 2105 (rrestrict (rel_to_reln $<=) {N l | i <= l})` by metis_tac[LEQ_CHAIN_FIXP] 2106 >> `?j. (k = N j) /\ (i <= j)` by ( 2107 fs[minimal_elements_def, rrestrict_def, rel_to_reln_def] 2108 >> metis_tac[] 2109 ) 2110 >> `!h. h >= j ==> x ��� (rs (N j)).V (h - N j) ��� (N h = N j)` by ( 2111 strip_tac >> strip_tac 2112 >> `h >= i` by simp[] 2113 >> `x ��� 2114 (rs (LEAST j. x ��� (rs j).V (h ��� j))).V 2115 (h ��� LEAST j. x ��� (rs j).V (h ��� j))` by metis_tac[] 2116 >> `x ��� (rs (N h)).V (h - N h)` by fs[] 2117 >> `N j = N h` suffices_by metis_tac[] 2118 >> `!a b. a >= b ��� b >= i ==> N a <= N b` by ( 2119 Induct_on `a` 2120 >- (rpt strip_tac >> fs[] >> `b' = 0` by simp[] >> fs[]) 2121 >- (rpt strip_tac >> Cases_on `SUC a = b'` >> fs[] 2122 >> `a >= b'` by simp[] >> `N a <= N b'` by simp[] 2123 >> `N (SUC a) <= N a` suffices_by simp[] 2124 >> `a >= i` by simp[] 2125 >> metis_tac[DECIDE ``SUC a = a + 1``] 2126 ) 2127 ) 2128 >> `N h <= N j` by fs[] 2129 >> `N j <= N h` by ( 2130 fs[minimal_elements_def,rrestrict_def, rel_to_reln_def] 2131 >> fs[] 2132 >> `(���l. (N h = N l) ��� i ��� l) ��� N h ��� N j ��� 2133 (���l. (N h = N l) ��� i ��� l) ��� (���l. (N j = N l) ��� i ��� l)` by ( 2134 rpt strip_tac >> fs[] 2135 >- (qexists_tac `h` >> fs[]) 2136 >- (qexists_tac `h` >> fs[]) 2137 >- (qexists_tac `j` >> fs[]) 2138 ) >> metis_tac[] 2139 ) 2140 >> fs[] 2141 ) 2142 >> `infBranchSuffOf (rs (N j)) (j - N j) (\_. x)` by ( 2143 fs[infBranchSuffOf_def] 2144 >> `!a. x ��� (rs (N j)).E (a + (j - N j),x)` suffices_by fs[] 2145 >> rpt strip_tac 2146 >> `x ��� always_run_V f1 f2 rs j` by fs[] 2147 >> `x ��� always_run_V f1 f2 rs (a + j)` by fs[] 2148 >> `N j < j` by metis_tac[ALWAYS_RUN_LEMM1] 2149 >> fs[infBranchOf_def] 2150 >> `b (a + j + 1) = x` by simp[] 2151 >> `b (a + j) = x` by simp[] 2152 >> `x ��� always_run_E f1 f2 rs (a + j, x)` by metis_tac[] 2153 >> fs[always_run_E_def, always_run_cond_def] 2154 >> `x ��� 2155 (rs (LEAST j'. x ��� (rs j').V (a + j ��� j'))).E 2156 (a + j ��� (LEAST j'. x ��� (rs j').V (a + j ��� j')),x)` by metis_tac[] 2157 >> `x ��� (rs (N (a + j))).E (a + j - N (a + j),x)` by metis_tac[] 2158 >> metis_tac[DECIDE ``a + j >= j``] 2159 ) 2160 >> qabbrev_tac `b1 = (��_ : num. x : �� ltl_frml)` 2161 >> `infBranchSuffOf (rs (N j)) (j ��� (N j)) b1` by fs[] 2162 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f')) f2) (rs (N j)) (suff w (N j))` 2163 by metis_tac[runForAA_def] 2164 >> imp_res_tac BRANCH_SUFF_LEMM 2165 >> qexists_tac `b''` >> qexists_tac `N j` 2166 >> fs[] >> qexists_tac `j - N j` >> fs[] 2167 >> strip_tac 2168 >- metis_tac[DECIDE ``0 + (j - N j) = j - N j``] 2169 >- (rpt strip_tac 2170 >> `?q. q + (j - N j) = m` by fs[LESS_EQ_ADD_EXISTS] 2171 >> `b'' m = b1 q` by metis_tac[] 2172 >> metis_tac[] 2173 ) 2174 ); 2175 2176val ALWAYS_RUN = store_thm 2177 ("ALWAYS_RUN", 2178``!f' f1 f2 w. (word_range w ��� POW (props f')) ��� 2179 (!n. ?r. runForAA (ltl2vwaa_free_alph (POW (props f')) f2) r (suff w n)) 2180 ==> (?r. runForAA (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) r w)``, 2181 rpt strip_tac 2182 >> `?rs. !n. runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n)` 2183 by metis_tac[SKOLEM_THM] 2184 >> qexists_tac `always_run f1 f2 rs` 2185 >> `!n. ((rs n).V 0) ��� tempDNF f2 2186 ==> ���a. (a,(rs n).V 1) ��� trans (POW (props f')) f2 ��� at (suff w n) 0 ��� a` 2187 by metis_tac[TRANS_LEMM1] 2188 >> simp[runForAA_def] 2189 >> `(validAARunFor (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) 2190 (always_run f1 f2 rs) w) 2191 ��� ((validAARunFor (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) 2192 (always_run f1 f2 rs) w) 2193 ==> acceptingAARun (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) 2194 (always_run f1 f2 rs))` suffices_by metis_tac[] 2195 >> strip_tac 2196 >- (imp_res_tac ALWAYS_RUN_LEMM2 2197 >> imp_res_tac ALWAYS_RUN_LEMM1 2198 >> fs[validAARunFor_def, ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 2199 >> rpt strip_tac 2200 >- fs[always_run_def, always_run_V_def] 2201 >- (fs[always_run_def, always_run_V_def] 2202 >> Induct_on `i` >> fs[always_run_V_def, tempSubForms_def] 2203 >> fs[SUBSET_DEF] >> rpt strip_tac 2204 >> `((q' = R f1 f2) ��� q' ��� tempSubForms f1) ��� q' ��� tempSubForms f2` 2205 by metis_tac[] 2206 >- (fs[always_run_cond_def] 2207 >> `x ��� {R f1 f2} ��� (rs i).V 1` by metis_tac[] 2208 >> `x ��� {R f1 f2} \/ x ��� (rs i).V 1` 2209 by metis_tac[IN_UNION] 2210 >- metis_tac[IN_SING] 2211 >- (fs[runForAA_def, validAARunFor_def] 2212 >> `(rs i).V 0 ��� tempDNF f2` 2213 by metis_tac[] 2214 >> imp_res_tac TEMPDNF_TEMPSUBF 2215 >> disj2_tac 2216 >> metis_tac[SUBSET_DEF] 2217 ) 2218 ) 2219 >- (`~(q' = R f1 f2)` by ( 2220 CCONTR_TAC >> fs[] 2221 >> `R f1 f2 ��� subForms f1` by metis_tac[TSF_IMPL_SF] 2222 >> `f1 ��� subForms (R f1 f2)` 2223 by fs[subForms_def, SUBFORMS_REFL] 2224 >> `f1 = R f1 f2` by metis_tac[SF_ANTISYM_LEMM] 2225 >> `(!f g. ~(f = R f g))` by (Induct_on `f` >> fs[]) 2226 >> metis_tac[] 2227 ) 2228 >> `x ��� (rs (LEAST j. q' ��� (rs j).V (i ��� j))).E 2229 (i ��� (LEAST j. q' ��� (rs j).V (i ��� j)),q')` 2230 by metis_tac[always_run_cond_def] 2231 >> qabbrev_tac `N = (LEAST j. q' ��� (rs j).V (i ��� j))` 2232 >> fs[runForAA_def, validAARunFor_def] 2233 >> `q' ��� (rs N).V (i - N)` by ( 2234 qunabbrev_tac `N` >> numLib.LEAST_ELIM_TAC 2235 >> simp[] >> metis_tac[]) 2236 >> `?a. (a,(rs N).E (i-N,q')) ��� trans (POW (props f')) q'` 2237 by metis_tac[] 2238 >> `(x,q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 2239 >> disj1_tac >> disj2_tac 2240 >> metis_tac[TSF_def, IN_DEF, TSF_TRANS_LEMM, transitive_def] 2241 ) 2242 >- (`~(q' = R f1 f2)` by ( 2243 CCONTR_TAC >> fs[] 2244 >> `R f1 f2 ��� subForms f2` by metis_tac[TSF_IMPL_SF] 2245 >> `f2 ��� subForms (R f1 f2)` 2246 by fs[subForms_def, SUBFORMS_REFL] 2247 >> `f2 = R f1 f2` by metis_tac[SF_ANTISYM_LEMM] 2248 >> `(!f g. ~(g = R f g))` by (Induct_on `g` >> fs[]) 2249 >> metis_tac[] 2250 ) 2251 >> `x ��� (rs (LEAST j. q' ��� (rs j).V (i ��� j))).E 2252 (i ��� (LEAST j. q' ��� (rs j).V (i ��� j)),q')` 2253 by metis_tac[always_run_cond_def] 2254 >> qabbrev_tac `N = (LEAST j. q' ��� (rs j).V (i ��� j))` 2255 >> fs[runForAA_def, validAARunFor_def] 2256 >> `q' ��� (rs N).V (i - N)` by ( 2257 qunabbrev_tac `N` >> numLib.LEAST_ELIM_TAC 2258 >> simp[] >> metis_tac[]) 2259 >> `?a. (a,(rs N).E (i-N,q')) ��� trans (POW (props f')) q'` 2260 by metis_tac[] 2261 >> `(x,q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 2262 >> disj2_tac 2263 >> metis_tac[TSF_def, IN_DEF, TSF_TRANS_LEMM, transitive_def] 2264 ) 2265 ) 2266 >- (Cases_on `q = R f1 f2` 2267 >- (fs[always_run_def, always_run_V_def, always_run_E_def] 2268 >> fs[always_run_V_def, always_run_cond_def] 2269 >> fs[runForAA_def, validAARunFor_def] 2270 >> fs[trans_def, d_conj_def] 2271 >> `���a. 2272 (a,(rs i).V 1) ��� trans (POW (props f')) f2 ��� 2273 at (suff w i) 0 ��� a` by metis_tac[] 2274 >> qexists_tac `a` >> dsimp[] >> disj2_tac 2275 >> qexists_tac `a` >> qexists_tac `(rs i).V 1` 2276 >> fs[AT_SUFF_LEMM] 2277 >> strip_tac 2278 >- metis_tac[TRANS_ALPH_LEMM,INTER_SUBSET_EQN] 2279 >- metis_tac[UNION_COMM] 2280 ) 2281 >- (fs[always_run_def, always_run_V_def, always_run_E_def] 2282 >> fs[always_run_V_def, always_run_cond_def] 2283 >> fs[runForAA_def, validAARunFor_def] 2284 >> fs[trans_def, d_conj_def] 2285 >> qabbrev_tac `N = LEAST j. q ��� (rs j).V (i ��� j)` 2286 >> `q ��� (rs N).V (i ��� N)` by metis_tac[] 2287 >> `���a. 2288 (a,(rs N).E (i - N,q)) ��� trans (POW (props f')) q ��� 2289 at (suff w N) (i - N) ��� a` by fs[] 2290 >> qexists_tac `a` >> fs[AT_SUFF_LEMM] 2291 >> `N < i` by metis_tac[] 2292 >> `i - N + N = i` by simp[] 2293 >> metis_tac[] 2294 ) 2295 ) 2296 >- (fs[SUBSET_DEF, always_run_def, always_run_V_def] >> rpt strip_tac 2297 >> `x ��� always_run_V f1 f2 rs (SUC i)` 2298 suffices_by metis_tac[SUC_ONE_ADD, ADD_COMM] 2299 >> fs[always_run_V_def, always_run_E_def] 2300 >> Cases_on `x = R f1 f2` >> fs[] 2301 >> Cases_on `q = R f1 f2` 2302 >- (qexists_tac `q` >> fs[] 2303 >> Cases_on `i` >> fs[always_run_V_def]) 2304 >- (qexists_tac `q` >> fs[] 2305 >> fs[always_run_cond_def] 2306 >> metis_tac[NOT_IN_EMPTY] 2307 ) 2308 ) 2309 >- (Cases_on `i = 0` >> fs[] 2310 >> `?j. i = SUC j` by (Cases_on `i` >> fs[]) 2311 >> rw[] 2312 >> fs[always_run_def, always_run_V_def] 2313 >> `!i. R f1 f2 ��� (always_run f1 f2 rs).V i` by ( 2314 strip_tac >> fs[always_run_def,always_run_V_def] 2315 >> Cases_on `i` >> fs[always_run_V_def] 2316 ) 2317 >- (qexists_tac `R f1 f2` 2318 >> strip_tac >> fs[always_run_def, always_run_V_def, always_run_E_def] 2319 >> fs[always_run_cond_def] 2320 ) 2321 >- (qexists_tac `q'` >> fs[] >> simp[always_run_E_def]) 2322 ) 2323 ) 2324 >- (rpt strip_tac 2325 >> `���b x. infBranchOf (always_run f1 f2 rs) b ��� branchFixP b x 2326 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)).final` 2327 suffices_by metis_tac[BRANCH_ACC_LEMM, LTL2WAA_ISFINITE, LTL2WAA_ISWEAK_LEMM] 2328 >> rpt strip_tac 2329 >> Cases_on `x = R f1 f2` 2330 >> imp_res_tac ALWAYS_RUN_LEMM2 2331 >- fs[ltl2vwaa_free_alph_def, finalForms_def] 2332 >- (`���b' i. infBranchOf (rs i) b' ��� branchFixP b' x` 2333 by metis_tac[ALWAYS_RUN_ACC_LEMM] 2334 >> `x ��� (ltl2vwaa_free_alph (POW (props f')) f2).final` 2335 by metis_tac[BRANCH_ACC_LEMM,LTL2WAA_ISFINITE,LTL2WAA_ISWEAK_LEMM,runForAA_def] 2336 >> fs[ltl2vwaa_free_alph_def, finalForms_def] 2337 >> `U f1' f2' ��� tempSubForms f2` suffices_by metis_tac[] 2338 >> `?i. U f1' f2' ��� (always_run f1 f2 rs).V i` 2339 by metis_tac[branchFixP_def, BRANCH_V_LEMM] 2340 >> `~(U f1' f2' = R f1 f2)` by simp[] 2341 >> fs[always_run_def] 2342 >> `(U f1' f2') ��� 2343 (rs (LEAST j. (U f1' f2') ��� (rs j).V (i' ��� j))).V 2344 (i' ��� LEAST j. (U f1' f2') ��� (rs j).V (i' ��� j))` 2345 by metis_tac[] 2346 >> qabbrev_tac `N = LEAST j. U f1' f2' ��� (rs j).V (i' ��� j)` 2347 >> `(rs N).V (i' - N ) ��� tempSubForms f2` 2348 by fs[runForAA_def, validAARunFor_def] 2349 >> metis_tac[SUBSET_DEF] 2350 ) 2351 ) 2352 ); 2353 2354val ALWAYS_F2_OR_EVTL_F1_R = store_thm 2355 ("ALWAYS_F2_OR_EVTL_F1_R", 2356 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) r w 2357 ==> ((!n. ?a. (a, r.E (n, R f1 f2)) ��� 2358 d_conj (trans (POW (props f)) f2) {(POW (props f), {R f1 f2})} 2359 ��� at w n ��� a) \/ 2360 (?n a. (a, r.E (n, R f1 f2)) ��� trans (POW (props f)) (CONJ f1 f2) 2361 ��� at w n ��� a))``, 2362 rpt strip_tac >> Cases_on `!i. R f1 f2 ��� r.V i` 2363 >- (disj1_tac >> rpt strip_tac 2364 >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 2365 >> `R f1 f2 ��� r.V n` by metis_tac[] 2366 >> `���a. (a,r.E (n,R f1 f2)) ��� trans (POW (props f)) (R f1 f2) ��� at w n ��� a` 2367 by metis_tac[] 2368 >> qexists_tac `a` >> fs[] 2369 >> fs[trans_def] 2370 >> `R f1 f2 ��� r.V (n+1)` by metis_tac[] 2371 >> `((n + 1) = 0) ��� ���q'. (R f1 f2) ��� r.E ((n + 1) ��� 1,q') ��� q' ��� r.V ((n + 1) ��� 1)` 2372 by metis_tac[] >> fs[] 2373 >> `q' = R f1 f2` by ( 2374 `q' ��� tempSubForms (R f1 f2)` by metis_tac[SUBSET_DEF] 2375 >> `���a. (a,r.E (n,q')) ��� trans (POW (props f)) q' ��� at w n ��� a` 2376 by metis_tac[] 2377 >> `(R f1 f2,q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 2378 >> metis_tac[TSF_def,IN_DEF,TSF_ANTISYM_LEMM] 2379 ) 2380 >> `(a,r.E (n,R f1 f2)) ��� 2381 d_conj (trans (POW (props f)) f2) (trans (POW (props f)) f1) 2382 ��� d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})}` 2383 by metis_tac[D_CONJ_UNION_DISTR] 2384 >> fs[IN_UNION] >> POP_ASSUM mp_tac >> simp[d_conj_def] 2385 >> rpt strip_tac 2386 >> (`!q. (q ��� e1) ==> (q,f2) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 2387 >> `!q. (q ��� e2) ==> (q,f1) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS] 2388 >> `R f1 f2 ��� e1 \/ R f1 f2 ��� e2` by metis_tac[IN_UNION] 2389 >- (`R f1 f2 ��� tempSubForms f2` by metis_tac[TSF_def, IN_DEF] 2390 >> `R f1 f2 ��� subForms f2` by metis_tac[TSF_IMPL_SF] 2391 >> `f2 ��� subForms (R f1 f2)` by fs[subForms_def, SUBFORMS_REFL] 2392 >> `R f1 f2 = f2` by metis_tac[SF_ANTISYM_LEMM] 2393 >> `(!f g. ~(g = R f g))` by (Induct_on `g` >> fs[]) 2394 >> metis_tac[] 2395 ) 2396 >- (`R f1 f2 ��� tempSubForms f1` by metis_tac[TSF_def, IN_DEF] 2397 >> `R f1 f2 ��� subForms f1` by metis_tac[TSF_IMPL_SF] 2398 >> `f1 ��� subForms (R f1 f2)` by fs[subForms_def, SUBFORMS_REFL] 2399 >> `R f1 f2 = f1` by metis_tac[SF_ANTISYM_LEMM] 2400 >> `(!f g. ~(g = R g f))` by (Induct_on `g` >> fs[]) 2401 >> metis_tac[] 2402 ) 2403 ) 2404 ) 2405 >- (disj2_tac 2406 >> fs[runForAA_def, validAARunFor_def] 2407 >> qabbrev_tac `N = LEAST j. ~(R f1 f2 ��� r.V j)` 2408 >> qexists_tac `N - 1` 2409 >> `R f1 f2 ��� r.V 0` 2410 by (fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] >> metis_tac[IN_SING]) 2411 >> `R f1 f2 ��� r.V (N - 1)` by ( 2412 qunabbrev_tac `N` >> numLib.LEAST_ELIM_TAC 2413 >> rpt strip_tac 2414 >- metis_tac[] 2415 >- (`~(n = 0)` by metis_tac[] 2416 >> `n - 1 < n` by simp[] 2417 >> metis_tac[]) 2418 ) 2419 >> fs[ltl2vwaa_free_alph_def] 2420 >> `���a. (a,r.E (N-1,(R f1 f2))) ��� trans (POW (props f)) (R f1 f2) ��� at w (N-1) ��� a` 2421 by fs[] 2422 >> qexists_tac `a` >> fs[] 2423 >> fs[trans_def] 2424 >> `(a,r.E (N -1,R f1 f2)) ��� 2425 d_conj (trans (POW (props f)) f2) (trans (POW (props f)) f1) 2426 ��� d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})}` 2427 by metis_tac[D_CONJ_UNION_DISTR] 2428 >> fs[IN_UNION] 2429 >- (fs[d_conj_def]>> metis_tac[UNION_COMM, INTER_COMM]) 2430 >- (fs[d_conj_def] 2431 >> `r.E (N - 1, R f1 f2) ��� r.V (N - 1 + 1)` by metis_tac[] 2432 >> fs[] 2433 >> `~(R f1 f2 ��� r.V N)` by ( 2434 qunabbrev_tac `N` 2435 >> numLib.LEAST_ELIM_TAC 2436 >> rpt strip_tac >> fs[] 2437 >> metis_tac[]) 2438 >> `~(N = 0)` by metis_tac[] 2439 >> `N - 1 + 1 = N` by simp[] 2440 >> `R f1 f2 ��� r.V N` by metis_tac[IN_UNION,SUBSET_DEF,IN_SING] 2441 ) 2442 ) 2443 ); 2444 2445val SUBFORM_LEMMA = store_thm 2446 ("SUBFORM_LEMMA", 2447 ``!f. (!g. g ��� subForms f ==> 2448 ({w | MODELS w g /\ (word_range w ��� POW (props f))} = 2449 alterA_lang (ltl2vwaa_free_alph (POW (props f)) g))) ==> 2450 (ltl_lang f = alterA_lang (ltl2vwaa f))``, 2451 rpt strip_tac >> `f ��� (subForms f)` by metis_tac[SUBFORMS_REFL] 2452 >> `({w | MODELS w f /\ (word_range w ��� POW (props f)) } 2453 = alterA_lang (ltl2vwaa_free_alph (POW (props f)) f))` 2454 by metis_tac[] 2455 >> metis_tac[ltl_lang_def, ltl2vwaa_def] 2456 ); 2457 2458val LTL2WAA_ISCORRECT = store_thm 2459 ("LTL2WAA_ISCORRECT", 2460 ``!f. (ltl_lang f = alterA_lang (ltl2vwaa f))``, 2461 strip_tac >> 2462 `(!g. (g ��� subForms f) ==> 2463 ({w | MODELS w g /\ (word_range w ��� POW (props f))} = 2464 alterA_lang (ltl2vwaa_free_alph (POW (props f)) g)))` 2465 suffices_by metis_tac[SUBFORM_LEMMA] 2466 >> `!g. (g ��� subForms f) ==> 2467 (({w | MODELS w g ��� word_range w ��� POW (props f)} 2468 ��� alterA_lang (ltl2vwaa_free_alph (POW (props f)) g)) 2469 /\ (alterA_lang (ltl2vwaa_free_alph (POW (props f)) g) 2470 ��� {w | MODELS w g ��� word_range w ��� POW (props f)}))` 2471 suffices_by rw[SET_EQ_SUBSET] 2472 >> Induct_on `g` >> rpt strip_tac >> simp[MODELS_def] 2473 >- (fs[alterA_lang_def, ltl2vwaa_free_alph_def, SUBSET_DEF] 2474 >> rpt strip_tac 2475 >> qexists_tac `ALTERA_RUN (\i. if i=0 then {VAR a} else {}) (\_. {})` 2476 >> simp[runForAA_def, validAARunFor_def, acceptingAARun_def] 2477 >> rpt strip_tac 2478 >> simp[initForms_def, tempDNF_def, trans_def] 2479 >> Cases_on `i=0` 2480 >> fs[SUBSET_DEF, tempSubForms_def, infBranchOf_def] 2481 >> qexists_tac `char (POW (props f)) a` >> rpt strip_tac 2482 >> fs[char_def, trans_def,POW_DEF, SUBSET_DEF] >> rpt strip_tac 2483 >> fs[word_range_def] 2484 >> `���y. (y ��� at x 0) ��� (y ��� props f)` by metis_tac[] 2485 >> metis_tac[] 2486 ) 2487 >- (fs[alterA_lang_def, ltl2vwaa_free_alph_def, SUBSET_DEF] 2488 >> rpt strip_tac 2489 >> fs[runForAA_def, validAARunFor_def, acceptingAARun_def, tempSubForms_def] 2490 >> fs[SUBSET_DEF,initForms_def] 2491 >> `VAR a ��� run.V 0` by fs[tempDNF_def] 2492 >> `���a'. ((a',run.E (0,VAR a)) ��� trans (POW (props f)) (VAR a)) 2493 ��� (at x 0 ��� a')` by metis_tac[] 2494 >> fs[trans_def, char_def] 2495 >> `(at x 0) ��� { a' | (a' ��� POW (props f)) ��� (a ��� a')}` by rw[] 2496 >> fs[] 2497 ) 2498 >- (fs[alterA_lang_def, ltl2vwaa_free_alph_def, SUBSET_DEF] 2499 >> rpt strip_tac 2500 >> qexists_tac `ALTERA_RUN (\i. if i=0 then {N_VAR a} else {}) (\_. {})` 2501 >> simp[runForAA_def, validAARunFor_def, acceptingAARun_def] 2502 >> rpt strip_tac 2503 >> simp[initForms_def, tempDNF_def, trans_def] 2504 >> Cases_on `i=0` 2505 >> fs[SUBSET_DEF, tempSubForms_def, infBranchOf_def] 2506 >> qexists_tac `(POW (props f)) DIFF (char (POW (props f)) a)` 2507 >> rpt strip_tac 2508 >> fs[char_def, trans_def,POW_DEF, SUBSET_DEF] >> rpt strip_tac 2509 >> fs[word_range_def] 2510 >> `���y. (y ��� at x 0) ��� (y ��� props f)` by metis_tac[] 2511 >> metis_tac[] 2512 ) 2513 >- (fs[alterA_lang_def, ltl2vwaa_free_alph_def, SUBSET_DEF] 2514 >> rpt strip_tac 2515 >> fs[runForAA_def, validAARunFor_def, acceptingAARun_def, tempSubForms_def] 2516 >> fs[SUBSET_DEF,initForms_def] 2517 >> `N_VAR a ��� run.V 0` by fs[tempDNF_def] 2518 >> `���a'. ((a',run.E (0,N_VAR a)) ��� trans (POW (props f)) (N_VAR a)) 2519 ��� (at x 0 ��� a')` by metis_tac[] 2520 >> fs[trans_def, char_def, DIFF_DEF] 2521 >> `(at x 0) ��� { x | (x ��� POW (props f)) 2522 ��� (~(x ��� POW (props f)) \/ ~(a ��� x))}` by rw[] 2523 >> fs[] >> fs[] 2524 ) 2525 >- (`subForms (DISJ g g') = {DISJ g g'} ��� (subForms g) ��� (subForms g')` 2526 by rw[subForms_def] 2527 >> fs[UNION_DEF] 2528 >> `g ��� subForms (DISJ g g')` by simp[SUBFORMS_REFL] 2529 >> `g' ��� subForms (DISJ g g')` by simp[SUBFORMS_REFL] 2530 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2531 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2532 >> dsimp[] 2533 >> `{w | MODELS w g ��� word_range w ��� POW (props f)} 2534 ��� alterA_lang (ltl2vwaa_free_alph (POW (props f)) g)` by metis_tac[] 2535 >> `{w | MODELS w g' ��� word_range w ��� POW (props f)} 2536 ��� alterA_lang (ltl2vwaa_free_alph (POW (props f)) g')` by metis_tac[] 2537 >> fs[alterA_lang_def, SUBSET_DEF] >> rpt strip_tac 2538 >- (`���run. 2539 runForAA (ltl2vwaa_free_alph (POW (props f)) g) run x ��� 2540 ���x'. x' ��� word_range x 2541 ==> x' ��� (ltl2vwaa_free_alph (POW (props f)) g).alphabet` 2542 by metis_tac[] 2543 >> qexists_tac `run` >> rpt strip_tac >> fs[] 2544 >- metis_tac[RUN_FOR_DISJ_LEMM] 2545 >- fs[ltl2vwaa_free_alph_def] 2546 ) 2547 >- (`���run. 2548 runForAA (ltl2vwaa_free_alph (POW (props f)) g') run x ��� 2549 ���x'. x' ��� word_range x 2550 ==> x' ��� (ltl2vwaa_free_alph (POW (props f)) g').alphabet` 2551 by metis_tac[] 2552 >> qexists_tac `run` >> rpt strip_tac >> fs[] 2553 >- metis_tac[RUN_FOR_DISJ_LEMM] 2554 >- fs[ltl2vwaa_free_alph_def] 2555 ) 2556 ) 2557 >- (`subForms (DISJ g g') = {DISJ g g'} ��� (subForms g) ��� (subForms g')` 2558 by rw[subForms_def] 2559 >> fs[UNION_DEF] 2560 >> `g ��� subForms (DISJ g g')` by simp[SUBFORMS_REFL] 2561 >> `g' ��� subForms (DISJ g g')` by simp[SUBFORMS_REFL] 2562 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2563 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2564 >> dsimp[] 2565 >> `{w | MODELS w g ��� word_range w ��� POW (props f)} 2566 ��� alterA_lang (ltl2vwaa_free_alph (POW (props f)) g)` by metis_tac[] 2567 >> `{w | MODELS w g' ��� word_range w ��� POW (props f)} 2568 ��� alterA_lang (ltl2vwaa_free_alph (POW (props f)) g')` by metis_tac[] 2569 >> fs[alterA_lang_def, SUBSET_DEF] >> rpt strip_tac 2570 >> `runForAA (ltl2vwaa_free_alph (POW (props f)) g) run x ��� 2571 runForAA (ltl2vwaa_free_alph (POW (props f)) g') run x` 2572 by metis_tac[RUN_FOR_DISJ_LEMM2] 2573 >- (`(���run. runForAA (ltl2vwaa_free_alph (POW (props f)) g) run x 2574 ��� ���x'. 2575 ((x' ��� word_range x) ��� 2576 (x' ��� (ltl2vwaa_free_alph (POW (props f)) g).alphabet))) ��� 2577 MODELS x g ��� ���x'. (x' ��� word_range x) ��� (x' ��� POW (props f))` 2578 by metis_tac[] 2579 >> `(���run. 2580 runForAA (ltl2vwaa_free_alph (POW (props f)) g) run x ��� 2581 ���x'. 2582 x' ��� word_range x ��� 2583 x' ��� (ltl2vwaa_free_alph (POW (props f)) g).alphabet)` 2584 suffices_by metis_tac[] 2585 >> qexists_tac `run` >> fs[ltl2vwaa_free_alph_def]) 2586 >- (`(���run. runForAA (ltl2vwaa_free_alph (POW (props f)) g') run x 2587 ��� ���x'. 2588 ((x' ��� word_range x) ��� 2589 (x' ��� (ltl2vwaa_free_alph (POW (props f)) g').alphabet))) ��� 2590 MODELS x g' ��� ���x'. (x' ��� word_range x) ��� (x' ��� POW (props f))` 2591 by metis_tac[] 2592 >> `(���run. 2593 runForAA (ltl2vwaa_free_alph (POW (props f)) g') run x ��� 2594 ���x'. 2595 x' ��� word_range x ��� 2596 x' ��� (ltl2vwaa_free_alph (POW (props f)) g').alphabet)` 2597 suffices_by metis_tac[] 2598 >> qexists_tac `run` >> fs[ltl2vwaa_free_alph_def]) 2599 ) 2600 >- (`subForms (CONJ g g') = {CONJ g g'} ��� (subForms g) ��� (subForms g')` 2601 by rw[subForms_def] 2602 >> fs[UNION_DEF] 2603 >> `g ��� subForms (CONJ g g')` by simp[SUBFORMS_REFL] 2604 >> `g' ��� subForms (CONJ g g')` by simp[SUBFORMS_REFL] 2605 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2606 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2607 >> fs[SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 2608 >> `���run. 2609 runForAA (ltl2vwaa_free_alph (POW (props f)) g) run x 2610 ��� word_range x ��� (ltl2vwaa_free_alph (POW (props f)) g).alphabet` 2611 by metis_tac[] 2612 >> `���run. 2613 runForAA (ltl2vwaa_free_alph (POW (props f)) g') run x 2614 ��� word_range x ��� (ltl2vwaa_free_alph (POW (props f)) g').alphabet` 2615 by metis_tac[] 2616 >> `���r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ g g')) r x` 2617 by metis_tac[RUN_FOR_CONJ_LEMM] 2618 >> qexists_tac `r` >> rpt strip_tac >> fs[] 2619 >> fs[ltl2vwaa_free_alph_def] 2620 ) 2621 >- (`subForms (CONJ g g') = {CONJ g g'} ��� (subForms g) ��� (subForms g')` 2622 by rw[subForms_def] 2623 >> fs[UNION_DEF] 2624 >> `g ��� subForms (CONJ g g')` by simp[SUBFORMS_REFL] 2625 >> `g' ��� subForms (CONJ g g')` by simp[SUBFORMS_REFL] 2626 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2627 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2628 >> fs[SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 2629 >- (`���r1. runForAA (ltl2vwaa_free_alph (POW (props f)) g) r1 x` 2630 by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 2631 >> `word_range x ��� 2632 (ltl2vwaa_free_alph (POW (props f)) g).alphabet` 2633 suffices_by metis_tac[] 2634 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def]) 2635 >- (`���r1. runForAA (ltl2vwaa_free_alph (POW (props f)) g') r1 x` 2636 by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 2637 >> `word_range x ��� 2638 (ltl2vwaa_free_alph (POW (props f)) g').alphabet` 2639 suffices_by metis_tac[] 2640 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def]) 2641 >- (fs[ltl2vwaa_free_alph_def, word_range_def, SUBSET_DEF] 2642 >> metis_tac[] 2643 ) 2644 ) 2645 >- (`subForms (X g) = {X g} ��� (subForms g)` 2646 by rw[subForms_def] 2647 >> fs[UNION_DEF] 2648 >> `g ��� subForms (X g)` by simp[SUBFORMS_REFL] 2649 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2650 >> fs[SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 2651 >> `word_range (suff x 1) ��� word_range x` by metis_tac[WORD_RANGE_SUFF_LEMM] 2652 >> `word_range (suff x 1) ��� POW (props f)` by metis_tac[SUBSET_TRANS, SUBSET_DEF] 2653 >> `?run. runForAA (ltl2vwaa_free_alph (POW (props f)) g) run (suff x 1)` 2654 by metis_tac[WORD_RANGE_SUFF_LEMM, SUBSET_DEF] 2655 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) (X g)) r' x` 2656 by metis_tac[RUN_FOR_X_LEMM, SUBSET_DEF] 2657 >> qexists_tac `r'` >> fs[ltl2vwaa_free_alph_def] >> metis_tac[SUBSET_DEF] 2658 ) 2659 >- (`subForms (X g) = {X g} ��� (subForms g)` 2660 by rw[subForms_def] 2661 >> fs[UNION_DEF] 2662 >> `g ��� subForms (X g)` by simp[SUBFORMS_REFL] 2663 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2664 >> fs[SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 2665 >- (`���run. runForAA (ltl2vwaa_free_alph (POW (props f)) g) run (suff x 1)` 2666 by metis_tac[RUN_FOR_X_LEMM2] 2667 >> `word_range (suff x 1) ��� word_range x` by metis_tac[WORD_RANGE_SUFF_LEMM] 2668 >> `?run. runForAA (ltl2vwaa_free_alph (POW (props f)) g) run (suff x 1) ��� 2669 word_range (suff x 1) ��� (ltl2vwaa_free_alph (POW (props f)) g).alphabet` 2670 suffices_by metis_tac[] 2671 >> qexists_tac `run'` >> fs[ltl2vwaa_free_alph_def] 2672 >> metis_tac[SUBSET_TRANS]) 2673 >- (fs[ltl2vwaa_free_alph_def, SUBSET_DEF]) 2674 ) 2675 >- (`{w | 2676 (���n. MODELS (suff w n) g' ��� ���i. i < n ��� MODELS (suff w i) g) 2677 ��� word_range w ��� POW (props f) } 2678 ��� alterA_lang 2679 (ltl2vwaa_free_alph (POW (props f)) 2680 (DISJ g' (CONJ g (X (U g g')))))` 2681 suffices_by metis_tac[U_AUTO_CHARACTERISATION] 2682 >> simp[SUBSET_DEF] >> rpt strip_tac 2683 >> `subForms (U g g') = {U g g'} ��� (subForms g) ��� (subForms g')` 2684 by rw[subForms_def] 2685 >> fs[UNION_DEF] 2686 >> `g ��� subForms (U g g')` by simp[SUBFORMS_REFL] 2687 >> `g' ��� subForms (U g g')` by simp[SUBFORMS_REFL] 2688 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2689 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2690 >> `suff x 0 = x` by 2691 (Cases_on `x` >> fs[suff_def] >> metis_tac[]) 2692 >> Cases_on `n = 0` 2693 >- (`MODELS x g'` by metis_tac[] 2694 >> fs[SUBSET_DEF, alterA_lang_def] 2695 >> `?run. 2696 runForAA (ltl2vwaa_free_alph (POW (props f)) g') 2697 run x` 2698 by metis_tac[word_range_def] 2699 >> qexists_tac `run` 2700 >> strip_tac 2701 >- metis_tac[RUN_FOR_DISJ_LEMM] 2702 >- fs[ltl2vwaa_free_alph_def] 2703 ) 2704 >- (`!j. suff x (n - j) ��� 2705 alterA_lang (ltl2vwaa_free_alph (POW (props f)) 2706 (DISJ g' (CONJ g (X (U g g')))))` 2707 suffices_by (`n - n = 0` by simp[] 2708 >> metis_tac[]) 2709 >> Induct_on `j` 2710 >- (fs[alterA_lang_def] 2711 >> `word_range (suff x n) ��� word_range x` 2712 by metis_tac[WORD_RANGE_SUFF_LEMM] 2713 >> fs[SUBSET_DEF] 2714 >> `���run. 2715 runForAA (ltl2vwaa_free_alph (POW (props f)) g') 2716 run 2717 (suff x n) 2718 ��� word_range (suff x n) 2719 ��� (ltl2vwaa_free_alph (POW (props f)) g').alphabet` 2720 by metis_tac[SUBSET_DEF] 2721 >> qexists_tac `run` >> rpt strip_tac 2722 >- metis_tac[RUN_FOR_DISJ_LEMM] 2723 >- fs[ltl2vwaa_free_alph_def] 2724 ) 2725 >- (Cases_on `n <= j` 2726 >- (`n - j = 0` by simp[] 2727 >> `n - SUC j = 0` by simp[] 2728 >> rw[] >> metis_tac[] 2729 ) 2730 >- (`suff x (n ��� j) ��� 2731 alterA_lang 2732 (ltl2vwaa_free_alph (POW (props f)) (U g g'))` 2733 by metis_tac[U_AUTO_CHARACTERISATION] 2734 >> POP_ASSUM mp_tac >> simp[alterA_lang_def] 2735 >> rpt strip_tac 2736 >> `suff (suff x (n - SUC j)) 1 = suff x (n - j)` 2737 by (Cases_on `x` >> fs[suff_def] 2738 >> simp[] >> rw[SUC_ONE_ADD]) 2739 >> `word_range (suff x (n ��� SUC j)) 2740 ��� word_range x` 2741 by metis_tac[WORD_RANGE_SUFF_LEMM] 2742 >> `���r'. 2743 runForAA 2744 (ltl2vwaa_free_alph (POW (props f)) (X (U g g'))) 2745 r' (suff x (n - SUC j))` 2746 by metis_tac[RUN_FOR_X_LEMM, SUBSET_DEF] 2747 >> `n - SUC j < n` by simp[] 2748 >> `MODELS (suff x (n - SUC j)) g` by fs[] 2749 >> `���r'. 2750 runForAA 2751 (ltl2vwaa_free_alph (POW (props f)) g) 2752 r' (suff x (n - SUC j))` by 2753 (fs[alterA_lang_def, SUBSET_DEF] 2754 >> metis_tac[]) 2755 >> `���r. 2756 runForAA 2757 (ltl2vwaa_free_alph (POW (props f)) 2758 (CONJ g (X (U g g')))) 2759 r (suff x (n - SUC j))` by metis_tac[RUN_FOR_CONJ_LEMM] 2760 >> qexists_tac `r` 2761 >> rpt strip_tac 2762 >- metis_tac[RUN_FOR_DISJ_LEMM] 2763 >- (fs[ltl2vwaa_free_alph_def] >> metis_tac[SUBSET_DEF]) 2764 ) 2765 ) 2766 ) 2767 ) 2768 >- (`subForms (U g g') = {U g g'} ��� (subForms g) ��� (subForms g')` 2769 by rw[subForms_def] 2770 >> fs[UNION_DEF] 2771 >> `g ��� subForms (U g g')` by simp[SUBFORMS_REFL] 2772 >> `g' ��� subForms (U g g')` by simp[SUBFORMS_REFL] 2773 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2774 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2775 >> simp[SUBSET_DEF, alterA_lang_def] >> rpt strip_tac 2776 >- (imp_res_tac EVTL_F2_RUN_LEMM 2777 >> qexists_tac `n` >> strip_tac 2778 >- (`word_range (suff x n) ��� POW (props f)` by ( 2779 fs[ltl2vwaa_free_alph_def] 2780 >> `word_range x ��� POW (props f)` 2781 suffices_by metis_tac[WORD_RANGE_SUFF_LEMM,SUBSET_TRANS] 2782 >> metis_tac[SUBSET_DEF] 2783 ) 2784 >> fs[SUBSET_DEF, alterA_lang_def, ltl2vwaa_free_alph_def] >> metis_tac[] 2785 ) 2786 >- (rpt strip_tac 2787 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) g) r' (suff x i)` 2788 by fs[] 2789 >> `word_range (suff x i) ��� POW (props f)` by ( 2790 fs[ltl2vwaa_free_alph_def] 2791 >> `word_range x ��� POW (props f)` 2792 suffices_by metis_tac[WORD_RANGE_SUFF_LEMM,SUBSET_TRANS] 2793 >> metis_tac[SUBSET_DEF] 2794 ) 2795 >> fs[SUBSET_DEF, alterA_lang_def, ltl2vwaa_free_alph_def] >> metis_tac[] 2796 ) 2797 ) 2798 >- fs[ltl2vwaa_free_alph_def] 2799 ) 2800 >- (`subForms (R g g') = {R g g'} ��� (subForms g) ��� (subForms g')` 2801 by rw[subForms_def] 2802 >> fs[UNION_DEF] 2803 >> `g ��� subForms (R g g')` by simp[SUBFORMS_REFL] 2804 >> `g' ��� subForms (R g g')` by simp[SUBFORMS_REFL] 2805 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2806 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2807 >> simp[SUBSET_DEF] >> rpt strip_tac 2808 >> `(���n. MODELS (suff x n) g') ��� 2809 ���n. MODELS (suff x n) g ��� ���i. i <= n ��� MODELS (suff x i) g'` 2810 by metis_tac[R_COND_LEMM] 2811 >- (fs[alterA_lang_def] 2812 >> `!n. ?r. runForAA (ltl2vwaa_free_alph (POW (props f)) g') r (suff x n)` 2813 by (rpt strip_tac >> `MODELS (suff x n) g'` by metis_tac[] 2814 >> fs[alterA_lang_def, SUBSET_DEF] 2815 >> metis_tac[WORD_RANGE_SUFF_LEMM, SUBSET_DEF] 2816 ) 2817 >> imp_res_tac ALWAYS_RUN 2818 >> `word_range x ��� POW (props f)` by metis_tac[SUBSET_DEF] 2819 >> fs[] 2820 >> `���r. runForAA (ltl2vwaa_free_alph (POW (props f)) (R g g')) r x` 2821 by fs[] 2822 >> qexists_tac `r` 2823 >> strip_tac >> fs[] 2824 >> fs[ltl2vwaa_free_alph_def] 2825 ) 2826 >- (`x ��� alterA_lang (ltl2vwaa_free_alph (POW (props f)) 2827 (CONJ g' (DISJ g (X (R g g')))))` 2828 suffices_by metis_tac[R_AUTO_CHARACTERISATION] 2829 >> fs[alterA_lang_def] 2830 >> rw[LEFT_EXISTS_AND_THM] 2831 >- (`suff x 0 = x` by 2832 (Cases_on `x` >> fs[suff_def] >> metis_tac[]) 2833 >> `!j. 2834 ���run. runForAA 2835 (ltl2vwaa_free_alph (POW (props f)) (CONJ g' (DISJ g (X (R g g'))))) 2836 run (suff x (n - j))` 2837 suffices_by metis_tac[DECIDE ``n - n = 0``] 2838 >> Induct_on `j` 2839 >- (fs[SUBSET_DEF] 2840 >> `word_range (suff x n) ��� POW (props f)` 2841 by metis_tac[WORD_RANGE_SUFF_LEMM, SUBSET_DEF] 2842 >> `���run. 2843 runForAA (ltl2vwaa_free_alph (POW (props f)) g) run (suff x n)` 2844 by metis_tac[SUBSET_DEF] 2845 >> `���run. 2846 runForAA (ltl2vwaa_free_alph (POW (props f)) g') run (suff x n)` 2847 by metis_tac[SUBSET_DEF, DECIDE ``n <= n``] 2848 >> `���r. 2849 runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ g' g)) r 2850 (suff x n)` 2851 by metis_tac[RUN_FOR_CONJ_LEMM] 2852 >> metis_tac[CONJ_DISJ_DISTRIB] 2853 ) 2854 >- (`���run. 2855 runForAA 2856 (ltl2vwaa_free_alph (POW (props f)) 2857 (R g g')) run (suff x (n ��� j))` by ( 2858 `alterA_lang (ltl2vwaa_free_alph (POW (props f)) (R g g')) = 2859 alterA_lang 2860 (ltl2vwaa_free_alph (POW (props f)) 2861 (CONJ g' (DISJ g (X (R g g')))))` 2862 by metis_tac[R_AUTO_CHARACTERISATION] 2863 >> fs[alterA_lang_def, SUBSET_DEF, SET_EQ_SUBSET] 2864 >> first_x_assum (qspec_then `suff x (n - j)` mp_tac) 2865 >> first_x_assum (qspec_then `suff x (n - j)` mp_tac) 2866 >> `word_range (suff x (n - j)) ��� POW (props f)` 2867 by metis_tac[WORD_RANGE_SUFF_LEMM, SUBSET_DEF] 2868 >> rpt strip_tac 2869 >> fs[ltl2vwaa_free_alph_def] >> metis_tac[SUBSET_DEF] 2870 ) 2871 >> Cases_on `n <= j` 2872 >- (`n - j = 0` by simp[] 2873 >> `n - SUC j = 0` by simp[] 2874 >> rw[] >> metis_tac[] 2875 ) 2876 >- (`suff (suff x (n - SUC j)) 1 = suff x (n - j)` 2877 by (Cases_on `x` >> fs[suff_def] 2878 >> simp[] >> rw[SUC_ONE_ADD]) 2879 >> `word_range (suff x (n ��� SUC j)) 2880 ��� word_range x` 2881 by metis_tac[WORD_RANGE_SUFF_LEMM] 2882 >> `���r'. 2883 runForAA 2884 (ltl2vwaa_free_alph (POW (props f)) (X (R g g'))) 2885 r' (suff x (n - SUC j))` 2886 by metis_tac[RUN_FOR_X_LEMM, SUBSET_DEF] 2887 >> `n - SUC j < n` by simp[] 2888 >> `MODELS (suff x (n - SUC j)) g'` by fs[] 2889 >> `���r'. 2890 runForAA 2891 (ltl2vwaa_free_alph (POW (props f)) g') 2892 r' (suff x (n - SUC j))` by 2893 (fs[alterA_lang_def, SUBSET_DEF] 2894 >> metis_tac[]) 2895 >> `���r. 2896 runForAA 2897 (ltl2vwaa_free_alph (POW (props f)) 2898 (CONJ g' (X (R g g')))) 2899 r (suff x (n - SUC j))` by metis_tac[RUN_FOR_CONJ_LEMM] 2900 >> metis_tac[CONJ_DISJ_DISTRIB] 2901 ) 2902 ) 2903 ) 2904 >- (fs[word_range_def, SUBSET_DEF, ltl2vwaa_free_alph_def]) 2905 ) 2906 ) 2907 >- (`subForms (R g g') = {R g g'} ��� (subForms g) ��� (subForms g')` 2908 by rw[subForms_def] 2909 >> fs[UNION_DEF] 2910 >> `g ��� subForms (R g g')` by simp[SUBFORMS_REFL] 2911 >> `g' ��� subForms (R g g')` by simp[SUBFORMS_REFL] 2912 >> `g ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2913 >> `g' ��� subForms f` by metis_tac[SUBFORMS_TRANS, subForms_def] 2914 >> simp[SUBSET_DEF, alterA_lang_def] >> rpt gen_tac 2915 >> strip_tac >> strip_tac 2916 >- (`(���n. MODELS (suff x n) g') ��� 2917 ���n. MODELS (suff x n) g ��� ���i. i ��� n ��� MODELS (suff x i) g'` 2918 suffices_by metis_tac[R_COND_LEMM] 2919 >> imp_res_tac ALWAYS_F2_OR_EVTL_F1_R 2920 >- (disj1_tac >> strip_tac 2921 >> first_x_assum (qspec_then `n` mp_tac) 2922 >> strip_tac 2923 >> `���r'. 2924 runForAA 2925 (ltl2vwaa_free_alph (POW (props f)) (CONJ g' (X (R g g')))) r' 2926 (suff x n)` by metis_tac[R_REPL_F1_LEMM] 2927 >> `word_range (suff x n) ��� word_range x` 2928 by metis_tac[WORD_RANGE_SUFF_LEMM] 2929 >> `���r1. 2930 runForAA (ltl2vwaa_free_alph (POW (props f)) g') r1 (suff x n)` 2931 by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 2932 >> fs[alterA_lang_def, SUBSET_DEF] 2933 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def] 2934 >> metis_tac[] 2935 ) 2936 >- (disj2_tac 2937 >> qabbrev_tac 2938 `N = LEAST j. (?a. 2939 (a,run.E (j,R g g')) ��� trans (POW (props f)) (CONJ g g') 2940 ��� at x j ��� a)` 2941 >> `!i. i < N ==> (R g g' ��� run.V i)` by ( 2942 Induct_on `i` 2943 >- (strip_tac >> fs[runForAA_def,validAARunFor_def] 2944 >> fs[ltl2vwaa_free_alph_def, initForms_def, tempDNF_def] 2945 ) 2946 >- (strip_tac >> `R g g' ��� run.V i` by fs[] 2947 >> `~(?a.(a,run.E (i,R g g')) ��� trans (POW (props f)) (CONJ g g') 2948 ��� at x i ��� a)` by ( 2949 CCONTR_TAC >> fs[] >> `N <= i` suffices_by simp[] 2950 >> qunabbrev_tac `N` 2951 >> numLib.LEAST_ELIM_TAC >> rpt strip_tac 2952 >- metis_tac[] 2953 >- (CCONTR_TAC >> `i < n'` by simp[] 2954 >> metis_tac[]) 2955 ) 2956 >> fs[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 2957 >> `?a'. (a', run.E (i, R g g')) ��� trans (POW (props f)) (R g g') 2958 ��� at x i ��� a'` by metis_tac[] 2959 >> fs[trans_def] 2960 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2961 >> simp[D_CONJ_UNION_DISTR] >> rpt strip_tac 2962 >- (fs[d_conj_def] 2963 >> first_x_assum (qspec_then `a'` mp_tac) 2964 >> metis_tac[UNION_COMM, INTER_COMM] 2965 ) 2966 >- (fs[d_conj_def] 2967 >> `e1' ��� {R g g'} ��� run.V (i + 1)` by metis_tac[] 2968 >> `SUC i = i + 1` by simp[] 2969 >> metis_tac[IN_UNION,IN_SING,SUBSET_DEF] 2970 ) 2971 ) 2972 ) 2973 >> qexists_tac `N` 2974 >> rpt strip_tac 2975 >- (`?a.(a,run.E (N,R g g')) ��� trans (POW (props f)) (CONJ g g') 2976 ��� at x N ��� a` by ( 2977 qunabbrev_tac `N` >> numLib.LEAST_ELIM_TAC 2978 >> rpt strip_tac 2979 >- (metis_tac[]) 2980 >- metis_tac[] 2981 ) 2982 >> `���r'. 2983 runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ g g')) 2984 r' (suff x N)` by metis_tac[REPL_F2_LEMM,SUBSET_REFL] 2985 >> ` ���r1. 2986 runForAA (ltl2vwaa_free_alph (POW (props f)) g) r1 (suff x N)` 2987 by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 2988 >> `word_range (suff x N) ��� word_range x` 2989 by metis_tac[WORD_RANGE_SUFF_LEMM] 2990 >> fs[alterA_lang_def, SUBSET_DEF] 2991 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def] 2992 >> metis_tac[] 2993 ) 2994 >- (Cases_on `i = N` 2995 >- (`?a.(a,run.E (N,R g g')) ��� trans (POW (props f)) (CONJ g g') 2996 ��� at x N ��� a` by ( 2997 qunabbrev_tac `N` >> numLib.LEAST_ELIM_TAC 2998 >> rpt strip_tac >> metis_tac[] 2999 ) 3000 >> `���r'. 3001 runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ g g')) 3002 r' (suff x N)` by metis_tac[REPL_F2_LEMM,SUBSET_REFL] 3003 >> ` ���r1. 3004 runForAA (ltl2vwaa_free_alph (POW (props f)) g') 3005 r1 (suff x N)` 3006 by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 3007 >> `word_range (suff x N) ��� word_range x` 3008 by metis_tac[WORD_RANGE_SUFF_LEMM] 3009 >> fs[alterA_lang_def, SUBSET_DEF] 3010 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def] 3011 >> metis_tac[]) 3012 >- (`i < N` by simp[] 3013 >> `~(?a.(a,run.E (i,R g g')) ��� trans (POW (props f)) (CONJ g g') 3014 ��� at x i ��� a)` by ( 3015 CCONTR_TAC >> fs[] >> `N <= i` suffices_by simp[] 3016 >> qunabbrev_tac `N` 3017 >> numLib.LEAST_ELIM_TAC >> rpt strip_tac 3018 >- (metis_tac[]) 3019 >- (CCONTR_TAC >> `i < n'` by simp[] 3020 >> metis_tac[]) 3021 ) 3022 >> `R g g' ��� run.V i` by fs[] 3023 >> imp_res_tac R_REPL_F1_LEMM 3024 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 3025 >> RULE_ASSUM_TAC( 3026 SIMP_RULE 3027 (srw_ss())[runForAA_def, validAARunFor_def, ltl2vwaa_free_alph_def] 3028 ) 3029 >> rpt strip_tac 3030 >> `?a. (a,run.E (i,R g g')) ��� trans (POW (props f)) (R g g') 3031 ��� at x i ��� a` by metis_tac[] 3032 >> fs[trans_def] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 3033 >> simp[D_CONJ_UNION_DISTR] 3034 >> rpt strip_tac 3035 >- (fs[d_conj_def] 3036 >> first_x_assum (qspec_then `a'` mp_tac) 3037 >> metis_tac[UNION_COMM, INTER_COMM]) 3038 >- (`���r'. 3039 runForAA 3040 (ltl2vwaa_free_alph (POW (props f)) 3041 (CONJ g' (X (R g g')))) r' 3042 (suff x i)` by metis_tac[] 3043 >> `���r1. 3044 runForAA (ltl2vwaa_free_alph (POW (props f)) g') r1 3045 (suff x i)` by metis_tac[RUN_FOR_CONJ_LEMM2_UNION] 3046 >> `word_range (suff x i) ��� word_range x` 3047 by metis_tac[WORD_RANGE_SUFF_LEMM] 3048 >> fs[alterA_lang_def, SUBSET_DEF] 3049 >> fs[SUBSET_DEF, ltl2vwaa_free_alph_def] 3050 >> metis_tac[] 3051 ) 3052 ) 3053 ) 3054 ) 3055 ) 3056 >- fs[ltl2vwaa_free_alph_def] 3057 ) 3058 ); 3059 3060val _ = export_theory(); 3061