# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1488416200 0
# Node ID a8749366ad5dda9cd2dea07d5e72a24ba1e45146
# Parent  d131cd45a3463d2755364b35177505c9e54c424a
NMTIMES case also done

diff -r d131cd45a346 -r a8749366ad5d thys/LexerExt.thy
--- a/thys/LexerExt.thy	Wed Mar 01 00:13:15 2017 +0000
+++ b/thys/LexerExt.thy	Thu Mar 02 00:56:40 2017 +0000
@@ -155,6 +155,7 @@
 | UPNTIMES rexp nat
 | NTIMES rexp nat
 | FROMNTIMES rexp nat
+| NMTIMES rexp nat nat
 
 section {* Semantics of Regular Expressions *}
  
@@ -168,8 +169,9 @@
 | "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)"
+| "L (NTIMES r n) = (L r) \<up> n"
 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"
+| "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 
 
 section {* Nullable, Derivatives *}
 
@@ -185,6 +187,7 @@
 | "nullable (UPNTIMES r n) = True"
 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)"
+| "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
 fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -204,6 +207,9 @@
 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)"
 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)"
 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)"
+| "der c (NMTIMES r n m) = 
+     (if m < n then ZERO else (if n = 0 then  (if m = 0 then ZERO else SEQ (der c r) (UPNTIMES r (m - 1))) else 
+                               SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" 
 
 fun 
  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -269,6 +275,14 @@
 apply(simp)
 by (smt Der_Pow Suc_Union inf_sup_aci(5) inf_sup_aci(7) sup_idem)
 
+lemma test2:
+  shows "(\<Union>x\<in>(Suc ` A). Der c (L r \<up> x)) = (\<Union>x\<in>A. Der c (L r) ;; L r \<up> x)"
+apply(auto)[1]
+apply(case_tac "[] \<in> L r")
+apply(simp)
+defer
+apply(simp)
+using Der_Pow_subseteq by blast
 
 
 lemma Der_Pow_notin:
@@ -299,7 +313,28 @@
 apply(simp only: der.simps)
 apply(simp only: L.simps)
 apply(simp add: Der_UNION)
-by (smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1)
+apply(smt Der_Pow Der_Pow_notin Der_Pow_subseteq SUP_cong Seq_UNION Suc_reduce_Union2 sup.absorb_iff1)
+(* NMTIMES *)
+apply(case_tac "n \<le> m")
+prefer 2
+apply(simp only: der.simps if_True)
+apply(simp only: L.simps)
+apply(simp)
+apply(auto)
+apply(subst (asm) Seq_UNION[symmetric])
+apply(subst (asm) test[symmetric])
+apply(auto simp add: Der_UNION)[1]
+apply(auto simp add: Der_UNION)[1]
+apply(subst Seq_UNION[symmetric])
+apply(subst test[symmetric])
+apply(auto)[1]
+apply(subst (asm) Seq_UNION[symmetric])
+apply(subst (asm) test2[symmetric])
+apply(auto simp add: Der_UNION)[1]
+apply(subst Seq_UNION[symmetric])
+apply(subst test2[symmetric])
+apply(auto simp add: Der_UNION)[1]
+done
 
 lemma ders_correctness:
   shows "L (ders s r) = Ders s (L r)"
@@ -375,6 +410,7 @@
 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n"
 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n"
 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m"
 
 inductive_cases Prf_elims:
   "\<turnstile> v : ZERO"
@@ -417,6 +453,10 @@
 apply(rule Prf_Pow)
 apply(simp)
 apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
 done
 
 lemma Star_string:
@@ -501,6 +541,15 @@
 apply(simp)
 apply(simp)
 using Star_Pow 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 = x)")
+apply(auto)[1]
+apply(rule_tac x="Stars vs" in exI)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(simp)
+using Star_Pow Star_val_length apply blast
 done
 
 lemma L_flat_Prf:
@@ -515,11 +564,13 @@
 where
   "mkeps(ONE) = Void"
 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
-| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
+| "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))"
 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
+| "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
+
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
@@ -533,6 +584,8 @@
 | "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)"
 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+| "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+
 
 section {* Mkeps, injval *}
 
@@ -542,13 +595,15 @@
 using assms
 apply(induct r rule: mkeps.induct) 
 apply(auto intro: Prf.intros)
-done
+by (metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
 
 lemma mkeps_flat:
   assumes "nullable(r)" 
   shows "flat (mkeps r) = []"
 using assms
-by (induct rule: nullable.induct) (auto)
+apply (induct rule: nullable.induct) 
+apply(auto)
+by meson
 
 
 lemma Prf_injval:
@@ -608,7 +663,23 @@
 apply(erule Prf.cases)
 apply(simp_all)
 apply(clarify)
-using Prf.intros(9) by auto
+using Prf.intros(9) apply auto
+(* NMTIMES *)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rule Prf.intros)
+apply(auto)[2]
+apply simp
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(clarify)
+apply(rule Prf.intros)
+apply(auto)[2]
+apply simp
+done
 
 
 lemma Prf_injval_flat:
@@ -633,6 +704,12 @@
 apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 4)
+apply(erule Prf.cases)
+apply(simp_all)
 done
 
 
@@ -664,6 +741,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 (FROMNTIMES r n))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)"
 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow>  s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs"
+| Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n 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 r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))\<rbrakk>
+    \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"
+| Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow>  s \<in> NMTIMES r 0 m \<rightarrow> Stars vs"
 
 
 inductive_cases Posix_elims:
@@ -684,7 +765,10 @@
 apply(auto simp add: Sequ_def)
 apply(rule_tac x="Suc x" in bexI)
 apply(auto simp add: Sequ_def)
-by (simp add: Star_in_Pow)
+apply(simp add: Star_in_Pow)
+apply(rule_tac x="Suc x" in bexI)
+apply(auto simp add: Sequ_def)
+done
 
 
 lemma Posix1a:
@@ -703,20 +787,50 @@
 apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)
-apply (smt Posix_UPNTIMES2 Posix_elims(2) Prf.simps le_0_eq le_Suc_eq length_0_conv nat_induct nullable.simps(3) nullable.simps(7) rexp.distinct(61) rexp.distinct(67) rexp.distinct(69) rexp.inject(5) val.inject(5) val.simps(29) val.simps(33) val.simps(35))
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)[1]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
 apply(rule Prf.intros)
 apply(auto)[1]
 apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)
-apply (smt Prf.simps rexp.distinct(63) rexp.distinct(67) rexp.distinct(71) rexp.inject(6) val.distinct(17) val.distinct(9) val.inject(5) val.simps(29) val.simps(33) val.simps(35))
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
 apply(rule Prf.intros)
-apply(auto)[1]
+apply(auto)[2]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)[3]
 apply(rotate_tac 3)
 apply(erule Prf.cases)
 apply(simp_all)
-using Prf.simps apply blast
-by (smt Prf.simps le0 rexp.distinct(61) rexp.distinct(63) rexp.distinct(65) rexp.inject(4) val.distinct(17) val.distinct(9) val.simps(29) val.simps(33) val.simps(35))
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)[3]
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+
 
 lemma  Posix_NTIMES_mkeps:
   assumes "[] \<in> r \<rightarrow> mkeps r"
@@ -745,6 +859,24 @@
 apply(rule assms)
 done
 
+lemma  Posix_NMTIMES_mkeps:
+  assumes "[] \<in> r \<rightarrow> mkeps r" "n \<le> m"
+  shows "[] \<in> NMTIMES r n m \<rightarrow> Stars (replicate n (mkeps r))"
+using assms(2)
+apply(induct n arbitrary: m)
+apply(simp)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(subst append_Nil[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+apply(rule assms)
+done
+
+
 
 lemma Posix_mkeps:
   assumes "nullable r"
@@ -776,6 +908,21 @@
 apply(auto)
 apply(rule Posix_FROMNTIMES_mkeps)
 apply(simp)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(case_tac n)
+apply(simp)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(simp)
+apply(case_tac m)
+apply(simp)
+apply(simp)
+apply(subst append_Nil[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+apply(rule Posix_NMTIMES_mkeps)
+apply(auto)
 done
 
 
@@ -900,6 +1047,27 @@
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
   ultimately show "Stars (v # vs) = v2" by auto
+next
+  case (Posix_NMTIMES2 s r m v1 v2)
+  have "s \<in> NMTIMES r 0 m \<rightarrow> v2" "s \<in> UPNTIMES r m \<rightarrow> Stars v1" 
+       "\<And>v3. s \<in> UPNTIMES r m \<rightarrow> v3 \<Longrightarrow> Stars v1 = v3" by fact+
+  then show ?case 
+  apply(cases)
+  apply(auto)
+  done
+next
+  case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
+  have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" 
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n 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 r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))" by fact+
+  then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')"
+  apply(cases) apply (auto simp add: append_eq_append_conv2)
+  using Posix1(1) apply fastforce
+  by (metis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2)
+  moreover
+  have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
+            "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
+  ultimately show "Stars (v # vs) = v2" by auto
 qed
 
 lemma NTIMES_Stars:
@@ -935,6 +1103,17 @@
 apply(simp_all)
 done
 
+lemma NMTIMES_Stars:
+ assumes "\<turnstile> v : NMTIMES r n m"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs \<and> length vs \<le> m"
+using assms
+apply(induct n arbitrary: m v)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(erule Prf.cases)
+apply(simp_all)
+done
+
 
 lemma Posix_injval:
   assumes "s \<in> (der c r) \<rightarrow> v"
@@ -1220,9 +1399,59 @@
       done
       then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp
     qed
+next 
+  case (NMTIMES r n m)
+  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 (NMTIMES r n m) \<rightarrow> v" by fact
+  then show "(c # s) \<in> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v"
+        apply(case_tac "m < n")
+        apply(simp)
+        using Posix_elims(1) apply blast
+        apply(case_tac n)
+        apply(simp_all)
+        apply(case_tac m)
+        apply(simp)
+        apply(erule Posix_elims(1))
+        apply(simp)
+        apply(erule Posix.cases)
+        apply(simp_all)
+        apply(clarify)
+        apply(rotate_tac 5)
+        apply(frule Posix1a)
+        apply(drule UPNTIMES_Stars)
+        apply(clarify)
+        apply(simp)
+        apply(subst append_Cons[symmetric])
+        apply(rule Posix.intros)
+        apply(rule Posix.intros)
+        apply(auto)
+        apply(rule IH)
+        apply blast
+        using Posix1a Prf_injval_flat apply auto[1]
+        apply(simp add: der_correctness Der_def)
+        apply blast
+        apply(case_tac m)
+        apply(simp)
+        apply(simp)
+        apply(erule Posix.cases)
+        apply(simp_all)
+        apply(clarify)
+        apply(rotate_tac 6)
+        apply(frule Posix1a)
+        apply(drule NMTIMES_Stars)
+        apply(clarify)
+        apply(simp)
+        apply(subst append_Cons[symmetric])
+        apply(rule Posix.intros)
+        apply(rule IH)
+        apply(blast)
+        apply(simp)
+        apply(simp add: der_correctness Der_def)
+        done
 qed
 
 
+
 section {* The Lexer by Sulzmann and Lu  *}
 
 fun