--- a/thys/SpecExt.thy Tue Jan 25 13:12:50 2022 +0000
+++ b/thys/SpecExt.thy Thu Jan 27 23:25:26 2022 +0000
@@ -1,6 +1,6 @@
theory SpecExt
- imports Main (*"~~/src/HOL/Library/Sublist"*)
+ imports Main "HOL-Library.Sublist" (*"~~/src/HOL/Library/Sublist"*)
begin
section {* Sequential Composition of Languages *}
@@ -165,10 +165,6 @@
apply(auto simp add: Sequ_def)
done
-lemma
- assumes "[] \<in> A" "n \<noteq> 0" "A \<noteq> {}"
- shows "A \<up> (Suc n) = A \<up> n"
-
lemma Der_Pow_0:
shows "Der c (A \<up> 0) = {}"
by(simp add: Der_def)
@@ -221,7 +217,7 @@
datatype rexp =
ZERO
| ONE
-| CHAR char
+| CH char
| SEQ rexp rexp
| ALT rexp rexp
| STAR rexp
@@ -238,7 +234,7 @@
where
"L (ZERO) = {}"
| "L (ONE) = {[]}"
-| "L (CHAR c) = {[c]}"
+| "L (CH c) = {[c]}"
| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
| "L (STAR r) = (L r)\<star>"
@@ -255,7 +251,7 @@
where
"nullable (ZERO) = False"
| "nullable (ONE) = True"
-| "nullable (CHAR c) = False"
+| "nullable (CH c) = False"
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
| "nullable (STAR r) = True"
@@ -270,7 +266,7 @@
where
"der c (ZERO) = ZERO"
| "der c (ONE) = ZERO"
-| "der c (CHAR d) = (if c = d then ONE else ZERO)"
+| "der c (CH d) = (if c = d then ONE else ZERO)"
| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
| "der c (SEQ r1 r2) =
(if nullable r1
@@ -340,48 +336,6 @@
by (metis append.assoc)
-
-lemma
- "L(FROMNTIMES r n) = L(SEQ (NTIMES r n) (STAR r))"
- apply(auto simp add: Sequ_def)
- defer
- apply(subgoal_tac "\<exists>m. s2 \<in> (L r) \<up> m")
- prefer 2
- apply (simp add: Star_Pow)
- apply(auto)
- apply(rule_tac x="n + m" in bexI)
- apply (simp add: pow_add)
- apply simp
- apply(subgoal_tac "\<exists>m. m + n = xa")
- apply(auto)
- prefer 2
- using le_add_diff_inverse2 apply auto[1]
- by (smt Pow_Star Sequ_def add.commute mem_Collect_eq pow_add2)
-
-lemma
- "L (der c (FROMNTIMES r n)) =
- L (SEQ (der c r) (FROMNTIMES r (n - 1)))"
- apply(auto simp add: Sequ_def)
- using Star_Pow apply blast
- using Pow_Star by blast
-
-lemma
- "L (der c (UPNTIMES r n)) =
- L(if n = 0 then ZERO else
- ALT (der c r) (SEQ (der c r) (UPNTIMES r (n - 1))))"
- apply(auto simp add: Sequ_def)
- using SpecExt.Pow_empty by blast
-
-abbreviation "FROM \<equiv> FROMNTIMES"
-
-lemma
- shows "L (der c (FROM r n)) =
- L (if n <= 0 then SEQ (der c r) (ALT ONE (FROM r 0))
- else SEQ (der c r) (ALT ZERO (FROM r (n -1))))"
- apply(auto simp add: Sequ_def)
- oops
-
-
fun
ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
where
@@ -454,8 +408,10 @@
apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1]
apply(rule_tac x="Suc xa" in bexI)
apply(auto simp add: Sequ_def)[2]
-apply (metis append_Cons)
-apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq)
+ apply (metis append_Cons)
+ apply(rule_tac x="xa - 1" in bexI)
+ apply(auto simp add: Sequ_def)[2]
+ apply (metis One_nat_def Pow_decomp)
apply(rule impI)+
apply(subst Sequ_Union_in)
apply(subst Der_Pow_Sequ[symmetric])
@@ -485,7 +441,7 @@
| Right val
| Left val
| Stars "val list"
-
+| Nt val
section {* The string behind a value *}
@@ -499,6 +455,7 @@
| "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
| "flat (Stars []) = []"
| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
+| "flat (Nt v) = flat v"
abbreviation
"flats vs \<equiv> concat (map flat vs)"
@@ -597,7 +554,7 @@
| "\<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"
+| "\<Turnstile> Char c : CH c"
| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r"
| "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n"
| "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> [];
@@ -622,7 +579,7 @@
"\<Turnstile> v : SEQ r1 r2"
"\<Turnstile> v : ALT r1 r2"
"\<Turnstile> v : ONE"
- "\<Turnstile> v : CHAR c"
+ "\<Turnstile> v : CH c"
"\<Turnstile> vs : STAR r"
"\<Turnstile> vs : UPNTIMES r n"
"\<Turnstile> vs : NTIMES r n"
@@ -867,7 +824,10 @@
then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n"
using IH flats_cval_nonempty by (smt order.trans)
then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s"
- using Prf.intros(7) flat_Stars by blast
+ using Prf.intros(7) flat_Stars by blast
+next
+ case (NOT r)
+ then show ?case sorry
qed (auto intro: Prf.intros)
@@ -917,7 +877,7 @@
lemma LV_simps:
shows "LV ZERO s = {}"
and "LV ONE s = (if s = [] then {Void} else {})"
- and "LV (CHAR c) s = (if s = [c] then {Char c} else {})"
+ and "LV (CH c) s = (if s = [c] then {Char c} else {})"
and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s"
unfolding LV_def
apply(auto intro: Prf.intros elim: Prf.cases)
@@ -1226,8 +1186,8 @@
case (ONE s)
show "finite (LV ONE s)" by (simp add: LV_simps)
next
- case (CHAR c s)
- show "finite (LV (CHAR c) s)" by (simp add: LV_simps)
+ case (CH c s)
+ show "finite (LV (CH c) s)" by (simp add: LV_simps)
next
case (ALT r1 r2 s)
then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps)
@@ -1270,7 +1230,10 @@
case (NMTIMES r n m s)
have "\<And>s. finite (LV r s)" by fact
then show "finite (LV (NMTIMES r n m) s)"
- by (simp add: LV_NMTIMES_6)
+ by (simp add: LV_NMTIMES_6)
+next
+ case (NOT r s)
+ then show ?case sorry
qed
@@ -1281,7 +1244,7 @@
Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
where
Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
-| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
+| Posix_CHAR: "[c] \<in> (CH c) \<rightarrow> (Char c)"
| Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
| Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
| Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
@@ -1320,7 +1283,7 @@
inductive_cases Posix_elims:
"s \<in> ZERO \<rightarrow> v"
"s \<in> ONE \<rightarrow> v"
- "s \<in> CHAR c \<rightarrow> v"
+ "s \<in> CH c \<rightarrow> v"
"s \<in> ALT r1 r2 \<rightarrow> v"
"s \<in> SEQ r1 r2 \<rightarrow> v"
"s \<in> STAR r \<rightarrow> v"
@@ -1396,7 +1359,7 @@
then show "Void = v2" by cases auto
next
case (Posix_CHAR c v2)
- have "[c] \<in> CHAR c \<rightarrow> v2" by fact
+ have "[c] \<in> CH c \<rightarrow> v2" by fact
then show "Char c = v2" by cases auto
next
case (Posix_ALT1 s r1 v r2 v2)
@@ -1503,14 +1466,9 @@
using Posix1(1) Posix1(2) apply blast
apply(case_tac n)
apply(simp)
- apply(simp)
- apply(drule_tac x="va" in meta_spec)
- apply(drule_tac x="vs" in meta_spec)
- apply(simp)
- apply(drule meta_mp)
- apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil diff_Suc_1 local.Posix_FROMNTIMES1(4) val.inject(5))
- apply (metis L.simps(9) Posix1(1) UN_E append.right_neutral append_Nil)
- by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) self_append_conv self_append_conv2)
+ apply(simp)
+ apply (smt (verit, ccfv_threshold) L.simps(9) Posix1(1) UN_E append_eq_append_conv2)
+ by (metis One_nat_def Posix1(1) Posix_FROMNTIMES1.hyps(7) append_Nil2 append_self_conv2)
moreover
have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
"\<And>v2. s2 \<in> FROMNTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1555,18 +1513,8 @@
apply(case_tac m)
apply(simp)
apply(simp)
- apply(drule_tac x="va" in meta_spec)
- apply(drule_tac x="vs" in meta_spec)
- apply(simp)
- apply(drule meta_mp)
- apply(drule Posix1(1))
- apply(drule Posix1(1))
- apply(drule Posix1(1))
- apply(frule Posix1(1))
- apply(simp)
- using Posix_NMTIMES1.hyps(4) apply force
- apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
- by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)
+ apply (metis L.simps(10) Posix1(1) UN_E append.right_neutral append_Nil)
+ by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append_Nil self_append_conv)
moreover
have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
"\<And>v2. s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1616,7 +1564,6 @@
apply(auto simp add: intro!: Prf.intros elim!: Prf_elims)[2]
apply (metis (mono_tags, lifting) Prf.intros(9) append_Nil empty_iff flat_Stars flats_empty list.set(1) mem_Collect_eq)
apply(simp)
- apply(clarify)
apply(case_tac n)
apply(simp)
apply(simp)
@@ -1632,7 +1579,6 @@
apply(simp)
apply(simp)
apply(simp)
- apply(clarify)
apply(erule Prf_elims)
apply(simp)
apply(rule Prf.intros)
@@ -1660,7 +1606,6 @@
apply(simp)
apply (metis Prf.intros(11) append_Nil empty_iff list.set(1))
apply(simp)
- apply(clarify)
apply(rotate_tac 6)
apply(erule Prf_elims)
apply(simp)
@@ -1675,7 +1620,6 @@
apply(simp)
apply(simp)
apply(simp)
- apply(clarify)
apply(rotate_tac 6)
apply(erule Prf_elims)
apply(simp)