theory Myhill
imports Myhill_1
begin
section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
subsection {* The scheme*}
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 :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<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
qed
qed
lemma 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
qed
qed
lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)"
apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def)
by blast
lemma 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
qed
qed
text {*
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
qed
qed
subsection {* The proof*}
subsubsection {* The case for @{const "NULL"} *}
lemma quot_null_eq:
shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
unfolding quotient_def Image_def str_eq_rel_def by auto
lemma quot_null_finiteI [intro]:
shows "finite ((UNIV // \<approx>{})::lang set)"
unfolding quot_null_eq by simp
subsubsection {* The case for @{const "EMPTY"} *}
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
qed
qed
lemma quot_empty_finiteI [intro]:
shows "finite (UNIV // (\<approx>{[]}))"
by (rule finite_subset[OF quot_empty_subset]) (simp)
subsubsection {* The case for @{const "CHAR"} *}
lemma 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
qed
qed
lemma quot_char_finiteI [intro]:
shows "finite (UNIV // (\<approx>{[c]}))"
by (rule finite_subset[OF quot_char_subset]) (simp)
subsubsection {* The case for @{text "SEQ"}*}
definition
tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
where
"tag_str_SEQ L1 L2 =
(\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
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 blast
qed
lemma 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 [intro]:
fixes L1 L2::"lang"
assumes fin1: "finite (UNIV // \<approx>L1)"
and fin2: "finite (UNIV // \<approx>L2)"
shows "finite (UNIV // \<approx>(L1 ;; L2))"
proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
by (rule tag_str_SEQ_injI)
next
have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))"
using fin1 fin2 by auto
show "finite (range (tag_str_SEQ L1 L2))"
unfolding tag_str_SEQ_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
qed
subsubsection {* The case for @{const ALT} *}
definition
tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
where
"tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
lemma quot_union_finiteI [intro]:
fixes L1 L2::"lang"
assumes finite1: "finite (UNIV // \<approx>L1)"
and finite2: "finite (UNIV // \<approx>L2)"
shows "finite (UNIV // \<approx>(L1 \<union> L2))"
proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD)
show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y"
unfolding tag_str_ALT_def
unfolding str_eq_def
unfolding Image_def
unfolding str_eq_rel_def
by auto
next
have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))"
using finite1 finite2 by auto
show "finite (range (tag_str_ALT L1 L2))"
unfolding tag_str_ALT_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
qed
subsubsection {* The case for @{const "STAR"} *}
text {*
This turned out to be the trickiest case. The essential goal is
to proved @{text "y @ z \<in> L\<^isub>1*"} under the assumptions that @{text "x @ z \<in> L\<^isub>1*"}
and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following:
\begin{enumerate}
\item Since @{text "x @ z \<in> L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found
such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}(a).
Such a prefix always exists, @{text "xa = []"}, for example, is one.
\item There could be many but fintie many of such @{text "xa"}, from which we can find the longest
and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}(b).
\item The next step is to split @{text "z"} into @{text "za"} and @{text "zb"} such that
@{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"} as shown in Fig. \ref{last_split}(d).
Such a split always exists because:
\begin{enumerate}
\item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be split into prefix @{text "a"}
and suffix @{text "b"}, such that @{text "a \<in> L\<^isub>1"} and @{text "b \<in> L\<^isub>1*"},
as shown in Fig. \ref{ab_split}(c).
\item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"}, otherwise
@{text "xa_max"} is not the max in it's kind.
\item Now, @{text "za"} is just @{text "a - (x - xa_max)"} and @{text "zb"} is just @{text "b"}.
\end{enumerate}
\item \label{tansfer_step}
By the assumption that @{text "x"} and @{text "y"} have the same tag, the structure on @{text "x @ z"}
can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}(e). The detailed steps are:
\begin{enumerate}
\item A @{text "y"}-prefix @{text "ya"} corresponding to @{text "xa"} can be found,
which satisfies conditions: @{text "ya \<in> L\<^isub>1*"} and @{text "(y - ya)@za \<in> L\<^isub>1"}.
\item Since we already know @{text "zb \<in> L\<^isub>1*"}, we get @{text "(y - ya)@za@zb \<in> L\<^isub>1*"},
and this is just @{text "(y - ya)@z \<in> L\<^isub>1*"}.
\item With fact @{text "ya \<in> L\<^isub>1*"}, we finally get @{text "y@z \<in> L\<^isub>1*"}.
\end{enumerate}
\end{enumerate}
The formal proof of lemma @{text "tag_str_STAR_injI"} faithfully follows this informal argument
while the tagging function @{text "tag_str_STAR"} is defined to make the transfer in step
\ref{transfer_step}4 feasible.
\begin{figure}[h!]
\centering
\subfigure[First split]{\label{first_split}
\scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) {$\hspace{2em}xa\hspace{2em}$};
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{5em}x - xa\hspace{5em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
node[midway, above=0.5em]{$x$};
\draw[decoration={brace,transform={yscale=3}},decorate]
(z.north west) -- ($(z.north east)+(0em,0em)$)
node[midway, above=0.5em]{$z$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
node[midway, above=0.8em]{$x @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$(x - xa) @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$xa \in L_1*$};
\end{tikzpicture}}}
\subfigure[Max split]{\label{max_split}
\scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
node[midway, above=0.5em]{$x$};
\draw[decoration={brace,transform={yscale=3}},decorate]
(z.north west) -- ($(z.north east)+(0em,0em)$)
node[midway, above=0.5em]{$z$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
node[midway, above=0.8em]{$x @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$xa \in L_1*$};
\end{tikzpicture}}}
\subfigure[Max split with $a$ and $b$]{\label{ab_split}
\scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
node[midway, above=0.5em]{$x$};
\draw[decoration={brace,transform={yscale=3}},decorate]
(z.north west) -- ($(z.north east)+(0em,0em)$)
node[midway, above=0.5em]{$z$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
node[midway, above=0.8em]{$x @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$xa \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xxa.south east)+(6em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
node[midway, below=0.5em]{$a \in L_1$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(6em,-5ex)$)
node[midway, below=0.5em]{$b \in L_1*$};
\end{tikzpicture}}}
\subfigure[Last split]{\label{last_split}
\scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
node[midway, above=0.5em]{$x$};
\draw[decoration={brace,transform={yscale=3}},decorate]
(za.north west) -- ($(zb.north east)+(0em,0em)$)
node[midway, above=0.5em]{$z$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
node[midway, above=0.8em]{$x @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$(x - xa\_max) @ za \in L_1$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$xa\_max \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$zb \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
node[midway, below=0.5em]{$(x - xa\_max)@z \in L_1*$};
\end{tikzpicture}}}
\subfigure[Transferring to $y$]{\label{trans_split}
\scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) { $\hspace{5em}ya\hspace{5em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{2em}y - ya\hspace{2em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };
\draw[decoration={brace,transform={yscale=3}},decorate]
(xa.north west) -- ($(xxa.north east)+(0em,0em)$)
node[midway, above=0.5em]{$y$};
\draw[decoration={brace,transform={yscale=3}},decorate]
(za.north west) -- ($(zb.north east)+(0em,0em)$)
node[midway, above=0.5em]{$z$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
node[midway, above=0.8em]{$y @ z \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$(y - ya) @ za \in L_1$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$ya \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
node[midway, below=0.5em]{$zb \in L_1*$};
\draw[decoration={brace,transform={yscale=3}},decorate]
($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
node[midway, below=0.5em]{$(y - ya)@z \in L_1*$};
\end{tikzpicture}}}
\caption{The case for $STAR$}
\end{figure}
*}
definition
tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
where
"tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<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 simp
next
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
qed
qed
text {* 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)
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
-- {*
\begin{minipage}{0.9\textwidth}
Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splited
by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such
that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},
and there could be many such splittings.Therefore, the following set @{text "?S"}
is nonempty, and finite as well:
\end{minipage}
*}
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)
-- {* Since @{text "?S"} is finite, we can always single out the longest
and name it @{text "xa_max"}:
*}
ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max"
using finite_set_has_max by blast
then obtain xa_max
where h1: "xa_max < x"
and h2: "xa_max \<in> L\<^isub>1\<star>"
and h3: "(x - xa_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 xa_max"
by blast
-- {*
\begin{minipage}{0.9\textwidth}
By the equality of tags, the counterpart of @{text "xa_max"} among
@{text "y"}-prefixes, named @{text "ya"}, can be found:
\end{minipage}
*}
obtain ya
where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>"
and eq_xya: "(x - xa_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 - xa_max} \<in> ?left" using h1 h2 by auto
ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
with prems show ?thesis apply
(simp add:Image_def str_eq_rel_def str_eq_def) by blast
qed
-- {*
\begin{minipage}{0.9\textwidth}
If the following proposition can be proved, then the @{text "?thesis"}:
@{text "y @ z \<in> L\<^isub>1\<star>"} is just a simple consequence.
\end{minipage}
*}
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
proof-
-- {* The idea is to split the suffix @{text "z"} into @{text "za"} and @{text "zb"},
such that: *}
obtain za zb where eq_zab: "z = za @ zb"
and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
proof -
-- {*
\begin{minipage}{0.9\textwidth}
Since @{text "(x - xa_max) @ z"} is in @{text "L\<^isub>1\<star>"}, it can be split into
@{text "a"} and @{text "b"} such that:
\end{minipage}
*}
from h1 have "(x - xa_max) @ z \<noteq> []"
by (auto simp:strict_prefix_def elim:prefixE)
from star_decom [OF h3 this]
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 - xa_max) @ z = a @ b" by blast
-- {* Now the candiates for @{text "za"} and @{text "zb"} are found:*}
let ?za = "a - (x - xa_max)" and ?zb = "b"
have pfx: "(x - xa_max) \<le> a" (is "?P1")
and eq_z: "z = ?za @ ?zb" (is "?P2")
proof -
-- {*
\begin{minipage}{0.9\textwidth}
Since @{text "(x - xa_max) @ z = a @ b"}, the string @{text "(x - xa_max) @ z"}
could be splited in two ways:
\end{minipage}
*}
have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or>
(a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)"
using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
moreover {
-- {* However, the undsired way can be refuted by absurdity: *}
assume np: "a < (x - xa_max)"
and b_eqs: "((x - xa_max) - a) @ z = b"
have "False"
proof -
let ?xa_max' = "xa_max @ a"
have "?xa_max' < x"
using np h1 by (clarsimp simp:strict_prefix_def diff_prefix)
moreover have "?xa_max' \<in> L\<^isub>1\<star>"
using a_in h2 by (simp add:star_intro3)
moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>"
using b_eqs b_in np h1 by (simp add:diff_diff_appd)
moreover have "\<not> (length ?xa_max' \<le> length xa_max)"
using a_neq by simp
ultimately show ?thesis using h4 by blast
qed }
-- {* Now it can be shown that the splitting goes the way we desired. *}
ultimately show ?P1 and ?P2 by auto
qed
hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
-- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}
with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
by (auto simp:str_eq_def str_eq_rel_def)
with eq_z and b_in prems
show ?thesis by blast
qed
-- {*
\begin{minipage}{0.9\textwidth}
From the properties of @{text "za"} and @{text "zb"} such obtained,
@{text "?thesis"} can be shown easily.
\end{minipage}
*}
from step [OF l_za ls_zb]
have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" .
with eq_zab show ?thesis by simp
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)
qed
lemma -- {* The oringal version with a poor readability*}
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)
qed
lemma quot_star_finiteI [intro]:
fixes L1::"lang"
assumes finite1: "finite (UNIV // \<approx>L1)"
shows "finite (UNIV // \<approx>(L1\<star>))"
proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y"
by (rule tag_str_STAR_injI)
next
have *: "finite (Pow (UNIV // \<approx>L1))"
using finite1 by auto
show "finite (range (tag_str_STAR L1))"
unfolding tag_str_STAR_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
qed
subsubsection{* The conclusion *}
lemma rexp_imp_finite:
fixes r::"rexp"
shows "finite (UNIV // \<approx>(L r))"
by (induct r) (auto)
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
qed
next
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
qed
qed
*)
(*
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
qed
qed
*)