898 lines
27 KiB
Plaintext
898 lines
27 KiB
Plaintext
(*
|
|
* Copyright 2014, NICTA
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_BSD2.txt" for details.
|
|
*
|
|
* @TAG(NICTA_BSD)
|
|
*)
|
|
|
|
theory Aligned
|
|
imports WordLib MoreDivides WordSetup
|
|
begin
|
|
|
|
lemma is_aligned_mask: "(is_aligned w n) = (w && mask n = 0)"
|
|
unfolding is_aligned_def by (rule and_mask_dvd_nat)
|
|
|
|
|
|
lemma list_of_false:
|
|
"True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False"
|
|
by (induct xs, simp_all)
|
|
|
|
lemma eq_zero_set_bl: "(w = 0) = (True \<notin> set (to_bl w))"
|
|
apply (subst word_bl.Rep_inject[symmetric])
|
|
apply (subst to_bl_0)
|
|
apply (rule iffI)
|
|
apply clarsimp
|
|
apply (drule list_of_false)
|
|
apply simp
|
|
done
|
|
|
|
lemmas and_bang = word_and_nth
|
|
|
|
lemma diff_diff_less: "(i < m - (m - (n :: nat))) = (i < m \<and> i < n)"
|
|
apply (case_tac "n \<le> m")
|
|
apply fastforce+
|
|
done
|
|
|
|
lemma is_aligned_to_bl:
|
|
"is_aligned (w :: 'a :: len word) n = (True \<notin> set (drop (size w - n) (to_bl w)))"
|
|
apply (simp add: is_aligned_mask eq_zero_set_bl)
|
|
apply (clarsimp simp: in_set_conv_nth word_size)
|
|
apply (simp add: to_bl_nth word_size cong: conj_cong)
|
|
apply (simp add: diff_diff_less)
|
|
apply safe
|
|
apply (case_tac "n \<le> len_of TYPE('a)")
|
|
prefer 2
|
|
apply (rule_tac x=i in exI)
|
|
apply clarsimp
|
|
apply (subgoal_tac "\<exists>j < len_of TYPE('a). j < n \<and> len_of TYPE('a) - n + j = i")
|
|
apply (erule exE)
|
|
apply (rule_tac x=j in exI)
|
|
apply clarsimp
|
|
apply (thin_tac "w !! t" for t)
|
|
apply (rule_tac x="i + n - len_of TYPE('a)" in exI)
|
|
apply clarsimp
|
|
apply arith
|
|
apply (rule_tac x="len_of TYPE('a) - n + i" in exI)
|
|
apply clarsimp
|
|
apply arith
|
|
done
|
|
|
|
lemma unat_power_lower [simp]:
|
|
assumes nv: "n < len_of TYPE('a::len)"
|
|
shows "unat ((2::'a::len word) ^ n) = 2 ^ n"
|
|
apply (subst word_unat_power)
|
|
apply (subst unat_of_nat)
|
|
apply (subst mod_less)
|
|
apply (simp add: nv)
|
|
apply simp
|
|
done
|
|
|
|
lemma power_overflow:
|
|
"n \<ge> len_of TYPE('a) \<Longrightarrow> 2 ^ n = (0 :: 'a::len word)"
|
|
apply (subgoal_tac "\<exists>m. n = (len_of TYPE ('a)) + m")
|
|
apply safe
|
|
apply (simp only: power_add word_pow_0)
|
|
apply simp
|
|
apply (rule exI[where x="n - len_of TYPE ('a)"])
|
|
apply simp
|
|
done
|
|
|
|
lemma is_alignedI [intro?]:
|
|
fixes x::"'a::len word"
|
|
assumes xv: "x = 2 ^ n * k"
|
|
shows "is_aligned x n"
|
|
proof cases
|
|
assume nv: "n < len_of TYPE('a)"
|
|
show ?thesis
|
|
unfolding is_aligned_def
|
|
proof (rule dvdI [where k = "unat k mod 2 ^ (len_of TYPE('a) - n)"])
|
|
from xv
|
|
have "unat x = (unat (2::word32) ^ n * unat k) mod 2 ^ len_of TYPE('a)"
|
|
using nv
|
|
by (subst (asm) word_unat.Rep_inject [symmetric], simp,
|
|
subst unat_word_ariths, simp)
|
|
|
|
also have "\<dots> = 2 ^ n * (unat k mod 2 ^ (len_of TYPE('a) - n))" using nv
|
|
by (simp add: mult_mod_right power_add [symmetric] add_diff_inverse)
|
|
|
|
finally show "unat x = 2 ^ n * (unat k mod 2 ^ (len_of TYPE('a) - n))" .
|
|
qed
|
|
next
|
|
assume "\<not> n < len_of TYPE('a)"
|
|
with xv
|
|
show ?thesis by (simp add: not_less power_overflow is_aligned_def)
|
|
qed
|
|
|
|
lemma is_aligned_weaken:
|
|
"\<lbrakk> is_aligned w x; x \<ge> y \<rbrakk> \<Longrightarrow> is_aligned w y"
|
|
apply (simp add: is_aligned_def)
|
|
apply (rule dvd_trans)
|
|
prefer 2
|
|
apply assumption
|
|
apply (simp add: le_imp_power_dvd)
|
|
done
|
|
|
|
|
|
lemma nat_power_less_diff:
|
|
assumes lt: "(2::nat) ^ n * q < 2 ^ m"
|
|
shows "q < 2 ^ (m - n)"
|
|
using lt
|
|
proof (induct n arbitrary: m)
|
|
case 0
|
|
thus ?case by simp
|
|
next
|
|
case (Suc n)
|
|
|
|
have ih: "\<And>m. 2 ^ n * q < 2 ^ m \<Longrightarrow> q < 2 ^ (m - n)"
|
|
and prem: "2 ^ Suc n * q < 2 ^ m" by fact+
|
|
|
|
show ?case
|
|
proof (cases m)
|
|
case 0
|
|
thus ?thesis using Suc by simp
|
|
next
|
|
case (Suc m')
|
|
thus ?thesis using prem
|
|
by (simp add: ac_simps ih)
|
|
qed
|
|
qed
|
|
|
|
lemma is_alignedE_pre:
|
|
fixes w::"'a::len word"
|
|
assumes aligned: "is_aligned w n"
|
|
shows rl: "\<exists>q. w = 2 ^ n * (of_nat q) \<and> q < 2 ^ (len_of TYPE('a) - n)"
|
|
proof -
|
|
from aligned obtain q where wv: "unat w = 2 ^ n * q"
|
|
unfolding is_aligned_def ..
|
|
|
|
show ?thesis
|
|
proof (rule exI, intro conjI)
|
|
show "q < 2 ^ (len_of TYPE('a) - n)"
|
|
proof (rule nat_power_less_diff)
|
|
have "unat w < 2 ^ size w" unfolding word_size ..
|
|
hence "unat w < 2 ^ len_of TYPE('a)" by simp
|
|
with wv show "2 ^ n * q < 2 ^ len_of TYPE('a)" by simp
|
|
qed
|
|
|
|
have r: "of_nat (2 ^ n) = (2::word32) ^ n"
|
|
by (induct n) simp+
|
|
|
|
from wv have "of_nat (unat w) = of_nat (2 ^ n * q)" by simp
|
|
hence "w = of_nat (2 ^ n * q)" by (subst word_unat.Rep_inverse [symmetric])
|
|
thus "w = 2 ^ n * (of_nat q)" by (simp add: r)
|
|
qed
|
|
qed
|
|
|
|
lemma is_alignedE:
|
|
"\<lbrakk>is_aligned (w::'a::len word) n;
|
|
\<And>q. \<lbrakk>w = 2 ^ n * (of_nat q); q < 2 ^ (len_of TYPE('a) - n)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
|
|
by (auto dest: is_alignedE_pre)
|
|
|
|
lemma is_aligned_replicate:
|
|
fixes w::"'a::len word"
|
|
assumes aligned: "is_aligned w n"
|
|
and nv: "n \<le> len_of TYPE('a)"
|
|
shows "to_bl w = (take (len_of TYPE('a) - n) (to_bl w)) @ replicate n False"
|
|
proof -
|
|
from nv have rl: "\<And>q. q < 2 ^ (len_of TYPE('a) - n) \<Longrightarrow>
|
|
to_bl (2 ^ n * (of_nat q :: 'a word)) =
|
|
drop n (to_bl (of_nat q :: 'a word)) @ replicate n False"
|
|
apply (subst shiftl_t2n [symmetric])
|
|
apply (subst bl_shiftl)
|
|
apply (simp add: min_def word_size)
|
|
done
|
|
|
|
show ?thesis using aligned
|
|
by (auto simp: rl elim: is_alignedE)
|
|
qed
|
|
|
|
lemma is_aligned_drop:
|
|
fixes w::"'a::len word"
|
|
assumes "is_aligned w n" "n \<le> len_of TYPE('a)"
|
|
shows "drop (len_of TYPE('a) - n) (to_bl w) = replicate n False"
|
|
proof -
|
|
have "to_bl w = take (len_of TYPE('a) - n) (to_bl w) @ replicate n False"
|
|
by (rule is_aligned_replicate) fact+
|
|
hence "drop (len_of TYPE('a) - n) (to_bl w) = drop (len_of TYPE('a) - n) \<dots>" by simp
|
|
also have "\<dots> = replicate n False" by simp
|
|
finally show ?thesis .
|
|
qed
|
|
|
|
lemma less_is_drop_replicate:
|
|
fixes x::"'a::len word"
|
|
assumes lt: "x < 2 ^ n"
|
|
shows "to_bl x = replicate (len_of TYPE('a) - n) False @ drop (len_of TYPE('a) - n) (to_bl x)"
|
|
proof -
|
|
show ?thesis
|
|
apply (subst less_mask_eq [OF lt, symmetric])
|
|
apply (subst bl_and_mask)
|
|
apply simp
|
|
done
|
|
qed
|
|
|
|
lemma is_aligned_add_conv:
|
|
fixes off::"'a::len word"
|
|
assumes aligned: "is_aligned w n"
|
|
and offv: "off < 2 ^ n"
|
|
shows "to_bl (w + off) =
|
|
(take (len_of TYPE('a) - n) (to_bl w)) @ (drop (len_of TYPE('a) - n) (to_bl off))"
|
|
proof cases
|
|
assume nv: "n \<le> len_of TYPE('a)"
|
|
show ?thesis
|
|
proof (subst aligned_bl_add_size, simp_all only: word_size)
|
|
show "drop (len_of TYPE('a) - n) (to_bl w) = replicate n False"
|
|
by (subst is_aligned_replicate [OF aligned nv]) (simp add: word_size)
|
|
|
|
from offv show "take (len_of TYPE('a) - n) (to_bl off) =
|
|
replicate (len_of TYPE('a) - n) False"
|
|
by (subst less_is_drop_replicate, assumption) simp
|
|
qed fact
|
|
next
|
|
assume "\<not> n \<le> len_of TYPE('a)"
|
|
with offv show ?thesis by (simp add: power_overflow)
|
|
qed
|
|
|
|
lemma nat_less_power_trans:
|
|
fixes n :: nat
|
|
assumes nv: "n < 2 ^ (m - k)"
|
|
and kv: "k \<le> m"
|
|
shows "2 ^ k * n < 2 ^ m"
|
|
proof (rule order_less_le_trans)
|
|
show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)"
|
|
by (rule mult_less_mono2 [OF nv zero_less_power]) simp
|
|
|
|
show "(2::nat) ^ k * 2 ^ (m - k) \<le> 2 ^ m" using nv kv
|
|
by (subst power_add [symmetric]) simp
|
|
qed
|
|
|
|
lemma aligned_add_aligned:
|
|
fixes x::"'a::len word"
|
|
assumes aligned1: "is_aligned x n"
|
|
and aligned2: "is_aligned y m"
|
|
and lt: "m \<le> n"
|
|
shows "is_aligned (x + y) m"
|
|
proof cases
|
|
assume nlt: "n < len_of TYPE('a)"
|
|
show ?thesis
|
|
unfolding is_aligned_def dvd_def
|
|
proof -
|
|
from aligned2 obtain q2 where yv: "y = 2 ^ m * of_nat q2"
|
|
and q2v: "q2 < 2 ^ (len_of TYPE('a) - m)"
|
|
by (auto elim: is_alignedE)
|
|
|
|
from lt obtain k where kv: "m + k = n" by (auto simp: le_iff_add)
|
|
with aligned1 obtain q1 where xv: "x = 2 ^ (m + k) * of_nat q1"
|
|
and q1v: "q1 < 2 ^ (len_of TYPE('a) - (m + k))"
|
|
by (auto elim: is_alignedE)
|
|
|
|
have l1: "2 ^ (m + k) * q1 < 2 ^ len_of TYPE('a)"
|
|
by (rule nat_less_power_trans [OF q1v])
|
|
(subst kv, rule order_less_imp_le [OF nlt])
|
|
|
|
have l2: "2 ^ m * q2 < 2 ^ len_of TYPE('a)"
|
|
by (rule nat_less_power_trans [OF q2v],
|
|
rule order_less_imp_le [OF order_le_less_trans])
|
|
fact+
|
|
|
|
have "x = of_nat (2 ^ (m + k) * q1)" using xv
|
|
by simp
|
|
|
|
moreover have "y = of_nat (2 ^ m * q2)" using yv
|
|
by simp
|
|
|
|
ultimately have upls: "unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)"
|
|
apply -
|
|
apply (erule ssubst)+
|
|
apply (subst unat_of_nat)
|
|
apply (subst mod_less [OF l1])
|
|
apply (subst unat_of_nat)
|
|
apply (subst mod_less [OF l2])
|
|
apply (subst power_add)
|
|
apply (subst add_mult_distrib2)
|
|
apply simp
|
|
done
|
|
|
|
(* (2 ^ k * q1 + q2) *)
|
|
show "\<exists>d. unat (x + y) = 2 ^ m * d"
|
|
proof (cases "unat x + unat y < 2 ^ len_of TYPE('a)")
|
|
case True
|
|
|
|
have "unat (x + y) = unat x + unat y"
|
|
by (subst unat_plus_if', rule if_P) fact
|
|
|
|
also have "\<dots> = 2 ^ m * (2 ^ k * q1 + q2)" by (rule upls)
|
|
finally show ?thesis ..
|
|
next
|
|
case False
|
|
hence "unat (x + y) = (unat x + unat y) mod 2 ^ len_of TYPE('a)"
|
|
by (subst unat_word_ariths(1)) simp
|
|
|
|
also have "\<dots> = (2 ^ m * (2 ^ k * q1 + q2)) mod 2 ^ len_of TYPE('a)"
|
|
by (subst upls, rule refl)
|
|
|
|
also have "\<dots> = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (len_of TYPE('a) - m))"
|
|
apply (subst mult_mod_right)
|
|
apply (subst power_add [symmetric])
|
|
apply (subst le_add_diff_inverse
|
|
[OF order_trans[OF lt order_less_imp_le[OF nlt]]])
|
|
apply (rule refl)
|
|
done
|
|
|
|
finally show ?thesis ..
|
|
qed
|
|
qed
|
|
next
|
|
assume "\<not> n < len_of TYPE('a)"
|
|
with assms
|
|
show ?thesis by (simp add: not_less power_overflow is_aligned_mask mask_def)
|
|
qed
|
|
|
|
corollary aligned_sub_aligned:
|
|
"\<lbrakk>is_aligned (x::'a::len word) n; is_aligned y m; m \<le> n\<rbrakk>
|
|
\<Longrightarrow> is_aligned (x - y) m"
|
|
apply (simp del: add_uminus_conv_diff add:diff_conv_add_uminus)
|
|
apply (erule aligned_add_aligned, simp_all)
|
|
apply (erule is_alignedE)
|
|
apply (rule_tac k="- of_nat q" in is_alignedI)
|
|
apply simp
|
|
done
|
|
|
|
lemma is_aligned_shift:
|
|
fixes k::"'a::len word"
|
|
shows "is_aligned (k << m) m"
|
|
proof cases
|
|
assume mv: "m < len_of TYPE('a)"
|
|
from mv obtain q where mq: "m + q = len_of TYPE('a)" and "0 < q"
|
|
by (auto dest: less_imp_add_positive)
|
|
|
|
have "(2\<Colon>nat) ^ m dvd unat (k << m)"
|
|
proof
|
|
have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k"
|
|
by (rule mod_div_equality)
|
|
|
|
have "unat (k << m) = unat (2 ^ m * k)" by (simp add: shiftl_t2n)
|
|
also have "\<dots> = (2 ^ m * unat k) mod (2 ^ len_of TYPE('a))" using mv
|
|
by (subst unat_word_ariths(2))+ simp
|
|
also have "\<dots> = 2 ^ m * (unat k mod 2 ^ q)"
|
|
by (subst mq [symmetric], subst power_add, subst mod_mult2_eq) simp
|
|
finally show "unat (k << m) = 2 ^ m * (unat k mod 2 ^ q)" .
|
|
qed
|
|
|
|
thus ?thesis by (unfold is_aligned_def)
|
|
next
|
|
assume "\<not> m < len_of TYPE('a)"
|
|
thus ?thesis
|
|
by (simp add: not_less power_overflow is_aligned_mask mask_def
|
|
shiftl_zero_size word_size)
|
|
qed
|
|
|
|
lemma word_mod_by_0: "k mod (0::'a::len word) = k"
|
|
by (simp add: word_arith_nat_mod)
|
|
|
|
lemma aligned_mod_eq_0:
|
|
fixes p::"'a::len word"
|
|
assumes al: "is_aligned p sz"
|
|
shows "p mod 2 ^ sz = 0"
|
|
proof cases
|
|
assume szv: "sz < len_of TYPE('a)"
|
|
with al
|
|
show ?thesis
|
|
unfolding is_aligned_def
|
|
apply -
|
|
apply (rule word_unat.Rep_eqD)
|
|
apply (subst unat_mod)
|
|
apply (simp add: dvd_eq_mod_eq_0)
|
|
done
|
|
next
|
|
assume "\<not> sz < len_of TYPE('a)"
|
|
with al show ?thesis
|
|
by (simp add: not_less power_overflow is_aligned_mask mask_def
|
|
word_mod_by_0)
|
|
qed
|
|
|
|
lemma is_aligned_triv: "is_aligned (2 ^ n ::'a::len word) n"
|
|
by (rule is_alignedI [where k = 1], simp)
|
|
|
|
lemma is_aligned_mult_triv1: "is_aligned (2 ^ n * x ::'a::len word) n"
|
|
by (rule is_alignedI [OF refl])
|
|
|
|
lemma is_aligned_mult_triv2: "is_aligned (x * 2 ^ n ::'a::len word) n"
|
|
by (subst mult.commute, simp add: is_aligned_mult_triv1)
|
|
|
|
lemma word_power_less_0_is_0:
|
|
fixes x :: "'a::len word"
|
|
shows "x < a ^ 0 \<Longrightarrow> x = 0" by simp
|
|
|
|
lemma nat_add_offset_less:
|
|
fixes x :: nat
|
|
assumes yv: "y < 2 ^ n"
|
|
and xv: "x < 2 ^ m"
|
|
and mn: "sz = m + n"
|
|
shows "x * 2 ^ n + y < 2 ^ sz"
|
|
proof (subst mn)
|
|
from yv obtain qy where "y + qy = 2 ^ n" and "0 < qy"
|
|
by (auto dest: less_imp_add_positive)
|
|
|
|
have "x * 2 ^ n + y < x * 2 ^ n + 2 ^ n" by simp fact+
|
|
also have "\<dots> = (x + 1) * 2 ^ n" by simp
|
|
also have "\<dots> \<le> 2 ^ (m + n)" using xv
|
|
by (subst power_add) (rule mult_le_mono1, simp)
|
|
finally show "x * 2 ^ n + y < 2 ^ (m + n)" .
|
|
qed
|
|
|
|
lemma is_aligned_no_wrap:
|
|
fixes off :: "'a::len word"
|
|
fixes ptr :: "'a::len word"
|
|
assumes al: "is_aligned ptr sz"
|
|
and off: "off < 2 ^ sz"
|
|
shows "unat ptr + unat off < 2 ^ len_of TYPE('a)"
|
|
proof -
|
|
have szv: "sz < len_of TYPE('a)"
|
|
apply (rule ccontr)
|
|
using off
|
|
by (clarsimp simp: not_less p2_eq_0[THEN iffD2])
|
|
|
|
from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
|
|
qv: "q < 2 ^ (len_of TYPE('a) - sz)" by (auto elim: is_alignedE)
|
|
|
|
show ?thesis
|
|
proof (cases "sz = 0")
|
|
case True
|
|
thus ?thesis using off ptrq qv
|
|
by clarsimp
|
|
next
|
|
case False
|
|
hence sne: "0 < sz" ..
|
|
|
|
show ?thesis
|
|
proof -
|
|
have uq: "unat (of_nat q ::'a::len word) = q"
|
|
apply (subst unat_of_nat)
|
|
apply (rule mod_less)
|
|
apply (rule order_less_trans [OF qv])
|
|
apply (rule power_strict_increasing [OF diff_less [OF sne]])
|
|
apply (simp_all)
|
|
done
|
|
|
|
have uptr: "unat ptr = 2 ^ sz * q"
|
|
apply (subst ptrq)
|
|
apply (subst iffD1 [OF unat_mult_lem])
|
|
apply (subst unat_power_lower [OF szv])
|
|
apply (subst uq)
|
|
apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]])
|
|
apply (subst uq)
|
|
apply (subst unat_power_lower [OF szv])
|
|
apply simp
|
|
done
|
|
|
|
show "unat ptr + unat off < 2 ^ len_of TYPE('a)" using szv
|
|
apply (subst uptr)
|
|
apply (subst mult.commute, rule nat_add_offset_less [OF _ qv])
|
|
apply (rule order_less_le_trans [OF unat_mono [OF off] order_eq_refl])
|
|
apply simp_all
|
|
done
|
|
qed
|
|
qed
|
|
qed
|
|
|
|
lemma is_aligned_no_wrap':
|
|
fixes ptr :: "'a::len word"
|
|
assumes al: "is_aligned ptr sz"
|
|
and off: "off < 2 ^ sz"
|
|
shows "ptr \<le> ptr + off"
|
|
by (subst no_plus_overflow_unat_size, subst word_size, rule is_aligned_no_wrap) fact+
|
|
|
|
lemma is_aligned_no_overflow':
|
|
fixes p :: "'a::len word"
|
|
assumes al: "is_aligned p n"
|
|
shows "p \<le> p + (2 ^ n - 1)"
|
|
proof cases
|
|
assume "n<len_of TYPE('a)"
|
|
with al
|
|
have "2^n - (1::'a::len word) < 2^n"
|
|
by (simp add: word_less_nat_alt unat_sub_if_size)
|
|
with al
|
|
show ?thesis by (rule is_aligned_no_wrap')
|
|
next
|
|
assume "\<not> n<len_of TYPE('a)"
|
|
with al
|
|
show ?thesis
|
|
by (simp add: not_less power_overflow is_aligned_mask mask_2pm1)
|
|
qed
|
|
|
|
lemma is_aligned_no_overflow:
|
|
"is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2^sz - 1"
|
|
by (drule is_aligned_no_overflow') (simp add: field_simps)
|
|
|
|
lemma replicate_not_True:
|
|
"\<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs"
|
|
by (induct xs) auto
|
|
|
|
lemma is_aligned_replicateI:
|
|
"to_bl p = addr @ replicate n False \<Longrightarrow> is_aligned (p::'a::len word) n"
|
|
apply (simp add: is_aligned_to_bl word_size)
|
|
apply (subgoal_tac "length addr = len_of TYPE('a) - n")
|
|
apply (simp add: replicate_not_True)
|
|
apply (drule arg_cong [where f=length])
|
|
apply simp
|
|
done
|
|
|
|
lemma to_bl_1: "to_bl (1::'a::len word) = replicate (len_of TYPE('a) - 1) False @ [True]"
|
|
proof -
|
|
have "to_bl (1 :: 'a::len word) = to_bl (mask 1 :: 'a::len word)"
|
|
by (simp add: mask_def)
|
|
|
|
also have "\<dots> = replicate (len_of TYPE('a) - 1) False @ [True]"
|
|
apply (subst to_bl_mask)
|
|
apply (clarsimp simp add: min_def)
|
|
apply (case_tac "len_of TYPE('a)", simp)
|
|
apply simp
|
|
done
|
|
|
|
finally show ?thesis .
|
|
qed
|
|
|
|
lemma to_bl_2p:
|
|
"n < len_of TYPE('a) \<Longrightarrow>
|
|
to_bl ((2::'a::len word) ^ n) =
|
|
replicate (len_of TYPE('a) - Suc n) False @ True # replicate n False"
|
|
apply (subst shiftl_1 [symmetric])
|
|
apply (subst bl_shiftl)
|
|
apply (simp add: to_bl_1 min_def word_size)
|
|
done
|
|
|
|
lemma map_zip_replicate_False_xor:
|
|
"n = length xs \<Longrightarrow> map (\<lambda>(x, y). x = (\<not> y)) (zip xs (replicate n False)) = xs"
|
|
by (induct xs arbitrary: n, auto)
|
|
|
|
lemma drop_minus_lem:
|
|
"\<lbrakk> n \<le> length xs; 0 < n; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs"
|
|
proof (induct xs arbitrary: n n')
|
|
case Nil thus ?case by simp
|
|
next
|
|
case (Cons y ys)
|
|
from Cons.prems
|
|
show ?case
|
|
apply simp
|
|
apply (cases "n = Suc (length ys)")
|
|
apply (simp add: nth_append)
|
|
apply (simp add: Suc_diff_le Cons.hyps nth_append)
|
|
apply clarsimp
|
|
apply arith
|
|
done
|
|
qed
|
|
|
|
lemma drop_minus:
|
|
"\<lbrakk> n < length xs; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n # drop (n' - n) xs"
|
|
apply (subst drop_minus_lem)
|
|
apply simp
|
|
apply simp
|
|
apply simp
|
|
apply simp
|
|
apply (cases "length xs", simp)
|
|
apply (simp add: Suc_diff_le)
|
|
done
|
|
|
|
lemma xor_2p_to_bl:
|
|
fixes x::"'a::len word"
|
|
shows "to_bl (x xor 2^n) =
|
|
(if n < len_of TYPE('a)
|
|
then take (len_of TYPE('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (len_of TYPE('a)-n) (to_bl x)
|
|
else to_bl x)"
|
|
proof -
|
|
have x: "to_bl x = take (len_of TYPE('a)-Suc n) (to_bl x) @ drop (len_of TYPE('a)-Suc n) (to_bl x)"
|
|
by simp
|
|
|
|
show ?thesis
|
|
apply simp
|
|
apply (rule conjI)
|
|
apply (clarsimp simp: word_size)
|
|
apply (simp add: bl_word_xor map2_def to_bl_2p)
|
|
apply (subst x)
|
|
apply (subst zip_append)
|
|
apply simp
|
|
apply (simp add: map_zip_replicate_False_xor drop_minus)
|
|
apply (auto simp add: word_size nth_w2p intro!: word_eqI)
|
|
done
|
|
qed
|
|
|
|
lemma aligned_add_xor:
|
|
assumes al: "is_aligned (x::'a::len word) n'" and le: "n < n'"
|
|
shows "(x + 2^n) xor 2^n = x"
|
|
proof cases
|
|
assume "n' < len_of TYPE('a)"
|
|
with assms show ?thesis
|
|
apply -
|
|
apply (rule word_bl.Rep_eqD)
|
|
apply (subst xor_2p_to_bl)
|
|
apply simp
|
|
apply (subst is_aligned_add_conv, simp,
|
|
simp add: word_less_nat_alt)+
|
|
apply (simp add: to_bl_2p nth_append)
|
|
apply (cases "n' = Suc n")
|
|
apply simp
|
|
apply (subst is_aligned_replicate [where n="Suc n",
|
|
simplified, symmetric])
|
|
apply assumption
|
|
apply simp
|
|
apply (rule refl)
|
|
apply (subgoal_tac "\<not> len_of TYPE('a) - Suc n \<le> len_of TYPE('a) - n'")
|
|
prefer 2
|
|
apply arith
|
|
apply (simp add: min_def)
|
|
apply (subst replicate_Suc [symmetric])
|
|
apply (subst replicate_add [symmetric])
|
|
apply simp
|
|
apply (simp add: is_aligned_replicate [simplified, symmetric])
|
|
done
|
|
next
|
|
assume "\<not> n' < len_of TYPE('a)"
|
|
with al show ?thesis
|
|
by (simp add: is_aligned_mask mask_def not_less power_overflow)
|
|
qed
|
|
|
|
lemma is_aligned_0 [simp]:
|
|
"is_aligned p 0"
|
|
by (simp add: is_aligned_def)
|
|
|
|
lemma is_aligned_replicateD:
|
|
"\<lbrakk> is_aligned (w::'a::len word) n; n \<le> len_of TYPE('a) \<rbrakk>
|
|
\<Longrightarrow> \<exists>xs. to_bl w = xs @ replicate n False
|
|
\<and> length xs = size w - n"
|
|
apply (subst is_aligned_replicate, assumption+)
|
|
apply (rule exI, rule conjI, rule refl)
|
|
apply (simp add: word_size)
|
|
done
|
|
|
|
lemma is_aligned_add_mult_multI:
|
|
fixes p :: "'a::len word"
|
|
shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n'"
|
|
apply (erule aligned_add_aligned)
|
|
apply (auto intro: is_alignedI [where k="x*z"])
|
|
done
|
|
|
|
lemma is_aligned_add_multI:
|
|
fixes p :: "'a::len word"
|
|
shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n'"
|
|
apply (erule aligned_add_aligned)
|
|
apply (auto intro: is_alignedI [where k="x"])
|
|
done
|
|
|
|
lemma unat_of_nat_len:
|
|
"x < 2 ^ len_of TYPE('a) \<Longrightarrow> unat (of_nat x :: 'a::len word) = x"
|
|
by (simp add: word_size unat_of_nat)
|
|
|
|
lemma is_aligned_no_wrap''':
|
|
fixes ptr :: "'a::len word"
|
|
shows"\<lbrakk> is_aligned ptr sz; sz < len_of TYPE('a); off < 2 ^ sz \<rbrakk>
|
|
\<Longrightarrow> unat ptr + off < 2 ^ len_of TYPE('a)"
|
|
apply (drule is_aligned_no_wrap[where off="of_nat off"])
|
|
apply (simp add: word_less_nat_alt)
|
|
apply (erule order_le_less_trans[rotated])
|
|
apply (subst unat_of_nat)
|
|
apply (rule mod_le_dividend)
|
|
apply (subst(asm) unat_of_nat_len)
|
|
apply (erule order_less_trans)
|
|
apply (erule power_strict_increasing)
|
|
apply simp
|
|
apply assumption
|
|
done
|
|
|
|
lemma is_aligned_get_word_bits:
|
|
fixes p :: "'a::len word"
|
|
shows "\<lbrakk> is_aligned p n; \<lbrakk> is_aligned p n; n < len_of TYPE('a) \<rbrakk> \<Longrightarrow> P;
|
|
\<lbrakk> p = 0; n \<ge> len_of TYPE('a) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
|
|
apply (cases "n < len_of TYPE('a)")
|
|
apply simp
|
|
apply simp
|
|
apply (erule meta_mp)
|
|
apply (clarsimp simp: is_aligned_mask mask_def power_add
|
|
power_overflow)
|
|
done
|
|
|
|
lemma rsubst:
|
|
"\<lbrakk> P s; s = t \<rbrakk> \<Longrightarrow> P t"
|
|
by simp
|
|
|
|
lemma aligned_small_is_0:
|
|
"\<lbrakk> is_aligned x n; x < 2 ^ n \<rbrakk> \<Longrightarrow> x = 0"
|
|
apply (erule is_aligned_get_word_bits)
|
|
apply (frule is_aligned_add_conv [rotated, where w=0])
|
|
apply (simp add: is_aligned_def)
|
|
apply simp
|
|
apply (drule is_aligned_replicateD)
|
|
apply simp
|
|
apply (clarsimp simp: word_size)
|
|
apply (subst (asm) replicate_add [symmetric])
|
|
apply (drule arg_cong[where f="of_bl :: bool list \<Rightarrow> 'a::len word"])
|
|
apply simp
|
|
apply (simp only: replicate.simps[symmetric, where x=False]
|
|
drop_replicate)
|
|
done
|
|
|
|
corollary is_aligned_less_sz:
|
|
"\<lbrakk>is_aligned a sz; a \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> a < 2 ^ sz"
|
|
by (rule notI, drule(1) aligned_small_is_0, erule(1) notE)
|
|
|
|
lemma aligned_at_least_t2n_diff:
|
|
"\<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n"
|
|
apply (erule is_aligned_get_word_bits[where p=y])
|
|
apply (rule ccontr)
|
|
apply (clarsimp simp: linorder_not_le)
|
|
apply (subgoal_tac "y - x = 0")
|
|
apply clarsimp
|
|
apply (rule aligned_small_is_0)
|
|
apply (erule(1) aligned_sub_aligned)
|
|
apply simp
|
|
apply unat_arith
|
|
apply simp
|
|
done
|
|
|
|
lemma word_sub_1_le:
|
|
"x \<noteq> 0 \<Longrightarrow> x - 1 \<le> (x :: ('a :: len) word)"
|
|
apply (subst no_ulen_sub)
|
|
apply simp
|
|
apply (cases "uint x = 0")
|
|
apply (simp add: uint_0_iff)
|
|
apply (insert uint_ge_0[where x=x])
|
|
apply arith
|
|
done
|
|
|
|
lemma is_aligned_no_overflow'':
|
|
"\<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n"
|
|
apply (frule is_aligned_no_overflow')
|
|
apply (erule order_trans)
|
|
apply (simp add: field_simps)
|
|
apply (erule word_sub_1_le)
|
|
done
|
|
|
|
lemma is_aligned_nth:
|
|
"is_aligned p m = (\<forall>n < m. \<not>p !! n)"
|
|
apply (clarsimp simp: is_aligned_mask bang_eq word_size)
|
|
apply (rule iffI)
|
|
apply clarsimp
|
|
apply (case_tac "n < size p")
|
|
apply (simp add: word_size)
|
|
apply (drule test_bit_size)
|
|
apply simp
|
|
apply clarsimp
|
|
done
|
|
|
|
lemma range_inter:
|
|
"({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not>(a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))"
|
|
by auto
|
|
|
|
lemma aligned_inter_non_empty:
|
|
"\<lbrakk> {p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {};
|
|
is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False"
|
|
apply (clarsimp simp only: range_inter)
|
|
apply (erule_tac x=p in allE)
|
|
apply simp
|
|
apply (erule impE)
|
|
apply (erule is_aligned_no_overflow')
|
|
apply (erule notE)
|
|
apply (erule is_aligned_no_overflow)
|
|
done
|
|
|
|
lemma not_aligned_mod_nz:
|
|
assumes al: "\<not> is_aligned a n"
|
|
shows "a mod 2 ^ n \<noteq> 0"
|
|
proof cases
|
|
assume "n < len_of TYPE('a)"
|
|
with al
|
|
show ?thesis
|
|
apply (simp add: is_aligned_def dvd_eq_mod_eq_0 word_arith_nat_mod)
|
|
apply (erule of_nat_neq_0)
|
|
apply (rule order_less_trans)
|
|
apply (rule mod_less_divisor)
|
|
apply simp
|
|
apply simp
|
|
done
|
|
next
|
|
assume "\<not> n < len_of TYPE('a)"
|
|
with al
|
|
show ?thesis
|
|
by (simp add: is_aligned_mask mask_def not_less power_overflow
|
|
word_less_nat_alt word_mod_by_0)
|
|
qed
|
|
|
|
lemma nat_add_offset_le:
|
|
fixes x :: nat
|
|
assumes yv: "y \<le> 2 ^ n"
|
|
and xv: "x < 2 ^ m"
|
|
and mn: "sz = m + n"
|
|
shows "x * 2 ^ n + y \<le> 2 ^ sz"
|
|
proof (subst mn)
|
|
from yv obtain qy where "y + qy = 2 ^ n"
|
|
by (auto simp: le_iff_add)
|
|
|
|
have "x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n"
|
|
using yv xv by simp
|
|
also have "\<dots> = (x + 1) * 2 ^ n" by simp
|
|
also have "\<dots> \<le> 2 ^ (m + n)" using xv
|
|
by (subst power_add) (rule mult_le_mono1, simp)
|
|
finally show "x * 2 ^ n + y \<le> 2 ^ (m + n)" .
|
|
qed
|
|
|
|
lemma is_aligned_no_wrap_le:
|
|
fixes ptr::"'a::len word"
|
|
assumes al: "is_aligned ptr sz"
|
|
and szv: "sz < len_of TYPE('a)"
|
|
and off: "off \<le> 2 ^ sz"
|
|
shows "unat ptr + off \<le> 2 ^ len_of TYPE('a)"
|
|
proof -
|
|
from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
|
|
qv: "q < 2 ^ (len_of TYPE('a) - sz)" by (auto elim: is_alignedE)
|
|
|
|
show ?thesis
|
|
proof (cases "sz = 0")
|
|
case True
|
|
thus ?thesis using off ptrq qv
|
|
apply (clarsimp)
|
|
apply (erule le_SucE)
|
|
apply (simp add: unat_of_nat)
|
|
apply (simp add: less_eq_Suc_le [symmetric] unat_of_nat)
|
|
done
|
|
next
|
|
case False
|
|
hence sne: "0 < sz" ..
|
|
|
|
show ?thesis
|
|
proof -
|
|
have uq: "unat (of_nat q :: 'a word) = q"
|
|
apply (subst unat_of_nat)
|
|
apply (rule mod_less)
|
|
apply (rule order_less_trans [OF qv])
|
|
apply (rule power_strict_increasing [OF diff_less [OF sne]])
|
|
apply simp_all
|
|
done
|
|
|
|
have uptr: "unat ptr = 2 ^ sz * q"
|
|
apply (subst ptrq)
|
|
apply (subst iffD1 [OF unat_mult_lem])
|
|
apply (subst unat_power_lower [OF szv])
|
|
apply (subst uq)
|
|
apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]])
|
|
apply (subst uq)
|
|
apply (subst unat_power_lower [OF szv])
|
|
apply simp
|
|
done
|
|
|
|
show "unat ptr + off \<le> 2 ^ len_of TYPE('a)" using szv
|
|
apply (subst uptr)
|
|
apply (subst mult.commute, rule nat_add_offset_le [OF off qv])
|
|
apply simp
|
|
done
|
|
qed
|
|
qed
|
|
qed
|
|
|
|
lemma is_aligned_neg_mask:
|
|
"m \<le> n \<Longrightarrow> is_aligned (x && ~~ mask n) m"
|
|
apply (simp add: and_not_mask)
|
|
apply (erule is_aligned_weaken[rotated])
|
|
apply (rule is_aligned_shift)
|
|
done
|
|
|
|
lemma unat_minus:
|
|
"unat (- (x :: ('a :: len) word))
|
|
= (if x = 0 then 0 else (2 ^ size x) - unat x)"
|
|
using unat_sub_if_size[where x="2 ^ size x" and y=x]
|
|
apply (simp add: unat_eq_0 word_size)
|
|
done
|
|
|
|
lemma is_aligned_minus:
|
|
"is_aligned p n \<Longrightarrow> is_aligned (- p) n"
|
|
apply (clarsimp simp: is_aligned_def unat_minus word_size word_neq_0_conv)
|
|
apply (rule dvd_diff_nat, simp_all)
|
|
apply (rule le_imp_power_dvd)
|
|
apply (fold is_aligned_def)
|
|
apply (erule_tac Q="0<p" in contrapos_pp)
|
|
apply (clarsimp simp add: is_aligned_mask mask_def power_overflow)
|
|
done
|
|
|
|
end
|