--- a/Myhill_2.thy	Wed Aug 03 00:52:41 2011 +0000
+++ b/Myhill_2.thy	Wed Aug 03 12:36:23 2011 +0000
@@ -217,7 +217,7 @@
 subsubsection {* The inductive case for @{text "Times"} *}
 
 definition
-  "Partitions s \<equiv> {(u, v). u @ v = s}"
+  "Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}"
 
 lemma conc_partitions_elim:
   assumes "x \<in> A \<cdot> B"
@@ -241,25 +241,13 @@
 apply(metis append_Nil2)
 done
 
-
-abbreviation
-  tag_Times_1 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
+definition 
+  tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> 'a lang set"
 where
-  "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_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set"
-where
-  "tag_Times A B \<equiv> \<lambda>x. (tag_Times_1 A B x, tag_Times_2 A B x)"
+  "tag_Times A B \<equiv> \<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x\<^isub>s}) | x\<^isub>p x\<^isub>s. x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"
 
 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"
+  assumes a: "tag_Times A B x = tag_Times A B y"
   and     c: "x @ z \<in> A \<cdot> B"
   shows "y @ z \<in> A \<cdot> B"
 proof -
@@ -273,28 +261,30 @@
     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_Times_2 A B x"
-      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
+    have "(\<approx>B `` {us}) \<in> snd (tag_Times A B x)"
+      unfolding Partitions_def tag_Times_def using h2 eq 
+      by (auto simp add: str_eq_def)
+    then have "(\<approx>B `` {us}) \<in> snd (tag_Times A B y)"
+      using a by simp
     then obtain u' us' where
-      q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and
+      q1: "u' \<in> A" and
       q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and
-      q3: "(u', us') \<in> Partitions y" by auto
-    from q1 h2 have "u' \<in> A" 
-      using equiv_class_member by auto
-    moreover from q2 h3 eq 
+      q3: "(u', us') \<in> Partitions y" 
+      unfolding tag_Times_def by auto
+    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 
+    then have "y @ z \<in> A \<cdot> B" using q1 q3 
       unfolding Partitions_def by auto
   }
   moreover
   { assume eq: "x @ us = u" "z = us @ v"
-    have "(\<approx>A `` {x}) = tag_Times_1 A B x" by simp
-    then have "(\<approx>A `` {x}) = tag_Times_1 A B y"
+    have "(\<approx>A `` {x}) = fst (tag_Times A B x)" 
+      by (simp add: tag_Times_def)
+    then have "(\<approx>A `` {x}) = fst (tag_Times A B y)"
       using a by simp
-    then have "\<approx>A `` {x} = \<approx>A `` {y}" by simp
+    then have "\<approx>A `` {x} = \<approx>A `` {y}" 
+      by (simp add: tag_Times_def)
     moreover 
     have "x @ us \<in> A" using h2 eq by simp
     ultimately 
@@ -319,7 +309,7 @@
     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)))" 
+  have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))" 
     using fin1 fin2 by auto
   show "finite (range (tag_Times A B))" 
     unfolding tag_Times_def