diff -r 71e26f43c896 -r d74bfa11802c thys/ReStar.thy
--- a/thys/ReStar.thy	Sun Mar 06 20:00:47 2016 +0000
+++ b/thys/ReStar.thy	Mon Mar 07 03:23:28 2016 +0000
@@ -722,6 +722,20 @@
 apply(simp add: der_correctness Der_def)
 done
 
+lemma lex_correct1a:
+  shows "s \<notin> L r \<longleftrightarrow> matcher r s = None"
+using assms
+apply(induct s arbitrary: r)
+apply(simp)
+apply (metis nullable_correctness)
+apply(auto)
+apply(drule_tac x="der a r" in meta_spec)
+apply(auto)
+apply(simp add: der_correctness Der_def)
+apply(drule_tac x="der a r" in meta_spec)
+apply(auto)
+apply(simp add: der_correctness Der_def)
+done
 
 lemma lex_correct2:
   assumes "s \<in> L r"
@@ -751,6 +765,21 @@
 apply(auto)
 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)"
+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(auto)
+apply(metis PMatch2_roy_version)
+apply(simp add: der_correctness Der_def)
+using lex_correct1a 
+apply fastforce
+apply(simp add: der_correctness Der_def)
+by (simp add: lex_correct1a)
+
 lemma lex_correct5:
   assumes "s \<in> L r"
   shows "s \<in> r \<rightarrow> (matcher2 r s)"