|
1 (* Title: POSIX Lexing with Derivatives of Regular Expressions |
|
2 Authors: Fahad Ausaf <fahad.ausaf at icloud.com>, 2016 |
|
3 Roy Dyckhoff <roy.dyckhoff at st-andrews.ac.uk>, 2016 |
|
4 Christian Urban <christian.urban at kcl.ac.uk>, 2016 |
|
5 Maintainer: Christian Urban <christian.urban at kcl.ac.uk> |
|
6 *) |
|
7 |
|
8 theory Lexer |
|
9 imports Derivatives |
|
10 begin |
|
11 |
|
12 section {* Values *} |
|
13 |
|
14 datatype 'a val = |
|
15 Void |
|
16 | Atm 'a |
|
17 | Seq "'a val" "'a val" |
|
18 | Right "'a val" |
|
19 | Left "'a val" |
|
20 | Stars "('a val) list" |
|
21 |
|
22 |
|
23 section {* The string behind a value *} |
|
24 |
|
25 fun |
|
26 flat :: "'a val \<Rightarrow> 'a list" |
|
27 where |
|
28 "flat (Void) = []" |
|
29 | "flat (Atm c) = [c]" |
|
30 | "flat (Left v) = flat v" |
|
31 | "flat (Right v) = flat v" |
|
32 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
|
33 | "flat (Stars []) = []" |
|
34 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
|
35 |
|
36 lemma flat_Stars [simp]: |
|
37 "flat (Stars vs) = concat (map flat vs)" |
|
38 by (induct vs) (auto) |
|
39 |
|
40 section {* Relation between values and regular expressions *} |
|
41 |
|
42 inductive |
|
43 Prf :: "'a val \<Rightarrow> 'a rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
44 where |
|
45 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : Times r1 r2" |
|
46 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : Plus r1 r2" |
|
47 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : Plus r1 r2" |
|
48 | "\<turnstile> Void : One" |
|
49 | "\<turnstile> Atm c : Atom c" |
|
50 | "\<turnstile> Stars [] : Star r" |
|
51 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : Star r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : Star r" |
|
52 |
|
53 inductive_cases Prf_elims: |
|
54 "\<turnstile> v : Zero" |
|
55 "\<turnstile> v : Times r1 r2" |
|
56 "\<turnstile> v : Plus r1 r2" |
|
57 "\<turnstile> v : One" |
|
58 "\<turnstile> v : Atom c" |
|
59 (* "\<turnstile> vs : Star r"*) |
|
60 |
|
61 lemma Prf_flat_lang: |
|
62 assumes "\<turnstile> v : r" shows "flat v \<in> lang r" |
|
63 using assms |
|
64 by(induct v r rule: Prf.induct) (auto) |
|
65 |
|
66 lemma Prf_Stars: |
|
67 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
|
68 shows "\<turnstile> Stars vs : Star r" |
|
69 using assms |
|
70 by(induct vs) (auto intro: Prf.intros) |
|
71 |
|
72 lemma Star_string: |
|
73 assumes "s \<in> star A" |
|
74 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
|
75 using assms |
|
76 by (metis in_star_iff_concat set_mp) |
|
77 |
|
78 lemma Star_val: |
|
79 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
80 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
81 using assms |
|
82 apply(induct ss) |
|
83 apply(auto) |
|
84 apply (metis empty_iff list.set(1)) |
|
85 by (metis concat.simps(2) list.simps(9) set_ConsD) |
|
86 |
|
87 lemma L_flat_Prf1: |
|
88 assumes "\<turnstile> v : r" shows "flat v \<in> lang r" |
|
89 using assms |
|
90 by (induct)(auto) |
|
91 |
|
92 lemma L_flat_Prf2: |
|
93 assumes "s \<in> lang r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
|
94 using assms |
|
95 apply(induct r arbitrary: s) |
|
96 apply(auto intro: Prf.intros) |
|
97 using Prf.intros(2) flat.simps(3) apply blast |
|
98 using Prf.intros(3) flat.simps(4) apply blast |
|
99 apply (metis Prf.intros(1) concE flat.simps(5)) |
|
100 apply(subgoal_tac "\<exists>vs::('a val) list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
|
101 apply(auto)[1] |
|
102 apply(rule_tac x="Stars vs" in exI) |
|
103 apply(simp) |
|
104 apply (simp add: Prf_Stars) |
|
105 apply(drule Star_string) |
|
106 apply(auto) |
|
107 apply(rule Star_val) |
|
108 apply(auto) |
|
109 done |
|
110 |
|
111 lemma L_flat_Prf: |
|
112 "lang r = {flat v | v. \<turnstile> v : r}" |
|
113 using L_flat_Prf1 L_flat_Prf2 by blast |
|
114 |
|
115 |
|
116 section {* Sulzmann and Lu functions *} |
|
117 |
|
118 fun |
|
119 mkeps :: "'a rexp \<Rightarrow> 'a val" |
|
120 where |
|
121 "mkeps(One) = Void" |
|
122 | "mkeps(Times r1 r2) = Seq (mkeps r1) (mkeps r2)" |
|
123 | "mkeps(Plus r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
|
124 | "mkeps(Star r) = Stars []" |
|
125 |
|
126 fun injval :: "'a rexp \<Rightarrow> 'a \<Rightarrow> 'a val \<Rightarrow> 'a val" |
|
127 where |
|
128 "injval (Atom d) c Void = Atm d" |
|
129 | "injval (Plus r1 r2) c (Left v1) = Left(injval r1 c v1)" |
|
130 | "injval (Plus r1 r2) c (Right v2) = Right(injval r2 c v2)" |
|
131 | "injval (Times r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
|
132 | "injval (Times r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
|
133 | "injval (Times r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
|
134 | "injval (Star r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
135 |
|
136 |
|
137 section {* Mkeps, injval *} |
|
138 |
|
139 lemma mkeps_nullable: |
|
140 assumes "nullable r" |
|
141 shows "\<turnstile> mkeps r : r" |
|
142 using assms |
|
143 by (induct r) |
|
144 (auto intro: Prf.intros) |
|
145 |
|
146 lemma mkeps_flat: |
|
147 assumes "nullable r" |
|
148 shows "flat (mkeps r) = []" |
|
149 using assms |
|
150 by (induct r) (auto) |
|
151 |
|
152 |
|
153 lemma Prf_injval: |
|
154 assumes "\<turnstile> v : deriv c r" |
|
155 shows "\<turnstile> (injval r c v) : r" |
|
156 using assms |
|
157 apply(induct r arbitrary: c v rule: rexp.induct) |
|
158 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
|
159 (* Star *) |
|
160 apply(rotate_tac 2) |
|
161 apply(erule Prf.cases) |
|
162 apply(simp_all)[7] |
|
163 apply(auto) |
|
164 apply (metis Prf.intros(6) Prf.intros(7)) |
|
165 by (metis Prf.intros(7)) |
|
166 |
|
167 lemma Prf_injval_flat: |
|
168 assumes "\<turnstile> v : deriv c r" |
|
169 shows "flat (injval r c v) = c # (flat v)" |
|
170 using assms |
|
171 apply(induct r arbitrary: v c) |
|
172 apply(auto elim!: Prf_elims split: if_splits) |
|
173 apply(metis mkeps_flat) |
|
174 apply(rotate_tac 2) |
|
175 apply(erule Prf.cases) |
|
176 apply(simp_all)[7] |
|
177 done |
|
178 |
|
179 (* HERE *) |
|
180 |
|
181 section {* Our Alternative Posix definition *} |
|
182 |
|
183 inductive |
|
184 Posix :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
185 where |
|
186 Posix_One: "[] \<in> One \<rightarrow> Void" |
|
187 | Posix_Atom: "[c] \<in> (Atom c) \<rightarrow> (Atm c)" |
|
188 | Posix_Plus1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (Plus r1 r2) \<rightarrow> (Left v)" |
|
189 | Posix_Plus2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> lang r1\<rbrakk> \<Longrightarrow> s \<in> (Plus r1 r2) \<rightarrow> (Right v)" |
|
190 | Posix_Times: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
191 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)\<rbrakk> \<Longrightarrow> |
|
192 (s1 @ s2) \<in> (Times r1 r2) \<rightarrow> (Seq v1 v2)" |
|
193 | Posix_Star1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> Star r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
194 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> lang r \<and> s\<^sub>4 \<in> lang (Star r))\<rbrakk> |
|
195 \<Longrightarrow> (s1 @ s2) \<in> Star r \<rightarrow> Stars (v # vs)" |
|
196 | Posix_Star2: "[] \<in> Star r \<rightarrow> Stars []" |
|
197 |
|
198 inductive_cases Posix_elims: |
|
199 "s \<in> Zero \<rightarrow> v" |
|
200 "s \<in> One \<rightarrow> v" |
|
201 "s \<in> Atom c \<rightarrow> v" |
|
202 "s \<in> Plus r1 r2 \<rightarrow> v" |
|
203 "s \<in> Times r1 r2 \<rightarrow> v" |
|
204 "s \<in> Star r \<rightarrow> v" |
|
205 |
|
206 lemma Posix1: |
|
207 assumes "s \<in> r \<rightarrow> v" |
|
208 shows "s \<in> lang r" "flat v = s" |
|
209 using assms |
|
210 by (induct s r v rule: Posix.induct) (auto) |
|
211 |
|
212 |
|
213 lemma Posix1a: |
|
214 assumes "s \<in> r \<rightarrow> v" |
|
215 shows "\<turnstile> v : r" |
|
216 using assms |
|
217 by (induct s r v rule: Posix.induct)(auto intro: Prf.intros) |
|
218 |
|
219 |
|
220 lemma Posix_mkeps: |
|
221 assumes "nullable r" |
|
222 shows "[] \<in> r \<rightarrow> mkeps r" |
|
223 using assms |
|
224 apply(induct r) |
|
225 apply(auto intro: Posix.intros simp add: nullable_iff) |
|
226 apply(subst append.simps(1)[symmetric]) |
|
227 apply(rule Posix.intros) |
|
228 apply(auto) |
|
229 done |
|
230 |
|
231 |
|
232 lemma Posix_determ: |
|
233 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
234 shows "v1 = v2" |
|
235 using assms |
|
236 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
237 case (Posix_One v2) |
|
238 have "[] \<in> One \<rightarrow> v2" by fact |
|
239 then show "Void = v2" by cases auto |
|
240 next |
|
241 case (Posix_Atom c v2) |
|
242 have "[c] \<in> Atom c \<rightarrow> v2" by fact |
|
243 then show "Atm c = v2" by cases auto |
|
244 next |
|
245 case (Posix_Plus1 s r1 v r2 v2) |
|
246 have "s \<in> Plus r1 r2 \<rightarrow> v2" by fact |
|
247 moreover |
|
248 have "s \<in> r1 \<rightarrow> v" by fact |
|
249 then have "s \<in> lang r1" by (simp add: Posix1) |
|
250 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
251 moreover |
|
252 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
253 ultimately have "v = v'" by simp |
|
254 then show "Left v = v2" using eq by simp |
|
255 next |
|
256 case (Posix_Plus2 s r2 v r1 v2) |
|
257 have "s \<in> Plus r1 r2 \<rightarrow> v2" by fact |
|
258 moreover |
|
259 have "s \<notin> lang r1" by fact |
|
260 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
261 by cases (auto simp add: Posix1) |
|
262 moreover |
|
263 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
264 ultimately have "v = v'" by simp |
|
265 then show "Right v = v2" using eq by simp |
|
266 next |
|
267 case (Posix_Times s1 r1 v1 s2 r2 v2 v') |
|
268 have "(s1 @ s2) \<in> Times r1 r2 \<rightarrow> v'" |
|
269 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
270 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" by fact+ |
|
271 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
272 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
273 using Posix1(1) by fastforce+ |
|
274 moreover |
|
275 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
276 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
277 ultimately show "Seq v1 v2 = v'" by simp |
|
278 next |
|
279 case (Posix_Star1 s1 r v s2 vs v2) |
|
280 have "(s1 @ s2) \<in> Star r \<rightarrow> v2" |
|
281 "s1 \<in> r \<rightarrow> v" "s2 \<in> Star r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
282 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (Star r))" by fact+ |
|
283 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (Star r) \<rightarrow> (Stars vs')" |
|
284 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
285 using Posix1(1) apply fastforce |
|
286 apply (metis Posix1(1) Posix_Star1.hyps(6) append_Nil append_Nil2) |
|
287 using Posix1(2) by blast |
|
288 moreover |
|
289 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
290 "\<And>v2. s2 \<in> Star r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
291 ultimately show "Stars (v # vs) = v2" by auto |
|
292 next |
|
293 case (Posix_Star2 r v2) |
|
294 have "[] \<in> Star r \<rightarrow> v2" by fact |
|
295 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
296 qed |
|
297 |
|
298 |
|
299 lemma Posix_injval: |
|
300 assumes "s \<in> (deriv c r) \<rightarrow> v" |
|
301 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
|
302 using assms |
|
303 proof(induct r arbitrary: s v rule: rexp.induct) |
|
304 case Zero |
|
305 have "s \<in> deriv c Zero \<rightarrow> v" by fact |
|
306 then have "s \<in> Zero \<rightarrow> v" by simp |
|
307 then have "False" by cases |
|
308 then show "(c # s) \<in> Zero \<rightarrow> (injval Zero c v)" by simp |
|
309 next |
|
310 case One |
|
311 have "s \<in> deriv c One \<rightarrow> v" by fact |
|
312 then have "s \<in> Zero \<rightarrow> v" by simp |
|
313 then have "False" by cases |
|
314 then show "(c # s) \<in> One \<rightarrow> (injval One c v)" by simp |
|
315 next |
|
316 case (Atom d) |
|
317 consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast |
|
318 then show "(c # s) \<in> (Atom d) \<rightarrow> (injval (Atom d) c v)" |
|
319 proof (cases) |
|
320 case eq |
|
321 have "s \<in> deriv c (Atom d) \<rightarrow> v" by fact |
|
322 then have "s \<in> One \<rightarrow> v" using eq by simp |
|
323 then have eqs: "s = [] \<and> v = Void" by cases simp |
|
324 show "(c # s) \<in> Atom d \<rightarrow> injval (Atom d) c v" using eq eqs |
|
325 by (auto intro: Posix.intros) |
|
326 next |
|
327 case ineq |
|
328 have "s \<in> deriv c (Atom d) \<rightarrow> v" by fact |
|
329 then have "s \<in> Zero \<rightarrow> v" using ineq by simp |
|
330 then have "False" by cases |
|
331 then show "(c # s) \<in> Atom d \<rightarrow> injval (Atom d) c v" by simp |
|
332 qed |
|
333 next |
|
334 case (Plus r1 r2) |
|
335 have IH1: "\<And>s v. s \<in> deriv c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact |
|
336 have IH2: "\<And>s v. s \<in> deriv c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact |
|
337 have "s \<in> deriv c (Plus r1 r2) \<rightarrow> v" by fact |
|
338 then have "s \<in> Plus (deriv c r1) (deriv c r2) \<rightarrow> v" by simp |
|
339 then consider (left) v' where "v = Left v'" "s \<in> deriv c r1 \<rightarrow> v'" |
|
340 | (right) v' where "v = Right v'" "s \<notin> lang (deriv c r1)" "s \<in> deriv c r2 \<rightarrow> v'" |
|
341 by cases auto |
|
342 then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" |
|
343 proof (cases) |
|
344 case left |
|
345 have "s \<in> deriv c r1 \<rightarrow> v'" by fact |
|
346 then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp |
|
347 then have "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c (Left v')" by (auto intro: Posix.intros) |
|
348 then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" using left by simp |
|
349 next |
|
350 case right |
|
351 have "s \<notin> lang (deriv c r1)" by fact |
|
352 then have "c # s \<notin> lang r1" by (simp add: lang_deriv Deriv_def) |
|
353 moreover |
|
354 have "s \<in> deriv c r2 \<rightarrow> v'" by fact |
|
355 then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp |
|
356 ultimately have "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c (Right v')" |
|
357 by (auto intro: Posix.intros) |
|
358 then show "(c # s) \<in> Plus r1 r2 \<rightarrow> injval (Plus r1 r2) c v" using right by simp |
|
359 qed |
|
360 next |
|
361 case (Times r1 r2) |
|
362 have IH1: "\<And>s v. s \<in> deriv c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact |
|
363 have IH2: "\<And>s v. s \<in> deriv c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact |
|
364 have "s \<in> deriv c (Times r1 r2) \<rightarrow> v" by fact |
|
365 then consider |
|
366 (left_nullable) v1 v2 s1 s2 where |
|
367 "v = Left (Seq v1 v2)" "s = s1 @ s2" |
|
368 "s1 \<in> deriv c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1" |
|
369 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" |
|
370 | (right_nullable) v1 s1 s2 where |
|
371 "v = Right v1" "s = s1 @ s2" |
|
372 "s \<in> deriv c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> lang (Times (deriv c r1) r2)" |
|
373 | (not_nullable) v1 v2 s1 s2 where |
|
374 "v = Seq v1 v2" "s = s1 @ s2" |
|
375 "s1 \<in> deriv c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" |
|
376 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" |
|
377 by (force split: if_splits elim!: Posix_elims simp add: lang_deriv Deriv_def) |
|
378 then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" |
|
379 proof (cases) |
|
380 case left_nullable |
|
381 have "s1 \<in> deriv c r1 \<rightarrow> v1" by fact |
|
382 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
|
383 moreover |
|
384 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" by fact |
|
385 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" |
|
386 by (simp add: lang_deriv Deriv_def) |
|
387 ultimately have "((c # s1) @ s2) \<in> Times r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros) |
|
388 then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using left_nullable by simp |
|
389 next |
|
390 case right_nullable |
|
391 have "nullable r1" by fact |
|
392 then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps) |
|
393 moreover |
|
394 have "s \<in> deriv c r2 \<rightarrow> v1" by fact |
|
395 then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp |
|
396 moreover |
|
397 have "s1 @ s2 \<notin> lang (Times (deriv c r1) r2)" by fact |
|
398 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" |
|
399 using right_nullable |
|
400 apply (auto simp add: lang_deriv Deriv_def append_eq_Cons_conv) |
|
401 by (metis concI mem_Collect_eq) |
|
402 ultimately have "([] @ (c # s)) \<in> Times r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)" |
|
403 by(rule Posix.intros) |
|
404 then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using right_nullable by simp |
|
405 next |
|
406 case not_nullable |
|
407 have "s1 \<in> deriv c r1 \<rightarrow> v1" by fact |
|
408 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
|
409 moreover |
|
410 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r1) \<and> s\<^sub>4 \<in> lang r2)" by fact |
|
411 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r1 \<and> s\<^sub>4 \<in> lang r2)" by (simp add: lang_deriv Deriv_def) |
|
412 ultimately have "((c # s1) @ s2) \<in> Times r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable |
|
413 by (rule_tac Posix.intros) (simp_all) |
|
414 then show "(c # s) \<in> Times r1 r2 \<rightarrow> injval (Times r1 r2) c v" using not_nullable by simp |
|
415 qed |
|
416 next |
|
417 case (Star r) |
|
418 have IH: "\<And>s v. s \<in> deriv c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
419 have "s \<in> deriv c (Star r) \<rightarrow> v" by fact |
|
420 then consider |
|
421 (cons) v1 vs s1 s2 where |
|
422 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
|
423 "s1 \<in> deriv c r \<rightarrow> v1" "s2 \<in> (Star r) \<rightarrow> (Stars vs)" |
|
424 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))" |
|
425 apply(auto elim!: Posix_elims(1-5) simp add: lang_deriv Deriv_def intro: Posix.intros) |
|
426 apply(rotate_tac 3) |
|
427 apply(erule_tac Posix_elims(6)) |
|
428 apply (simp add: Posix.intros(6)) |
|
429 using Posix.intros(7) by blast |
|
430 then show "(c # s) \<in> Star r \<rightarrow> injval (Star r) c v" |
|
431 proof (cases) |
|
432 case cons |
|
433 have "s1 \<in> deriv c r \<rightarrow> v1" by fact |
|
434 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
|
435 moreover |
|
436 have "s2 \<in> Star r \<rightarrow> Stars vs" by fact |
|
437 moreover |
|
438 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
|
439 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
|
440 then have "flat (injval r c v1) \<noteq> []" by simp |
|
441 moreover |
|
442 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> lang (deriv c r) \<and> s\<^sub>4 \<in> lang (Star r))" by fact |
|
443 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> lang r \<and> s\<^sub>4 \<in> lang (Star r))" |
|
444 by (simp add: lang_deriv Deriv_def) |
|
445 ultimately |
|
446 have "((c # s1) @ s2) \<in> Star r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros) |
|
447 then show "(c # s) \<in> Star r \<rightarrow> injval (Star r) c v" using cons by(simp) |
|
448 qed |
|
449 qed |
|
450 |
|
451 |
|
452 section {* The Lexer by Sulzmann and Lu *} |
|
453 |
|
454 fun |
|
455 lexer :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> ('a val) option" |
|
456 where |
|
457 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
458 | "lexer r (c#s) = (case (lexer (deriv c r) s) of |
|
459 None \<Rightarrow> None |
|
460 | Some(v) \<Rightarrow> Some(injval r c v))" |
|
461 |
|
462 |
|
463 lemma lexer_correct_None: |
|
464 shows "s \<notin> lang r \<longleftrightarrow> lexer r s = None" |
|
465 using assms |
|
466 apply(induct s arbitrary: r) |
|
467 apply(simp add: nullable_iff) |
|
468 apply(drule_tac x="deriv a r" in meta_spec) |
|
469 apply(auto simp add: lang_deriv Deriv_def) |
|
470 done |
|
471 |
|
472 lemma lexer_correct_Some: |
|
473 shows "s \<in> lang r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
|
474 using assms |
|
475 apply(induct s arbitrary: r) |
|
476 apply(auto simp add: Posix_mkeps nullable_iff)[1] |
|
477 apply(drule_tac x="deriv a r" in meta_spec) |
|
478 apply(simp add: lang_deriv Deriv_def) |
|
479 apply(rule iffI) |
|
480 apply(auto intro: Posix_injval simp add: Posix1(1)) |
|
481 done |
|
482 |
|
483 lemma lexer_correctness: |
|
484 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
|
485 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
|
486 apply(auto) |
|
487 using lexer_correct_None lexer_correct_Some apply fastforce |
|
488 using Posix1(1) Posix_determ lexer_correct_Some apply blast |
|
489 using Posix1(1) lexer_correct_None apply blast |
|
490 using lexer_correct_None lexer_correct_Some by blast |
|
491 |
|
492 |
|
493 end |