--- a/thys/Lexer.thy	Tue Jun 27 08:59:11 2017 +0100
+++ b/thys/Lexer.thy	Tue Jun 27 13:15:55 2017 +0100
@@ -256,6 +256,18 @@
 using assms
 by(induct vs) (auto intro: Prf.intros)
 
+lemma Prf_Stars_append:
+  assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
+  shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
+using assms
+apply(induct vs1 arbitrary: vs2)
+apply(auto intro: Prf.intros)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto intro: Prf.intros)
+done
+
+
 lemma Star_string:
   assumes "s \<in> A\<star>"
   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
@@ -268,7 +280,6 @@
 apply(simp)
 done
 
-
 lemma Star_val:
   assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
   shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
@@ -278,6 +289,7 @@
 apply (metis empty_iff list.set(1))
 by (metis concat.simps(2) list.simps(9) set_ConsD)
 
+
 lemma L_flat_Prf1:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
@@ -306,6 +318,16 @@
   "L(r) = {flat v | v. \<turnstile> v : r}"
 using L_flat_Prf1 L_flat_Prf2 by blast
 
+lemma Star_values_exists:
+  assumes "s \<in> (L r)\<star>"
+  shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
+using assms
+apply(drule_tac Star_string)
+apply(auto)
+
+by (metis L_flat_Prf2 Prf_Stars Star_val)
+
+
 
 section {* Sulzmann and Lu functions *}