1 |
1 |
2 theory Lexer |
2 theory Lexer |
3 imports PosixSpec |
3 imports PosixSpec |
4 begin |
4 begin |
5 |
5 |
6 section {* The Lexer Functions by Sulzmann and Lu (without simplification) *} |
6 section \<open>The Lexer Functions by Sulzmann and Lu (without simplification)\<close> |
7 |
7 |
8 fun |
8 fun |
9 mkeps :: "rexp \<Rightarrow> val" |
9 mkeps :: "rexp \<Rightarrow> val" |
10 where |
10 where |
11 "mkeps(ONE) = Void" |
11 "mkeps(ONE) = Void" |
12 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
12 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
13 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
13 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
14 | "mkeps(STAR r) = Stars []" |
14 | "mkeps(STAR r) = Stars []" |
|
15 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
15 |
16 |
16 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
17 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
17 where |
18 where |
18 "injval (CH d) c Void = Char d" |
19 "injval (CH d) c Void = Char d" |
19 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
20 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
20 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
21 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
21 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
22 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
22 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
23 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
23 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
24 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
24 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
25 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
26 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
25 |
27 |
26 fun |
28 fun |
27 lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
29 lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
28 where |
30 where |
29 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
31 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
31 None \<Rightarrow> None |
33 None \<Rightarrow> None |
32 | Some(v) \<Rightarrow> Some(injval r c v))" |
34 | Some(v) \<Rightarrow> Some(injval r c v))" |
33 |
35 |
34 |
36 |
35 |
37 |
36 section {* Mkeps, Injval Properties *} |
38 section \<open>Mkeps, Injval Properties\<close> |
|
39 |
|
40 lemma mkeps_flat: |
|
41 assumes "nullable(r)" |
|
42 shows "flat (mkeps r) = []" |
|
43 using assms |
|
44 by (induct rule: mkeps.induct) (auto) |
|
45 |
|
46 lemma Prf_NTimes_empty: |
|
47 assumes "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v = []" |
|
48 and "length vs = n" |
|
49 shows "\<Turnstile> Stars vs : NTIMES r n" |
|
50 using assms |
|
51 by (metis Prf.intros(7) empty_iff eq_Nil_appendI list.set(1)) |
|
52 |
37 |
53 |
38 lemma mkeps_nullable: |
54 lemma mkeps_nullable: |
39 assumes "nullable(r)" |
55 assumes "nullable(r)" |
40 shows "\<Turnstile> mkeps r : r" |
56 shows "\<Turnstile> mkeps r : r" |
41 using assms |
57 using assms |
42 by (induct rule: nullable.induct) |
58 apply (induct rule: mkeps.induct) |
43 (auto intro: Prf.intros) |
59 apply(auto intro: Prf.intros split: if_splits) |
44 |
60 apply (metis Prf.intros(7) append_is_Nil_conv empty_iff list.set(1) list.size(3)) |
45 lemma mkeps_flat: |
61 apply(rule Prf_NTimes_empty) |
46 assumes "nullable(r)" |
62 apply(auto simp add: mkeps_flat) |
47 shows "flat (mkeps r) = []" |
63 done |
48 using assms |
|
49 by (induct rule: nullable.induct) (auto) |
|
50 |
64 |
51 lemma Prf_injval_flat: |
65 lemma Prf_injval_flat: |
52 assumes "\<Turnstile> v : der c r" |
66 assumes "\<Turnstile> v : der c r" |
53 shows "flat (injval r c v) = c # (flat v)" |
67 shows "flat (injval r c v) = c # (flat v)" |
54 using assms |
68 using assms |
60 assumes "\<Turnstile> v : der c r" |
74 assumes "\<Turnstile> v : der c r" |
61 shows "\<Turnstile> (injval r c v) : r" |
75 shows "\<Turnstile> (injval r c v) : r" |
62 using assms |
76 using assms |
63 apply(induct r arbitrary: c v rule: rexp.induct) |
77 apply(induct r arbitrary: c v rule: rexp.induct) |
64 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
78 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
|
79 (* Star *) |
65 apply(simp add: Prf_injval_flat) |
80 apply(simp add: Prf_injval_flat) |
66 done |
81 (* NTimes *) |
67 |
82 apply(case_tac x2) |
68 |
83 apply(simp) |
69 |
84 apply(simp) |
70 text {* |
85 apply(subst append.simps(2)[symmetric]) |
71 Mkeps and injval produce, or preserve, Posix values. |
86 apply(rule Prf.intros) |
72 *} |
87 apply(auto simp add: Prf_injval_flat) |
|
88 done |
|
89 |
|
90 |
|
91 text \<open>Mkeps and injval produce, or preserve, Posix values.\<close> |
|
92 |
73 |
93 |
74 lemma Posix_mkeps: |
94 lemma Posix_mkeps: |
75 assumes "nullable r" |
95 assumes "nullable r" |
76 shows "[] \<in> r \<rightarrow> mkeps r" |
96 shows "[] \<in> r \<rightarrow> mkeps r" |
77 using assms |
97 using assms |
78 apply(induct r rule: nullable.induct) |
98 apply(induct r rule: nullable.induct) |
79 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
99 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
80 apply(subst append.simps(1)[symmetric]) |
100 apply(subst append.simps(1)[symmetric]) |
81 apply(rule Posix.intros) |
101 apply(rule Posix.intros) |
82 apply(auto) |
102 apply(auto) |
83 done |
103 by (simp add: Posix_NTIMES2 pow_empty_iff) |
84 |
104 |
85 lemma Posix_injval: |
105 lemma Posix_injval: |
86 assumes "s \<in> (der c r) \<rightarrow> v" |
106 assumes "s \<in> (der c r) \<rightarrow> v" |
87 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
107 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
88 using assms |
108 using assms |
226 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> L r \<and> s\<^sub>4 \<in> L (STAR r))" |
246 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> L r \<and> s\<^sub>4 \<in> L (STAR r))" |
227 by (simp add: der_correctness Der_def) |
247 by (simp add: der_correctness Der_def) |
228 ultimately |
248 ultimately |
229 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros) |
249 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros) |
230 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
250 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
231 qed |
251 qed |
|
252 next |
|
253 case (NTIMES r n) |
|
254 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
255 have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact |
|
256 then consider |
|
257 (cons) v1 vs s1 s2 where |
|
258 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
|
259 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
|
260 "\<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> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
|
261 |
|
262 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
|
263 apply(erule Posix_elims) |
|
264 apply(simp) |
|
265 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
|
266 apply(clarify) |
|
267 apply(drule_tac x="vss" in meta_spec) |
|
268 apply(drule_tac x="s1" in meta_spec) |
|
269 apply(drule_tac x="s2" in meta_spec) |
|
270 apply(simp add: der_correctness Der_def) |
|
271 apply(erule Posix_elims) |
|
272 apply(auto) |
|
273 done |
|
274 then show "(c # s) \<in> (NTIMES r n) \<rightarrow> injval (NTIMES r n) c v" |
|
275 proof (cases) |
|
276 case cons |
|
277 have "s1 \<in> der c r \<rightarrow> v1" by fact |
|
278 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
|
279 moreover |
|
280 have "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> Stars vs" by fact |
|
281 moreover |
|
282 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
|
283 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
|
284 then have "flat (injval r c v1) \<noteq> []" by simp |
|
285 moreover |
|
286 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> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact |
|
287 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> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
|
288 by (simp add: der_correctness Der_def) |
|
289 ultimately |
|
290 have "((c # s1) @ s2) \<in> NTIMES r n \<rightarrow> Stars (injval r c v1 # vs)" |
|
291 apply (rule_tac Posix.intros) |
|
292 apply(simp_all) |
|
293 apply(case_tac n) |
|
294 apply(simp) |
|
295 using Posix_elims(1) NTIMES.prems apply auto[1] |
|
296 apply(simp) |
|
297 done |
|
298 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
|
299 qed |
|
300 |
232 qed |
301 qed |
233 |
302 |
234 |
303 |
235 section {* Lexer Correctness *} |
304 section \<open>Lexer Correctness\<close> |
236 |
305 |
237 |
306 |
238 lemma lexer_correct_None: |
307 lemma lexer_correct_None: |
239 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
308 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
240 apply(induct s arbitrary: r) |
309 apply(induct s arbitrary: r) |
352 apply(auto) |
421 apply(auto) |
353 apply(erule Prf_elims) |
422 apply(erule Prf_elims) |
354 apply(erule Prf_elims) |
423 apply(erule Prf_elims) |
355 apply(auto) |
424 apply(auto) |
356 apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5)) |
425 apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5)) |
357 by (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5)) |
426 apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5)) |
|
427 by (smt (verit, best) Prf_elims(1) Prf_elims(2) Prf_elims(7) injval.simps(8) list.inject val.simps(5)) |
358 |
428 |
359 |
429 |
360 |
430 |
361 lemma uu: |
431 lemma uu: |
362 assumes "(c # s) \<in> r \<rightarrow> injval r c v" "\<Turnstile> v : (der c r)" |
432 assumes "(c # s) \<in> r \<rightarrow> injval r c v" "\<Turnstile> v : (der c r)" |
373 apply(case_tac "s \<in> der c r \<rightarrow> a") |
443 apply(case_tac "s \<in> der c r \<rightarrow> a") |
374 prefer 2 |
444 prefer 2 |
375 apply (simp add: lexer_correctness(1)) |
445 apply (simp add: lexer_correctness(1)) |
376 apply(subgoal_tac "\<Turnstile> a : (der c r)") |
446 apply(subgoal_tac "\<Turnstile> a : (der c r)") |
377 prefer 2 |
447 prefer 2 |
378 using Posix_Prf apply blast |
448 using Posix1a apply blast |
379 using injval_inj by blast |
449 using injval_inj by blast |
380 |
450 |
381 |
451 |
382 lemma Posix_flex2: |
452 lemma Posix_flex2: |
383 assumes "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r" |
453 assumes "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r" |