# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1488241594 0
# Node ID 4c02878e2fe050dff79e9975b6c1a98ea738b9d0
# Parent  c21938d0b3964b12adfcca4cf1f41dcbeff3764a
added two sanity lemmas

diff -r c21938d0b396 -r 4c02878e2fe0 thys/LexerExt.thy
--- 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))"