--- a/thys/LexerExt.thy Sun Apr 02 02:14:01 2017 +0800
+++ b/thys/LexerExt.thy Wed May 17 09:38:58 2017 +0100
@@ -67,11 +67,6 @@
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
@@ -222,10 +217,6 @@
| FROMNTIMES rexp nat
| NMTIMES rexp nat nat
| PLUS rexp
-| AND rexp rexp
-| NOT rexp
-| ALLL
-| ALLBUT
section {* Semantics of Regular Expressions *}
@@ -243,10 +234,6 @@
| "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)"
-| "L (NOT r) = UNIV - (L r)"
-| "L (ALLL) = UNIV"
-| "L (ALLBUT) = UNIV - {[]}"
section {* Nullable, Derivatives *}
@@ -264,11 +251,6 @@
| "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)"
-| "nullable (NOT r) = (\<not>nullable r)"
-| "nullable (ALLL) = True"
-| "nullable (ALLBUT) = False"
-
fun
der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -294,11 +276,6 @@
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)"
-| "der c (NOT r) = NOT (der c r)"
-| "der c (ALLL) = ALLL"
-| "der c (ALLBUT) = ALLL"
-
fun
ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -353,7 +330,7 @@
apply(simp only: der.simps if_True)
apply(simp only: L.simps)
apply(simp)
-apply(auto)[3]
+apply(auto)
apply(subst (asm) Sequ_UNION[symmetric])
apply(subst (asm) test[symmetric])
apply(auto simp add: Der_UNION)[1]
@@ -378,20 +355,12 @@
apply(case_tac xa)
apply(simp)
apply(simp)
-apply(auto)[1]
+apply(auto)
apply(auto simp add: Sequ_def Der_def)[1]
using Star_def apply auto[1]
apply(case_tac "[] \<in> L r")
-apply(auto)[1]
-using Der_UNION Der_star Star_def apply fastforce
-apply(simp)
-apply(simp)
-apply(simp add: Der_def)
-apply(blast)
-(* ALLL*)
-apply(simp add: Der_def)
-apply(simp add: Der_def)
-done
+apply(auto)
+using Der_UNION Der_star Star_def by fastforce
lemma ders_correctness:
shows "L (ders s r) = Ders s (L r)"
@@ -433,10 +402,7 @@
| Right val
| Left val
| Stars "val list"
-| And val val
-| Not val
-| Alll
-| Allbut
+
section {* The string behind a value *}
@@ -450,15 +416,77 @@
| "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"
-| "flat (Not v) = flat v"
-| "flat Allbut = []"
-
lemma flat_Stars [simp]:
"flat (Stars vs) = concat (map flat vs)"
by (induct vs) (auto)
+
+section {* Relation between values and regular expressions *}
+
+inductive
+ Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
+where
+ "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
+| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
+| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
+| "\<turnstile> Void : ONE"
+| "\<turnstile> Char c : CHAR c"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r"
+| "\<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"
+| "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r"
+
+
+inductive_cases Prf_elims:
+ "\<turnstile> v : ZERO"
+ "\<turnstile> v : SEQ r1 r2"
+ "\<turnstile> v : ALT r1 r2"
+ "\<turnstile> v : ONE"
+ "\<turnstile> v : CHAR c"
+(* "\<turnstile> vs : STAR r"*)
+
+lemma Prf_STAR:
+ assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r"
+ shows "concat (map flat vs) \<in> L r\<star>"
+using assms
+apply(induct vs)
+apply(auto)
+done
+
+lemma Prf_Pow:
+ assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r"
+ shows "concat (map flat vs) \<in> L r \<up> length vs"
+using assms
+apply(induct vs)
+apply(auto simp add: Sequ_def)
+done
+
+lemma Prf_flat_L:
+ assumes "\<turnstile> v : r" shows "flat v \<in> L r"
+using assms
+apply(induct v r rule: Prf.induct)
+apply(auto simp add: Sequ_def)
+apply(rule Prf_STAR)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
+apply(rule Prf_Pow)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
+apply(rule_tac x="length vs" in bexI)
+apply(rule Prf_Pow)
+apply(simp)
+apply(simp)
+using Prf_Pow by blast
+
lemma Star_Pow:
assumes "s \<in> A \<up> n"
shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)"
@@ -479,6 +507,90 @@
using Star_Pow by blast
+lemma Star_val:
+ assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+ shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
+using assms
+apply(induct ss)
+apply(auto)
+apply (metis empty_iff list.set(1))
+by (metis concat.simps(2) list.simps(9) set_ConsD)
+
+lemma Star_val_length:
+ assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
+ shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r) \<and> (length vs) = (length ss)"
+using assms
+apply(induct ss)
+apply(auto)
+by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD)
+
+
+
+
+
+lemma L_flat_Prf2:
+ assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
+using assms
+apply(induct r arbitrary: s)
+apply(auto simp add: Sequ_def intro: Prf.intros)
+using Prf.intros(1) flat.simps(5) apply blast
+using Prf.intros(2) flat.simps(3) apply blast
+using Prf.intros(3) flat.simps(4) apply blast
+apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
+apply(auto)[1]
+apply(rule_tac x="Stars vs" in exI)
+apply(simp)
+apply(rule Prf.intros)
+apply(simp)
+using Star_string Star_val apply force
+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)
+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 = x2)")
+apply(auto)[1]
+apply(rule_tac x="Stars vs" in exI)
+apply(simp)
+apply(rule Prf.intros)
+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)
+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
+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)
+using Star_Pow Star_val_length apply blast
+done
+
+lemma L_flat_Prf:
+ "L(r) = {flat v | v. \<turnstile> v : r}"
+using Prf_flat_L L_flat_Prf2 by blast
+
+
section {* Sulzmann and Lu functions *}
fun
@@ -493,9 +605,6 @@
| "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)"
-| "mkeps(NOT r) = Not (Allbut)"
-| "mkeps(ALLL) = Void"
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -512,61 +621,25 @@
| "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) = []"
using assms
-apply (induct r)
-apply(auto)[15]
-apply(case_tac "x3a < x2")
-apply(auto)[2]
-done
+apply (induct rule: nullable.induct)
+apply(auto)
+by meson
-lemma Prf_injval_flat:
- assumes "flat v \<in> L (der c r)"
- shows "flat (injval r c v) = c # (flat v)"
-using assms
-apply(induct arbitrary: v rule: der.induct)
-apply(simp_all)
-apply(case_tac "c = d")
-prefer 2
-apply(simp)
-apply(simp)
-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"
@@ -647,18 +720,41 @@
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 *}
@@ -696,7 +792,6 @@
| 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"
@@ -831,9 +926,7 @@
apply(simp_all)
apply(rule Prf.intros)
apply(auto)
-apply(rule Prf.intros)
-apply(auto)
-by (simp add: Posix1(2))
+done
lemma Posix_NTIMES_mkeps:
@@ -1088,17 +1181,6 @@
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:
@@ -1523,17 +1605,6 @@
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