--- 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))))"