# HG changeset patch
# User urbanc
# Date 1298146559 0
# Node ID c1f596c7f59ecd20734bdb08c991ead4b1eb666b
# Parent  ece3f197b92b26aa34ed534b11a8eb36010792c3
ALT case done

diff -r ece3f197b92b -r c1f596c7f59e Myhill_2.thy
--- a/Myhill_2.thy	Sat Feb 19 19:27:33 2011 +0000
+++ b/Myhill_2.thy	Sat Feb 19 20:15:59 2011 +0000
@@ -275,7 +275,7 @@
     by (rule rev_finite_subset) (auto)
 next
   show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
-    unfolding tag_str_ALT_def 
+    unfolding tag_str_ALT_def
     unfolding str_eq_def
     unfolding str_eq_rel_def
     by auto
diff -r ece3f197b92b -r c1f596c7f59e Paper/Paper.thy
--- a/Paper/Paper.thy	Sat Feb 19 19:27:33 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 20:15:59 2011 +0000
@@ -976,9 +976,26 @@
   where @{text "A"} and @{text "B"} are some arbitrary languages.
   We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
   then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
-  @{term "tag_str_ALT A B"} is a subset of this. It remains to be shown
-  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T="} refines @{text "\<approx>(A \<union> B)"}.
+  @{term "tag_str_ALT A B"} is a subset of this product set. It remains to show
+  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
+  showing
+  %
+  \begin{center}
+  @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+  \end{center}
 
+  \noindent
+  which by unfolding the Myhill-Nerode relation is identical to
+  %
+  \begin{equation}\label{pattern}
+  @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
+  \end{equation}
+
+  \noindent
+  since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
+  \eqref{pattern} we just have to unfold the tagging-relation and analyse 
+  in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. Fianlly we
+  can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
   \end{proof}