# HG changeset patch
# User urbanc
# Date 1298200447 0
# Node ID 8440863a9900f6eaed009a609e15ebfac2d8b2ee
# Parent  c7fdc28b8a76a578d4ae4eb0788f7b4264516138
seq case finished

diff -r c7fdc28b8a76 -r 8440863a9900 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 09:54:24 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 11:14:07 2011 +0000
@@ -981,7 +981,7 @@
   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 product set, so finite. It remains to be shown
+  @{term "tag_str_ALT A B"} is a subset of this product set---so finite. It remains to be shown
   that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
   showing
   %
@@ -1040,8 +1040,8 @@
 
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
-  Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways how this string
-  can be `distributed'  over @{term "A ;; B"}:
+  Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' 
+  this string to be in @{term "A ;; B"}:
 
   \begin{center}
   \scalebox{0.7}{
@@ -1110,11 +1110,47 @@
   \end{center}
 
   \noindent
-  with the idea ???
+  with the idea that in the first split we have to make sure that @{text "x - x'"}
+  is in the language @{text B}.
 
   \begin{proof}[@{const SEQ}-Case]
+  If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+  then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
+  @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
+  We have to show injectivity of this tagging function as
 
+  \begin{center}
+  @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+  \end{center}
 
+  \noindent
+  There are two cases to be considered. First, there exists a @{text "x'"} such that
+  @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
+  
+  \begin{center}
+  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
+  \end{center}
+
+  \noindent
+  and by the assumption about @{term "tag_str_SEQ A B"} also 
+
+  \begin{center}
+  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
+  \end{center}
+
+  \noindent
+  That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 
+  @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
+  @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
+  relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
+  have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
+  @{term "y @ z \<in> A ;; B"}, as needed in this case.
+
+  Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
+  By the assumption about @{term "tag_str_SEQ A B"} we have
+  @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
+  relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude aslo in this case
+  with @{term "y @ z \<in> A ;; B"}. That completes the @{const SEQ}-case.\qed 
   \end{proof}
 
   \begin{proof}[@{const STAR}-Case]