# HG changeset patch
# User urbanc
# Date 1312298857 0
# Node ID 560712a29a36cd78a33fb4745964361d67fbe958
# Parent  97090fc7aa9fe850a65adfb0cef95dd81ced3371
a version of the proof which dispenses with the notion of string-subtraction

diff -r 97090fc7aa9f -r 560712a29a36 Attic/Prefix_subtract.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Prefix_subtract.thy	Tue Aug 02 15:27:37 2011 +0000
@@ -0,0 +1,60 @@
+theory Prefix_subtract
+  imports Main "~~/src/HOL/Library/List_Prefix"
+begin
+
+
+section {* A small theory of prefix subtraction *}
+
+text {*
+  The notion of @{text "prefix_subtract"} makes 
+  the second direction of the Myhill-Nerode theorem 
+  more readable.
+*}
+
+instantiation list :: (type) minus
+begin
+
+fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
+where
+  "minus_list []     xs     = []" 
+| "minus_list (x#xs) []     = x#xs" 
+| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"
+
+instance by default
+
+end
+
+lemma [simp]: "x - [] = x"
+by (induct x) (auto)
+
+lemma [simp]: "(x @ y) - x = y"
+by (induct x) (auto)
+
+lemma [simp]: "x - x = []"
+by (induct x) (auto)
+
+lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "
+by (induct x) (auto)
+
+lemma diff_prefix:
+  "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
+by (auto elim: prefixE)
+
+lemma diff_diff_append: 
+  "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
+apply (clarsimp simp:strict_prefix_def)
+by (drule diff_prefix, auto elim:prefixE)
+
+lemma append_eq_cases:
+  assumes a: "x @ y = m @ n"
+  shows "x \<le> m \<or> m \<le> x"
+unfolding prefix_def using a
+by (auto simp add: append_eq_append_conv2)
+
+lemma append_eq_dest:
+  assumes a: "x @ y = m @ n" 
+  shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
+using append_eq_cases[OF a] a
+by (auto elim: prefixE)
+
+end
diff -r 97090fc7aa9f -r 560712a29a36 Journal/Paper.thy
--- a/Journal/Paper.thy	Sun Jul 31 10:27:41 2011 +0000
+++ b/Journal/Paper.thy	Tue Aug 02 15:27:37 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Closures" 
+imports "../Closures" "../Attic/Prefix_subtract" 
 begin
 
 declare [[show_question_marks = false]]
@@ -1290,15 +1290,7 @@
   %
   \noindent
   and \emph{string subtraction}:
-  %
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{text "[] - y"}  & @{text "\<equiv>"} & @{text "[]"}\\
-  @{text "x - []"}  & @{text "\<equiv>"} & @{text "x"}\\
-  @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}
-  \end{tabular}
-  \end{center}
-  %
+
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. 
   
diff -r 97090fc7aa9f -r 560712a29a36 Myhill_2.thy
--- a/Myhill_2.thy	Sun Jul 31 10:27:41 2011 +0000
+++ b/Myhill_2.thy	Tue Aug 02 15:27:37 2011 +0000
@@ -1,6 +1,6 @@
 theory Myhill_2
-  imports Myhill_1 Prefix_subtract
-          "~~/src/HOL/Library/List_Prefix"
+  imports Myhill_1 
+  "~~/src/HOL/Library/List_Prefix"
 begin
 
 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
@@ -28,7 +28,6 @@
 apply(clarify, simp (no_asm_use))
 by metis
 
-
 lemma finite_eq_tag_rel:
   assumes rng_fnt: "finite (range tag)"
   shows "finite (UNIV // =tag=)"
@@ -225,72 +224,71 @@
 definition
   "Partitions s \<equiv> {(u, v). u @ v = s}"
 
-lemma conc_elim:
+lemma conc_partitions_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:
+lemma conc_partitions_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)
+lemma equiv_class_member:
+  assumes "x \<in> A"
+  and "\<approx>A `` {x} = \<approx>A `` {y}" 
+  shows "y \<in> A"
+using assms
+apply(simp add: Image_def str_eq_def set_eq_iff)
+apply(metis append_Nil2)
 done
 
-definition 
-  tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
+
+abbreviation
+  tag_Times_1 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
 where
-  "tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})"
+  "tag_Times_1 A B \<equiv> \<lambda>x. \<approx>A `` {x}"
+
+abbreviation
+  tag_Times_2 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
+where
+  "tag_Times_2 A B \<equiv> \<lambda>x. {(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}"
 
 definition 
-  tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
+  tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('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}))"
+  "tag_Times A B \<equiv> \<lambda>x. (tag_Times_1 A B x, tag_Times_2 A B x)"
 
-definition 
-  tag_Times3 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set"
-where
-  "tag_Times3 A B \<equiv>
-     (\<lambda>x. (tag_Times3a A B x, tag_Times3b A B x))"
-
-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"
+lemma tag_Times_injI:
+  assumes a: "tag_Times_1 A B x = tag_Times_1 A B y"
+  and     b: "tag_Times_2 A B x = tag_Times_2 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)
+    h3: "v \<in> B" by (auto dest: conc_partitions_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"
+    have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x"
+      unfolding Partitions_def using eq by auto
+    then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 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)
+      q3: "(u', us') \<in> Partitions y" by auto
     from q1 h2 have "u' \<in> A" 
-      using y unfolding Image_def str_eq_def by blast
+      using equiv_class_member by auto
     moreover from q2 h3 eq 
     have "us' @ z \<in> B"
       unfolding Image_def str_eq_def by auto
@@ -299,16 +297,14 @@
   }
   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"
+    have "(\<approx>A `` {x}) = tag_Times_1 A B x" by simp
+    then have "(\<approx>A `` {x}) = tag_Times_1 A B y"
       using a by simp
-    then have "\<approx>A `` {x} = \<approx>A `` {y}" 
-      unfolding tag_Times3a_def by simp
+    then have "\<approx>A `` {x} = \<approx>A `` {y}" by simp
     moreover 
     have "x @ us \<in> A" using h2 eq by simp
     ultimately 
-    have "y @ us \<in> A" using y 
+    have "y @ us \<in> A" using equiv_class_member 
       unfolding Image_def str_eq_def by blast
     then have "(y @ us) @ v \<in> A \<cdot> B" 
       using h3 unfolding conc_def by blast
@@ -317,88 +313,24 @@
   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)"
-using assms
-unfolding conc_def prefix_def
-by (auto simp add: append_eq_append_conv2)
-
-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_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 *)
-        fix x'
-        assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"
-        obtain y' 
-          where "y' \<le> y" 
-          and "y' \<in> A" 
-          and "(y - y') @ z \<in> B"
-        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_Times_def by simp
-          moreover 
-	  have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
-          ultimately 
-	  have "\<approx>B `` {x - x'} \<in> ?Right" by simp
-          then obtain y' 
-            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_def by auto
-          with h3 have "(y - y') @ z \<in> B" 
-	    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"
-	  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_Times_def by simp
-         with h2 have "y @ z' \<in> A"
-            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 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 by blast
-qed 
-
 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)
+  have "=(tag_Times A B)= \<subseteq> \<approx>(A \<cdot> B)"
+    apply(rule test_refined_intro)
+    apply(rule tag_Times_injI)
+    prefer 3
+    apply(assumption)
+    apply(simp add: tag_Times_def tag_eq_def)
+    apply(simp add: tag_eq_def tag_Times_def)
+    done
+  then show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y"
+    unfolding tag_eq_def by auto
 next
-  have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))" 
+  have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))" 
     using fin1 fin2 by auto
   show "finite (range (tag_Times A B))" 
     unfolding tag_Times_def
@@ -410,90 +342,29 @@
 
 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>"
+lemma append_eq_append_conv3:
+  assumes "xs @ ys = zs @ ts" "zs < xs"
+  shows "\<exists>us. xs = zs @ us \<and> us @ ys = ts"
 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)
-
+apply(auto simp add: append_eq_append_conv2 strict_prefix_def)
+done
 
-
-definition 
-  tag_Star3 :: "'a lang \<Rightarrow> 'a list \<Rightarrow> (bool \<times> 'a lang) set"
-where
-  "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> 
-           (\<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
-  case (insertI A a)
-  show ?case
-  proof (cases "A = {}")
-    case True thus ?thesis by (rule_tac x = a in bexI, auto)
-  next
-    case False
-    with insertI.hyps and False  
-    obtain max 
-      where h1: "max \<in> A" 
-      and h2: "\<forall>a\<in>A. f a \<le> f max" by blast
-    show ?thesis
-    proof (cases "f a \<le> f max")
-      assume "f a \<le> f max"
-      with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto)
-    next
-      assume "\<not> (f a \<le> f max)"
-      thus ?thesis using h2 by (rule_tac x = a in bexI, auto)
-    qed
-  qed
+lemma star_spartitions_elim:
+  assumes "x @ z \<in> A\<star>" "x \<noteq> []"
+  shows "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>"
+proof -
+  have "([], x @ z) \<in> Partitions (x @ z)" "[] < x" "[] \<in> A\<star>" "x @ z \<in> A\<star>"
+    using assms by (auto simp add: Partitions_def strict_prefix_def)
+  then show "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>"
+    by blast
 qed
 
 
-text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
+lemma finite_set_has_max2: 
+  "\<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 insert_iff linorder_linear order_trans)
 
 lemma finite_strict_prefix_set: 
   shows "finite {xa. xa < (x::'a list)}"
@@ -501,119 +372,162 @@
 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
 by (auto simp:strict_prefix_def)
 
+lemma append_eq_cases:
+  assumes a: "x @ y = m @ n" "m \<noteq> []"  
+  shows "x \<le> m \<or> m < x"
+unfolding prefix_def strict_prefix_def using a
+by (auto simp add: append_eq_append_conv2)
+
+lemma star_spartitions_elim2:
+  assumes a: "x @ z \<in> A\<star>" 
+  and     b: "x \<noteq> []"
+  shows "\<exists>(u, v) \<in> Partitions x. \<exists> (u', v') \<in> Partitions z. u < x \<and> u \<in> A\<star> \<and> v @ u' \<in> A \<and> v' \<in> A\<star>"
+proof -
+  def S \<equiv> "{u | u v. (u, v) \<in> Partitions x \<and> u < x \<and> u \<in> A\<star> \<and> v @ z \<in> A\<star>}"
+  have "finite {u. u < x}" by (rule finite_strict_prefix_set)
+  then have "finite S" unfolding S_def
+    by (rule rev_finite_subset) (auto)
+  moreover 
+  have "S \<noteq> {}" using a b unfolding S_def Partitions_def
+    by (auto simp: strict_prefix_def)
+  ultimately have "\<exists> u_max \<in> S. \<forall> u \<in> S. length u \<le> length u_max"  
+    using finite_set_has_max2 by blast
+  then obtain u_max v 
+    where h0: "(u_max, v) \<in> Partitions x"
+    and h1: "u_max < x" 
+    and h2: "u_max \<in> A\<star>" 
+    and h3: "v @ z \<in> A\<star>"  
+    and h4: "\<forall> u v. (u, v) \<in> Partitions x \<and> u < x \<and> u \<in> A\<star> \<and> v @ z \<in> A\<star> \<longrightarrow> length u \<le> length u_max"
+    unfolding S_def Partitions_def by blast
+  have q: "v \<noteq> []" using h0 h1 b unfolding Partitions_def by auto
+  from h3 obtain a b
+    where i1: "(a, b) \<in> Partitions (v @ z)"
+    and   i2: "a \<in> A"
+    and   i3: "b \<in> A\<star>"
+    and   i4: "a \<noteq> []"
+    unfolding Partitions_def
+    using q by (auto dest: star_decom)
+  have "v \<le> a"
+  proof (rule ccontr)
+    assume a: "\<not>(v \<le> a)"
+    from i1 have i1': "a @ b = v @ z" unfolding Partitions_def by simp
+    then have "a \<le> v \<or> v < a" using append_eq_cases q by blast
+    then have q: "a < v" using a unfolding strict_prefix_def prefix_def by auto
+    then obtain as where eq: "a @ as = v" unfolding strict_prefix_def prefix_def by auto
+    have "(u_max @ a, as) \<in> Partitions x" using eq h0 unfolding Partitions_def by auto
+    moreover
+    have "u_max @ a < x" using h0 eq q unfolding Partitions_def strict_prefix_def prefix_def by auto
+    moreover
+    have "u_max @ a \<in> A\<star>" using i2 h2 by simp
+    moreover
+    have "as @ z \<in> A\<star>" using i1' i2 i3 eq by auto
+    ultimately have "length (u_max @ a) \<le> length u_max" using h4 by blast
+    moreover
+    have "a \<noteq> []" using i4 .
+    ultimately show "False" by auto
+  qed
+  with i1 obtain za zb
+    where k1: "v @ za = a"
+    and   k2: "(za, zb) \<in> Partitions z" 
+    and   k4: "zb = b" 
+    unfolding Partitions_def prefix_def
+    by (auto simp add: append_eq_append_conv2)
+  show "\<exists> (u, v) \<in> Partitions x. \<exists> (u', v') \<in> Partitions z. u < x \<and> u \<in> A\<star> \<and> v @ u' \<in> A \<and> v' \<in> A\<star>"
+    using h0 k2 h1 h2 i2 k1 i3 k4 unfolding Partitions_def by blast
+qed
+
+
+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})"
+
 
 lemma tag_Star_injI:
-  fixes L\<^isub>1::"('a::finite) lang"
-  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_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_Star_def strict_prefix_def)
-      thus ?thesis using xz_in_star True by simp
-    next
-      case False
-      let ?S = "{xa::('a::finite) list. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
-      have "finite ?S"
-	by (rule_tac B = "{xa. xa < x}" in finite_subset)
-	   (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)
-      ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 
-        using finite_set_has_max by blast
-      then obtain xa_max 
-        where h1: "xa_max < x" 
-        and h2: "xa_max \<in> L\<^isub>1\<star>" 
-        and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" 
-        and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>  
-                                     \<longrightarrow> length xa \<le> length xa_max"
-        by blast
-      obtain ya 
-        where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" 
-        and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"
-      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_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_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> []"
-	    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>" 
-            and ab_max: "(x - xa_max) @ z = a @ b" by blast
-          let ?za = "a - (x - xa_max)" and ?zb = "b"
-          have pfx: "(x - xa_max) \<le> a" (is "?P1") 
-            and eq_z: "z = ?za @ ?zb" (is "?P2")
-          proof -
-            have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 
-              (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" 
-              using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
-            moreover {
-              assume np: "a < (x - xa_max)" 
-                and b_eqs: "((x - xa_max) - a) @ z = b"
-              have "False"
-              proof -
-                let ?xa_max' = "xa_max @ a"
-                have "?xa_max' < x" 
-                  using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 
-                moreover have "?xa_max' \<in> L\<^isub>1\<star>" 
-                  using a_in h2 by (auto)
-                moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 
-                  using b_eqs b_in np h1 by (simp add:diff_diff_append)
-                moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 
-                  using a_neq by simp
-                ultimately show ?thesis using h4 by blast
-              qed }
-            ultimately show ?P1 and ?P2 by auto
-          qed
-          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)
-           with eq_z and b_in 
-          show ?thesis using that by blast
-        qed
-        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb 
-	  by (rule_tac append_in_starI) (auto)
-        with eq_zab show ?thesis by simp
-      qed
-      with h5 h6 show ?thesis 	
-	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 by blast
-qed
+  fixes x::"'a list"
+  assumes a: "tag_Star A x = tag_Star A y"
+  and     c: "x @ z \<in> A\<star>"
+  and     d: "x \<noteq> []"
+  shows "y @ z \<in> A\<star>"
+using c d
+apply(drule_tac star_spartitions_elim2)
+apply(simp)
+apply(simp add: Partitions_def)
+apply(erule exE | erule conjE)+
+apply(subgoal_tac "((\<approx>A) `` {b}) \<in> tag_Star A x")
+apply(simp add: a)
+apply(simp add: tag_Star_def)
+apply(erule exE | erule conjE)+
+apply(simp add: test)
+apply(simp add: Partitions_def)
+apply(subgoal_tac "v @ aa \<in> A\<star>")
+prefer 2
+apply(simp add: str_eq_def)
+apply(subgoal_tac "(u @ v) @ aa @ ba \<in> A\<star>")
+apply(simp)
+apply(simp (no_asm_use))
+apply(rule append_in_starI)
+apply(simp)
+apply(simp (no_asm) only: append_assoc[symmetric])
+apply(rule append_in_starI)
+apply(simp)
+apply(simp)
+apply(simp add: tag_Star_def)
+apply(rule_tac x="a" in exI)
+apply(rule_tac x="b" in exI)
+apply(simp)
+apply(simp add: Partitions_def)
+done
+  
+lemma tag_Star_injI2:
+  fixes x::"'a list"
+  assumes a: "tag_Star A x = tag_Star A y"
+  and     c: "x @ z \<in> A\<star>"
+  and     d: "x = []"
+  shows "y @ z \<in> A\<star>"
+using c d
+apply(simp)
+using a
+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)
+
 
 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_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)
+  have "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
+    apply(rule test_refined_intro)
+    apply(case_tac "x=[]")
+    apply(rule tag_Star_injI2)
+    prefer 3
+    apply(assumption)
+    prefer 2
+    apply(assumption)
+    apply(simp add: tag_eq_def)
+    apply(rule tag_Star_injI)
+    prefer 3
+    apply(assumption)
+    prefer 2
+    apply(assumption)
+    unfolding tag_eq_def
+    apply(simp)
+    done
+  then show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
+    apply(simp add: tag_eq_def)
+    apply(auto)
+    done
 next
   have *: "finite (Pow (UNIV // \<approx>A))" 
-    using finite1 by auto
+     using finite1 by auto
   show "finite (range (tag_Star A))"
     unfolding tag_Star_def
     apply(rule finite_subset[OF _ *])
     unfolding quotient_def
-    by auto
+    apply(auto)
+    done
 qed
 
 subsubsection{* The conclusion *}
diff -r 97090fc7aa9f -r 560712a29a36 Prefix_subtract.thy
--- a/Prefix_subtract.thy	Sun Jul 31 10:27:41 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-theory Prefix_subtract
-  imports Main "~~/src/HOL/Library/List_Prefix"
-begin
-
-
-section {* A small theory of prefix subtraction *}
-
-text {*
-  The notion of @{text "prefix_subtract"} makes 
-  the second direction of the Myhill-Nerode theorem 
-  more readable.
-*}
-
-instantiation list :: (type) minus
-begin
-
-fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
-where
-  "minus_list []     xs     = []" 
-| "minus_list (x#xs) []     = x#xs" 
-| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"
-
-instance by default
-
-end
-
-lemma [simp]: "x - [] = x"
-by (induct x) (auto)
-
-lemma [simp]: "(x @ y) - x = y"
-by (induct x) (auto)
-
-lemma [simp]: "x - x = []"
-by (induct x) (auto)
-
-lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "
-by (induct x) (auto)
-
-lemma diff_prefix:
-  "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
-by (auto elim: prefixE)
-
-lemma diff_diff_append: 
-  "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
-apply (clarsimp simp:strict_prefix_def)
-by (drule diff_prefix, auto elim:prefixE)
-
-lemma append_eq_cases:
-  assumes a: "x @ y = m @ n"
-  shows "x \<le> m \<or> m \<le> x"
-unfolding prefix_def using a
-by (auto simp add: append_eq_append_conv2)
-
-lemma append_eq_dest:
-  assumes a: "x @ y = m @ n" 
-  shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
-using append_eq_cases[OF a] a
-by (auto elim: prefixE)
-
-end