--- a/thys/LexerExt.thy Sat Mar 04 21:35:12 2017 +0000
+++ b/thys/LexerExt.thy Sat Mar 04 22:27:09 2017 +0000
@@ -216,6 +216,7 @@
| NTIMES rexp nat
| FROMNTIMES rexp nat
| NMTIMES rexp nat nat
+| PLUS rexp
section {* Semantics of Regular Expressions *}
@@ -232,6 +233,7 @@
| "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)"
+| "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)"
section {* Nullable, Derivatives *}
@@ -248,6 +250,7 @@
| "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))"
+| "nullable (PLUS r) = (nullable r)"
fun
der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -272,6 +275,7 @@
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))))"
+| "der c (PLUS r) = SEQ (der c r) (STAR r)"
fun
ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
@@ -340,7 +344,23 @@
apply(subst Sequ_UNION[symmetric])
apply(subst test2[symmetric])
apply(auto simp add: Der_UNION)[1]
-done
+(* PLUS *)
+apply(auto simp add: Sequ_def Star_def)[1]
+apply(simp add: Der_UNION)
+apply(rule_tac x="Suc xa" in bexI)
+apply(auto simp add: Sequ_def Der_def)[2]
+apply (metis append_Cons)
+apply(simp add: Der_UNION)
+apply(erule_tac bexE)
+apply(case_tac xa)
+apply(simp)
+apply(simp)
+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)
+using Der_UNION Der_star Star_def by fastforce
lemma ders_correctness:
shows "L (ders s r) = Ders s (L r)"
@@ -417,6 +437,8 @@
| "\<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"
@@ -463,7 +485,7 @@
apply(rule Prf_Pow)
apply(simp)
apply(simp)
-done
+using Prf_Pow by blast
lemma Star_Pow:
assumes "s \<in> A \<up> n"
@@ -554,6 +576,14 @@
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:
@@ -574,6 +604,7 @@
| "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))"
+| "mkeps(PLUS r) = Stars ([mkeps r])"
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
@@ -589,7 +620,7 @@
| "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)"
-
+| "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
section {* Mkeps, injval *}
@@ -683,6 +714,12 @@
apply(rule Prf.intros)
apply(auto)[2]
apply simp
+(* PLUS *)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(auto)
+using Prf.intros apply auto[1]
done
@@ -714,6 +751,9 @@
apply(rotate_tac 4)
apply(erule Prf.cases)
apply(simp_all)
+apply(rotate_tac 2)
+apply(erule Prf.cases)
+apply(simp_all)
done
@@ -749,6 +789,9 @@
\<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"
+| Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<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 (STAR r))\<rbrakk>
+ \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)"
inductive_cases Posix_elims:
@@ -772,6 +815,10 @@
apply(simp add: Star_def)
apply(rule_tac x="Suc x" in bexI)
apply(auto simp add: Sequ_def)
+apply(simp add: Star_def)
+apply(clarify)
+apply(rule_tac x="Suc x" in bexI)
+apply(auto simp add: Sequ_def)
done
@@ -833,6 +880,11 @@
apply(simp_all)
apply(erule Prf.cases)
apply(simp_all)
+apply(rotate_tac 3)
+apply(erule Prf.cases)
+apply(simp_all)
+apply(rule Prf.intros)
+apply(auto)
done
@@ -927,6 +979,10 @@
apply(auto)
apply(rule Posix_NMTIMES_mkeps)
apply(auto)
+apply(subst append_Nil[symmetric])
+apply(rule Posix.intros)
+apply(auto)
+apply(rule Posix.intros)
done
@@ -1072,6 +1128,19 @@
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
+next
+ case (Posix_PLUS1 s1 r v s2 vs v2)
+ have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2"
+ "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<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 (STAR r))" by fact+
+ then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
+ apply(cases) apply (auto simp add: append_eq_append_conv2)
+ using Posix1(1) apply fastforce
+ by (metis Posix1(1) Posix_PLUS1.hyps(5) append_Nil2 self_append_conv2)
+ moreover
+ 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
qed
lemma NTIMES_Stars:
@@ -1107,6 +1176,14 @@
apply(simp_all)
done
+lemma PLUS_Stars:
+ assumes "\<turnstile> v : PLUS r"
+ shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> 1 \<le> length vs"
+using assms
+apply(erule_tac Prf.cases)
+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"
@@ -1452,6 +1529,40 @@
apply(simp)
apply(simp add: der_correctness Der_def)
done
+next
+ case (PLUS r)
+ 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 (PLUS r) \<rightarrow> v" by fact
+ then consider
+ (cons) v1 vs s1 s2 where
+ "v = Seq v1 (Stars vs)" "s = s1 @ s2"
+ "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<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 (STAR r))"
+ apply(simp)
+ apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
+ defer
+ apply(rotate_tac 3)
+ apply(erule_tac Posix_elims(6))
+ apply (simp add: Posix.intros(6))
+ using Posix.intros(7) by blast
+ then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v"
+ proof (cases)
+ case cons
+ 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> STAR r \<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 (STAR r))" 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 (STAR r))"
+ by (simp add: der_correctness Der_def)
+ ultimately
+ have "((c # s1) @ s2) \<in> (PLUS r) \<rightarrow> Stars (injval r c v1 # vs)"
+ apply(rule_tac Posix.intros)
+ apply(simp_all)
+ done
+ then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" using cons by(simp)
+ qed
qed