diff -r 560712a29a36 -r c4893e84c88e Myhill_2.thy
--- a/Myhill_2.thy	Tue Aug 02 15:27:37 2011 +0000
+++ b/Myhill_2.thy	Wed Aug 03 00:52:41 2011 +0000
@@ -15,16 +15,14 @@
 where
    "x =tag= y \<equiv> (x, y) \<in> =tag="
 
-lemma test:
+lemma [simp]:
   shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"
-unfolding str_eq_def
-by auto
+unfolding str_eq_def by auto
 
-lemma test_refined_intro:
+lemma 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
+using assms unfolding str_eq_def tag_eq_def
 apply(clarify, simp (no_asm_use))
 by metis
 
@@ -103,14 +101,13 @@
 
 lemma tag_finite_imageD:
   assumes rng_fnt: "finite (range tag)" 
-  and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
+  and same_tag_eqvt: "=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" unfolding tag_eq_def str_eq_def
-    by blast
+  show "=tag= \<subseteq> \<approx>A" .
 next
   show "equiv UNIV =tag="
     unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
@@ -199,7 +196,7 @@
 definition 
   tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
 where
-  "tag_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_plus_finiteI [intro]:
   assumes finite1: "finite (UNIV // \<approx>A)"
@@ -212,14 +209,12 @@
     unfolding tag_Plus_def quotient_def
     by (rule rev_finite_subset) (auto)
 next
-  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
-    by auto
+  show "=tag_Plus A B= \<subseteq> \<approx>(A \<union> B)"
+    unfolding tag_eq_def tag_Plus_def str_eq_def by auto
 qed
 
 
-subsubsection {* The inductive case for @{text "Times"}*}
+subsubsection {* The inductive case for @{text "Times"} *}
 
 definition
   "Partitions s \<equiv> {(u, v). u @ v = s}"
@@ -227,15 +222,13 @@
 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
+using assms unfolding conc_def Partitions_def
 by auto
 
 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
+using assms unfolding conc_def Partitions_def
 by auto
 
 lemma equiv_class_member:
@@ -243,7 +236,8 @@
   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(simp)
+apply(simp add: str_eq_def)
 apply(metis append_Nil2)
 done
 
@@ -280,7 +274,7 @@
   moreover
   { assume eq: "x = u @ us" "us @ z = v"
     have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x"
-      unfolding Partitions_def using eq by auto
+      unfolding Partitions_def using eq by (auto simp add: str_eq_def)
     then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B y"
       using b by simp
     then obtain u' us' where
@@ -314,21 +308,16 @@
 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)
-  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
+  have "\<And>x y z. \<lbrakk>tag_Times A B x = tag_Times A B y; x @ z \<in> A \<cdot> B\<rbrakk> \<Longrightarrow> y @ z \<in> A \<cdot> B"
+    by (rule tag_Times_injI)
+       (auto simp add: tag_Times_def tag_eq_def)
+  then show "=tag_Times A B= \<subseteq> \<approx>(A \<cdot> B)"
+    by (rule refined_intro)
+       (auto simp add: tag_eq_def)
 next
   have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))" 
     using fin1 fin2 by auto
@@ -342,14 +331,7 @@
 
 subsubsection {* The inductive case for @{const "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(auto simp add: append_eq_append_conv2 strict_prefix_def)
-done
-
-lemma star_spartitions_elim:
+lemma star_partitions_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 -
@@ -359,7 +341,6 @@
     by blast
 qed
 
-
 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)
@@ -422,9 +403,7 @@
     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
+    with i4 show "False" by auto
   qed
   with i1 obtain za zb
     where k1: "v @ za = a"
@@ -433,107 +412,75 @@
     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
+    using h0 h1 h2 i2 i3 k1 k2 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 x::"'a list"
+lemma tag_Star_non_empty_injI:
   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"
+proof -
+  obtain u v u' v' 
+    where a1: "(u,  v) \<in> Partitions x" "(u', v')\<in> Partitions z"
+    and   a2: "u < x"
+    and   a3: "u \<in> A\<star>"
+    and   a4: "v @ u' \<in> A" 
+    and   a5: "v' \<in> A\<star>"
+    using c d by (auto dest: star_spartitions_elim2)
+  have "(\<approx>A) `` {v} \<in> tag_Star A x" 
+    apply(simp add: tag_Star_def Partitions_def str_eq_def)
+    using a1 a2 a3 by (auto simp add: Partitions_def)
+  then have "(\<approx>A) `` {v} \<in> tag_Star A y" using a by simp
+  then obtain u1 v1 
+    where b1: "v \<approx>A v1"
+    and   b3: "u1 \<in> A\<star>"
+    and   b4: "(u1, v1) \<in> Partitions y"
+    unfolding tag_Star_def by auto
+  have c: "v1 @ u' \<in> A\<star>" using b1 a4 unfolding str_eq_def by simp
+  have "u1 @ (v1 @ u') @ v' \<in> A\<star>"
+    using b3 c a5 by (simp only: append_in_starI)
+  then show "y @ z \<in> A\<star>" using b4 a1 
+    unfolding Partitions_def by auto
+qed
+    
+lemma tag_Star_empty_injI:
   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
+using assms
 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)
-  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
+  have "\<And>x y z. \<lbrakk>tag_Star A x = tag_Star A y; x @ z \<in> A\<star>\<rbrakk> \<Longrightarrow> y @ z \<in> A\<star>"
+    by (case_tac "x = []") (blast intro: tag_Star_empty_injI tag_Star_non_empty_injI)+
+  then show "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
+    by (rule refined_intro) (auto simp add: tag_eq_def)
 next
   have *: "finite (Pow (UNIV // \<approx>A))" 
      using finite1 by auto
   show "finite (range (tag_Star A))"
-    unfolding tag_Star_def
-    apply(rule finite_subset[OF _ *])
-    unfolding quotient_def
-    apply(auto)
-    done
+    unfolding tag_Star_def 
+    by (rule finite_subset[OF _ *])
+       (auto simp add: quotient_def)
 qed
 
 subsubsection{* The conclusion *}
 
 lemma Myhill_Nerode2:
-  fixes r::"('a::finite) rexp"
+  fixes r::"'a rexp"
   shows "finite (UNIV // \<approx>(lang r))"
 by (induct r) (auto)
 
@@ -542,4 +489,4 @@
   shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
 using Myhill_Nerode1 Myhill_Nerode2 by auto
 
-end
+end
\ No newline at end of file