Theory AutoCorres2.LemmaBucket_C
theory LemmaBucket_C
imports
More_Lib
WordSetup
TypHeapLib
ArrayAssertion
begin
declare word_neq_0_conv [simp del]
lemma Ptr_not_null_pointer_not_zero: "(Ptr p ≠ NULL)=(p≠0)"
by simp
lemma hrs_mem_f: "f (hrs_mem s) = hrs_mem (hrs_mem_update f s)"
apply (cases s)
apply (clarsimp simp: hrs_mem_def hrs_mem_update_def)
done
lemma hrs_mem_heap_update:
"heap_update p v (hrs_mem s) = hrs_mem (hrs_mem_update (heap_update p v) s)"
apply (rule hrs_mem_f)
done
lemma surj_Ptr [simp]:
"surj Ptr"
by (rule surjI [where f = ptr_val], simp)
lemma inj_Ptr [simp]:
"inj Ptr"
apply (rule injI)
apply simp
done
lemma bij_Ptr :
"bij Ptr"
by (simp add: bijI)
lemma exec_Guard:
"(G ⊢ ⟨Guard Err S c, Normal s⟩ ⇒ s')
= (if s ∈ S then G ⊢ ⟨c, Normal s⟩ ⇒ s'
else s' = Fault Err)"
by (auto split: if_split elim!: exec_elim_cases intro: exec.intros)
lemma byte_ptr_guarded:"ptr_val (x::8 word ptr) ≠ 0 ⟹ c_guard x"
unfolding c_guard_def c_null_guard_def ptr_aligned_def
by (clarsimp simp: intvl_Suc)
lemma intvl_aligned_bottom_eq:
fixes p :: "'a::len word"
assumes al1: "is_aligned x n"
and al2: "is_aligned p bits"
and nb: "¬ n < bits"
and off: "off ≤ 2 ^ bits" "off ≠ 0"
shows "(x ∈ {p ..+ off}) = (x = p)"
proof (rule iffI)
assume "x = p"
thus "x ∈ {p ..+ off}" using off
by (simp add: intvl_self)
next
assume x_in_intvl: "x ∈ {p ..+ off}"
show "x = p"
proof cases
assume wb: "bits < len_of TYPE('a)"
from x_in_intvl obtain kp where xp: "x = p + of_nat kp" and kp: "kp < off"
by (clarsimp dest!: intvlD)
hence "is_aligned (p + of_nat kp) n" using al1 by simp
hence "2 ^ n dvd unat (p + of_nat kp)" unfolding is_aligned_def .
hence "2 ^ n dvd unat p + kp" using kp off wb
apply -
apply (subst (asm) iffD1 [OF unat_plus_simple])
apply (rule is_aligned_no_wrap' [OF al2])
apply (rule of_nat_power)
apply simp_all[2]
apply (subst (asm) unat_of_nat)
apply (subst (asm) mod_less)
apply (erule order_less_le_trans)
apply (erule order_trans)
apply simp
apply simp
done
moreover from al2 obtain q2 where pbits: "p = 2 ^ bits * of_nat q2"
and q2: "q2 < 2 ^ (len_of TYPE('a) - bits)"
by (rule is_alignedE)
moreover from nb obtain kn where nbits: "n = bits + kn"
by (clarsimp simp: linorder_not_less le_iff_add)
ultimately have "2 ^ bits dvd 2 ^ bits * q2 + kp"
apply (simp add: power_add)
apply (simp add: unat_mult_power_lem [OF q2])
apply (erule dvd_mult_left)
done
hence "2 ^ bits dvd kp" by (simp add: dvd_reduce_multiple)
with kp have "kp = 0"
apply -
apply (erule contrapos_pp)
apply (simp add: linorder_not_less)
apply (drule (1) dvd_imp_le)
apply (erule order_trans [OF off(1)])
done
thus ?thesis using xp by simp
next
assume wb: "¬ bits < len_of TYPE('a)"
with assms
show ?thesis by (simp add: is_aligned_mask mask_def power_overflow)
qed
qed
lemma intvl_mem_weaken: "x ∈ {p..+a - n} ⟹ x ∈ {p..+a}"
apply -
apply (drule intvlD)
apply clarsimp
apply (rule intvlI)
apply simp
done
lemma upto_intvl_eq:
fixes x :: "'a::len word"
assumes al: "is_aligned x n"
shows "{x..+2 ^ n} = {x .. x + 2 ^ n - 1}"
proof cases
assume "n < len_of TYPE('a)"
with assms show ?thesis
unfolding intvl_def
apply simp
apply standard
apply clarsimp
apply (subgoal_tac "of_nat k < (2 :: 'a word) ^ n")
apply (intro conjI)
apply (erule (1) is_aligned_no_wrap')
apply (subst p_assoc_help)
apply (rule word_plus_mono_right)
apply (simp add: word_less_sub_1)
apply (simp add: field_simps is_aligned_no_overflow)
apply (simp add: of_nat_power)
apply clarsimp
subgoal for xa
apply (rule exI[where x = "unat (xa - x)"])
apply clarsimp
apply (rule unat_less_power, assumption)
apply (subst word_less_sub_le [symmetric])
apply assumption
apply (rule word_diff_ls'(4))
apply (simp add: field_simps)
apply assumption
done
done
next
assume "¬ n < len_of TYPE('a)"
with assms show ?thesis
apply (simp add: is_aligned_mask mask_def power_overflow intvl_def)
apply (rule set_eqI)
apply clarsimp
by (metis (no_types, opaque_lifting) le_less_trans nat_power_less_imp_less not_le power_eq_0_iff
power_zero_numeral unat_lt2p word_unat.Rep_inverse)
qed
lemma upto_intvl_eq':
fixes x :: "'a :: len word"
shows "⟦ x ≤ x + (of_nat b - 1); b ≠ 0; b ≤ 2 ^ len_of TYPE('a)⟧ ⟹ {x..+b} = {x .. x + of_nat b - 1}"
unfolding intvl_def
supply unsigned_of_nat
apply standard
apply clarsimp
apply (subgoal_tac "of_nat k ≤ (of_nat (b - 1) :: 'a word)")
apply (intro conjI)
apply (erule word_random)
apply simp
apply (subst field_simps [symmetric], rule word_plus_mono_right)
apply simp
apply assumption
apply (subst More_Word.of_nat_mono_maybe_le [symmetric])
apply simp
apply simp
apply simp
apply clarsimp
subgoal for xa
apply (rule exI[where x = "unat (xa - x)"])
apply simp
apply (simp add: unat_sub)
apply (rule nat_diff_less)
apply (subst (asm) word_le_nat_alt, erule order_le_less_trans)
apply (subst add_diff_eq[symmetric], subst unat_plus_if')
apply (simp add: no_olen_add_nat)
apply (simp add: le_eq_less_or_eq)
apply (erule disjE)
apply (subst unat_minus_one)
apply (erule (1) of_nat_neq_0)
apply (simp add: unat_of_nat)
apply (erule ssubst, rule unat_lt2p)
apply (simp add: word_le_nat_alt)
done
done
lemma intvl_aligned_top:
fixes x :: "'a::len word"
assumes al1: "is_aligned x n"
and al2: "is_aligned p bits"
and nb: "n ≤ bits"
and offn: "off < 2 ^ n"
and wb: "bits < len_of TYPE('a)"
shows "(x ∈ {p ..+ 2 ^ bits - off}) = (x ∈ {p ..+ 2 ^ bits})"
proof (rule iffI)
assume "x ∈ {p..+2 ^ bits - off}"
thus "x ∈ {p..+2 ^ bits}" by (rule intvl_mem_weaken)
next
assume asm: "x ∈ {p..+2 ^ bits}"
show "x ∈ {p..+2 ^ bits - off}"
proof (cases "n = 0")
case True
with offn asm show ?thesis by simp
next
case False
from asm have "x ∈ {p .. p + 2 ^ bits - 1}"
by (simp add: upto_intvl_eq [OF al2])
then obtain q where xp: "x = p + of_nat (q * 2 ^ n)" and qb: "q < 2 ^ (bits - n)" using False nb
by (fastforce dest!: is_aligned_diff[OF al1 al2 wb,simplified field_simps])
have "q * 2 ^ n < 2 ^ bits - off"
proof -
show ?thesis using offn qb nb
apply (simp add: less_diff_conv)
apply (erule (1) nat_add_offset_less)
apply arith
done
qed
with xp show ?thesis
apply -
apply (erule ssubst)
apply (erule intvlI)
done
qed
qed
lemma heap_update_list_update:
fixes v :: word8
shows "x ≠ y ⟹ heap_update_list s xs (hp(y := v)) x = heap_update_list s xs hp x"
apply (induct xs rule: rev_induct)
apply simp
apply (simp add: heap_update_list_append cong: if_cong)
done
lemma heap_update_list_append2:
"length xs + length ys < 2 ^ word_bits ⟹
heap_update_list s (xs @ ys) hp
= heap_update_list s xs (heap_update_list (s + of_nat (length xs)) ys hp)"
proof (induct xs arbitrary: hp s)
case Nil
show ?case by simp
next
case (Cons v' vs')
have "(1 :: addr) + of_nat (length vs') = of_nat (length (v' # vs'))"
by simp
also have "… ≠ 0" using Cons.prems
apply -
apply (rule of_nat_neq_0)
apply simp
apply (simp add: word_bits_conv)
done
finally have neq0: "(1 :: addr) + of_nat (length vs') ≠ 0" .
have "(1 :: addr) + of_nat (length vs') = of_nat (length (v' # vs'))"
by simp
also have "unat … + length ys < 2 ^ word_bits" using Cons.prems
apply (subst unat_of_nat)
apply (simp add: word_bits_conv)
done
finally have lt: "unat ((1 :: addr) + of_nat (length vs')) + length ys < 2 ^ word_bits" .
from Cons.prems have "length vs' + length ys < 2 ^ word_bits" by simp
thus ?case
apply simp
apply (subst Cons.hyps, assumption)
apply (rule arg_cong [where f = "heap_update_list (s + 1) vs'"])
apply (rule ext)
subgoal for x
apply (cases "x = s")
apply simp
apply (subst heap_update_nmem_same)
apply (subst add.assoc)
apply (rule intvl_nowrap[OF neq0 order_less_imp_le
[OF lt[unfolded word_bits_def]]])
apply simp
apply (clarsimp simp: heap_update_list_update field_simps)
done
done
qed
lemma heap_update_word8:
"heap_update p (v :: word8) hp = hp(ptr_val p := v)"
unfolding heap_update_def by (simp add: to_bytes_word8)
lemma index_foldr_update2:
"⟦ n ≤ i; i < CARD('b::finite) ⟧ ⟹ index (foldr (λn arr. Arrays.update arr n m) [0..<n] (x :: ('a,'b) array)) i = index x i"
apply (induct n arbitrary: x)
apply simp
apply simp
done
lemma index_foldr_update:
"⟦ i < n; n ≤ CARD('b::finite) ⟧ ⟹ index (foldr (λn arr. Arrays.update arr n m) [0..<n] (x :: ('a,'b) array)) i = m"
apply (induct n arbitrary: x)
apply simp
apply simp
apply (erule less_SucE)
apply simp
apply simp
apply (subst index_foldr_update2)
apply simp
apply simp
apply simp
done
lemma intvl_disjoint1:
fixes a :: "'a :: len word"
assumes abc: "a + of_nat b ≤ c"
and alb: "a ≤ a + of_nat b"
and cld: "c ≤ c + of_nat d"
and blt: "b < 2 ^ len_of TYPE('a)"
and dlt: "d < 2 ^ len_of TYPE('a)"
shows "{a..+b} ∩ {c..+d} = {}"
proof (rule disjointI, rule notI)
fix x y
assume x: "x ∈ {a..+b}" and y: "y ∈ {c..+d}" and xy: "x = y"
from x obtain kx where "x = a + of_nat kx" and kx: "kx < b"
by (clarsimp dest!: intvlD)
moreover from y obtain ky where "y = c + of_nat ky" and ky: "ky < d"
by (clarsimp dest!: intvlD)
ultimately have ac: "a + of_nat kx = c + of_nat ky" using xy by simp
have "of_nat kx < (of_nat b :: 'a word)" using blt kx
by (rule of_nat_mono_maybe)
hence "a + of_nat kx < a + of_nat b" using alb
by (rule word_plus_strict_mono_right)
also have "… ≤ c" by (rule abc)
also have "… ≤ c + of_nat ky" using cld dlt ky
by - (rule word_random [OF _ iffD1 [OF More_Word.of_nat_mono_maybe_le]], simp+ )
finally show False using ac by simp
qed
lemma intvl_disjoint2:
fixes a :: "'a :: len word"
assumes abc: "a + of_nat b ≤ c"
and alb: "a ≤ a + of_nat b"
and cld: "c ≤ c + of_nat d"
and blt: "b < 2 ^ len_of TYPE('a)"
and dlt: "d < 2 ^ len_of TYPE('a)"
shows "{c..+d} ∩ {a..+b} = {}"
using abc alb cld blt dlt
by (subst Int_commute, rule intvl_disjoint1)
lemma typ_slice_t_self:
"td ∈ fst ` set (typ_slice_t td m)"
apply (cases td)
apply (simp split: if_split)
done
lemma index_fold_update:
"⟦ distinct xs; set xs ⊆ {..< card (UNIV :: 'b set)}; n < card (UNIV :: 'b set) ⟧ ⟹
index (foldr (λn (arr :: 'a['b :: finite]). Arrays.update arr n (f n (index arr n))) xs v) n
= (if n ∈ set xs then f n (index v n) else index v n)"
apply (induct xs)
apply simp
subgoal for x xs by (cases "x = n", auto)
done
lemma hrs_mem_update_cong:
"⟦ ⋀x. f x = f' x ⟧ ⟹ hrs_mem_update f = hrs_mem_update f'"
by (simp add: hrs_mem_update_def)
lemma Guard_no_cong:
"⟦ A=A'; c=c' ⟧ ⟹ Guard A P c = Guard A' P c'"
by simp
lemma coerce_heap_update_to_heap_updates:
assumes n: "n = chunk * m" and len: "length xs = n"
shows "heap_update_list x xs
= (λs. foldl (λs n. heap_update_list (x + (of_nat n * of_nat chunk))
(take chunk (drop (n * chunk) xs)) s)
s [0 ..< m])"
using len[simplified n]
apply (induct m arbitrary: x xs)
apply (rule ext, simp)
apply (rule ext)
subgoal for m x xs s
apply (simp only: upt_conv_Cons map_Suc_upt[symmetric])
apply (subgoal_tac "∃ys zs. length ys = chunk ∧ xs = ys @ zs")
apply (clarsimp simp: heap_update_list_concat_unfold foldl_map
field_simps)
apply (rule exI[where x="take chunk xs"])
apply (rule exI[where x="drop chunk xs"])
apply simp
done
done
lemma update_ti_list_array':
"⟦ update_ti_list_t (map f [0 ..< n]) xs v = y;
∀n. size_td_tuple (f n) = v3; length xs = v3 * n;
∀m xs v'. length xs = v3 ∧ m < n ⟶
update_ti_tuple_t (f m) xs v' = Arrays.update v' m (update_ti_t (g m) xs (index v' m)) ⟧
⟹ y = foldr (λn arr. Arrays.update arr n (update_ti_t (g n) (take v3 (drop (v3 * n) xs)) (index arr n))) [0 ..< n] v"
apply (subgoal_tac "∀ys. size_td_list (map f ys) = v3 * length ys")
prefer 2
apply (rule allI)
subgoal for ys by (induct ys) auto
apply (induct n arbitrary: xs y v)
apply simp
apply (simp add: access_ti_append)
apply (elim meta_allE, drule(1) meta_mp)
apply simp
apply (rule foldr_cong, (rule refl)+)
apply (simp add: take_drop)
apply (subst min.absorb1)
apply (fold mult_Suc_right, rule mult_le_mono2)
apply simp
apply simp
done
lemma update_ti_list_array:
"⟦ update_ti_list_t (map f [0 ..< n]) xs v = (y :: 'a['b :: finite]);
∀n. size_td_tuple (f n) = v3; length xs = v3 * n;
∀m xs v'. length xs = v3 ∧ m < n ⟶
update_ti_tuple_t (f m) xs v' = Arrays.update v' m (update_ti_t (g m) xs (index v' m));
n ≤ card (UNIV :: 'b set) ⟧
⟹ ∀m < n. update_ti_t (g m) (take v3 (drop (v3 * m) xs)) (index v m) = index y m"
apply (subst update_ti_list_array'[where y=y], assumption+)
apply clarsimp
apply (subst index_fold_update)
apply clarsimp+
done
lemma access_in_array:
fixes y :: "('a :: c_type)['b :: finite]"
assumes assms: "h_val hp x = y"
"n < card (UNIV :: 'b set)"
and subst: "∀xs v. length xs = size_of TYPE('a)
⟶ update_ti_t (typ_info_t TYPE('a)) xs v = f xs"
shows "h_val hp
(Ptr (ptr_val x + of_nat (n * size_of TYPE('a)))) = index y n"
using assms
apply (simp add: h_val_def drop_heap_list_le2 del: of_nat_mult)
apply (subst take_heap_list_le[symmetric, where n="card (UNIV :: 'b set) * size_of TYPE ('a)"])
apply (fold mult_Suc, rule mult_le_mono1)
apply simp
apply (simp add: from_bytes_def typ_info_array')
apply (drule update_ti_list_array, simp+)
apply (simp add: size_of_def)
apply (clarsimp simp: update_ti_s_adjust_ti)
apply (rule refl)
apply simp
apply (drule spec, drule(1) mp)
apply (simp add: size_of_def ac_simps drop_take)
apply (subgoal_tac "length v = size_of TYPE('a)" for v)
apply (subst subst, assumption)
apply (subst(asm) subst, assumption)
apply simp
apply (simp add: size_of_def)
apply (subst le_diff_conv2)
apply simp
apply (fold mult_Suc, rule mult_le_mono1)
apply simp
done
lemma access_ti_list_array:
"⟦ ∀n. size_td_tuple (f n) = v3; length xs = v3 * n;
∀m. m < n ∧ v3 ≤ length (drop (v3 * m) xs)
⟶ access_ti_tuple (f m) (FCP g) (take v3 (drop (v3 * m) xs)) = (h m)
⟧ ⟹
access_ti_list (map f [0 ..< n]) (FCP g) xs
= foldl (@) [] (map h [0 ..< n])"
apply (subgoal_tac "∀ys. size_td_list (map f ys) = v3 * length ys")
prefer 2
apply (rule allI)
subgoal for ys by (induct ys, simp+)
apply (induct n arbitrary: xs)
apply simp
apply (simp add: access_ti_append)
apply (erule_tac x="take (v3 * n) xs" in meta_allE)
apply simp
apply (frule spec, drule mp, rule conjI, rule lessI)
apply simp
apply simp
apply (erule meta_mp)
apply (auto simp add: drop_take)
done
lemma take_drop_foldl_concat:
"⟦ ⋀y. y < m ⟹ length (f y) = n; x < m ⟧
⟹ take n (drop (x * n) (foldl (@) [] (map f [0 ..< m]))) = f x"
apply (subst split_upt_on_n, assumption)
apply (simp only: foldl_concat_concat map_append)
apply (subst drop_append_miracle)
apply (induct x, simp_all)[1]
apply simp
done
lemma heap_update_Array:
"heap_update (p ::('a::packed_type['b::finite]) ptr) arr
= (λs. foldl (λs n. heap_update (array_ptr_index p False n)
(Arrays.index arr n) s) s [0 ..< card (UNIV :: 'b set)])"
apply (rule ext, simp add: heap_update_def)
apply (subst coerce_heap_update_to_heap_updates
[OF _ refl, where chunk="size_of TYPE('a)" and m="card (UNIV :: 'b set)"])
apply (simp)
apply (rule foldl_cong[OF refl refl])
apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def)
subgoal for s a x
apply (rule arg_cong[where f="λxs. heap_update_list p xs s" for p s])
apply (simp add: to_bytes_def size_of_def
packed_type_access_ti)
apply (simp add: typ_info_array')
apply (subst fcp_eta[symmetric], subst access_ti_list_array)
apply simp
apply simp
apply (simp add: packed_type_access_ti size_of_def)
apply fastforce
apply (rule take_drop_foldl_concat)
apply (simp add: size_of_def)
apply simp
done
done
lemma from_bytes_Array_element:
fixes p :: "('a::mem_type['b::finite]) ptr"
assumes less: "of_nat n < card (UNIV :: 'b set)"
assumes len: "length bs = size_of TYPE('a) * CARD('b)"
shows
"index (from_bytes bs :: 'a['b]) n
= from_bytes (take (size_of TYPE('a)) (drop (n * size_of TYPE('a)) bs))"
using less
apply (simp add: from_bytes_def size_of_def typ_info_array')
apply (subst update_ti_list_array'[OF refl])
apply simp
apply (simp add: len size_of_def)
apply (clarsimp simp: update_ti_s_adjust_ti)
apply (rule refl)
apply (simp add: split_upt_on_n[OF less])
apply (rule trans, rule foldr_does_nothing_to_xf[where xf="λs. index s n"])
apply simp+
apply (subst foldr_does_nothing_to_xf[where xf="λs. index s n"])
apply simp
apply (simp add: mult.commute)
apply (frule Suc_leI)
apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2)
apply (rule upd_rf)
apply (simp add: size_of_def len mult.commute)
done
lemma heap_access_Array_element':
fixes p :: "('a::mem_type['b::finite]) ptr"
assumes less: "of_nat n < card (UNIV :: 'b set)"
shows
"index (h_val hp p) n
= h_val hp (array_ptr_index p False n)"
using less
apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def h_val_def)
apply (simp add: from_bytes_Array_element)
apply (simp add: drop_heap_list_le take_heap_list_le)
apply (subst take_heap_list_le)
apply (simp add: le_diff_conv2)
apply (drule Suc_leI)
apply (drule_tac k="size_of TYPE('a)" in mult_le_mono2)
apply (simp add: mult.commute)
apply simp
done
lemmas heap_access_Array_element
= heap_access_Array_element'[simplified array_ptr_index_simps]
lemma heap_update_id:
"h_val hp ptr = (v :: 'a :: packed_type)
⟹ heap_update ptr v hp = hp"
apply (simp add: h_val_def heap_update_def)
apply (rule heap_update_list_id'[where n="size_of TYPE('a)"])
apply clarsimp
apply (simp add: from_bytes_def to_bytes_def update_ti_t_def
size_of_def field_access_update_same
td_fafu_idem)
done
lemma heap_update_Array_update:
assumes n: "n < CARD('b :: finite)"
assumes size: "CARD('b) * size_of TYPE('a :: packed_type) < 2 ^ addr_bitsize"
shows "heap_update p (Arrays.update (arr :: 'a['b]) n v) hp
= heap_update (array_ptr_index p False n) v (heap_update p arr hp)"
proof -
have P: "⋀x k. ⟦ x < CARD('b); k < size_of TYPE('a) ⟧
⟹ unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: addr))
= x * size_of TYPE('a) + k"
using size
supply unsigned_of_nat
apply (cases "size_of TYPE('a)", simp_all)
apply (cases "CARD('b)", simp_all)
apply (subst unat_add_lem[THEN iffD1])
apply (simp add: unat_word_ariths unat_of_nat less_Suc_eq_le)
apply (subgoal_tac "Suc x * size_of TYPE('a) < 2 ^ addr_bitsize", simp_all)
apply (erule order_le_less_trans[rotated], simp add: add_mono)
apply (subst unat_mult_lem[THEN iffD1])
apply (simp add: unat_of_nat unat_add_lem[THEN iffD1])
apply (rule order_less_le_trans, erule order_le_less_trans[rotated],
rule add_mono, simp+)
apply (simp add: less_Suc_eq_le trans_le_add2)
apply simp
apply (simp add: unat_of_nat unat_add_lem[THEN iffD1])
done
let ?key_upd = "heap_update (array_ptr_index p False n) v"
note commute = fold_commute_apply[where h="?key_upd"
and xs="[Suc n ..< CARD('b)]", where g=f' and f=f' for f']
show ?thesis using n
apply (simp add: heap_update_Array split_upt_on_n[OF n]
foldl_conv_fold)
apply (subst commute)
apply (simp_all add: packed_heap_update_collapse
cong: fold_cong')
apply (rule ext, simp)
subgoal for x
apply (rule heap_update_commute, simp_all add: ptr_add_def)
apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def intvl_def Suc_le_eq)
apply (rule set_eqI, clarsimp)
apply (drule word_unat.Rep_inject[THEN iffD2])
apply (clarsimp simp: P nat_eq_add_iff1)
apply (cases x, simp_all add: less_Suc_eq_le Suc_diff_le)
done
done
qed
lemma heap_update_id_Array:
fixes arr :: "('a :: packed_type)['b :: finite]"
shows "arr = h_val hp p
⟹ heap_update p arr hp = hp"
apply (simp add: heap_update_Array)
apply (rule foldl_does_nothing[where s=hp])
apply (simp add: heap_access_Array_element' heap_update_id)
done
lemma heap_update_Array_element'':
fixes p' :: "(('a :: packed_type)['b::finite]) ptr"
fixes p :: "('a :: packed_type) ptr"
fixes hp w
assumes p: "p = array_ptr_index p' False n"
assumes n: "n < CARD('b)"
assumes size: "CARD('b) * size_of TYPE('a) < 2 ^ addr_bitsize"
shows "heap_update p' (Arrays.update (h_val hp p') n w) hp
= heap_update p w hp"
apply (subst heap_update_Array_update[OF n size])
apply (simp add: heap_update_id_Array p)
done
lemmas heap_update_Array_element'
= heap_update_Array_element''[simplified array_ptr_index_simps]
lemma array_count_size:
"CARD('b :: array_max_count) * size_of TYPE('a :: array_outer_max_size) < 2 ^ addr_bitsize"
using array_outer_max_size_ax[where 'a='a] array_max_count_ax[where 'a='b]
apply (clarsimp dest!: nat_le_Suc_less_imp)
apply (drule(1) mult_mono, simp+)
done
lemmas heap_update_Array_element
= heap_update_Array_element'[OF refl _ array_count_size]
lemma typ_slice_list_cut:
"⟦ (∀x ∈ set xs. size_td (dt_fst x) = m); m ≠ 0; n < (length xs * m) ⟧
⟹ typ_slice_list xs n =
typ_slice_tuple (xs ! (n div m)) (n mod m)"
apply (induct xs arbitrary: n, simp_all)
subgoal for x1 xs n
apply (intro conjI impI)
apply simp
apply (subgoal_tac "∃n'. n = n' + m")
apply clarsimp
apply (metis (no_types, opaque_lifting) add.commute add.left_neutral cancel_comm_monoid_add_class.diff_cancel
div_add1_eq div_mult_self_is_m mod_div_trivial modulo_nat_def mult.left_neutral nth_Cons_Suc plus_1_eq_Suc)
apply (rule exI[where x="n - m"])
apply simp
done
done
lemma typ_slice_t_array:
"⟦ n < CARD('b); y < size_of TYPE('a) ⟧
⟹ typ_slice_t (export_uinfo (typ_info_t TYPE('a))) y ≤
typ_slice_t (export_uinfo (array_tag TYPE('a['b :: finite])))
(y + size_of TYPE('a :: mem_type) * n)"
apply (simp add: array_tag_def array_tag_n_eq
split del: if_split)
apply (rule disjI2)
apply (subgoal_tac "y + (size_of TYPE('a) * n) < CARD('b) * size_of TYPE('a)")
apply (simp add: typ_slice_list_cut[where m="size_of TYPE('a)"]
map_td_list_map o_def size_of_def
sz_nzero[unfolded size_of_def])
apply (simp flip: export_uinfo_def)
apply (rule order_less_le_trans[where y="Suc n * size_of TYPE('a)"])
apply (simp add: size_of_def)
apply (simp only: size_of_def mult_le_mono1)
done
lemma h_t_valid_Array_element':
"⟦ htd ⊨⇩t (p :: (('a :: mem_type)['b :: finite]) ptr); coerce ∨ n < CARD('b) ⟧
⟹ htd ⊨⇩t array_ptr_index p coerce n" for coerce
apply (clarsimp simp only: h_t_valid_def valid_footprint_def Let_def
c_guard_def c_null_guard_def)
apply (subgoal_tac "∃offs. array_ptr_index p coerce n = CTypesDefs.ptr_add (ptr_coerce p) (of_nat offs)
∧ offs < CARD ('b)")
apply (clarsimp simp: size_td_array size_of_def typ_uinfo_t_def
typ_info_array array_tag_def)
subgoal for offs
apply (intro conjI)
apply (clarsimp simp: CTypesDefs.ptr_add_def
field_simps)
apply (rename_tac y)
apply (drule_tac x="offs * size_of TYPE('a) + y" in spec)
apply (drule mp)
apply (rule order_less_le_trans[where y="Suc offs * size_of TYPE('a)"])
apply (simp add: size_of_def)
apply (simp only: size_of_def mult_le_mono1)
apply (clarsimp simp: field_simps)
apply (erule map_le_trans[rotated])
apply (rule list_map_mono)
apply (subst mult.commute, rule typ_slice_t_array[unfolded array_tag_def])
apply assumption
apply (simp add: size_of_def)
apply (simp add: ptr_aligned_def align_of_def align_td_array
array_ptr_index_def
CTypesDefs.ptr_add_def unat_word_ariths unat_of_nat)
using align_size_of[where 'a='a] align[where 'a='a]
apply (simp add: align_of_def size_of_def addr_card_def card_word)
apply (simp add: dvd_mod)
apply (thin_tac "∀x. P x" for P)
apply (clarsimp simp: intvl_def)
apply (rename_tac k)
apply (drule_tac x="offs * size_of TYPE('a) + k" in spec)
apply (drule mp)
apply (simp add: array_ptr_index_def CTypesDefs.ptr_add_def field_simps)
apply (erule notE)
apply (rule order_less_le_trans[where y="Suc offs * size_of TYPE('a)"])
apply (simp add: size_of_def)
apply (simp only: size_of_def mult_le_mono1)
done
subgoal by (auto simp add: array_ptr_index_def intro: exI[where x=0])
done
lemma h_t_valid_Array_element:
"⟦ htd ⊨⇩t (p :: (('a :: mem_type)['b :: finite]) ptr); 0 ≤ n; n < int CARD('b) ⟧
⟹ htd ⊨⇩t ((ptr_coerce p :: 'a ptr) +⇩p n)"
apply (drule_tac n="nat n" and coerce=False in h_t_valid_Array_element')
apply simp
apply (simp add: array_ptr_index_def)
done
lemma ptr_safe_Array_element:
"⟦ ptr_safe (p :: (('a :: mem_type)['b :: finite]) ptr) htd; coerce ∨ n < CARD('b) ⟧
⟹ ptr_safe (array_ptr_index p coerce n) htd" for coerce
apply (simp add: ptr_safe_def)
apply (erule order_trans[rotated])
apply (subgoal_tac "∃offs. array_ptr_index p coerce n = CTypesDefs.ptr_add (ptr_coerce p) (of_nat offs)
∧ offs < CARD ('b)")
prefer 2
subgoal by (auto simp: array_ptr_index_def intro: exI[where x=0])[1]
apply (clarsimp simp: s_footprint_def s_footprint_untyped_def
CTypesDefs.ptr_add_def
size_td_array size_of_def)
subgoal for offs x k
apply (rule exI[where x="offs * size_of TYPE('a) + x"])
apply (simp add: size_of_def)
apply (rule conjI)
apply (rule order_less_le_trans[where y="Suc offs * size_of TYPE('a)"])
apply (simp add: size_of_def)
apply (simp only: size_of_def)
apply (rule mult_le_mono1)
apply simp
apply (thin_tac "coerce ∨ P" for P)
apply (elim disjE exE conjE, simp_all add: typ_uinfo_t_def)
apply (erule order_less_le_trans)
apply (rule prefix_length_le)
apply (rule order_trans, erule typ_slice_t_array)
apply (simp add: size_of_def)
apply (simp add: size_of_def field_simps typ_info_array)
done
done
lemma from_bytes_eq:
"from_bytes [x] = x"
apply (clarsimp simp:from_bytes_def update_ti_t_def typ_info_word)
apply (simp add:word_rcat_def)
done
lemma bytes_disjoint:"(x::('a::c_type) ptr) ≠ y ⟹ {ptr_val x + a ..+ 1} ∩ {ptr_val y + a ..+ 1} = {}"
by (clarsimp simp:intvl_def)
lemma byte_ptrs_disjoint:"(x::('a::c_type) ptr) ≠ y ⟹ ∀i < of_nat (size_of TYPE('a)). ptr_val x + i ≠ ptr_val y + i"
by force
lemma le_step:"⟦(x::('a::len) word) < y + 1; x ≠ y⟧ ⟹ x < y"
by (metis less_x_plus_1 max_word_max order_less_le)
lemma ptr_add_disjoint:
"⟦ ptr_val y ∉ {ptr_val x ..+ size_of TYPE('a)};
ptr_val (x::('a::c_type) ptr) < ptr_val (y::('b::c_type) ptr);
a < of_nat (size_of TYPE('a)) ⟧ ⟹
ptr_val x + a < ptr_val y"
apply (erule swap)
apply (rule intvl_inter_le [where k=0 and ka="unat (ptr_val y - ptr_val x)"])
apply clarsimp
apply (metis (opaque_lifting, mono_tags) add_diff_cancel2 add_diff_inverse diff_add_cancel
trans_less_add1 unat_less_helper word_le_less_eq word_less_add_right
word_of_nat_less word_unat.Rep_inverse)
apply simp
done
lemma ptr_add_disjoint2:
"⟦ ptr_val x ∉ {ptr_val y ..+ size_of TYPE('a)};
ptr_val (y::('b::c_type) ptr) < ptr_val (x::('a::c_type) ptr);
a < of_nat (size_of TYPE('a)) ⟧ ⟹
ptr_val y + a < ptr_val x"
apply (erule swap)
apply (rule intvl_inter_le[where k=0 and ka="unat (ptr_val x - ptr_val y)"])
apply clarsimp
apply (metis (no_types, opaque_lifting) add.commute less_imp_le less_le_trans not_le unat_less_helper
word_diff_ls'(4))
apply simp
done
lemma ptr_aligned_is_aligned:"⟦ptr_aligned (x::('a::c_type) ptr); align_of TYPE('a) = 2 ^ n⟧ ⟹ is_aligned (ptr_val x) n"
by (clarsimp simp: ptr_aligned_def is_aligned_def)
lemma intvl_no_overflow:
assumes no_overflow: "unat a + b < 2 ^ len_of TYPE('a::len)"
shows "(x ∈ {(a :: 'a word) ..+ b}) = (a ≤ x ∧ x < (a + of_nat b))"
proof -
obtain "sk" :: "'a word ⇒ 'a word ⇒ nat ⇒ nat"
where f1: "⋀x y z. x ∉ {y..+z} ∨ x = y + of_nat (sk x y z) ∧ sk x y z < z"
using [[metis_new_skolem]] by (metis intvlD)
have f2: "⋀x. a + x < a + of_nat b ∨ ¬ x < of_nat b"
using no_overflow
by (metis PackedTypes.of_nat_mono_maybe_le add_lessD1 le_add1
add.commute olen_add_eqv unat_of_nat_eq word_arith_nat_add
word_plus_strict_mono_right)
have f3: "∀x y. y ∉ {x..+b} ∨ of_nat (sk y x b) < (of_nat b :: 'a word)"
using no_overflow f1
by (metis add_lessD1 add.commute of_nat_mono_maybe)
have "x < a + of_nat b ∨ ¬ of_nat (sk x a b) < (of_nat b :: 'a word) ∨ ?thesis"
using f1 f2 by metis
hence "x < a + of_nat b ∨ ?thesis"
using f3 by metis
thus "?thesis"
apply (rule disjE)
apply (rule iffI)
apply (clarsimp simp: intvl_def)
apply (rename_tac k)
apply (clarsimp simp: unat_sub_if_size word_le_nat_alt word_less_nat_alt)
apply (cut_tac no_overflow)
apply (subgoal_tac "k + (b + unat a) < 2 ^ len_of (TYPE('a)) + b")
apply (subgoal_tac "k + unat a < 2 ^ len_of (TYPE('a))")
apply (metis add_lessD1 le_def less_not_refl2 add.commute unat_eq_of_nat word_arith_nat_add)
apply clarsimp
apply clarsimp
apply (clarsimp simp: intvl_def)
apply (rule exI [where x="unat (x - a)"])
apply (clarsimp simp: unat_sub_if_size word_le_nat_alt word_less_nat_alt)
apply (cut_tac no_overflow)
apply (metis diff_le_self le_add_diff_inverse le_diff_conv le_eq_less_or_eq le_unat_uoi add.commute nat_neq_iff unat_of_nat_eq word_arith_nat_add)
apply simp
done
qed
lemma FCP_arg_cong:"f = g ⟹ FCP f = FCP g"
by simp
lemma h_val_id:
"h_val (hrs_mem (hrs_mem_update (heap_update x y) s)) x = (y::'a::mem_type)"
apply (subst hrs_mem_update)
apply (rule h_val_heap_update)
done
lemma h_val_id_padding:
"length bs = size_of TYPE('a) ⟹ h_val (hrs_mem (hrs_mem_update (heap_update_padding x y bs) s)) x = (y::'a::mem_type)"
apply (subst hrs_mem_update)
apply (simp add: h_val_heap_update_padding)
done
lemma heap_update_id2:
"hrs_mem_update (heap_update p ((h_val (hrs_mem s) p)::'a::packed_type)) s = s"
apply (clarsimp simp:hrs_mem_update_def case_prod_beta)
apply (subst heap_update_id)
apply (simp add:hrs_mem_def)+
done
lemma intvlI_unat:"unat b < unat c ⟹ a + b ∈ {a ..+ unat c}"
by (metis intvlI word_unat.Rep_inverse)
lemma neq_imp_bytes_disjoint:
"⟦ c_guard (x::'a::c_type ptr); c_guard y; unat j < align_of TYPE('a);
unat i < align_of TYPE('a); x ≠ y; 2 ^ n = align_of TYPE('a); n < 32⟧ ⟹
ptr_val x + j ≠ ptr_val y + i"
apply (rule ccontr)
apply (subgoal_tac "is_aligned (ptr_val x) n")
apply (subgoal_tac "is_aligned (ptr_val y) n")
apply (subgoal_tac "(ptr_val x + j && ~~ mask n) = (ptr_val y + i && ~~ mask n)")
apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt)
apply (subst (asm) neg_mask_add_aligned, simp, simp add: word_less_nat_alt)
apply clarsimp
apply simp
apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def)
apply (clarsimp simp: c_guard_def ptr_aligned_def is_aligned_def)
done
lemma heap_update_list_base':"heap_update_list p [] = id"
by (rule ext, simp)
lemma hrs_mem_update_id3: "hrs_mem_update id = id"
unfolding hrs_mem_update_def by simp
lemma h_t_valid_ptr_retyp_inside_eq:
fixes p :: "'a :: mem_type ptr" and p' :: "'a :: mem_type ptr"
assumes inside: "ptr_val p' ∈ {ptr_val p ..+ size_of TYPE('a)}"
and ht: "ptr_retyp p td, g ⊨⇩t p'"
shows "p = p'"
using ptr_retyp_same_cleared_region[OF ht] inside mem_type_self[where p=p']
by blast
lemma typ_slice_t_self_nth:
"∃n < length (typ_slice_t td m). ∃b. typ_slice_t td m ! n = (td, b)"
using typ_slice_t_self [where td = td and m = m]
by (fastforce simp add: in_set_conv_nth)
lemma ptr_retyp_other_cleared_region:
fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
assumes ht: "ptr_retyp p td, g ⊨⇩t p'"
and tdisj: "typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b :: mem_type)"
and clear: "∀x ∈ {ptr_val p ..+ size_of TYPE('a)}. ∀n b. snd (td x) n ≠ Some (typ_uinfo_t TYPE('b), b)"
shows "{ptr_val p'..+ size_of TYPE('b)} ∩ {ptr_val p ..+ size_of TYPE('a)} = {}"
proof (rule classical)
assume asm: "{ptr_val p'..+ size_of TYPE('b)} ∩ {ptr_val p ..+ size_of TYPE('a)} ≠ {}"
then obtain mv where mvp: "mv ∈ {ptr_val p..+size_of TYPE('a)}"
and mvp': "mv ∈ {ptr_val p'..+size_of TYPE('b)}"
by blast
then obtain k' where mv: "mv = ptr_val p' + of_nat k'" and klt: "k' < size_td (typ_info_t TYPE('b))"
by (clarsimp dest!: intvlD simp: size_of_def)
let ?mv = "ptr_val p' + of_nat k'"
obtain n b where nl: "n < length (typ_slice_t (typ_uinfo_t TYPE('b)) k')"
and tseq: "typ_slice_t (typ_uinfo_t TYPE('b)) k' ! n = (typ_uinfo_t TYPE('b), b)"
using typ_slice_t_self_nth [where td = "typ_uinfo_t TYPE('b)" and m = k']
by clarsimp
with ht have "snd (ptr_retyp p td ?mv) n = Some (typ_uinfo_t TYPE('b), b)"
unfolding h_t_valid_def
apply -
apply (clarsimp simp: valid_footprint_def Let_def)
apply (drule spec, drule mp [OF _ klt])
apply (clarsimp simp: map_le_def)
apply (drule bspec)
apply simp
apply simp
done
moreover {
assume "snd (ptr_retyp p empty_htd ?mv) n = Some (typ_uinfo_t TYPE('b), b)"
hence "(typ_uinfo_t TYPE('b)) ∈ fst ` set (typ_slice_t (typ_uinfo_t TYPE('a))
(unat (ptr_val p' + of_nat k' - ptr_val p)))"
using asm mv mvp
apply -
apply (rule image_eqI[where x = "(typ_uinfo_t TYPE('b), b)"])
apply simp
apply (fastforce simp add: ptr_retyp_footprint list_map_eq in_set_conv_nth split: if_split_asm)
done
with typ_slice_set have "(typ_uinfo_t TYPE('b)) ∈ fst ` td_set (typ_uinfo_t TYPE('a)) 0"
by (rule subsetD)
hence False using tdisj by (clarsimp simp: tag_disj_def typ_tag_le_def)
} ultimately show ?thesis using mvp mvp' mv unfolding h_t_valid_def valid_footprint_def
apply -
apply (subst (asm) ptr_retyp_d_eq_snd)
apply (auto simp add: map_add_Some_iff clear)
done
qed
end