diff -r ab7fe342e004 -r 0eaa1851a5b6 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Wed Mar 13 12:31:03 2019 +0000
+++ b/thys/BitCoded.thy	Sat Mar 16 11:15:22 2019 +0000
@@ -873,31 +873,152 @@
     apply(simp)
     oops
 
-function (sequential) bretrieve :: "arexp \<Rightarrow> bit list \<Rightarrow> (bit list) * (bit list)" where
-  "bretrieve (AZERO) bs1 = ([], bs1)"
-| "bretrieve (AONE bs) bs1 = (bs, bs1)"
-| "bretrieve (ACHAR bs c) bs1 = (bs, bs1)"
-| "bretrieve (AALTs bs rs) [] = (bs, [])"
-| "bretrieve (AALTs bs [r]) bs1 = 
-     (let (bs2, bs3) = bretrieve r bs1 in (bs @ bs2, bs3))"
-| "bretrieve (AALTs bs (r#rs)) (Z#bs1) = 
-     (let (bs2, bs3) = bretrieve r bs1 in (bs @ [Z] @ bs2, bs3))"
-| "bretrieve (AALTs bs (r#rs)) (S#bs1) = 
-     (let (bs2, bs3) = bretrieve (AALTs [] rs) bs1 in (bs @ [S] @ bs2, bs3))"
-| "bretrieve (ASEQ bs r1 r2) bs1 = 
-     (let (bs2, bs3) = bretrieve r1 bs1 in 
-      let (bs4, bs5) = bretrieve r2 bs3 in (bs @ bs2 @ bs4, bs5))"
-| "bretrieve (ASTAR bs r) [] = (bs, [])"
-| "bretrieve (ASTAR bs r) (S#bs1) = (bs @ [S], bs1)"
-| "bretrieve (ASTAR bs r) (Z#bs1) = 
-     (let (bs2, bs3) = bretrieve r bs1 in 
-      let (bs4, bs5) = bretrieve (ASTAR [] r) bs3 in (bs @ bs2 @ [Z] @ bs4, bs5))"
-  by (pat_completeness) (auto)
+fun vsimp :: "arexp \<Rightarrow> val \<Rightarrow> val"
+  where
+  "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1"
+| "vsimp _ v = v" 
+
+lemma fuse_vsimp:
+  assumes "\<Turnstile> v : (erase r)"
+  shows "vsimp (fuse bs r) v = vsimp r v"
+  using assms
+  apply(induct r arbitrary: v bs)
+       apply(simp_all)
+  apply(case_tac "\<exists>bs. r1 = AONE bs")
+   apply(auto)
+   apply (metis Prf_elims(2) vsimp.simps(1))
+  apply(erule Prf_elims)
+  apply(auto)
+  apply(case_tac r1)
+       apply(auto)
+  done  
+  
+
+lemma retrieve_XXX0:
+  assumes "\<And>r v. \<lbrakk>r \<in> set rs; \<Turnstile> v : erase r\<rbrakk> \<Longrightarrow> 
+              \<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v"
+          "\<Turnstile> v : erase (AALTs bs rs)"
+        shows "\<exists>v'. \<Turnstile> v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \<and>
+                retrieve (bsimp_AALTs bs (flts (map bsimp rs))) v' = retrieve (AALTs bs rs) v"
+  using assms
+apply(induct rs arbitrary: bs v taking: size rule: measure_induct)
+  apply(case_tac x)
+   apply(simp)
+  using Prf_elims(1) apply blast
+  apply(simp)
+  apply(case_tac list)
+   apply(simp_all)
+   apply(case_tac a)
+  apply(simp_all)
+  using Prf_elims(1) apply blast
+       apply (metis erase.simps(2) fuse.simps(2) retrieve_fuse2)
+  using Prf_elims(5) apply force
+     apply(erule Prf_elims)
+     apply(auto)[1]
+  
+  
+  
+
+  apply(simp)
+       apply(erule Prf_elims)
+  using Prf_elims(1) apply b last
+       apply(auto)
+       apply (metis append_Ni l2 erase_fuse fuse.simps(4) retrieve_fuse2)
+  apply(case_tac rs)
+       apply(auto)
+
+  
+  oops
+
+fun get where
+  "get (Some v) = v"
 
-termination
-  sorry
+  
+lemma retrieve_XXX:
+  assumes "\<Turnstile> v : erase r" 
+  shows "\<Turnstile> get (decode (code v) (erase (bsimp r))) : erase (bsimp r)"
+  using assms
+apply(induct r arbitrary: v)
+       apply(simp)
+  using Prf_elims(1) apply auto[1]  
+      apply(simp)
+  apply (simp add: decode_code)
+     apply(simp)
+  apply (simp add: decode_code)
+    apply(simp)
+    apply(erule Prf_elims)
+  apply(simp)
+   apply(case_tac  "r1 = AZERO")
+     apply(simp)
+  apply (meson Prf_elims(1) Prf_elims(2))
+  apply(case_tac  "r2 = AZERO")
+     apply(simp)
+     apply (meson Prf_elims(1) Prf_elims(2))
+   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+     apply(clarify)
+     apply(simp)
+     apply(subst bsimp_ASEQ2)
+     apply(subst bsimp_ASEQ2)
+  apply(simp add: erase_fuse)
+     defer
+     apply(subst bsimp_ASEQ1)
+  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
+  using L_bsimp_erase L_
 
-thm Prf.intros
+lemma retrieve_XXX:
+  assumes "\<Turnstile> v : erase r" 
+  shows "\<Turnstile> (vsimp (bsimp r) v : erase (bsimp r)  \<and> retrieve (bsimp r) (vsimp (bsimp r) v) = retrieve r v"
+  using assms
+  apply(induct r arbitrary: v)
+       apply(simp)
+  using Prf_elims(1) apply blast
+      apply(simp)
+  using Prf_elims(4) apply fastforce
+    apply(simp)
+  apply blast
+  apply simp
+   apply(case_tac  "r1 = AZERO")
+     apply(simp)
+  apply (meson Prf_elims(1) Prf_elims(2))
+  apply(case_tac  "r2 = AZERO")
+     apply(simp)
+     apply (meson Prf_elims(1) Prf_elims(2))
+  apply(erule Prf_elims)
+  apply(simp)
+   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+     apply(clarify)
+     apply(simp)
+    apply(subst bsimp_ASEQ2)
+     defer
+     apply(subst bsimp_ASEQ1)
+  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
+  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
+      apply(simp)
+    apply(simp)
+  apply(drule_tac  x="v1" in meta_spec)
+  apply(drule_tac  x="v2" in meta_spec)
+     apply(simp)
+  apply(clarify)
+     apply(rule_tac x="Seq v' v'a" in exI)
+     apply(simp)
+  apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))
+    prefer 3
+  apply(drule_tac  x="v1" in meta_spec)
+  apply(drule_tac  x="v2" in meta_spec)
+     apply(simp)
+    apply(clarify)
+    apply(rule_tac x="v'a" in exI)
+    apply(subst bsimp_ASEQ2)
+    apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)
+   prefer 2  
+   apply(auto)
+  apply(case_tac "x2a")
+   apply(simp)
+  using Prf_elims(1) apply blast
+  apply(simp)
+  apply(case_tac "list")
+   apply(simp)
+  sorry  
 
 
 lemma retrieve_XXX:
@@ -958,10 +1079,11 @@
 
 lemma TEST:
   assumes "\<Turnstile> v : ders s r"
-  shows "retrieve (bders (intern r) s) v = retrieve (bsimp (bders (intern r) s)) v"
+  shows "\<exists>v'. retrieve (bders (intern r) s) v' = retrieve (bsimp (bders (intern r) s)) v"
   using assms
   apply(induct s arbitrary: r v rule: rev_induct)
    apply(simp)
+  
    defer
    apply(simp add: ders_append)
    apply(frule Prf_injval)