# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1488239628 0
# Node ID c21938d0b3964b12adfcca4cf1f41dcbeff3764a
# Parent  a8b32da484dfe66b5eb367ebf5ccd3ae63b495cd
added also the ntimes case

diff -r a8b32da484df -r c21938d0b396 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Mon Feb 27 14:50:39 2017 +0000
+++ b/thys/LexerExt.thy	Mon Feb 27 23:53:48 2017 +0000
@@ -158,6 +158,7 @@
 | ALT rexp rexp
 | STAR rexp
 | UPNTIMES rexp nat
+| NTIMES rexp nat
 
 section {* Semantics of Regular Expressions *}
  
@@ -171,6 +172,7 @@
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)"
+| "L (NTIMES r n) = ((L r) \<up> n)"
 
 
 section {* Nullable, Derivatives *}
@@ -185,6 +187,7 @@
 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 | "nullable (STAR r) = True"
 | "nullable (UPNTIMES r n) = True"
+| "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -200,6 +203,8 @@
 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 | "der c (UPNTIMES r 0) = ZERO"
 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)"
+| "der c (NTIMES r 0) = ZERO"
+| "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)"
 
 
 fun 
@@ -211,7 +216,9 @@
 
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-by (induct r) (auto simp add: Sequ_def) 
+apply(induct r) 
+apply(auto simp add: Sequ_def) 
+done
 
 lemma Suc_reduce_Union:
   "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
@@ -244,6 +251,19 @@
 by (metis UN_insert atMost_Suc)
 
 
+lemma Der_Pow_subseteq:
+  assumes "[] \<in> A"  
+  shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
+using assms
+apply(induct n)
+apply(simp add: Sequ_def Der_def)
+apply(simp)
+apply(rule conjI)
+apply (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI)
+apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))")
+apply(auto)[1]
+by (smt Sequ_def append_Nil2 mem_Collect_eq seq_assoc subsetI)
+
 lemma test:
   shows "(\<Union>x\<le>Suc n. Der c (L r \<up> x)) = (\<Union>x\<le>n. Der c (L r) ;; L r \<up> x)"
 apply(induct n)
@@ -258,6 +278,20 @@
 apply(simp)
 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem)
 
+lemma Der_Pow_in:
+  assumes "[] \<in> A"
+  shows "Der c (A \<up> n) = (\<Union>x\<le>n. Der c (A \<up> x))"
+using assms 
+apply(induct n)
+apply(simp)
+apply(simp add: Suc_Union)
+done
+
+lemma Der_Pow_notin:
+  assumes "[] \<notin> A"
+  shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
+using assms
+by(simp)
 
 lemma der_correctness:
   shows "L (der c r) = Der c (L r)"
@@ -267,7 +301,12 @@
 apply(simp only: Der_UNION)
 apply(simp only: Seq_UNION[symmetric])
 apply(simp add: test)
-done
+apply(simp)
+(* NTIMES *)
+apply(simp only: L.simps der.simps)
+apply(simp)
+apply(rule impI)
+by (simp add: Der_Pow_subseteq sup_absorb1)
 
 
 lemma ders_correctness:
@@ -345,7 +384,8 @@
 | "\<turnstile> Stars [] : UPNTIMES r 0"
 | "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : UPNTIMES r (Suc n)"
 | "\<lbrakk>\<turnstile> Stars vs : UPNTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r (Suc n)"
-
+| "\<turnstile> Stars [] : NTIMES r 0"
+| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : NTIMES r n\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : NTIMES r (Suc n)"
 
 
 inductive_cases Prf_elims:
@@ -372,6 +412,14 @@
 using assms
 by(induct vs) (auto intro: Prf.intros)
 
+lemma Prf_Stars_NTIMES:
+  assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"
+  shows "\<turnstile> Stars vs : NTIMES r n"
+using assms
+apply(induct vs arbitrary: n) 
+apply(auto intro: Prf.intros)
+done
+
 lemma Prf_Stars_UPNTIMES:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r" "(length vs) = n"
   shows "\<turnstile> Stars vs : UPNTIMES r n"
@@ -400,6 +448,18 @@
 apply(auto)
 using le_SucI by blast
 
+lemma NTIMES_Stars:
+ assumes "\<turnstile> v : NTIMES r n"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n"
+using assms
+apply(induct n arbitrary: v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+done
+
 lemma Star_string:
   assumes "s \<in> A\<star>"
   shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
@@ -477,7 +537,16 @@
 using Prf_UPNTIMES_bigger apply blast
 apply(drule Star_Pow)
 apply(auto)
-using Star_val_length by blast
+using Star_val_length apply blast
+apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)")
+apply(auto)[1]
+apply(rule_tac x="Stars vs" in exI)
+apply(simp)
+apply(rule Prf_Stars_NTIMES)
+apply(simp)
+apply(simp)
+using Star_Pow Star_val_length by blast
+
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
@@ -494,6 +563,7 @@
 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
 | "mkeps(STAR r) = Stars []"
 | "mkeps(UPNTIMES r n) = Stars []"
+| "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
 
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -506,6 +576,8 @@
 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" 
 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+| "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+
 
 section {* Mkeps, injval *}
 
@@ -513,10 +585,16 @@
   assumes "nullable(r)" 
   shows "\<turnstile> mkeps r : r"
 using assms
-apply(induct rule: nullable.induct) 
+apply(induct r rule: mkeps.induct) 
 apply(auto intro: Prf.intros)
-using Prf.intros(8) Prf_UPNTIMES_bigger by blast
-
+using Prf.intros(8) Prf_UPNTIMES_bigger apply blast
+apply(case_tac n)
+apply(auto)
+apply(rule Prf.intros)
+apply(rule Prf_Stars_NTIMES)
+apply(simp)
+apply(simp)
+done
 
 lemma mkeps_flat:
   assumes "nullable(r)" 
@@ -551,7 +629,21 @@
 apply(simp)
 apply(rule Prf.intros(9))
 apply(simp)
-using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger by blast
+using Prf_Stars_UPNTIMES Prf_UPNTIMES_bigger apply blast
+(* NTIMES *)
+apply(case_tac x2)
+apply(simp)
+using Prf_elims(1) apply auto[1]
+apply(simp)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(drule NTIMES_Stars)
+apply(clarify)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+using Prf_Stars_NTIMES by blast
 
 lemma Prf_injval_flat:
   assumes "\<turnstile> v : der c r" 
@@ -566,6 +658,9 @@
 apply(drule UPNTIMES_Stars)
 apply(clarify)
 apply(simp)
+apply(drule NTIMES_Stars)
+apply(clarify)
+apply(simp)
 done
 
 
@@ -590,6 +685,10 @@
     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []"
+| Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; 
+    \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r n))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
+| Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []"
 
 
 inductive_cases Posix_elims:
@@ -619,6 +718,18 @@
 apply(auto intro: Prf.intros)
 using Prf.intros(8) Prf_UPNTIMES_bigger by blast
 
+lemma  Posix_NTIMES_mkeps:
+  assumes "[] \<in> r \<rightarrow> mkeps r"
+  shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))"
+apply(induct n)
+apply(simp)
+apply (rule Posix_NTIMES2)
+apply(simp)
+apply(subst append_Nil[symmetric])
+apply (rule Posix_NTIMES1)
+apply(auto)
+apply(rule assms)
+done
 
 lemma Posix_mkeps:
   assumes "nullable r"
@@ -629,6 +740,11 @@
 apply(subst append.simps(1)[symmetric])
 apply(rule Posix.intros)
 apply(auto)
+apply(case_tac n)
+apply(simp)
+apply (simp add: Posix_NTIMES2)
+apply(rule Posix_NTIMES_mkeps)
+apply(simp)
 done
 
 
@@ -714,6 +830,24 @@
   case (Posix_UPNTIMES2 r n v2)
   have "[] \<in> UPNTIMES r n \<rightarrow> v2" by fact
   then show "Stars [] = v2" by cases (auto simp add: Posix1)
+next
+  case (Posix_NTIMES2 r v2)
+  have "[] \<in> NTIMES r 0 \<rightarrow> v2" by fact
+  then show "Stars [] = v2" by cases (auto simp add: Posix1)
+next
+  case (Posix_NTIMES1 s1 r v s2 n vs v2)
+  have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> (NTIMES r n) \<rightarrow> Stars vs"
+       "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r n))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+  using Posix1(1) apply fastforce
+  apply (metis Posix1(1) Posix_NTIMES1.hyps(5) append_Nil append_Nil2)
+  done  
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
 qed
 
 
@@ -904,6 +1038,42 @@
           done
         then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" using cons by(simp)
     qed
+next 
+  case (NTIMES r n)
+  have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
+  have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact
+  then consider
+      (cons) m v1 vs s1 s2 where 
+        "n = Suc m"
+        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
+        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r m) \<rightarrow> (Stars vs)"
+        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" 
+        apply(case_tac n)
+        apply(simp)
+        using Posix_elims(1) apply blast
+        apply(simp)
+        apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+        by (metis NTIMES_Stars Posix1a)
+    then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" 
+    proof (cases)
+      case cons
+        have "n = Suc m" by fact
+        moreover
+          have "s1 \<in> der c r \<rightarrow> v1" by fact
+          then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
+        moreover
+          have "s2 \<in> NTIMES r m \<rightarrow> Stars vs" by fact
+        moreover 
+          have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" by fact
+          then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r m))" 
+            by (simp add: der_correctness Der_def)
+        ultimately 
+        have "((c # s1) @ s2) \<in> NTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" 
+          apply(rule_tac Posix.intros(10))
+          apply(simp_all)
+          done
+        then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp)
+    qed
 qed