1open HolKernel Parse boolLib bossLib 2open boolSimps 3open grammarTheory finite_mapTheory 4open locationTheory 5 6val _ = new_theory "peg" 7 8(* Based on 9 Koprowski and Binzstok, "TRX: A Formally Verified Parser Interpreter". 10 LMCS vol 7, no. 2. 2011. 11 DOI: 10.2168/LMCS-7(2:18)2011 12*) 13 14val _ = Hol_datatype `pegsym = 15 empty of 'c 16 | any of (('a # locs) -> 'c) 17 | tok of ('a -> bool) => (('a # locs) -> 'c) 18 | nt of 'b inf => ('c -> 'c) 19 | seq of pegsym => pegsym => ('c -> 'c -> 'c) 20 | choice of pegsym => pegsym => ('c + 'c -> 'c) 21 | rpt of pegsym => ('c list -> 'c) 22 | not of pegsym => 'c 23` 24 25val _ = Hol_datatype` 26 peg = <| start : ('a,'b,'c) pegsym ; 27 rules : 'b inf |-> ('a,'b,'c) pegsym |> 28` 29(* Option type should be replaced with sum type (loc. for NONE *) 30val (peg_eval_rules, peg_eval_ind, peg_eval_cases) = Hol_reln` 31 (���s c. peg_eval G (s, empty c) (SOME(s, c))) ��� 32 (���n r s f c. 33 n ��� FDOM G.rules ��� peg_eval G (s, G.rules ' n) (SOME(r,c)) ��� 34 peg_eval G (s, nt n f) (SOME(r, f c))) ��� 35 (���n s f. 36 n ��� FDOM G.rules ��� peg_eval G (s, G.rules ' n) NONE ��� 37 peg_eval G (s, nt n f) NONE) ��� 38 (���h t f. peg_eval G (h::t, any f) (SOME (t, f h))) ��� 39 (���f. peg_eval G ([], any f) NONE) ��� 40 (���e t P f. P (FST e) ��� peg_eval G (e::t, tok P f) (SOME(t, f e))) ��� 41 (���e t P f. ��P (FST e) ��� peg_eval G (e::t, tok P f) NONE) ��� 42 (���P f. peg_eval G ([], tok P f) NONE) ��� 43 (���e s c. peg_eval G (s, e) NONE ��� peg_eval G (s, not e c) (SOME(s,c))) ��� 44 (���e s s' c. peg_eval G (s, e) (SOME s') ��� peg_eval G (s, not e c) NONE) ��� 45 (���e1 e2 s f. peg_eval G (s, e1) NONE ��� peg_eval G (s, seq e1 e2 f) NONE) ��� 46 (���e1 e2 s0 s1 c1 f. 47 peg_eval G (s0, e1) (SOME (s1, c1)) ��� peg_eval G (s1, e2) NONE ��� 48 peg_eval G (s0, seq e1 e2 f) NONE) ��� 49 (���e1 e2 s0 s1 s2 c1 c2 f. 50 peg_eval G (s0, e1) (SOME(s1, c1)) ��� 51 peg_eval G (s1, e2) (SOME(s2, c2)) ��� 52 peg_eval G (s0, seq e1 e2 f) (SOME(s2, f c1 c2))) ��� 53 (���e1 e2 s f. 54 peg_eval G (s, e1) NONE ��� peg_eval G (s, e2) NONE ��� 55 peg_eval G (s, choice e1 e2 f) NONE) ��� 56 (���e1 e2 s s' f c. 57 peg_eval G (s, e1) (SOME(s',c)) ��� 58 peg_eval G (s, choice e1 e2 f) (SOME(s', f (INL c)))) ��� 59 (���e1 e2 s s' f c. 60 peg_eval G (s, e1) NONE ��� peg_eval G (s, e2) (SOME(s',c)) ��� 61 peg_eval G (s, choice e1 e2 f) (SOME(s',f (INR c)))) ��� 62 (���e f s s1 list. 63 peg_eval_list G (s, e) (s1,list) ��� 64 peg_eval G (s, rpt e f) (SOME(s1, f list))) ��� 65 (���e s. peg_eval G (s, e) NONE ��� peg_eval_list G (s, e) (s,[])) ��� 66 (���e s0 s1 s2 c cs. 67 peg_eval G (s0, e) (SOME(s1,c)) ��� 68 peg_eval_list G (s1, e) (s2,cs) ��� 69 peg_eval_list G (s0, e) (s2,c::cs)) 70`; 71 72val peg_eval_strongind' = save_thm( 73 "peg_eval_strongind'", 74 theorem "peg_eval_strongind" 75 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] 76 |> Q.SPECL [`G`, `\es0 r. P1 (FST es0) (SND es0) r`, 77 `\es0 sr. P2 (FST es0) (SND es0) (FST sr) (SND sr)`] 78 |> SIMP_RULE (srw_ss()) []) 79 80open rich_listTheory 81val peg_eval_suffix0 = prove( 82 ``(���s0 e sr. peg_eval G (s0,e) sr ��� ���s r. sr = SOME (s,r) ��� IS_SUFFIX s0 s) ��� 83 ���s0 e s rl. peg_eval_list G (s0,e) (s,rl) ��� IS_SUFFIX s0 s``, 84 HO_MATCH_MP_TAC peg_eval_strongind' THEN SRW_TAC [][IS_SUFFIX_compute, IS_PREFIX_APPEND3, 85 IS_PREFIX_REFL] THEN 86 METIS_TAC [IS_PREFIX_TRANS]); 87 88(* Theorem 3.1 *) 89val peg_eval_suffix = save_thm( 90 "peg_eval_suffix", 91 peg_eval_suffix0 |> SIMP_RULE (srw_ss() ++ DNF_ss) []) 92 93(* Theorem 3.2 *) 94val peg_deterministic = store_thm( 95 "peg_deterministic", 96 ``(���s0 e sr. peg_eval G (s0,e) sr ��� ���sr'. peg_eval G (s0,e) sr' ��� sr' = sr) ��� 97 ���s0 e s rl. peg_eval_list G (s0,e) (s,rl) ��� 98 ���srl'. peg_eval_list G (s0,e) srl' ��� srl' = (s,rl)``, 99 HO_MATCH_MP_TAC peg_eval_strongind' THEN SRW_TAC [][] THEN 100 ONCE_REWRITE_TAC [peg_eval_cases] THEN SRW_TAC [][]); 101 102(* Lemma 3.3 *) 103val peg_badrpt = store_thm( 104 "peg_badrpt", 105 ``peg_eval G (s0,e) (SOME(s0,r)) ��� ���r. ��peg_eval G (s0, rpt e f) r``, 106 strip_tac >> simp[Once peg_eval_cases] >> map_every qx_gen_tac [`s1`, `l`] >> 107 disch_then (assume_tac o MATCH_MP (CONJUNCT2 peg_deterministic)) >> 108 `peg_eval_list G (s0,e) (s1,r::l)` 109 by METIS_TAC [last (peg_eval_rules |> SPEC_ALL |> CONJUNCTS)] >> 110 pop_assum mp_tac >> simp[]); 111 112val (peg0_rules, peg0_ind, peg0_cases) = Hol_reln` 113 (���c. peg0 G (empty c)) ��� 114 115 (* any *) 116 (���f. peggt0 G (any f)) ��� 117 (���f. pegfail G (any f)) ��� 118 119 (* tok *) 120 (���t f. peggt0 G (tok t f)) ��� 121 (���t f. pegfail G (tok t f)) ��� 122 123 (* rpt *) 124 (���e f. pegfail G e ��� peg0 G (rpt e f)) ��� 125 (���e f. peggt0 G e ��� peggt0 G (rpt e f)) ��� 126 127 (* nt rules *) 128 (���n f. n ��� FDOM G.rules ��� peg0 G (G.rules ' n) ��� 129 peg0 G (nt n f)) ��� 130 (���n f. n ��� FDOM G.rules ��� peggt0 G (G.rules ' n) ��� 131 peggt0 G (nt n f)) ��� 132 (���n f. n ��� FDOM G.rules ��� pegfail G (G.rules ' n) ��� 133 pegfail G (nt n f)) ��� 134 135 (* seq rules *) 136 (���e1 e2 f. pegfail G e1 ��� (peg0 G e1 ��� pegfail G e2) ��� 137 (peggt0 G e1 ��� pegfail G e2) ��� 138 pegfail G (seq e1 e2 f)) ��� 139 (���e1 e2 f. peggt0 G e1 ��� (peg0 G e2 ��� peggt0 G e2) ��� 140 (peg0 G e1 ��� peggt0 G e1) ��� peggt0 G e2 ��� 141 peggt0 G (seq e1 e2 f)) ��� 142 (���e1 e2 f. peg0 G e1 ��� peg0 G e2 ��� peg0 G (seq e1 e2 f)) ��� 143 144 (* choice rules *) 145 (���e1 e2 f. peg0 G e1 ��� (pegfail G e1 ��� peg0 G e2) ��� 146 peg0 G (choice e1 e2 f)) ��� 147 (���e1 e2 f. pegfail G e1 ��� pegfail G e2 ��� pegfail G (choice e1 e2 f)) ��� 148 (���e1 e2 f. peggt0 G e1 ��� (pegfail G e1 ��� peggt0 G e2) ��� 149 peggt0 G (choice e1 e2 f)) ��� 150 151 (* not *) 152 (���e c. pegfail G e ��� peg0 G (not e c)) ��� 153 (���e c. peg0 G e ��� peggt0 G e ��� pegfail G (not e c)) 154`; 155 156val peg_eval_suffix' = store_thm( 157 "peg_eval_suffix'", 158 ``peg_eval G (s0,e) (SOME(s,c)) ��� 159 s0 = s ��� IS_SUFFIX s0 s ��� LENGTH s < LENGTH s0``, 160 strip_tac >> imp_res_tac peg_eval_suffix >> Cases_on `s0 = s` >- simp[] >> 161 fs[IS_SUFFIX_compute] >> 162 imp_res_tac IS_PREFIX_LENGTH >> fs[] >> 163 qsuff_tac `LENGTH s ��� LENGTH s0` >- (strip_tac >> decide_tac) >> 164 strip_tac >> 165 metis_tac [IS_PREFIX_LENGTH_ANTI, LENGTH_REVERSE, REVERSE_REVERSE]); 166 167val peg_eval_list_suffix' = store_thm( 168 "peg_eval_list_suffix'", 169 ``peg_eval_list G (s0, e) (s,rl) ��� 170 s0 = s ��� IS_SUFFIX s0 s ��� LENGTH s < LENGTH s0``, 171 strip_tac >> imp_res_tac peg_eval_suffix >> Cases_on `s0 = s` >- simp[] >> 172 fs[IS_SUFFIX_compute] >> imp_res_tac IS_PREFIX_LENGTH >> fs[] >> 173 qsuff_tac `LENGTH s ��� LENGTH s0` >- (strip_tac >> decide_tac) >> strip_tac >> 174 metis_tac [IS_PREFIX_LENGTH_ANTI, LENGTH_REVERSE, REVERSE_REVERSE]); 175 176 177fun rule_match th = FIRST (List.mapPartial (total MATCH_MP_TAC) 178 (th |> SPEC_ALL |> CONJUNCTS)) 179 180val lemma4_1a0 = prove( 181 ``(���s0 e r. peg_eval G (s0, e) r ��� 182 (���c. r = SOME(s0,c) ��� peg0 G e) ��� 183 (r = NONE ��� pegfail G e) ��� 184 (���s c. r = SOME(s,c) ��� LENGTH s < LENGTH s0 ��� peggt0 G e)) ��� 185 (���s0 e s rl. peg_eval_list G (s0,e) (s,rl) ��� 186 (s0 = s ��� pegfail G e) ��� 187 (LENGTH s < LENGTH s0 ��� peggt0 G e))``, 188 ho_match_mp_tac peg_eval_strongind' >> simp[peg0_rules] >> rpt conj_tac 189 >- (rpt strip_tac >> imp_res_tac peg_eval_suffix' >> fs[peg0_rules]) 190 >- (rpt strip_tac >> rule_match peg0_rules >> 191 imp_res_tac peg_eval_suffix' >> fs[] >> rw[] >> 192 full_simp_tac (srw_ss() ++ ARITH_ss) []) 193 >- (rpt strip_tac >> rule_match peg0_rules >> 194 imp_res_tac peg_eval_suffix' >> fs[] >> rw[] >> 195 full_simp_tac (srw_ss() ++ ARITH_ss) []) >> 196 rpt strip_tac 197 >- (first_x_assum match_mp_tac >> rw[] >> 198 imp_res_tac peg_eval_suffix >> fs[IS_SUFFIX_compute] >> 199 imp_res_tac IS_PREFIX_LENGTH >> fs[] >> 200 `LENGTH s = LENGTH s0'` by decide_tac >> 201 metis_tac [IS_PREFIX_LENGTH_ANTI, LENGTH_REVERSE, REVERSE_REVERSE]) >> 202 imp_res_tac peg_eval_suffix' >- rw[] >> 203 imp_res_tac peg_eval_list_suffix' >- rw[] >> 204 asm_simp_tac (srw_ss() ++ ARITH_ss) []) 205 206val lemma4_1a = save_thm("lemma4_1a",lemma4_1a0 |> SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO]) 207 208val (wfpeg_rules, wfpeg_ind, wfpeg_cases) = Hol_reln` 209 (���n f. n ��� FDOM G.rules ��� wfpeg G (G.rules ' n) ��� wfpeg G (nt n f)) ��� 210 (���c. wfpeg G (empty c)) ��� 211 (���f. wfpeg G (any f)) ��� 212 (���t f. wfpeg G (tok t f)) ��� 213 (���e c. wfpeg G e ��� wfpeg G (not e c)) ��� 214 (���e1 e2 f. wfpeg G e1 ��� (peg0 G e1 ��� wfpeg G e2) ��� 215 wfpeg G (seq e1 e2 f)) ��� 216 (���e1 e2 f. wfpeg G e1 ��� wfpeg G e2 ��� wfpeg G (choice e1 e2 f)) ��� 217 (���e f. wfpeg G e ��� ��peg0 G e ��� wfpeg G (rpt e f)) 218` 219 220val subexprs_def = Define` 221 (subexprs (any f1) = { any f1 }) ��� 222 (subexprs (empty c) = { empty c }) ��� 223 (subexprs (tok t f2) = { tok t f2 }) ��� 224 (subexprs (nt s f) = { nt s f }) ��� 225 (subexprs (not e c) = not e c INSERT subexprs e) ��� 226 (subexprs (seq e1 e2 f3) = seq e1 e2 f3 INSERT subexprs e1 ��� subexprs e2) ��� 227 (subexprs (choice e1 e2 f4) = 228 choice e1 e2 f4 INSERT subexprs e1 ��� subexprs e2) ��� 229 (subexprs (rpt e f5) = rpt e f5 INSERT subexprs e) 230` 231val _ = export_rewrites ["subexprs_def"] 232 233 234val subexprs_included = store_thm( 235 "subexprs_included", 236 ``e ��� subexprs e``, 237 Induct_on `e` >> srw_tac[][subexprs_def] ) 238 239val Gexprs_def = Define` 240 Gexprs G = BIGUNION (IMAGE subexprs (G.start INSERT FRANGE G.rules)) 241` 242 243val start_IN_Gexprs = store_thm( 244 "start_IN_Gexprs", 245 ``G.start ��� Gexprs G``, 246 simp[Gexprs_def, subexprs_included]); 247val _ = export_rewrites ["start_IN_Gexprs"] 248 249val wfG_def = Define`wfG G ��� ���e. e ��� Gexprs G ��� wfpeg G e`; 250 251val IN_subexprs_TRANS = store_thm( 252 "IN_subexprs_TRANS", 253 ``���a b c. a ��� subexprs b ��� b ��� subexprs c ��� a ��� subexprs c``, 254 Induct_on `c` >> simp[] >> rpt strip_tac >> fs[] >> metis_tac[]); 255 256val Gexprs_subexprs = store_thm( 257 "Gexprs_subexprs", 258 ``e ��� Gexprs G ��� subexprs e ��� Gexprs G``, 259 simp_tac (srw_ss() ++ DNF_ss) [Gexprs_def, pred_setTheory.SUBSET_DEF] >> 260 strip_tac >> metis_tac [IN_subexprs_TRANS]); 261 262val IN_Gexprs_E = store_thm( 263 "IN_Gexprs_E", 264 ``(not e c ��� Gexprs G ��� e ��� Gexprs G) ��� 265 (seq e1 e2 f ��� Gexprs G ��� e1 ��� Gexprs G ��� e2 ��� Gexprs G) ��� 266 (choice e1 e2 f2 ��� Gexprs G ��� e1 ��� Gexprs G ��� e2 ��� Gexprs G) ��� 267 (rpt e f3 ��� Gexprs G ��� e ��� Gexprs G)``, 268 rpt strip_tac >> imp_res_tac Gexprs_subexprs >> fs[] >> 269 metis_tac [pred_setTheory.SUBSET_DEF, subexprs_included]); 270 271val pair_CASES = pairTheory.pair_CASES 272val option_CASES = optionTheory.option_nchotomy 273val list_CASES = listTheory.list_CASES 274 275val reducing_peg_eval_makes_list = prove( 276 ``(���s. LENGTH s < n ��� ���r. peg_eval G (s, e) r) ��� ��peg0 G e ��� LENGTH s0 < n ��� 277 ���s' rl. peg_eval_list G (s0,e) (s',rl)``, 278 strip_tac >> completeInduct_on `LENGTH s0` >> rw[] >> 279 full_simp_tac (srw_ss() ++ DNF_ss ++ ARITH_ss) [] >> 280 `peg_eval G (s0,e) NONE ��� ���s1 c. peg_eval G (s0,e) (SOME(s1,c))` 281 by metis_tac [pair_CASES, option_CASES] 282 >- metis_tac [peg_eval_rules] >> 283 `s0 ��� s1` by metis_tac [lemma4_1a] >> 284 `LENGTH s1 < LENGTH s0` by metis_tac [peg_eval_suffix'] >> 285 metis_tac [peg_eval_rules]); 286 287val peg_eval_total = store_thm( 288 "peg_eval_total", 289 ``wfG G ��� ���s e. e ��� Gexprs G ��� ���r. peg_eval G (s,e) r``, 290 simp[wfG_def] >> strip_tac >> gen_tac >> 291 completeInduct_on `LENGTH s` >> 292 full_simp_tac (srw_ss() ++ DNF_ss) [] >> rpt strip_tac >> 293 `wfpeg G e` by metis_tac[] >> 294 Q.UNDISCH_THEN `e ��� Gexprs G` mp_tac >> 295 pop_assum mp_tac >> qid_spec_tac `e` >> 296 Induct_on `wfpeg` >> rw[] 297 >- ((* nt *) 298 qsuff_tac `G.rules ' n ��� Gexprs G` 299 >- metis_tac [peg_eval_rules, option_CASES, pair_CASES] >> 300 asm_simp_tac (srw_ss() ++ DNF_ss) [Gexprs_def, FRANGE_DEF] >> 301 metis_tac [subexprs_included]) 302 >- (* empty *) metis_tac [peg_eval_rules] 303 >- (* any *) metis_tac [peg_eval_rules, list_CASES] 304 >- (* tok *) metis_tac [peg_eval_rules, list_CASES] 305 >- (* not *) metis_tac [peg_eval_rules, optionTheory.option_nchotomy, 306 IN_Gexprs_E] 307 >- ((* seq *) Q.MATCH_ASSUM_ABBREV_TAC `seq e1 e2 f ��� Gexprs G` >> 308 markerLib.RM_ALL_ABBREVS_TAC >> 309 `e1 ��� Gexprs G` by imp_res_tac IN_Gexprs_E >> 310 `peg_eval G (s,e1) NONE ��� ���s' c. peg_eval G (s,e1) (SOME(s',c))` 311 by metis_tac[option_CASES, pair_CASES] 312 >- metis_tac [peg_eval_rules] >> 313 Cases_on `s' = s` 314 >- (`peg0 G e1` by metis_tac [lemma4_1a] >> 315 `e2 ��� Gexprs G` by imp_res_tac IN_Gexprs_E >> 316 metis_tac [peg_eval_rules, option_CASES, pair_CASES]) >> 317 `LENGTH s' < LENGTH s` by metis_tac [peg_eval_suffix'] >> 318 `���r'. peg_eval G (s',e2) r'` by metis_tac [IN_Gexprs_E] >> 319 metis_tac [option_CASES, pair_CASES, peg_eval_rules]) 320 >- (* choice *) 321 metis_tac [peg_eval_rules, option_CASES, IN_Gexprs_E, pair_CASES] >> 322 (* rpt *) imp_res_tac IN_Gexprs_E >> 323 `peg_eval G (s, e) NONE ��� ���s' c. peg_eval G (s,e) (SOME (s',c))` 324 by metis_tac [option_CASES, pair_CASES] 325 >- (`peg_eval_list G (s,e) (s,[])` by metis_tac [peg_eval_rules] >> 326 metis_tac [peg_eval_rules]) >> 327 `s' ��� s` by metis_tac [lemma4_1a] >> 328 `LENGTH s' < LENGTH s` by metis_tac [peg_eval_suffix'] >> 329 metis_tac [peg_eval_rules, reducing_peg_eval_makes_list]) 330 331(* derived and useful PEG forms *) 332val pegf_def = Define`pegf sym f = seq sym (empty ARB) (��l1 l2. f l1)` 333 334val ignoreL_def = Define` 335 ignoreL s1 s2 = seq s1 s2 (��a b. b) 336`; 337val _ = set_mapped_fixity{fixity = Infixl 500, term_name = "ignoreL", 338 tok = "~>"} 339 340val ignoreR_def = Define` 341 ignoreR s1 s2 = seq s1 s2 (��a b. a) 342`; 343val _ = set_mapped_fixity{fixity = Infixl 500, term_name = "ignoreR", 344 tok = "<~"} 345 346val choicel_def = Define` 347 (choicel [] = not (empty ARB) ARB) ��� 348 (choicel (h::t) = choice h (choicel t) (��s. sum_CASE s I I)) 349`; 350 351val checkAhead_def = Define` 352 checkAhead P s = not (not (tok P ARB) ARB) ARB ~> s 353`; 354 355val peg_eval_seq_SOME = store_thm( 356 "peg_eval_seq_SOME", 357 ``peg_eval G (i0, seq s1 s2 f) (SOME (i,r)) ��� 358 ���i1 r1 r2. peg_eval G (i0, s1) (SOME (i1,r1)) ��� 359 peg_eval G (i1, s2) (SOME (i,r2)) ��� (r = f r1 r2)``, 360 simp[Once peg_eval_cases] >> metis_tac[]); 361 362val peg_eval_seq_NONE = store_thm( 363 "peg_eval_seq_NONE", 364 ``peg_eval G (i0, seq s1 s2 f) NONE ��� 365 peg_eval G (i0, s1) NONE ��� 366 ���i r. peg_eval G (i0,s1) (SOME(i,r)) ��� 367 peg_eval G (i,s2) NONE``, 368 simp[Once peg_eval_cases] >> metis_tac[]); 369 370val peg_eval_tok_NONE = save_thm( 371 "peg_eval_tok_NONE", 372 ``peg_eval G (i, tok P f) NONE`` 373 |> SIMP_CONV (srw_ss()) [Once peg_eval_cases]) 374 375val peg_eval_tok_SOME = store_thm( 376 "peg_eval_tok_SOME", 377 ``peg_eval G (i0, tok P f) (SOME (i,r)) ��� ���h. P (FST h) ��� i0 = h::i ��� r = f h``, 378 simp[Once peg_eval_cases] >> metis_tac[]); 379 380val peg_eval_empty = store_thm( 381 "peg_eval_empty[simp]", 382 ``peg_eval G (i, empty r) x ��� (x = SOME(i,r))``, 383 simp[Once peg_eval_cases]) 384 385val peg_eval_NT_SOME = store_thm( 386 "peg_eval_NT_SOME", 387 ``peg_eval G (i0,nt N f) (SOME(i,r)) ��� 388 ���r0. r = f r0 ��� N ��� FDOM G.rules ��� 389 peg_eval G (i0,G.rules ' N) (SOME(i,r0))``, 390 simp[Once peg_eval_cases]); 391 392val peg_eval_choice = store_thm( 393 "peg_eval_choice", 394 ``���x. 395 peg_eval G (i0, choice s1 s2 f) x ��� 396 (���i r. peg_eval G (i0, s1) (SOME(i, r)) ��� x = SOME(i, f (INL r))) ��� 397 (���i r. peg_eval G (i0, s1) NONE ��� 398 peg_eval G (i0, s2) (SOME(i, r)) ��� x = SOME(i, f (INR r))) ��� 399 peg_eval G (i0, s1) NONE ��� peg_eval G (i0,s2) NONE ��� (x = NONE)``, 400 simp[Once peg_eval_cases, SimpLHS] >> 401 simp[optionTheory.FORALL_OPTION, pairTheory.FORALL_PROD] >> metis_tac[]); 402 403val peg_eval_choicel_NIL = store_thm( 404 "peg_eval_choicel_NIL[simp]", 405 ``peg_eval G (i0, choicel []) x = (x = NONE)``, 406 simp[choicel_def, Once peg_eval_cases]); 407 408val peg_eval_choicel_CONS = store_thm( 409 "peg_eval_choicel_CONS", 410 ``���x. peg_eval G (i0, choicel (h::t)) x ��� 411 peg_eval G (i0, h) x ��� x <> NONE ��� 412 peg_eval G (i0,h) NONE ��� peg_eval G (i0, choicel t) x``, 413 simp[choicel_def, SimpLHS, Once peg_eval_cases] >> 414 simp[pairTheory.FORALL_PROD, optionTheory.FORALL_OPTION]); 415 416val peg_eval_rpt = store_thm( 417 "peg_eval_rpt", 418 ``peg_eval G (i0, rpt s f) x ��� 419 ���i l. peg_eval_list G (i0,s) (i,l) ��� x = SOME(i,f l)``, 420 simp[Once peg_eval_cases, SimpLHS] >> metis_tac[]); 421 422val peg_eval_list = Q.store_thm( 423 "peg_eval_list", 424 `peg_eval_list G (i0, e) (i, r) ��� 425 peg_eval G (i0, e) NONE ��� i = i0 ��� r = [] ��� 426 (���i1 rh rt. 427 peg_eval G (i0, e) (SOME (i1, rh)) ��� 428 peg_eval_list G (i1, e) (i, rt) ��� r = rh::rt)`, 429 simp[Once peg_eval_cases, SimpLHS] >> metis_tac[]); 430 431val pegfail_empty = store_thm( 432 "pegfail_empty[simp]", 433 ``pegfail G (empty r) = F``, 434 simp[Once peg0_cases]); 435 436val peg0_empty = store_thm( 437 "peg0_empty[simp]", 438 ``peg0 G (empty r) = T``, 439 simp[Once peg0_cases]); 440 441val peg0_not = store_thm( 442 "peg0_not[simp]", 443 ``peg0 G (not s r) ��� pegfail G s``, 444 simp[Once peg0_cases, SimpLHS]); 445 446val peg0_choice = store_thm( 447 "peg0_choice[simp]", 448 ``peg0 G (choice s1 s2 f) ��� peg0 G s1 ��� pegfail G s1 ��� peg0 G s2``, 449 simp[Once peg0_cases, SimpLHS]); 450 451val peg0_choicel = store_thm( 452 "peg0_choicel[simp]", 453 ``(peg0 G (choicel []) = F) ��� 454 (peg0 G (choicel (h::t)) ��� peg0 G h ��� pegfail G h ��� peg0 G (choicel t))``, 455 simp[choicel_def]) 456 457val peg0_seq = store_thm( 458 "peg0_seq[simp]", 459 ``peg0 G (seq s1 s2 f) ��� peg0 G s1 ��� peg0 G s2``, 460 simp[Once peg0_cases, SimpLHS]) 461 462val peg0_tok = store_thm( 463 "peg0_tok[simp]", 464 ``peg0 G (tok P f) = F``, 465 simp[Once peg0_cases]) 466 467val peg0_pegf = store_thm( 468 "peg0_pegf[simp]", 469 ``peg0 G (pegf s f) = peg0 G s``, 470 simp[pegf_def]) 471 472val _ = export_theory() 473