diff -r 212bfa431fa5 -r 79b37ef9505f Myhill_2.thy
--- a/Myhill_2.thy	Wed Feb 16 06:51:58 2011 +0000
+++ b/Myhill_2.thy	Wed Feb 16 12:25:53 2011 +0000
@@ -18,15 +18,18 @@
   "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
 text {*
-  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.
-  where base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
-  proof. Real difficulty lies in inductive cases.  By inductive hypothesis, languages defined by
-  sub-expressions induce finite partitiions. Under such hypothsis, we need to prove that the language 
-  defined by the composite regular expression gives rise to finite partion.  
-  The basic idea is to attach a tag @{text "tag(x)"} to every string 
-  @{text "x"}. The tagging fuction @{text "tag"} is carefully devised, which returns tags 
-  made of equivalent classes of the partitions induced by subexpressoins, and therefore has a finite
-  range. Let @{text "Lang"} be the composite language, it is proved that:
+  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural
+  induction over regular expressions.  where base cases (cases for @{const
+  "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
+  proof. Real difficulty lies in inductive cases.  By inductive hypothesis,
+  languages defined by sub-expressions induce finite partitiions. Under such
+  hypothsis, we need to prove that the language defined by the composite
+  regular expression gives rise to finite partion.  The basic idea is to
+  attach a tag @{text "tag(x)"} to every string @{text "x"}. The tagging
+  fuction @{text "tag"} is carefully devised, which returns tags made of
+  equivalent classes of the partitions induced by subexpressoins, and
+  therefore has a finite range. Let @{text "Lang"} be the composite language,
+  it is proved that:
   \begin{quote}
   If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
   \[
@@ -57,19 +60,22 @@
 definition 
    f_eq_rel ("=_=")
 where
-   "(=f=) = {(x, y) | x y. f x = f y}"
+   "=f= \<equiv> {(x, y) | x y. f x = f y}"
 
 lemma equiv_f_eq_rel:"equiv UNIV (=f=)"
   by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
 
-lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"
-  by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)
+lemma finite_range_image: 
+  assumes "finite (range f)"
+  shows "finite (f ` A)"
+  using assms unfolding image_def
+  by (rule_tac finite_subset) (auto)
 
 lemma finite_eq_f_rel:
   assumes rng_fnt: "finite (range tag)"
-  shows "finite (UNIV // (=tag=))"
+  shows "finite (UNIV // =tag=)"
 proof -
-  let "?f" =  "op ` tag" and ?A = "(UNIV // (=tag=))"
+  let "?f" =  "op ` tag" and ?A = "(UNIV // =tag=)"
   show ?thesis
   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
     -- {* 
@@ -109,7 +115,8 @@
   qed
 qed
 
-lemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"
+lemma finite_image_finite: 
+  "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"
   by (rule finite_subset [of _ B], auto)
 
 lemma refined_partition_finite:
@@ -357,7 +364,7 @@
 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 L1 L2 \<equiv> (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
 
 lemma quot_union_finiteI [intro]:
   fixes L1 L2::"lang"
@@ -401,7 +408,7 @@
 definition 
   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 where
-  "tag_str_SEQ L1 L2 = 
+  "tag_str_SEQ L1 L2 \<equiv>
      (\<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.*}
@@ -581,7 +588,7 @@
 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 L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
 
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>