661 using Prf.intros(8) flat_Stars by blast |
663 using Prf.intros(8) flat_Stars by blast |
662 next |
664 next |
663 case (FROMNTIMES r n) |
665 case (FROMNTIMES r n) |
664 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
666 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
665 have "s \<in> L (FROMNTIMES r n)" by fact |
667 have "s \<in> L (FROMNTIMES r n)" by fact |
666 then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m" |
668 then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k" |
667 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
669 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
668 using Pow_cstring by force |
670 using Pow_cstring by force |
669 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m" |
671 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k" |
670 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
672 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
671 using IH flats_cval |
673 using IH flats_cval |
672 apply - |
674 apply - |
673 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
675 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
674 apply(drule_tac x="r" in meta_spec) |
676 apply(drule_tac x="r" in meta_spec) |
721 apply(drule_tac x="vs1" in meta_spec) |
723 apply(drule_tac x="vs1" in meta_spec) |
722 apply(drule_tac x="vs2" in meta_spec) |
724 apply(drule_tac x="vs2" in meta_spec) |
723 apply(simp) |
725 apply(simp) |
724 done |
726 done |
725 then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s" |
727 then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s" |
726 apply(rule_tac x="Stars (vs1 @ vs2)" in exI) |
728 apply(case_tac "length vs1 \<le> n") |
727 apply(simp) |
729 apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI) |
728 apply(rule Prf.intros) |
730 apply(simp) |
729 apply(auto) |
731 apply(subgoal_tac "flats (take (n - length vs1) vs2) = []") |
730 sorry |
732 prefer 2 |
|
733 apply (meson flats_empty in_set_takeD) |
|
734 apply(clarify) |
|
735 apply(rule conjI) |
|
736 apply(rule Prf.intros) |
|
737 apply(simp) |
|
738 apply (meson in_set_takeD) |
|
739 apply(simp) |
|
740 apply(simp) |
|
741 apply (simp add: flats_empty) |
|
742 apply(rule_tac x="Stars vs1" in exI) |
|
743 apply(simp) |
|
744 apply(rule conjI) |
|
745 apply(rule Prf.intros) |
|
746 apply(auto) |
|
747 done |
731 next |
748 next |
732 case (UPNTIMES r n s) |
749 case (UPNTIMES r n s) |
733 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
750 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
734 have "s \<in> L (UPNTIMES r n)" by fact |
751 have "s \<in> L (UPNTIMES r n)" by fact |
735 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n" |
752 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n" |
804 unfolding suffix_def prefix_def image_def |
821 unfolding suffix_def prefix_def image_def |
805 by (auto)(metis rev_append rev_rev_ident)+ |
822 by (auto)(metis rev_append rev_rev_ident)+ |
806 ultimately show "finite (Prefixes s)" by simp |
823 ultimately show "finite (Prefixes s)" by simp |
807 qed |
824 qed |
808 |
825 |
|
826 definition |
|
827 "Stars_Cons V Vs \<equiv> {Stars (v # vs) | v vs. v \<in> V \<and> Stars vs \<in> Vs}" |
|
828 |
|
829 definition |
|
830 "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}" |
|
831 |
|
832 fun Stars_Pow :: "val set \<Rightarrow> nat \<Rightarrow> val set" |
|
833 where |
|
834 "Stars_Pow Vs 0 = {Stars []}" |
|
835 | "Stars_Pow Vs (Suc n) = Stars_Cons Vs (Stars_Pow Vs n)" |
|
836 |
|
837 lemma finite_Stars_Cons: |
|
838 assumes "finite V" "finite Vs" |
|
839 shows "finite (Stars_Cons V Vs)" |
|
840 using assms |
|
841 proof - |
|
842 from assms(2) have "finite (Stars -` Vs)" |
|
843 by(simp add: finite_vimageI inj_on_def) |
|
844 with assms(1) have "finite (V \<times> (Stars -` Vs))" |
|
845 by(simp) |
|
846 then have "finite ((\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs)))" |
|
847 by simp |
|
848 moreover have "Stars_Cons V Vs = (\<lambda>(v, vs). Stars (v # vs)) ` (V \<times> (Stars -` Vs))" |
|
849 unfolding Stars_Cons_def by auto |
|
850 ultimately show "finite (Stars_Cons V Vs)" |
|
851 by simp |
|
852 qed |
|
853 |
|
854 lemma finite_Stars_Append: |
|
855 assumes "finite Vs1" "finite Vs2" |
|
856 shows "finite (Stars_Append Vs1 Vs2)" |
|
857 using assms |
|
858 proof - |
|
859 define UVs1 where "UVs1 \<equiv> Stars -` Vs1" |
|
860 define UVs2 where "UVs2 \<equiv> Stars -` Vs2" |
|
861 from assms have "finite UVs1" "finite UVs2" |
|
862 unfolding UVs1_def UVs2_def |
|
863 by(simp_all add: finite_vimageI inj_on_def) |
|
864 then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))" |
|
865 by simp |
|
866 moreover |
|
867 have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)" |
|
868 unfolding Stars_Append_def UVs1_def UVs2_def by auto |
|
869 ultimately show "finite (Stars_Append Vs1 Vs2)" |
|
870 by simp |
|
871 qed |
|
872 |
|
873 lemma finite_Stars_Pow: |
|
874 assumes "finite Vs" |
|
875 shows "finite (Stars_Pow Vs n)" |
|
876 by (induct n) (simp_all add: finite_Stars_Cons assms) |
|
877 |
809 lemma LV_STAR_finite: |
878 lemma LV_STAR_finite: |
810 assumes "\<forall>s. finite (LV r s)" |
879 assumes "\<forall>s. finite (LV r s)" |
811 shows "finite (LV (STAR r) s)" |
880 shows "finite (LV (STAR r) s)" |
812 proof(induct s rule: length_induct) |
881 proof(induct s rule: length_induct) |
813 fix s::"char list" |
882 fix s::"char list" |
814 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
883 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
815 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
884 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
816 by (auto simp add: strict_suffix_def) |
885 by (auto simp add: strict_suffix_def) |
817 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
886 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
818 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
887 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
819 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
888 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2" |
820 have "finite S1" using assms |
889 have "finite S1" using assms |
821 unfolding S1_def by (simp_all add: finite_Prefixes) |
890 unfolding S1_def by (simp_all add: finite_Prefixes) |
822 moreover |
891 moreover |
823 with IH have "finite S2" unfolding S2_def |
892 with IH have "finite S2" unfolding S2_def |
824 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
893 by (auto simp add: finite_SSuffixes) |
825 ultimately |
894 ultimately |
826 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
895 have "finite ({Stars []} \<union> Stars_Cons S1 S2)" |
|
896 by (simp add: finite_Stars_Cons) |
827 moreover |
897 moreover |
828 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
898 have "LV (STAR r) s \<subseteq> {Stars []} \<union> (Stars_Cons S1 S2)" |
829 unfolding S1_def S2_def f_def |
899 unfolding S1_def S2_def f_def LV_def Stars_Cons_def |
830 unfolding LV_def image_def prefix_def strict_suffix_def |
900 unfolding prefix_def strict_suffix_def |
|
901 unfolding image_def |
831 apply(auto) |
902 apply(auto) |
832 apply(case_tac x) |
903 apply(case_tac x) |
833 apply(auto elim: Prf_elims) |
904 apply(auto elim: Prf_elims) |
834 apply(erule Prf_elims) |
905 apply(erule Prf_elims) |
835 apply(auto) |
906 apply(auto) |
836 apply(case_tac vs) |
907 apply(case_tac vs) |
837 apply(auto intro: Prf.intros) |
908 apply(auto intro: Prf.intros) |
838 apply(rule exI) |
909 apply(rule exI) |
839 apply(rule conjI) |
910 apply(rule conjI) |
|
911 apply(rule_tac x="flats list" in exI) |
|
912 apply(rule conjI) |
840 apply(rule_tac x="flat a" in exI) |
913 apply(rule_tac x="flat a" in exI) |
841 apply(rule conjI) |
|
842 apply(rule_tac x="flats list" in exI) |
|
843 apply(simp) |
914 apply(simp) |
844 apply(blast) |
915 apply(blast) |
845 using Prf.intros(6) by blast |
916 using Prf.intros(6) flat_Stars by blast |
846 ultimately |
917 ultimately |
847 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
918 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
848 qed |
919 qed |
849 |
920 |
850 lemma LV_UPNTIMES_STAR: |
921 lemma LV_UPNTIMES_STAR: |
851 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
922 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
852 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
923 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
853 |
|
854 |
|
855 lemma LV_NTIMES_0: |
|
856 shows "LV (NTIMES r 0) s \<subseteq> {Stars []}" |
|
857 unfolding LV_def |
|
858 apply(auto elim: Prf_elims) |
|
859 done |
|
860 |
|
861 lemma LV_NTIMES_1: |
|
862 shows "LV (NTIMES r 1) s \<subseteq> (\<lambda>v. Stars [v]) ` (LV r s)" |
|
863 unfolding LV_def |
|
864 apply(auto elim!: Prf_elims) |
|
865 apply(case_tac vs1) |
|
866 apply(simp) |
|
867 apply(case_tac vs2) |
|
868 apply(simp) |
|
869 apply(simp) |
|
870 apply(simp) |
|
871 done |
|
872 |
|
873 lemma LV_NTIMES_2: |
|
874 shows "LV (NTIMES r 2) [] \<subseteq> (\<lambda>(v1,v2). Stars [v1,v2]) ` (LV r [] \<times> LV r [])" |
|
875 unfolding LV_def |
|
876 apply(auto elim!: Prf_elims simp add: image_def) |
|
877 apply(case_tac vs1) |
|
878 apply(auto) |
|
879 apply(case_tac vs2) |
|
880 apply(auto) |
|
881 apply(case_tac list) |
|
882 apply(auto) |
|
883 done |
|
884 |
924 |
885 lemma LV_NTIMES_3: |
925 lemma LV_NTIMES_3: |
886 shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))" |
926 shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))" |
887 unfolding LV_def |
927 unfolding LV_def |
888 apply(auto elim!: Prf_elims simp add: image_def) |
928 apply(auto elim!: Prf_elims simp add: image_def) |
894 apply(rule Prf.intros) |
934 apply(rule Prf.intros) |
895 apply(auto) |
935 apply(auto) |
896 apply(subst append.simps(1)[symmetric]) |
936 apply(subst append.simps(1)[symmetric]) |
897 apply(rule Prf.intros) |
937 apply(rule Prf.intros) |
898 apply(auto) |
938 apply(auto) |
899 done |
939 done |
900 |
940 |
901 thm card_cartesian_product |
941 lemma LV_FROMNTIMES_3: |
902 |
942 shows "LV (FROMNTIMES r (Suc n)) [] = |
903 lemma finite_list: |
943 (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (FROMNTIMES r n) [])))" |
904 assumes "finite A" |
944 unfolding LV_def |
905 shows "finite {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n}" |
945 apply(auto elim!: Prf_elims simp add: image_def) |
|
946 apply(case_tac vs1) |
|
947 apply(auto) |
|
948 apply(case_tac vs2) |
|
949 apply(auto) |
|
950 apply(subst append.simps(1)[symmetric]) |
|
951 apply(rule Prf.intros) |
|
952 apply(auto) |
|
953 apply (metis le_imp_less_Suc length_greater_0_conv less_antisym list.exhaust list.set_intros(1) not_less_eq zero_le) |
|
954 prefer 2 |
|
955 using nth_mem apply blast |
|
956 apply(case_tac vs1) |
|
957 apply (smt Groups.add_ac(2) Prf.intros(9) add.right_neutral add_Suc_right append.simps(1) insert_iff length_append list.set(2) list.size(3) list.size(4)) |
|
958 apply(auto) |
|
959 done |
|
960 |
|
961 lemma LV_NTIMES_4: |
|
962 "LV (NTIMES r n) [] = Stars_Pow (LV r []) n" |
906 apply(induct n) |
963 apply(induct n) |
907 apply(simp) |
964 apply(simp add: LV_def) |
908 apply (smt Collect_cong empty_iff finite.emptyI finite.insertI |
965 apply(auto elim!: Prf_elims simp add: image_def)[1] |
909 in_listsI list.set(1) lists_empty mem_Collect_eq singleton_conv2) |
966 apply(subst append.simps[symmetric]) |
910 apply(rule_tac B="{[]} \<union> (\<lambda>(v,vs). v # vs) `(A \<times> {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n})" in finite_subset) |
967 apply(rule Prf.intros) |
911 apply(auto simp add: image_def)[1] |
968 apply(simp_all) |
|
969 apply(simp add: LV_NTIMES_3 image_def Stars_Cons_def) |
|
970 apply blast |
|
971 done |
|
972 |
|
973 lemma LV_NTIMES_5: |
|
974 "LV (NTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) [])" |
|
975 apply(auto simp add: LV_def) |
|
976 apply(auto elim!: Prf_elims) |
|
977 apply(auto simp add: Stars_Append_def) |
|
978 apply(rule_tac x="vs1" in exI) |
|
979 apply(rule_tac x="vs2" in exI) |
|
980 apply(auto) |
|
981 using Prf.intros(6) apply(auto) |
|
982 apply(rule_tac x="length vs2" in bexI) |
|
983 thm Prf.intros |
|
984 apply(subst append.simps(1)[symmetric]) |
|
985 apply(rule Prf.intros) |
|
986 apply(auto)[1] |
|
987 apply(auto)[1] |
|
988 apply(simp) |
|
989 apply(simp) |
|
990 done |
|
991 |
|
992 lemma ttty: |
|
993 "LV (FROMNTIMES r n) [] = Stars_Pow (LV r []) n" |
|
994 apply(induct n) |
|
995 apply(simp add: LV_def) |
|
996 apply(auto elim: Prf_elims simp add: image_def)[1] |
|
997 prefer 2 |
|
998 apply(subst append.simps[symmetric]) |
|
999 apply(rule Prf.intros) |
|
1000 apply(simp_all) |
|
1001 apply(erule Prf_elims) |
|
1002 apply(case_tac vs1) |
|
1003 apply(simp) |
|
1004 apply(simp) |
912 apply(case_tac x) |
1005 apply(case_tac x) |
913 apply(simp) |
1006 apply(simp_all) |
914 apply(simp) |
1007 apply(simp add: LV_FROMNTIMES_3 image_def Stars_Cons_def) |
915 apply(simp) |
1008 apply blast |
916 apply(rule finite_imageI) |
1009 done |
917 using assms |
1010 |
918 apply(simp) |
1011 lemma LV_FROMNTIMES_5: |
919 done |
1012 "LV (FROMNTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (FROMNTIMES r i) [])" |
920 |
1013 apply(auto simp add: LV_def) |
921 lemma test: |
1014 apply(auto elim!: Prf_elims) |
922 "LV (NTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}" |
1015 apply(auto simp add: Stars_Append_def) |
923 apply(auto simp add: LV_def elim: Prf_elims) |
1016 apply(rule_tac x="vs1" in exI) |
924 done |
1017 apply(rule_tac x="vs2" in exI) |
|
1018 apply(auto) |
|
1019 using Prf.intros(6) apply(auto) |
|
1020 apply(rule_tac x="length vs2" in bexI) |
|
1021 thm Prf.intros |
|
1022 apply(subst append.simps(1)[symmetric]) |
|
1023 apply(rule Prf.intros) |
|
1024 apply(auto)[1] |
|
1025 apply(auto)[1] |
|
1026 apply(simp) |
|
1027 apply(simp) |
|
1028 apply(rule_tac x="vs" in exI) |
|
1029 apply(rule_tac x="[]" in exI) |
|
1030 apply(auto) |
|
1031 by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le) |
|
1032 |
|
1033 lemma LV_FROMNTIMES_6: |
|
1034 assumes "\<forall>s. finite (LV r s)" |
|
1035 shows "finite (LV (FROMNTIMES r n) s)" |
|
1036 apply(rule finite_subset) |
|
1037 apply(rule LV_FROMNTIMES_5) |
|
1038 apply(rule finite_Stars_Append) |
|
1039 apply(rule LV_STAR_finite) |
|
1040 apply(rule assms) |
|
1041 apply(rule finite_UN_I) |
|
1042 apply(auto) |
|
1043 by (simp add: assms finite_Stars_Pow ttty) |
925 |
1044 |
926 lemma test3: |
1045 lemma LV_NMTIMES_5: |
927 "LV (FROMNTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}" |
1046 "LV (NMTIMES r n m) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (FROMNTIMES r i) [])" |
928 apply(auto simp add: image_def LV_def elim!: Prf_elims) |
1047 apply(auto simp add: LV_def) |
929 apply blast |
1048 apply(auto elim!: Prf_elims) |
930 apply(case_tac vs) |
1049 apply(auto simp add: Stars_Append_def) |
|
1050 apply(rule_tac x="vs1" in exI) |
|
1051 apply(rule_tac x="vs2" in exI) |
|
1052 apply(auto) |
|
1053 using Prf.intros(6) apply(auto) |
|
1054 apply(rule_tac x="length vs2" in bexI) |
|
1055 thm Prf.intros |
|
1056 apply(subst append.simps(1)[symmetric]) |
|
1057 apply(rule Prf.intros) |
|
1058 apply(auto)[1] |
|
1059 apply(auto)[1] |
|
1060 apply(simp) |
|
1061 apply(simp) |
|
1062 apply(rule_tac x="vs" in exI) |
|
1063 apply(rule_tac x="[]" in exI) |
931 apply(auto) |
1064 apply(auto) |
932 done |
1065 by (metis Prf.intros(9) append_Nil atMost_iff empty_iff le_imp_less_Suc less_antisym list.set(1) nth_mem zero_le) |
|
1066 |
|
1067 lemma LV_NMTIMES_6: |
|
1068 assumes "\<forall>s. finite (LV r s)" |
|
1069 shows "finite (LV (NMTIMES r n m) s)" |
|
1070 apply(rule finite_subset) |
|
1071 apply(rule LV_NMTIMES_5) |
|
1072 apply(rule finite_Stars_Append) |
|
1073 apply(rule LV_STAR_finite) |
|
1074 apply(rule assms) |
|
1075 apply(rule finite_UN_I) |
|
1076 apply(auto) |
|
1077 by (simp add: assms finite_Stars_Pow ttty) |
|
1078 |
933 |
1079 |
934 |
|
935 |
|
936 lemma LV_NTIMES_empty_finite: |
|
937 assumes "finite (LV r [])" |
|
938 shows "finite (LV (NTIMES r n) [])" |
|
939 using assms |
|
940 apply - |
|
941 apply(rule finite_subset) |
|
942 apply(rule test) |
|
943 apply(rule finite_imageI) |
|
944 apply(rule finite_list) |
|
945 apply(simp) |
|
946 done |
|
947 |
|
948 lemma LV_NTIMES_STAR: |
|
949 "LV (NTIMES r n) s \<subseteq> LV (STAR r) s" |
|
950 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
|
951 apply(rule Prf.intros) |
|
952 oops |
|
953 |
|
954 lemma LV_FROMNTIMES_STAR: |
|
955 "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s" |
|
956 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
|
957 oops |
|
958 |
|
959 lemma LV_finite: |
1080 lemma LV_finite: |
960 shows "finite (LV r s)" |
1081 shows "finite (LV r s)" |
961 proof(induct r arbitrary: s) |
1082 proof(induct r arbitrary: s) |
962 case (ZERO s) |
1083 case (ZERO s) |
963 show "finite (LV ZERO s)" by (simp add: LV_simps) |
1084 show "finite (LV ZERO s)" by (simp add: LV_simps) |
1018 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
1149 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
1019 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
1150 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
1020 \<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> |
1151 \<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> |
1021 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1152 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
1022 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
1153 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
1023 |
1154 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
|
1155 \<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 (NTIMES r (n - 1)))\<rbrakk> |
|
1156 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)" |
|
1157 | Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
|
1158 \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs" |
|
1159 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
|
1160 \<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 (UPNTIMES r (n - 1)))\<rbrakk> |
|
1161 \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r n \<rightarrow> Stars (v # vs)" |
|
1162 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
|
1163 | Posix_FROMNTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
|
1164 \<Longrightarrow> [] \<in> FROMNTIMES r n \<rightarrow> Stars vs" |
|
1165 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
|
1166 \<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 - 1)))\<rbrakk> |
|
1167 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (v # vs)" |
|
1168 | Posix_NMTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n; n \<le> m\<rbrakk> |
|
1169 \<Longrightarrow> [] \<in> NMTIMES r n m \<rightarrow> Stars vs" |
|
1170 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v \<noteq> []; n \<le> m; |
|
1171 \<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> |
|
1172 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
|
1173 |
1024 inductive_cases Posix_elims: |
1174 inductive_cases Posix_elims: |
1025 "s \<in> ZERO \<rightarrow> v" |
1175 "s \<in> ZERO \<rightarrow> v" |
1026 "s \<in> ONE \<rightarrow> v" |
1176 "s \<in> ONE \<rightarrow> v" |
1027 "s \<in> CHAR c \<rightarrow> v" |
1177 "s \<in> CHAR c \<rightarrow> v" |
1028 "s \<in> ALT r1 r2 \<rightarrow> v" |
1178 "s \<in> ALT r1 r2 \<rightarrow> v" |
1029 "s \<in> SEQ r1 r2 \<rightarrow> v" |
1179 "s \<in> SEQ r1 r2 \<rightarrow> v" |
1030 "s \<in> STAR r \<rightarrow> v" |
1180 "s \<in> STAR r \<rightarrow> v" |
1031 |
1181 "s \<in> NTIMES r n \<rightarrow> v" |
|
1182 "s \<in> UPNTIMES r n \<rightarrow> v" |
|
1183 "s \<in> FROMNTIMES r n \<rightarrow> v" |
|
1184 "s \<in> NMTIMES r n m \<rightarrow> v" |
|
1185 |
1032 lemma Posix1: |
1186 lemma Posix1: |
1033 assumes "s \<in> r \<rightarrow> v" |
1187 assumes "s \<in> r \<rightarrow> v" |
1034 shows "s \<in> L r" "flat v = s" |
1188 shows "s \<in> L r" "flat v = s" |
1035 using assms |
1189 using assms |
1036 by (induct s r v rule: Posix.induct) |
1190 apply(induct s r v rule: Posix.induct) |
1037 (auto simp add: Sequ_def) |
1191 apply(auto simp add: Sequ_def)[18] |
1038 |
1192 apply(case_tac n) |
|
1193 apply(simp) |
|
1194 apply(simp add: Sequ_def) |
|
1195 apply(auto)[1] |
|
1196 apply(simp) |
|
1197 apply(clarify) |
|
1198 apply(rule_tac x="Suc x" in bexI) |
|
1199 apply(simp add: Sequ_def) |
|
1200 apply(auto)[5] |
|
1201 using nth_mem nullable.simps(9) nullable_correctness apply auto[1] |
|
1202 apply simp |
|
1203 apply(simp) |
|
1204 apply(clarify) |
|
1205 apply(rule_tac x="Suc x" in bexI) |
|
1206 apply(simp add: Sequ_def) |
|
1207 apply(auto)[3] |
|
1208 apply(simp) |
|
1209 apply fastforce |
|
1210 apply(simp) |
|
1211 apply(simp) |
|
1212 apply(clarify) |
|
1213 apply(rule_tac x="Suc x" in bexI) |
|
1214 apply(auto simp add: Sequ_def)[2] |
|
1215 apply(simp) |
|
1216 done |
|
1217 |
1039 text {* |
1218 text {* |
1040 Our Posix definition determines a unique value. |
1219 Our Posix definition determines a unique value. |
1041 *} |
1220 *} |
|
1221 |
|
1222 lemma List_eq_zipI: |
|
1223 assumes "\<forall>(v1, v2) \<in> set (zip vs1 vs2). v1 = v2" |
|
1224 and "length vs1 = length vs2" |
|
1225 shows "vs1 = vs2" |
|
1226 using assms |
|
1227 apply(induct vs1 arbitrary: vs2) |
|
1228 apply(case_tac vs2) |
|
1229 apply(simp) |
|
1230 apply(simp) |
|
1231 apply(case_tac vs2) |
|
1232 apply(simp) |
|
1233 apply(simp) |
|
1234 done |
1042 |
1235 |
1043 lemma Posix_determ: |
1236 lemma Posix_determ: |
1044 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
1237 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
1045 shows "v1 = v2" |
1238 shows "v1 = v2" |
1046 using assms |
1239 using assms |
1102 ultimately show "Stars (v # vs) = v2" by auto |
1295 ultimately show "Stars (v # vs) = v2" by auto |
1103 next |
1296 next |
1104 case (Posix_STAR2 r v2) |
1297 case (Posix_STAR2 r v2) |
1105 have "[] \<in> STAR r \<rightarrow> v2" by fact |
1298 have "[] \<in> STAR r \<rightarrow> v2" by fact |
1106 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
1299 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
1300 next |
|
1301 case (Posix_NTIMES2 vs r n v2) |
|
1302 then show "Stars vs = v2" |
|
1303 apply(erule_tac Posix_elims) |
|
1304 apply(auto) |
|
1305 apply (simp add: Posix1(2)) |
|
1306 apply(rule List_eq_zipI) |
|
1307 apply(auto) |
|
1308 by (meson in_set_zipE) |
|
1309 next |
|
1310 case (Posix_NTIMES1 s1 r v s2 n vs v2) |
|
1311 have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2" |
|
1312 "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1313 "\<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 (NTIMES r (n - 1 )))" by fact+ |
|
1314 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
|
1315 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1316 using Posix1(1) apply fastforce |
|
1317 apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2) |
|
1318 using Posix1(2) by blast |
|
1319 moreover |
|
1320 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1321 "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1322 ultimately show "Stars (v # vs) = v2" by auto |
|
1323 next |
|
1324 case (Posix_UPNTIMES1 s1 r v s2 n vs v2) |
|
1325 have "(s1 @ s2) \<in> UPNTIMES r n \<rightarrow> v2" |
|
1326 "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1327 "\<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 (UPNTIMES r (n - 1 )))" by fact+ |
|
1328 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
|
1329 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1330 using Posix1(1) apply fastforce |
|
1331 apply (metis One_nat_def Posix1(1) Posix_UPNTIMES1.hyps(7) append.right_neutral append_self_conv2) |
|
1332 using Posix1(2) by blast |
|
1333 moreover |
|
1334 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1335 "\<And>v2. s2 \<in> UPNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1336 ultimately show "Stars (v # vs) = v2" by auto |
|
1337 next |
|
1338 case (Posix_UPNTIMES2 r n v2) |
|
1339 then show "Stars [] = v2" |
|
1340 apply(erule_tac Posix_elims) |
|
1341 apply(auto) |
|
1342 by (simp add: Posix1(2)) |
|
1343 next |
|
1344 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
|
1345 have "(s1 @ s2) \<in> FROMNTIMES r n \<rightarrow> v2" |
|
1346 "s1 \<in> r \<rightarrow> v" "s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1347 "\<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 - 1 )))" by fact+ |
|
1348 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
|
1349 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1350 using Posix1(1) Posix1(2) apply blast |
|
1351 apply(drule_tac x="v" in meta_spec) |
|
1352 apply(drule_tac x="vs" in meta_spec) |
|
1353 apply(simp) |
|
1354 apply(drule meta_mp) |
|
1355 apply(case_tac n) |
|
1356 apply(simp) |
|
1357 apply(rule conjI) |
|
1358 apply (smt L.simps(9) One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps Suc_mono Suc_pred UN_E append.right_neutral append_Nil lessI less_antisym list.size(3) nat.simps(3) neq0_conv not_less_eq val.inject(5)) |
|
1359 apply(rule List_eq_zipI) |
|
1360 apply(auto)[1] |
|
1361 sorry |
|
1362 moreover |
|
1363 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1364 "\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1365 ultimately show "Stars (v # vs) = v2" by auto |
|
1366 next |
|
1367 case (Posix_FROMNTIMES2 vs r n v2) |
|
1368 then show "Stars vs = v2" |
|
1369 apply(erule_tac Posix_elims) |
|
1370 apply(auto) |
|
1371 apply(rule List_eq_zipI) |
|
1372 apply(auto) |
|
1373 apply(meson in_set_zipE) |
|
1374 by (simp add: Posix1(2)) |
|
1375 next |
|
1376 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
|
1377 then show "Stars (v # vs) = v2" |
|
1378 sorry |
|
1379 next |
|
1380 case (Posix_NMTIMES2 vs r n m v2) |
|
1381 then show "Stars vs = v2" |
|
1382 sorry |
1107 qed |
1383 qed |
1108 |
1384 |
1109 |
1385 |
1110 text {* |
1386 text {* |
1111 Our POSIX value is a lexical value. |
1387 Our POSIX value is a lexical value. |
1114 lemma Posix_LV: |
1390 lemma Posix_LV: |
1115 assumes "s \<in> r \<rightarrow> v" |
1391 assumes "s \<in> r \<rightarrow> v" |
1116 shows "v \<in> LV r s" |
1392 shows "v \<in> LV r s" |
1117 using assms unfolding LV_def |
1393 using assms unfolding LV_def |
1118 apply(induct rule: Posix.induct) |
1394 apply(induct rule: Posix.induct) |
1119 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
1395 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[7] |
1120 done |
1396 defer |
1121 |
1397 defer |
|
1398 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2] |
|
1399 apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq) |
|
1400 prefer 4 |
|
1401 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[1] |
|
1402 apply(subst append.simps(2)[symmetric]) |
|
1403 apply(rule Prf.intros) |
|
1404 apply(auto) |
|
1405 prefer 4 |
|
1406 apply (metis Prf.intros(8) append_Nil empty_iff list.set(1)) |
|
1407 apply(erule Posix_elims) |
|
1408 apply(auto) |
|
1409 apply(rule_tac t="v # vsa" and s = "[v] @ vsa" in subst) |
|
1410 apply(simp) |
|
1411 apply(rule Prf.intros) |
|
1412 apply(simp) |
|
1413 apply(auto)[1] |
|
1414 apply(auto simp add: Sequ_def intro: Prf.intros elim: Prf_elims)[1] |
|
1415 apply(simp) |
|
1416 apply(rotate_tac 4) |
|
1417 apply(erule Prf_elims) |
|
1418 apply(auto) |
|
1419 apply(case_tac n) |
|
1420 apply(simp) |
|
1421 |
|
1422 apply(subst append.simps(2)[symmetric]) |
|
1423 apply(rule Prf.intros) |
|
1424 apply(auto) |
|
1425 apply(rule Prf.intros(10)) |
|
1426 apply(auto) |
|
1427 apply (metis Prf.intros(11) append_Nil empty_iff list.set(1)) |
|
1428 apply(rotate_tac 6) |
|
1429 apply(erule Prf_elims) |
|
1430 apply(simp) |
|
1431 apply(subst append.simps(2)[symmetric]) |
|
1432 apply(rule Prf.intros) |
|
1433 apply(auto) |
|
1434 apply(rule_tac t="v # vsa" and s = "(v # vsa) @ []" in subst) |
|
1435 apply(simp) |
|
1436 apply(simp add: Prf.intros(12)) |
|
1437 done |
|
1438 |
|
1439 lemma FROMNTIMES_0: |
|
1440 assumes "s \<in> FROMNTIMES r 0 \<rightarrow> v" |
|
1441 shows "s = [] \<and> v = Stars []" |
|
1442 using assms |
|
1443 apply(erule_tac Posix_elims) |
|
1444 apply(auto) |
|
1445 done |
|
1446 |
|
1447 lemma FROMNTIMES_der_0: |
|
1448 shows "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)" |
|
1449 by(simp) |
|
1450 |
1122 end |
1451 end |