787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; |
789 \<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 (NMTIMES r n m))\<rbrakk> |
789 \<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 (NMTIMES r n m))\<rbrakk> |
790 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
790 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
791 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
791 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
792 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; |
792 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
793 \<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> |
793 \<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> |
794 \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)" |
794 \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)" |
795 |
|
796 |
795 |
797 inductive_cases Posix_elims: |
796 inductive_cases Posix_elims: |
798 "s \<in> ZERO \<rightarrow> v" |
797 "s \<in> ZERO \<rightarrow> v" |
799 "s \<in> ONE \<rightarrow> v" |
798 "s \<in> ONE \<rightarrow> v" |
800 "s \<in> CHAR c \<rightarrow> v" |
799 "s \<in> CHAR c \<rightarrow> v" |
818 apply(simp add: Star_def) |
817 apply(simp add: Star_def) |
819 apply(clarify) |
818 apply(clarify) |
820 apply(rule_tac x="Suc x" in bexI) |
819 apply(rule_tac x="Suc x" in bexI) |
821 apply(auto simp add: Sequ_def) |
820 apply(auto simp add: Sequ_def) |
822 done |
821 done |
|
822 |
|
823 |
|
824 lemma |
|
825 "([] @ []) \<in> PLUS (ONE) \<rightarrow> Stars ([Void])" |
|
826 apply(rule Posix_PLUS1) |
|
827 apply(rule Posix.intros) |
|
828 apply(rule Posix.intros) |
|
829 apply(simp) |
|
830 apply(simp) |
|
831 done |
|
832 |
|
833 lemma |
|
834 assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []" "\<forall>s' \<in> L r. length s' < length s" |
|
835 shows "([] @ (s @ [])) \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left Void, Right v])" |
|
836 using assms |
|
837 oops |
|
838 |
|
839 lemma |
|
840 "([] @ ([] @ [])) \<in> FROMNTIMES (ONE) (Suc (Suc 0)) \<rightarrow> Stars ([Void, Void])" |
|
841 apply(rule Posix.intros) |
|
842 apply(rule Posix.intros) |
|
843 apply(rule Posix.intros) |
|
844 apply(rule Posix.intros) |
|
845 apply(rule Posix.intros) |
|
846 apply(rule Posix.intros) |
|
847 apply(auto) |
|
848 done |
|
849 |
|
850 |
|
851 lemma |
|
852 assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []" |
|
853 "s \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left(Void), Right(v)])" |
|
854 shows "False" |
|
855 using assms |
|
856 apply(rotate_tac 2) |
|
857 apply(erule_tac Posix.cases) |
|
858 apply(simp_all) |
|
859 apply(auto) |
|
860 oops |
|
861 |
|
862 |
|
863 |
823 |
864 |
824 |
865 |
825 lemma Posix1a: |
866 lemma Posix1a: |
826 assumes "s \<in> r \<rightarrow> v" |
867 assumes "s \<in> r \<rightarrow> v" |
827 shows "\<turnstile> v : r" |
868 shows "\<turnstile> v : r" |
1129 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1170 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1130 ultimately show "Stars (v # vs) = v2" by auto |
1171 ultimately show "Stars (v # vs) = v2" by auto |
1131 next |
1172 next |
1132 case (Posix_PLUS1 s1 r v s2 vs v2) |
1173 case (Posix_PLUS1 s1 r v s2 vs v2) |
1133 have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2" |
1174 have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2" |
1134 "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs" |
1175 "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs" (*"flat v = [] \<Longrightarrow> flat (Stars vs) = []"*) |
1135 "\<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+ |
1176 "\<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+ |
1136 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
1177 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
1137 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1178 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1138 using Posix1(1) apply fastforce |
1179 using Posix1(1) apply fastforce |
1139 by (metis Posix1(1) Posix_PLUS1.hyps(5) append_Nil2 self_append_conv2) |
1180 by (metis Posix1(1) Posix_PLUS1.hyps(6) append_self_conv append_self_conv2) |
1140 moreover |
1181 moreover |
1141 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1182 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1142 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1183 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1143 ultimately show "Stars (v # vs) = v2" by auto |
1184 ultimately show "Stars (v # vs) = v2" by auto |
1144 qed |
1185 qed |
1531 done |
1572 done |
1532 next |
1573 next |
1533 case (PLUS r) |
1574 case (PLUS r) |
1534 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1575 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1535 have "s \<in> der c (PLUS r) \<rightarrow> v" by fact |
1576 have "s \<in> der c (PLUS r) \<rightarrow> v" by fact |
1536 then consider |
1577 then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" |
1537 (cons) v1 vs s1 s2 where |
1578 apply - |
1538 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1579 apply(erule Posix.cases) |
1539 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
1580 apply(simp_all) |
1540 "\<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))" |
1581 apply(auto) |
1541 apply(simp) |
1582 apply(rotate_tac 3) |
1542 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
1583 apply(erule Posix.cases) |
1543 defer |
1584 apply(simp_all) |
1544 apply(rotate_tac 3) |
1585 apply(subst append_Cons[symmetric]) |
1545 apply(erule_tac Posix_elims(6)) |
1586 apply(rule Posix.intros) |
1546 apply (simp add: Posix.intros(6)) |
1587 using PLUS.hyps apply auto[1] |
1547 using Posix.intros(7) by blast |
1588 apply(rule Posix.intros) |
1548 then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" |
1589 apply(simp) |
1549 proof (cases) |
1590 apply(simp) |
1550 case cons |
1591 apply(simp) |
1551 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1592 apply(simp) |
1552 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1593 apply(simp) |
1553 moreover |
1594 using Posix1a Prf_injval_flat apply auto[1] |
1554 have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact |
1595 apply(simp add: der_correctness Der_def) |
1555 moreover |
1596 apply(subst append_Nil2[symmetric]) |
1556 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 |
1597 apply(rule Posix.intros) |
1557 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))" |
1598 using PLUS.hyps apply auto[1] |
1558 by (simp add: der_correctness Der_def) |
1599 apply(rule Posix.intros) |
1559 ultimately |
1600 apply(simp) |
1560 have "((c # s1) @ s2) \<in> (PLUS r) \<rightarrow> Stars (injval r c v1 # vs)" |
1601 apply(simp) |
1561 apply(rule_tac Posix.intros) |
1602 done |
1562 apply(simp_all) |
|
1563 done |
|
1564 then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" using cons by(simp) |
|
1565 qed |
|
1566 qed |
1603 qed |
1567 |
1604 |
1568 |
1605 |
1569 |
1606 |
1570 section {* The Lexer by Sulzmann and Lu *} |
1607 section {* The Lexer by Sulzmann and Lu *} |
1600 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
1637 shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v" |
1601 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
1638 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
1602 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
1639 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
1603 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
1640 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
1604 |
1641 |
|
1642 value "lexer (PLUS (ALT ONE (SEQ (CHAR (CHR ''a'')) (CHAR (CHR ''b''))))) [CHR ''a'', CHR ''b'']" |
|
1643 |
|
1644 |
1605 unused_thms |
1645 unused_thms |
1606 end |
1646 end |