--- a/Myhill_2.thy	Wed Aug 03 17:08:31 2011 +0000
+++ b/Myhill_2.thy	Fri Aug 05 05:34:11 2011 +0000
@@ -101,21 +101,17 @@
 
 lemma tag_finite_imageD:
   assumes rng_fnt: "finite (range tag)" 
-  and same_tag_eqvt: "=tag=  \<subseteq> \<approx>A"
+  and     refined: "=tag=  \<subseteq> \<approx>A"
   shows "finite (UNIV // \<approx>A)"
 proof (rule_tac refined_partition_finite [of "=tag="])
   show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
 next
-  from same_tag_eqvt
-  show "=tag= \<subseteq> \<approx>A" .
+  show "=tag= \<subseteq> \<approx>A" using refined .
 next
   show "equiv UNIV =tag="
-    unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
+  and  "equiv UNIV (\<approx>A)" 
+    unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def
     by auto
-next
-  show "equiv UNIV (\<approx>A)" 
-    unfolding equiv_def str_eq_def sym_def refl_on_def trans_def
-    by blast
 qed
 
 
@@ -139,18 +135,16 @@
 proof
   fix x
   assume "x \<in> UNIV // \<approx>{[]}"
-  then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" 
+  then obtain y where h: "x = {z. y \<approx>{[]} z}" 
     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_def)
-    thus ?thesis by simp
-  next
-    case False with h
-    have "x = UNIV - {[]}" by (auto simp: str_eq_def)
-    thus ?thesis by simp
-  qed
+  { assume "y = []"
+    with h have "x = {[]}" by (auto simp: str_eq_def)
+    then have "x \<in> {{[]}, UNIV - {[]}}" by simp }
+  moreover
+  { assume "y \<noteq> []"
+    with h have "x = UNIV - {[]}" by (auto simp: str_eq_def)
+    then have "x \<in> {{[]}, UNIV - {[]}}" by simp }
+  ultimately show "x \<in> {{[]}, UNIV - {[]}}" by blast
 qed
 
 lemma quot_one_finiteI [intro]:
@@ -408,7 +402,7 @@
 definition 
   tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
 where
-  "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x})"
+  "tag_Star A \<equiv> \<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x}"
 
 lemma tag_Star_non_empty_injI:
   assumes a: "tag_Star A x = tag_Star A y"
@@ -444,11 +438,13 @@
   and     c: "x @ z \<in> A\<star>"
   and     d: "x = []"
   shows "y @ z \<in> A\<star>"
-using assms
-apply(simp)
-apply(simp add: tag_Star_def strict_prefix_def)
-apply(auto simp add: prefix_def Partitions_def)
-by (metis Nil_in_star append_self_conv2)
+proof -
+  from a have "{} = tag_Star A y" unfolding tag_Star_def using d by auto 
+  then have "y = []"
+    unfolding tag_Star_def Partitions_def strict_prefix_def prefix_def
+    by (auto) (metis Nil_in_star append_self_conv2)
+  then show "y @ z \<in> A\<star>" using c d by simp
+qed
 
 lemma quot_star_finiteI [intro]:
   assumes finite1: "finite (UNIV // \<approx>A)"