204 | "\<turnstile> Void : ONE" |
202 | "\<turnstile> Void : ONE" |
205 | "\<turnstile> Char c : CHAR c" |
203 | "\<turnstile> Char c : CHAR c" |
206 | "\<turnstile> Stars [] : STAR r" |
204 | "\<turnstile> Stars [] : STAR r" |
207 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r" |
205 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r" |
208 |
206 |
209 lemma not_nullable_flat: |
207 inductive_cases Prf_elims: |
210 assumes "\<turnstile> v : r" "\<not> nullable r" |
208 "\<turnstile> v : ZERO" |
211 shows "flat v \<noteq> []" |
209 "\<turnstile> v : SEQ r1 r2" |
212 using assms |
210 "\<turnstile> v : ALT r1 r2" |
213 by (induct) (auto) |
211 "\<turnstile> v : ONE" |
|
212 "\<turnstile> v : CHAR c" |
|
213 (* "\<turnstile> vs : STAR r"*) |
|
214 |
|
215 |
214 |
216 |
215 lemma Prf_flat_L: |
217 lemma Prf_flat_L: |
216 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
218 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
217 using assms |
219 using assms |
218 apply(induct v r rule: Prf.induct) |
220 apply(induct v r rule: Prf.induct) |
256 apply (metis Prf.intros(4) flat.simps(1)) |
259 apply (metis Prf.intros(4) flat.simps(1)) |
257 apply (metis Prf.intros(5) flat.simps(2)) |
260 apply (metis Prf.intros(5) flat.simps(2)) |
258 apply (metis Prf.intros(1) flat.simps(5)) |
261 apply (metis Prf.intros(1) flat.simps(5)) |
259 apply (metis Prf.intros(2) flat.simps(3)) |
262 apply (metis Prf.intros(2) flat.simps(3)) |
260 apply (metis Prf.intros(3) flat.simps(4)) |
263 apply (metis Prf.intros(3) flat.simps(4)) |
261 apply(erule Prf.cases) |
264 apply(auto elim!: Prf_elims) |
262 apply(auto) |
|
263 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
265 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = x \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
264 apply(auto)[1] |
266 apply(auto)[1] |
265 apply(rule_tac x="Stars vs" in exI) |
267 apply(rule_tac x="Stars vs" in exI) |
266 apply(simp) |
268 apply(simp) |
267 apply(rule Prf_Stars) |
269 apply(rule Prf_Stars) |
302 "matcher r [] = (if nullable r then Some(mkeps r) else None)" |
304 "matcher r [] = (if nullable r then Some(mkeps r) else None)" |
303 | "matcher r (c#s) = (case (matcher (der c r) s) of |
305 | "matcher r (c#s) = (case (matcher (der c r) s) of |
304 None \<Rightarrow> None |
306 None \<Rightarrow> None |
305 | Some(v) \<Rightarrow> Some(injval r c v))" |
307 | Some(v) \<Rightarrow> Some(injval r c v))" |
306 |
308 |
307 fun |
|
308 matcher2 :: "rexp \<Rightarrow> string \<Rightarrow> val" |
|
309 where |
|
310 "matcher2 r [] = mkeps r" |
|
311 | "matcher2 r (c#s) = injval r c (matcher2 (der c r) s)" |
|
312 |
|
313 |
|
314 |
309 |
315 section {* Mkeps, injval *} |
310 section {* Mkeps, injval *} |
316 |
311 |
317 lemma mkeps_nullable: |
312 lemma mkeps_nullable: |
318 assumes "nullable(r)" |
313 assumes "nullable(r)" |
319 shows "\<turnstile> mkeps r : r" |
314 shows "\<turnstile> mkeps r : r" |
320 using assms |
315 using assms |
321 apply(induct rule: nullable.induct) |
316 by (induct rule: nullable.induct) |
322 apply(auto intro: Prf.intros) |
317 (auto intro: Prf.intros) |
323 done |
|
324 |
318 |
325 lemma mkeps_flat: |
319 lemma mkeps_flat: |
326 assumes "nullable(r)" |
320 assumes "nullable(r)" |
327 shows "flat (mkeps r) = []" |
321 shows "flat (mkeps r) = []" |
328 using assms |
322 using assms |
329 apply(induct rule: nullable.induct) |
323 by (induct rule: nullable.induct) (auto) |
330 apply(auto) |
324 |
331 done |
|
332 |
325 |
333 lemma Prf_injval: |
326 lemma Prf_injval: |
334 assumes "\<turnstile> v : der c r" |
327 assumes "\<turnstile> v : der c r" |
335 shows "\<turnstile> (injval r c v) : r" |
328 shows "\<turnstile> (injval r c v) : r" |
336 using assms |
329 using assms |
337 apply(induct r arbitrary: c v rule: rexp.induct) |
330 apply(induct r arbitrary: c v rule: rexp.induct) |
338 apply(simp_all) |
331 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
339 (* ZERO *) |
|
340 apply(erule Prf.cases) |
|
341 apply(simp_all)[7] |
|
342 (* ONE *) |
|
343 apply(erule Prf.cases) |
|
344 apply(simp_all)[7] |
|
345 (* CHAR *) |
|
346 apply(case_tac "c = x") |
|
347 apply(simp) |
|
348 apply(erule Prf.cases) |
|
349 apply(simp_all)[7] |
|
350 apply(rule Prf.intros(5)) |
|
351 apply(simp) |
|
352 apply(erule Prf.cases) |
|
353 apply(simp_all)[7] |
|
354 (* SEQ *) |
|
355 apply(case_tac "nullable x1") |
|
356 apply(simp) |
|
357 apply(erule Prf.cases) |
|
358 apply(simp_all)[7] |
|
359 apply(auto)[1] |
|
360 apply(erule Prf.cases) |
|
361 apply(simp_all)[7] |
|
362 apply(auto)[1] |
|
363 apply(rule Prf.intros) |
|
364 apply(auto)[2] |
|
365 apply (metis Prf.intros(1) mkeps_nullable) |
|
366 apply(simp) |
|
367 apply(erule Prf.cases) |
|
368 apply(simp_all)[7] |
|
369 apply(auto)[1] |
|
370 apply(rule Prf.intros) |
|
371 apply(auto)[2] |
|
372 (* ALT *) |
|
373 apply(erule Prf.cases) |
|
374 apply(simp_all)[7] |
|
375 apply(clarify) |
|
376 apply (metis Prf.intros(2)) |
|
377 apply (metis Prf.intros(3)) |
|
378 (* STAR *) |
332 (* STAR *) |
379 apply(erule Prf.cases) |
|
380 apply(simp_all)[7] |
|
381 apply(clarify) |
|
382 apply(rotate_tac 2) |
333 apply(rotate_tac 2) |
383 apply(erule Prf.cases) |
334 apply(erule Prf.cases) |
384 apply(simp_all)[7] |
335 apply(simp_all)[7] |
385 apply(auto) |
336 apply(auto) |
386 apply (metis Prf.intros(6) Prf.intros(7)) |
337 apply (metis Prf.intros(6) Prf.intros(7)) |
476 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def) |
427 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def) |
477 apply(subst append.simps(1)[symmetric]) |
428 apply(subst append.simps(1)[symmetric]) |
478 apply (rule PMatch.intros) |
429 apply (rule PMatch.intros) |
479 apply(auto) |
430 apply(auto) |
480 done |
431 done |
|
432 |
|
433 inductive_cases PMatch_elims: |
|
434 "s \<in> ONE \<rightarrow> v" |
|
435 "s \<in> CHAR c \<rightarrow> v" |
|
436 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
437 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
438 "s \<in> STAR r \<rightarrow> v" |
|
439 |
|
440 thm PMatch_elims |
481 |
441 |
482 lemma PMatch_determ: |
442 lemma PMatch_determ: |
483 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
443 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
484 shows "v1 = v2" |
444 shows "v1 = v2" |
485 using assms |
445 using assms |
558 proof (cases) |
518 proof (cases) |
559 case eq |
519 case eq |
560 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
520 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
561 then have "s \<in> ONE \<rightarrow> v" using eq by simp |
521 then have "s \<in> ONE \<rightarrow> v" using eq by simp |
562 then have eqs: "s = [] \<and> v = Void" by cases simp |
522 then have eqs: "s = [] \<and> v = Void" by cases simp |
563 show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs by (auto intro: PMatch.intros) |
523 show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs |
|
524 by (auto intro: PMatch.intros) |
564 next |
525 next |
565 case ineq |
526 case ineq |
566 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
527 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
567 then have "s \<in> ZERO \<rightarrow> v" using ineq by simp |
528 then have "s \<in> ZERO \<rightarrow> v" using ineq by simp |
568 then have "False" by cases |
529 then have "False" by cases |
610 "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" |
571 "s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" |
611 | (not_nullable) v1 v2 s1 s2 where |
572 | (not_nullable) v1 v2 s1 s2 where |
612 "v = Seq v1 v2" "s = s1 @ s2" |
573 "v = Seq v1 v2" "s = s1 @ s2" |
613 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" |
574 "s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1" |
614 "\<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)" |
575 "\<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)" |
615 apply(auto split: if_splits simp add: Sequ_def) apply(erule PMatch.cases) |
576 by (force split: if_splits elim!: PMatch_elims simp add: Sequ_def der_correctness Der_def) |
616 apply(auto elim: PMatch.cases simp add: Sequ_def der_correctness Der_def) |
|
617 by fastforce |
|
618 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" |
577 then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" |
619 proof (cases) |
578 proof (cases) |
620 case left_nullable |
579 case left_nullable |
621 have "s1 \<in> der c r1 \<rightarrow> v1" by fact |
580 have "s1 \<in> der c r1 \<rightarrow> v1" by fact |
622 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
581 then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp |
657 then consider |
616 then consider |
658 (cons) v1 vs s1 s2 where |
617 (cons) v1 vs s1 s2 where |
659 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
618 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
660 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
619 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
661 "\<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))" |
620 "\<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))" |
662 apply(erule_tac PMatch.cases) |
621 apply(auto elim!: PMatch_elims(1-4) simp add: der_correctness Der_def intro: PMatch.intros) |
663 apply(auto) |
622 apply(rotate_tac 3) |
664 apply(rotate_tac 4) |
623 apply(erule_tac PMatch_elims(5)) |
665 apply(erule_tac PMatch.cases) |
|
666 apply(auto) |
|
667 apply (simp add: PMatch.intros(6)) |
624 apply (simp add: PMatch.intros(6)) |
668 using PMatch.intros(7) by blast |
625 using PMatch.intros(7) by blast |
669 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" |
626 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" |
670 proof (cases) |
627 proof (cases) |
671 case cons |
628 case cons |
775 apply(auto) |
732 apply(auto) |
776 apply(rule PMatch2_roy_version) |
733 apply(rule PMatch2_roy_version) |
777 apply(simp) |
734 apply(simp) |
778 using PMatch1(1) by auto |
735 using PMatch1(1) by auto |
779 |
736 |
780 lemma lex_correct5: |
|
781 assumes "s \<in> L r" |
|
782 shows "s \<in> r \<rightarrow> (matcher2 r s)" |
|
783 using assms |
|
784 apply(induct s arbitrary: r) |
|
785 apply(simp) |
|
786 apply (metis PMatch_mkeps nullable_correctness) |
|
787 apply(simp) |
|
788 apply(rule PMatch2_roy_version) |
|
789 apply(drule_tac x="der a r" in meta_spec) |
|
790 apply(drule meta_mp) |
|
791 apply(simp add: der_correctness Der_def) |
|
792 apply(auto) |
|
793 done |
|
794 |
|
795 lemma |
|
796 "matcher2 (ALT (CHAR a) (ALT (CHAR b) (SEQ (CHAR a) (CHAR b)))) [a,b] = Right (Right (Seq (Char a) (Char b)))" |
|
797 apply(simp) |
|
798 done |
|
799 |
737 |
800 fun F_RIGHT where |
738 fun F_RIGHT where |
801 "F_RIGHT f v = Right (f v)" |
739 "F_RIGHT f v = Right (f v)" |
802 |
740 |
803 fun F_LEFT where |
741 fun F_LEFT where |