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