811 |
813 |
812 lemma LV_UPNTIMES_STAR: |
814 lemma LV_UPNTIMES_STAR: |
813 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
815 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
814 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
816 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
815 |
817 |
|
818 (* |
|
819 lemma LV_NTIMES_finite: |
|
820 assumes "\<forall>s. finite (LV r s)" |
|
821 shows "finite (LV (NTIMES r n) s)" |
|
822 proof(induct s rule: length_induct) |
|
823 fix s::"char list" |
|
824 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (NTIMES r n) s')" |
|
825 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (NTIMES r n) s')" |
|
826 by (auto simp add: suffix_def) |
|
827 def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" |
|
828 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'" |
|
829 def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (NTIMES r n) s2)" |
|
830 have "finite S1" using assms |
|
831 unfolding S1_def by (simp_all add: finite_Prefixes) |
|
832 moreover |
|
833 with IH have "finite S2" unfolding S2_def |
|
834 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
|
835 ultimately |
|
836 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
|
837 moreover |
|
838 have "LV (NTIMES r n) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
|
839 unfolding S1_def S2_def f_def |
|
840 unfolding LV_def image_def prefixeq_def suffix_def |
|
841 apply(auto elim: Prf_elims) |
|
842 apply(erule Prf_elims) |
|
843 apply(auto) |
|
844 apply(case_tac vs1) |
|
845 apply(auto intro: Prf.intros) |
|
846 |
|
847 done |
|
848 ultimately |
|
849 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
|
850 qed |
|
851 *) |
|
852 |
|
853 lemma LV_NTIMES_0: |
|
854 shows "LV (NTIMES r 0) s \<subseteq> {Stars []}" |
|
855 unfolding LV_def |
|
856 apply(auto elim: Prf_elims) |
|
857 done |
|
858 |
|
859 lemma LV_NTIMES_1: |
|
860 shows "LV (NTIMES r 1) s \<subseteq> (\<lambda>v. Stars [v]) ` (LV r s)" |
|
861 unfolding LV_def |
|
862 apply(auto elim!: Prf_elims) |
|
863 apply(case_tac vs1) |
|
864 apply(simp) |
|
865 apply(case_tac vs2) |
|
866 apply(simp) |
|
867 apply(simp) |
|
868 apply(simp) |
|
869 done |
|
870 |
|
871 lemma LV_NTIMES_2: |
|
872 shows "LV (NTIMES r 2) [] \<subseteq> (\<lambda>(v1,v2). Stars [v1,v2]) ` (LV r [] \<times> LV r [])" |
|
873 unfolding LV_def |
|
874 apply(auto elim!: Prf_elims simp add: image_def) |
|
875 apply(case_tac vs1) |
|
876 apply(auto) |
|
877 apply(case_tac vs2) |
|
878 apply(auto) |
|
879 apply(case_tac list) |
|
880 apply(auto) |
|
881 done |
|
882 |
|
883 lemma LV_NTIMES_3: |
|
884 shows "LV (NTIMES r (Suc n)) [] = (\<lambda>(v,vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))" |
|
885 unfolding LV_def |
|
886 apply(auto elim!: Prf_elims simp add: image_def) |
|
887 apply(case_tac vs1) |
|
888 apply(auto) |
|
889 apply(case_tac vs2) |
|
890 apply(auto) |
|
891 apply(subst append.simps(1)[symmetric]) |
|
892 apply(rule Prf.intros) |
|
893 apply(auto) |
|
894 apply(subst append.simps(1)[symmetric]) |
|
895 apply(rule Prf.intros) |
|
896 apply(auto) |
|
897 done |
|
898 |
|
899 thm card_cartesian_product |
|
900 |
|
901 lemma LV_empty_finite: |
|
902 shows "card (LV (NTIMES r n) []) \<le> ((card (LV r [])) ^ n)" |
|
903 apply(induct n arbitrary:) |
|
904 using LV_NTIMES_0 |
|
905 apply (metis card_empty card_insert_disjoint card_mono empty_iff finite.emptyI finite.insertI nat_power_eq_Suc_0_iff) |
|
906 apply(simp add: LV_NTIMES_3) |
|
907 apply(subst card_image) |
|
908 apply(simp add: inj_on_def) |
|
909 apply(subst card_cartesian_product) |
|
910 apply(subst card_vimage_inj) |
|
911 apply(simp add: inj_on_def) |
|
912 apply(auto simp add: LV_def elim: Prf_elims)[1] |
|
913 using nat_mult_le_cancel_disj by blast |
|
914 |
|
915 lemma LV_NTIMES_STAR: |
|
916 "LV (NTIMES r n) s \<subseteq> LV (STAR r) s" |
|
917 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
|
918 apply(rule Prf.intros) |
|
919 oops |
|
920 |
816 lemma LV_FROMNTIMES_STAR: |
921 lemma LV_FROMNTIMES_STAR: |
817 "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s" |
922 "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s" |
818 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
923 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
819 oops |
924 oops |
820 |
925 |
850 by (simp add: finite_subset) |
955 by (simp add: finite_subset) |
851 next |
956 next |
852 case (STAR r s) |
957 case (STAR r s) |
853 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
958 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
854 next |
959 next |
855 case (NTIMES r n s) |
960 case (UPNTIMES r n s) |
856 have "\<And>s. finite (LV r s)" by fact |
961 have "\<And>s. finite (LV r s)" by fact |
857 then show "finite (LV (NTIMES r n) s)" |
962 then show "finite (LV (UPNTIMES r n) s)" |
858 apply(simp add: LV_def) |
963 by (meson LV_STAR_finite LV_UPNTIMES_STAR rev_finite_subset) |
|
964 next |
|
965 case (FROMNTIMES r n s) |
|
966 have "\<And>s. finite (LV r s)" by fact |
|
967 then show "finite (LV (FROMNTIMES r n) s)" |
|
968 |
859 qed |
969 qed |
860 |
970 |
861 |
971 |
862 |
972 |
863 section {* Our POSIX Definition *} |
973 section {* Our POSIX Definition *} |