# HG changeset patch
# User zhang
# Date 1296215531 0
# Node ID 7aa6c20e6d311d94aa0757cb5dcf2e17845c1c39
# Parent  5a7e02dcd3d59d3bb948a99a2210d8b253436b2d
More improvement

diff -r 5a7e02dcd3d5 -r 7aa6c20e6d31 Myhill.thy
--- a/Myhill.thy	Thu Jan 27 17:37:20 2011 +0000
+++ b/Myhill.thy	Fri Jan 28 11:52:11 2011 +0000
@@ -13,46 +13,51 @@
   *}
 
 definition
-  str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
+  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.
-  *}
+  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}"
 
-(* 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 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 "equiv UNIV (\<cong>f)"
-  by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
-
-lemma 
+lemma finite_eq_f_rel:
   assumes rng_fnt: "finite (range tag)"
-  shows "finite (UNIV // (\<cong>tag))"
+  shows "finite (UNIV // (=tag=))"
 proof -
-  let "?f" =  "op ` tag" and ?A = "(UNIV // (\<cong>tag))"
+  let "?f" =  "op ` tag" and ?A = "(UNIV // (=tag=))"
   show ?thesis
   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
     -- {* 
@@ -68,7 +73,7 @@
     qed
   next
     -- {* 
-      The injectivity of @{text "f"}-image is a consequence of the definition of @{text "\<cong>tag"}
+      The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}:
       *}
     show "inj_on ?f ?A" 
     proof-
@@ -79,8 +84,10 @@
         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
+          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) 
@@ -90,23 +97,114 @@
   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 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 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 L :: "lang"
+  fixes tag
   assumes rng_fnt: "finite (range tag)" 
-  -- {* Suppose the range of tagging fucntion @{text "tag"} is finite. *}
-  and same_tag_eqvt: "\<And> m n. tag m = tag n \<Longrightarrow> m \<approx>L n"
+  -- {* 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>L)"
-  -- {* Then the partition generated by @{text "\<approx>L"} is finite. *}
+  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>L)"
+  let "?f" =  "op ` tag" and ?A = "(UNIV // \<approx>Lang)"
   show ?thesis
   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
     -- {* 
@@ -136,7 +234,7 @@
           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>L y" .
+          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
@@ -148,33 +246,18 @@
 subsection {* Lemmas for basic cases *}
 
 text {*
-  The the final result of this direction is in @{text "rexp_imp_finite"},
-  which is an induction on the structure of regular expressions. There is one
-  case for each regular expression operator. For basic operators such as
-  @{const NULL}, @{const EMPTY}, @{const CHAR}, the finiteness of their 
-  language partition can be established directly with no need of tagging. 
-  This section contains several technical lemma for these base cases.
-
-  The inductive cases involve operators @{const ALT}, @{const SEQ} and @{const
-  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.
-*}
+  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.
 
-subsection {* 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
-
-
-subsection {* The case for @{const "EMPTY"} *}
-
+  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 - {[]}}"
@@ -183,25 +266,18 @@
   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 - {[]}}"
+  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_rel_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_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)
-
-
-subsection {* The case for @{const "CHAR"} *}
-
 lemma quot_char_subset:
   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
 proof 
@@ -227,18 +303,17 @@
   qed
 qed
 
-lemma quot_char_finiteI [intro]:
-  shows "finite (UNIV // (\<approx>{[c]}))"
-by (rule finite_subset[OF quot_char_subset]) (simp)
-
-
-subsection {* The case for @{const SEQ}*}
+subsection {* 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}))"
+  "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"
@@ -306,71 +381,52 @@
     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
+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
+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 @{const ALT} *}
+subsection {* The case for @{text "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}))"
-
+  "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 [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
+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
-  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
+  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 @{const "STAR"} *}
+subsection {*
+  The case for @{text "STAR"}
+  *}
 
 text {* 
   This turned out to be the trickiest case. 
-  *} (* I will make some illustrations for it. *)
+  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 :: "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>})"
+  "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))"
+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
@@ -394,24 +450,62 @@
   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)
 
+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:
-  "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
+  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"
+    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" 
@@ -478,36 +572,163 @@
       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
+  } 
+  -- {* 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)
+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_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
-  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
-
-
-subsection {* The main lemma *}
-
-lemma rexp_imp_finite:
-  fixes r::"rexp"
-  shows "finite (UNIV // \<approx>(L r))"
-by (induct r) (auto)
-
+  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
 
+(*
+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
+*)