--- a/thys/Lexer.thy	Wed May 16 20:58:39 2018 +0100
+++ b/thys/Lexer.thy	Wed Aug 15 13:48:57 2018 +0100
@@ -53,7 +53,7 @@
   assumes "\<Turnstile> v : der c r" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
-apply(induct arbitrary: v rule: der.induct)
+apply(induct c r arbitrary: v rule: der.induct)
 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 done
 
@@ -238,20 +238,33 @@
 
 lemma lexer_correct_None:
   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
-apply(induct s arbitrary: r)
-apply(simp add: nullable_correctness)
-apply(drule_tac x="der a r" in meta_spec)
-apply(auto simp add: der_correctness Der_def)
+  apply(induct s arbitrary: r)
+  apply(simp)
+  apply(simp add: nullable_correctness)
+  apply(simp)
+  apply(drule_tac x="der a r" in meta_spec) 
+  apply(auto)
+  apply(auto simp add: der_correctness Der_def)
 done
 
 lemma lexer_correct_Some:
   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
-apply(induct s arbitrary: r)
-apply(auto simp add: Posix_mkeps nullable_correctness)[1]
-apply(drule_tac x="der a r" in meta_spec)
-apply(simp add: der_correctness Der_def)
-apply(rule iffI)
-apply(auto intro: Posix_injval simp add: Posix1(1))
+  apply(induct s arbitrary : r)
+  apply(simp only: lexer.simps)
+  apply(simp)
+  apply(simp add: nullable_correctness Posix_mkeps)
+  apply(drule_tac x="der a r" in meta_spec)
+  apply(simp (no_asm_use) add: der_correctness Der_def del: lexer.simps) 
+  apply(simp del: lexer.simps)
+  apply(simp only: lexer.simps)
+  apply(case_tac "lexer (der a r) s = None")
+   apply(auto)[1]
+  apply(simp)
+  apply(erule exE)
+  apply(simp)
+  apply(rule iffI)
+  apply(simp add: Posix_injval)
+  apply(simp add: Posix1(1))
 done 
 
 lemma lexer_correctness:
@@ -260,4 +273,37 @@
 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
 using Posix1(1) lexer_correct_None lexer_correct_Some by blast
 
+
+
+
+fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)"
+  where
+  "flex r f [] = f"
+| "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s"  
+
+lemma flex_fun_apply:
+  shows "g (flex r f s v) = flex r (g o f) s v"
+  apply(induct s arbitrary: g f r v)
+  apply(simp_all add: comp_def)
+  by meson
+
+lemma flex_append:
+  shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
+  apply(induct s1 arbitrary: s2 r f)
+   apply(simp)
+  apply(drule_tac x="s2" in meta_spec)
+  apply(drule_tac x="der a r" in meta_spec)
+  apply(simp)
+  done  
+
+lemma lexer_flex:
+  shows "lexer r s = (if nullable (ders s r) 
+                      then Some(flex r id s (mkeps (ders s r))) else None)"
+  apply(induct s arbitrary: r)
+  apply(simp)
+  apply(simp add: flex_fun_apply)
+  done  
+
+unused_thms
+
 end
\ No newline at end of file