--- a/thys/LexerExt.thy	Mon Feb 27 23:53:48 2017 +0000
+++ b/thys/LexerExt.thy	Tue Feb 28 00:26:34 2017 +0000
@@ -718,6 +718,19 @@
 apply(auto intro: Prf.intros)
 using Prf.intros(8) Prf_UPNTIMES_bigger by blast
 
+lemma Posix_NTIMES_length:
+  assumes "s \<in> NTIMES r n \<rightarrow> Stars vs"
+  shows "length vs = n"
+using assms
+using NTIMES_Stars Posix1a val.inject(5) by blast
+
+lemma Posix_UPNTIMES_length:
+  assumes "s \<in> UPNTIMES r n \<rightarrow> Stars vs"
+  shows "length vs \<le> n"
+using assms
+using Posix1a UPNTIMES_Stars val.inject(5) by blast
+
+
 lemma  Posix_NTIMES_mkeps:
   assumes "[] \<in> r \<rightarrow> mkeps r"
   shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"