--- a/thys/LexerExt.thy Mon Mar 13 14:54:12 2017 +0000
+++ b/thys/LexerExt.thy Fri Mar 17 19:47:42 2017 +0000
@@ -67,6 +67,11 @@
unfolding Der_def Sequ_def
by (auto simp add: Cons_eq_append_conv)
+lemma Der_inter [simp]:
+ shows "Der c (A \<inter> B) = Der c A \<inter> Der c B"
+unfolding Der_def
+by auto
+
lemma Der_union [simp]:
shows "Der c (A \<union> B) = Der c A \<union> Der c B"
unfolding Der_def
@@ -217,6 +222,7 @@
| FROMNTIMES rexp nat
| NMTIMES rexp nat nat
| PLUS rexp
+| AND rexp rexp
section {* Semantics of Regular Expressions *}
@@ -234,6 +240,7 @@
| "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)"
| "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)"
+| "L (AND r1 r2) = (L r1) \<inter> (L r2)"
section {* Nullable, Derivatives *}
@@ -251,6 +258,7 @@
| "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))"
| "nullable (PLUS r) = (nullable r)"
+| "nullable (AND r1 r2) = (nullable r1 \<and> nullable r2)"
fun
der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -276,6 +284,7 @@
SEQ (der c r) (UPNTIMES r (m - 1))) else
SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))"
| "der c (PLUS r) = SEQ (der c r) (STAR r)"
+| "der c (AND r1 r2) = AND (der c r1) (der c r2)"
fun
ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -402,7 +411,7 @@
| Right val
| Left val
| Stars "val list"
-
+| And val val
section {* The string behind a value *}
@@ -416,6 +425,7 @@
| "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
| "flat (Stars []) = []"
| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
+| "flat (And v1 v2) = flat v1"
lemma flat_Stars [simp]:
"flat (Stars vs) = concat (map flat vs)"
@@ -438,6 +448,7 @@
| "\<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"
| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r"
+| "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2; flat v1 = flat v2\<rbrakk> \<Longrightarrow> \<turnstile> And v1 v2: AND r1 r2"
inductive_cases Prf_elims:
@@ -584,7 +595,8 @@
apply(simp)
apply(simp)
using Star_Pow Star_val_length apply blast
-done
+(* AND *)
+using Prf.intros(12) by fastforce
lemma L_flat_Prf:
"L(r) = {flat v | v. \<turnstile> v : r}"
@@ -605,6 +617,7 @@
| "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
| "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
| "mkeps(PLUS r) = Stars ([mkeps r])"
+| "mkeps(AND r1 r2) = And (mkeps r1) (mkeps r2)"
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -621,17 +634,10 @@
| "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)"
| "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
+| "injval (AND r1 r2) c (And v1 v2) = And (injval r1 c v1) (injval r2 c v2)"
section {* Mkeps, injval *}
-lemma mkeps_nullable:
- assumes "nullable(r)"
- shows "\<turnstile> mkeps r : r"
-using assms
-apply(induct r rule: mkeps.induct)
-apply(auto intro: Prf.intros)
-by (metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
-
lemma mkeps_flat:
assumes "nullable(r)"
shows "flat (mkeps r) = []"
@@ -640,6 +646,52 @@
apply(auto)
by meson
+lemma mkeps_nullable:
+ assumes "nullable(r)"
+ shows "\<turnstile> mkeps r : r"
+using assms
+apply(induct r rule: mkeps.induct)
+apply(auto intro: Prf.intros)
+apply(metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl)
+apply(rule Prf.intros)
+apply(simp_all add: mkeps_flat)
+done
+
+lemma Prf_injval_flat:
+ assumes "\<turnstile> v : der c r"
+ shows "flat (injval r c v) = c # (flat v)"
+using assms
+apply(induct arbitrary: v rule: der.induct)
+apply(auto elim!: Prf_elims split: if_splits)
+apply(metis mkeps_flat)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+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)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+done
lemma Prf_injval:
assumes "\<turnstile> v : der c r"
@@ -720,41 +772,18 @@
apply(simp_all)
apply(auto)
using Prf.intros apply auto[1]
+(* AND *)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+apply(rule Prf.intros)
+apply(simp)
+apply(simp)
+apply(simp add: Prf_injval_flat)
done
-lemma Prf_injval_flat:
- assumes "\<turnstile> v : der c r"
- shows "flat (injval r c v) = c # (flat v)"
-using assms
-apply(induct arbitrary: v rule: der.induct)
-apply(auto elim!: Prf_elims split: if_splits)
-apply(metis mkeps_flat)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-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)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)
-done
+
section {* Our Alternative Posix definition *}
@@ -792,6 +821,7 @@
| Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (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 (STAR r))\<rbrakk>
\<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)"
+| Posix_AND: "\<lbrakk>s \<in> r1 \<rightarrow> v1; s \<in> r2 \<rightarrow> v2\<rbrakk> \<Longrightarrow> s \<in> (AND r1 r2) \<rightarrow> (And v1 v2)"
inductive_cases Posix_elims:
"s \<in> ZERO \<rightarrow> v"
@@ -926,7 +956,9 @@
apply(simp_all)
apply(rule Prf.intros)
apply(auto)
-done
+apply(rule Prf.intros)
+apply(auto)
+by (simp add: Posix1(2))
lemma Posix_NTIMES_mkeps:
@@ -1181,6 +1213,17 @@
have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
"\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
ultimately show "Stars (v # vs) = v2" by auto
+next
+ case (Posix_AND s r1 v1 r2 v2 v')
+ have "s \<in> AND r1 r2 \<rightarrow> v'"
+ "s \<in> r1 \<rightarrow> v1" "s \<in> r2 \<rightarrow> v2" by fact+
+ then obtain v1' v2' where "v' = And v1' v2'" "s \<in> r1 \<rightarrow> v1'" "s \<in> r2 \<rightarrow> v2'"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ done
+ moreover
+ have IHs: "\<And>v1'. s \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
+ "\<And>v2'. s \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
+ ultimately show "And v1 v2 = v'" by simp
qed
lemma NTIMES_Stars:
@@ -1605,6 +1648,17 @@
apply(simp)
apply(simp)
done
+next
+ case (AND r1 r2)
+ then show ?case
+ apply -
+ apply(erule Posix.cases)
+ apply(simp_all)
+ apply(auto)
+ apply(rule Posix.intros)
+ apply(simp)
+ apply(simp)
+ done
qed