--- a/thys/Paper/Paper.thy	Fri Mar 11 00:56:46 2016 +0000
+++ b/thys/Paper/Paper.thy	Fri Mar 11 10:43:44 2016 +0000
@@ -36,14 +36,12 @@
   Sequ ("_ @ _" [78,77] 63) and
   injval ("inj _ _ _" [79,77,79] 76) and 
   mkeps ("mkeps _" [79] 76) and 
-  (*projval ("proj _ _ _" [1000,77,1000] 77) and*) 
   length ("len _" [78] 73) and
-  matcher ("lexer _ _" [78,78] 77) and
-
+ 
   Prf ("_ : _" [75,75] 75) and  
   PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
-  (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *)
-  
+ 
+  lexer ("lexer _ _" [78,78] 77) and 
   F_RIGHT ("F\<^bsub>Right\<^esub> _") and
   F_LEFT ("F\<^bsub>Left\<^esub> _") and  
   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and
@@ -52,7 +50,7 @@
   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and
   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
-  matcher3 ("lexer\<^sup>+ _ _" [78,78] 77)
+  slexer ("lexer\<^sup>+ _ _" [78,78] 77)
 
 definition 
   "match r s \<equiv> nullable (ders s r)"
@@ -558,8 +556,8 @@
 
   \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}\\
+  @{thm (lhs) lexer.simps(1)} & $\dn$ & @{thm (rhs) lexer.simps(1)}\\
+  @{thm (lhs) lexer.simps(2)} & $\dn$ & @{text "case"} @{term "lexer (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}
@@ -870,10 +868,10 @@
   
   \begin{center}
   \begin{tabular}{lcl}
-  @{thm (lhs) matcher3.simps(1)} & $\dn$ & @{thm (rhs) matcher3.simps(1)}\\
-  @{thm (lhs) matcher3.simps(2)} & $\dn$ & 
+  @{thm (lhs) slexer.simps(1)} & $\dn$ & @{thm (rhs) slexer.simps(1)}\\
+  @{thm (lhs) slexer.simps(2)} & $\dn$ & 
                          @{text "let (r\<^sub>s, f\<^sub>r) = simp (r "}$\backslash$@{text " c) in"}\\
-                     & & @{text "case"} @{term "matcher3 r\<^sub>s s"} @{text of}\\
+                     & & @{text "case"} @{term "slexer r\<^sub>s s"} @{text of}\\
                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\
                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"}                          
   \end{tabular}
@@ -888,7 +886,7 @@
   it (that is construct @{term "f\<^sub>r v"}). We can prove that
 
   \begin{lemma}
-  @{term "matcher3 r s = matcher r s"}
+  @{term "slexer r s = lexer r s"}
   \end{lemma}
 
   \noindent

--- a/thys/ReStar.thy	Fri Mar 11 00:56:46 2016 +0000
+++ b/thys/ReStar.thy	Fri Mar 11 10:43:44 2016 +0000
@@ -24,7 +24,7 @@
 by (simp_all add: Sequ_def)
 
 
-section {* Semantic Derivative of Languages *}
+section {* Semantic Derivative (Left Quotient) of Languages *}
 
 definition
   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
@@ -272,7 +272,7 @@
 done
 
 
-section {* Sulzmann functions *}
+section {* Sulzmann and Lu functions *}
 
 fun 
   mkeps :: "rexp \<Rightarrow> val"
@@ -293,17 +293,6 @@
 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
 
 
-section {* Matcher *}
-
-fun 
-  matcher :: "rexp \<Rightarrow> string \<Rightarrow> val option"
-where
-  "matcher r [] = (if nullable r then Some(mkeps r) else None)"
-| "matcher r (c#s) = (case (matcher (der c r) s) of  
-                    None \<Rightarrow> None
-                  | Some(v) \<Rightarrow> Some(injval r c v))"
-
-
 section {* Mkeps, injval *}
 
 lemma mkeps_nullable:
@@ -605,9 +594,22 @@
     qed
 qed
 
+
+section {* The Lexer by Sulzmann and Lu  *}
+
+fun 
+  lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+where
+  "lexer r [] = (if nullable r then Some(mkeps r) else None)"
+| "lexer r (c#s) = (case (lexer (der c r) s) of  
+                    None \<Rightarrow> None
+                  | Some(v) \<Rightarrow> Some(injval r c v))"
+
+
+
 lemma lex_correct1:
   assumes "s \<notin> L r"
-  shows "matcher r s = None"
+  shows "lexer r s = None"
 using assms
 apply(induct s arbitrary: r)
 apply(simp add: nullable_correctness)
@@ -616,7 +618,7 @@
 done
 
 lemma lex_correct1a:
-  shows "s \<notin> L r \<longleftrightarrow> matcher r s = None"
+  shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
 using assms
 apply(induct s arbitrary: r)
 apply(simp add: nullable_correctness)
@@ -626,7 +628,7 @@
 
 lemma lex_correct2:
   assumes "s \<in> L r"
-  shows "\<exists>v. matcher r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
+  shows "\<exists>v. lexer r s = Some(v) \<and> \<turnstile> v : r \<and> flat v = s"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
@@ -641,7 +643,7 @@
 
 lemma lex_correct3:
   assumes "s \<in> L r"
-  shows "\<exists>v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v"
+  shows "\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
@@ -653,7 +655,7 @@
 by (metis PMatch2_roy_version)
 
 lemma lex_correct3a:
-  shows "s \<in> L r \<longleftrightarrow> (\<exists>v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
+  shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
@@ -668,14 +670,14 @@
 by (simp add: lex_correct1a)
 
 lemma lex_correct3b:
-  shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. matcher r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
+  shows "s \<in> L r \<longleftrightarrow> (\<exists>!v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
 using assms
 apply(induct s arbitrary: r)
 apply(simp)
 apply (metis PMatch_mkeps nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
 apply(simp add: der_correctness Der_def)
-apply(case_tac "matcher (der a r) s = None")
+apply(case_tac "lexer (der a r) s = None")
 apply(simp)
 apply(simp)
 apply(clarify)
@@ -685,6 +687,8 @@
 apply(simp)
 using PMatch1(1) by auto
 
+section {* Lexer including simplifications *}
+
 
 fun F_RIGHT where
   "F_RIGHT f v = Right (f v)"
@@ -723,11 +727,11 @@
 | "simp r = (r, id)"
 
 fun 
-  matcher3 :: "rexp \<Rightarrow> string \<Rightarrow> val option"
+  slexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
 where
-  "matcher3 r [] = (if nullable r then Some(mkeps r) else None)"
-| "matcher3 r (c#s) = (let (rs, fr) = simp (der c r) in
-                         (case (matcher3 rs s) of  
+  "slexer r [] = (if nullable r then Some(mkeps r) else None)"
+| "slexer r (c#s) = (let (rs, fr) = simp (der c r) in
+                         (case (slexer rs s) of  
                             None \<Rightarrow> None
                           | Some(v) \<Rightarrow> Some(injval r c (fr v))))"
 

Binary file thys/paper.pdf has changed