umm_heap updated to Isabelle2015
This commit is contained in:
Gerwin Klein
parent
327d651ffc
commit
4ebd10ee1b
|
|
@ -209,7 +209,7 @@ begin
|
|||
instance
|
||||
apply intro_classes
|
||||
apply(simp_all add: typ_info_array array_tag_def size_of_def
|
||||
norm_bytes_def zero_less_card_finite)
|
||||
norm_bytes_def)
|
||||
|
||||
apply clarsimp
|
||||
apply(rule fu_eq_mask)
|
||||
|
|
@ -219,7 +219,7 @@ apply intro_classes
|
|||
|
||||
apply(clarsimp simp: align_of_def typ_info_array array_tag_def)
|
||||
apply(subst align_td_array_tag)
|
||||
apply (simp add: zero_less_card_finite)
|
||||
apply simp
|
||||
apply(rule dvd_trans)
|
||||
apply(subgoal_tac "align_of TYPE('a) dvd size_of TYPE('a)")
|
||||
apply(simp only: align_of_def)
|
||||
|
|
@ -529,7 +529,7 @@ done
|
|||
|
||||
instance "ty8192" :: finite
|
||||
apply intro_classes
|
||||
apply (simp add: finite univ8192)
|
||||
apply (simp add: univ8192)
|
||||
done
|
||||
|
||||
lemma card8192[simp]: "CARD(ty8192) = CARD(8192)"
|
||||
|
|
@ -537,9 +537,7 @@ apply (simp add: univ8192 card_image inj_on_def)
|
|||
done
|
||||
|
||||
instance "ty8192" :: fourthousand_count
|
||||
apply intro_classes
|
||||
apply (simp add: card8192)
|
||||
done
|
||||
by intro_classes simp
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1091,8 +1091,7 @@ lemma fd_cons_update_access_list_append:
|
|||
(* FIXME MOVE *)
|
||||
lemma min_ll:
|
||||
"min (x + y) x = (x::nat)"
|
||||
by (simp add: min_def)
|
||||
|
||||
by simp
|
||||
|
||||
lemma fd_cons_access_update_list_append:
|
||||
"\<lbrakk> fd_cons_access_update (field_desc_list xs) (size_td_list xs);
|
||||
|
|
@ -1104,7 +1103,7 @@ apply(drule_tac x="take (size_td_list xs) bs" in spec)
|
|||
apply clarsimp
|
||||
apply(erule impE)
|
||||
apply(clarsimp simp: min_def)
|
||||
apply(simp add: access_ti_append min_ll)
|
||||
apply(simp add: access_ti_append)
|
||||
apply(drule_tac x="drop (size_td_list xs) bs" in spec)
|
||||
apply clarsimp
|
||||
apply(drule_tac x="take (size_td_list xs) bs'" in spec)
|
||||
|
|
@ -1363,15 +1362,15 @@ apply(induct t and st and ts and x)
|
|||
apply(drule tf4D)
|
||||
apply clarsimp
|
||||
apply(erule disjE)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x="t2d (a,b)" in spec)
|
||||
apply(thin_tac "\<forall>x y. ?P x y")
|
||||
apply(thin_tac "\<forall>x y. P x y" for P)
|
||||
apply(drule_tac x="y" in spec)
|
||||
apply(fastforce simp: t2d_def image_def)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x="t2d (a,b)" in spec)
|
||||
apply(drule_tac x="y" in spec)
|
||||
apply(fastforce simp: t2d_def image_def)
|
||||
|
|
@ -1380,7 +1379,7 @@ apply(rotate_tac)
|
|||
apply(subst (asm) ti_ind_fn)
|
||||
apply(simp add: t2d_def)
|
||||
apply(clarsimp simp: ti_ind_def)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x="t2d (aa,ba)" in spec)
|
||||
apply(drule_tac x=y in spec)
|
||||
apply(fastforce simp: t2d_def image_def)
|
||||
|
|
@ -1429,9 +1428,11 @@ done
|
|||
lemma ln_fn_disj [rule_format]:
|
||||
"\<forall>x. dt_snd x \<notin> dt_snd ` set xs \<longrightarrow>
|
||||
lf_fn ` lf_set_pair x fn \<inter> lf_fn ` lf_set_list xs fn = {}"
|
||||
apply(induct_tac xs, auto)
|
||||
apply(case_tac x, auto)
|
||||
apply(case_tac a, auto)
|
||||
apply(induct_tac xs, clarsimp)
|
||||
apply(rename_tac a list)
|
||||
apply auto (* FIXME! *)
|
||||
apply(case_tac x, auto) (* FIXME! *)
|
||||
apply(case_tac a, auto) (* FIXME! *)
|
||||
apply(drule lf_set_fn)+
|
||||
apply clarsimp
|
||||
apply(clarsimp simp: prefixeq_def less_eq_list_def)
|
||||
|
|
@ -1504,9 +1505,9 @@ apply(induct t and st and ts and x)
|
|||
apply(clarsimp simp: fd_cons_access_update_def field_desc_list_def)
|
||||
apply(simp add: fu_commutes_def)
|
||||
apply(clarsimp simp: fa_fu_ind_def field_desc_pair_def field_desc_list_def)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(rotate_tac -4)
|
||||
apply(drule_tac x="take (size_td_pair dt_pair) bs" in spec)
|
||||
apply clarsimp
|
||||
|
|
@ -1656,6 +1657,7 @@ lemma fu_commutes_ts [rule_format]:
|
|||
fu_commutes d (update_ti_list_t ts)"
|
||||
apply(induct_tac ts)
|
||||
apply(clarsimp simp: fu_commutes_def)
|
||||
apply(rename_tac a list)
|
||||
apply(clarsimp simp: fu_commutes_def)
|
||||
apply(case_tac a, clarsimp)
|
||||
done
|
||||
|
|
@ -1667,6 +1669,7 @@ lemma fa_fu_ind_ts [rule_format]:
|
|||
(size_td_list ts) n"
|
||||
apply(induct_tac ts)
|
||||
apply(clarsimp simp: fa_fu_ind_def)
|
||||
apply(rename_tac a list)
|
||||
apply(clarsimp simp: fa_fu_ind_def)
|
||||
apply(case_tac a, clarsimp)
|
||||
done
|
||||
|
|
@ -1678,6 +1681,7 @@ lemma fa_fu_ind_ts2 [rule_format]:
|
|||
n (size_td_list ts)"
|
||||
apply(induct_tac ts)
|
||||
apply(clarsimp simp: fa_fu_ind_def)
|
||||
apply(rename_tac a list)
|
||||
apply(clarsimp simp: fa_fu_ind_def)
|
||||
apply(case_tac a, clarsimp)
|
||||
done
|
||||
|
|
@ -1709,6 +1713,7 @@ apply(induct t and st and ts and x)
|
|||
apply fast
|
||||
apply(clarsimp simp: wf_fdp_def)
|
||||
apply(case_tac dt_pair, clarsimp)
|
||||
apply(rename_tac a b)
|
||||
apply(frule_tac x=a in spec)
|
||||
apply(drule_tac x="[b]" in spec)
|
||||
apply clarsimp
|
||||
|
|
@ -1719,6 +1724,7 @@ apply(induct t and st and ts and x)
|
|||
apply(drule_tac x="dt_fst x" in spec, erule impE, rule_tac x="[dt_snd x]" in exI)
|
||||
apply clarsimp
|
||||
apply(case_tac x, clarsimp)
|
||||
apply(rename_tac aa ba)
|
||||
apply(simp add: tf_set_list_mem)
|
||||
apply(rule, clarsimp)
|
||||
apply(clarsimp simp: image_def)
|
||||
|
|
@ -1733,6 +1739,7 @@ apply(induct t and st and ts and x)
|
|||
apply(drule_tac x="dt_fst x" in spec, erule impE, rule_tac x="[dt_snd x]" in exI)
|
||||
apply clarsimp
|
||||
apply(case_tac x, clarsimp)
|
||||
apply(rename_tac aa ba)
|
||||
apply(simp add: tf_set_list_mem)
|
||||
apply(rule, clarsimp)
|
||||
apply(clarsimp simp: image_def)
|
||||
|
|
@ -1744,11 +1751,12 @@ apply(induct t and st and ts and x)
|
|||
apply(drule_tac x=t in spec)
|
||||
apply clarsimp
|
||||
apply(case_tac x, clarsimp)
|
||||
apply(rename_tac aa ba)
|
||||
apply(drule_tac x="[ba]" in spec)
|
||||
apply clarsimp
|
||||
apply(simp add: tf_set_list_mem)
|
||||
apply clarsimp
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=a in spec)
|
||||
apply (erule impE, rule_tac x="[b]" in exI)
|
||||
apply simp
|
||||
|
|
@ -2037,7 +2045,7 @@ apply(induct t and st and ts and x)
|
|||
apply clarsimp+
|
||||
apply(clarsimp simp: fd_cons_desc_def split: option.splits)
|
||||
apply(case_tac f, clarsimp+)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x="a#lista" in spec)
|
||||
apply(drule_tac x="s" in spec)
|
||||
apply(drule_tac x="m + size_td (dt_fst dt_pair)" in spec)
|
||||
|
|
@ -2149,7 +2157,7 @@ lemma fi_fu_consistent [rule_format]:
|
|||
apply(induct t and st and ts and x)
|
||||
apply clarsimp
|
||||
apply(drule wf_fd_cons_structD)
|
||||
apply(clarsimp simp: fd_cons_struct_def fd_cons_double_update_def field_desc_def super_update_bs_def fd_cons_desc_def)
|
||||
apply(clarsimp simp: fd_cons_struct_def fd_cons_double_update_def super_update_bs_def fd_cons_desc_def)
|
||||
apply clarsimp+
|
||||
apply(case_tac f, clarsimp+)
|
||||
apply(clarsimp simp: fd_cons_desc_def split: option.splits)
|
||||
|
|
@ -2164,6 +2172,7 @@ apply(induct t and st and ts and x)
|
|||
apply(drule td_set_list_field_lookup_listD)
|
||||
apply(drule td_set_list_offset_size_m)
|
||||
apply(case_tac dt_pair, clarsimp+)
|
||||
apply(rename_tac aa ba)
|
||||
apply(drule_tac x="drop (size_td aa) bs" in spec)
|
||||
apply simp
|
||||
apply(drule_tac x=v in spec)
|
||||
|
|
@ -2436,7 +2445,7 @@ lemma fa_fu_lookup_disj:
|
|||
apply(induct t and st and ts and x)
|
||||
apply (auto simp: disj_fn_def)
|
||||
apply(clarsimp simp: split: option.splits)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=f in spec)
|
||||
apply(drule_tac x="m + size_td (dt_fst dt_pair)" in spec)
|
||||
apply(drule_tac x=d in spec)
|
||||
|
|
@ -2455,7 +2464,7 @@ apply(induct t and st and ts and x)
|
|||
apply(drule_tac x=m in spec)
|
||||
apply(drule_tac x=d in spec)
|
||||
apply clarsimp
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=f' in spec)
|
||||
apply(drule_tac x=m' in spec)
|
||||
apply(drule_tac x=d' in spec)
|
||||
|
|
@ -2605,7 +2614,7 @@ lemma fa_fu_lookup_disj_inter:
|
|||
apply(induct t and st and ts and x)
|
||||
apply(auto simp: disj_fn_def)
|
||||
apply(clarsimp split: option.splits)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=f in spec)
|
||||
apply(drule_tac x=d in spec)
|
||||
apply(drule_tac x=n in spec)
|
||||
|
|
@ -2632,7 +2641,7 @@ apply(induct t and st and ts and x)
|
|||
apply(drule_tac x=f in spec)
|
||||
apply(drule_tac x=d in spec)
|
||||
apply(drule_tac x=n in spec)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=f' in spec)
|
||||
apply(drule_tac x="m" in spec)
|
||||
apply clarsimp
|
||||
|
|
@ -2669,6 +2678,7 @@ apply(insert fa_fu_lookup_disj_inter(3) [of ts])
|
|||
apply clarsimp
|
||||
done
|
||||
|
||||
|
||||
lemma upd_rf:
|
||||
"length bs = size_of TYPE('a) \<Longrightarrow>
|
||||
update_ti_t (typ_info_t TYPE('a::mem_type_sans_size)) bs v
|
||||
|
|
@ -2714,10 +2724,31 @@ apply(subgoal_tac "align_of (TYPE('a)) dvd size_of ((TYPE('a)))")
|
|||
apply(rule align_size_of)
|
||||
done
|
||||
|
||||
lemma to_bytes_inj:
|
||||
"to_bytes (v::'a::mem_type) = to_bytes (v'::'a) \<Longrightarrow> v=v'"
|
||||
apply (drule_tac x="replicate (size_of TYPE('a)) 0" in fun_cong)
|
||||
apply (drule_tac f="from_bytes::byte list \<Rightarrow> 'a" in arg_cong)
|
||||
apply (simp add: inv)
|
||||
done
|
||||
|
||||
lemmas unat_simps = unat_simps' max_size
|
||||
|
||||
lemmas mem_type_simps [simp] = inv len sz_nzero max_size align
|
||||
|
||||
lemma ptr_aligned_plus:
|
||||
assumes aligned: "ptr_aligned (p::'a::mem_type ptr) "
|
||||
shows "ptr_aligned (p +\<^sub>p i)"
|
||||
proof -
|
||||
have "int (align_of TYPE('a)) dvd (i * int (size_of TYPE('a)))"
|
||||
by (metis dvd_mult zdvd_int align_size_of)
|
||||
with aligned show ?thesis
|
||||
apply (case_tac p, simp add: ptr_aligned_def ptr_add_def scast_id)
|
||||
apply (simp only: unat_simps len_signed)
|
||||
apply (metis align align_size_of dvd_add dvd_mod dvd_mult2 mult.commute)
|
||||
done
|
||||
qed
|
||||
|
||||
|
||||
lemma mem_type_self [simp]:
|
||||
"ptr_val (p::'a::mem_type ptr) \<in> {ptr_val p..+size_of TYPE('a)}"
|
||||
by (rule intvl_self, rule sz_nzero)
|
||||
|
|
@ -2733,8 +2764,9 @@ lemma wf_size_desc_typ_uinfo_t_simp [simp]:
|
|||
|
||||
lemma aggregate_map [simp]:
|
||||
"aggregate (map_td f t) = aggregate t"
|
||||
apply(case_tac t, simp)
|
||||
apply(case_tac typ_struct, simp+)
|
||||
apply(case_tac t)
|
||||
apply(rename_tac st n)
|
||||
apply(case_tac st, simp+)
|
||||
done
|
||||
|
||||
|
||||
|
|
@ -2781,8 +2813,9 @@ lemma field_of_t_simple:
|
|||
"field_of_t p (x::'a::simple_mem_type ptr) \<Longrightarrow> ptr_val p = ptr_val x"
|
||||
apply(clarsimp simp: field_of_t_def)
|
||||
apply(case_tac "typ_uinfo_t TYPE('a)")
|
||||
apply(rename_tac st n)
|
||||
apply clarsimp
|
||||
apply(case_tac typ_struct)
|
||||
apply(case_tac st)
|
||||
apply clarsimp
|
||||
apply(clarsimp simp: field_of_def)
|
||||
apply(subst (asm) unat_eq_zero)
|
||||
|
|
@ -2790,26 +2823,6 @@ apply(case_tac typ_struct)
|
|||
apply simp
|
||||
done
|
||||
|
||||
(* FIXME: move to where class defined *)
|
||||
lemma to_bytes_inj:
|
||||
"to_bytes (v::'a::mem_type) = to_bytes (v'::'a) \<Longrightarrow> v=v'"
|
||||
apply(drule_tac x="replicate (size_of TYPE('a)) 0" in fun_cong)
|
||||
apply (drule_tac f="from_bytes::byte list \<Rightarrow> 'a" in arg_cong)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma ptr_aligned_plus:
|
||||
assumes aligned: "ptr_aligned (p::'a::mem_type ptr) "
|
||||
shows "ptr_aligned (p +\<^sub>p i)"
|
||||
proof -
|
||||
have "int (align_of TYPE('a)) dvd (i * int (size_of TYPE('a)))"
|
||||
by (metis dvd_mult zdvd_int align_size_of)
|
||||
with aligned show ?thesis
|
||||
apply (case_tac p, simp add: ptr_aligned_def ptr_add_def scast_id)
|
||||
apply (simp only: unat_simps len_signed)
|
||||
apply (metis align align_size_of dvd_add dvd_mod dvd_mult2 mult.commute)
|
||||
done
|
||||
qed
|
||||
|
||||
lemma fold_td'_unfold:
|
||||
"fold_td' t = (let (f,s) = t in (case s of TypDesc st nm \<Rightarrow> case st of
|
||||
|
|
@ -2828,9 +2841,9 @@ lemma fold_td_alt_def':
|
|||
TypScalar n algn d \<Rightarrow> d |
|
||||
TypAggregate ts \<Rightarrow> f nm (map (\<lambda>x. (fold_td f (dt_fst x),dt_snd x)) ts))"
|
||||
apply(case_tac t)
|
||||
apply auto
|
||||
apply(auto simp: fold_td_def split: typ_desc.split typ_struct_splits dt_pair.splits)
|
||||
apply(subgoal_tac "map ( \<lambda>x. (fold_td' (f, dt_fst x), dt_snd x)) lista = map (case_dt_pair (\<lambda>a. Pair (fold_td' (f, a)))) lista")
|
||||
apply(auto split: typ_desc.split typ_struct_splits dt_pair.splits) (* FIXME *)
|
||||
apply(rename_tac xs)
|
||||
apply(subgoal_tac "map ( \<lambda>x. (fold_td' (f, dt_fst x), dt_snd x)) xs = map (case_dt_pair (\<lambda>a. Pair (fold_td' (f, a)))) xs")
|
||||
apply(simp only:)
|
||||
apply auto
|
||||
apply(clarsimp split: dt_pair.splits)
|
||||
|
|
@ -2900,25 +2913,6 @@ apply(insert align_td_fm'(1) [of t])
|
|||
apply auto
|
||||
done
|
||||
|
||||
lemma blah0 [rule_format]:
|
||||
"\<forall>f t n. DTPair t n \<in> set (map_td_list f ts) \<longrightarrow> (n \<in> dt_snd ` set ts)"
|
||||
apply(induct_tac ts)
|
||||
apply auto
|
||||
apply(case_tac a, auto)
|
||||
done
|
||||
|
||||
lemma blah1:
|
||||
"map_td_pair f x = DTPair a b \<Longrightarrow> b = dt_snd x"
|
||||
apply(case_tac x)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma blah2 [rule_format]:
|
||||
"\<forall>aa a b. (DTPair aa b \<in> set ts \<longrightarrow>
|
||||
b \<in> dt_snd ` set (map_td_list (\<lambda>n x d. True) ts))"
|
||||
apply(induct_tac ts, auto)
|
||||
done
|
||||
|
||||
lemma case_dt_pair:
|
||||
"snd ` case_dt_pair (\<lambda>t. Pair (f t)) ` X = dt_snd ` X"
|
||||
apply(auto simp: image_def split: dt_pair.splits)
|
||||
|
|
@ -2931,33 +2925,24 @@ apply(rule_tac x=xa in bexI)
|
|||
apply assumption
|
||||
done
|
||||
|
||||
lemma map_DTPair_dt_snd:
|
||||
"map_td_pair f x = DTPair a b \<Longrightarrow> b = dt_snd x"
|
||||
by (metis dt_pair.inject map_td'_map'(4))
|
||||
|
||||
lemma wf_desc_fm':
|
||||
"wf_desc (t::'a typ_desc) = fold_td wfd (map_td (\<lambda>n x d. True) t)"
|
||||
"wf_desc_struct (st::'a typ_struct) = fold_td_struct (typ_name t) wfd (map_td_struct (\<lambda>n x d. True) st)"
|
||||
"wf_desc_list (ts::'a typ_pair list) = fold_td_list (typ_name t) wfd (map_td_list (\<lambda>n x d. True) ts)"
|
||||
"wf_desc_pair (x::'a typ_pair) = fold_td_pair wfd (map_td_pair (\<lambda>n x d. True) x)"
|
||||
apply(induct t and st and ts and x)
|
||||
apply(auto simp: wfd_def image_comp[symmetric] split: dt_pair.splits)
|
||||
apply(drule blah0)
|
||||
apply simp
|
||||
apply(drule blah1)
|
||||
apply simp
|
||||
apply(drule blah1)
|
||||
apply simp
|
||||
apply(case_tac x)
|
||||
apply simp
|
||||
apply(case_tac dt_pair, simp)
|
||||
apply(clarsimp simp: case_dt_pair)
|
||||
apply(drule blah2)
|
||||
apply simp
|
||||
apply(auto simp: wfd_def image_comp[symmetric] split: dt_pair.splits) (* FIXME *)
|
||||
apply (metis (no_types, lifting) dt_snd.simps dt_snd_map_td_list image_eqI map_td'_map'(4))
|
||||
apply (metis map_DTPair_dt_snd case_dt_pair dt_snd_map_td_list image_eqI)
|
||||
done
|
||||
|
||||
|
||||
lemma wf_desc_fm:
|
||||
"wf_desc (t::'a typ_desc) \<equiv> fold_td wfd (map_td (\<lambda>n algn d. True) t)"
|
||||
apply(insert wf_desc_fm'(1) [of t])
|
||||
apply auto
|
||||
done
|
||||
using wf_desc_fm'(1) [of t] by auto
|
||||
|
||||
lemma update_tag_list_empty [simp]:
|
||||
"(map_td_list f xs = []) = (xs = [])"
|
||||
|
|
@ -2974,8 +2959,6 @@ done
|
|||
|
||||
lemma wf_size_desc_fm:
|
||||
"wf_size_desc (t::'a typ_desc) \<equiv> fold_td wfsd (map_td (\<lambda>n algn d. 0 < n) t)"
|
||||
apply(insert wf_size_desc_fm'(1) [of t])
|
||||
apply auto
|
||||
done
|
||||
using wf_size_desc_fm'(1) [of t] by auto
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -30,7 +30,8 @@ lemma aggregate_empty_typ_info [simp]:
|
|||
|
||||
lemma aggregate_extend_ti [simp]:
|
||||
"aggregate (extend_ti tag t f)"
|
||||
apply(case_tac tag, simp)
|
||||
apply(case_tac tag)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
done
|
||||
|
||||
|
|
@ -137,7 +138,8 @@ lemma field_names_list_empty_typ_info [simp]:
|
|||
lemma field_names_list_extend_ti [simp]:
|
||||
"set (field_names_list (extend_ti tag t fn)) = set (field_names_list tag) \<union> {fn}"
|
||||
apply(clarsimp simp: field_names_list_def)
|
||||
apply(case_tac tag, simp)
|
||||
apply(case_tac tag)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, simp+)
|
||||
done
|
||||
|
||||
|
|
@ -170,21 +172,24 @@ lemma wf_desc_extend_ti:
|
|||
"\<lbrakk> wf_desc tag; wf_desc t; f \<notin> set (field_names_list tag) \<rbrakk> \<Longrightarrow>
|
||||
wf_desc (extend_ti tag t f)"
|
||||
apply(clarsimp simp: field_names_list_def)
|
||||
apply(case_tac tag, clarsimp)
|
||||
apply(case_tac tag)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, clarsimp+)
|
||||
done
|
||||
|
||||
lemma foldl_append_length [rule_format]:
|
||||
"\<forall>s. length (foldl op @ s xs) \<ge> length s"
|
||||
apply(induct_tac xs, auto)
|
||||
apply(drule_tac x="s@a" in spec)
|
||||
lemma foldl_append_length:
|
||||
"length (foldl op @ s xs) \<ge> length s"
|
||||
apply(induct xs arbitrary: s, clarsimp)
|
||||
apply(rename_tac a list s)
|
||||
apply(drule_tac x="s@a" in meta_spec)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma foldl_append_nmem [rule_format]:
|
||||
"\<forall>s. s \<noteq> [] \<longrightarrow> foldl op @ s xs \<notin> set xs"
|
||||
apply(induct_tac xs, auto)
|
||||
apply(drule_tac x="s@a" in spec)
|
||||
lemma foldl_append_nmem:
|
||||
"s \<noteq> [] \<Longrightarrow> foldl op @ s xs \<notin> set xs"
|
||||
apply(induct xs arbitrary: s, clarsimp)
|
||||
apply(rename_tac a list s)
|
||||
apply(drule_tac x="s@a" in meta_spec)
|
||||
apply clarsimp
|
||||
apply(subgoal_tac "length (foldl op @ (s@a) list) \<ge> length (s@a)")
|
||||
apply simp
|
||||
|
|
@ -196,7 +201,7 @@ lemma wf_desc_ti_pad_combine:
|
|||
wf_desc (ti_pad_combine n tag)"
|
||||
apply(clarsimp simp: ti_pad_combine_def Let_def)
|
||||
apply(erule wf_desc_extend_ti)
|
||||
apply simp
|
||||
apply simp
|
||||
apply(rule foldl_append_nmem, simp)
|
||||
done
|
||||
|
||||
|
|
@ -209,29 +214,24 @@ lemma wf_desc_ti_typ_combine:
|
|||
wf_desc (ti_typ_combine (t_b::'a::wf_type itself) f_ab f_upd_ab fn tag)"
|
||||
apply(clarsimp simp: ti_typ_combine_def Let_def)
|
||||
apply(erule wf_desc_extend_ti)
|
||||
apply simp+
|
||||
apply simp+
|
||||
done
|
||||
|
||||
lemma wf_desc_ti_typ_pad_combine:
|
||||
"\<lbrakk> wf_desc tag; fn \<notin> set (field_names_list tag);
|
||||
hd fn \<noteq> CHR ''!'' \<rbrakk> \<Longrightarrow>
|
||||
wf_desc (ti_typ_pad_combine (t_b::'a::wf_type itself) f_ab f_upd_ab fn tag)"
|
||||
apply(auto simp: ti_typ_pad_combine_def Let_def)
|
||||
apply(rule wf_desc_ti_typ_combine)
|
||||
apply auto
|
||||
apply(erule wf_desc_ti_pad_combine)
|
||||
apply(erule (1) wf_desc_ti_typ_combine)
|
||||
done
|
||||
unfolding ti_typ_pad_combine_def Let_def
|
||||
by (auto intro!: wf_desc_ti_typ_combine wf_desc_ti_pad_combine)
|
||||
|
||||
lemma wf_desc_final_pad:
|
||||
"wf_desc tag \<Longrightarrow> wf_desc (final_pad tag)"
|
||||
apply(clarsimp simp: final_pad_def Let_def)
|
||||
apply(erule wf_desc_ti_pad_combine)
|
||||
done
|
||||
by (auto simp: final_pad_def Let_def elim: wf_desc_ti_pad_combine)
|
||||
|
||||
lemma wf_size_desc_extend_ti:
|
||||
"\<lbrakk> wf_size_desc tag; wf_size_desc t \<rbrakk> \<Longrightarrow> wf_size_desc (extend_ti tag t fn)"
|
||||
apply(case_tac tag, auto)
|
||||
apply(rename_tac typ_struct list)
|
||||
apply(case_tac typ_struct, auto)
|
||||
done
|
||||
|
||||
|
|
@ -242,13 +242,6 @@ apply(erule wf_size_desc_extend_ti)
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma wf_size_desc_map:
|
||||
"wf_size_desc (map_td f t) = wf_size_desc (t::'a typ_info)"
|
||||
"wf_size_desc_struct (map_td_struct f st) = wf_size_desc_struct (st::'a field_desc typ_struct)"
|
||||
"wf_size_desc_list (map_td_list f ts) = wf_size_desc_list (ts::('a typ_info,field_name) dt_pair list)"
|
||||
"wf_size_desc_pair (map_td_pair f x) = wf_size_desc_pair (x::('a typ_info,field_name) dt_pair)"
|
||||
by (induct t and st and ts and x) auto
|
||||
|
||||
lemma wf_size_desc_adjust_ti:
|
||||
"wf_size_desc (adjust_ti t f g) = wf_size_desc (t::'a typ_info)"
|
||||
by (simp add: adjust_ti_def wf_size_desc_map)
|
||||
|
|
@ -382,7 +375,7 @@ lemma update_ti_adjust_ti:
|
|||
"fg_cons f g \<Longrightarrow> update_ti_t (adjust_ti t f g) bs v =
|
||||
g (update_ti_t t bs (f v)) v"
|
||||
apply(insert field_desc_adjust_ti(1) [of f g t])
|
||||
apply(clarsimp simp: field_desc_def update_desc_def)
|
||||
apply(clarsimp simp: update_desc_def)
|
||||
done
|
||||
|
||||
declare field_desc_def [simp del]
|
||||
|
|
@ -410,16 +403,10 @@ done
|
|||
lemma align_of_extend_ti [simp]:
|
||||
"aggregate ti \<Longrightarrow> align_td (extend_ti ti t fn) = max (align_td ti) (align_td t)"
|
||||
apply(case_tac ti, clarsimp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, clarsimp+)
|
||||
done
|
||||
|
||||
lemma align_of_map [simp]:
|
||||
"align_td (map_td f t) = align_td (t::'a typ_info)"
|
||||
"align_td_struct (map_td_struct f st) = align_td_struct (st::'a field_desc typ_struct)"
|
||||
"align_td_list (map_td_list f ts) = align_td_list (ts::('a typ_info,field_name) dt_pair list)"
|
||||
"align_td_pair (map_td_pair f x) = align_td_pair (x::('a typ_info,field_name) dt_pair)"
|
||||
by(induct t and st and ts and x) auto
|
||||
|
||||
lemma align_of_adjust_ti [simp]:
|
||||
"align_td (adjust_ti t f g) = align_td (t::'a typ_info)"
|
||||
by (simp add: adjust_ti_def)
|
||||
|
|
@ -459,6 +446,7 @@ lemma fc_extend_ti:
|
|||
"\<lbrakk> fu_commutes (update_ti_t s) h; fu_commutes (update_ti_t t) h \<rbrakk>
|
||||
\<Longrightarrow> fu_commutes (update_ti_t (extend_ti s t fn)) h"
|
||||
apply(case_tac s, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(auto simp: fu_commutes_def)
|
||||
done
|
||||
|
|
@ -517,6 +505,7 @@ lemma fu_eq_mask_ti_pad_combine:
|
|||
"\<lbrakk> fu_eq_mask ti f; aggregate ti \<rbrakk> \<Longrightarrow> fu_eq_mask (ti_pad_combine n ti) f"
|
||||
apply(clarsimp simp: ti_pad_combine_def Let_def)
|
||||
apply(case_tac ti, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(clarsimp simp: fu_eq_mask_def update_ti_list_t_def)
|
||||
done
|
||||
|
|
@ -544,7 +533,9 @@ lemma fu_eq_mask_ti_typ_combine:
|
|||
apply(frule fg_cons_upd_local)
|
||||
apply(auto simp: ti_typ_combine_def Let_def)
|
||||
apply(case_tac ti, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(rename_tac xs')
|
||||
apply(auto simp: fu_eq_mask_def)
|
||||
apply(simp add: update_ti_adjust_ti)
|
||||
apply(auto simp: update_ti_list_t_def size_of_def)
|
||||
|
|
@ -552,20 +543,20 @@ apply(subst upd [where w="f undefined"])
|
|||
apply(simp add: size_of_def)
|
||||
apply(subst upd [where w="f undefined" and v="f (h v')"])
|
||||
apply(simp add: size_of_def)
|
||||
apply(subgoal_tac "fu_commutes (\<lambda>v. update_ti_list_t lista v) g")
|
||||
apply(subgoal_tac "fu_commutes (\<lambda>v. update_ti_list_t xs' v) g")
|
||||
apply(clarsimp simp: fu_commutes_def)
|
||||
apply(frule_tac x="h v" in spec)
|
||||
apply(rotate_tac -1)
|
||||
apply(drule_tac x="take (size_td_list lista) bs" in spec)
|
||||
apply(drule_tac x="take (size_td_list xs') bs" in spec)
|
||||
apply(drule_tac x="update_ti_t (typ_info_t TYPE('a))
|
||||
(drop (size_td_list lista) bs) (f undefined)" in spec)
|
||||
(drop (size_td_list xs') bs) (f undefined)" in spec)
|
||||
apply(frule_tac x="h v'" in spec)
|
||||
apply(rotate_tac -1)
|
||||
apply(drule_tac x="take (size_td_list lista) bs" in spec)
|
||||
apply(drule_tac x="take (size_td_list xs') bs" in spec)
|
||||
apply(drule_tac x="update_ti_t (typ_info_t TYPE('a))
|
||||
(drop (size_td_list lista) bs) (f undefined)" in spec)
|
||||
(drop (size_td_list xs') bs) (f undefined)" in spec)
|
||||
apply(clarsimp simp: update_ti_list_t_def)
|
||||
apply(drule_tac x="take (size_td_list lista) bs" in spec)
|
||||
apply(drule_tac x="take (size_td_list xs') bs" in spec)
|
||||
apply simp
|
||||
apply(rotate_tac -1)
|
||||
apply(drule_tac x="v" in spec)
|
||||
|
|
@ -573,18 +564,18 @@ apply(subgoal_tac "fu_commutes (\<lambda>v. update_ti_list_t lista v) g")
|
|||
apply(drule_tac x="v'" in spec)
|
||||
|
||||
apply(frule_tac x="h v" in spec)
|
||||
apply(drule_tac x="(take (size_td_list lista) bs)" in spec)
|
||||
apply(drule_tac x="(take (size_td_list xs') bs)" in spec)
|
||||
apply(drule_tac x="f undefined" in spec)
|
||||
apply(frule_tac x="h v'" in spec)
|
||||
apply(drule_tac x="(take (size_td_list lista) bs)" in spec)
|
||||
apply(drule_tac x="(take (size_td_list xs') bs)" in spec)
|
||||
apply(drule_tac x="f undefined" in spec)
|
||||
apply(thin_tac "\<forall>v bs bs'. ?X v bs bs'")
|
||||
apply(thin_tac "\<forall>v bs bs'. X v bs bs'" for X)
|
||||
apply simp
|
||||
apply(unfold upd_local_def)
|
||||
apply fast
|
||||
apply(unfold fu_commutes_def)
|
||||
apply(thin_tac "\<forall>bs. ?X bs")
|
||||
apply(thin_tac "\<forall>x y z a. ?X x y z a")
|
||||
apply(thin_tac "\<forall>bs. X bs" for X)
|
||||
apply(thin_tac "\<forall>x y z a. X x y z a" for X)
|
||||
apply(clarsimp simp: update_ti_list_t_def)
|
||||
done
|
||||
|
||||
|
|
@ -616,6 +607,7 @@ done
|
|||
lemma size_td_extend_ti:
|
||||
"aggregate s \<Longrightarrow> size_td (extend_ti s t fn) = size_td s + size_td t"
|
||||
apply(case_tac s, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
done
|
||||
|
||||
|
|
@ -638,23 +630,15 @@ apply auto
|
|||
apply(simp add: padup_dvd)
|
||||
done
|
||||
|
||||
lemma size_td_lt_extend_ti:
|
||||
"aggregate s \<Longrightarrow> size_td (extend_ti s t fn) = size_td s + size_td t"
|
||||
apply(case_tac s, auto)
|
||||
apply(case_tac typ_struct, auto)
|
||||
done
|
||||
|
||||
lemma size_td_lt_ti_pad_combine:
|
||||
"aggregate t \<Longrightarrow> size_td (ti_pad_combine n t) = size_td t + n"
|
||||
apply(clarsimp simp: ti_pad_combine_def Let_def)
|
||||
apply(simp add: size_td_lt_extend_ti)
|
||||
done
|
||||
by (metis add.commute size_td_ti_pad_combine)
|
||||
|
||||
lemma size_td_lt_ti_typ_combine:
|
||||
"aggregate ti \<Longrightarrow> size_td (ti_typ_combine (t::'b::c_type itself) f g fn ti) =
|
||||
size_td ti + size_td (typ_info_t TYPE('b))"
|
||||
apply(clarsimp simp: ti_typ_combine_def Let_def)
|
||||
apply(simp add: size_td_lt_extend_ti)
|
||||
apply(simp add: size_td_extend_ti)
|
||||
done
|
||||
|
||||
lemma size_td_lt_ti_typ_pad_combine:
|
||||
|
|
@ -689,7 +673,9 @@ lemma lf_fn_disj_fn [rule_format]:
|
|||
"\<forall>fn t tn. fn \<notin> set (field_names_list (TypDesc (TypAggregate xs) tn))
|
||||
\<longrightarrow> lf_fn ` lf_set_list xs [] \<inter> lf_fn ` lf_set t [fn] = {}"
|
||||
apply(induct_tac xs)
|
||||
apply clarsimp+
|
||||
apply clarsimp
|
||||
apply(rename_tac a list)
|
||||
apply clarsimp
|
||||
apply(drule_tac x=fn in spec)
|
||||
apply(erule impE)
|
||||
apply(clarsimp simp: field_names_list_def split: split_if_asm)
|
||||
|
|
@ -712,6 +698,7 @@ lemma wf_lf_extend_ti:
|
|||
ti_ind (lf_set ti []) (lf_set t []) \<rbrakk> \<Longrightarrow>
|
||||
wf_lf (lf_set (extend_ti ti t fn) [])"
|
||||
apply(case_tac ti, clarsimp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, clarsimp+)
|
||||
apply(subst wf_lf_fn)
|
||||
apply simp+
|
||||
|
|
@ -776,6 +763,7 @@ lemma ti_ind_extend_ti:
|
|||
ti_ind (lf_set ti []) (lf_set (adjust_ti k f g) []) \<rbrakk>
|
||||
\<Longrightarrow> ti_ind (lf_set (extend_ti ti t fn) []) (lf_set (adjust_ti k f g) [])"
|
||||
apply(case_tac ti, clarsimp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, clarsimp)
|
||||
apply(subst ti_ind_fn)
|
||||
apply simp
|
||||
|
|
@ -857,6 +845,7 @@ lemma g_ind_extend_ti:
|
|||
"\<lbrakk> g_ind (lf_set s []) g; g_ind (lf_set t []) g \<rbrakk> \<Longrightarrow>
|
||||
g_ind (lf_set (extend_ti s t fn) []) g"
|
||||
apply(case_tac s, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(auto simp: g_ind_def image_Un fu_s_comm_k_def)
|
||||
apply(subgoal_tac "lf_fd xb \<in> lf_fd ` lf_set t [fn]")
|
||||
|
|
@ -908,6 +897,7 @@ lemma f_ind_extend_ti:
|
|||
"\<lbrakk> f_ind f (lf_fd ` lf_set s []); f_ind f (lf_fd ` lf_set t []) \<rbrakk> \<Longrightarrow>
|
||||
f_ind f (lf_fd ` lf_set (extend_ti s t fn) [])"
|
||||
apply(case_tac s, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(auto simp: f_ind_def)
|
||||
apply(subgoal_tac "lf_fd xa \<in> lf_fd ` lf_set t [fn]")
|
||||
|
|
@ -959,6 +949,7 @@ lemma fa_ind_extend_ti:
|
|||
"\<lbrakk> fa_ind (lf_fd ` lf_set s []) g; fa_ind (lf_fd ` lf_set t []) g \<rbrakk> \<Longrightarrow>
|
||||
fa_ind (lf_fd ` lf_set (extend_ti s t fn) []) g"
|
||||
apply(case_tac s, auto)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(auto simp: fa_ind_def )
|
||||
apply(subgoal_tac "lf_fd xa \<in> lf_fd ` lf_set t [fn]")
|
||||
|
|
@ -1054,7 +1045,7 @@ lemma align_td_field_lookup:
|
|||
apply(induct t and st and ts and x)
|
||||
apply auto
|
||||
apply(clarsimp split: option.splits)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=f in spec)
|
||||
apply(drule_tac x="m+size_td (dt_fst dt_pair)" in spec)
|
||||
apply(drule_tac x=s in spec)
|
||||
|
|
@ -1069,7 +1060,8 @@ done
|
|||
lemma align_field_extend_ti:
|
||||
"\<lbrakk> align_field s; align_field t; 2^(align_td t) dvd size_td s \<rbrakk> \<Longrightarrow>
|
||||
align_field (extend_ti s t fn)"
|
||||
apply(case_tac s, clarsimp, thin_tac "s = ?X")
|
||||
apply(case_tac s, clarsimp, thin_tac "s = X" for X)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, clarsimp)
|
||||
apply(clarsimp simp: align_field_def split: option.splits)
|
||||
apply(clarsimp simp: align_field_def)
|
||||
|
|
@ -1208,6 +1200,7 @@ lemma npf_extend_ti [simp]:
|
|||
"non_padding_fields (extend_ti s t fn) = non_padding_fields s @
|
||||
(if hd fn = CHR ''!'' then [] else [fn])"
|
||||
apply(case_tac s, clarsimp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ lemma aggregate_x_struct_ex_tag [simp]:
|
|||
lemma
|
||||
"upd_local (x_example_update \<circ> (\<lambda>x _. x))"
|
||||
apply(auto simp: upd_local_def )
|
||||
apply(tactic {* Record.split_tac 1 *} )
|
||||
apply(tactic {* Record.split_tac @{context} 1 *} )
|
||||
apply simp
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ type_synonym typ_base = bool
|
|||
datatype s_heap_index = SIndexVal | SIndexTyp nat
|
||||
datatype s_heap_value = SValue byte | STyp "typ_uinfo \<times> typ_base"
|
||||
|
||||
primrec
|
||||
primrec (nonexhaustive)
|
||||
s_heap_tag :: "s_heap_value \<Rightarrow> typ_uinfo \<times> typ_base"
|
||||
where
|
||||
"s_heap_tag (STyp t) = t"
|
||||
|
|
|
|||
|
|
@ -47,7 +47,6 @@ where
|
|||
F \<subseteq> fields TYPE('a) \<and>
|
||||
dom s = s_footprint p - fs_footprint p F \<and> wf_heap_val s"
|
||||
|
||||
(*XXX: 0,1000 or 1000,1000?*)
|
||||
notation (input)
|
||||
mfs_sep_map ("_ \<mapsto>\<^sub>_\<^sup>_ _" [56,0,1000,51] 56)
|
||||
|
||||
|
|
@ -237,23 +236,23 @@ apply(case_tac "x \<in> s_footprint p")
|
|||
apply(case_tac x, clarsimp)
|
||||
apply(drule_tac x=aa in fun_cong)
|
||||
apply(auto simp: s_footprint_restrict lift_state_def
|
||||
split: s_heap_index.splits split_if_asm option.splits)
|
||||
split: s_heap_index.splits split_if_asm option.splits) (* FIXME! *)
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(drule_tac x="nat" in fun_cong)
|
||||
apply(drule_tac x="x2" in fun_cong)
|
||||
apply clarsimp
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(drule_tac x="nat" in fun_cong)
|
||||
apply(drule_tac x="x2" in fun_cong)
|
||||
apply clarsimp
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(drule_tac x="nat" in fun_cong)
|
||||
apply(drule_tac x="x2" in fun_cong)
|
||||
apply clarsimp
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(drule_tac x="nat" in fun_cong)
|
||||
apply(drule_tac x="x2" in fun_cong)
|
||||
apply clarsimp
|
||||
apply(clarsimp simp: restrict_s_def)
|
||||
apply(drule_tac x="nat" in fun_cong)
|
||||
apply(drule_tac x="x2" in fun_cong)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
|
|
@ -353,7 +352,7 @@ apply(erule impE)
|
|||
apply simp
|
||||
apply simp
|
||||
apply(subgoal_tac "unat (q - p) = unat (1::32 word) + unat (q - (p + 1))")
|
||||
apply(simp add: unat_1)
|
||||
apply(simp)
|
||||
apply(subgoal_tac "q - (p + 1) = (q-p) - 1")
|
||||
apply(simp only:)
|
||||
apply(subst unat_minus_one)
|
||||
|
|
@ -397,7 +396,7 @@ apply(induct_tac n)
|
|||
apply simp
|
||||
apply clarsimp
|
||||
apply rule
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=p in spec)
|
||||
apply(erule impE)
|
||||
apply(rule intvl_self)
|
||||
|
|
@ -697,7 +696,7 @@ oops
|
|||
|
||||
lemma sep_map_mfs_sep_map_empty:
|
||||
"(p \<mapsto>\<^sub>g (v::'a::mem_type)) = (p \<mapsto>\<^sub>g\<^sup>({}) v)"
|
||||
by (auto simp: sep_map_def mfs_sep_map_def map_add_dom_eq intro!: ext)
|
||||
by (auto simp: sep_map_def mfs_sep_map_def map_add_dom_eq)
|
||||
|
||||
lemma fd_cons_double_update:
|
||||
"\<lbrakk> fd_cons t; length bs = length bs' \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -814,7 +813,7 @@ lemma field_access_take_drop:
|
|||
access_ti\<^sub>0 s v"
|
||||
apply(induct t and st and ts and x)
|
||||
apply(auto simp: access_ti\<^sub>0_def)
|
||||
apply(thin_tac "All ?P")+
|
||||
apply(thin_tac "All P" for P)+
|
||||
apply(subst (asm) take_all)
|
||||
apply(drule wf_fd_cons_structD)
|
||||
apply(clarsimp simp: fd_cons_struct_def fd_cons_desc_def fd_cons_length_def)
|
||||
|
|
@ -1425,6 +1424,7 @@ apply(clarsimp split: option.splits)
|
|||
apply(erule impE)
|
||||
apply simp
|
||||
apply(case_tac dt_pair, simp+)
|
||||
apply(rename_tac a b)
|
||||
apply(drule_tac x=bs in spec)
|
||||
apply(drule_tac x="drop (size_td a) bs'" in spec)
|
||||
apply clarsimp
|
||||
|
|
@ -1588,7 +1588,7 @@ lemma from_bytes_heap_list_s_update:
|
|||
update_ti_t s (to_bytes_p w) (from_bytes (heap_list_s (singleton_t p v ++ x) (size_of TYPE('a)) (ptr_val p)))"
|
||||
apply(subst map_add_restrict_UNIV [where X="s_footprint_untyped (&(p\<rightarrow>f)) (export_uinfo s)" and h="singleton_t p v"])
|
||||
apply(clarsimp simp: fs_footprint_def field_footprint_def field_lvalue_def)
|
||||
apply(thin_tac "dom x = ?X")
|
||||
apply(thin_tac "dom x = X" for X)
|
||||
apply(clarsimp simp: field_typ_def field_typ_untyped_def)
|
||||
apply force
|
||||
apply simp
|
||||
|
|
@ -1924,7 +1924,7 @@ lemma sep_cut_0 [simp]:
|
|||
|
||||
lemma heap_merge_restrict_dom_un:
|
||||
"dom s = P \<union> Q \<Longrightarrow> (s|`P) ++ (s|`Q) = s"
|
||||
by (force simp: map_add_def restrict_map_def intro: ext split: option.splits)
|
||||
by (force simp: map_add_def restrict_map_def split: option.splits)
|
||||
|
||||
lemma sep_cut_split:
|
||||
assumes sc: "sep_cut p y s" and le: "x \<le> y"
|
||||
|
|
|
|||
|
|
@ -636,7 +636,7 @@ apply(subgoal_tac "(a,b) \<notin> s_footprint (p (restrict_htd s X))")
|
|||
apply(drule (1) subsetD)
|
||||
apply(clarsimp simp: restrict_htd_def)
|
||||
apply(drule dom_restrict_s, clarsimp)
|
||||
apply(thin_tac "?P \<notin> ?Q")
|
||||
apply(thin_tac "P \<notin> Q" for P Q)
|
||||
apply(auto simp: restrict_htd_def lift_state_def split_def split: s_heap_index.splits split: option.splits)
|
||||
apply(subst (asm) ptr_retyp_d_eq_fst)
|
||||
apply(clarsimp split: split_if_asm)
|
||||
|
|
|
|||
|
|
@ -133,7 +133,7 @@ done
|
|||
lemma sep_map'_any_old:
|
||||
"(p \<hookrightarrow>\<^sup>i\<^sub>g -) = (\<lambda>s. \<exists>v. (p \<hookrightarrow>\<^sup>i\<^sub>g v) s)"
|
||||
apply(rule ext)
|
||||
apply(simp add: sep_map'_inv_def sep_map'_any_inv_def sep_map'_any_def sep_conj_exists sep_conj_exists2)
|
||||
apply(simp add: sep_map'_inv_def sep_map'_any_inv_def sep_map'_any_def sep_conj_exists)
|
||||
done
|
||||
|
||||
lemma sep_map_sep_map' [simp]:
|
||||
|
|
|
|||
|
|
@ -28,9 +28,7 @@ lemma sep_conj_extract1D:
|
|||
|
||||
lemma sep_conj_extract2D:
|
||||
"sep_conj_extract P s \<Longrightarrow> P s \<and> (sep_conj_extract P \<and>\<^sup>* sep_true) s"
|
||||
apply(simp add: sep_conj_extract_def)
|
||||
apply(erule sep_conj_sep_true)
|
||||
done
|
||||
by (auto simp: sep_conj_extract_def elim: sep_conj_sep_true)
|
||||
|
||||
lemma sep_conj_extract_assoc:
|
||||
"sep_conj_extract ((P \<and>\<^sup>* Q) \<and>\<^sup>* R) = sep_conj_extract (P \<and>\<^sup>* (Q \<and>\<^sup>* R))"
|
||||
|
|
@ -39,7 +37,7 @@ lemma sep_conj_extract_assoc:
|
|||
lemma sep_conj_extract_decomposeD:
|
||||
"(sep_conj_extract (P \<and>\<^sup>* Q) \<and>\<^sup>* sep_true) s \<Longrightarrow> sep_points P s \<and>
|
||||
(sep_conj_extract Q \<and>\<^sup>* sep_true) s"
|
||||
apply rule
|
||||
apply (rule conjI)
|
||||
apply(simp add: sep_conj_extract_def sep_points_def sep_conj_ac)
|
||||
apply(erule (1) sep_conj_impl, simp)
|
||||
apply(simp add: sep_conj_extract_def sep_conj_ac)
|
||||
|
|
@ -65,24 +63,24 @@ lemma sep_point_map_excD:
|
|||
|
||||
lemma sep_point_otherD:
|
||||
"sep_points P s \<Longrightarrow> True"
|
||||
by simp
|
||||
by (rule TrueI)
|
||||
|
||||
ML {*
|
||||
|
||||
val sep_point_ds = [@{thm sep_point_mapD}, @{thm sep_point_map_excD}]
|
||||
|
||||
fun sep_point_tacs ds ctxt = [
|
||||
REPEAT1 (dresolve_tac [@{thm sep_conj_extract1D}] 1),
|
||||
REPEAT1 (dresolve_tac [@{thm sep_conj_extract2D}] 1),
|
||||
REPEAT1 (dresolve_tac ctxt [@{thm sep_conj_extract1D}] 1),
|
||||
REPEAT1 (dresolve_tac ctxt [@{thm sep_conj_extract2D}] 1),
|
||||
clarify_tac ctxt 1,
|
||||
TRY (full_simp_tac (put_simpset HOL_ss ctxt addsimps
|
||||
[@{thm sep_conj_extract_assoc}]) 1),
|
||||
REPEAT (dresolve_tac [@{thm sep_conj_extract_decomposeD},
|
||||
REPEAT (dresolve_tac ctxt [@{thm sep_conj_extract_decomposeD},
|
||||
@{thm sep_conj_extract_decomposeD2}] 1 THEN
|
||||
clarify_tac ctxt 1),
|
||||
TRY (full_simp_tac ctxt 1),
|
||||
REPEAT (dresolve_tac (sep_point_ds@ds) 1),
|
||||
REPEAT (dresolve_tac [@{thm sep_point_otherD}] 1),
|
||||
REPEAT (dresolve_tac ctxt (sep_point_ds@ds) 1),
|
||||
REPEAT (dresolve_tac ctxt [@{thm sep_point_otherD}] 1),
|
||||
TRY (full_simp_tac ctxt 1)
|
||||
]
|
||||
|
||||
|
|
@ -149,21 +147,21 @@ lemma sep_emp_rem:
|
|||
|
||||
lemma sep_mark2_left:
|
||||
"(P \<and>\<^sup>* (sep_mark2 Q \<and>\<^sup>* R)) = (sep_mark2 Q \<and>\<^sup>* (P \<and>\<^sup>* R))"
|
||||
by (simp add: sep_mark2_def sep_conj_ac)
|
||||
by (rule sep_conj_left_com)
|
||||
|
||||
lemma sep_mark2_left2:
|
||||
"(P \<and>\<^sup>* sep_mark2 Q) = (sep_mark2 Q \<and>\<^sup>* P)"
|
||||
by (simp add: sep_mark2_def sep_conj_ac)
|
||||
by (rule sep_conj_com)
|
||||
|
||||
ML {*
|
||||
|
||||
(* Replace all occurences of an underscore that does not have an alphanumeric
|
||||
(* Replace all occurrences of an underscore that does not have an alphanumeric
|
||||
on either side of it *)
|
||||
local
|
||||
val dummy_char = #" ";
|
||||
fun get_next (x::xs) = x
|
||||
fun get_next (x::_) = x
|
||||
| get_next [] = dummy_char;
|
||||
fun nth_id n = "?SEPTAC"^(Int.toString n);
|
||||
fun nth_id n = "SEPTAC"^(Int.toString n);
|
||||
|
||||
fun ok_char c = not (Char.isAlphaNum c);
|
||||
|
||||
|
|
@ -171,12 +169,15 @@ local
|
|||
(ok_char prev) andalso (cur = #"_") andalso (ok_char last);
|
||||
|
||||
fun replace_usc n prev_char (x::xs) =
|
||||
let val (xs', ys) = replace_usc (n+1) x xs
|
||||
in
|
||||
if can_replace (prev_char,x,get_next xs)
|
||||
then (nth_id n)::(replace_usc (n+1) x xs)
|
||||
else (String.str x)::(replace_usc (n+1) x xs)
|
||||
| replace_usc _ _ [] = []
|
||||
then (nth_id n::xs', nth_id n::ys)
|
||||
else (String.str x::xs', ys)
|
||||
end
|
||||
| replace_usc _ _ [] = ([],[])
|
||||
in
|
||||
val rusc = String.concat o replace_usc 0 dummy_char o String.explode
|
||||
val rusc = apfst String.concat o replace_usc 0 dummy_char o String.explode
|
||||
end;
|
||||
|
||||
(* some tests *)
|
||||
|
|
@ -188,19 +189,25 @@ rusc "_ O_o _"
|
|||
|
||||
ML{*
|
||||
|
||||
fun sep_select_tacs s ctxt = [
|
||||
fun sep_select_tacs s ctxt =
|
||||
let val (str, vars) = rusc s
|
||||
val subst = [((Lexicon.read_indexname "P", Position.none), str)]
|
||||
val fixes = map (fn v => (Binding.name v, NONE, Mixfix.NoSyn)) vars
|
||||
in
|
||||
[
|
||||
TRY (simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm sep_conj_assoc}]) 1),
|
||||
resolve_tac [@{thm sep_markI}] 1,
|
||||
REPEAT (res_inst_tac ctxt [(Lexicon.read_indexname "P",rusc s)] @{thm sep_mark_match} 1 ORELSE
|
||||
res_inst_tac ctxt [(Lexicon.read_indexname "P",rusc s)] @{thm sep_mark_match2} 1 ORELSE
|
||||
resolve_tac [@{thm sep_mark_mismatch}] 1 ORELSE
|
||||
resolve_tac [@{thm sep_mark_mismatch2}] 1),
|
||||
resolve_tac ctxt [@{thm sep_markI}] 1,
|
||||
REPEAT (Rule_Insts.res_inst_tac ctxt subst fixes @{thm sep_mark_match} 1 ORELSE
|
||||
(Rule_Insts.res_inst_tac ctxt subst fixes @{thm sep_mark_match2} 1 ORELSE
|
||||
resolve_tac ctxt [@{thm sep_mark_mismatch}] 1 ORELSE
|
||||
resolve_tac ctxt [@{thm sep_mark_mismatch2}] 1)),
|
||||
TRY (simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm sep_conj_assoc}]) 1),
|
||||
resolve_tac [@{thm sep_emp_rem}] 1,
|
||||
resolve_tac ctxt [@{thm sep_emp_rem}] 1,
|
||||
TRY (simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm sep_mark2_left},
|
||||
@{thm sep_mark2_left2}]) 1),
|
||||
TRY (simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm sep_mark2_id}]) 1)
|
||||
]
|
||||
end
|
||||
|
||||
fun sep_select_tac s ctxt = SELECT_GOAL (EVERY (sep_select_tacs s ctxt))
|
||||
|
||||
|
|
@ -213,8 +220,6 @@ method_setup sep_select_tac =
|
|||
{* lift_parser Args.name >> (fn s => Method.SIMPLE_METHOD' o sep_select_tac s) *}
|
||||
"takes a target conjunct in the goal and reorders it to the front"
|
||||
|
||||
(* Method.goal_args Args.name *)
|
||||
|
||||
lemma
|
||||
"\<And>R x f n. ((P::heap_assert) \<and>\<^sup>* fac x n \<and>\<^sup>* R (f x)) s"
|
||||
apply(sep_select_tac "fac _ _")
|
||||
|
|
@ -259,7 +264,7 @@ ML {*
|
|||
fun destruct bs (Bound n) = Free (List.nth (bs,n))
|
||||
| destruct bs (Abs (s,ty,t)) = destruct ((s,ty)::bs) t
|
||||
| destruct bs (l$r) = destruct bs l $ destruct bs r
|
||||
| destruct bs x = x
|
||||
| destruct _ x = x
|
||||
|
||||
fun schems (Abs (_,_,t)) = schems t
|
||||
| schems (l$r) = schems l + schems r
|
||||
|
|
@ -272,7 +277,7 @@ fun hrs_mem_update (Const (@{const_name "HeapRawState.hrs_mem_update"},_)$_$s) =
|
|||
fun hrs_htd_update (Const (@{const_name "HeapRawState.hrs_htd_update"},_)$_$s) = SOME s
|
||||
| hrs_htd_update _ = NONE
|
||||
|
||||
fun lift_state_arg thy nc (Const (@{const_name "TypHeap.lift_state"},_)$s) = SOME s
|
||||
fun lift_state_arg _ _ (Const (@{const_name "TypHeap.lift_state"},_)$s) = SOME s
|
||||
| lift_state_arg thy nc (l$r) =
|
||||
(case lift_state_arg thy nc r of
|
||||
SOME s => if nc orelse hrs_mem_update s <> NONE orelse
|
||||
|
|
@ -281,26 +286,26 @@ fun lift_state_arg thy nc (Const (@{const_name "TypHeap.lift_state"},_)$s) = SOM
|
|||
| NONE => lift_state_arg thy nc l)
|
||||
| lift_state_arg thy nc (Abs (_,_,t)) =
|
||||
lift_state_arg thy nc t
|
||||
| lift_state_arg thy nc s =
|
||||
| lift_state_arg _ _ _ =
|
||||
NONE (*error (Sign.string_of_term thy s)*)
|
||||
|
||||
fun term_of_thm thm = term_of (cprop_of thm)
|
||||
fun term_of_thm thm = Thm.term_of (Thm.cprop_of thm)
|
||||
|
||||
fun lift_tac ctxt s old_schems =
|
||||
res_inst_tac ctxt [(Lexicon.read_indexname "s",s)] @{thm sep_map_lift_wp_hrs} 1 THEN
|
||||
Rule_Insts.res_inst_tac ctxt [((Lexicon.read_indexname "s",Position.none),s)] [] @{thm sep_map_lift_wp_hrs} 1 THEN
|
||||
(fn thm => if schems (term_of_thm thm) = old_schems then all_tac thm
|
||||
else no_tac thm)
|
||||
|
||||
fun heap_update_tac ctxt s =
|
||||
res_inst_tac ctxt [(Lexicon.read_indexname "s",s)] @{thm sep_heap_update'_hrs} 1
|
||||
Rule_Insts.res_inst_tac ctxt [((Lexicon.read_indexname "s",Position.none),s)] [] @{thm sep_heap_update'_hrs} 1
|
||||
|
||||
fun ptr_retyp_tac ctxt s =
|
||||
res_inst_tac ctxt [(Lexicon.read_indexname "s",s)] @{thm ptr_retyp_sep_cut'_wp_hrs} 1
|
||||
Rule_Insts.res_inst_tac ctxt [((Lexicon.read_indexname "s",Position.none),s)] [] @{thm ptr_retyp_sep_cut'_wp_hrs} 1
|
||||
|
||||
fun sep_wp_step_tac' ctxt lift_only s old_schems = let
|
||||
fun prt s = (
|
||||
case s of
|
||||
Free (a, b) => a
|
||||
Free (a, _) => a
|
||||
| _ => raise TERM ("Not a free variable",[s]))
|
||||
val state = prt s
|
||||
val step = case hrs_mem_update s of
|
||||
|
|
|
|||
|
|
@ -124,6 +124,7 @@ apply(auto simp: lift_state_def split: s_heap_index.splits option.splits)
|
|||
apply(drule s_footprintD)
|
||||
apply(drule intvlD, clarsimp simp: size_of_def)
|
||||
apply(frule s_footprintD2)
|
||||
apply(rename_tac nat)
|
||||
apply(drule s_footprintD)
|
||||
apply(drule intvlD, clarsimp)
|
||||
apply(drule_tac x=k in spec)
|
||||
|
|
@ -293,7 +294,7 @@ lemma sep_map_any_singleton:
|
|||
|
||||
lemma proj_h_heap_merge:
|
||||
"proj_h (s ++ t) = (\<lambda>x. if (x,SIndexVal) \<in> dom t then proj_h t x else proj_h s x)"
|
||||
by (force simp: proj_h_def intro: ext split: option.splits)
|
||||
by (force simp: proj_h_def split: option.splits)
|
||||
|
||||
lemma s_valid_heap_merge_right:
|
||||
"s\<^sub>1,g \<Turnstile>\<^sub>s p \<Longrightarrow> s\<^sub>0 ++ s\<^sub>1,g \<Turnstile>\<^sub>s p"
|
||||
|
|
@ -441,11 +442,11 @@ qed
|
|||
|
||||
lemma sep_conj_com:
|
||||
"(P \<and>\<^sup>* Q) = (Q \<and>\<^sup>* P)"
|
||||
by (rule ext) (auto simp: map_ac_simps map_disj_com sep_conjI dest!: sep_conjD)
|
||||
by (rule ext) (auto simp: map_ac_simps sep_conjI dest!: sep_conjD)
|
||||
|
||||
lemma sep_conj_false_right [simp]:
|
||||
"(P \<and>\<^sup>* sep_false) = sep_false"
|
||||
by (force dest: sep_conjD intro!: ext)
|
||||
by (force dest: sep_conjD)
|
||||
|
||||
lemma sep_conj_false_left [simp]:
|
||||
"(sep_false \<and>\<^sup>* P) = sep_false"
|
||||
|
|
@ -535,11 +536,11 @@ lemma sep_conj_conj:
|
|||
|
||||
lemma sep_conj_exists1:
|
||||
"((\<lambda>s. \<exists>x. P x s) \<and>\<^sup>* Q) = (\<lambda>s. (\<exists>x. (P x \<and>\<^sup>* Q) s))"
|
||||
by (force intro: sep_conjI intro!: ext dest: sep_conjD)
|
||||
by (force intro: sep_conjI dest: sep_conjD)
|
||||
|
||||
lemma sep_conj_exists2:
|
||||
"(P \<and>\<^sup>* (\<lambda>s. \<exists>x. Q x s)) = (\<lambda>s. (\<exists>x. (P \<and>\<^sup>* Q x) s))"
|
||||
by (force intro: sep_conjI intro!: ext dest: sep_conjD)
|
||||
by (force intro: sep_conjI dest: sep_conjD)
|
||||
|
||||
lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2
|
||||
|
||||
|
|
@ -583,7 +584,8 @@ lemma sep_implD:
|
|||
|
||||
lemma sep_emp_sep_impl [simp]:
|
||||
"(\<box> \<longrightarrow>\<^sup>* P) = P"
|
||||
apply(auto simp: sep_impl_def intro!: ext)
|
||||
apply(rule ext)
|
||||
apply(auto simp: sep_impl_def)
|
||||
apply(drule_tac x=empty in spec)
|
||||
apply auto
|
||||
apply(drule sep_empD)
|
||||
|
|
@ -592,11 +594,11 @@ done
|
|||
|
||||
lemma sep_impl_sep_true [simp]:
|
||||
"(P \<longrightarrow>\<^sup>* sep_true) = sep_true"
|
||||
by (force intro: sep_implI intro!: ext)
|
||||
by (force intro: sep_implI)
|
||||
|
||||
lemma sep_impl_sep_false [simp]:
|
||||
"(sep_false \<longrightarrow>\<^sup>* P) = sep_true"
|
||||
by (force intro: sep_implI intro!: ext)
|
||||
by (force intro: sep_implI)
|
||||
|
||||
lemma sep_impl_sep_true_P:
|
||||
"(sep_true \<longrightarrow>\<^sup>* P) s \<Longrightarrow> P s"
|
||||
|
|
@ -604,7 +606,7 @@ lemma sep_impl_sep_true_P:
|
|||
|
||||
lemma sep_impl_sep_true_false [simp]:
|
||||
"(sep_true \<longrightarrow>\<^sup>* sep_false) = sep_false"
|
||||
by (force intro!: ext dest: sep_impl_sep_true_P)
|
||||
by (force dest: sep_impl_sep_true_P)
|
||||
|
||||
lemma sep_impl_impl:
|
||||
"(P \<longrightarrow>\<^sup>* Q \<longrightarrow>\<^sup>* R) = (P \<and>\<^sup>* Q \<longrightarrow>\<^sup>* R)"
|
||||
|
|
@ -712,14 +714,14 @@ proof cases
|
|||
with disj show ?x
|
||||
by (clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
|
||||
(rename_tac s\<^sub>0' s\<^sub>1', rule_tac s\<^sub>1="s\<^sub>1'" and s\<^sub>0="s\<^sub>0' ++ s\<^sub>1" in sep_conjI,
|
||||
auto simp: map_add_disj map_ac_simps)
|
||||
auto simp: map_ac_simps)
|
||||
next
|
||||
assume "\<not> (p \<hookrightarrow>\<^sub>g v) s\<^sub>0"
|
||||
with map'_v have "(p \<hookrightarrow>\<^sub>g v) s\<^sub>1" by simp
|
||||
with disj show ?x
|
||||
by (clarsimp simp: sep_map'_def sep_conj_ac dest!: sep_conjD)
|
||||
(rename_tac s\<^sub>0' s\<^sub>1', rule_tac s\<^sub>1="s\<^sub>1'" and s\<^sub>0="s\<^sub>0 ++ s\<^sub>0'" in sep_conjI,
|
||||
auto simp: map_add_disj map_ac_simps)
|
||||
auto simp: map_ac_simps)
|
||||
qed
|
||||
|
||||
lemma sep_conj_overlapD:
|
||||
|
|
@ -783,7 +785,7 @@ lemma pure_sep_fasle:
|
|||
|
||||
lemma pure_split:
|
||||
"pure P = (P = sep_true \<or> P = sep_false)"
|
||||
by (force simp: pure_def intro!: ext)
|
||||
by (force simp: pure_def)
|
||||
|
||||
lemma pure_sep_conj:
|
||||
"\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>\<^sup>* Q)"
|
||||
|
|
@ -947,7 +949,7 @@ lemma intuitionistic_sep_conj_sep_true_P:
|
|||
|
||||
lemma intuitionistic_sep_conj_sep_true_simp:
|
||||
"intuitionistic P \<Longrightarrow> (P \<and>\<^sup>* sep_true) = P"
|
||||
by (fast intro: sep_conj_sep_true intro!: ext elim: intuitionistic_sep_conj_sep_true_P)
|
||||
by (fast intro: sep_conj_sep_true elim: intuitionistic_sep_conj_sep_true_P)
|
||||
|
||||
lemma intuitionistic_sep_impl_sep_true_P:
|
||||
"\<lbrakk> P s; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>\<^sup>* P) s"
|
||||
|
|
@ -955,8 +957,7 @@ lemma intuitionistic_sep_impl_sep_true_P:
|
|||
|
||||
lemma intuitionistic_sep_impl_sep_true_simp:
|
||||
"intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>\<^sup>* P) = P"
|
||||
by (fast intro!: ext
|
||||
elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)
|
||||
by (fast elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P)
|
||||
|
||||
(* Domain exact *)
|
||||
|
||||
|
|
@ -987,7 +988,7 @@ lemma dom_exact_sep_conj_conj:
|
|||
|
||||
lemma sep_conj_conj_simp:
|
||||
"dom_exact R \<Longrightarrow> ((\<lambda>s. P s \<and> Q s) \<and>\<^sup>* R) = (\<lambda>s. (P \<and>\<^sup>* R) s \<and> (Q \<and>\<^sup>* R) s)"
|
||||
by (fast intro!: sep_conj_conj dom_exact_sep_conj_conj ext)
|
||||
by (fast intro!: sep_conj_conj dom_exact_sep_conj_conj)
|
||||
|
||||
definition dom_eps :: "('a,'b) map_assert \<Rightarrow> 'a set" where
|
||||
"dom_eps P \<equiv> THE x. \<forall>s. P s \<longrightarrow> x = dom s"
|
||||
|
|
@ -1008,15 +1009,15 @@ lemma dom_eps:
|
|||
|
||||
lemma map_restrict_dom_exact:
|
||||
"\<lbrakk> dom_exact P; P s \<rbrakk> \<Longrightarrow> s |` dom_eps P = s"
|
||||
by (force simp: restrict_map_def None_com intro: dom_epsI ext)
|
||||
by (force simp: restrict_map_def None_com intro: dom_epsI)
|
||||
|
||||
lemma map_restrict_dom_exact2:
|
||||
"\<lbrakk> dom_exact P; P s\<^sub>0; s\<^sub>0 \<bottom> s\<^sub>1 \<rbrakk> \<Longrightarrow> (s\<^sub>1 |` dom_eps P) = empty"
|
||||
by (force simp: restrict_map_def map_disj_def intro: ext dest: dom_epsD)
|
||||
by (force simp: restrict_map_def map_disj_def dest: dom_epsD)
|
||||
|
||||
lemma map_restrict_dom_exact3:
|
||||
"\<lbrakk> dom_exact P; P s \<rbrakk> \<Longrightarrow> s |` (UNIV - dom_eps P) = empty"
|
||||
by (force simp: restrict_map_def intro: ext dest: dom_epsI)
|
||||
by (force simp: restrict_map_def dest: dom_epsI)
|
||||
|
||||
lemma map_add_restrict_dom_exact:
|
||||
"\<lbrakk> dom_exact P; s\<^sub>0 \<bottom> s\<^sub>1; P s\<^sub>1 \<rbrakk> \<Longrightarrow> (s\<^sub>1 ++ s\<^sub>0) |` (dom_eps P) = s\<^sub>1"
|
||||
|
|
@ -1047,7 +1048,7 @@ qed
|
|||
|
||||
lemma sep_conj_forall_simp:
|
||||
"dom_exact Q \<Longrightarrow> ((\<lambda>s. \<forall>x. P x s) \<and>\<^sup>* Q) = (\<lambda>s. \<forall>x. (P x \<and>\<^sup>* Q) s)"
|
||||
by (fast dest: sep_conj_forall dom_exact_sep_conj_forall intro!: ext)
|
||||
by (fast dest: sep_conj_forall dom_exact_sep_conj_forall)
|
||||
|
||||
lemma dom_exact_sep_map:
|
||||
"dom_exact (i \<mapsto>\<^sub>g x)"
|
||||
|
|
@ -1077,14 +1078,6 @@ lemma strictly_exact_dom_exact:
|
|||
"strictly_exact P \<Longrightarrow> dom_exact P"
|
||||
by (force simp: strictly_exact_def dom_exact_def)
|
||||
|
||||
(* Need a stronger def. such as (op =) (singleton p (v::'a)) s \<and> g p" for
|
||||
sep_map for this to hold
|
||||
|
||||
lemma strictly_exact_sep_map:
|
||||
"strictly_exact (x \<mapsto>\<^sub>g y)"
|
||||
by (clarsimp simp: strictly_exact_def sep_map_def lift_typ_heap_def split: option.splits)
|
||||
*)
|
||||
|
||||
lemma strictly_exact_sep_emp:
|
||||
"strictly_exact \<box>"
|
||||
by (force simp: strictly_exact_def dest: sep_empD)
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ lemma field_lookup_list_Some2 [rule_format]:
|
|||
field_lookup t fs (m + size_td_list ts)"
|
||||
apply(induct_tac ts)
|
||||
apply(clarsimp split: option.splits)
|
||||
apply(rename_tac a list)
|
||||
apply(clarsimp split: option.splits)
|
||||
apply auto
|
||||
apply(case_tac a, clarsimp split: split_if_asm)
|
||||
|
|
@ -36,6 +37,7 @@ lemma fnl_extend_ti:
|
|||
field_lookup (extend_ti tag t fn) (f # fs) m =
|
||||
(if f=fn then field_lookup t fs (size_td tag+m) else field_lookup tag (f # fs) m)"
|
||||
apply(case_tac tag, simp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, simp)
|
||||
apply auto
|
||||
apply(subst field_lookup_list_Some2)
|
||||
|
|
@ -206,6 +208,7 @@ lemma field_names_list:
|
|||
lemma field_names_extend_ti:
|
||||
"typ_name t \<noteq> typ_name ti \<Longrightarrow> field_names (extend_ti ti xi fn) t = field_names ti t @ (map (\<lambda>fs. fn#fs) (field_names xi t))"
|
||||
apply(cases ti, clarsimp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto)
|
||||
apply(simp add: field_names_list)
|
||||
done
|
||||
|
|
@ -252,19 +255,14 @@ lemma size_empty_typ_info [simp]:
|
|||
"size (empty_typ_info tn) = 2"
|
||||
by (simp add: empty_typ_info_def)
|
||||
|
||||
lemma list_size_append [simp]:
|
||||
"size_list (size_dt_pair size (size_list size_char)) (xs @ ys) =
|
||||
size_list (size_dt_pair size (size_list size_char)) xs +
|
||||
size_list (size_dt_pair size (size_list size_char)) ys"
|
||||
by (induct xs) auto
|
||||
|
||||
lemma list_size_char:
|
||||
"size_list size_char xs = length xs"
|
||||
by (induct xs) auto
|
||||
|
||||
lemma size_ti_extend_ti [simp]:
|
||||
"aggregate ti \<Longrightarrow> size (extend_ti ti t fn) = size ti + size t + 2 + size fn"
|
||||
apply(cases ti, auto)
|
||||
apply(cases ti, clarsimp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto simp: list_size_char)
|
||||
done
|
||||
|
||||
|
|
@ -393,7 +391,7 @@ apply(rule_tac s\<^sub>0="(s\<^sub>1 ++ s\<^sub>0) |` {(x,y) | x y. x \<in> {&(p
|
|||
apply(frule sep_map_dom_exc)
|
||||
apply(rotate_tac -1)
|
||||
apply(drule sym)
|
||||
apply(thin_tac "s = ?x")
|
||||
apply(thin_tac "s = x" for x)
|
||||
apply(clarsimp simp: restrict_map_disj_dom_empty map_ac_simps sep_conj_ac)
|
||||
apply(clarsimp simp: inv_footprint_def sep_conj_ac)
|
||||
apply(rule inter_sub)
|
||||
|
|
@ -569,16 +567,16 @@ lemma td_names_empty_typ_info [simp]:
|
|||
|
||||
lemma td_names_ptr [simp]:
|
||||
"td_names (typ_info_t TYPE(('a :: c_type) ptr)) = {typ_name_itself TYPE('a) @ ''+ptr''}"
|
||||
by (simp add: typ_info_ptr pad_typ_name_def)
|
||||
by (simp add: pad_typ_name_def)
|
||||
|
||||
lemma td_names_word8 [simp]:
|
||||
fixes x :: "byte itself"
|
||||
shows "td_names (typ_info_t x) = {''word00010''}"
|
||||
by (simp add:typ_info_word pad_typ_name_def nat_to_bin_string.simps)
|
||||
by (simp add: pad_typ_name_def nat_to_bin_string.simps)
|
||||
|
||||
lemma td_names_word32 [simp]:
|
||||
"td_names (typ_info_t TYPE(32 word)) = {''word0000010''}"
|
||||
by (simp add: typ_info_word pad_typ_name_def nat_to_bin_string.simps)
|
||||
by (simp add: pad_typ_name_def nat_to_bin_string.simps)
|
||||
|
||||
lemma td_names_export_uinfo [simp]:
|
||||
"td_names (export_uinfo td) = td_names td"
|
||||
|
|
@ -689,7 +687,6 @@ lemma typ_name_array_tag_n:
|
|||
lemma typ_name_array [simp]:
|
||||
"typ_name (typ_info_t TYPE('a::c_type['b :: finite])) =
|
||||
typ_name (typ_info_t TYPE('a)) @ ''_array_'' @ nat_to_bin_string (card (UNIV :: 'b set))"
|
||||
apply (simp add: typ_info_array array_tag_def typ_name_array_tag_n)
|
||||
done
|
||||
|
||||
by (simp add: typ_info_array array_tag_def typ_name_array_tag_n)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -214,12 +214,12 @@ where
|
|||
|
||||
|
||||
definition
|
||||
sub_typ :: "'a::c_type itself \<Rightarrow> 'b::c_type itself \<Rightarrow> bool" ("_ \<le>\<^sub>\<tau> _")
|
||||
sub_typ :: "'a::c_type itself \<Rightarrow> 'b::c_type itself \<Rightarrow> bool" ("_ \<le>\<^sub>\<tau> _" [51, 51] 50)
|
||||
where
|
||||
"s \<le>\<^sub>\<tau> t \<equiv> typ_uinfo_t s \<le> typ_uinfo_t t"
|
||||
|
||||
definition
|
||||
sub_typ_proper :: "'a::c_type itself \<Rightarrow> 'b::c_type itself \<Rightarrow> bool" ("_ <\<^sub>\<tau> _")
|
||||
sub_typ_proper :: "'a::c_type itself \<Rightarrow> 'b::c_type itself \<Rightarrow> bool" ("_ <\<^sub>\<tau> _" [51, 51] 50)
|
||||
where
|
||||
"s <\<^sub>\<tau> t \<equiv> typ_uinfo_t s < typ_uinfo_t t"
|
||||
|
||||
|
|
@ -308,7 +308,7 @@ text {* ---- *}
|
|||
|
||||
lemma wf_heap_val_SIndexVal_STyp_simp [simp]:
|
||||
"wf_heap_val s \<Longrightarrow> s (x,SIndexVal) \<noteq> Some (STyp t)"
|
||||
apply(auto simp: wf_heap_val_def wf_heap_val_def)
|
||||
apply(clarsimp simp: wf_heap_val_def)
|
||||
apply(drule_tac x=x in spec)
|
||||
apply clarsimp
|
||||
apply(case_tac t, simp)
|
||||
|
|
@ -520,7 +520,7 @@ lemma s_valid_g:
|
|||
lemma lift_typ_heap_if:
|
||||
"lift_typ_heap g s = (\<lambda>(p::'a::c_type ptr). if s,g \<Turnstile>\<^sub>s p then Some (from_bytes
|
||||
(heap_list_s s (size_of TYPE('a)) (ptr_val p))) else None)"
|
||||
by (force simp: lift_typ_heap_def intro: ext)
|
||||
by (force simp: lift_typ_heap_def)
|
||||
|
||||
lemma lift_typ_heap_s_valid:
|
||||
"lift_typ_heap g s p = Some x \<Longrightarrow> s,g \<Turnstile>\<^sub>s p"
|
||||
|
|
@ -566,9 +566,9 @@ lemma fun2list_nth [simp]:
|
|||
|
||||
lemma proj_d_lift_state:
|
||||
"proj_d (lift_state (h,d)) = d"
|
||||
apply(auto simp: proj_d_def Let_def intro!: ext split: option.splits)
|
||||
apply(rule ext)
|
||||
apply(case_tac "d x")
|
||||
apply(auto simp: lift_state_def split: option.splits)
|
||||
apply(auto simp: proj_d_def lift_state_def Let_def split: option.splits)
|
||||
done
|
||||
|
||||
lemma lift_state_proj [simp]:
|
||||
|
|
@ -709,7 +709,7 @@ lemma lift_t_if:
|
|||
"lift_t g (h,d) = (\<lambda>p. if d,g \<Turnstile>\<^sub>t p then Some (h_val h (p::'a::c_type ptr)) else
|
||||
None)"
|
||||
by (force simp: lift_t_def lift_typ_heap_if h_t_s_valid h_val_def
|
||||
heap_list_s_heap_list h_t_valid_taut intro: ext)
|
||||
heap_list_s_heap_list h_t_valid_taut)
|
||||
|
||||
lemma lift_lift_t:
|
||||
"d,g \<Turnstile>\<^sub>t (p::'a::c_type ptr) \<Longrightarrow> lift h p = the (lift_t g (h,d) p)"
|
||||
|
|
@ -730,7 +730,7 @@ next
|
|||
case (Cons x xs)
|
||||
have "heap_update_list (p + of_nat k) (x # xs) h p =
|
||||
heap_update_list (p + of_nat (k + 1)) xs (h(p + of_nat k := x)) p"
|
||||
by (simp add: add.assoc of_nat_add ac_simps)
|
||||
by (simp add: ac_simps)
|
||||
also have "\<dots> = (h(p + of_nat k := x)) p"
|
||||
proof -
|
||||
from Cons have "k + 1 \<le> addr_card - length xs" by simp
|
||||
|
|
@ -852,7 +852,7 @@ apply(auto simp: ladder_set_def)
|
|||
apply(drule_tac x=m in spec)
|
||||
apply(drule_tac x=0 in spec)
|
||||
apply force
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x="m + size_td (dt_fst dt_pair)" in spec)
|
||||
apply(drule_tac x="n - size_td (dt_fst dt_pair)" in spec)
|
||||
apply(case_tac dt_pair)
|
||||
|
|
@ -981,7 +981,8 @@ apply(induct t and st and xs and x)
|
|||
apply auto[4]
|
||||
apply clarsimp
|
||||
apply(case_tac dt_pair, clarsimp)
|
||||
apply(thin_tac "All ?P")
|
||||
apply(rename_tac a)
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x=s in spec)
|
||||
apply(drule_tac x="k - size_td a" in spec)
|
||||
apply clarsimp
|
||||
|
|
@ -1023,9 +1024,7 @@ lemma typ_slice_0_True':
|
|||
"\<forall>x. x \<in> set (typ_slice_struct st 0) \<longrightarrow> snd x = True"
|
||||
"\<forall>x. x \<in> set (typ_slice_list xs 0) \<longrightarrow> snd x = True"
|
||||
"\<forall>x. x \<in> set (typ_slice_pair y 0) \<longrightarrow> snd x = True"
|
||||
apply(induct t and st and xs and y)
|
||||
apply auto
|
||||
done
|
||||
by (induct t and st and xs and y) auto
|
||||
|
||||
lemma typ_slice_0_True:
|
||||
"x \<in> set (typ_slice_t t 0) \<Longrightarrow> snd x = True"
|
||||
|
|
@ -1033,9 +1032,7 @@ lemma typ_slice_0_True:
|
|||
|
||||
lemma typ_slice_False_self:
|
||||
"k \<noteq> 0 \<Longrightarrow> (t,False) \<in> set (typ_slice_t t k)"
|
||||
apply(case_tac t)
|
||||
apply simp
|
||||
done
|
||||
by (cases t) simp
|
||||
|
||||
lemma tag_prefix_True:
|
||||
"typ_slice_t s k \<le> typ_slice_t t 0 \<Longrightarrow> k = 0"
|
||||
|
|
@ -1163,12 +1160,9 @@ lemma sub_typ_proper_not_same [simp]:
|
|||
|
||||
lemma sub_typ_proper_not_simple [simp]:
|
||||
"\<not> TYPE('a::c_type) <\<^sub>\<tau> TYPE('b::simple_mem_type)"
|
||||
apply(simp add: sub_typ_proper_def)
|
||||
apply(case_tac "typ_uinfo_t TYPE('b)")
|
||||
apply simp
|
||||
apply(case_tac typ_struct)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply(cases "typ_uinfo_t TYPE('b)")
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, auto simp: sub_typ_proper_def)
|
||||
done
|
||||
|
||||
lemma field_of_sub:
|
||||
|
|
@ -1206,6 +1200,7 @@ apply(drule (1) map_prefix_same_cases[where xs="typ_slice_t (typ_uinfo_t TYPE('a
|
|||
apply(erule disjE)
|
||||
apply(drule typ_slice_sub)
|
||||
apply(case_tac "typ_info_t TYPE('b)")
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac "typ_struct")
|
||||
apply clarsimp
|
||||
apply(simp add: typ_tag_le_def)
|
||||
|
|
@ -1214,6 +1209,7 @@ apply(erule disjE)
|
|||
apply simp
|
||||
apply(drule typ_slice_sub)
|
||||
apply(case_tac "typ_info_t TYPE('a)")
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac "typ_struct")
|
||||
apply clarsimp
|
||||
apply(simp add: typ_tag_le_def typ_uinfo_t_def)
|
||||
|
|
@ -1253,20 +1249,15 @@ lemma peer_typ_simple [simp]:
|
|||
apply(clarsimp simp: peer_typ_def tag_disj_def typ_tag_le_def typ_uinfo_t_def)
|
||||
apply(erule disjE)
|
||||
apply(case_tac "typ_info_t TYPE('b)", simp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, simp+)
|
||||
apply(case_tac "typ_info_t TYPE('a)", simp)
|
||||
apply(rename_tac typ_struct xs)
|
||||
apply(case_tac typ_struct, simp+)
|
||||
done
|
||||
|
||||
lemma peer_typ_nlt:
|
||||
"peer_typ TYPE('a::c_type) TYPE('b::c_type) \<Longrightarrow> \<not> TYPE('a) <\<^sub>\<tau> TYPE('b)"
|
||||
apply(clarsimp simp: peer_typ_def sub_typ_proper_def typ_uinfo_t_def)
|
||||
apply(erule disjE)
|
||||
apply simp
|
||||
apply(clarsimp simp: tag_disj_def)
|
||||
apply(drule order_less_imp_le)
|
||||
apply simp
|
||||
done
|
||||
(* FIXME: remove *)
|
||||
lemmas peer_typ_nlt = peer_typD
|
||||
|
||||
lemma peer_typ_not_field_of:
|
||||
"\<lbrakk> peer_typ TYPE('a::c_type) TYPE('b::c_type); ptr_val p \<noteq> ptr_val q \<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -1303,13 +1294,14 @@ lemma heap_list_update_list [rule_format]:
|
|||
heap_list (heap_update_list p v h) n (p + of_nat x) = take n (drop x v)"
|
||||
apply(induct_tac v)
|
||||
apply simp
|
||||
apply auto
|
||||
apply(rename_tac a list)
|
||||
apply clarsimp
|
||||
apply(case_tac x)
|
||||
apply clarsimp
|
||||
apply(case_tac n)
|
||||
apply clarsimp
|
||||
apply clarsimp
|
||||
apply rule
|
||||
apply (rule conjI)
|
||||
apply(subgoal_tac "heap_update_list (p + of_nat 1) list (h(p := a)) p = a")
|
||||
apply simp
|
||||
apply(subst heap_update_list_same)
|
||||
|
|
@ -1350,6 +1342,7 @@ apply(induct t and st and ts and x)
|
|||
apply simp
|
||||
apply(erule notE)
|
||||
apply(case_tac dt_pair, clarsimp)
|
||||
apply(rename_tac a)
|
||||
apply(subgoal_tac "size_td s + n \<le> size_td a")
|
||||
apply simp
|
||||
apply(drule_tac td_set_offset_size_m)
|
||||
|
|
@ -1357,6 +1350,7 @@ apply(induct t and st and ts and x)
|
|||
apply(rotate_tac)
|
||||
apply(drule_tac x=s in spec)
|
||||
apply(case_tac dt_pair, clarsimp)
|
||||
apply(rename_tac a)
|
||||
apply(drule_tac x="m + size_td a" in spec)
|
||||
apply(drule_tac x="n - size_td a" in spec)
|
||||
apply(drule_tac x="k" in spec)
|
||||
|
|
@ -1768,7 +1762,7 @@ apply(induct t and st and ts and x)
|
|||
apply(drule_tac x=m in spec)
|
||||
apply(drule_tac x=f in spec)
|
||||
apply clarsimp
|
||||
apply(thin_tac "All ?P")
|
||||
apply(thin_tac "All P" for P)
|
||||
apply(drule_tac x="m + size_td (dt_fst dt_pair)" in spec)
|
||||
apply(drule_tac x=f in spec)
|
||||
apply clarsimp
|
||||
|
|
@ -1778,7 +1772,8 @@ done
|
|||
|
||||
lemma dt_snd_field_names_list_simp [simp]:
|
||||
"\<forall>f fs s. f \<notin> dt_snd ` set xs \<longrightarrow> \<not> f#fs \<in> set (field_names_list xs s)"
|
||||
apply(induct_tac xs, auto)
|
||||
apply(induct_tac xs, clarsimp)
|
||||
apply(rename_tac a list)
|
||||
apply(case_tac a, auto)
|
||||
done
|
||||
|
||||
|
|
@ -1808,7 +1803,7 @@ lemma field_names_SomeD:
|
|||
by (simp add: field_names_Some)
|
||||
|
||||
lemma lift_t_sub_field_update' [rule_format]:
|
||||
"\<lbrakk> d,g' \<Turnstile>\<^sub>t p; \<not> (TYPE('a) <\<^sub>\<tau> TYPE('b)) (*; guard_mono g' p g*) \<rbrakk> \<Longrightarrow> fs_consistent fs TYPE('a) TYPE('b) \<longrightarrow>
|
||||
"\<lbrakk> d,g' \<Turnstile>\<^sub>t p; \<not> (TYPE('a) <\<^sub>\<tau> TYPE('b)) \<rbrakk> \<Longrightarrow> fs_consistent fs TYPE('a) TYPE('b) \<longrightarrow>
|
||||
(\<forall>K. K = UNIV - (((field_offset_footprint p (field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b))))) - (field_offset_footprint p fs)) \<longrightarrow>
|
||||
lift_t g (heap_update p (v::'a::mem_type) h,d) |` K =
|
||||
sub_field_update_t fs p v ((lift_t g (h,d))::'b::mem_type typ_heap) |` K)"
|
||||
|
|
@ -1831,11 +1826,12 @@ apply(induct_tac fs)
|
|||
apply clarsimp
|
||||
apply(drule field_names_SomeD3)
|
||||
apply simp
|
||||
apply(rename_tac a list)
|
||||
apply clarify
|
||||
apply clarsimp
|
||||
apply(erule impE)
|
||||
apply(clarsimp simp: fs_consistent_def)
|
||||
apply rule
|
||||
apply (rule conjI)
|
||||
prefer 2
|
||||
apply clarsimp
|
||||
apply(rule ccontr, clarsimp)
|
||||
|
|
@ -2025,7 +2021,7 @@ done
|
|||
lemma uvt1':
|
||||
"update_value_t (f#fs) v (w::'b) x = (if x=field_offset TYPE('b) f then
|
||||
update_ti_t (field_typ TYPE('b) f) (to_bytes_p (v::'a::c_type)) (w::'b::c_type) else update_value_t fs v w x)"
|
||||
by (simp add: uvt1)
|
||||
by simp
|
||||
|
||||
lemma field_typ_self [simp]:
|
||||
"field_typ TYPE('a) [] = typ_info_t TYPE('a::c_type)"
|
||||
|
|
@ -2130,7 +2126,7 @@ apply(erule disjE)
|
|||
apply(rule max_size)
|
||||
apply(rule sz_nzero)
|
||||
apply(subst len_of_addr_card)
|
||||
apply(thin_tac "?P \<in> ?Q")
|
||||
apply(thin_tac "x \<in> S" for x S)
|
||||
apply(simp add: field_of_t_def field_of_def)
|
||||
apply(drule td_set_offset_size)
|
||||
apply(simp add: size_of_def)
|
||||
|
|
@ -2190,23 +2186,11 @@ apply(subst drop_heap_list_le)
|
|||
apply simp
|
||||
done
|
||||
|
||||
lemma update_field_update' [rule_format]:
|
||||
"n \<in> (\<lambda>f. field_offset TYPE('b) f) ` set fs \<longrightarrow>
|
||||
lemma update_field_update':
|
||||
"n \<in> (\<lambda>f. field_offset TYPE('b) f) ` set fs \<Longrightarrow>
|
||||
(\<exists>f. update_value_t fs (v::'a::c_type) (v'::'b::c_type) n =
|
||||
field_update (field_desc (field_typ TYPE('b) f)) (to_bytes_p v) v' \<and> f \<in> set fs \<and> n = field_offset TYPE('b) f)"
|
||||
apply(induct_tac fs)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply(rule, clarsimp)
|
||||
apply rule
|
||||
apply(rule_tac x=a in exI)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply(rule_tac x=a in exI)
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply force
|
||||
done
|
||||
by (induct fs) auto
|
||||
|
||||
lemma update_field_update:
|
||||
"field_of_t (p::'a ptr) (x::'b ptr) \<Longrightarrow>
|
||||
|
|
@ -2279,7 +2263,7 @@ apply(frule_tac bs="access_ti t v bs" in wf_fd_norm_tuD)
|
|||
apply assumption
|
||||
apply simp+
|
||||
apply(clarsimp simp: access_ti\<^sub>0_def)
|
||||
apply(thin_tac "norm_tu ?X ?Y = ?Z")+
|
||||
apply(thin_tac "norm_tu X Y = Z" for X Y Z)+
|
||||
apply(subst (asm) fa_fu_v [where w=v])
|
||||
apply fast
|
||||
apply(subst length_fa_ti)
|
||||
|
|
@ -3000,7 +2984,7 @@ proof -
|
|||
apply(auto simp: field_lvalue_def split: option.splits)
|
||||
apply(frule_tac v=v and v'=v' in update_field_update)
|
||||
apply clarsimp
|
||||
apply(thin_tac "?P = update_ti_t ?x ?y ?z")
|
||||
apply(thin_tac "P = update_ti_t x y z" for P x y z)
|
||||
apply(clarsimp simp: field_of_t_def field_of_def typ_uinfo_t_def)
|
||||
apply(frule_tac m=0 in field_names_SomeD2)
|
||||
apply simp
|
||||
|
|
|
|||
|
|
@ -49,7 +49,7 @@ begin
|
|||
|
||||
instance
|
||||
apply intro_classes
|
||||
apply (auto simp: size_of_def typ_info_unit align_of_def align_field_def addr_card
|
||||
apply (auto simp: size_of_def align_of_def align_field_def addr_card
|
||||
wf_lf_def fd_cons_desc_def
|
||||
fd_cons_double_update_def fd_cons_update_access_def
|
||||
fd_cons_access_update_def fd_cons_length_def)
|
||||
|
|
@ -366,7 +366,7 @@ begin
|
|||
instance
|
||||
apply (intro_classes)
|
||||
apply (auto simp: to_bytes_def from_bytes_def
|
||||
length_word_rsplit_exp_size' word_size align_of_ptr
|
||||
length_word_rsplit_exp_size' word_size
|
||||
word_rcat_rsplit size_of_def addr_card
|
||||
typ_info_ptr fd_cons_double_update_def
|
||||
fd_cons_update_access_def fd_cons_access_update_def
|
||||
|
|
@ -423,7 +423,7 @@ lemma ptr_aligned_coerceI:
|
|||
lemma lift_ptr_ptr [simp]:
|
||||
"\<And>p::'a::mem_type ptr ptr.
|
||||
lift h (ptr_coerce p) = ptr_val (lift h p)"
|
||||
by (simp add: lift_def h_val_def from_bytes_def from_bytes_def
|
||||
by (simp add: lift_def h_val_def from_bytes_def
|
||||
typ_info_word word_tag_def typ_info_ptr)
|
||||
|
||||
lemmas Vanilla32_tags [simp] =
|
||||
|
|
|
|||
Loading…
Reference in New Issue