theory Myhill
imports Myhill_1
begin
section {* 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 very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"}
is by attaching a tag to every string. The set of tags are carfully choosen to be finite so that
the range of tagging function is finite. If it can be proved that strings with the same tag
are equivlent with respect @{text "Lang"}, then the partition given rise by @{text "Lang"} must be finite.
The detailed argjument for this is formalized by the following lemma @{text "tag_finite_imageD"}.
The basic idea is using lemma @{thm [source] "finite_imageD"}
from standard library:
\[
@{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.
*}
(*
(* I am trying to reduce the following proof to even simpler principles. But not yet succeed. *)
definition
f_eq_rel ("\<cong>_")
where
"\<cong>(f::'a \<Rightarrow> 'b) = {(x, y) | x y. f x = f y}"
thm finite.induct
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 "equiv UNIV (\<cong>f)"
by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
lemma
assumes rng_fnt: "finite (range tag)"
shows "finite (UNIV // (\<cong>tag))"
proof -
let "?f" = "op ` tag" and ?A = "(UNIV // (\<cong>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 "\<cong>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_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 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))"
-- {* 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 {* 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
qed
qed
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
subsection {* 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 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:
"\<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 auto
next
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)
qed
subsection {*
The case for @{text "STAR"}
*}
text {*
This turned out to be the trickiest case.
*} (* 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>}"
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
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_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)
lemma tag_str_STAR_injI:
"tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
proof-
{ 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 = []")
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
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
} thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
by (auto simp add:str_eq_def str_eq_rel_def)
qed
lemma 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_directio\<nu>:
"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 simp
next
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 simp
qed
end