401 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
401 | "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
402 \<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> |
402 \<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> |
403 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
403 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
404 | "[] \<in> STAR r \<rightarrow> Stars []" |
404 | "[] \<in> STAR r \<rightarrow> Stars []" |
405 |
405 |
406 lemma PMatch1: |
|
407 assumes "s \<in> r \<rightarrow> v" |
|
408 shows "s \<in> L r" "flat v = s" |
|
409 using assms |
|
410 apply(induct s r v rule: PMatch.induct) |
|
411 apply(auto simp add: Sequ_def) |
|
412 done |
|
413 |
|
414 lemma PMatch1a: |
|
415 assumes "s \<in> r \<rightarrow> v" |
|
416 shows "\<turnstile> v : r" |
|
417 using assms |
|
418 apply(induct s r v rule: PMatch.induct) |
|
419 apply(auto intro: Prf.intros) |
|
420 done |
|
421 |
|
422 lemma PMatch_mkeps: |
|
423 assumes "nullable r" |
|
424 shows "[] \<in> r \<rightarrow> mkeps r" |
|
425 using assms |
|
426 apply(induct r) |
|
427 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def) |
|
428 apply(subst append.simps(1)[symmetric]) |
|
429 apply (rule PMatch.intros) |
|
430 apply(auto) |
|
431 done |
|
432 |
|
433 inductive_cases PMatch_elims: |
406 inductive_cases PMatch_elims: |
434 "s \<in> ONE \<rightarrow> v" |
407 "s \<in> ONE \<rightarrow> v" |
435 "s \<in> CHAR c \<rightarrow> v" |
408 "s \<in> CHAR c \<rightarrow> v" |
436 "s \<in> ALT r1 r2 \<rightarrow> v" |
409 "s \<in> ALT r1 r2 \<rightarrow> v" |
437 "s \<in> SEQ r1 r2 \<rightarrow> v" |
410 "s \<in> SEQ r1 r2 \<rightarrow> v" |
438 "s \<in> STAR r \<rightarrow> v" |
411 "s \<in> STAR r \<rightarrow> v" |
439 |
412 |
440 thm PMatch_elims |
413 lemma PMatch1: |
|
414 assumes "s \<in> r \<rightarrow> v" |
|
415 shows "s \<in> L r" "flat v = s" |
|
416 using assms |
|
417 by (induct s r v rule: PMatch.induct) |
|
418 (auto simp add: Sequ_def) |
|
419 |
|
420 |
|
421 lemma PMatch1a: |
|
422 assumes "s \<in> r \<rightarrow> v" |
|
423 shows "\<turnstile> v : r" |
|
424 using assms |
|
425 apply(induct s r v rule: PMatch.induct) |
|
426 apply(auto intro: Prf.intros) |
|
427 done |
|
428 |
|
429 lemma PMatch_mkeps: |
|
430 assumes "nullable r" |
|
431 shows "[] \<in> r \<rightarrow> mkeps r" |
|
432 using assms |
|
433 apply(induct r) |
|
434 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def) |
|
435 apply(subst append.simps(1)[symmetric]) |
|
436 apply (rule PMatch.intros) |
|
437 apply(auto) |
|
438 done |
|
439 |
441 |
440 |
442 lemma PMatch_determ: |
441 lemma PMatch_determ: |
443 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
442 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
444 shows "v1 = v2" |
443 shows "v1 = v2" |
445 using assms |
444 using assms |
495 done |
494 done |
496 |
495 |
497 (* a proof that does not need proj *) |
496 (* a proof that does not need proj *) |
498 lemma PMatch2_roy_version: |
497 lemma PMatch2_roy_version: |
499 assumes "s \<in> (der c r) \<rightarrow> v" |
498 assumes "s \<in> (der c r) \<rightarrow> v" |
500 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
499 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
501 using assms |
500 using assms |
502 proof(induct r arbitrary: s v rule: rexp.induct) |
501 proof(induct r arbitrary: s v rule: rexp.induct) |
503 case ZERO |
502 case ZERO |
504 have "s \<in> der c ZERO \<rightarrow> v" by fact |
503 have "s \<in> der c ZERO \<rightarrow> v" by fact |
505 then have "s \<in> ZERO \<rightarrow> v" by simp |
504 then have "s \<in> ZERO \<rightarrow> v" by simp |
506 then have "False" by cases |
505 then have "False" by cases |
507 then show "(c#s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp |
506 then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp |
508 next |
507 next |
509 case ONE |
508 case ONE |
510 have "s \<in> der c ONE \<rightarrow> v" by fact |
509 have "s \<in> der c ONE \<rightarrow> v" by fact |
511 then have "s \<in> ZERO \<rightarrow> v" by simp |
510 then have "s \<in> ZERO \<rightarrow> v" by simp |
512 then have "False" by cases |
511 then have "False" by cases |
513 then show "(c#s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp |
512 then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp |
514 next |
513 next |
515 case (CHAR d) |
514 case (CHAR d) |
516 consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast |
515 consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast |
517 then show "(c#s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)" |
516 then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)" |
518 proof (cases) |
517 proof (cases) |
519 case eq |
518 case eq |
520 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
519 have "s \<in> der c (CHAR d) \<rightarrow> v" by fact |
521 then have "s \<in> ONE \<rightarrow> v" using eq by simp |
520 then have "s \<in> ONE \<rightarrow> v" using eq by simp |
522 then have eqs: "s = [] \<and> v = Void" by cases simp |
521 then have eqs: "s = [] \<and> v = Void" by cases simp |
647 lemma lex_correct1: |
646 lemma lex_correct1: |
648 assumes "s \<notin> L r" |
647 assumes "s \<notin> L r" |
649 shows "matcher r s = None" |
648 shows "matcher r s = None" |
650 using assms |
649 using assms |
651 apply(induct s arbitrary: r) |
650 apply(induct s arbitrary: r) |
652 apply(simp) |
651 apply(simp add: nullable_correctness) |
653 apply (metis nullable_correctness) |
|
654 apply(auto) |
|
655 apply(drule_tac x="der a r" in meta_spec) |
652 apply(drule_tac x="der a r" in meta_spec) |
656 apply(drule meta_mp) |
653 apply(auto simp add: der_correctness Der_def) |
657 apply(auto) |
|
658 apply(simp add: der_correctness Der_def) |
|
659 done |
654 done |
660 |
655 |
661 lemma lex_correct1a: |
656 lemma lex_correct1a: |
662 shows "s \<notin> L r \<longleftrightarrow> matcher r s = None" |
657 shows "s \<notin> L r \<longleftrightarrow> matcher r s = None" |
663 using assms |
658 using assms |
664 apply(induct s arbitrary: r) |
659 apply(induct s arbitrary: r) |
665 apply(simp) |
660 apply(simp add: nullable_correctness) |
666 apply (metis nullable_correctness) |
|
667 apply(auto) |
|
668 apply(drule_tac x="der a r" in meta_spec) |
661 apply(drule_tac x="der a r" in meta_spec) |
669 apply(auto) |
662 apply(auto simp add: der_correctness Der_def) |
670 apply(simp add: der_correctness Der_def) |
|
671 apply(drule_tac x="der a r" in meta_spec) |
|
672 apply(auto) |
|
673 apply(simp add: der_correctness Der_def) |
|
674 done |
663 done |
675 |
664 |
676 lemma lex_correct2: |
665 lemma lex_correct2: |
677 assumes "s \<in> L r" |
666 assumes "s \<in> L r" |
678 shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |
667 shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s" |