1open HolKernel Parse boolLib bossLib 2 3open listTheory 4open grammarTheory 5open lcsymtacs 6open pred_setTheory 7 8val rveq = rpt BasicProvers.VAR_EQ_TAC 9fun asm_match q = Q.MATCH_ASSUM_RENAME_TAC q 10 11val MAP_EQ_CONS = prove( 12 ``(MAP f l = h::t) ��� ���e es. l = e::es ��� f e = h ��� MAP f es = t``, 13 Cases_on `l` >> simp[]) 14 15fun Store_thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n] 16 17val _ = new_theory "NTproperties" 18 19fun dsimp thl = asm_simp_tac (srw_ss() ++ boolSimps.DNF_ss) thl 20fun asimp thl = asm_simp_tac (srw_ss() ++ ARITH_ss) thl 21fun qxchl [] ttac = ttac 22 | qxchl (q::qs) ttac = Q.X_CHOOSE_THEN q (qxchl qs ttac) 23 24val APPEND_EQ_SING' = CONV_RULE (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) 25 listTheory.APPEND_EQ_SING 26 27val RTC_R_I = relationTheory.RTC_RULES |> SPEC_ALL |> CONJUNCT2 |> GEN_ALL 28 29(* ---------------------------------------------------------------------- 30 A sentential form is nullable if it can derive the empty string. 31 32 This work draws on Aditi Barthwal's formalisation. Using parse trees 33 rather than derivations simplifies some of the resulting proofs. 34 ---------------------------------------------------------------------- *) 35 36val nullable_def = Define` 37 nullable G sf = derives G sf [] 38` 39val _ = overload_on ("nullableNT", ``��G n. nullable G [NT n]``) 40 41val derives_TOK = store_thm( 42 "derives_TOK", 43 ``���G p s t sf. 44 derives G (p ++ [TOK t] ++ s) sf ��� 45 ���ps ss. sf = ps ++ [TOK t] ++ ss ��� derives G p ps ��� derives G s ss``, 46 gen_tac >> 47 `���sf0 sf. derives G sf0 sf ��� 48 ���p s t. sf0 = p ++ [TOK t] ++ s ��� 49 ���ps ss. sf = ps ++ [TOK t] ++ ss ��� derives G p ps ��� 50 derives G s ss` suffices_by metis_tac[] >> 51 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT >> dsimp[] >> conj_tac 52 >- metis_tac [relationTheory.RTC_REFL] >> 53 map_every qx_gen_tac [`sf0`, `sf`, `p`, `s`, `t`] >> 54 simp[derive_def, Once listTheory.APPEND_EQ_APPEND_MID] >> 55 disch_then (CONJUNCTS_THEN2 (qxchl [`p0`, `N`, `r`, `s0`] mp_tac) 56 strip_assume_tac) >> 57 disch_then (CONJUNCTS_THEN2 (DISJ_CASES_THEN (qxchl [`l`] strip_assume_tac)) 58 strip_assume_tac) >> 59 rw[] >| [ 60 qpat_x_assum `x = y` mp_tac >> simp[Once listTheory.APPEND_EQ_APPEND_MID] >> 61 simp[APPEND_EQ_SING'] >> disch_then (qxchl [`l'`] strip_assume_tac) >> 62 rw[] >> first_x_assum (qspecl_then [`p`, `l' ++ r ++ s0`, `t`] mp_tac), 63 first_x_assum (qspecl_then [`p0 ++ r ++ l`, `s`, `t`] mp_tac) 64 ] >> 65 simp[] >> disch_then (qxchl [`ps`, `ss`] strip_assume_tac) >> 66 map_every qexists_tac [`ps`, `ss`] >> simp[] >> 67 match_mp_tac RTC_R_I >> simp[derive_def] >> metis_tac[]) 68 69val nullable_CONS_TOK = store_thm( 70 "nullable_CONS_TOK[simp]", 71 ``nullable G (TOK t :: rest) = F``, 72 simp[nullable_def] >> strip_tac >> 73 qspecl_then [`G`, `[]`, `rest`, `t`, `[]`] mp_tac derives_TOK >> simp[]) 74 75val nullable_NIL = store_thm( 76 "nullable_NIL[simp]", 77 ``nullable G [] = T``, 78 simp[nullable_def]) 79 80val nullable_CONS_NT = store_thm( 81 "nullable_CONS_NT", 82 ``nullable G (NT n :: rest) <=> 83 nullable G rest ��� n ��� FDOM G.rules ��� 84 ���r. r ��� G.rules ' n ��� nullable G r``, 85 simp[nullable_def] >> REVERSE eq_tac 86 >- (strip_tac >> match_mp_tac RTC_R_I >> simp[derive_def] >> 87 qexists_tac `r ++ rest` >> REVERSE conj_tac 88 >- metis_tac[derives_paste_horizontally, listTheory.APPEND] >> 89 qexists_tac `[]` >> simp[]) >> 90 `NT n :: rest = [NT n] ++ rest` by simp[] >> pop_assum SUBST1_TAC >> 91 simp[derives_split_horizontally] >> strip_tac >> 92 Q.UNDISCH_THEN `derives G [NT n] []` 93 (mp_tac o SIMP_RULE (srw_ss()) [Once relationTheory.RTC_CASES1]) >> 94 metis_tac[]); 95 96 97 98val paireq = prove( 99 ``(x,y) = z ��� x = FST z ��� y = SND z``, Cases_on `z` >> simp[]) 100 101val GSPEC_INTER = prove( 102 ``GSPEC f ��� Q = 103 GSPEC (S ($, o FST o f) (S ($/\ o SND o f) (Q o FST o f)))``, 104 simp[GSPECIFICATION, EXTENSION, SPECIFICATION] >> qx_gen_tac `e` >> 105 simp[paireq] >> metis_tac[]) 106 107val _ = SIMP_CONV (srw_ss())[GSPEC_INTER, combinTheory.o_ABS_R, combinTheory.S_ABS_R, combinTheory.S_ABS_L, pairTheory.o_UNCURRY_R, pairTheory.S_UNCURRY_R] ``{ n + m | n > 10 ��� m < 3 } ��� Q`` 108 109(* nullableML is an "executable" version of nullable that examines the grammar 110 to determine nullability. I put the "executable" in quotes because of the 111 scary looking set comprehension below. This will work fine if the 112 sets of rules for non-terminals are always finite. *) 113val nullableML_def = tDefine "nullableML" ` 114 nullableML seen [] = T ��� 115 nullableML seen (TOK t :: _) = F ��� 116 nullableML seen (NT n :: rest) = 117 if n ��� FDOM G.rules ��� n ��� seen then 118 if G.rules ' n ��� { r | nullableML (n INSERT seen) r } = ��� then F 119 else nullableML seen rest 120 else F 121` 122 (WF_REL_TAC `measure (��s. CARD (FDOM G.rules DIFF s)) LEX measure LENGTH` >> 123 rpt strip_tac >> simp[] >> DISJ1_TAC >> simp[CARD_DIFF_EQN] >> 124 simp[Once INTER_COMM] >> simp[INSERT_INTER] >> 125 simp[FINITE_INTER] >> simp[Once INTER_COMM] >> 126 simp[arithmeticTheory.SUB_LEFT_LESS] >> 127 match_mp_tac arithmeticTheory.LESS_LESS_EQ_TRANS >> 128 qexists_tac `CARD (n INSERT FDOM G.rules ��� seen)` >> 129 conj_tac >- simp[] >> 130 `FINITE (FDOM G.rules)` by simp[] >> 131 pop_assum (MATCH_MP_TAC o MATCH_MP CARD_SUBSET) >> 132 simp[SUBSET_DEF]) 133 134val nullableML_nullable = store_thm( 135 "nullableML_nullable", 136 ``���sn sf. nullableML G sn sf ��� nullable G sf``, 137 HO_MATCH_MP_TAC (theorem "nullableML_ind") >> 138 simp[nullableML_def, nullable_CONS_NT] >> 139 map_every qx_gen_tac [`sn`, `N`, `sf`] >> rpt strip_tac >> 140 qpat_x_assum `SS ��� ���` mp_tac >> simp[EXTENSION] >> metis_tac[]); 141 142 143val ptree_NTs_def = tDefine "ptree_NTs" ` 144 (ptree_NTs (Lf (l,_)) = case l of NT N => {N} | _ => ���) ��� 145 (ptree_NTs (Nd (n,_) subs) = n INSERT BIGUNION (IMAGE ptree_NTs (set subs))) 146` 147 (WF_REL_TAC `measure ptree_size` >> Induct_on `subs` >> simp[] >> fs[] >> 148 rpt strip_tac >> res_tac >> asimp[]) 149 150val ptree_rptfree_def = tDefine "ptree_rptfree" ` 151 ptree_rptfree (Lf _) = T ��� 152 ptree_rptfree (Nd (N,_) subs) = 153 ���s. MEM s subs ��� ptree_rptfree s ��� N ��� ptree_NTs s 154` 155 (WF_REL_TAC `measure ptree_size` >> Induct_on `subs` >> simp[] >> fs[] >> 156 rpt strip_tac >> res_tac >> asimp[]) 157 158val nullableML_by_singletons = store_thm( 159 "nullableML_by_singletons", 160 ``nullableML G sn sf ��� ���a. MEM a sf ��� nullableML G sn [a]``, 161 Induct_on `sf` >> dsimp[nullableML_def] >> qx_gen_tac `h` >> 162 Cases_on `h` >> simp[nullableML_def, CONJ_ASSOC]); 163 164val nullable_by_singletons = store_thm( 165 "nullable_by_singletons", 166 ``nullable G sf ��� ���a. MEM a sf ��� nullable G [a]``, 167 Induct_on `sf` >> simp[] >> qx_gen_tac `h` >> Cases_on `h` >> 168 dsimp[nullable_CONS_NT] >> metis_tac[]) 169 170val ptree_nullableML = store_thm( 171 "ptree_nullableML", 172 ``���pt sn. DISJOINT (ptree_NTs pt) sn ��� ptree_fringe pt = [] ��� 173 valid_ptree G pt ��� ptree_rptfree pt ��� 174 nullableML G sn [ptree_head pt]``, 175 HO_MATCH_MP_TAC grammarTheory.ptree_ind >> 176 strip_tac >- (rw[] >> Cases_on`pt` >> fs[]) >> 177 qx_gen_tac `subs` >> strip_tac >> dsimp[] >> 178 dsimp[FLAT_EQ_NIL, listTheory.MEM_MAP] >> 179 map_every qx_gen_tac [`N`, `sn`] >> Cases_on `N` >> 180 simp[nullableML_def, ptree_NTs_def, ptree_rptfree_def] >> 181 strip_tac >> simp[EXTENSION] >> 182 qexists_tac `MAP ptree_head subs` >> simp[] >> 183 simp[Once nullableML_by_singletons] >> dsimp[listTheory.MEM_MAP] >> 184 rw[] >> res_tac >> rw[]); 185 186val rptfree_subtree = store_thm( 187 "rptfree_subtree", 188 ``���pt : (��,��,��) parsetree. 189 ptree_rptfree pt ��� N ��� ptree_NTs pt ��� ptree_fringe pt = [] ��� 190 valid_ptree G pt ��� 191 ���pt' : (��,��,��) parsetree. 192 ptree_rptfree pt' ��� ptree_head pt' = NT N ��� 193 ptree_fringe pt' = [] ��� valid_ptree G pt'``, 194 HO_MATCH_MP_TAC grammarTheory.ptree_ind >> 195 strip_tac >- (rw[] >> Cases_on`pt` >> fs[]) >> 196 simp[ptree_rptfree_def, ptree_NTs_def] >> qx_gen_tac `subs` >> strip_tac >> 197 dsimp[listTheory.MEM_MAP, FLAT_EQ_NIL] >> 198 NTAC 2 strip_tac >> 199 Cases_on `pt` >> 200 fs[ptree_rptfree_def, FLAT_EQ_NIL, listTheory.MEM_MAP,ptree_NTs_def] 201 >-(qexists_tac `Nd (N, ARB) subs` >> 202 fs[ptree_rptfree_def, FLAT_EQ_NIL, listTheory.MEM_MAP] >> dsimp[]) >> 203 metis_tac[]); 204 205val rptfree_nullable_ptrees_possible = store_thm( 206 "rptfree_nullable_ptrees_possible", 207 ``���pt : (��,��,��) parsetree. 208 valid_ptree G pt ��� ptree_fringe pt = [] ��� 209 ���pt' : (��,��,��) parsetree. 210 valid_ptree G pt' ��� ptree_head pt' = ptree_head pt ��� 211 ptree_fringe pt' = [] ��� ptree_rptfree pt'``, 212 HO_MATCH_MP_TAC grammarTheory.ptree_ind >> 213 strip_tac >- (rw[] >> Cases_on`pt` >> fs[]) >> 214 dsimp[FLAT_EQ_NIL, listTheory.MEM_MAP] >> 215 map_every qx_gen_tac [`subs`, `N`] >> rpt strip_tac >> 216 Cases_on `N` >> fs[] >> 217 `���subs' : (��,��,��) parsetree list. 218 MAP ptree_head subs' = MAP ptree_head subs ��� 219 ���p. MEM p subs' ��� 220 valid_ptree G p ��� ptree_fringe p = [] ��� 221 ptree_rptfree p` 222 by (qpat_x_assum `MAP ptree_head subs ��� G.rules ' q` (K ALL_TAC) >> 223 Induct_on `subs` >- (rpt strip_tac >> qexists_tac `[]` >> simp[]) >> 224 dsimp[] >> qx_gen_tac `h` >> rpt strip_tac >> fs[] >> 225 qexists_tac `pt'::subs'` >> dsimp[] >> metis_tac[]) >> 226 Cases_on `���pt. MEM pt subs' ��� q ��� ptree_NTs pt` 227 >- (fs[] >> metis_tac[rptfree_subtree]) >> 228 fs[] >> qexists_tac `Nd (q,r) subs'` >> 229 dsimp[ptree_rptfree_def, FLAT_EQ_NIL, listTheory.MEM_MAP] >> metis_tac[]) 230 231val nullable_nullableML = store_thm( 232 "nullable_nullableML", 233 ``���sf. nullable G sf ��� nullableML G ��� sf``, 234 simp[Once nullable_by_singletons, Once nullableML_by_singletons] >> 235 ntac 2 strip_tac >> qx_gen_tac `a` >> strip_tac >> 236 `nullable G [a]` by res_tac >> 237 `derives G [a] []` by fs[nullable_def] >> 238 qspecl_then [`Lf (a, ARB)`, `[]`] mp_tac ptrees_derive_extensible >> simp[] >> 239 disch_then (qxchl [`pt`] strip_assume_tac) >> 240 `���pt' : (��,��)lfptree. 241 ptree_rptfree pt' ��� ptree_head pt' = ptree_head pt ��� 242 ptree_fringe pt' = [] ��� valid_ptree G pt'` 243 by metis_tac [rptfree_nullable_ptrees_possible] >> 244 Q.ISPECL_THEN [`pt'`] assume_tac ptree_nullableML >> 245 pop_assum (qspecl_then [`���`] mp_tac) >> simp[]); 246 247val nullableML_EQN = store_thm( 248 "nullableML_EQN", 249 ``nullable G sf ��� nullableML G ��� sf``, 250 metis_tac[nullable_nullableML, nullableML_nullable]) 251 252(* ---------------------------------------------------------------------- 253 Calculating first sets 254 ---------------------------------------------------------------------- *) 255 256val firstSet_def = Define` 257 firstSet G sf = { t | ���rest. derives G sf (TOK t :: rest) } 258`; 259 260val firstSet_nonempty_fringe = store_thm( 261 "firstSet_nonempty_fringe", 262 ``���pt t rest. ptree_fringe pt = TOK t :: rest ��� valid_ptree G pt ��� 263 t ��� firstSet G [ptree_head pt]``, 264 simp[firstSet_def] >> metis_tac [grammarTheory.valid_ptree_derive]); 265 266val IN_firstSet = store_thm( 267 "IN_firstSet", 268 ``t ��� firstSet G [sym] ��� 269 ���pt:(��,��)lfptree rest. 270 ptree_head pt = sym ��� valid_ptree G pt ��� 271 ptree_fringe pt = TOK t :: rest``, 272 simp[firstSet_def] >> 273 metis_tac [grammarTheory.ptrees_derive_extensible 274 |> Q.SPECL [`Lf (sym,())`, `TOK t :: rest`] 275 |> SIMP_RULE (srw_ss()) []]); 276 277val derives_preserves_leading_toks = store_thm( 278 "derives_preserves_leading_toks", 279 ``���G syms rest x. 280 derives G (MAP TOK syms ++ rest) x ��� 281 ���rest'. derives G rest rest' ��� x = MAP TOK syms ++ rest'``, 282 rpt gen_tac >> eq_tac 283 >- (`���x y. derives G x y ��� 284 ���syms rest. 285 (x = MAP TOK syms ++ rest) ��� 286 ���rest'. derives G rest rest' ��� y = MAP TOK syms ++ rest'` 287 suffices_by metis_tac[] >> 288 ho_match_mp_tac relationTheory.RTC_INDUCT >> rw[] >> 289 fs[grammarTheory.derive_def] >> rveq >> 290 qpat_x_assum `MAP TOK syms ++ rest = Y` mp_tac >> 291 dsimp[listTheory.APPEND_EQ_APPEND, MAP_EQ_APPEND, MAP_EQ_CONS, 292 listTheory.APPEND_EQ_SING] >> rw[] >> 293 first_x_assum (qspec_then `syms` mp_tac) >> 294 simp_tac bool_ss [listTheory.APPEND_11, GSYM APPEND_ASSOC] >> 295 rw[] >> 296 metis_tac [grammarTheory.derive_def, relationTheory.RTC_CASES1, 297 listTheory.APPEND]) >> 298 rw[] >> match_mp_tac grammarTheory.derives_paste_horizontally >> 299 simp[]); 300 301val firstSet_NIL = Store_thm( 302 "firstSet_NIL", 303 ``firstSet G [] = {}``, 304 simp[firstSet_def] >> simp[Once relationTheory.RTC_CASES1] >> 305 simp[grammarTheory.derive_def]); 306 307val firstSet_TOK = store_thm( 308 "firstSet_TOK[simp]", 309 ``firstSet G (TOK t::rest) = {t}``, 310 simp[firstSet_def, EXTENSION, EQ_IMP_THM] >> rw[] 311 >- (qspecl_then [`G`, `[t]`, `rest`] mp_tac derives_preserves_leading_toks >> 312 simp[] >> strip_tac >> fs[]) >> 313 metis_tac[relationTheory.RTC_REFL]); 314 315val firstSet_NT = store_thm( 316 "firstSet_NT", 317 ``firstSet G (NT N :: rest) = 318 if N ��� FDOM G.rules then 319 BIGUNION (IMAGE (firstSet G) (G.rules ' N)) ��� 320 (if nullable G [NT N] then firstSet G rest 321 else {}) 322 else {}``, 323 reverse (Cases_on `N ��� FDOM G.rules`) 324 >- simp[firstSet_def, derives_leading_nonNT] >> 325 simp[Once EXTENSION] >> qx_gen_tac `t` >> reverse eq_tac 326 >- (dsimp[] >> rw[] >> fs[firstSet_def] 327 >- (asm_match `rhs ��� G.rules ' N` >> 328 asm_match `derives G rhs (TOK t :: rest0)` >> 329 qexists_tac`rest0 ++ rest` >> 330 match_mp_tac RTC_R_I >> 331 qexists_tac `rhs ++ rest` >> simp[grammarTheory.derive_def] >> 332 metis_tac [listTheory.APPEND, APPEND_ASSOC, 333 grammarTheory.derives_paste_horizontally, 334 relationTheory.RTC_REFL]) >> 335 fs[nullable_def] >> 336 metis_tac [listTheory.APPEND, 337 grammarTheory.derives_paste_horizontally]) >> 338 dsimp[firstSet_def] >> qx_gen_tac `rest'` >> strip_tac >> 339 `���Z1 Z2. derives G [NT N] Z1 ��� derives G rest Z2 ��� 340 (TOK t :: rest' = Z1 ++ Z2)` 341 by metis_tac [derives_split_horizontally, listTheory.APPEND] >> 342 Cases_on `Z1` 343 >- (`nullableNT G N` by fs[nullable_def] >> fs[] >> metis_tac[]) >> 344 fs[] >> rveq >> 345 qpat_x_assum `derives G [NT N] X` 346 (mp_tac o ONCE_REWRITE_RULE [relationTheory.RTC_CASES1]) >> 347 simp[] >> metis_tac[]); 348 349val firstSetML_def = tDefine "firstSetML" ` 350 firstSetML seen [] = {} ��� 351 firstSetML seen (TOK t :: _) = {t} ��� 352 firstSetML seen (NT n :: rest) = 353 if n ��� FDOM G.rules then 354 (if n ��� seen then 355 BIGUNION (IMAGE (firstSetML (n INSERT seen)) 356 (G.rules ' n)) 357 else {}) ��� 358 (if nullable G [NT n] then firstSetML seen rest 359 else {}) 360 else {} 361` 362 (WF_REL_TAC `measure (��s. CARD (FDOM G.rules DIFF s)) LEX measure LENGTH` >> 363 simp[] >> rw[] >> DISJ1_TAC >> simp[CARD_DIFF_EQN] >> 364 simp[Once INTER_COMM] >> simp[INSERT_INTER] >> 365 simp[FINITE_INTER] >> simp[Once INTER_COMM] >> 366 simp[arithmeticTheory.SUB_LEFT_LESS] >> 367 match_mp_tac arithmeticTheory.LESS_LESS_EQ_TRANS >> 368 qexists_tac `CARD (n INSERT FDOM G.rules ��� seen)` >> 369 conj_tac >- simp[] >> 370 `FINITE (FDOM G.rules)` by simp[] >> 371 pop_assum (MATCH_MP_TAC o MATCH_MP CARD_SUBSET) >> 372 simp[SUBSET_DEF]) 373 374val firstSetML_firstSet = store_thm( 375 "firstSetML_firstSet", 376 ``���seen sf. firstSetML G seen sf ��� firstSet G sf``, 377 ho_match_mp_tac (theorem "firstSetML_ind") >> simp[firstSetML_def] >> 378 map_every qx_gen_tac [`seen`, `N`, `sf`] >> strip_tac >> 379 reverse (Cases_on `N ��� FDOM G.rules`) >> fs[] >> 380 reverse conj_tac 381 >- (rw[] >> fs[] >> simp[firstSet_NT] >> fs[SUBSET_DEF]) >> 382 Cases_on `N ��� seen` >> simp[] >> 383 dsimp[SUBSET_DEF] >> simp[firstSet_NT] >> rpt strip_tac >> 384 DISJ1_TAC >> dsimp[] >> fs[SUBSET_DEF] >> metis_tac[]); 385 386val nts_derive_def = Define` 387 (nts_derive G [] tok ��� F) ��� 388 (nts_derive G [N] tok ��� 389 N ��� FDOM G.rules ��� 390 ���p s. p ++ [TOK tok] ++ s ��� G.rules ' N ��� 391 nullable G p) ��� 392 (nts_derive G (N1::N2::NS) tok ��� 393 N1 ��� FDOM G.rules ��� 394 ���p s. p ++ [NT N2] ++ s ��� G.rules ' N1 ��� 395 nullable G p ��� 396 nts_derive G (N2::NS) tok) 397`; 398val _ = export_rewrites ["nts_derive_def"] 399 400val nts_derive_APPEND_E = store_thm( 401 "nts_derive_APPEND_E", 402 ``nts_derive G (n1 ++ n2) t ��� n2 ��� [] ��� nts_derive G n2 t``, 403 Induct_on `n1` >> simp[] >> reverse (Cases_on `n1`) 404 >- (rpt strip_tac >> fs[]) >> 405 fs[] >> Cases_on `n2` >> simp[] >> metis_tac[]); 406 407val firstSetML_nullable_prefix = store_thm( 408 "firstSetML_nullable_prefix", 409 ``x ��� firstSetML G sn sf ��� nullable G p ��� 410 x ��� firstSetML G sn (p ++ sf)``, 411 Induct_on `p` >> simp[] >> Cases >> 412 simp[firstSetML_def, nullable_CONS_NT]); 413 414val firstSetML_CONS_I = store_thm( 415 "firstSetML_CONS_I", 416 ``tk ��� firstSetML G sn [h] ��� tk ��� firstSetML G sn (h::t)``, 417 Cases_on `h` >> simp[firstSetML_def] >> rw[]); 418 419val firstSet_CONS_I = store_thm( 420 "firstSet_CONS_I", 421 ``tk ��� firstSet G [h] ��� tk ��� firstSet G (h::t)``, 422 Cases_on `h` >> simp[firstSet_NT] >> rw[]); 423 424val distinct_nts_derive_firstSetML = store_thm( 425 "distinct_nts_derive_firstSetML", 426 ``���sn. nts_derive G ns tok ��� ALL_DISTINCT ns ��� 427 set ns ��� sn = ��� ��� 428 tok ��� firstSetML G sn [NT (HD ns)]``, 429 Induct_on `ns` >> simp[] >> 430 Cases_on `ns` 431 >- (simp[firstSetML_def] >> map_every qx_gen_tac [`N`, `seen`] >> 432 simp[Once EXTENSION] >> dsimp[] >> 433 map_every qx_gen_tac [`p`, `s`] >> strip_tac >> 434 qexists_tac `p ++ [TOK tok] ++ s` >> simp[] >> 435 REWRITE_TAC [GSYM APPEND_ASSOC] >> 436 match_mp_tac firstSetML_nullable_prefix >> 437 simp[firstSetML_def]) >> 438 simp[EXTENSION] >> rpt strip_tac >> 439 asm_match `p ++ [NT N'] ++ s ��� G.rules ' N` >> 440 simp[firstSetML_def] >> `N ��� sn` by metis_tac[] >> 441 dsimp[] >> qexists_tac `p ++ [NT N'] ++ s` >> simp[] >> 442 REWRITE_TAC [GSYM APPEND_ASSOC] >> 443 match_mp_tac firstSetML_nullable_prefix >> simp[] >> 444 match_mp_tac firstSetML_CONS_I >> fs[] >> 445 first_x_assum match_mp_tac >> simp[EXTENSION] >> 446 metis_tac[]); 447 448val heads_give_first = prove( 449 ``FLAT (MAP ptree_fringe subs) = tk :: rest ��� 450 ���p sym s r0. 451 p ++ [sym] ++ s = subs ��� ptree_fringe sym = tk :: r0 ��� 452 FLAT (MAP ptree_fringe p) = []``, 453 Induct_on `subs` >> simp[] >> simp[APPEND_EQ_CONS] >> rpt strip_tac >> 454 dsimp[] >>fs[] >> map_every qexists_tac [`sym`, `s`, `r0`, `p`] >> simp[]); 455 456val nullable_alltrees = store_thm( 457 "nullable_alltrees", 458 ``nullable G sf ��� 459 ���sym. MEM sym sf ��� 460 ���pt:(��,��)lfptree. 461 valid_ptree G pt ��� ptree_head pt = sym ��� ptree_fringe pt = []``, 462 simp[Once nullable_by_singletons] >> eq_tac >> rpt strip_tac >> res_tac 463 >- (pop_assum mp_tac >> simp_tac (srw_ss())[nullable_def] >> 464 simp[singleton_derives_ptree]) >> 465 simp[nullable_def] >> rw[] >> metis_tac [valid_ptree_derive]); 466 467val MEM_last_strip = prove( 468 ``���l. MEM e l ��� ���p s. l = p ++ [e] ++ s ��� ��MEM e s``, 469 ho_match_mp_tac rich_listTheory.SNOC_INDUCT >> dsimp[] >> conj_tac 470 >- (qx_gen_tac `l` >> strip_tac >> map_every qexists_tac [`l`, `[]`] >> 471 simp[]) >> 472 map_every qx_gen_tac [`l`, `x`] >> rpt strip_tac >> fs[] >> 473 Cases_on `x = e` 474 >- (map_every qexists_tac [`p ++ [e] ++ s`, `[]`] >> simp[]) >> 475 map_every qexists_tac [`p`, `s ++ [x]`] >> simp[]); 476 477val firstSet_nts_derive = store_thm( 478 "firstSet_nts_derive", 479 ``tk ��� firstSet G [NT N] ��� 480 ���Ns. ALL_DISTINCT Ns ��� nts_derive G Ns tk ��� HD Ns = N``, 481 strip_tac >> pop_assum (strip_assume_tac o MATCH_MP IN_firstSet) >> 482 rpt (pop_assum mp_tac) >> map_every qid_spec_tac [`N`, `rest`, `pt`] >> 483 ho_match_mp_tac ptree_ind >> simp[] >> rpt strip_tac 484 >- (rw[] >> Cases_on`pt` >> fs[]) >> 485 Cases_on `pt` >> fs[] >> 486 imp_res_tac heads_give_first >> rveq >> fs[DISJ_IMP_THM, FORALL_AND_THM] >> 487 `nullable G (MAP ptree_head p)` 488 by (dsimp[nullable_alltrees, MEM_MAP] >> 489 full_simp_tac (srw_ss() ++ boolSimps.DNF_ss) [MEM_MAP, FLAT_EQ_NIL] >> 490 metis_tac[]) >> 491 Cases_on `sym` >> Cases_on `p'` >> fs[] 492 >- (qexists_tac `[N]` >> simp[] >> metis_tac[]) >> 493 Cases_on `MEM N Ns` 494 >- ( 495 pop_assum (qxchl [`Ns0`, `Ns1`] strip_assume_tac o 496 MATCH_MP MEM_last_strip) >> 497 `nts_derive G (N::Ns1) tk` 498 by (match_mp_tac (GEN_ALL nts_derive_APPEND_E) >> simp[] >> 499 fs[] >> qexists_tac `Ns0` >> 500 RULE_ASSUM_TAC (REWRITE_RULE[GSYM APPEND_ASSOC, APPEND]) >> 501 simp[]) >> 502 qexists_tac `N::Ns1` >> simp[] >> fs[ALL_DISTINCT_APPEND] 503 ) >> 504 qexists_tac `N::Ns` >> simp[] >> Cases_on `Ns` >> fs[] >> metis_tac[]); 505 506val firstSet_singleton = store_thm( 507 "firstSet_singleton", 508 ``tk ��� firstSet G sf ��� 509 ���p e s. sf = p ++ [e] ++ s ��� nullable G p ��� tk ��� firstSet G [e]``, 510 Induct_on `sf` >> simp[] >> Cases_on `h` >> simp[] >> eq_tac >> strip_tac 511 >- (map_every qexists_tac [`[]`, `TOK tk`, `sf`] >> simp[]) 512 >- (fs[APPEND_EQ_CONS] >> rw[] >> fs[]) 513 >- (fs[firstSet_NT] >> pop_assum mp_tac >> rw[] 514 >- (asm_match `rhs ��� G.rules ' N` >> 515 map_every qexists_tac [`[]`, `NT N`, `sf`] >> simp[] >> 516 dsimp[firstSet_NT] >> metis_tac[]) 517 >- (asm_match `nullableNT G N` >> asm_match `tk ��� firstSet G [e]` >> 518 asm_match `nullable G p` >> 519 map_every qexists_tac [`NT N::p`, `e`] >> simp[] >> 520 simp[Once nullable_by_singletons, DISJ_IMP_THM, FORALL_AND_THM] >> 521 metis_tac[nullable_by_singletons]) >> 522 asm_match `tk ��� firstSet G rhs` >> asm_match `rhs ��� G.rules ' N` >> 523 map_every qexists_tac [`[]`, `NT N`, `sf`] >> simp[] >> 524 simp[firstSet_NT] >> metis_tac[]) >> 525 Cases_on `p` >> fs[] >> rw[] >- simp[firstSet_CONS_I] >> 526 fs[Once nullable_by_singletons, DISJ_IMP_THM, FORALL_AND_THM] >> 527 simp[firstSet_NT] >> fs[nullable_CONS_NT] >> metis_tac[]); 528 529val firstSet_firstSetML = store_thm( 530 "firstSet_firstSetML", 531 ``tk ��� firstSet G sf ��� tk ��� firstSetML G {} sf``, 532 simp[Once firstSet_singleton] >> rw[] >> REWRITE_TAC [GSYM APPEND_ASSOC] >> 533 match_mp_tac firstSetML_nullable_prefix >> simp[] >> 534 match_mp_tac firstSetML_CONS_I >> 535 asm_match `tk ��� firstSet G [sym]` >> 536 Cases_on `sym` >> fs[] >- simp[firstSetML_def] >> 537 imp_res_tac firstSet_nts_derive >> rw[] >> 538 match_mp_tac distinct_nts_derive_firstSetML >> simp[]); 539 540val firstSetML_eqn = store_thm( 541 "firstSetML_eqn", 542 ``firstSet G sf = firstSetML G {} sf``, 543 simp[EXTENSION, EQ_IMP_THM, firstSet_firstSetML] >> 544 metis_tac [SUBSET_DEF, firstSetML_firstSet]); 545 546val _ = export_theory() 547