
diff -r c19d2fc2cc69 -r d71424eb5d0c Myhill.thy
--- a/Myhill.thy	Mon Jan 31 12:54:31 2011 +0000
+++ b/Myhill.thy	Mon Jan 31 14:51:47 2011 +0000
@@ -18,19 +18,27 @@
   "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:
+  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.
+  While base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straight forward,
+  the inductive cases are rather involved. What we have when starting to prove these inductive caes is that
+  the partitions induced by the componet language are finite. The basic idea to show the finiteness of the 
+  partition induced by the composite language is to attach a tag @{text "tag(x)"} to every string 
+  @{text "x"}. The tags are made of equivalent classes from the component partitions. Let @{text "tag"}
+  be the tagging function and @{text "Lang"} be the composite language, it can be proved that
+  if strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
+  \[
+  @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
+  \]
+  then the partition induced by @{text "Lang"} must be 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, 
+    \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite, 
            the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).
+           Since tags are made from equivalent classes from component partitions, and the inductive
+           hypothesis ensures the finiteness of these partitions, it is not difficult to prove
+           the finiteness of @{text "range(tag)"}.
     \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"}
@@ -117,7 +125,8 @@
     next
       from eq2
       show " ?f ` A // R2 \<subseteq> Pow ?B"
-        apply (unfold image_def Pow_def quotient_def, auto)
+        unfolding image_def Pow_def quotient_def
+        apply auto
         by (rule_tac x = xb in bexI, simp, 
                  unfold equiv_def sym_def refl_on_def, blast)
     qed
@@ -132,7 +141,7 @@
           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)
+            unfolding equiv_def quotient_def refl_on_def by 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
@@ -140,7 +149,7 @@
           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)
+              unfolding equiv_def quotient_def refl_on_def by auto
             from eq_equiv_class_iff [OF eq1 this] and eq_r
             show ?thesis by simp
           qed
@@ -154,7 +163,7 @@
 qed
 
 lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)"
-  apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def)
+  unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
   by blast
 
 lemma tag_finite_imageD:
@@ -245,7 +254,32 @@
 
 subsection {* The proof*}
 
-subsubsection {* The case for @{const "NULL"} *}
+text {*
+  Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by
+  illustrations are given for non-trivial cases.
+
+  
+  For ever inductive case, there are two tasks, the easier one is to show the range finiteness of
+  of the tagging function based on the finiteness of component partitions, the
+  difficult one is to show that strings with the same tag are equivalent with respect to the 
+  composite language. Suppose the composite language be @{text "Lang"}, tagging function be 
+  @{text "tag"}, it amounts to show:
+  \[
+  @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
+  \]
+  expanding the definition of @{text "\<approx>Lang"}, it amounts to show:
+  \[
+  @{text "tag(x) = tag(y) \<Longrightarrow> (\<forall> z. x@z \<in> Lang \<longleftrightarrow> y@z \<in> Lang)"}
+  \]
+  Because the assumed tag equlity @{text "tag(x) = tag(y)"} is symmetric,
+  it is suffcient to show just one direction:
+  \[
+  @{text "\<And> x y z. \<lbrakk>tag(x) = tag(y); x@z \<in> Lang\<rbrakk> \<Longrightarrow> y@z \<in> Lang"}
+  \]
+  This is the pattern followed by every inductive case.
+  *}
+
+subsubsection {* The base case for @{const "NULL"} *}
 
 lemma quot_null_eq:
   shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
@@ -256,7 +290,7 @@
 unfolding quot_null_eq by simp
 
 
-subsubsection {* The case for @{const "EMPTY"} *}
+subsubsection {* The base case for @{const "EMPTY"} *}
 
 
 lemma quot_empty_subset:
@@ -283,7 +317,7 @@
 by (rule finite_subset[OF quot_empty_subset]) (simp)
 
 
-subsubsection {* The case for @{const "CHAR"} *}
+subsubsection {* The base case for @{const "CHAR"} *}
 
 lemma quot_char_subset:
   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
@@ -315,110 +349,13 @@
 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} *}
+subsubsection {* The inductive 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)"
@@ -441,7 +378,161 @@
     by auto
 qed
 
-subsubsection {* The case for @{const "STAR"} *}
+subsubsection {* The inductive case for @{text "SEQ"}*}
+
+text {*
+  For case @{const "SEQ"}, the language @{text "L"} is @{text "L\<^isub>1 ;; L\<^isub>2"}.
+  Given @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"}, according to the defintion of @{text " L\<^isub>1 ;; L\<^isub>2"},
+  string @{text "x @ z"} can be splitted with the prefix in @{text "L\<^isub>1"} and suffix in @{text "L\<^isub>2"}.
+  The split point can either be in @{text "x"} (as shown in Fig. \ref{seq_first_split}),
+  or in @{text "z"} (as shown in Fig. \ref{seq_snd_split}). Whichever way it goes, the structure
+  on @{text "x @ z"} cn be transfered faithfully onto @{text "y @ z"} 
+  (as shown in Fig. \ref{seq_trans_first_split} and \ref{seq_trans_snd_split}) with the the help of the assumed 
+  tag equality. The following tag function @{text "tag_str_SEQ"} is such designed to facilitate
+  such transfers and lemma @{text "tag_str_SEQ_injI"} formalizes the informal argument above. The details 
+  of structure transfer will be given their.
+\input{fig_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}))"
+
+text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}
+
+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 eq_xys: "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)
+  from app_eq_dest [OF eq_xys]
+  have
+    "(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)" 
+               (is "?Split1 \<or> ?Split2") .
+  moreover have "?Split1 \<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 "?Split2 \<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:
+  fixes v w 
+  assumes eq_tag: "tag_str_SEQ L\<^isub>1 L\<^isub>2 v = tag_str_SEQ L\<^isub>1 L\<^isub>2 w" 
+  shows "v \<approx>(L\<^isub>1 ;; L\<^isub>2) w"
+proof-
+    -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
+  { 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-
+      -- {* There are two ways to split @{text "x@z"}: *}
+      from append_seq_elim [OF xz_in_seq]
+      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)" .
+      -- {* It can be shown that @{text "?thesis"} holds in either case: *}
+      moreover {
+        -- {* The case for the first split:*}
+        fix xa
+        assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"
+        -- {* The following subgoal implements the structure transfer:*}
+        obtain ya 
+          where "ya \<le> y" 
+          and "ya \<in> L\<^isub>1" 
+          and "(y - ya) @ z \<in> L\<^isub>2"
+        proof -
+        -- {*
+            \begin{minipage}{0.8\textwidth}
+            By expanding the definition of 
+            @{thm [display] "tag_xy"}
+            and extracting the second compoent, we get:
+            \end{minipage}
+            *}
+          have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = 
+                   {\<approx>L\<^isub>2 `` {y - ya} |ya. ya \<le> y \<and> ya \<in> L\<^isub>1}" (is "?Left = ?Right")
+            using tag_xy unfolding tag_str_SEQ_def by simp
+            -- {* Since @{thm "h1"} and @{thm "h2"} hold, it is not difficult to show: *}
+          moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto
+            -- {* 
+            \begin{minipage}{0.7\textwidth}
+            Through tag equality, equivalent class @{term "\<approx>L\<^isub>2 `` {x - xa}"} also 
+                  belongs to the @{text "?Right"}:
+            \end{minipage}
+            *}
+          ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp
+            -- {* From this, the counterpart of @{text "xa"} in @{text "y"} is obtained:*}
+          then obtain ya 
+            where eq_xya: "\<approx>L\<^isub>2 `` {x - xa} = \<approx>L\<^isub>2 `` {y - ya}" 
+            and pref_ya: "ya \<le> y" and ya_in: "ya \<in> L\<^isub>1"
+            by simp blast
+          -- {* It can be proved that @{text "ya"} has the desired property:*}
+          have "(y - ya)@z \<in> L\<^isub>2" 
+          proof -
+            from eq_xya have "(x - xa)  \<approx>L\<^isub>2 (y - ya)" 
+              unfolding Image_def str_eq_rel_def str_eq_def by auto
+            with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp
+          qed
+          -- {* Now, @{text "ya"} has all properties to be a qualified candidate:*}
+          with pref_ya ya_in 
+          show ?thesis using prems by blast
+        qed
+          -- {* From the properties of @{text "ya"}, @{text "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"} is derived easily.*}
+        hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)
+      } moreover {
+        -- {* The other case is even more simpler: *}
+        fix za
+        assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"
+        have "y @ za \<in> L\<^isub>1"
+        proof-
+          have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}" 
+            using tag_xy unfolding tag_str_SEQ_def by simp
+          with h2 show ?thesis
+            unfolding Image_def str_eq_rel_def str_eq_def by auto
+        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
+  } 
+  -- {* 
+      \begin{minipage}{0.8\textwidth}
+      @{text "?thesis"} is proved by exploiting the symmetry of 
+      @{thm [source] "eq_tag"}:
+      \end{minipage}
+      *}
+  from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
+    show ?thesis unfolding str_eq_def str_eq_rel_def by blast
+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 inductive case for @{const "STAR"} *}
 
 text {* 
   This turned out to be the trickiest case. The essential goal is 
@@ -449,24 +540,25 @@
   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 that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}.
           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).
+          and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}.
     \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).
+           @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"}  as shown in Fig. \ref{last_split}.
           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"}
+            \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be splitted 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"}.
+              as shown in Fig. \ref{ab_split}.
+            \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"} 
+              (as shown in Fig. \ref{ab_split_wrong}), becasue otherwise,
+                   @{text "ma_max@a"} would be in the same kind as @{text "xa_max"} but with 
+                   a larger size, conflicting with the fact that @{text "xa_max"} is the longest.
           \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:
+          can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}. 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"}.
@@ -478,182 +570,9 @@
 
   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*$};
+  \ref{ansfer_step} feasible.
 
-    \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}
-
+  \input{fig_star}
 *} 
 
 definition 
@@ -688,7 +607,7 @@
 qed
 
 
-text {* Technical lemma. *}
+text {* The following is a technical lemma.which helps to show the range finiteness of tag function. *}
 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}")
@@ -700,16 +619,7 @@
   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}
-    *}
+    -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
   { 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"
@@ -723,16 +633,12 @@
         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}
+        -- {* The nontrival case:
         *}
       case False
       -- {* 
-        \begin{minipage}{0.9\textwidth}
-        Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splited
+        \begin{minipage}{0.8\textwidth}
+        Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splitted
         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"} 
@@ -745,8 +651,9 @@
           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"}:
+      -- {* \begin{minipage}{0.7\textwidth} 
+            Since @{text "?S"} is finite, we can always single out the longest and name it @{text "xa_max"}: 
+            \end{minipage}
           *}
       ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 
         using finite_set_has_max by blast
@@ -758,7 +665,7 @@
                                      \<longrightarrow> length xa \<le> length xa_max"
         by blast
       -- {*
-          \begin{minipage}{0.9\textwidth}
+          \begin{minipage}{0.8\textwidth}
           By the equality of tags, the counterpart of @{text "xa_max"} among 
           @{text "y"}-prefixes, named @{text "ya"}, can be found:
           \end{minipage}
@@ -776,9 +683,9 @@
           (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.
+          \begin{minipage}{0.8\textwidth}
+          The @{text "?thesis"}, @{prop "y @ z \<in> L\<^isub>1\<star>"}, is a simple consequence
+          of the following proposition:
           \end{minipage}
           *}
       have "(y - ya) @ z \<in> L\<^isub>1\<star>" 
@@ -789,8 +696,8 @@
           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
+            \begin{minipage}{0.8\textwidth}
+            Since @{thm "h1"}, @{text "x"} can be splitted into
             @{text "a"} and @{text "b"} such that:
             \end{minipage}
             *}
@@ -806,9 +713,9 @@
             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:
+              \begin{minipage}{0.8\textwidth}
+              Since @{text "(x - xa_max) @ z = a @ b"}, string @{text "(x - xa_max) @ z"}
+              can be splitted in two ways:
               \end{minipage}
               *}
             have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 
@@ -842,10 +749,7 @@
           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}
+           @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
             *}
         from step [OF l_za ls_zb]
         have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" .
@@ -858,17 +762,17 @@
   -- {* 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)
+    show  ?thesis unfolding str_eq_def str_eq_rel_def by blast
 qed
 
 
-lemma -- {* The oringal version with a poor readability*}
+lemma -- {* The oringal version with less explicit details. *}
   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}
+    \begin{minipage}{0.8\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"},
@@ -891,7 +795,7 @@
       thus ?thesis using xz_in_star True by simp
     next
         -- {*
-        \begin{minipage}{0.9\textwidth}
+        \begin{minipage}{0.8\textwidth}
         The case when @{text "x"} is not null, and
         @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, 
         \end{minipage}
@@ -967,7 +871,7 @@
   -- {* 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)
+    show  ?thesis unfolding str_eq_def str_eq_rel_def by blast
 qed
 
 lemma quot_star_finiteI [intro]:




