diff -r b755090d0f3d -r 97090fc7aa9f Myhill_2.thy
--- 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