--- a/Myhill_2.thy Thu Jul 28 17:52:36 2011 +0000
+++ b/Myhill_2.thy Sun Jul 31 10:27:41 2011 +0000
@@ -5,21 +5,30 @@
section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
-definition
- str_eq :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _")
-where
- "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
-
-lemma str_eq_def2:
- shows "\<approx>A = {(x, y) | x y. x \<approx>A y}"
-unfolding str_eq_def
-by simp
-
definition
- tag_eq_rel :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
+ tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
where
"=tag= \<equiv> {(x, y). tag x = tag y}"
+abbreviation
+ tag_eq_applied :: "'a list \<Rightarrow> ('a list \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> bool" ("_ =_= _")
+where
+ "x =tag= y \<equiv> (x, y) \<in> =tag="
+
+lemma test:
+ shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"
+unfolding str_eq_def
+by auto
+
+lemma test_refined_intro:
+ assumes "\<And>x y z. \<lbrakk>x =tag= y; x @ z \<in> A\<rbrakk> \<Longrightarrow> y @ z \<in> A"
+ shows "=tag= \<subseteq> \<approx>A"
+using assms
+unfolding str_eq_def tag_eq_def
+apply(clarify, simp (no_asm_use))
+by metis
+
+
lemma finite_eq_tag_rel:
assumes rng_fnt: "finite (range tag)"
shows "finite (UNIV // =tag=)"
@@ -45,11 +54,11 @@
and tag_eq: "?f X = ?f Y"
then obtain x y
where "x \<in> X" "y \<in> Y" "tag x = tag y"
- unfolding quotient_def Image_def image_def tag_eq_rel_def
+ unfolding quotient_def Image_def image_def tag_eq_def
by (simp) (blast)
with X_in Y_in
have "X = Y"
- unfolding quotient_def tag_eq_rel_def by auto
+ unfolding quotient_def tag_eq_def by auto
}
then show "inj_on ?f ?A" unfolding inj_on_def by auto
qed
@@ -101,15 +110,15 @@
show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
next
from same_tag_eqvt
- show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def
- by auto
+ show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_def str_eq_def
+ by blast
next
show "equiv UNIV =tag="
- unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
+ unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
by auto
next
show "equiv UNIV (\<approx>A)"
- unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
+ unfolding equiv_def str_eq_def sym_def refl_on_def trans_def
by blast
qed
@@ -120,7 +129,7 @@
lemma quot_zero_eq:
shows "UNIV // \<approx>{} = {UNIV}"
-unfolding quotient_def Image_def str_eq_rel_def by auto
+unfolding quotient_def Image_def str_eq_def by auto
lemma quot_zero_finiteI [intro]:
shows "finite (UNIV // \<approx>{})"
@@ -139,11 +148,11 @@
show "x \<in> {{[]}, UNIV - {[]}}"
proof (cases "y = []")
case True with h
- have "x = {[]}" by (auto simp: str_eq_rel_def)
+ have "x = {[]}" by (auto simp: str_eq_def)
thus ?thesis by simp
next
case False with h
- have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)
+ have "x = UNIV - {[]}" by (auto simp: str_eq_def)
thus ?thesis by simp
qed
qed
@@ -165,17 +174,17 @@
show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
proof -
{ assume "y = []" hence "x = {[]}" using h
- by (auto simp:str_eq_rel_def) }
+ by (auto simp: str_eq_def) }
moreover
{ assume "y = [c]" hence "x = {[c]}" using h
- by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) }
+ by (auto dest!: spec[where x = "[]"] simp: str_eq_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)
+ by (auto simp add: str_eq_def)
}
ultimately show ?thesis by blast
qed
@@ -189,38 +198,126 @@
subsubsection {* The inductive case for @{const Plus} *}
definition
- tag_str_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
+ tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
where
- "tag_str_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
+ "tag_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
-lemma quot_union_finiteI [intro]:
+lemma quot_plus_finiteI [intro]:
assumes finite1: "finite (UNIV // \<approx>A)"
and finite2: "finite (UNIV // \<approx>B)"
shows "finite (UNIV // \<approx>(A \<union> B))"
-proof (rule_tac tag = "tag_str_Plus A B" in tag_finite_imageD)
+proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD)
have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"
using finite1 finite2 by auto
- then show "finite (range (tag_str_Plus A B))"
- unfolding tag_str_Plus_def quotient_def
+ then show "finite (range (tag_Plus A B))"
+ unfolding tag_Plus_def quotient_def
by (rule rev_finite_subset) (auto)
next
- show "\<And>x y. tag_str_Plus A B x = tag_str_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
- unfolding tag_str_Plus_def
+ show "\<And>x y. tag_Plus A B x = tag_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
+ unfolding tag_Plus_def
unfolding str_eq_def
- unfolding str_eq_rel_def
by auto
qed
subsubsection {* The inductive case for @{text "Times"}*}
+definition
+ "Partitions s \<equiv> {(u, v). u @ v = s}"
+
+lemma conc_elim:
+ assumes "x \<in> A \<cdot> B"
+ shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B"
+using assms
+unfolding conc_def Partitions_def
+by auto
+
+lemma conc_intro:
+ assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and> v \<in> B"
+ shows "x \<in> A \<cdot> B"
+using assms
+unfolding conc_def Partitions_def
+by auto
+
+
+lemma y:
+ "\<lbrakk>x \<in> A; x \<approx>A y\<rbrakk> \<Longrightarrow> y \<in> A"
+apply(simp add: str_eq_def)
+apply(drule_tac x="[]" in spec)
+apply(simp)
+done
+
definition
- tag_str_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
+ tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
+where
+ "tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})"
+
+definition
+ tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
+where
+ "tag_Times3b A B \<equiv>
+ (\<lambda>x. ({(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}))"
+
+definition
+ tag_Times3 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set"
where
- "tag_str_Times L1 L2 \<equiv>
- (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
+ "tag_Times3 A B \<equiv>
+ (\<lambda>x. (tag_Times3a A B x, tag_Times3b A B x))"
-lemma Seq_in_cases:
+lemma
+ assumes a: "tag_Times3a A B x = tag_Times3a A B y"
+ and b: "tag_Times3b A B x = tag_Times3b A B y"
+ and c: "x @ z \<in> A \<cdot> B"
+ shows "y @ z \<in> A \<cdot> B"
+proof -
+ from c obtain u v where
+ h1: "(u, v) \<in> Partitions (x @ z)" and
+ h2: "u \<in> A" and
+ h3: "v \<in> B" by (auto dest: conc_elim)
+ from h1 have "x @ z = u @ v" unfolding Partitions_def by simp
+ then obtain us
+ where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)"
+ by (auto simp add: append_eq_append_conv2)
+ moreover
+ { assume eq: "x = u @ us" "us @ z = v"
+ have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B x"
+ unfolding tag_Times3b_def Partitions_def using eq by auto
+ then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B y"
+ using b by simp
+ then obtain u' us' where
+ q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and
+ q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and
+ q3: "(u', us') \<in> Partitions y"
+ by (auto simp add: tag_Times3b_def)
+ from q1 h2 have "u' \<in> A"
+ using y unfolding Image_def str_eq_def by blast
+ moreover from q2 h3 eq
+ have "us' @ z \<in> B"
+ unfolding Image_def str_eq_def by auto
+ ultimately have "y @ z \<in> A \<cdot> B" using q3
+ unfolding Partitions_def by auto
+ }
+ moreover
+ { assume eq: "x @ us = u" "z = us @ v"
+ have "(\<approx>A `` {x}) = tag_Times3a A B x"
+ unfolding tag_Times3a_def by simp
+ then have "(\<approx>A `` {x}) = tag_Times3a A B y"
+ using a by simp
+ then have "\<approx>A `` {x} = \<approx>A `` {y}"
+ unfolding tag_Times3a_def by simp
+ moreover
+ have "x @ us \<in> A" using h2 eq by simp
+ ultimately
+ have "y @ us \<in> A" using y
+ unfolding Image_def str_eq_def by blast
+ then have "(y @ us) @ v \<in> A \<cdot> B"
+ using h3 unfolding conc_def by blast
+ then have "y @ z \<in> A \<cdot> B" using eq by simp
+ }
+ ultimately show "y @ z \<in> A \<cdot> B" by blast
+qed
+
+lemma conc_in_cases2:
assumes "x @ z \<in> A \<cdot> B"
shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or>
(\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
@@ -228,13 +325,19 @@
unfolding conc_def prefix_def
by (auto simp add: append_eq_append_conv2)
-lemma tag_str_Times_injI:
- assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y"
+definition
+ tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
+where
+ "tag_Times A B \<equiv>
+ (\<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> A}))"
+
+lemma tag_Times_injI:
+ assumes eq_tag: "tag_Times A B x = tag_Times A B y"
shows "x \<approx>(A \<cdot> B) y"
proof -
{ fix x y z
assume xz_in_seq: "x @ z \<in> A \<cdot> B"
- and tag_xy: "tag_str_Times A B x = tag_str_Times A B y"
+ and tag_xy: "tag_Times A B x = tag_Times A B y"
have"y @ z \<in> A \<cdot> B"
proof -
{ (* first case with x' in A and (x - x') @ z in B *)
@@ -247,7 +350,7 @@
proof -
have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} =
{\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
- using tag_xy unfolding tag_str_Times_def by simp
+ using tag_xy unfolding tag_Times_def by simp
moreover
have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
ultimately
@@ -256,49 +359,49 @@
where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"
and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
by simp blast
-
have "(x - x') \<approx>B (y - y')" using eq_xy'
- unfolding Image_def str_eq_rel_def str_eq_def by auto
+ unfolding Image_def str_eq_def by auto
with h3 have "(y - y') @ z \<in> B"
- unfolding str_eq_rel_def str_eq_def by simp
+ unfolding str_eq_def by simp
with pref_y' y'_in
show ?thesis using that by blast
qed
- then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def)
+ then have "y @ z \<in> A \<cdot> B"
+ unfolding prefix_def by auto
}
moreover
{ (* second case with x @ z' in A and z - z' in B *)
fix z'
assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
have "\<approx>A `` {x} = \<approx>A `` {y}"
- using tag_xy unfolding tag_str_Times_def by simp
+ using tag_xy unfolding tag_Times_def by simp
with h2 have "y @ z' \<in> A"
- unfolding Image_def str_eq_rel_def str_eq_def by auto
+ unfolding Image_def str_eq_def by auto
with h1 h3 have "y @ z \<in> A \<cdot> B"
unfolding prefix_def conc_def
by (auto) (metis append_assoc)
}
ultimately show "y @ z \<in> A \<cdot> B"
- using Seq_in_cases [OF xz_in_seq] by blast
+ using conc_in_cases2 [OF xz_in_seq] by blast
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast
+ show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def by blast
qed
-lemma quot_seq_finiteI [intro]:
- fixes L1 L2::"'a lang"
- assumes fin1: "finite (UNIV // \<approx>L1)"
- and fin2: "finite (UNIV // \<approx>L2)"
- shows "finite (UNIV // \<approx>(L1 \<cdot> L2))"
-proof (rule_tac tag = "tag_str_Times L1 L2" in tag_finite_imageD)
- show "\<And>x y. tag_str_Times L1 L2 x = tag_str_Times L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
- by (rule tag_str_Times_injI)
+lemma quot_conc_finiteI [intro]:
+ fixes A B::"'a lang"
+ assumes fin1: "finite (UNIV // \<approx>A)"
+ and fin2: "finite (UNIV // \<approx>B)"
+ shows "finite (UNIV // \<approx>(A \<cdot> B))"
+proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD)
+ show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y"
+ by (rule tag_Times_injI)
next
- have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))"
+ have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"
using fin1 fin2 by auto
- show "finite (range (tag_str_Times L1 L2))"
- unfolding tag_str_Times_def
+ show "finite (range (tag_Times A B))"
+ unfolding tag_Times_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
@@ -307,10 +410,60 @@
subsubsection {* The inductive case for @{const "Star"} *}
+definition
+ "SPartitions s \<equiv> {(u, v). u @ v = s \<and> u < s}"
+
+lemma
+ assumes "x \<in> A\<star>" "x \<noteq> []"
+ shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v \<in> A\<star>"
+using assms
+apply(subst (asm) star_unfold_left)
+apply(simp)
+apply(simp add: conc_def)
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x="([], xs @ ys)" in bexI)
+apply(simp)
+apply(simp add: SPartitions_def)
+apply(auto)
+apply (metis append_Cons list.exhaust strict_prefix_simps(2))
+by (metis Nil_is_append_conv Nil_prefix xt1(11))
+
+lemma
+ assumes "x @ z \<in> A\<star>" "x \<noteq> []"
+ shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v @ z \<in> A\<star>"
+using assms
+apply(subst (asm) star_unfold_left)
+apply(simp)
+apply(simp add: conc_def)
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x="([], x)" in bexI)
+apply(simp)
+apply(simp add: SPartitions_def)
+by (metis Nil_prefix xt1(11))
+
+lemma finite_set_has_max:
+ "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max"
+apply (induct rule:finite.induct)
+apply(simp)
+by (metis (full_types) all_not_in_conv insertI1 insert_iff linorder_linear order_eq_iff order_trans prefix_length_le)
+
+
+
definition
- tag_str_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
+ tag_Star3 :: "'a lang \<Rightarrow> 'a list \<Rightarrow> (bool \<times> 'a lang) set"
where
- "tag_str_Star L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+ "tag_Star3 A \<equiv>
+ (\<lambda>x. ({(u \<in> A\<star>, \<approx>A `` {v}) | u v. (u, v) \<in> Partitions x}))"
+
+
+
+
+definition
+ tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
+where
+ "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {x - xa} | xa. xa < x \<and> xa \<in> A\<star>})"
text {* A technical lemma. *}
lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>
@@ -349,19 +502,19 @@
by (auto simp:strict_prefix_def)
-lemma tag_str_Star_injI:
+lemma tag_Star_injI:
fixes L\<^isub>1::"('a::finite) lang"
- assumes eq_tag: "tag_str_Star L\<^isub>1 v = tag_str_Star L\<^isub>1 w"
+ assumes eq_tag: "tag_Star L\<^isub>1 v = tag_Star L\<^isub>1 w"
shows "v \<approx>(L\<^isub>1\<star>) w"
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"
+ and tag_xy: "tag_Star L\<^isub>1 x = tag_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 add: tag_str_Star_def strict_prefix_def)
+ by (auto simp add: tag_Star_def strict_prefix_def)
thus ?thesis using xz_in_star True by simp
next
case False
@@ -386,19 +539,19 @@
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)
+ by (auto simp:tag_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
thus ?thesis using that
- apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
+ apply (simp add: Image_def str_eq_def) by blast
qed
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
proof-
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 -
- from h1 have "(x - xa_max) @ z \<noteq> []"
- by (auto simp:strict_prefix_def elim:prefixE)
+ from h1 have "(x - xa_max) @ z \<noteq> []"
+ unfolding strict_prefix_def prefix_def by auto
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>"
@@ -428,9 +581,9 @@
qed }
ultimately show ?P1 and ?P2 by auto
qed
- hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
+ hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in unfolding prefix_def by auto
with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
- by (auto simp:str_eq_def str_eq_rel_def)
+ by (auto simp: str_eq_def)
with eq_z and b_in
show ?thesis using that by blast
qed
@@ -439,25 +592,25 @@
with eq_zab show ?thesis by simp
qed
with h5 h6 show ?thesis
- by (auto simp:strict_prefix_def elim: prefixE)
+ unfolding strict_prefix_def prefix_def by auto
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show ?thesis unfolding str_eq_def str_eq_rel_def by blast
+ show ?thesis unfolding str_eq_def by blast
qed
lemma quot_star_finiteI [intro]:
fixes A::"('a::finite) lang"
assumes finite1: "finite (UNIV // \<approx>A)"
shows "finite (UNIV // \<approx>(A\<star>))"
-proof (rule_tac tag = "tag_str_Star A" in tag_finite_imageD)
- show "\<And>x y. tag_str_Star A x = tag_str_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
- by (rule tag_str_Star_injI)
+proof (rule_tac tag = "tag_Star A" in tag_finite_imageD)
+ show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
+ by (rule tag_Star_injI)
next
have *: "finite (Pow (UNIV // \<approx>A))"
using finite1 by auto
- show "finite (range (tag_str_Star A))"
- unfolding tag_str_Star_def
+ show "finite (range (tag_Star A))"
+ unfolding tag_Star_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto