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