diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/SizeBoundStrong.thy
--- 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))
                                  )
                            )
                     "