1open HolKernel Parse boolLib bossLib 2 3open boolSimps lcsymtacs 4 5open listTheory pred_setTheory finite_mapTheory locationTheory 6 7val FLAT_APPEND = rich_listTheory.FLAT_APPEND 8val rveq = rpt BasicProvers.VAR_EQ_TAC 9fun asm_match q = Q.MATCH_ASSUM_RENAME_TAC q 10 11val _ = new_theory "grammar" 12 13val _ = ParseExtras.tight_equality() 14 15val _ = type_abbrev("inf", ``:'a + num``) 16val _ = Datatype `symbol = TOK 'a | NT ('b inf)`; 17 18val isTOK_def = Define`(isTOK (TOK tok) = T) ��� (isTOK (NT n) = F)` 19val _ = export_rewrites ["isTOK_def"] 20 21val destTOK_def = Define` 22 (destTOK (TOK tk, _) = SOME tk) ��� 23 (destTOK _ = NONE) 24`; 25val _ = export_rewrites ["destTOK_def"] 26 27val _ = Datatype` 28 grammar = <| 29 start : 'b inf; 30 rules : 'b inf |-> ('a,'b)symbol list set 31|> `; 32 33val _ = Datatype` 34 parsetree = Lf (('a,'b) symbol # 'locs) 35 | Nd ('b inf # 'locs) (parsetree list) 36`; 37 38val ptree_loc_def = Define` 39 (ptree_loc (Lf(_,l)) = l)/\ 40 (ptree_loc (Nd(_,l) _) = l)` 41 42val ptree_list_loc = Define` 43 ptree_list_loc l = merge_list_locs (MAP ptree_loc l)` 44 45 46val ptree_size_def = tDefine "ptree_size" ` 47 (ptree_size (Lf _) = 1) ��� 48 (ptree_size (Nd nt children) = 1 + SUM (MAP ptree_size children)) 49` 50(WF_REL_TAC `measure (parsetree_size (K 1) (K 1) (K 1))` >> 51 Induct_on `children` >> 52 rw[definition "parsetree_size_def"] >- decide_tac >> 53 res_tac >> pop_assum (qspecl_then [`p_2`, `p_1`] mp_tac) >> 54 simp_tac (srw_ss()) [] >> decide_tac) 55 56val ptree_size_def = save_thm( 57 "ptree_size_def", 58 CONV_RULE (DEPTH_CONV ETA_CONV) ptree_size_def) 59val _ = export_rewrites ["ptree_size_def"] 60 61val ptree_head_def = Define` 62 (ptree_head (Lf (tok,l)) = tok) ��� 63 (ptree_head (Nd (nt,l) children) = NT nt) 64`; 65val _ = export_rewrites ["ptree_head_def"] 66 67val noneval = Lib.with_flag (computeLib.auto_import_definitions,false) 68fun tzDefine nm q tac = noneval (tDefine nm q) tac 69val valid_ptree_def = tzDefine "valid_ptree" ` 70 (valid_ptree G (Lf _) ��� T) ��� 71 (valid_ptree G (Nd (nt,l) children) ��� 72 nt ��� FDOM G.rules ��� MAP ptree_head children ��� G.rules ' nt ��� 73 ���pt. pt ��� set children ��� valid_ptree G pt)` 74 (WF_REL_TAC `measure (ptree_size o SND)` THEN 75 Induct_on `children` THEN SRW_TAC [][] THEN1 DECIDE_TAC THEN 76 RES_TAC THEN FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []) 77val _ = export_rewrites ["valid_ptree_def"] 78 79val ptree_fringe_def = tDefine "ptree_fringe" ` 80 (ptree_fringe (Lf (t,_)) = [t]) ��� 81 (ptree_fringe (Nd _ children) = FLAT (MAP ptree_fringe children)) 82` (WF_REL_TAC `measure ptree_size` THEN Induct_on `children` THEN 83 SRW_TAC [][ptree_size_def] THEN1 DECIDE_TAC THEN 84 FULL_SIMP_TAC (srw_ss() ++ ETA_ss) [ptree_size_def] THEN 85 RES_TAC THEN DECIDE_TAC) 86 87val ptree_fringe_def = save_thm( 88 "ptree_fringe_def", 89 CONV_RULE (DEPTH_CONV ETA_CONV) ptree_fringe_def) 90val _ = export_rewrites ["ptree_fringe_def"] 91 92val complete_ptree_def = Define` 93 complete_ptree G pt ��� 94 valid_ptree G pt ��� ptree_head pt = NT G.start ��� 95 ���t. t ��� set (ptree_fringe pt) ��� isTOK t` 96 97(* loc-free parse tree *) 98val _ = type_abbrev("lfptree", ``:(��,��,one) parsetree``) 99 100val real_fringe_def = tDefine "real_fringe" ` 101 (real_fringe (Lf t) = [t]) ��� 102 (real_fringe (Nd n ptl) = FLAT (MAP real_fringe ptl)) 103` (WF_REL_TAC `measure ptree_size` >> Induct_on `ptl` >> dsimp[] >> 104 fs[] >> rpt strip_tac >> res_tac >> simp[]); 105val _ = export_rewrites ["real_fringe_def"] 106 107val MAP_TKI_11 = Q.store_thm( 108 "MAP_TKI_11[simp]", 109 ���(MAP (TOK ## I) l1 = MAP (TOK ## I) l2) ��� (l1 = l2)���, 110 simp[listTheory.INJ_MAP_EQ_IFF, 111 pred_setTheory.INJ_DEF, pairTheory.FORALL_PROD]); 112 113val real_fringe_ind = theorem "real_fringe_ind" 114val ptree_fringe_real_fringe = Q.store_thm( 115 "ptree_fringe_real_fringe", 116 ������pt. ptree_fringe pt = MAP FST (real_fringe pt)���, 117 ho_match_mp_tac real_fringe_ind >> 118 simp[pairTheory.FORALL_PROD, MAP_FLAT, MAP_MAP_o, combinTheory.o_ABS_R] >> 119 rpt strip_tac >> AP_TERM_TAC >> simp[MAP_EQ_f]); 120 121val LENGTH_real_fringe = Q.store_thm( 122 "LENGTH_real_fringe", 123 ������pt. LENGTH (real_fringe pt) = LENGTH (ptree_fringe pt)���, 124 simp[ptree_fringe_real_fringe]); 125 126val real_fringe_NIL_ptree_fringe = Q.prove( 127 `���pt. real_fringe pt = [] ��� ptree_fringe pt = []`, 128 simp[ptree_fringe_real_fringe]); 129 130val real_fringe_CONS_ptree_fringe = Q.prove( 131 `���pt rest. real_fringe pt = (TOK t, l) :: rest ��� 132 ���rest'. ptree_fringe pt = TOK t :: rest'`, 133 simp[ptree_fringe_real_fringe]); 134 135val valid_locs_def = tDefine "valid_locs" ��� 136 (valid_locs (Lf _) ��� T) ��� 137 (valid_locs (Nd (_, l) children) ��� 138 l = merge_list_locs (MAP ptree_loc children) ��� 139 ���pt. MEM pt children ��� valid_locs pt)��� 140 (WF_REL_TAC ���measure ptree_size��� >> simp[] >> Induct >> dsimp[] >> 141 rpt strip_tac >> res_tac >> simp[]); 142val _ = export_rewrites ["valid_locs_def"] 143 144val valid_lptree_def = Define ` 145 valid_lptree G pt ��� valid_locs pt ��� valid_ptree G pt 146`; 147 148val valid_lptree_thm = Q.store_thm( 149 "valid_lptree_thm[simp]", 150 ���(valid_lptree G (Lf p) ��� T) ��� 151 (valid_lptree G (Nd (n, l) children) ��� 152 l = merge_list_locs (MAP ptree_loc children) ��� 153 n ��� FDOM G.rules ��� MAP ptree_head children ��� G.rules ' n ��� 154 ���pt. MEM pt children ��� valid_lptree G pt)���, 155 simp[valid_lptree_def] >> metis_tac[]); 156 157val language_def = Define` 158 language G = 159 { ts | 160 ���pt:(��,��)lfptree. complete_ptree G pt ��� ptree_fringe pt = MAP TOK ts }` 161 162val derive_def = Define` 163 derive G sf1 sf2 ��� 164 ���p sym rhs s. sf1 = p ++ [NT sym] ++ s ��� sf2 = p ++ rhs ++ s ��� 165 sym ��� FDOM G.rules ��� rhs ��� G.rules ' sym 166`; 167 168val RTC1 = relationTheory.RTC_RULES |> Q.SPEC `R` |> CONJUNCT2 169 |> Q.GEN `R` 170val qxch = Q.X_CHOOSE_THEN 171fun qxchl [] ttac = ttac 172 | qxchl (q::qs) ttac = qxch q (qxchl qs ttac) 173 174val derive_common_prefix = store_thm( 175 "derive_common_prefix", 176 ``derive G sf1 sf2 ��� derive G (p ++ sf1) (p ++ sf2)``, 177 rw[derive_def] >> metis_tac [APPEND_ASSOC]); 178val derive_common_suffix = store_thm( 179 "derive_common_suffix", 180 ``derive G sf1 sf2 ��� derive G (sf1 ++ s) (sf2 ++ s)``, 181 rw[derive_def] >> metis_tac [APPEND_ASSOC]); 182 183val _ = overload_on ("derives", ``��G. RTC (derive G)``) 184val derive_paste_horizontally = store_thm( 185 "derive_paste_horizontally", 186 ``derive G sf11 sf12 ��� derive G sf21 sf22 ��� 187 derives G (sf11 ++ sf21) (sf12 ++ sf22)``, 188 metis_tac [derive_common_prefix, derive_common_suffix, 189 relationTheory.RTC_RULES]) 190 191val derive_1NT = store_thm( 192 "derive_1NT", 193 ``derive G [NT s] l ��� s ��� FDOM G.rules ��� l ��� G.rules ' s``, 194 rw[derive_def, APPEND_EQ_CONS]); 195val _ = export_rewrites ["derive_1NT"] 196 197val derives_common_prefix = store_thm( 198 "derives_common_prefix", 199 ``���sf1 sf2 p. derives G sf1 sf2 ��� derives G (p ++ sf1) (p ++ sf2)``, 200 simp[GSYM PULL_FORALL] >> 201 ho_match_mp_tac relationTheory.RTC_INDUCT >> rw[] >> 202 metis_tac [relationTheory.RTC_RULES, derive_common_prefix]); 203val derives_common_suffix = store_thm( 204 "derives_common_suffix", 205 ``���sf1 sf2 s. derives G sf1 sf2 ��� derives G (sf1 ++ s) (sf2 ++ s)``, 206 simp[GSYM PULL_FORALL] >> 207 ho_match_mp_tac relationTheory.RTC_INDUCT >> rw[] >> 208 metis_tac [relationTheory.RTC_RULES, derive_common_suffix]); 209 210val derives_paste_horizontally = store_thm( 211 "derives_paste_horizontally", 212 ``derives G sf11 sf12 ��� derives G sf21 sf22 ��� 213 derives G (sf11 ++ sf21) (sf12 ++ sf22)``, 214 metis_tac [relationTheory.RTC_CASES_RTC_TWICE, 215 derives_common_suffix, derives_common_prefix]) 216 217val ptree_ind = save_thm( 218 "ptree_ind", 219 TypeBase.induction_of ``:('a,'b,'l)parsetree`` 220 |> Q.SPECL [`P`, `��l. ���pt. MEM pt l ��� P pt`] 221 |> SIMP_RULE (srw_ss() ++ CONJ_ss) [] 222 |> SIMP_RULE (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] 223 |> Q.GEN `P`); 224 225val valid_ptree_derive = store_thm( 226 "valid_ptree_derive", 227 ``���pt. valid_ptree G pt ��� derives G [ptree_head pt] (ptree_fringe pt)``, 228 ho_match_mp_tac ptree_ind >> rw[] >> Cases_on`pt` >> fs[] >> 229 match_mp_tac RTC1 >> qexists_tac `MAP ptree_head l` >> rw[] >> 230 qpat_x_assum `SS ��� G.rules ' s` (K ALL_TAC) >> Induct_on `l` >> rw[] >> 231 fs[DISJ_IMP_THM, FORALL_AND_THM] >> 232 metis_tac [derives_paste_horizontally, APPEND]); 233 234val FLAT_EQ_APPEND = store_thm( 235 "FLAT_EQ_APPEND", 236 ``FLAT l = x ++ y ��� 237 (���p s. l = p ++ s ��� x = FLAT p ��� y = FLAT s) ��� 238 (���p s ip is. 239 l = p ++ [ip ++ is] ++ s ��� ip ��� [] ��� is ��� [] ��� 240 x = FLAT p ++ ip ��� 241 y = is ++ FLAT s)``, 242 reverse eq_tac >- (rw[] >> rw[rich_listTheory.FLAT_APPEND]) >> 243 map_every qid_spec_tac [`y`,`x`,`l`] >> Induct_on `l` >- simp[] >> 244 simp[] >> map_every qx_gen_tac [`h`, `x`, `y`] >> 245 simp[APPEND_EQ_APPEND] >> 246 disch_then (DISJ_CASES_THEN (qxch `m` strip_assume_tac)) 247 >- (Cases_on `x = []` 248 >- (fs[] >> map_every qexists_tac [`[]`, `m::l`] >> simp[]) >> 249 Cases_on `m = []` 250 >- (fs[] >> disj1_tac >> map_every qexists_tac [`[x]`, `l`] >> 251 simp[]) >> 252 disj2_tac >> 253 map_every qexists_tac [`[]`, `l`, `x`, `m`] >> simp[]) >> 254 `(���p s. l = p ++ s ��� FLAT p = m ��� FLAT s = y) ��� 255 (���p s ip is. 256 l = p ++ [ip ++ is] ++ s ��� m = FLAT p ++ ip ��� ip ��� [] ��� is ��� [] ��� 257 y = is ++ FLAT s)` by metis_tac[] 258 >- (disj1_tac >> map_every qexists_tac [`h::p`, `s`] >> simp[]) >> 259 disj2_tac >> map_every qexists_tac [`h::p`, `s`] >> simp[]) 260 261val FLAT_EQ_NIL = store_thm( 262 "FLAT_EQ_NIL", 263 ``FLAT l = [] ��� ���e. MEM e l ��� e = []``, 264 Induct_on `l` >> simp[DISJ_IMP_THM, FORALL_AND_THM]); 265 266val FLAT_EQ_SING = store_thm( 267 "FLAT_EQ_SING", 268 ``FLAT l = [x] ��� 269 ���p s. l = p ++ [[x]] ++ s ��� FLAT p = [] ��� FLAT s = []``, 270 Induct_on `l` >> simp[] >> simp[APPEND_EQ_CONS] >> 271 simp_tac (srw_ss() ++ DNF_ss) [] >> metis_tac[]); 272 273val fringe_element = store_thm( 274 "fringe_element", 275 ``���pt:(��,��)lfptree p x s. 276 ptree_fringe pt = p ++ [x] ++ s ��� 277 pt = Lf (x,()) ��� p = [] ��� s = [] ��� 278 ���nt ip is ts1 xpt ts2. 279 pt = Nd (nt,()) (ts1 ++ [xpt] ++ ts2) ��� 280 p = FLAT (MAP ptree_fringe ts1) ++ ip ��� 281 s = is ++ FLAT (MAP ptree_fringe ts2) ��� 282 ptree_fringe xpt = ip ++ [x] ++ is``, 283 gen_tac >> 284 `(���tok. pt = Lf (tok,())) ��� (���sym ptl. pt = Nd sym ptl)` 285 by (Cases_on `pt` >> Cases_on `p` >> simp[]) 286 >- simp[APPEND_EQ_CONS] >> 287 simp[] >> pop_assum (K ALL_TAC) >> rpt gen_tac >> 288 simp[Once FLAT_EQ_APPEND] >> 289 disch_then 290 (DISJ_CASES_THEN2 (qxchl [`fsp`, `fss`] strip_assume_tac) mp_tac) 291 >| [ 292 Cases_on `sym` >> simp[] >> 293 qpat_x_assum `p ++ [x] = FLAT fsp` mp_tac >> 294 simp[Once FLAT_EQ_APPEND] >> 295 disch_then 296 (DISJ_CASES_THEN2 (qxchl [`fsp1`, `fsp2`] strip_assume_tac) mp_tac) 297 >| [ 298 qpat_x_assum `[x] = FLAT fsp2` mp_tac >> 299 simp[FLAT_EQ_SING] >> 300 disch_then (qxchl [`nilps`, `nilss`] strip_assume_tac) >> 301 rw[] >> qpat_x_assum `MAP ptree_fringe ptl = XX` mp_tac >> 302 qabbrev_tac `fp = fsp1 ++ nilps` >> 303 qabbrev_tac `fs = nilss ++ fss` >> 304 `fsp1 ++ (nilps ++ [[x]] ++ nilss) ++ fss = fp ++ [[x]] ++ fs` 305 by simp[] >> 306 pop_assum SUBST_ALL_TAC >> 307 simp[MAP_EQ_APPEND] >> 308 disch_then (fn th => 309 `���ts1 ts2 xpt. ptl = ts1 ++ [xpt] ++ ts2 ��� 310 fp = MAP ptree_fringe ts1 ��� 311 fs = MAP ptree_fringe ts2 ��� 312 [x] = ptree_fringe xpt` 313 by metis_tac [th, APPEND_ASSOC]) >> 314 map_every qexists_tac [`[]`, `[]`, `ts1`, `xpt`, `ts2`] >> 315 simp[] >> 316 `FLAT fs = FLAT fss ��� FLAT fp = FLAT fsp1` 317 by metis_tac [rich_listTheory.FLAT_APPEND, APPEND, APPEND_NIL] >> 318 metis_tac[], 319 320 simp[APPEND_EQ_CONS] >> 321 simp[SimpL``(==>)``, LEFT_AND_OVER_OR, EXISTS_OR_THM, 322 FLAT_EQ_SING] >> 323 disch_then (qxchl [`f1`, `snils`, `xp`] strip_assume_tac) >> 324 rw[] >> qabbrev_tac `f2 = snils ++ fss` >> 325 `MAP ptree_fringe ptl = f1 ++ [xp ++ [x]] ++ f2` by simp[Abbr`f2`] >> 326 pop_assum mp_tac >> 327 simp_tac (srw_ss()) [MAP_EQ_APPEND] >> 328 disch_then (fn th => 329 `���pt1 pt2 ptx. ptl = pt1 ++ [ptx] ++ pt2 ��� 330 f1 = MAP ptree_fringe pt1 ��� 331 f2 = MAP ptree_fringe pt2 ��� 332 xp ++ [x] = ptree_fringe ptx` 333 by metis_tac[th,APPEND_ASSOC]) >> 334 map_every qexists_tac [`xp`, `[]`, `pt1`, `ptx`, `pt2`] >> 335 simp[] >> 336 `FLAT f2 = FLAT fss` by simp[Abbr`f2`, rich_listTheory.FLAT_APPEND] >> 337 metis_tac[] 338 ], 339 340 disch_then (qxchl [`f1`, `f2`, `fpx`, `fs`] strip_assume_tac) >> 341 `���fp. fpx = fp ++ [x]` 342 by (qpat_x_assum `p ++ [x] = XX` mp_tac >> 343 simp[APPEND_EQ_APPEND, APPEND_EQ_CONS, DISJ_IMP_THM] >> 344 metis_tac[]) >> 345 qpat_x_assum `MAP ptree_fringe XX = YY` mp_tac >> 346 simp[MAP_EQ_APPEND] >> 347 disch_then (fn th => 348 `���pt1 pt2 ptx. ptl = pt1 ++ [ptx] ++ pt2 ��� 349 f1 = MAP ptree_fringe pt1 ��� 350 f2 = MAP ptree_fringe pt2 ��� 351 fp ++ [x] ++ fs = ptree_fringe ptx` 352 by metis_tac [th,APPEND_ASSOC]) >> 353 Cases_on `sym` >> simp[] >> 354 map_every qexists_tac [`fp`, `fs`, `pt1`, `ptx`, `pt2`] >> 355 simp[] >> rw[] >> fs[] 356 ]); 357 358val derive_fringe = store_thm( 359 "derive_fringe", 360 ``���pt:(��,��)lfptree sf. 361 derive G (ptree_fringe pt) sf ��� valid_ptree G pt ��� 362 ���pt' : (��,��)lfptree. 363 ptree_head pt' = ptree_head pt ��� valid_ptree G pt' ��� 364 ptree_fringe pt' = sf``, 365 ho_match_mp_tac ptree_ind>> rw[] 366 >- ( 367 Cases_on `pt` >> 368 fs[derive_def, APPEND_EQ_CONS] >> 369 qexists_tac `Nd (sym,ARB) (MAP (\x. Lf(x, ARB)) sf)` 370 >> rw[MEM_MAP,ptree_fringe_def] 371 >- rw[MAP_MAP_o, combinTheory.o_DEF] 372 >- rw[] >> 373 rw[MAP_MAP_o, combinTheory.o_DEF] >> 374 pop_assum (K ALL_TAC) >> Induct_on `sf` >> rw[]) >> 375 rename [`Nd ntl pts`] >> Cases_on `ntl` >> rename [`Nd (rootnt,l) pts`] >> 376 qpat_x_assum `derive G XX YY` mp_tac >> 377 simp[derive_def] >> 378 disch_then (qxchl [`pfx`, `nt`, `rhs`, `sfx`] strip_assume_tac) >> 379 qspecl_then [`Nd (rootnt,l) pts`, `pfx`, `NT nt`, `sfx`] 380 mp_tac fringe_element >> 381 fs[] >> 382 disch_then (qxchl [`ip`, `is`, `ts1`, `xpt`, `ts2`] strip_assume_tac) >> 383 rw[] >> 384 fs[FLAT_APPEND, DISJ_IMP_THM, FORALL_AND_THM] >> 385 `derive G (ip ++ [NT nt] ++ is) (ip ++ rhs ++ is)` 386 by metis_tac [derive_def] >> 387 pop_assum 388 (fn th => first_x_assum 389 (fn impth => mp_tac (MATCH_MP impth th))) >> 390 disch_then (qxch `pt'` strip_assume_tac) >> 391 qexists_tac `Nd (rootnt, ()) (ts1 ++ [pt'] ++ ts2)` >> 392 simp[FLAT_APPEND, DISJ_IMP_THM, FORALL_AND_THM]); 393 394val ptrees_derive_extensible = store_thm( 395 "ptrees_derive_extensible", 396 ``���pt:(��,��)lfptree sf. 397 valid_ptree G pt ��� derives G (ptree_fringe pt) sf ��� 398 ���pt':(��,��)lfptree. 399 valid_ptree G pt' ��� ptree_head pt' = ptree_head pt ��� 400 ptree_fringe pt' = sf``, 401 qsuff_tac 402 `���sf1 sf2. 403 derives G sf1 sf2 ��� 404 ���pt:(��,��)lfptree. 405 valid_ptree G pt ��� ptree_fringe pt = sf1 ��� 406 ���pt':(��,��)lfptree. 407 valid_ptree G pt' ��� ptree_head pt' = ptree_head pt ��� 408 ptree_fringe pt' = sf2` 409 >- metis_tac[] >> 410 ho_match_mp_tac relationTheory.RTC_STRONG_INDUCT >> rw[] >> 411 metis_tac [derive_fringe]) 412 413val singleton_derives_ptree = store_thm( 414 "singleton_derives_ptree", 415 ``derives G [h] sf ��� 416 ���pt:(��,��)lfptree. 417 valid_ptree G pt ��� ptree_head pt = h ��� ptree_fringe pt = sf``, 418 strip_tac >> qspec_then `Lf (h,l)` mp_tac ptrees_derive_extensible >> simp[]); 419 420val derives_language = store_thm( 421 "derives_language", 422 ``language G = { ts | derives G [NT G.start] (MAP TOK ts) }``, 423 rw[language_def, EXTENSION, complete_ptree_def] >> eq_tac 424 >- metis_tac[valid_ptree_derive] >> 425 strip_tac >> 426 qspecl_then [`Lf (NT G.start, ())`, `MAP TOK x`] mp_tac 427 ptrees_derive_extensible >> simp[] >> 428 disch_then (qxch `pt` strip_assume_tac) >> qexists_tac `pt` >> 429 simp[] >> dsimp[MEM_MAP]); 430 431val derives_leading_nonNT_E = store_thm( 432 "derives_leading_nonNT_E", 433 ``N ��� FDOM G.rules ��� derives G (NT N :: rest) Y ��� 434 ���rest'. Y = NT N :: rest' ��� derives G rest rest'``, 435 `���X Y. derives G X Y ��� 436 ���N rest. N ��� FDOM G.rules ��� X = NT N :: rest ��� 437 ���rest'. Y = NT N :: rest' ��� derives G rest rest'` 438 suffices_by metis_tac[] >> 439 ho_match_mp_tac relationTheory.RTC_INDUCT >> simp[] >> rw[] >> 440 fs[derive_def, Once APPEND_EQ_CONS] >> 441 fs[APPEND_EQ_CONS] >> rw[] >> fs[] >> 442 match_mp_tac RTC1 >> metis_tac [derive_def]); 443 444val derives_leading_nonNT = store_thm( 445 "derives_leading_nonNT", 446 ``N ��� FDOM G.rules ��� 447 (derives G (NT N :: rest) Y ��� 448 ���rest'. Y = NT N :: rest' ��� derives G rest rest')``, 449 strip_tac >> eq_tac >- metis_tac [derives_leading_nonNT_E] >> 450 rw[] >> 451 metis_tac [APPEND, derives_paste_horizontally, 452 relationTheory.RTC_REFL]); 453 454val RTC_R_I = relationTheory.RTC_RULES |> SPEC_ALL |> CONJUNCT2 |> GEN_ALL 455val derives_split_horizontally = store_thm( 456 "derives_split_horizontally", 457 ``���p s sf. derives G (p ++ s) sf ��� 458 ���sf1 sf2. sf = sf1 ++ sf2 ��� derives G p sf1 ��� derives G s sf2``, 459 rpt gen_tac >> REVERSE eq_tac >- metis_tac [derives_paste_horizontally] >> 460 `���sf0. p ++ s = sf0` by simp[] >> simp[] >> 461 pop_assum 462 (fn th => disch_then 463 (fn th2 => mp_tac th >> map_every qid_spec_tac [`s`, `p`] >> 464 mp_tac th2)) >> 465 map_every qid_spec_tac [`sf`, `sf0`] >> 466 ho_match_mp_tac relationTheory.RTC_INDUCT >> simp[] >> conj_tac 467 >- metis_tac[relationTheory.RTC_REFL] >> 468 map_every qx_gen_tac [`sf0`, `sf'`, `sf`] >> simp[derive_def] >> 469 disch_then (CONJUNCTS_THEN2 470 (qxchl [`pfx`, `N`, `r`, `sfx`] strip_assume_tac) 471 strip_assume_tac) >> rw[] >> 472 qpat_x_assum `X = Y` mp_tac >> simp[listTheory.APPEND_EQ_APPEND_MID] >> 473 disch_then (DISJ_CASES_THEN (qxchl [`l`] strip_assume_tac)) >> rw[] >|[ 474 first_x_assum (qspecl_then [`pfx ++ r ++ l`, `s`] mp_tac), 475 first_x_assum (qspecl_then [`p`, `l ++ r ++ sfx`] mp_tac) 476 ] >> simp[] >> disch_then (qxchl [`sf1`, `sf2`] strip_assume_tac) >> rw[] >> 477 map_every qexists_tac [`sf1`, `sf2`] >> simp[] >> match_mp_tac RTC_R_I >> 478 metis_tac[derive_def]); 479 480val _ = export_theory() 481