491 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
491 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
492 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
492 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
493 length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n" |
493 length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n" |
494 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
494 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
495 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
495 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
496 length (vs1 @ vs2) \<ge> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n" |
496 length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n" |
|
497 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs > n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : FROMNTIMES r n" |
497 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
498 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
498 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
499 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
499 length (vs1 @ vs2) \<ge> n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m" |
500 length (vs1 @ vs2) = n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m" |
500 |
501 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; |
|
502 length vs > n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : NMTIMES r n m" |
|
503 |
|
504 |
501 inductive_cases Prf_elims: |
505 inductive_cases Prf_elims: |
502 "\<Turnstile> v : ZERO" |
506 "\<Turnstile> v : ZERO" |
503 "\<Turnstile> v : SEQ r1 r2" |
507 "\<Turnstile> v : SEQ r1 r2" |
504 "\<Turnstile> v : ALT r1 r2" |
508 "\<Turnstile> v : ALT r1 r2" |
505 "\<Turnstile> v : ONE" |
509 "\<Turnstile> v : ONE" |
600 using assms |
604 using assms |
601 apply(induct) |
605 apply(induct) |
602 apply(auto simp add: Sequ_def Star_concat Pow_flats) |
606 apply(auto simp add: Sequ_def Star_concat Pow_flats) |
603 apply(meson Pow_flats atMost_iff) |
607 apply(meson Pow_flats atMost_iff) |
604 using Pow_flats_appends apply blast |
608 using Pow_flats_appends apply blast |
605 apply(meson Pow_flats_appends atLeast_iff) |
609 using Pow_flats_appends apply blast |
|
610 apply (meson Pow_flats atLeast_iff less_imp_le) |
|
611 apply(rule_tac x="length vs1 + length vs2" in bexI) |
606 apply(meson Pow_flats_appends atLeastAtMost_iff) |
612 apply(meson Pow_flats_appends atLeastAtMost_iff) |
|
613 apply(simp) |
|
614 apply(meson Pow_flats atLeastAtMost_iff less_or_eq_imp_le) |
607 done |
615 done |
608 |
616 |
609 lemma L_flat_Prf2: |
617 lemma L_flat_Prf2: |
610 assumes "s \<in> L r" |
618 assumes "s \<in> L r" |
611 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
619 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
653 using Prf.intros(8) flat_Stars by blast |
661 using Prf.intros(8) flat_Stars by blast |
654 next |
662 next |
655 case (FROMNTIMES r n) |
663 case (FROMNTIMES r n) |
656 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
664 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
657 have "s \<in> L (FROMNTIMES r n)" by fact |
665 have "s \<in> L (FROMNTIMES r n)" by fact |
658 then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m" |
666 then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m" |
659 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
667 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
660 using Pow_cstring by auto blast |
668 using Pow_cstring by force |
661 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m" |
669 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m" |
662 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
670 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
663 using IH flats_cval |
671 using IH flats_cval |
664 apply - |
672 apply - |
665 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
673 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
671 apply(drule_tac x="vs1" in meta_spec) |
679 apply(drule_tac x="vs1" in meta_spec) |
672 apply(drule_tac x="vs2" in meta_spec) |
680 apply(drule_tac x="vs2" in meta_spec) |
673 apply(simp) |
681 apply(simp) |
674 done |
682 done |
675 then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s" |
683 then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s" |
676 using Prf.intros(9) flat_Stars by blast |
684 apply(case_tac "length vs1 \<le> n") |
|
685 apply(rule_tac x="Stars (vs1 @ take (n - length vs1) vs2)" in exI) |
|
686 apply(simp) |
|
687 apply(subgoal_tac "flats (take (n - length vs1) vs2) = []") |
|
688 prefer 2 |
|
689 apply (meson flats_empty in_set_takeD) |
|
690 apply(clarify) |
|
691 apply(rule conjI) |
|
692 apply(rule Prf.intros) |
|
693 apply(simp) |
|
694 apply (meson in_set_takeD) |
|
695 apply(simp) |
|
696 apply(simp) |
|
697 apply (simp add: flats_empty) |
|
698 apply(rule_tac x="Stars vs1" in exI) |
|
699 apply(simp) |
|
700 apply(rule conjI) |
|
701 apply(rule Prf.intros(10)) |
|
702 apply(auto) |
|
703 done |
677 next |
704 next |
678 case (NMTIMES r n m) |
705 case (NMTIMES r n m) |
679 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
706 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
680 have "s \<in> L (NMTIMES r n m)" by fact |
707 have "s \<in> L (NMTIMES r n m)" by fact |
681 then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k" "k \<le> m" |
708 then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k" "k \<le> m" |
738 unfolding LV_def |
765 unfolding LV_def |
739 apply(auto intro: Prf.intros elim: Prf.cases) |
766 apply(auto intro: Prf.intros elim: Prf.cases) |
740 done |
767 done |
741 |
768 |
742 abbreviation |
769 abbreviation |
743 "Prefixes s \<equiv> {s'. prefixeq s' s}" |
770 "Prefixes s \<equiv> {s'. prefix s' s}" |
744 |
771 |
745 abbreviation |
772 abbreviation |
746 "Suffixes s \<equiv> {s'. suffixeq s' s}" |
773 "Suffixes s \<equiv> {s'. suffix s' s}" |
747 |
774 |
748 abbreviation |
775 abbreviation |
749 "SSuffixes s \<equiv> {s'. suffix s' s}" |
776 "SSuffixes s \<equiv> {s'. strict_suffix s' s}" |
750 |
777 |
751 lemma Suffixes_cons [simp]: |
778 lemma Suffixes_cons [simp]: |
752 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
779 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
753 by (auto simp add: suffixeq_def Cons_eq_append_conv) |
780 by (auto simp add: suffix_def Cons_eq_append_conv) |
754 |
781 |
755 |
782 |
756 lemma finite_Suffixes: |
783 lemma finite_Suffixes: |
757 shows "finite (Suffixes s)" |
784 shows "finite (Suffixes s)" |
758 by (induct s) (simp_all) |
785 by (induct s) (simp_all) |
759 |
786 |
760 lemma finite_SSuffixes: |
787 lemma finite_SSuffixes: |
761 shows "finite (SSuffixes s)" |
788 shows "finite (SSuffixes s)" |
762 proof - |
789 proof - |
763 have "SSuffixes s \<subseteq> Suffixes s" |
790 have "SSuffixes s \<subseteq> Suffixes s" |
764 unfolding suffix_def suffixeq_def by auto |
791 unfolding suffix_def strict_suffix_def by auto |
765 then show "finite (SSuffixes s)" |
792 then show "finite (SSuffixes s)" |
766 using finite_Suffixes finite_subset by blast |
793 using finite_Suffixes finite_subset by blast |
767 qed |
794 qed |
768 |
795 |
769 lemma finite_Prefixes: |
796 lemma finite_Prefixes: |
772 have "finite (Suffixes (rev s))" |
799 have "finite (Suffixes (rev s))" |
773 by (rule finite_Suffixes) |
800 by (rule finite_Suffixes) |
774 then have "finite (rev ` Suffixes (rev s))" by simp |
801 then have "finite (rev ` Suffixes (rev s))" by simp |
775 moreover |
802 moreover |
776 have "rev ` (Suffixes (rev s)) = Prefixes s" |
803 have "rev ` (Suffixes (rev s)) = Prefixes s" |
777 unfolding suffixeq_def prefixeq_def image_def |
804 unfolding suffix_def prefix_def image_def |
778 by (auto)(metis rev_append rev_rev_ident)+ |
805 by (auto)(metis rev_append rev_rev_ident)+ |
779 ultimately show "finite (Prefixes s)" by simp |
806 ultimately show "finite (Prefixes s)" by simp |
780 qed |
807 qed |
781 |
808 |
782 lemma LV_STAR_finite: |
809 lemma LV_STAR_finite: |
784 shows "finite (LV (STAR r) s)" |
811 shows "finite (LV (STAR r) s)" |
785 proof(induct s rule: length_induct) |
812 proof(induct s rule: length_induct) |
786 fix s::"char list" |
813 fix s::"char list" |
787 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
814 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
788 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
815 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
789 by (auto simp add: suffix_def) |
816 by (auto simp add: strict_suffix_def) |
790 def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" |
817 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
791 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'" |
818 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
792 def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
819 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
793 have "finite S1" using assms |
820 have "finite S1" using assms |
794 unfolding S1_def by (simp_all add: finite_Prefixes) |
821 unfolding S1_def by (simp_all add: finite_Prefixes) |
795 moreover |
822 moreover |
796 with IH have "finite S2" unfolding S2_def |
823 with IH have "finite S2" unfolding S2_def |
797 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
824 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
798 ultimately |
825 ultimately |
799 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
826 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
800 moreover |
827 moreover |
801 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
828 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
802 unfolding S1_def S2_def f_def |
829 unfolding S1_def S2_def f_def |
803 unfolding LV_def image_def prefixeq_def suffix_def |
830 unfolding LV_def image_def prefix_def strict_suffix_def |
|
831 apply(auto) |
|
832 apply(case_tac x) |
804 apply(auto elim: Prf_elims) |
833 apply(auto elim: Prf_elims) |
805 apply(erule Prf_elims) |
834 apply(erule Prf_elims) |
806 apply(auto) |
835 apply(auto) |
807 apply(case_tac vs) |
836 apply(case_tac vs) |
808 apply(auto intro: Prf.intros) |
837 apply(auto intro: Prf.intros) |
809 done |
838 apply(rule exI) |
|
839 apply(rule conjI) |
|
840 apply(rule_tac x="flat a" in exI) |
|
841 apply(rule conjI) |
|
842 apply(rule_tac x="flats list" in exI) |
|
843 apply(simp) |
|
844 apply(blast) |
|
845 using Prf.intros(6) by blast |
810 ultimately |
846 ultimately |
811 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
847 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
812 qed |
848 qed |
813 |
849 |
814 lemma LV_UPNTIMES_STAR: |
850 lemma LV_UPNTIMES_STAR: |
815 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
851 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
816 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
852 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
817 |
853 |
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 |
854 |
853 lemma LV_NTIMES_0: |
855 lemma LV_NTIMES_0: |
854 shows "LV (NTIMES r 0) s \<subseteq> {Stars []}" |
856 shows "LV (NTIMES r 0) s \<subseteq> {Stars []}" |
855 unfolding LV_def |
857 unfolding LV_def |
856 apply(auto elim: Prf_elims) |
858 apply(auto elim: Prf_elims) |
896 apply(auto) |
898 apply(auto) |
897 done |
899 done |
898 |
900 |
899 thm card_cartesian_product |
901 thm card_cartesian_product |
900 |
902 |
901 lemma LV_empty_finite: |
903 lemma finite_list: |
902 shows "card (LV (NTIMES r n) []) \<le> ((card (LV r [])) ^ n)" |
904 assumes "finite A" |
903 apply(induct n arbitrary:) |
905 shows "finite {vs. \<forall>v\<in>set vs. v \<in> A \<and> length vs = n}" |
904 using LV_NTIMES_0 |
906 apply(induct n) |
905 apply (metis card_empty card_insert_disjoint card_mono empty_iff finite.emptyI finite.insertI nat_power_eq_Suc_0_iff) |
907 apply(simp) |
906 apply(simp add: LV_NTIMES_3) |
908 apply (smt Collect_cong empty_iff finite.emptyI finite.insertI |
907 apply(subst card_image) |
909 in_listsI list.set(1) lists_empty mem_Collect_eq singleton_conv2) |
908 apply(simp add: inj_on_def) |
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) |
909 apply(subst card_cartesian_product) |
911 apply(auto simp add: image_def)[1] |
910 apply(subst card_vimage_inj) |
912 apply(case_tac x) |
911 apply(simp add: inj_on_def) |
913 apply(simp) |
912 apply(auto simp add: LV_def elim: Prf_elims)[1] |
914 apply(simp) |
913 using nat_mult_le_cancel_disj by blast |
915 apply(simp) |
914 |
916 apply(rule finite_imageI) |
|
917 using assms |
|
918 apply(simp) |
|
919 done |
|
920 |
|
921 lemma test: |
|
922 "LV (NTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}" |
|
923 apply(auto simp add: LV_def elim: Prf_elims) |
|
924 done |
|
925 |
|
926 lemma test3: |
|
927 "LV (FROMNTIMES r n) [] \<subseteq> Stars ` {vs. \<forall>v \<in> set vs. v \<in> LV r [] \<and> length vs = n}" |
|
928 apply(auto simp add: image_def LV_def elim!: Prf_elims) |
|
929 apply blast |
|
930 apply(case_tac vs) |
|
931 apply(auto) |
|
932 done |
|
933 |
|
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 |
915 lemma LV_NTIMES_STAR: |
948 lemma LV_NTIMES_STAR: |
916 "LV (NTIMES r n) s \<subseteq> LV (STAR r) s" |
949 "LV (NTIMES r n) s \<subseteq> LV (STAR r) s" |
917 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
950 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
918 apply(rule Prf.intros) |
951 apply(rule Prf.intros) |
919 oops |
952 oops |
937 next |
970 next |
938 case (ALT r1 r2 s) |
971 case (ALT r1 r2 s) |
939 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
972 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
940 next |
973 next |
941 case (SEQ r1 r2 s) |
974 case (SEQ r1 r2 s) |
942 def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2" |
975 define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2" |
943 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'" |
976 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'" |
944 def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'" |
977 define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'" |
945 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
978 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
946 then have "finite S1" "finite S2" unfolding S1_def S2_def |
979 then have "finite S1" "finite S2" unfolding S1_def S2_def |
947 by (simp_all add: finite_Prefixes finite_Suffixes) |
980 by (simp_all add: finite_Prefixes finite_Suffixes) |
948 moreover |
981 moreover |
949 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
982 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
950 unfolding f_def S1_def S2_def |
983 unfolding f_def S1_def S2_def |
951 unfolding LV_def image_def prefixeq_def suffixeq_def |
984 unfolding LV_def image_def prefix_def suffix_def |
952 by (auto elim: Prf.cases) |
985 apply (auto elim!: Prf_elims) |
|
986 by (metis (mono_tags, lifting) mem_Collect_eq) |
953 ultimately |
987 ultimately |
954 show "finite (LV (SEQ r1 r2) s)" |
988 show "finite (LV (SEQ r1 r2) s)" |
955 by (simp add: finite_subset) |
989 by (simp add: finite_subset) |
956 next |
990 next |
957 case (STAR r s) |
991 case (STAR r s) |