1 |
|
2 theory ReStar |
|
3 imports "Main" |
|
4 begin |
|
5 |
|
6 |
|
7 section {* Sequential Composition of Languages *} |
|
8 |
|
9 definition |
|
10 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
|
11 where |
|
12 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
|
13 |
|
14 text {* Two Simple Properties about Sequential Composition *} |
|
15 |
|
16 lemma seq_empty [simp]: |
|
17 shows "A ;; {[]} = A" |
|
18 and "{[]} ;; A = A" |
|
19 by (simp_all add: Sequ_def) |
|
20 |
|
21 lemma seq_null [simp]: |
|
22 shows "A ;; {} = {}" |
|
23 and "{} ;; A = {}" |
|
24 by (simp_all add: Sequ_def) |
|
25 |
|
26 |
|
27 section {* Semantic Derivative (Left Quotient) of Languages *} |
|
28 |
|
29 definition |
|
30 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
31 where |
|
32 "Der c A \<equiv> {s. c # s \<in> A}" |
|
33 |
|
34 lemma Der_null [simp]: |
|
35 shows "Der c {} = {}" |
|
36 unfolding Der_def |
|
37 by auto |
|
38 |
|
39 lemma Der_empty [simp]: |
|
40 shows "Der c {[]} = {}" |
|
41 unfolding Der_def |
|
42 by auto |
|
43 |
|
44 lemma Der_char [simp]: |
|
45 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
46 unfolding Der_def |
|
47 by auto |
|
48 |
|
49 lemma Der_union [simp]: |
|
50 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
51 unfolding Der_def |
|
52 by auto |
|
53 |
|
54 lemma Der_Sequ [simp]: |
|
55 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
56 unfolding Der_def Sequ_def |
|
57 by (auto simp add: Cons_eq_append_conv) |
|
58 |
|
59 |
|
60 section {* Kleene Star for Languages *} |
|
61 |
|
62 inductive_set |
|
63 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
|
64 for A :: "string set" |
|
65 where |
|
66 start[intro]: "[] \<in> A\<star>" |
|
67 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
|
68 |
|
69 lemma star_cases: |
|
70 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
71 unfolding Sequ_def |
|
72 by (auto) (metis Star.simps) |
|
73 |
|
74 lemma star_decomp: |
|
75 assumes a: "c # x \<in> A\<star>" |
|
76 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
|
77 using a |
|
78 by (induct x\<equiv>"c # x" rule: Star.induct) |
|
79 (auto simp add: append_eq_Cons_conv) |
|
80 |
|
81 lemma Der_star [simp]: |
|
82 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
83 proof - |
|
84 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
85 by (simp only: star_cases[symmetric]) |
|
86 also have "... = Der c (A ;; A\<star>)" |
|
87 by (simp only: Der_union Der_empty) (simp) |
|
88 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
89 by simp |
|
90 also have "... = (Der c A) ;; A\<star>" |
|
91 unfolding Sequ_def Der_def |
|
92 by (auto dest: star_decomp) |
|
93 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
94 qed |
|
95 |
|
96 |
|
97 section {* Regular Expressions *} |
|
98 |
|
99 datatype rexp = |
|
100 ZERO |
|
101 | ONE |
|
102 | CHAR char |
|
103 | SEQ rexp rexp |
|
104 | ALT rexp rexp |
|
105 | STAR rexp |
|
106 |
|
107 section {* Semantics of Regular Expressions *} |
|
108 |
|
109 fun |
|
110 L :: "rexp \<Rightarrow> string set" |
|
111 where |
|
112 "L (ZERO) = {}" |
|
113 | "L (ONE) = {[]}" |
|
114 | "L (CHAR c) = {[c]}" |
|
115 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
|
116 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
117 | "L (STAR r) = (L r)\<star>" |
|
118 |
|
119 |
|
120 section {* Nullable, Derivatives *} |
|
121 |
|
122 fun |
|
123 nullable :: "rexp \<Rightarrow> bool" |
|
124 where |
|
125 "nullable (ZERO) = False" |
|
126 | "nullable (ONE) = True" |
|
127 | "nullable (CHAR c) = False" |
|
128 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
|
129 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
|
130 | "nullable (STAR r) = True" |
|
131 |
|
132 |
|
133 fun |
|
134 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
|
135 where |
|
136 "der c (ZERO) = ZERO" |
|
137 | "der c (ONE) = ZERO" |
|
138 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
|
139 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
140 | "der c (SEQ r1 r2) = |
|
141 (if nullable r1 |
|
142 then ALT (SEQ (der c r1) r2) (der c r2) |
|
143 else SEQ (der c r1) r2)" |
|
144 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
|
145 |
|
146 fun |
|
147 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
|
148 where |
|
149 "ders [] r = r" |
|
150 | "ders (c # s) r = ders s (der c r)" |
|
151 |
|
152 |
|
153 lemma nullable_correctness: |
|
154 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
155 by (induct r) (auto simp add: Sequ_def) |
|
156 |
|
157 |
|
158 lemma der_correctness: |
|
159 shows "L (der c r) = Der c (L r)" |
|
160 by (induct r) (simp_all add: nullable_correctness) |
|
161 |
|
162 |
|
163 section {* Values *} |
|
164 |
|
165 datatype val = |
|
166 Void |
|
167 | Char char |
|
168 | Seq val val |
|
169 | Right val |
|
170 | Left val |
|
171 | Stars "val list" |
|
172 |
|
173 |
|
174 section {* The string behind a value *} |
|
175 |
|
176 fun |
|
177 flat :: "val \<Rightarrow> string" |
|
178 where |
|
179 "flat (Void) = []" |
|
180 | "flat (Char c) = [c]" |
|
181 | "flat (Left v) = flat v" |
|
182 | "flat (Right v) = flat v" |
|
183 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
|
184 | "flat (Stars []) = []" |
|
185 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
|
186 |
|
187 lemma flat_Stars [simp]: |
|
188 "flat (Stars vs) = concat (map flat vs)" |
|
189 by (induct vs) (auto) |
|
190 |
|
191 |
|
192 section {* Relation between values and regular expressions *} |
|
193 |
|
194 inductive |
|
195 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
196 where |
|
197 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
|
198 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
|
199 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" |
|
200 | "\<turnstile> Void : ONE" |
|
201 | "\<turnstile> Char c : CHAR c" |
|
202 | "\<turnstile> Stars [] : STAR r" |
|
203 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r" |
|
204 |
|
205 inductive_cases Prf_elims: |
|
206 "\<turnstile> v : ZERO" |
|
207 "\<turnstile> v : SEQ r1 r2" |
|
208 "\<turnstile> v : ALT r1 r2" |
|
209 "\<turnstile> v : ONE" |
|
210 "\<turnstile> v : CHAR c" |
|
211 (* "\<turnstile> vs : STAR r"*) |
|
212 |
|
213 lemma Prf_flat_L: |
|
214 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
|
215 using assms |
|
216 by(induct v r rule: Prf.induct) |
|
217 (auto simp add: Sequ_def) |
|
218 |
|
219 lemma Prf_Stars: |
|
220 assumes "\<forall>v \<in> set vs. \<turnstile> v : r" |
|
221 shows "\<turnstile> Stars vs : STAR r" |
|
222 using assms |
|
223 apply(induct vs) |
|
224 apply (metis Prf.intros(6)) |
|
225 by (metis Prf.intros(7) insert_iff set_simps(2)) |
|
226 |
|
227 lemma Star_string: |
|
228 assumes "s \<in> A\<star>" |
|
229 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
|
230 using assms |
|
231 apply(induct rule: Star.induct) |
|
232 apply(auto) |
|
233 apply(rule_tac x="[]" in exI) |
|
234 apply(simp) |
|
235 apply(rule_tac x="s1#ss" in exI) |
|
236 apply(simp) |
|
237 done |
|
238 |
|
239 |
|
240 lemma Star_val: |
|
241 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
242 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
243 using assms |
|
244 apply(induct ss) |
|
245 apply(auto) |
|
246 apply (metis empty_iff list.set(1)) |
|
247 by (metis concat.simps(2) list.simps(9) set_ConsD) |
|
248 |
|
249 lemma L_flat_Prf: |
|
250 "L(r) = {flat v | v. \<turnstile> v : r}" |
|
251 apply(induct r) |
|
252 apply(auto dest: Prf_flat_L simp add: Sequ_def) |
|
253 apply (metis Prf.intros(4) flat.simps(1)) |
|
254 apply (metis Prf.intros(5) flat.simps(2)) |
|
255 apply (metis Prf.intros(1) flat.simps(5)) |
|
256 apply (metis Prf.intros(2) flat.simps(3)) |
|
257 apply (metis Prf.intros(3) flat.simps(4)) |
|
258 apply(auto elim!: Prf_elims) |
|
259 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
|
260 apply(auto)[1] |
|
261 apply(rule_tac x="Stars vs" in exI) |
|
262 apply(simp) |
|
263 apply(rule Prf_Stars) |
|
264 apply(simp) |
|
265 apply(drule Star_string) |
|
266 apply(auto) |
|
267 apply(rule Star_val) |
|
268 apply(simp) |
|
269 done |
|
270 |
|
271 |
|
272 section {* Sulzmann and Lu functions *} |
|
273 |
|
274 fun |
|
275 mkeps :: "rexp \<Rightarrow> val" |
|
276 where |
|
277 "mkeps(ONE) = Void" |
|
278 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
|
279 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
|
280 | "mkeps(STAR r) = Stars []" |
|
281 |
|
282 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
|
283 where |
|
284 "injval (CHAR d) c Void = Char d" |
|
285 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
|
286 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
|
287 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
|
288 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
|
289 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
|
290 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
|
291 |
|
292 |
|
293 section {* Mkeps, injval *} |
|
294 |
|
295 lemma mkeps_nullable: |
|
296 assumes "nullable(r)" |
|
297 shows "\<turnstile> mkeps r : r" |
|
298 using assms |
|
299 by (induct rule: nullable.induct) |
|
300 (auto intro: Prf.intros) |
|
301 |
|
302 lemma mkeps_flat: |
|
303 assumes "nullable(r)" |
|
304 shows "flat (mkeps r) = []" |
|
305 using assms |
|
306 by (induct rule: nullable.induct) (auto) |
|
307 |
|
308 |
|
309 lemma Prf_injval: |
|
310 assumes "\<turnstile> v : der c r" |
|
311 shows "\<turnstile> (injval r c v) : r" |
|
312 using assms |
|
313 apply(induct r arbitrary: c v rule: rexp.induct) |
|
314 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
|
315 (* STAR *) |
|
316 apply(rotate_tac 2) |
|
317 apply(erule Prf.cases) |
|
318 apply(simp_all)[7] |
|
319 apply(auto) |
|
320 apply (metis Prf.intros(6) Prf.intros(7)) |
|
321 by (metis Prf.intros(7)) |
|
322 |
|
323 lemma Prf_injval_flat: |
|
324 assumes "\<turnstile> v : der c r" |
|
325 shows "flat (injval r c v) = c # (flat v)" |
|
326 using assms |
|
327 apply(induct arbitrary: v rule: der.induct) |
|
328 apply(auto elim!: Prf_elims split: if_splits) |
|
329 apply(metis mkeps_flat) |
|
330 apply(rotate_tac 2) |
|
331 apply(erule Prf.cases) |
|
332 apply(simp_all)[7] |
|
333 done |
|
334 |
|
335 |
|
336 |
|
337 section {* Our Alternative Posix definition *} |
|
338 |
|
339 inductive |
|
340 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
341 where |
|
342 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
|
343 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
|
344 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
|
345 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
|
346 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
347 \<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 r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
|
348 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
349 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
350 \<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 r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
|
351 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
352 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
353 |
|
354 inductive_cases Posix_elims: |
|
355 "s \<in> ZERO \<rightarrow> v" |
|
356 "s \<in> ONE \<rightarrow> v" |
|
357 "s \<in> CHAR c \<rightarrow> v" |
|
358 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
359 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
360 "s \<in> STAR r \<rightarrow> v" |
|
361 |
|
362 lemma Posix1: |
|
363 assumes "s \<in> r \<rightarrow> v" |
|
364 shows "s \<in> L r" "flat v = s" |
|
365 using assms |
|
366 by (induct s r v rule: Posix.induct) |
|
367 (auto simp add: Sequ_def) |
|
368 |
|
369 |
|
370 lemma Posix1a: |
|
371 assumes "s \<in> r \<rightarrow> v" |
|
372 shows "\<turnstile> v : r" |
|
373 using assms |
|
374 apply(induct s r v rule: Posix.induct) |
|
375 apply(auto intro: Prf.intros) |
|
376 done |
|
377 |
|
378 lemma Posix_mkeps: |
|
379 assumes "nullable r" |
|
380 shows "[] \<in> r \<rightarrow> mkeps r" |
|
381 using assms |
|
382 apply(induct r) |
|
383 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
|
384 apply(subst append.simps(1)[symmetric]) |
|
385 apply(rule Posix.intros) |
|
386 apply(auto) |
|
387 done |
|
388 |
|
389 |
|
390 lemma Posix_determ: |
|
391 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
392 shows "v1 = v2" |
|
393 using assms |
|
394 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
395 case (Posix_ONE v2) |
|
396 have "[] \<in> ONE \<rightarrow> v2" by fact |
|
397 then show "Void = v2" by cases auto |
|
398 next |
|
399 case (Posix_CHAR c v2) |
|
400 have "[c] \<in> CHAR c \<rightarrow> v2" by fact |
|
401 then show "Char c = v2" by cases auto |
|
402 next |
|
403 case (Posix_ALT1 s r1 v r2 v2) |
|
404 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
405 moreover |
|
406 have "s \<in> r1 \<rightarrow> v" by fact |
|
407 then have "s \<in> L r1" by (simp add: Posix1) |
|
408 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
409 moreover |
|
410 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
411 ultimately have "v = v'" by simp |
|
412 then show "Left v = v2" using eq by simp |
|
413 next |
|
414 case (Posix_ALT2 s r2 v r1 v2) |
|
415 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
416 moreover |
|
417 have "s \<notin> L r1" by fact |
|
418 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
419 by cases (auto simp add: Posix1) |
|
420 moreover |
|
421 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
422 ultimately have "v = v'" by simp |
|
423 then show "Right v = v2" using eq by simp |
|
424 next |
|
425 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
|
426 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
|
427 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
428 "\<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 r1 \<and> s\<^sub>4 \<in> L r2)" by fact+ |
|
429 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
430 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
431 using Posix1(1) by fastforce+ |
|
432 moreover |
|
433 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
434 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
435 ultimately show "Seq v1 v2 = v'" by simp |
|
436 next |
|
437 case (Posix_STAR1 s1 r v s2 vs v2) |
|
438 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
|
439 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
440 "\<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 r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+ |
|
441 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
442 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
443 using Posix1(1) apply fastforce |
|
444 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
|
445 using Posix1(2) by blast |
|
446 moreover |
|
447 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
448 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
449 ultimately show "Stars (v # vs) = v2" by auto |
|
450 next |
|
451 case (Posix_STAR2 r v2) |
|
452 have "[] \<in> STAR r \<rightarrow> v2" by fact |
|
453 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
454 qed |
|
455 |
|
456 |
|
457 lemma Posix_injval: |
|
458 assumes "s \<in> (der c r) \<rightarrow> v" |
|
459 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
|
460 using assms |
|
461 proof(induct r arbitrary: s v rule: rexp.induct) |
|
462 case ZERO |
|
463 have "s \<in> der c ZERO \<rightarrow> v" by fact |
|
464 then have "s \<in> ZERO \<rightarrow> v" by simp |
|
465 then have "False" by cases |
|
466 then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp |
|
467 next |
|
468 case ONE |
|
469 have "s \<in> der c ONE \<rightarrow> v" by fact |
|
470 then have "s \<in> ZERO \<rightarrow> v" by simp |
|
471 then have "False" by cases |
|
472 then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp |
|
473 next |
|
474 case (CHAR d) |
|
475 consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast |
|
476 then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)" |
|
477 proof (cases) |
|
478 case eq |
|
479 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
|
480 then have "s \<in> ONE \<rightarrow> v" using eq by simp |
|
481 then have eqs: "s = [] \<and> v = Void" by cases simp |
|
482 show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs |
|
483 by (auto intro: Posix.intros) |
|
484 next |
|
485 case ineq |
|
486 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
|
487 then have "s \<in> ZERO \<rightarrow> v" using ineq by simp |
|
488 then have "False" by cases |
|
489 then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp |
|
490 qed |
|
491 next |
|
492 case (ALT r1 r2) |
|
493 have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact |
|
494 have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact |
|
495 have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact |
|
496 then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp |
|
497 then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'" |
|
498 | (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'" |
|
499 by cases auto |
|
500 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" |
|
501 proof (cases) |
|
502 case left |
|
503 have "s \<in> der c r1 \<rightarrow> v'" by fact |
|
504 then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp |
|
505 then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros) |
|
506 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp |
|
507 next |
|
508 case right |
|
509 have "s \<notin> L (der c r1)" by fact |
|
510 then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def) |
|
511 moreover |
|
512 have "s \<in> der c r2 \<rightarrow> v'" by fact |
|
513 then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp |
|
514 ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')" |
|
515 by (auto intro: Posix.intros) |
|
516 then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp |
|
517 qed |
|
518 next |
|
519 case (SEQ r1 r2) |
|
520 have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact |
|
521 have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact |
|
522 have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact |
|
523 then consider |
|
524 (left_nullable) v1 v2 s1 s2 where |
|
525 "v = Left (Seq v1 v2)" "s = s1 @ s2" |
|
526 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1" |
|
527 "\<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 r1) \<and> s\<^sub>4 \<in> L r2)" |
|
528 | (right_nullable) v1 s1 s2 where |
|
529 "v = Right v1" "s = s1 @ s2" |
|
530 "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" |
|
531 | (not_nullable) v1 v2 s1 s2 where |
|
532 "v = Seq v1 v2" "s = s1 @ s2" |
|
533 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" |
|
534 "\<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 r1) \<and> s\<^sub>4 \<in> L r2)" |
|
535 by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def) |
|
536 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" |
|
537 proof (cases) |
|
538 case left_nullable |
|
539 have "s1 \<in> der c r1 \<rightarrow> v1" by fact |
|
540 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
|
541 moreover |
|
542 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 r1) \<and> s\<^sub>4 \<in> L r2)" by fact |
|
543 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 r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def) |
|
544 ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros) |
|
545 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp |
|
546 next |
|
547 case right_nullable |
|
548 have "nullable r1" by fact |
|
549 then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps) |
|
550 moreover |
|
551 have "s \<in> der c r2 \<rightarrow> v1" by fact |
|
552 then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp |
|
553 moreover |
|
554 have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact |
|
555 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> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable |
|
556 by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def) |
|
557 ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)" |
|
558 by(rule Posix.intros) |
|
559 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp |
|
560 next |
|
561 case not_nullable |
|
562 have "s1 \<in> der c r1 \<rightarrow> v1" by fact |
|
563 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
|
564 moreover |
|
565 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 r1) \<and> s\<^sub>4 \<in> L r2)" by fact |
|
566 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 r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def) |
|
567 ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable |
|
568 by (rule_tac Posix.intros) (simp_all) |
|
569 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp |
|
570 qed |
|
571 next |
|
572 case (STAR r) |
|
573 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
574 have "s \<in> der c (STAR r) \<rightarrow> v" by fact |
|
575 then consider |
|
576 (cons) v1 vs s1 s2 where |
|
577 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
|
578 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
|
579 "\<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 (STAR r))" |
|
580 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
|
581 apply(rotate_tac 3) |
|
582 apply(erule_tac Posix_elims(6)) |
|
583 apply (simp add: Posix.intros(6)) |
|
584 using Posix.intros(7) by blast |
|
585 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" |
|
586 proof (cases) |
|
587 case cons |
|
588 have "s1 \<in> der c r \<rightarrow> v1" by fact |
|
589 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
|
590 moreover |
|
591 have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact |
|
592 moreover |
|
593 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
|
594 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
|
595 then have "flat (injval r c v1) \<noteq> []" by simp |
|
596 moreover |
|
597 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 (STAR r))" by fact |
|
598 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))" |
|
599 by (simp add: der_correctness Der_def) |
|
600 ultimately |
|
601 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros) |
|
602 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
|
603 qed |
|
604 qed |
|
605 |
|
606 |
|
607 section {* The Lexer by Sulzmann and Lu *} |
|
608 |
|
609 fun |
|
610 lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
611 where |
|
612 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
613 | "lexer r (c#s) = (case (lexer (der c r) s) of |
|
614 None \<Rightarrow> None |
|
615 | Some(v) \<Rightarrow> Some(injval r c v))" |
|
616 |
|
617 |
|
618 lemma lexer_correct_None: |
|
619 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
|
620 using assms |
|
621 apply(induct s arbitrary: r) |
|
622 apply(simp add: nullable_correctness) |
|
623 apply(drule_tac x="der a r" in meta_spec) |
|
624 apply(auto simp add: der_correctness Der_def) |
|
625 done |
|
626 |
|
627 lemma lexer_correct_Some: |
|
628 shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
|
629 using assms |
|
630 apply(induct s arbitrary: r) |
|
631 apply(auto simp add: Posix_mkeps nullable_correctness)[1] |
|
632 apply(drule_tac x="der a r" in meta_spec) |
|
633 apply(simp add: der_correctness Der_def) |
|
634 apply(rule iffI) |
|
635 apply(auto intro: Posix_injval simp add: Posix1(1)) |
|
636 done |
|
637 |
|
638 |
|
639 end |
|