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