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