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