--- a/thys/ReStar.thy	Mon Mar 07 22:20:15 2016 +0000
+++ b/thys/ReStar.thy	Tue Mar 08 00:34:15 2016 +0000
@@ -759,6 +759,24 @@
 apply(simp add: der_correctness Der_def)
 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)"
+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(simp)
+apply(simp)
+apply(clarify)
+apply(rule iffI)
+apply(auto)
+apply(rule PMatch2_roy_version)
+apply(simp)
+using PMatch1(1) by auto
+
 lemma lex_correct5:
   assumes "s \<in> L r"
   shows "s \<in> r \<rightarrow> (matcher2 r s)"