# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1457289643 0
# Node ID 79efc0bcfc9657b586dd29aeb63596e0ec5e6fe9
# Parent  2c4ffcc9539939763cc675cb04ae47f98999dd27
updated

diff -r 2c4ffcc95399 -r 79efc0bcfc96 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Sun Mar 06 16:51:32 2016 +0000
+++ b/thys/Paper/Paper.thy	Sun Mar 06 18:40:43 2016 +0000
@@ -13,8 +13,8 @@
 
 notation (latex output)
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
-  Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,75] 73) and
-  
+  Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,75] 73) and  
+
   ZERO ("\<^bold>0" 78) and 
   ONE ("\<^bold>1" 78) and 
   CHAR ("_" [1000] 80) and
@@ -38,6 +38,7 @@
   mkeps ("mkeps _" [79] 76) and 
   projval ("proj _ _ _" [1000,77,1000] 77) and 
   length ("len _" [78] 73) and
+  matcher ("lexer _ _" [78,78] 77) and
 
   Prf ("\<triangleright> _ : _" [75,75] 75) and  
   PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75)
@@ -463,26 +464,26 @@
   the shape of values.
 
   \begin{center}
-  \begin{tabular}{lcl}
-  @{thm (lhs) injval.simps(1)[of "d" "DUMMY"]} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
-  @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
+  \begin{tabular}{llcl}
+  (1) & @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
+  (2) & @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & 
       @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
-  @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
+  (3) & @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & 
       @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
-  @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+  (4) & @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
       & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
-  @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
+  (5) & @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ 
       & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
-  @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
+  (6) & @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ 
       & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
-  @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 
+  (7) & @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ 
       & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\
   \end{tabular}
   \end{center}
 
   \noindent To better understand what is going on in this definition it
   might be instructive to look first at the three sequence cases (clauses
-  4--6). In each case we need to construct an ``injected value'' for @{term
+  (4)--(6)). In each case we need to construct an ``injected value'' for @{term
   "SEQ r\<^sub>1 r\<^sub>2"}. Recall the clause of the @{const der}-function
   for sequence regular expressions:
 
@@ -492,18 +493,39 @@
 
   \noindent Consider first the else-branch where the derivative is @{term
   "SEQ (der c r\<^sub>1) r\<^sub>2"}. The corresponding value must therefore
-  be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches the fourth
-  clause of @{term inj}. In the if-branch the derivative is an alternative,
-  namely @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}.
-  This means we either have to consider a @{text Left}- or @{text
-  Right}-value. In case of the @{text Left}-value we know further it must be 
-  a value for a sequence regular expression. Therefore the pattern we
-  match in the fifth clause is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while
-  in the sixth it is just @{term "Right v\<^sub>2"}. One more interesting point
-  is in the right-hand side of the sixth clause: since in this case the regular
-  expression @{text "r\<^sub>1"} does not ``contribute'' in matching the string,
-  that is only matches the empty string, we need to call @{const mkeps} in order 
-  to construct a value how @{term "r\<^sub>1"} can match this empty string.
+  be the form @{term "Seq v\<^sub>1 v\<^sub>2"}, which matches clause (4) of
+  @{term inj}. In the if-branch the derivative is an alternative, namely
+  @{term "ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2)"}. This
+  means we either have to consider a @{text Left}- or @{text Right}-value.
+  In case of the @{text Left}-value we know further it must be a value for a
+  sequence regular expression. Therefore the pattern we match in the clause
+  (5) is @{term "Left (Seq v\<^sub>1 v\<^sub>2)"}, while in (6) it is just
+  @{term "Right v\<^sub>2"}. One more interesting point is in the right-hand
+  side of clause (6): since in this case the regular expression @{text
+  "r\<^sub>1"} does not ``contribute'' in matching the string, that is only
+  matches the empty string, we need to call @{const mkeps} in order to
+  construct a value how @{term "r\<^sub>1"} can match this empty string. A
+  similar argument applies for why we can expect in clause (7) that the
+  value is of the form @{term "Seq v (Stars vs)"} (the derivative of a star
+  is @{term "SEQ r (STAR r)"}). Finally, the reason for why we can ignore
+  the second argument in clause (1) of @{term inj} is that it will only ever
+  be called in cases where @{term "c=d"}, but the usual linearity
+  restrictions in pattern-matches do not allow is to build this constraint
+  explicitly into the pattern.
+
+  Having defined the @{const mkeps} and @{text inj} function we can extend
+  \Brz's matcher so that a [lexical] value is constructed (assuming the
+  regular expression matches the string). The clauses of the lexer are
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{thm (lhs) matcher.simps(1)} & $\dn$ & @{thm (rhs) matcher.simps(1)}\\
+  @{thm (lhs) matcher.simps(2)} & $\dn$ & @{text "case"} @{term "matcher (der c r) s"} @{text of}\\
+                     & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\
+                     & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}                          
+  \end{tabular}
+  \end{center}
+
 
 
   NOT DONE YET 
diff -r 2c4ffcc95399 -r 79efc0bcfc96 thys/paper.pdf
Binary file thys/paper.pdf has changed