--- 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)