equal
deleted
inserted
replaced
205 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
205 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
206 | "der c (UPNTIMES r 0) = ZERO" |
206 | "der c (UPNTIMES r 0) = ZERO" |
207 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)" |
207 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)" |
208 | "der c (NTIMES r 0) = ZERO" |
208 | "der c (NTIMES r 0) = ZERO" |
209 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)" |
209 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)" |
210 | "der c (FROMNTIMES r 0) = SEQ (der c r) (STAR r)" |
210 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)" |
211 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)" |
211 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)" |
212 |
212 |
213 fun |
213 fun |
214 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
214 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
215 where |
215 where |
311 apply(rule impI) |
311 apply(rule impI) |
312 apply (simp add: Der_Pow_subseteq sup_absorb1) |
312 apply (simp add: Der_Pow_subseteq sup_absorb1) |
313 (* FROMNTIMES *) |
313 (* FROMNTIMES *) |
314 apply(simp only: der.simps) |
314 apply(simp only: der.simps) |
315 apply(simp only: L.simps) |
315 apply(simp only: L.simps) |
316 apply(subst Der_star[symmetric]) |
316 apply(simp) |
317 apply(subst Star_def2) |
317 using Der_star Star_def2 apply auto[1] |
318 apply(auto)[1] |
|
319 apply(simp only: der.simps) |
318 apply(simp only: der.simps) |
320 apply(simp only: L.simps) |
319 apply(simp only: L.simps) |
321 apply(simp add: Der_UNION) |
320 apply(simp add: Der_UNION) |
322 by (smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1) |
321 by (smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1) |
323 |
322 |
681 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
680 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
682 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
681 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
683 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
682 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
684 \<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 (FROMNTIMES r n))\<rbrakk> |
683 \<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 (FROMNTIMES r n))\<rbrakk> |
685 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
684 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
686 | Posix_FROMNTIMES2: "[] \<in> FROMNTIMES r 0 \<rightarrow> Stars []" |
685 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
|
686 |
687 |
687 |
688 inductive_cases Posix_elims: |
688 inductive_cases Posix_elims: |
689 "s \<in> ZERO \<rightarrow> v" |
689 "s \<in> ZERO \<rightarrow> v" |
690 "s \<in> ONE \<rightarrow> v" |
690 "s \<in> ONE \<rightarrow> v" |
691 "s \<in> CHAR c \<rightarrow> v" |
691 "s \<in> CHAR c \<rightarrow> v" |
701 apply(auto simp add: Sequ_def) |
701 apply(auto simp add: Sequ_def) |
702 apply(rule_tac x="Suc x" in bexI) |
702 apply(rule_tac x="Suc x" in bexI) |
703 apply(auto simp add: Sequ_def) |
703 apply(auto simp add: Sequ_def) |
704 apply(rule_tac x="Suc x" in bexI) |
704 apply(rule_tac x="Suc x" in bexI) |
705 apply(auto simp add: Sequ_def) |
705 apply(auto simp add: Sequ_def) |
706 done |
706 by (simp add: Star_in_Pow) |
707 |
707 |
708 |
708 |
709 lemma Posix1a: |
709 lemma Posix1a: |
710 assumes "s \<in> r \<rightarrow> v" |
710 assumes "s \<in> r \<rightarrow> v" |
711 shows "\<turnstile> v : r" |
711 shows "\<turnstile> v : r" |
732 apply(rule Prf.intros) |
732 apply(rule Prf.intros) |
733 apply(auto)[1] |
733 apply(auto)[1] |
734 apply(rotate_tac 3) |
734 apply(rotate_tac 3) |
735 apply(erule Prf.cases) |
735 apply(erule Prf.cases) |
736 apply(simp_all) |
736 apply(simp_all) |
737 using Prf.simps by blast |
737 using Prf.simps apply blast |
|
738 by (smt Prf.simps le0 rexp.distinct(61) rexp.distinct(63) rexp.distinct(65) rexp.inject(4) val.distinct(17) val.distinct(9) val.simps(29) val.simps(33) val.simps(35)) |
738 |
739 |
739 lemma Posix_NTIMES_mkeps: |
740 lemma Posix_NTIMES_mkeps: |
740 assumes "[] \<in> r \<rightarrow> mkeps r" |
741 assumes "[] \<in> r \<rightarrow> mkeps r" |
741 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
742 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
742 apply(induct n) |
743 apply(induct n) |
753 assumes "[] \<in> r \<rightarrow> mkeps r" |
754 assumes "[] \<in> r \<rightarrow> mkeps r" |
754 shows "[] \<in> FROMNTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
755 shows "[] \<in> FROMNTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
755 apply(induct n) |
756 apply(induct n) |
756 apply(simp) |
757 apply(simp) |
757 apply (rule Posix_FROMNTIMES2) |
758 apply (rule Posix_FROMNTIMES2) |
|
759 apply (rule Posix.intros) |
758 apply(simp) |
760 apply(simp) |
759 apply(subst append_Nil[symmetric]) |
761 apply(subst append_Nil[symmetric]) |
760 apply (rule Posix_FROMNTIMES1) |
762 apply (rule Posix_FROMNTIMES1) |
761 apply(auto) |
763 apply(auto) |
762 apply(rule assms) |
764 apply(rule assms) |
779 apply(subst append.simps(1)[symmetric]) |
781 apply(subst append.simps(1)[symmetric]) |
780 apply(rule Posix.intros) |
782 apply(rule Posix.intros) |
781 apply(auto) |
783 apply(auto) |
782 apply(rule Posix_NTIMES_mkeps) |
784 apply(rule Posix_NTIMES_mkeps) |
783 apply(simp) |
785 apply(simp) |
|
786 apply(rule Posix.intros) |
|
787 apply(rule Posix.intros) |
784 apply(case_tac n) |
788 apply(case_tac n) |
785 apply(simp) |
789 apply(simp) |
786 apply (simp add: Posix_FROMNTIMES2) |
790 apply(rule Posix.intros) |
|
791 apply(rule Posix.intros) |
787 apply(simp) |
792 apply(simp) |
788 apply(subst append.simps(1)[symmetric]) |
793 apply(subst append.simps(1)[symmetric]) |
789 apply(rule Posix.intros) |
794 apply(rule Posix.intros) |
790 apply(auto) |
795 apply(auto) |
791 apply(rule Posix_FROMNTIMES_mkeps) |
796 apply(rule Posix_FROMNTIMES_mkeps) |
892 moreover |
897 moreover |
893 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
898 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
894 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
899 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
895 ultimately show "Stars (v # vs) = v2" by auto |
900 ultimately show "Stars (v # vs) = v2" by auto |
896 next |
901 next |
897 case (Posix_FROMNTIMES2 r v2) |
902 case (Posix_FROMNTIMES2 s r v1 v2) |
898 have "[] \<in> FROMNTIMES r 0 \<rightarrow> v2" by fact |
903 have "s \<in> FROMNTIMES r 0 \<rightarrow> v2" "s \<in> STAR r \<rightarrow> Stars v1" |
899 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
904 "\<And>v3. s \<in> STAR r \<rightarrow> v3 \<Longrightarrow> Stars v1 = v3" by fact+ |
|
905 then show ?case |
|
906 apply(cases) |
|
907 apply(auto) |
|
908 done |
900 next |
909 next |
901 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
910 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
902 have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" |
911 have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" |
903 "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs" |
912 "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs" |
904 "\<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 (FROMNTIMES r n))" by fact+ |
913 "\<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 (FROMNTIMES r n))" by fact+ |
1175 have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact |
1184 have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact |
1176 then consider |
1185 then consider |
1177 (null) v1 vs s1 s2 where |
1186 (null) v1 vs s1 s2 where |
1178 "n = 0" |
1187 "n = 0" |
1179 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1188 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1180 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)" |
1189 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)" |
1181 "\<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 0))" |
1190 "\<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 0))" |
1182 | (cons) m v1 vs s1 s2 where |
1191 | (cons) m v1 vs s1 s2 where |
1183 "n = Suc m" |
1192 "n = Suc m" |
1184 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1193 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1185 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
1194 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
1188 apply(simp) |
1197 apply(simp) |
1189 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
1198 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
1190 defer |
1199 defer |
1191 apply (metis FROMNTIMES_Stars Posix1a) |
1200 apply (metis FROMNTIMES_Stars Posix1a) |
1192 apply(rotate_tac 5) |
1201 apply(rotate_tac 5) |
1193 apply(erule_tac Posix_elims(6)) |
1202 apply(erule Posix.cases) |
1194 apply(auto) |
1203 apply(simp_all) |
1195 apply(drule_tac x="v1" in meta_spec) |
1204 apply(clarify) |
1196 apply(simp) |
1205 by (simp add: Posix_FROMNTIMES2) |
1197 apply(drule_tac x="v # vs" in meta_spec) |
|
1198 apply(simp) |
|
1199 apply(drule_tac x="s1" in meta_spec) |
|
1200 apply(simp) |
|
1201 apply(drule_tac x="s1a @ s2a" in meta_spec) |
|
1202 apply(simp) |
|
1203 apply(drule meta_mp) |
|
1204 apply(rule Posix.intros) |
|
1205 apply(simp) |
|
1206 apply(simp) |
|
1207 apply(simp) |
|
1208 apply(simp) |
|
1209 using Pow_in_Star apply blast |
|
1210 by (meson Posix_STAR2 append_is_Nil_conv self_append_conv) |
|
1211 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" |
1206 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" |
1212 proof (cases) |
1207 proof (cases) |
1213 case cons |
1208 case cons |
1214 have "n = Suc m" by fact |
1209 have "n = Suc m" by fact |
1215 moreover |
1210 moreover |
1227 apply(simp_all) |
1222 apply(simp_all) |
1228 done |
1223 done |
1229 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
1224 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
1230 next |
1225 next |
1231 case null |
1226 case null |
1232 then show ?thesis |
1227 then have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" |
|
1228 apply(rule_tac Posix.intros) |
|
1229 apply(rule_tac Posix.intros) |
|
1230 apply(rule IH) |
1233 apply(simp) |
1231 apply(simp) |
1234 sorry |
1232 apply(rotate_tac 4) |
|
1233 apply(erule Posix.cases) |
|
1234 apply(simp_all) |
|
1235 apply (simp add: Posix1a Prf_injval_flat) |
|
1236 apply(simp only: Star_def2) |
|
1237 apply(simp only: der_correctness Der_def) |
|
1238 apply(simp) |
|
1239 done |
|
1240 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp |
1235 qed |
1241 qed |
1236 qed |
1242 qed |
1237 |
1243 |
1238 |
1244 |
1239 section {* The Lexer by Sulzmann and Lu *} |
1245 section {* The Lexer by Sulzmann and Lu *} |