# HG changeset patch
# User urbanc
# Date 1298206264 0
# Node ID 6d2693c78c37584d6b26e1b6d847225f1b2dc2e2
# Parent  8440863a9900f6eaed009a609e15ebfac2d8b2ee
finished picture

diff -r 8440863a9900 -r 6d2693c78c37 Myhill_2.thy
--- a/Myhill_2.thy	Sun Feb 20 11:14:07 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 20 12:51:04 2011 +0000
@@ -481,7 +481,7 @@
 definition 
   tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
 where
-  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - x'} | x'. x' < x \<and> x' \<in> L1\<star>})"
 
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 
diff -r 8440863a9900 -r 6d2693c78c37 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 11:14:07 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 12:51:04 2011 +0000
@@ -1046,17 +1046,17 @@
   \begin{center}
   \scalebox{0.7}{
   \begin{tikzpicture}
-    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}x'\hspace{4em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - x'\hspace{0.5em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}z\hspace{10.1em}$ };
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'"}\hspace{4em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'"}\hspace{0.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}@{text z}\hspace{10.1em}$ };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
-               node[midway, above=0.5em]{$x$};
+               node[midway, above=0.5em]{@{text x}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            (z.north west) -- ($(z.north east)+(0em,0em)$)
-               node[midway, above=0.5em]{$z$};
+               node[midway, above=0.5em]{@{text z}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
@@ -1073,17 +1073,17 @@
 
   \scalebox{0.7}{
   \begin{tikzpicture}
-    \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}z'\hspace{2em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - z'\hspace{6.1em}$  };
+    \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}@{text x}\hspace{6.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}@{text "z'"}\hspace{2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}@{text "z - z'"}\hspace{6.1em}$  };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            (x.north west) -- ($(za.north west)+(0em,0em)$)
-               node[midway, above=0.5em]{$x$};
+               node[midway, above=0.5em]{@{text x}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
-               node[midway, above=0.8em]{$z$};
+               node[midway, above=0.5em]{@{text z}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
@@ -1124,7 +1124,8 @@
   \end{center}
 
   \noindent
-  There are two cases to be considered. First, there exists a @{text "x'"} such that
+  There are two cases to be considered (see pictures above). 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}
@@ -1152,12 +1153,77 @@
   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}
+  
+  \noindent
+  The case for @{const STAR} is similar, but poses a few extra challenges. When
+  we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"}, we 
+  have the following picture:
 
-  \begin{proof}[@{const STAR}-Case]
+  \begin{center}
+  \scalebox{0.7}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text x}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (za.north west) -- ($(zb.north east)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text z}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "z\<^isub>b \<in> A\<star>"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+               node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
+  \end{tikzpicture}}
+  \end{center}
+
+  \noindent
+  We can find a prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"}
+  and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string 
+  @{text "[]"} would do.
+  There are many such prefixes, but there can only be finitely many of them (the 
+  string @{text x} is finite). Let us therefore choose the longest one and call it 
+  @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
+  know it is in @{text "A\<star>"}. By definition of @{text "A\<star>"}, we can separate
+  this string into two parts, say @{text "a"} and @{text "b"}, such @{text "a \<in> A"}
+  and @{text "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
+  otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
+  `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
+   @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
+  @{text "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{text "x @ z \<in> A\<star>"}
+  such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
+  `border' of @{text x} and @{text z}. This string is @{text "(x - x') @ z\<^isub>a"}.
+
+  In order to show that @{text "x @ z \<in> A\<star>"} implies @{text "y @ z \<in> A\<star>"}, we use
+  the following tagging-function:
 
   \begin{center}
   @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
   \end{center}
+
+  \begin{proof}[@{const STAR}-Case]
+
+
   \end{proof}
 *}