--- a/thys/Lexer.thy	Mon Aug 19 16:24:28 2019 +0100
+++ b/thys/Lexer.thy	Tue Aug 20 23:42:28 2019 +0200
@@ -286,6 +286,11 @@
   apply(simp_all add: comp_def)
   by meson
 
+lemma flex_fun_apply2:
+  shows "g (flex r id s v) = flex r g s v"
+  by (simp add: flex_fun_apply)
+
+
 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)
@@ -397,7 +402,14 @@
   shows "flex (der a r) (injval r a) s v = injval r a (flex (der a r) id s v)"
   by (simp add: flex_fun_apply)
   
-
-
+lemma Prf_flex:
+  assumes "\<Turnstile> v : ders s r"
+  shows "\<Turnstile> flex r id s v : r"
+  using assms
+  apply(induct s arbitrary: v r)
+  apply(simp)
+  apply(simp)
+  by (simp add: Prf_injval flex_injval)
+  
 
 end
\ No newline at end of file