51 |
51 |
52 lemma Prf_injval_flat: |
52 lemma Prf_injval_flat: |
53 assumes "\<Turnstile> v : der c r" |
53 assumes "\<Turnstile> v : der c r" |
54 shows "flat (injval r c v) = c # (flat v)" |
54 shows "flat (injval r c v) = c # (flat v)" |
55 using assms |
55 using assms |
56 apply(induct arbitrary: v rule: der.induct) |
56 apply(induct c r arbitrary: v rule: der.induct) |
57 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits) |
57 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits) |
58 done |
58 done |
59 |
59 |
60 lemma Prf_injval: |
60 lemma Prf_injval: |
61 assumes "\<Turnstile> v : der c r" |
61 assumes "\<Turnstile> v : der c r" |
236 section {* Lexer Correctness *} |
236 section {* Lexer Correctness *} |
237 |
237 |
238 |
238 |
239 lemma lexer_correct_None: |
239 lemma lexer_correct_None: |
240 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
240 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
241 apply(induct s arbitrary: r) |
241 apply(induct s arbitrary: r) |
242 apply(simp add: nullable_correctness) |
242 apply(simp) |
243 apply(drule_tac x="der a r" in meta_spec) |
243 apply(simp add: nullable_correctness) |
244 apply(auto simp add: der_correctness Der_def) |
244 apply(simp) |
|
245 apply(drule_tac x="der a r" in meta_spec) |
|
246 apply(auto) |
|
247 apply(auto simp add: der_correctness Der_def) |
245 done |
248 done |
246 |
249 |
247 lemma lexer_correct_Some: |
250 lemma lexer_correct_Some: |
248 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
251 shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)" |
249 apply(induct s arbitrary: r) |
252 apply(induct s arbitrary : r) |
250 apply(auto simp add: Posix_mkeps nullable_correctness)[1] |
253 apply(simp only: lexer.simps) |
251 apply(drule_tac x="der a r" in meta_spec) |
254 apply(simp) |
252 apply(simp add: der_correctness Der_def) |
255 apply(simp add: nullable_correctness Posix_mkeps) |
253 apply(rule iffI) |
256 apply(drule_tac x="der a r" in meta_spec) |
254 apply(auto intro: Posix_injval simp add: Posix1(1)) |
257 apply(simp (no_asm_use) add: der_correctness Der_def del: lexer.simps) |
|
258 apply(simp del: lexer.simps) |
|
259 apply(simp only: lexer.simps) |
|
260 apply(case_tac "lexer (der a r) s = None") |
|
261 apply(auto)[1] |
|
262 apply(simp) |
|
263 apply(erule exE) |
|
264 apply(simp) |
|
265 apply(rule iffI) |
|
266 apply(simp add: Posix_injval) |
|
267 apply(simp add: Posix1(1)) |
255 done |
268 done |
256 |
269 |
257 lemma lexer_correctness: |
270 lemma lexer_correctness: |
258 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
271 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
259 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
272 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
260 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
273 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
261 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
274 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
262 |
275 |
|
276 |
|
277 |
|
278 |
|
279 fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)" |
|
280 where |
|
281 "flex r f [] = f" |
|
282 | "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s" |
|
283 |
|
284 lemma flex_fun_apply: |
|
285 shows "g (flex r f s v) = flex r (g o f) s v" |
|
286 apply(induct s arbitrary: g f r v) |
|
287 apply(simp_all add: comp_def) |
|
288 by meson |
|
289 |
|
290 lemma flex_append: |
|
291 shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2" |
|
292 apply(induct s1 arbitrary: s2 r f) |
|
293 apply(simp) |
|
294 apply(drule_tac x="s2" in meta_spec) |
|
295 apply(drule_tac x="der a r" in meta_spec) |
|
296 apply(simp) |
|
297 done |
|
298 |
|
299 lemma lexer_flex: |
|
300 shows "lexer r s = (if nullable (ders s r) |
|
301 then Some(flex r id s (mkeps (ders s r))) else None)" |
|
302 apply(induct s arbitrary: r) |
|
303 apply(simp) |
|
304 apply(simp add: flex_fun_apply) |
|
305 done |
|
306 |
|
307 unused_thms |
|
308 |
263 end |
309 end |