# HG changeset patch
# User urbanc
# Date 1298187234 0
# Node ID 8233510cab6c6bf1257b4c545edf42247f3e61ef
# Parent  23c0e6f2929d5182bd00fb3bcda6f588c6fe28eb
added definition of string prefix and string subtraction

diff -r 23c0e6f2929d -r 8233510cab6c Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 06:02:58 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 07:33:54 2011 +0000
@@ -1018,8 +1018,28 @@
 
   \noindent
   using the information given by the appropriate tagging function. The complication 
-  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}.
+  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
+  (this was easy in case of @{term "A \<union> B"}). For this we define the
+  notions of \emph{string prefixes} 
+
+  \begin{center}
+  @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+  @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+  \end{center}
 
+  \noindent
+  and \emph{string subtraction}:
+
+  \begin{center}
+  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
+  @{text "x - []"} & @{text "\<equiv>"} & @{text x}\\
+  @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
 
   \begin{proof}[@{const SEQ}-Case]