equal
deleted
inserted
replaced
883 shows "finite (LV (STAR r) s)" |
883 shows "finite (LV (STAR r) s)" |
884 proof(induct s rule: length_induct) |
884 proof(induct s rule: length_induct) |
885 fix s::"char list" |
885 fix s::"char list" |
886 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
886 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
887 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
887 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
888 by (auto simp add: strict_suffix_def) |
888 apply(auto simp add: strict_suffix_def suffix_def) |
|
889 by force |
889 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
890 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
890 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
891 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
891 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2" |
892 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. LV (STAR r) s2" |
892 have "finite S1" using assms |
893 have "finite S1" using assms |
893 unfolding S1_def by (simp_all add: finite_Prefixes) |
894 unfolding S1_def by (simp_all add: finite_Prefixes) |
910 apply(case_tac vs) |
911 apply(case_tac vs) |
911 apply(auto intro: Prf.intros) |
912 apply(auto intro: Prf.intros) |
912 apply(rule exI) |
913 apply(rule exI) |
913 apply(rule conjI) |
914 apply(rule conjI) |
914 apply(rule_tac x="flats list" in exI) |
915 apply(rule_tac x="flats list" in exI) |
915 apply(rule conjI) |
916 apply(rule conjI) |
916 apply(rule_tac x="flat a" in exI) |
917 apply(simp add: suffix_def) |
917 apply(simp) |
|
918 apply(blast) |
918 apply(blast) |
919 using Prf.intros(6) flat_Stars by blast |
919 using Prf.intros(6) flat_Stars by blast |
920 ultimately |
920 ultimately |
921 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
921 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
922 qed |
922 qed |