--- a/thys2/SizeBoundStrong.thy Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/SizeBoundStrong.thy Tue Apr 19 09:08:01 2022 +0100
@@ -502,6 +502,31 @@
decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
qed
+corollary main_decode1_horribly_wrong:
+ assumes "\<Turnstile> v : ders s r"
+ shows "Some(v) = decode (retrieve (bders (intern r) s) v) r"
+ using assms
+proof (induct s arbitrary: v rule: rev_induct)
+ case Nil
+ have "\<Turnstile> v : ders [] r" by fact
+ then have "\<Turnstile> v: r" by simp
+ then have "Some v = decode (retrieve (intern r) v) r"
+ using decode_code retrieve_code by force
+ then show "Some (v) = decode (retrieve (bders (intern r) []) v) r"
+ by simp
+next
+ case (snoc c s v)
+ have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow>
+ Some ( v) = decode (retrieve (bders (intern r) s) v ) r" by fact
+ have asm: "\<Turnstile> v: ders (s @ [c]) r" by fact
+ then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r"
+ using Prf_injval ders_snoc by force
+ then have injv: "Some (injval (ders s r) c v) =
+decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
+ by (simp add: IH asm2)
+ oops
+
+
definition blex where
"blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
@@ -592,17 +617,17 @@
| \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close>
-fun pruneRexp where
+fun pruneRexp :: "arexp \<Rightarrow> rexp list \<Rightarrow> arexp"
+ where
"pruneRexp (ASEQ bs r1 r2) allowableTerms =
(let termsTruncated = (collect (erase r2) allowableTerms) in
(let pruned = pruneRexp r1 termsTruncated in
- (bsimp_ASEQ1 bs pruned r2)))"
+ (bsimp_ASEQ bs pruned r2)))"
| \<open>pruneRexp (AALTs bs rs) allowableTerms =
(let rsp = (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )
\<close>
| \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close>
-
fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where
\<open> oneSimp (SEQ ONE r) = r \<close>
| \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close>
@@ -617,14 +642,16 @@
where
\<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close>
+
+(*newSubRexps: terms that are new--have not existed in acc before*)
fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list"
where
-"dBStrong [] acc = []"
+ "dBStrong [] acc = []"
| "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc
else let newSubRexps = (addToAcc r acc) in
(case (pruneRexp r newSubRexps) of
- AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) |
- r1 \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc))
+ AZERO \<Rightarrow> dBStrong rs (map oneSimp newSubRexps @ acc) |
+ r1 \<Rightarrow> r1 # (dBStrong rs (map oneSimp newSubRexps @ acc))
)
)
"