--- 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