871 apply(simp add: ders_append) |
871 apply(simp add: ders_append) |
872 defer |
872 defer |
873 apply(simp) |
873 apply(simp) |
874 oops |
874 oops |
875 |
875 |
876 function (sequential) bretrieve :: "arexp \<Rightarrow> bit list \<Rightarrow> (bit list) * (bit list)" where |
876 fun vsimp :: "arexp \<Rightarrow> val \<Rightarrow> val" |
877 "bretrieve (AZERO) bs1 = ([], bs1)" |
877 where |
878 | "bretrieve (AONE bs) bs1 = (bs, bs1)" |
878 "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1" |
879 | "bretrieve (ACHAR bs c) bs1 = (bs, bs1)" |
879 | "vsimp _ v = v" |
880 | "bretrieve (AALTs bs rs) [] = (bs, [])" |
880 |
881 | "bretrieve (AALTs bs [r]) bs1 = |
881 lemma fuse_vsimp: |
882 (let (bs2, bs3) = bretrieve r bs1 in (bs @ bs2, bs3))" |
882 assumes "\<Turnstile> v : (erase r)" |
883 | "bretrieve (AALTs bs (r#rs)) (Z#bs1) = |
883 shows "vsimp (fuse bs r) v = vsimp r v" |
884 (let (bs2, bs3) = bretrieve r bs1 in (bs @ [Z] @ bs2, bs3))" |
884 using assms |
885 | "bretrieve (AALTs bs (r#rs)) (S#bs1) = |
885 apply(induct r arbitrary: v bs) |
886 (let (bs2, bs3) = bretrieve (AALTs [] rs) bs1 in (bs @ [S] @ bs2, bs3))" |
886 apply(simp_all) |
887 | "bretrieve (ASEQ bs r1 r2) bs1 = |
887 apply(case_tac "\<exists>bs. r1 = AONE bs") |
888 (let (bs2, bs3) = bretrieve r1 bs1 in |
888 apply(auto) |
889 let (bs4, bs5) = bretrieve r2 bs3 in (bs @ bs2 @ bs4, bs5))" |
889 apply (metis Prf_elims(2) vsimp.simps(1)) |
890 | "bretrieve (ASTAR bs r) [] = (bs, [])" |
890 apply(erule Prf_elims) |
891 | "bretrieve (ASTAR bs r) (S#bs1) = (bs @ [S], bs1)" |
891 apply(auto) |
892 | "bretrieve (ASTAR bs r) (Z#bs1) = |
892 apply(case_tac r1) |
893 (let (bs2, bs3) = bretrieve r bs1 in |
893 apply(auto) |
894 let (bs4, bs5) = bretrieve (ASTAR [] r) bs3 in (bs @ bs2 @ [Z] @ bs4, bs5))" |
894 done |
895 by (pat_completeness) (auto) |
895 |
896 |
896 |
897 termination |
897 lemma retrieve_XXX0: |
898 sorry |
898 assumes "\<And>r v. \<lbrakk>r \<in> set rs; \<Turnstile> v : erase r\<rbrakk> \<Longrightarrow> |
899 |
899 \<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v" |
900 thm Prf.intros |
900 "\<Turnstile> v : erase (AALTs bs rs)" |
901 |
901 shows "\<exists>v'. \<Turnstile> v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \<and> |
902 |
902 retrieve (bsimp_AALTs bs (flts (map bsimp rs))) v' = retrieve (AALTs bs rs) v" |
|
903 using assms |
|
904 apply(induct rs arbitrary: bs v taking: size rule: measure_induct) |
|
905 apply(case_tac x) |
|
906 apply(simp) |
|
907 using Prf_elims(1) apply blast |
|
908 apply(simp) |
|
909 apply(case_tac list) |
|
910 apply(simp_all) |
|
911 apply(case_tac a) |
|
912 apply(simp_all) |
|
913 using Prf_elims(1) apply blast |
|
914 apply (metis erase.simps(2) fuse.simps(2) retrieve_fuse2) |
|
915 using Prf_elims(5) apply force |
|
916 apply(erule Prf_elims) |
|
917 apply(auto)[1] |
|
918 |
|
919 |
|
920 |
|
921 |
|
922 apply(simp) |
|
923 apply(erule Prf_elims) |
|
924 using Prf_elims(1) apply b last |
|
925 apply(auto) |
|
926 apply (metis append_Ni l2 erase_fuse fuse.simps(4) retrieve_fuse2) |
|
927 apply(case_tac rs) |
|
928 apply(auto) |
|
929 |
|
930 |
|
931 oops |
|
932 |
|
933 fun get where |
|
934 "get (Some v) = v" |
|
935 |
|
936 |
903 lemma retrieve_XXX: |
937 lemma retrieve_XXX: |
904 assumes "\<Turnstile> v : erase r" |
938 assumes "\<Turnstile> v : erase r" |
905 shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v" |
939 shows "\<Turnstile> get (decode (code v) (erase (bsimp r))) : erase (bsimp r)" |
|
940 using assms |
|
941 apply(induct r arbitrary: v) |
|
942 apply(simp) |
|
943 using Prf_elims(1) apply auto[1] |
|
944 apply(simp) |
|
945 apply (simp add: decode_code) |
|
946 apply(simp) |
|
947 apply (simp add: decode_code) |
|
948 apply(simp) |
|
949 apply(erule Prf_elims) |
|
950 apply(simp) |
|
951 apply(case_tac "r1 = AZERO") |
|
952 apply(simp) |
|
953 apply (meson Prf_elims(1) Prf_elims(2)) |
|
954 apply(case_tac "r2 = AZERO") |
|
955 apply(simp) |
|
956 apply (meson Prf_elims(1) Prf_elims(2)) |
|
957 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
958 apply(clarify) |
|
959 apply(simp) |
|
960 apply(subst bsimp_ASEQ2) |
|
961 apply(subst bsimp_ASEQ2) |
|
962 apply(simp add: erase_fuse) |
|
963 defer |
|
964 apply(subst bsimp_ASEQ1) |
|
965 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
966 using L_bsimp_erase L_ |
|
967 |
|
968 lemma retrieve_XXX: |
|
969 assumes "\<Turnstile> v : erase r" |
|
970 shows "\<Turnstile> (vsimp (bsimp r) v : erase (bsimp r) \<and> retrieve (bsimp r) (vsimp (bsimp r) v) = retrieve r v" |
906 using assms |
971 using assms |
907 apply(induct r arbitrary: v) |
972 apply(induct r arbitrary: v) |
908 apply(simp) |
973 apply(simp) |
909 using Prf_elims(1) apply blast |
974 using Prf_elims(1) apply blast |
910 apply(simp) |
975 apply(simp) |
951 apply(simp) |
1016 apply(simp) |
952 using Prf_elims(1) apply blast |
1017 using Prf_elims(1) apply blast |
953 apply(simp) |
1018 apply(simp) |
954 apply(case_tac "list") |
1019 apply(case_tac "list") |
955 apply(simp) |
1020 apply(simp) |
|
1021 sorry |
|
1022 |
|
1023 |
|
1024 lemma retrieve_XXX: |
|
1025 assumes "\<Turnstile> v : erase r" |
|
1026 shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v" |
|
1027 using assms |
|
1028 apply(induct r arbitrary: v) |
|
1029 apply(simp) |
|
1030 using Prf_elims(1) apply blast |
|
1031 apply(simp) |
|
1032 using Prf_elims(4) apply fastforce |
|
1033 apply(simp) |
|
1034 apply blast |
|
1035 apply simp |
|
1036 apply(case_tac "r1 = AZERO") |
|
1037 apply(simp) |
|
1038 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1039 apply(case_tac "r2 = AZERO") |
|
1040 apply(simp) |
|
1041 apply (meson Prf_elims(1) Prf_elims(2)) |
|
1042 apply(erule Prf_elims) |
|
1043 apply(simp) |
|
1044 apply(case_tac "\<exists>bs. bsimp r1 = AONE bs") |
|
1045 apply(clarify) |
|
1046 apply(simp) |
|
1047 apply(subst bsimp_ASEQ2) |
|
1048 defer |
|
1049 apply(subst bsimp_ASEQ1) |
|
1050 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
1051 using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce |
|
1052 apply(simp) |
|
1053 apply(simp) |
|
1054 apply(drule_tac x="v1" in meta_spec) |
|
1055 apply(drule_tac x="v2" in meta_spec) |
|
1056 apply(simp) |
|
1057 apply(clarify) |
|
1058 apply(rule_tac x="Seq v' v'a" in exI) |
|
1059 apply(simp) |
|
1060 apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6)) |
|
1061 prefer 3 |
|
1062 apply(drule_tac x="v1" in meta_spec) |
|
1063 apply(drule_tac x="v2" in meta_spec) |
|
1064 apply(simp) |
|
1065 apply(clarify) |
|
1066 apply(rule_tac x="v'a" in exI) |
|
1067 apply(subst bsimp_ASEQ2) |
|
1068 apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2) |
|
1069 prefer 2 |
|
1070 apply(auto) |
|
1071 apply(case_tac "x2a") |
|
1072 apply(simp) |
|
1073 using Prf_elims(1) apply blast |
|
1074 apply(simp) |
|
1075 apply(case_tac "list") |
|
1076 apply(simp) |
956 sorry |
1077 sorry |
957 |
1078 |
958 |
1079 |
959 lemma TEST: |
1080 lemma TEST: |
960 assumes "\<Turnstile> v : ders s r" |
1081 assumes "\<Turnstile> v : ders s r" |
961 shows "retrieve (bders (intern r) s) v = retrieve (bsimp (bders (intern r) s)) v" |
1082 shows "\<exists>v'. retrieve (bders (intern r) s) v' = retrieve (bsimp (bders (intern r) s)) v" |
962 using assms |
1083 using assms |
963 apply(induct s arbitrary: r v rule: rev_induct) |
1084 apply(induct s arbitrary: r v rule: rev_induct) |
964 apply(simp) |
1085 apply(simp) |
|
1086 |
965 defer |
1087 defer |
966 apply(simp add: ders_append) |
1088 apply(simp add: ders_append) |
967 apply(frule Prf_injval) |
1089 apply(frule Prf_injval) |
968 apply(drule_tac x="r" in meta_spec) |
1090 apply(drule_tac x="r" in meta_spec) |
969 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
1091 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |