theory Myhill imports Myhill_1beginsection {* Direction: @{text "regular language \<Rightarrow>finite partition"} *}subsection {* The scheme for this direction *}text {* The following convenient notation @{text "x \<approx>Lang y"} means: string @{text "x"} and @{text "y"} are equivalent with respect to language @{text "Lang"}. *}definition str_eq ("_ \<approx>_ _")where "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"text {* The basic idea to show the finiteness of the partition induced by relation @{text "\<approx>Lang"} is to attach a tag @{text "tag(x)"} to every string @{text "x"}, the set of tags are carfully choosen, so that the range of tagging function @{text "tag"} (denoted @{text "range(tag)"}) is finite. If strings with the same tag are equivlent with respect @{text "\<approx>Lang"}, i.e. @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} (this property is named `injectivity' in the following), then it can be proved that: the partition given rise by @{text "(\<approx>Lang)"} is finite. There are two arguments for this. The first goes as the following: \begin{enumerate} \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"} (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}). \item It is shown that: if the range of @{text "tag"} is finite, the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}). \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"} (expressed as @{text "R1 \<subseteq> R2"}), and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"} is finite as well (lemma @{text "refined_partition_finite"}). \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}. \item Combining the points above, we have: the partition induced by language @{text "Lang"} is finite (lemma @{text "tag_finite_imageD"}). \end{enumerate}*}definition f_eq_rel ("=_=")where "(=f=) = {(x, y) | x y. f x = f y}"lemma equiv_f_eq_rel:"equiv UNIV (=f=)" by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)" by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)lemma finite_eq_f_rel: assumes rng_fnt: "finite (range tag)" shows "finite (UNIV // (=tag=))"proof - let "?f" = "op ` tag" and ?A = "(UNIV // (=tag=))" show ?thesis proof (rule_tac f = "?f" and A = ?A in finite_imageD) -- {* The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: *} show "finite (?f ` ?A)" proof - have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def) moreover from rng_fnt have "finite (Pow (range tag))" by simp ultimately have "finite (range ?f)" by (auto simp only:image_def intro:finite_subset) from finite_range_image [OF this] show ?thesis . qed next -- {* The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}: *} show "inj_on ?f ?A" proof- { fix X Y assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and tag_eq: "?f X = ?f Y" have "X = Y" proof - from X_in Y_in tag_eq obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def f_eq_rel_def apply simp by blast with X_in Y_in show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def) qed } thus ?thesis unfolding inj_on_def by auto qed qedqedlemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)" by (rule finite_subset [of _ B], auto)lemma refined_partition_finite: fixes R1 R2 A assumes fnt: "finite (A // R1)" and refined: "R1 \<subseteq> R2" and eq1: "equiv A R1" and eq2: "equiv A R2" shows "finite (A // R2)"proof - let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" and ?A = "(A // R2)" and ?B = "(A // R1)" show ?thesis proof(rule_tac f = ?f and A = ?A in finite_imageD) show "finite (?f ` ?A)" proof(rule finite_subset [of _ "Pow ?B"]) from fnt show "finite (Pow (A // R1))" by simp next from eq2 show " ?f ` A // R2 \<subseteq> Pow ?B" apply (unfold image_def Pow_def quotient_def, auto) by (rule_tac x = xb in bexI, simp, unfold equiv_def sym_def refl_on_def, blast) qed next show "inj_on ?f ?A" proof - { fix X Y assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y" (is "?L = ?R") have "X = Y" using X_in proof(rule quotientE) fix x assume "X = R2 `` {x}" and "x \<in> A" with eq2 have x_in: "x \<in> X" by (unfold equiv_def quotient_def refl_on_def, auto) with eq_f have "R1 `` {x} \<in> ?R" by auto then obtain y where y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto have "(x, y) \<in> R1" proof - from x_in X_in y_in Y_in eq2 have "x \<in> A" and "y \<in> A" by (unfold equiv_def quotient_def refl_on_def, auto) from eq_equiv_class_iff [OF eq1 this] and eq_r show ?thesis by simp qed with refined have xy_r2: "(x, y) \<in> R2" by auto from quotient_eqI [OF eq2 X_in Y_in x_in y_in this] show ?thesis . qed } thus ?thesis by (auto simp:inj_on_def) qed qedqedlemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)" apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def) by blastlemma tag_finite_imageD: fixes tag assumes rng_fnt: "finite (range tag)" -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n" -- {* And strings with same tag are equivalent *} shows "finite (UNIV // (\<approx>Lang))"proof - let ?R1 = "(=tag=)" show ?thesis proof(rule_tac refined_partition_finite [of _ ?R1]) from finite_eq_f_rel [OF rng_fnt] show "finite (UNIV // =tag=)" . next from same_tag_eqvt show "(=tag=) \<subseteq> (\<approx>Lang)" by (auto simp:f_eq_rel_def str_eq_def) next from equiv_f_eq_rel show "equiv UNIV (=tag=)" by blast next from equiv_lang_eq show "equiv UNIV (\<approx>Lang)" by blast qedqedtext {* A more concise, but less intelligible argument for @{text "tag_finite_imageD"} is given as the following. The basic idea is still using standard library lemma @{thm [source] "finite_imageD"}: \[ @{thm "finite_imageD" [no_vars]} \] which says: if the image of injective function @{text "f"} over set @{text "A"} is finite, then @{text "A"} must be finte, as we did in the lemmas above. *}lemma fixes tag assumes rng_fnt: "finite (range tag)" -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *} and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n" -- {* And strings with same tag are equivalent *} shows "finite (UNIV // (\<approx>Lang))" -- {* Then the partition generated by @{text "(\<approx>Lang)"} is finite. *}proof - -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*} let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>Lang)" show ?thesis proof (rule_tac f = "?f" and A = ?A in finite_imageD) -- {* The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}: *} show "finite (?f ` ?A)" proof - have "\<forall> X. ?f X \<in> (Pow (range tag))" by (auto simp:image_def Pow_def) moreover from rng_fnt have "finite (Pow (range tag))" by simp ultimately have "finite (range ?f)" by (auto simp only:image_def intro:finite_subset) from finite_range_image [OF this] show ?thesis . qed next -- {* The injectivity of @{text "f"} is the consequence of assumption @{text "same_tag_eqvt"}: *} show "inj_on ?f ?A" proof- { fix X Y assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and tag_eq: "?f X = ?f Y" have "X = Y" proof - from X_in Y_in tag_eq obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y" unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def apply simp by blast from same_tag_eqvt [OF eq_tg] have "x \<approx>Lang y" . with X_in Y_in x_in y_in show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def) qed } thus ?thesis unfolding inj_on_def by auto qed qedqedsubsection {* Lemmas for basic cases *}text {* The the final result of this direction is in @{text "easier_direction"}, which is an induction on the structure of regular expressions. There is one case for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"}, the finiteness of their language partition can be established directly with no need of taggiing. This section contains several technical lemma for these base cases. The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. Tagging functions need to be defined individually for each of them. There will be one dedicated section for each of these cases, and each section goes virtually the same way: gives definition of the tagging function and prove that strings with the same tag are equivalent. *}lemma quot_empty_subset: "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"proof fix x assume "x \<in> UNIV // \<approx>{[]}" then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" unfolding quotient_def Image_def by blast show "x \<in> {{[]}, UNIV - {[]}}" proof (cases "y = []") case True with h have "x = {[]}" by (auto simp:str_eq_rel_def) thus ?thesis by simp next case False with h have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def) thus ?thesis by simp qedqedlemma quot_char_subset: "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"proof fix x assume "x \<in> UNIV // \<approx>{[c]}" then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}" unfolding quotient_def Image_def by blast show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}" proof - { assume "y = []" hence "x = {[]}" using h by (auto simp:str_eq_rel_def) } moreover { assume "y = [c]" hence "x = {[c]}" using h by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) } moreover { assume "y \<noteq> []" and "y \<noteq> [c]" hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto) moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])" by (case_tac p, auto) ultimately have "x = UNIV - {[],[c]}" using h by (auto simp add:str_eq_rel_def) } ultimately show ?thesis by blast qedqedsubsection {* The case for @{text "SEQ"}*}definition "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa. xa \<le> x \<and> xa \<in> L\<^isub>1})"lemma tag_str_seq_range_finite: "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (Pow (UNIV // \<approx>L\<^isub>2))" in finite_subset)by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits)lemma append_seq_elim: assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"proof- from assms obtain s\<^isub>1 s\<^isub>2 where "x @ y = s\<^isub>1 @ s\<^isub>2" and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2" by (auto simp:Seq_def) hence "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)" using app_eq_dest by auto moreover have "\<lbrakk>x \<le> s\<^isub>1; (s\<^isub>1 - x) @ s\<^isub>2 = y\<rbrakk> \<Longrightarrow> \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2" using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE) moreover have "\<lbrakk>s\<^isub>1 \<le> x; (x - s\<^isub>1) @ y = s\<^isub>2\<rbrakk> \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2" using in_seq by (rule_tac x = s\<^isub>1 in exI, auto) ultimately show ?thesis by blastqedlemma tag_str_SEQ_injI: "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n"proof- { fix x y z assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2" and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y" have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2" proof- have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)" using xz_in_seq append_seq_elim by simp moreover { fix xa assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2" obtain ya where "ya \<le> y" and "ya \<in> L\<^isub>1" and "(y - ya) @ z \<in> L\<^isub>2" proof - have "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1 \<and> (x - xa) \<approx>L\<^isub>2 (y - ya)" proof - have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = {\<approx>L\<^isub>2 `` {y - xa} |xa. xa \<le> y \<and> xa \<in> L\<^isub>1}" (is "?Left = ?Right") using h1 tag_xy by (auto simp:tag_str_SEQ_def) moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp thus ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def) qed with prems show ?thesis by (auto simp:str_eq_rel_def str_eq_def) qed hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def) } moreover { fix za assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2" hence "y @ za \<in> L\<^isub>1" proof- have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" using h1 tag_xy by (auto simp:tag_str_SEQ_def) with h2 show ?thesis by (auto simp:Image_def str_eq_rel_def str_eq_def) qed with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE) } ultimately show ?thesis by blast qed } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n" by (auto simp add: str_eq_def str_eq_rel_def)qed lemma quot_seq_finiteI: "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))" apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD) by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite)subsection {* The case for @{text "ALT"} *}definition "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"lemma quot_union_finiteI: assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))" and finite2: "finite (UNIV // \<approx>L\<^isub>2)" shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD) show "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n" unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by autonext show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset) by (auto simp:tag_str_ALT_def Image_def quotient_def)qedsubsection {* The case for @{text "STAR"} *}text {* This turned out to be the trickiest case. Any string @{text "x"} in language @{text "L\<^isub>1\<star>"}, can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}. For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then defined by collecting the @{text "L\<^isub>1"}-state of the suffixes from every possible split. *} (* I will make some illustrations for it. *)definition "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"text {* A technical lemma. *}lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"proof (induct rule:finite.induct) case emptyI thus ?case by simpnext case (insertI A a) show ?case proof (cases "A = {}") case True thus ?thesis by (rule_tac x = a in bexI, auto) next case False with prems obtain max where h1: "max \<in> A" and h2: "\<forall>a\<in>A. f a \<le> f max" by blast show ?thesis proof (cases "f a \<le> f max") assume "f a \<le> f max" with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto) next assume "\<not> (f a \<le> f max)" thus ?thesis using h2 by (rule_tac x = a in bexI, auto) qed qedqedtext {* Technical lemma. *}lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"apply (induct x rule:rev_induct, simp)apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")by (auto simp:strict_prefix_def)text {* The following lemma @{text "tag_str_star_range_finite"} establishes the range finiteness of the tagging function. *}lemma tag_str_star_range_finite: "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (range (tag_str_STAR L\<^isub>1))"apply (rule_tac B = "Pow (UNIV // \<approx>L\<^isub>1)" in finite_subset)by (auto simp:tag_str_STAR_def Image_def quotient_def split:if_splits)text {* The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of the tagging function for case @{text "STAR"}. *}lemma tag_str_STAR_injI: fixes v w assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w" shows "(v::string) \<approx>(L\<^isub>1\<star>) w"proof- -- {* \begin{minipage}{0.9\textwidth} According to the definition of @{text "\<approx>Lang"}, proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to showing: for any string @{text "u"}, if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa. The reasoning pattern for both directions are the same, as derived in the following: \end{minipage} *} { fix x y z assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y" have "y @ z \<in> L\<^isub>1\<star>" proof(cases "x = []") -- {* The degenerated case when @{text "x"} is a null string is easy to prove: *} case True with tag_xy have "y = []" by (auto simp:tag_str_STAR_def strict_prefix_def) thus ?thesis using xz_in_star True by simp next -- {* \begin{minipage}{0.9\textwidth} The case when @{text "x"} is not null, and @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, \end{minipage} *} case False obtain x_max where h1: "x_max < x" and h2: "x_max \<in> L\<^isub>1\<star>" and h3: "(x - x_max) @ z \<in> L\<^isub>1\<star>" and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star> \<longrightarrow> length xa \<le> length x_max" proof- let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}" have "finite ?S" by (rule_tac B = "{xa. xa < x}" in finite_subset, auto simp:finite_strict_prefix_set) moreover have "?S \<noteq> {}" using False xz_in_star by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def) ultimately have "\<exists> max \<in> ?S. \<forall> a \<in> ?S. length a \<le> length max" using finite_set_has_max by blast with prems show ?thesis by blast qed obtain ya where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" and h7: "(x - x_max) \<approx>L\<^isub>1 (y - ya)" proof- from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right") by (auto simp:tag_str_STAR_def) moreover have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?left" using h1 h2 by auto ultimately have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?right" by simp with prems show ?thesis apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast qed have "(y - ya) @ z \<in> L\<^isub>1\<star>" proof- from h3 h1 obtain a b where a_in: "a \<in> L\<^isub>1" and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" and ab_max: "(x - x_max) @ z = a @ b" by (drule_tac star_decom, auto simp:strict_prefix_def elim:prefixE) have "(x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z" proof - have "((x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z) \<or> (a < (x - x_max) \<and> ((x - x_max) - a) @ z = b)" using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def) moreover { assume np: "a < (x - x_max)" and b_eqs: " ((x - x_max) - a) @ z = b" have "False" proof - let ?x_max' = "x_max @ a" have "?x_max' < x" using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) moreover have "?x_max' \<in> L\<^isub>1\<star>" using a_in h2 by (simp add:star_intro3) moreover have "(x - ?x_max') @ z \<in> L\<^isub>1\<star>" using b_eqs b_in np h1 by (simp add:diff_diff_appd) moreover have "\<not> (length ?x_max' \<le> length x_max)" using a_neq by simp ultimately show ?thesis using h4 by blast qed } ultimately show ?thesis by blast qed then obtain za where z_decom: "z = za @ b" and x_za: "(x - x_max) @ za \<in> L\<^isub>1" using a_in by (auto elim:prefixE) from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1" by (auto simp:str_eq_def str_eq_rel_def) with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"]) qed with h5 h6 show ?thesis by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) qed } -- {* By instantiating the reasoning pattern just derived for both directions:*} from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] -- {* The thesis is proved as a trival consequence: *} show ?thesis by (unfold str_eq_def str_eq_rel_def, blast)qedlemma quot_star_finiteI: "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))" apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD) by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite)subsection {* The main lemma *}lemma easier_direction: "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"proof (induct arbitrary:Lang rule:rexp.induct) case NULL have "UNIV // (\<approx>{}) \<subseteq> {UNIV} " by (auto simp:quotient_def str_eq_rel_def str_eq_def) with prems show "?case" by (auto intro:finite_subset)next case EMPTY have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" by (rule quot_empty_subset) with prems show ?case by (auto intro:finite_subset)next case (CHAR c) have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" by (rule quot_char_subset) with prems show ?case by (auto intro:finite_subset)next case (SEQ r\<^isub>1 r\<^isub>2) have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 ;; L r\<^isub>2))" by (erule quot_seq_finiteI, simp) with prems show ?case by simpnext case (ALT r\<^isub>1 r\<^isub>2) have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 \<union> L r\<^isub>2))" by (erule quot_union_finiteI, simp) with prems show ?case by simp next case (STAR r) have "finite (UNIV // \<approx>(L r)) \<Longrightarrow> finite (UNIV // \<approx>((L r)\<star>))" by (erule quot_star_finiteI) with prems show ?case by simpqed end(*lemma refined_quotient_union_eq: assumes refined: "R1 \<subseteq> R2" and eq1: "equiv A R1" and eq2: "equiv A R2" and y_in: "y \<in> A" shows "\<Union>{R1 `` {x} | x. x \<in> (R2 `` {y})} = R2 `` {y}"proof show "\<Union>{R1 `` {x} |x. x \<in> R2 `` {y}} \<subseteq> R2 `` {y}" (is "?L \<subseteq> ?R") proof - { fix z assume zl: "z \<in> ?L" and nzr: "z \<notin> ?R" have "False" proof - from zl and eq1 eq2 and y_in obtain x where xy2: "(x, y) \<in> R2" and zx1: "(z, x) \<in> R1" by (simp only:equiv_def sym_def, blast) have "(z, y) \<in> R2" proof - from zx1 and refined have "(z, x) \<in> R2" by blast moreover from xy2 have "(x, y) \<in> R2" . ultimately show ?thesis using eq2 by (simp only:equiv_def, unfold trans_def, blast) qed with nzr eq2 show ?thesis by (auto simp:equiv_def sym_def) qed } thus ?thesis by blast qednext show "R2 `` {y} \<subseteq> \<Union>{R1 `` {x} |x. x \<in> R2 `` {y}}" (is "?L \<subseteq> ?R") proof fix x assume x_in: "x \<in> ?L" with eq1 eq2 have "x \<in> R1 `` {x}" by (unfold equiv_def refl_on_def, auto) with x_in show "x \<in> ?R" by auto qedqed*)(*lemma refined_partition_finite: fixes R1 R2 A assumes fnt: "finite (A // R1)" and refined: "R1 \<subseteq> R2" and eq1: "equiv A R1" and eq2: "equiv A R2" shows "finite (A // R2)"proof - let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}" and ?A = "(A // R2)" and ?B = "(A // R1)" show ?thesis proof(rule_tac f = ?f and A = ?A in finite_imageD) show "finite (?f ` ?A)" proof(rule finite_subset [of _ "Pow ?B"]) from fnt show "finite (Pow (A // R1))" by simp next from eq2 show " ?f ` A // R2 \<subseteq> Pow ?B" apply (unfold image_def Pow_def quotient_def, auto) by (rule_tac x = xb in bexI, simp, unfold equiv_def sym_def refl_on_def, blast) qed next show "inj_on ?f ?A" proof - { fix X Y assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y" (is "?L = ?R") hence "X = Y" proof - from X_in eq2 obtain x where x_in: "x \<in> A" and eq_x: "X = R2 `` {x}" (is "X = ?X") by (unfold quotient_def equiv_def refl_on_def, auto) from Y_in eq2 obtain y where y_in: "y \<in> A" and eq_y: "Y = R2 `` {y}" (is "Y = ?Y") by (unfold quotient_def equiv_def refl_on_def, auto) have "?X = ?Y" proof - from eq_f have "\<Union> ?L = \<Union> ?R" by auto moreover have "\<Union> ?L = ?X" proof - from eq_x have "\<Union> ?L = \<Union>{R1 `` {x} |x. x \<in> ?X}" by simp also from refined_quotient_union_eq [OF refined eq1 eq2 x_in] have "\<dots> = ?X" . finally show ?thesis . qed moreover have "\<Union> ?R = ?Y" proof - from eq_y have "\<Union> ?R = \<Union>{R1 `` {y} |y. y \<in> ?Y}" by simp also from refined_quotient_union_eq [OF refined eq1 eq2 y_in] have "\<dots> = ?Y" . finally show ?thesis . qed ultimately show ?thesis by simp qed with eq_x eq_y show ?thesis by auto qed } thus ?thesis by (auto simp:inj_on_def) qed qedqed*)