diff -r a730a5a0bab9 -r 89e6605c4ca4 thys/Lexer.thy
--- a/thys/Lexer.thy	Tue Jul 23 21:21:49 2019 +0100
+++ b/thys/Lexer.thy	Mon Jul 29 09:37:20 2019 +0100
@@ -299,6 +299,105 @@
   apply(simp_all add: flex_fun_apply)
   done  
 
-unused_thms
+lemma Posix_flex:
+  assumes "s2 \<in> (ders s1 r) \<rightarrow> v"
+  shows "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v"
+  using assms
+  apply(induct s1 arbitrary: r v s2)
+  apply(simp)
+  apply(simp)  
+  apply(drule_tac x="der a r" in meta_spec)
+  apply(drule_tac x="v" in meta_spec)
+  apply(drule_tac x="s2" in meta_spec)
+  apply(simp)
+  using  Posix_injval
+  apply(drule_tac Posix_injval)
+  apply(subst (asm) (5) flex_fun_apply)
+  apply(simp)
+  done
+
+lemma injval_inj:
+  assumes "\<Turnstile> a : (der c r)" "\<Turnstile> v : (der c r)" "injval r c a = injval r c v" 
+  shows "a = v"
+  using  assms
+  apply(induct r arbitrary: a c v)
+       apply(auto)
+  using Prf_elims(1) apply blast
+  using Prf_elims(1) apply blast
+     apply(case_tac "c = x")
+      apply(auto)
+  using Prf_elims(4) apply auto[1]
+  using Prf_elims(1) apply blast
+    prefer 2
+  apply (smt Prf_elims(3) injval.simps(2) injval.simps(3) val.distinct(25) val.inject(3) val.inject(4))
+  apply(case_tac "nullable r1")
+    apply(auto)
+    apply(erule Prf_elims)
+     apply(erule Prf_elims)
+     apply(erule Prf_elims)
+      apply(erule Prf_elims)
+      apply(auto)
+     apply (metis Prf_injval_flat list.distinct(1) mkeps_flat)
+  apply(erule Prf_elims)
+     apply(erule Prf_elims)
+  apply(auto)
+  using Prf_injval_flat mkeps_flat apply fastforce
+  apply(erule Prf_elims)
+     apply(erule Prf_elims)
+   apply(auto)
+  apply(erule Prf_elims)
+     apply(erule Prf_elims)
+  apply(auto)
+   apply (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))
+  by (smt Prf_elims(6) injval.simps(7) list.inject val.inject(5))
+  
+  
+
+lemma uu:
+  assumes "(c # s) \<in> r \<rightarrow> injval r c v" "\<Turnstile> v : (der c r)"
+  shows "s \<in> der c r \<rightarrow> v"
+  using assms
+  apply -
+  apply(subgoal_tac "lexer r (c # s) = Some (injval r c v)")
+  prefer 2
+  using lexer_correctness(1) apply blast
+  apply(simp add: )
+  apply(case_tac  "lexer (der c r) s")
+   apply(simp)
+  apply(simp)
+  apply(case_tac "s \<in> der c r \<rightarrow> a")
+   prefer 2
+   apply (simp add: lexer_correctness(1))
+  apply(subgoal_tac "\<Turnstile> a : (der c r)")
+   prefer 2
+  using Posix_Prf apply blast
+  using injval_inj by blast
+  
+
+lemma Posix_flex2:
+  assumes "(s1 @ s2) \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"
+  shows "s2 \<in> (ders s1 r) \<rightarrow> v"
+  using assms
+  apply(induct s1 arbitrary: r v s2 rule: rev_induct)
+  apply(simp)
+  apply(simp)  
+  apply(drule_tac x="r" in meta_spec)
+  apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
+  apply(drule_tac x="x#s2" in meta_spec)
+  apply(simp add: flex_append ders_append)
+  using Prf_injval uu by blast
+
+lemma Posix_flex3:
+  assumes "s1 \<in> r \<rightarrow> flex r id s1 v" "\<Turnstile> v : ders s1 r"
+  shows "[] \<in> (ders s1 r) \<rightarrow> v"
+  using assms
+  by (simp add: Posix_flex2)
+
+lemma flex_injval:
+  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)
+  
+
+
 
 end
\ No newline at end of file