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