adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

isabelle2021-1: sync Word_Lib from afp 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-11-14 21:05:54 +11:00 committed by Gerwin Klein
parent 36135c5654
commit 1b15714cbf
45 changed files with 4943 additions and 3329 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

224
lib/Word_Lib/Aligned.thy
View File

@ -10,8 +10,11 @@ theory Aligned
imports
"HOL-Library.Word"
More_Word
Word_EqI
Typedef_Morphisms
Bit_Shifts_Infix_Syntax
begin
context
includes bit_operations_syntax
begin
lift_definition is_aligned :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
@ -185,11 +188,9 @@ proof cases
ultimately have upls: "unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)"
proof -
have f1: "unat x = 2 ^ (m + k) * q1"
by (metis (no_types) \<open>x = of_nat (2 ^ (m + k) * q1)\<close> l1 nat_mod_lem word_unat.inverse_norm
zero_less_numeral zero_less_power)
using q1v unat_mult_power_lem xv by blast
have "unat y = 2 ^ m * q2"
by (metis (no_types) \<open>y = of_nat (2 ^ m * q2)\<close> l2 nat_mod_lem word_unat.inverse_norm
zero_less_numeral zero_less_power)
using q2v unat_mult_power_lem yv by blast
then show ?thesis
using f1 by (simp add: power_add semiring_normalization_rules(34))
qed
@ -249,29 +250,26 @@ proof cases
from mv obtain q where mq: "m + q = LENGTH('a)" and "0 < q"
by (auto dest: less_imp_add_positive)
have "(2::nat) ^ m dvd unat (k << m)"
have "(2::nat) ^ m dvd unat (push_bit m k)"
proof
have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k"
by (rule div_mult_mod_eq)
have "unat (k << m) = unat (2 ^ m * k)" by (simp add: shiftl_t2n)
have "unat (push_bit m k) = unat (2 ^ m * k)"
by (simp add: push_bit_eq_mult ac_simps)
also have "\<dots> = (2 ^ m * unat k) mod (2 ^ LENGTH('a))" using mv
by (simp add: unat_word_ariths(2))
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)" .
finally show "unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)" .
qed
then show ?thesis by (unfold is_aligned_iff_dvd_nat)
then show ?thesis by (unfold is_aligned_iff_dvd_nat shiftl_def)
next
assume "\<not> m < LENGTH('a)"
then show ?thesis
by (simp add: not_less power_overflow is_aligned_mask shiftl_zero_size word_size)
by (simp add: not_less power_overflow is_aligned_mask word_size shiftl_def)
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"
@ -454,7 +452,7 @@ lemma is_aligned_no_wrap''':
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 (simp add: take_bit_eq_mod)
apply (simp add: take_bit_eq_mod unsigned_of_nat)
apply (subst(asm) unat_of_nat_len)
apply (erule order_less_trans)
apply (erule power_strict_increasing)
@ -505,16 +503,19 @@ lemma is_aligned_no_overflow'':
apply (erule word_sub_1_le)
done
lemma is_aligned_nth [word_eqI_simps]:
"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
lemma is_aligned_bitI:
\<open>is_aligned p m\<close> if \<open>\<And>n. n < m \<Longrightarrow> \<not> bit p n\<close>
apply (simp add: is_aligned_mask)
apply (rule bit_word_eqI)
using that
apply (auto simp add: bit_simps)
done
lemma is_aligned_nth:
"is_aligned p m = (\<forall>n < m. \<not> bit p n)"
apply (auto intro: is_aligned_bitI simp add: is_aligned_mask bit_eq_iff)
apply (auto simp: bit_simps)
using bit_imp_le_length not_less apply blast
done
lemma range_inter:
@ -612,7 +613,7 @@ qed
lemma is_aligned_neg_mask:
"m \<le> n \<Longrightarrow> is_aligned (x AND NOT (mask n)) m"
by (metis and_not_mask is_aligned_shift is_aligned_weaken)
by (rule is_aligned_bitI) (simp add: bit_simps)
lemma unat_minus:
"unat (- (x :: 'a :: len word)) = (if x = 0 then 0 else 2 ^ size x - unat x)"
@ -632,32 +633,32 @@ lemma is_aligned_minus:
lemma add_mask_lower_bits:
"\<lbrakk>is_aligned (x :: 'a :: len word) n;
\<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> p !! n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x"
\<forall>n' \<ge> n. n' < LENGTH('a) \<longrightarrow> \<not> bit p n'\<rbrakk> \<Longrightarrow> x + p AND NOT (mask n) = x"
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size is_aligned_nth)
apply (erule_tac x=na in allE)+
apply simp
apply (simp add: bit_simps)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps not_less test_bit_eq_bit)
apply (metis is_aligned_nth not_le test_bit_eq_bit)
apply (auto simp add: bit_simps not_less word_size)
apply (metis is_aligned_nth not_le)
done
lemma is_aligned_andI1:
"is_aligned x n \<Longrightarrow> is_aligned (x AND y) n"
by (simp add: is_aligned_nth)
by (simp add: is_aligned_nth bit_simps)
lemma is_aligned_andI2:
"is_aligned y n \<Longrightarrow> is_aligned (x AND y) n"
by (simp add: is_aligned_nth)
by (simp add: is_aligned_nth bit_simps)
lemma is_aligned_shiftl:
"is_aligned w (n - m) \<Longrightarrow> is_aligned (w << m) n"
by (simp add: is_aligned_nth nth_shiftl)
by (simp add: is_aligned_nth bit_simps)
lemma is_aligned_shiftr:
"is_aligned w (n + m) \<Longrightarrow> is_aligned (w >> m) n"
by (simp add: is_aligned_nth nth_shiftr)
by (simp add: is_aligned_nth bit_simps)
lemma is_aligned_shiftl_self:
"is_aligned (p << n) n"
@ -665,22 +666,28 @@ lemma is_aligned_shiftl_self:
lemma is_aligned_neg_mask_eq:
"is_aligned p n \<Longrightarrow> p AND NOT (mask n) = p"
by (metis add.left_neutral is_aligned_mask word_plus_and_or_coroll2)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps is_aligned_nth)
done
lemma is_aligned_shiftr_shiftl:
"is_aligned w n \<Longrightarrow> w >> n << n = w"
by (metis and_not_mask is_aligned_neg_mask_eq)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps is_aligned_nth intro: ccontr)
apply (subst add_diff_inverse_nat)
apply (auto intro: ccontr)
done
lemma aligned_shiftr_mask_shiftl:
"is_aligned x n \<Longrightarrow> ((x >> n) AND mask v) << n = x AND mask (v + n)"
apply (rule word_eqI)
apply (simp add: word_size nth_shiftl nth_shiftr)
apply (subgoal_tac "\<forall>m. x !! m \<longrightarrow> m \<ge> n")
apply (simp add: word_size bit_simps)
apply (subgoal_tac "\<forall>m. bit x m \<longrightarrow> m \<ge> n")
apply auto[1]
apply (clarsimp simp: is_aligned_mask)
apply (drule_tac x=m in word_eqD)
apply (frule test_bit_size)
apply (simp add: word_size)
apply (simp add: word_size bit_simps)
done
lemma mask_zero:
@ -715,7 +722,7 @@ lemma is_aligned_neg_mask_weaken:
lemma is_aligned_neg_mask2 [simp]:
"is_aligned (a AND NOT (mask n)) n"
by (simp add: and_not_mask is_aligned_shift)
by (rule is_aligned_bitI) (simp add: bit_simps)
lemma is_aligned_0':
"is_aligned 0 n"
@ -759,16 +766,12 @@ proof cases
by (rule aligned_add_offset_no_wrap) fact+
show ?thesis using al szv
apply -
apply (erule is_alignedE)
apply (subst word_unat.Rep_inject [symmetric])
apply (subst unat_mod)
apply (subst iffD1 [OF unat_add_lem], rule ux)
apply simp
apply (subst unat_mult_power_lem, assumption+)
apply (simp)
apply (rule mod_less[OF less_le_trans[OF unat_mono], OF kv])
apply (erule eq_imp_le[OF unat_power_lower])
apply (simp flip: take_bit_eq_mod)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps)
apply (metis assms(2) bit_or_iff is_aligned_mask is_aligned_nth leD less_mask_eq word_and_le1 word_bw_lcs(1) word_neq_0_conv word_plus_and_or_coroll)
apply (meson assms(2) leI less_2p_is_upper_bits_unset)
apply (metis assms(2) bit_disjunctive_add_iff bit_imp_le_length bit_push_bit_iff is_alignedE' less_2p_is_upper_bits_unset)
done
next
assume "\<not> sz < LENGTH('a)"
@ -868,14 +871,11 @@ lemma mask_out_add_aligned:
lemma is_aligned_add_or:
"\<lbrakk>is_aligned p n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p + d = p OR d"
apply (subst disjunctive_add)
apply (simp_all add: is_aligned_iff_take_bit_eq_0)
apply (simp add: bit_eq_iff)
apply (auto simp add: bit_simps)
apply (subst disjunctive_add, simp_all)
apply (clarsimp simp: is_aligned_nth less_2p_is_upper_bits_unset)
subgoal for m
apply (cases \<open>m < n\<close>)
apply (auto simp add: not_less)
apply (metis bit_take_bit_iff less_mask_eq take_bit_eq_mask)
apply (auto simp add: not_less dest: bit_imp_possible_bit)
done
done
@ -921,10 +921,29 @@ lemma and_neg_mask_eq_iff_not_mask_le:
for w :: \<open>'a::len word\<close>
by (metis eq_iff neg_mask_mono_le word_and_le1 word_and_le2 word_bw_same(1))
lemma neg_mask_le_high_bits [word_eqI_simps]:
"NOT(mask n) \<le> w \<longleftrightarrow> (\<forall>i \<in> {n ..< size w}. w !! i)"
lemma neg_mask_le_high_bits:
\<open>NOT (mask n) \<le> w \<longleftrightarrow> (\<forall>i \<in> {n ..< size w}. bit w i)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
for w :: \<open>'a::len word\<close>
by (auto simp: word_size and_neg_mask_eq_iff_not_mask_le[symmetric] word_eq_iff neg_mask_test_bit)
proof
assume ?Q
then have \<open>w AND NOT (mask n) = NOT (mask n)\<close>
by (auto simp add: bit_simps word_size intro: bit_word_eqI)
then show ?P
by (simp add: and_neg_mask_eq_iff_not_mask_le)
next
assume ?P
then have *: \<open>w AND NOT (mask n) = NOT (mask n)\<close>
by (simp add: and_neg_mask_eq_iff_not_mask_le)
show \<open>?Q\<close>
proof (rule ccontr)
assume \<open>\<not> (\<forall>i\<in>{n..<size w}. bit w i)\<close>
then obtain m where m: \<open>\<not> bit w m\<close> \<open>n \<le> m\<close> \<open>m < LENGTH('a)\<close>
by (auto simp add: word_size)
from * have \<open>bit (w AND NOT (mask n)) m \<longleftrightarrow> bit (NOT (mask n :: 'a word)) m\<close>
by auto
with m show False by (auto simp add: bit_simps)
qed
qed
lemma is_aligned_add_less_t2n:
"\<lbrakk>is_aligned (p::'a::len word) n; d < 2^n; n \<le> m; p < 2^m\<rbrakk> \<Longrightarrow> p + d < 2^m"
@ -1016,8 +1035,6 @@ lemma aligned_less_plus_1:
apply (clarsimp simp: field_simps)
apply (drule arg_cong[where f="\<lambda>x. x - 1"])
apply (clarsimp simp: is_aligned_mask)
apply (drule word_eqD[where x=0])
apply simp
done
lemma aligned_add_offset_less:
@ -1134,12 +1151,12 @@ proof -
by (rule diff_less, simp)
ultimately show "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (LENGTH('a) - s1)"
using take_bit_nat_less_self_iff [of \<open>LENGTH('a)\<close> \<open>mq - 2 ^ sq * nq\<close>]
apply (auto simp add: word_less_nat_alt not_le not_less)
apply (auto simp add: word_less_nat_alt not_le not_less unsigned_of_nat)
apply (metis take_bit_nat_eq_self_iff)
done
qed
then have "mq - 2 ^ sq * nq < 2 ^ (s2 - s1)" using mq s2wb
apply (simp add: word_less_nat_alt take_bit_eq_mod)
apply (simp add: word_less_nat_alt take_bit_eq_mod unsigned_of_nat)
apply (subst (asm) mod_less)
apply auto
apply (rule order_le_less_trans)
@ -1181,20 +1198,20 @@ lemma is_aligned_add:
lemma aligned_shift:
"\<lbrakk>x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \<le> LENGTH('a)\<rbrakk>
\<Longrightarrow> x + y >> n = y >> n"
\<Longrightarrow> (x + y) >> n = y >> n"
apply (subst word_plus_and_or_coroll; rule bit_word_eqI)
apply (auto simp add: bit_simps is_aligned_nth test_bit_eq_bit)
apply (metis less_2p_is_upper_bits_unset not_le test_bit_word_eq)
apply (metis le_add1 less_2p_is_upper_bits_unset test_bit_bin test_bit_word_eq)
apply (auto simp add: bit_simps is_aligned_nth)
apply (metis less_2p_is_upper_bits_unset not_le)
apply (metis le_add1 less_2p_is_upper_bits_unset test_bit_bin)
done
lemma aligned_shift':
"\<lbrakk>x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \<le> LENGTH('a)\<rbrakk>
\<Longrightarrow> y + x >> n = y >> n"
\<Longrightarrow> (y + x) >> n = y >> n"
apply (subst word_plus_and_or_coroll; rule bit_word_eqI)
apply (auto simp add: bit_simps is_aligned_nth test_bit_eq_bit)
apply (metis less_2p_is_upper_bits_unset not_le test_bit_eq_bit)
apply (metis bit_imp_le_length le_add1 less_2p_is_upper_bits_unset test_bit_eq_bit)
apply (auto simp add: bit_simps is_aligned_nth)
apply (metis less_2p_is_upper_bits_unset not_le)
apply (metis bit_imp_le_length le_add1 less_2p_is_upper_bits_unset)
done
lemma and_neg_mask_plus_mask_mono: "(p AND NOT (mask n)) + mask n \<ge> p"
@ -1242,4 +1259,67 @@ lemma and_mask_plus:
apply (simp add:word_bw_comms word_bw_lcs)
done
lemma is_aligned_add_not_aligned:
"\<lbrakk>is_aligned (p::'a::len word) n; \<not> is_aligned (q::'a::len word) n\<rbrakk> \<Longrightarrow> \<not> is_aligned (p + q) n"
by (metis is_aligned_addD1)
lemma neg_mask_add_aligned:
"\<lbrakk> is_aligned p n; q < 2 ^ n \<rbrakk> \<Longrightarrow> (p + q) AND NOT (mask n) = p AND NOT (mask n)"
by (metis is_aligned_add_helper is_aligned_neg_mask_eq)
lemma word_add_power_off:
fixes a :: "'a :: len word"
assumes ak: "a < k"
and kw: "k < 2 ^ (LENGTH('a) - m)"
and mw: "m < LENGTH('a)"
and off: "off < 2 ^ m"
shows "(a * 2 ^ m) + off < k * 2 ^ m"
proof (cases "m = 0")
case True
then show ?thesis using off ak by simp
next
case False
from ak have ak1: "a + 1 \<le> k" by (rule inc_le)
then have "(a + 1) * 2 ^ m \<noteq> 0"
apply -
apply (rule word_power_nonzero)
apply (erule order_le_less_trans [OF _ kw])
apply (rule mw)
apply (rule less_is_non_zero_p1 [OF ak])
done
then have "(a * 2 ^ m) + off < ((a + 1) * 2 ^ m)" using kw mw
apply -
apply (simp add: distrib_right)
apply (rule word_plus_strict_mono_right [OF off])
apply (rule is_aligned_no_overflow'')
apply (rule is_aligned_mult_triv2)
apply assumption
done
also have "\<dots> \<le> k * 2 ^ m" using ak1 mw kw False
apply -
apply (erule word_mult_le_mono1)
apply (simp add: p2_gt_0)
apply (simp add: word_less_nat_alt)
apply (meson nat_mult_power_less_eq zero_less_numeral)
done
finally show ?thesis .
qed
lemma offset_not_aligned:
"\<lbrakk> is_aligned (p::'a::len word) n; i > 0; i < 2 ^ n; n < LENGTH('a)\<rbrakk> \<Longrightarrow>
\<not> is_aligned (p + of_nat i) n"
apply (erule is_aligned_add_not_aligned)
apply transfer
apply (auto simp add: is_aligned_iff_udvd)
apply (metis (no_types, lifting) le_less_trans less_not_refl2 less_or_eq_imp_le of_nat_eq_0_iff take_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_of_nat unat_lt2p unat_power_lower)
done
lemma le_or_mask:
"w \<le> w' \<Longrightarrow> w OR mask x \<le> w' OR mask x"
for w w' :: \<open>'a::len word\<close>
by (metis neg_mask_add_mask add.commute le_word_or1 mask_2pm1 neg_mask_mono_le word_plus_mono_left)
end
end

18
lib/Word_Lib/Ancient_Numeral.thy
View File

@ -5,7 +5,7 @@
*)
theory Ancient_Numeral
imports Main Reversed_Bit_Lists
imports Main Reversed_Bit_Lists Legacy_Aliases
begin
definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
@ -188,6 +188,10 @@ lemma sbintrunc_Suc_minus_Is:
lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
by (auto simp add: Bit_def concat_bit_Suc)
context
includes bit_operations_syntax
begin
lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
by (simp add: not_int_def Bit_def)
@ -200,6 +204,8 @@ lemma int_or_Bits [simp]: "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
lemma int_xor_Bits [simp]: "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
using xor_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
end
lemma mod_BIT:
"bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit" for bit
proof -
@ -221,13 +227,9 @@ lemma int_lsb_BIT [simp]: fixes x :: int shows
by(simp add: lsb_int_def)
lemma int_shiftr_BIT [simp]: fixes x :: int
shows int_shiftr0: "x >> 0 = x"
and int_shiftr_Suc: "x BIT b >> Suc n = x >> n"
proof -
show "x >> 0 = x" by (simp add: shiftr_int_def)
show "x BIT b >> Suc n = x >> n" by (cases b)
(simp_all add: shiftr_int_def Bit_def add.commute pos_zdiv_mult_2)
qed
shows int_shiftr0: "drop_bit 0 x = x"
and int_shiftr_Suc: "drop_bit (Suc n) (x BIT b) = drop_bit n x"
by (simp_all add: drop_bit_Suc)
lemma msb_BIT [simp]: "msb (x BIT b) = msb x"
by(simp add: msb_int_def)

7
lib/Word_Lib/Bit_Comprehension.thy
View File

@ -7,7 +7,8 @@
section \<open>Comprehension syntax for bit expressions\<close>
theory Bit_Comprehension
imports "HOL-Library.Word"
imports
"HOL-Library.Word"
begin
class bit_comprehension = ring_bit_operations +
@ -72,7 +73,7 @@ instance by standard
end
lemma bit_set_bits_word_iff:
lemma bit_set_bits_word_iff [bit_simps]:
\<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close>
by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)
@ -100,7 +101,7 @@ proof (cases \<open>\<exists>n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n\
then have n: \<open>\<And>m. n \<le> m \<Longrightarrow> f m \<longleftrightarrow> f n\<close>
by blast
from n_def have n_eq: \<open>(LEAST q. \<forall>m\<ge>q. f m \<longleftrightarrow> f n) = n\<close>
by (smt Least_equality Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.refl le_refl n order_refl)
by (smt (verit, best) Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.antisym wellorder_Least_lemma(1))
show ?thesis
proof (cases \<open>f n\<close>)
case False

201
lib/Word_Lib/Bit_Shifts_Infix_Syntax.thy Normal file
View File

@ -0,0 +1,201 @@
(*
* Copyright Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
(* Author: Jeremy Dawson, NICTA *)
section \<open>Shift operations with infix syntax\<close>
theory Bit_Shifts_Infix_Syntax
imports "HOL-Library.Word" More_Word
begin
context semiring_bit_operations
begin
definition shiftl :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close> (infixl "<<" 55)
where [code_unfold]: \<open>a << n = push_bit n a\<close>
lemma bit_shiftl_iff [bit_simps]:
\<open>bit (a << m) n \<longleftrightarrow> m \<le> n \<and> possible_bit TYPE('a) n \<and> bit a (n - m)\<close>
by (simp add: shiftl_def bit_simps)
definition shiftr :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close> (infixl ">>" 55)
where [code_unfold]: \<open>a >> n = drop_bit n a\<close>
lemma bit_shiftr_eq [bit_simps]:
\<open>bit (a >> n) = bit a \<circ> (+) n\<close>
by (simp add: shiftr_def bit_simps)
end
definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> (infixl \<open>>>>\<close> 55)
where [code_unfold]: \<open>w >>> n = signed_drop_bit n w\<close>
lemma bit_sshiftr_iff [bit_simps]:
\<open>bit (w >>> m) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
for w :: \<open>'a::len word\<close>
by (simp add: sshiftr_def bit_simps)
context
includes lifting_syntax
begin
lemma shiftl_word_transfer [transfer_rule]:
\<open>(pcr_word ===> (=) ===> pcr_word) (\<lambda>k n. push_bit n k) (<<)\<close>
apply (unfold shiftl_def)
apply transfer_prover
done
lemma shiftr_word_transfer [transfer_rule]:
\<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
(\<lambda>k n. drop_bit n (take_bit LENGTH('a) k))
(>>)\<close>
proof -
have \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
(\<lambda>k n. (drop_bit n \<circ> take_bit LENGTH('a)) k)
(>>)\<close>
by (unfold shiftr_def) transfer_prover
then show ?thesis
by simp
qed
lemma sshiftr_transfer [transfer_rule]:
\<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
(\<lambda>k n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))
(>>>)\<close>
proof -
have \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> _) ===> (=) ===> pcr_word)
(\<lambda>k n. (drop_bit n \<circ> signed_take_bit (LENGTH('a) - Suc 0)) k)
(>>>)\<close>
by (unfold sshiftr_def) transfer_prover
then show ?thesis
by simp
qed
end
context semiring_bit_operations
begin
lemma shiftl_0 [simp]:
\<open>0 << n = 0\<close>
by (simp add: shiftl_def)
lemma shiftl_of_0 [simp]:
\<open>a << 0 = a\<close>
by (simp add: shiftl_def)
lemma shiftl_of_Suc [simp]:
\<open>a << Suc n = (a * 2) << n\<close>
by (simp add: shiftl_def)
lemma shiftl_1 [simp]:
\<open>1 << n = 2 ^ n\<close>
by (simp add: shiftl_def)
lemma shiftl_numeral_Suc [simp]:
\<open>numeral m << Suc n = push_bit (Suc n) (numeral m)\<close>
by (fact shiftl_def)
lemma shiftl_numeral_numeral [simp]:
\<open>numeral m << numeral n = push_bit (numeral n) (numeral m)\<close>
by (fact shiftl_def)
lemma shiftr_0 [simp]:
\<open>0 >> n = 0\<close>
by (simp add: shiftr_def)
lemma shiftr_of_0 [simp]:
\<open>a >> 0 = a\<close>
by (simp add: shiftr_def)
lemma shiftr_1 [simp]:
\<open>1 >> n = of_bool (n = 0)\<close>
by (simp add: shiftr_def)
lemma shiftr_numeral_Suc [simp]:
\<open>numeral m >> Suc n = drop_bit (Suc n) (numeral m)\<close>
by (fact shiftr_def)
lemma shiftr_numeral_numeral [simp]:
\<open>numeral m >> numeral n = drop_bit (numeral n) (numeral m)\<close>
by (fact shiftr_def)
end
context ring_bit_operations
begin
context
includes bit_operations_syntax
begin
lemma shiftl_minus_1_numeral [simp]:
\<open>- 1 << numeral n = NOT (mask (numeral n))\<close>
by (simp add: shiftl_def)
end
end
lemma shiftl_Suc_0 [simp]:
\<open>Suc 0 << n = 2 ^ n\<close>
by (simp add: shiftl_def)
lemma shiftr_Suc_0 [simp]:
\<open>Suc 0 >> n = of_bool (n = 0)\<close>
by (simp add: shiftr_def)
lemma sshiftr_numeral_Suc [simp]:
\<open>numeral m >>> Suc n = signed_drop_bit (Suc n) (numeral m)\<close>
by (fact sshiftr_def)
lemma sshiftr_numeral_numeral [simp]:
\<open>numeral m >>> numeral n = signed_drop_bit (numeral n) (numeral m)\<close>
by (fact sshiftr_def)
context ring_bit_operations
begin
lemma shiftl_minus_numeral_Suc [simp]:
\<open>- numeral m << Suc n = push_bit (Suc n) (- numeral m)\<close>
by (fact shiftl_def)
lemma shiftl_minus_numeral_numeral [simp]:
\<open>- numeral m << numeral n = push_bit (numeral n) (- numeral m)\<close>
by (fact shiftl_def)
lemma shiftr_minus_numeral_Suc [simp]:
\<open>- numeral m >> Suc n = drop_bit (Suc n) (- numeral m)\<close>
by (fact shiftr_def)
lemma shiftr_minus_numeral_numeral [simp]:
\<open>- numeral m >> numeral n = drop_bit (numeral n) (- numeral m)\<close>
by (fact shiftr_def)
end
lemma sshiftr_0 [simp]:
\<open>0 >>> n = 0\<close>
by (simp add: sshiftr_def)
lemma sshiftr_of_0 [simp]:
\<open>w >>> 0 = w\<close>
by (simp add: sshiftr_def)
lemma sshiftr_1 [simp]:
\<open>(1 :: 'a::len word) >>> n = of_bool (LENGTH('a) = 1 \<or> n = 0)\<close>
by (simp add: sshiftr_def)
lemma sshiftr_minus_numeral_Suc [simp]:
\<open>- numeral m >>> Suc n = signed_drop_bit (Suc n) (- numeral m)\<close>
by (fact sshiftr_def)
lemma sshiftr_minus_numeral_numeral [simp]:
\<open>- numeral m >>> numeral n = signed_drop_bit (numeral n) (- numeral m)\<close>
by (fact sshiftr_def)
end

712
lib/Word_Lib/Bits_Int.thy
View File

File diff suppressed because it is too large Load Diff

33
lib/Word_Lib/Bitwise.thy
View File

@ -9,6 +9,7 @@ theory Bitwise
"HOL-Library.Word"
More_Arithmetic
Reversed_Bit_Lists
Bit_Shifts_Infix_Syntax
begin
text \<open>Helper constants used in defining addition\<close>
@ -101,7 +102,7 @@ lemma rbl_succ2_simps:
"rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
by (simp_all add: rbl_succ2_def)
lemma twos_complement: "- x = word_succ (NOT x)"
lemma twos_complement: "- x = word_succ (not x)"
using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
@ -165,22 +166,22 @@ lemma rbl_sshiftr:
drop_nonempty_def take_Cons')
apply (case_tac "LENGTH('a)", simp_all)
apply (rule word_eqI)
apply (simp add: nth_sshiftr word_size test_bit_of_bl
apply (simp add: bit_simps word_size test_bit_of_bl
msb_nth)
done
lemma nth_word_of_int:
"(word_of_int x :: 'a::len word) !! n = (n < LENGTH('a) \<and> bin_nth x n)"
"bit (word_of_int x :: 'a::len word) n = (n < LENGTH('a) \<and> bit x n)"
apply (simp add: test_bit_bl word_size to_bl_of_bin)
apply (subst conj_cong[OF refl], erule bin_nth_bl)
apply auto
done
lemma nth_scast:
"(scast (x :: 'a::len word) :: 'b::len word) !! n =
"bit (scast (x :: 'a::len word) :: 'b::len word) n =
(n < LENGTH('b) \<and>
(if n < LENGTH('a) - 1 then x !! n
else x !! (LENGTH('a) - 1)))"
(if n < LENGTH('a) - 1 then bit x n
else bit x (LENGTH('a) - 1)))"
apply transfer
apply (auto simp add: bit_signed_take_bit_iff min_def)
done
@ -235,7 +236,7 @@ next
by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
by (simp add: shiftl_t2n)
by (simp add: push_bit_eq_mult shiftl_def)
have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys"
by (rule nth_equalityI) simp_all
@ -244,7 +245,10 @@ next
apply (simp add: trans [OF of_bl_append add.commute]
rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl)
apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def)
apply (simp add: rbl_plus_def zip_take_triv)
apply (simp add: rbl_plus_def)
apply (simp add: zip_take_triv)
apply (simp only: mult.commute [of _ 2] to_bl_double_eq)
apply (simp flip: butlast_rev add: take_butlast)
done
qed
@ -349,13 +353,10 @@ lemma rev_bin_to_bl_simps:
False # rev (bin_to_bl n (- numeral num.One))"
by (simp_all add: bin_to_bl_aux_append bin_to_bl_zero_aux bin_to_bl_minus1_aux replicate_append_same)
lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])"
apply (rule nth_equalityI)
apply (simp add: word_size)
apply (auto simp: to_bl_nth word_size rev_nth)
done
lemma to_bl_upt: "to_bl x = rev (map (bit x) [0 ..< size x])"
by (simp add: to_bl_eq_rev word_size rev_map)
lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]"
lemma rev_to_bl_upt: "rev (to_bl x) = map (bit x) [0 ..< size x]"
by (simp add: to_bl_upt)
lemma upt_eq_list_intros:
@ -383,7 +384,7 @@ fun mk_nat_clist ns =
fun upt_conv ctxt ct =
case Thm.term_of ct of
(\<^const>\<open>upt\<close> $ n $ m) =>
\<^Const_>\<open>upt for n m\<close> =>
let
val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1))
@ -405,7 +406,7 @@ val expand_upt_simproc =
fun word_len_simproc_fn ctxt ct =
(case Thm.term_of ct of
Const (\<^const_name>\<open>len_of\<close>, _) $ t =>
\<^Const_>\<open>len_of _ for t\<close> =>
(let
val T = fastype_of t |> dest_Type |> snd |> the_single
val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T);

33
lib/Word_Lib/Enumeration_Word.thy
View File

@ -63,7 +63,7 @@ lemma minBound_word:
by (simp add: minBound_def enum_word_def upt_conv_Cons)
lemma maxBound_max_word:
"(maxBound::'a::len word) = max_word"
"(maxBound::'a::len word) = - 1"
by (fact maxBound_word)
lemma leq_maxBound [simp]:
@ -295,4 +295,35 @@ lemma enum_word_div:
apply simp
done
lemma remdups_enum_upto:
fixes s::"'a::len word"
shows "remdups [s .e. e] = [s .e. e]"
by simp
lemma card_enum_upto:
fixes s::"'a::len word"
shows "card (set [s .e. e]) = Suc (unat e) - unat s"
by (subst List.card_set) (simp add: remdups_enum_upto)
lemma length_upto_enum_one:
fixes x :: "'a :: len word"
assumes lt1: "x < y" and lt2: "z < y" and lt3: "x \<le> z"
shows "[x , y .e. z] = [x]"
unfolding upto_enum_step_def
proof (subst upto_enum_red, subst if_not_P [OF leD [OF lt3]], clarsimp, rule conjI)
show "unat ((z - x) div (y - x)) = 0"
proof (subst unat_div, rule div_less)
have syx: "unat (y - x) = unat y - unat x"
by (rule unat_sub [OF order_less_imp_le]) fact
moreover have "unat (z - x) = unat z - unat x"
by (rule unat_sub) fact
ultimately show "unat (z - x) < unat (y - x)"
using lt2 lt3 unat_mono word_less_minus_mono_left by blast
qed
then show "(z - x) div (y - x) * (y - x) = 0"
by (simp add: unat_div) (simp add: word_arith_nat_defs(6))
qed
end

1048
lib/Word_Lib/Examples.thy
View File

File diff suppressed because it is too large Load Diff

130
lib/Word_Lib/Generic_set_bit.thy
View File

@ -11,16 +11,17 @@ section \<open>Operation variant for setting and unsetting bits\<close>
theory Generic_set_bit
imports
"HOL-Library.Word"
Bits_Int
Most_significant_bit
begin
class set_bit = semiring_bits +
fixes set_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a\<close>
assumes bit_set_bit_iff [bit_simps]:
assumes bit_set_bit_iff_2n:
\<open>bit (set_bit a m b) n \<longleftrightarrow>
(if m = n then b else bit a n) \<and> 2 ^ n \<noteq> 0\<close>
lemmas bit_set_bit_iff[bit_simps] = bit_set_bit_iff_2n[simplified fold_possible_bit simp_thms]
lemma set_bit_eq:
\<open>set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\<close>
for a :: \<open>'a::{ring_bit_operations, set_bit}\<close>
@ -30,88 +31,43 @@ instantiation int :: set_bit
begin
definition set_bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> int\<close>
where \<open>set_bit i n b = bin_sc n b i\<close>
where \<open>set_bit_int i n b = (if b then Bit_Operations.set_bit else Bit_Operations.unset_bit) n i\<close>
instance
by standard
(simp_all add: set_bit_int_def bin_nth_sc_gen bit_simps)
by standard (simp_all add: set_bit_int_def bit_simps)
end
lemma int_set_bit_0 [simp]: fixes x :: int shows
"set_bit x 0 b = of_bool b + 2 * (x div 2)"
by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
lemma int_set_bit_Suc: fixes x :: int shows
"set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b"
by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
lemma bin_last_set_bit:
"bin_last (set_bit x n b) = (if n > 0 then bin_last x else b)"
by (cases n) (simp_all add: int_set_bit_Suc)
lemma bin_rest_set_bit:
"bin_rest (set_bit x n b) = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)"
by (cases n) (simp_all add: int_set_bit_Suc)
lemma int_set_bit_numeral: fixes x :: int shows
"set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b"
by (simp add: set_bit_int_def)
lemmas int_set_bit_numerals [simp] =
int_set_bit_numeral[where x="numeral w'"]
int_set_bit_numeral[where x="- numeral w'"]
int_set_bit_numeral[where x="Numeral1"]
int_set_bit_numeral[where x="1"]
int_set_bit_numeral[where x="0"]
int_set_bit_Suc[where x="numeral w'"]
int_set_bit_Suc[where x="- numeral w'"]
int_set_bit_Suc[where x="Numeral1"]
int_set_bit_Suc[where x="1"]
int_set_bit_Suc[where x="0"]
for w'
lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) \<longleftrightarrow> msb x"
by(simp add: msb_conv_bin_sign set_bit_int_def)
instantiation word :: (len) set_bit
begin
definition set_bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a word\<close>
where word_set_bit_def: \<open>set_bit a n x = word_of_int (bin_sc n x (uint a))\<close>
where set_bit_unfold: \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
for w :: \<open>'a::len word\<close>
instance
by standard
(auto simp add: word_set_bit_def bin_nth_sc_gen bit_simps)
by standard (auto simp add: set_bit_unfold bit_simps dest: bit_imp_le_length)
end
lemma set_bit_unfold:
\<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
for w :: \<open>'a::len word\<close>
by (simp add: set_bit_eq)
lemma bit_set_bit_word_iff [bit_simps]:
\<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
for w :: \<open>'a::len word\<close>
by (auto simp add: bit_simps dest: bit_imp_le_length)
lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
for w :: "'a::len word"
by (auto simp: word_test_bit_def word_set_bit_def)
lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
for w :: "'a::len word"
by (auto simp: word_size word_test_bit_def word_set_bit_def nth_bintr)
lemma test_bit_set_gen:
"test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
"bit (set_bit w n x) m \<longleftrightarrow> (if m = n then n < size w \<and> x else bit w m)"
for w :: "'a::len word"
apply (unfold word_size word_test_bit_def word_set_bit_def)
apply (clarsimp simp add: nth_bintr bin_nth_sc_gen)
apply (auto elim!: test_bit_size [unfolded word_size]
simp add: word_test_bit_def [symmetric])
done
by (simp add: bit_set_bit_word_iff word_size)
lemma test_bit_set:
"bit (set_bit w n x) n \<longleftrightarrow> n < size w \<and> x"
for w :: "'a::len word"
by (auto simp add: bit_simps word_size)
lemma word_set_nth: "set_bit w n (bit w n) = w"
for w :: "'a::len word"
by (rule bit_word_eqI) (simp add: bit_simps)
lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
for w :: "'a::len word"
@ -123,27 +79,7 @@ lemma word_set_set_diff:
shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
unfolding word_set_bit_def
by (rule word_eqI)(simp add: word_size bin_nth_sc_gen nth_bintr)
lemma word_set_numeral [simp]:
"set_bit (numeral bin::'a::len word) n b =
word_of_int (bin_sc n b (numeral bin))"
unfolding word_numeral_alt by (rule set_bit_word_of_int)
lemma word_set_neg_numeral [simp]:
"set_bit (- numeral bin::'a::len word) n b =
word_of_int (bin_sc n b (- numeral bin))"
unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
unfolding word_0_wi by (rule set_bit_word_of_int)
lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
unfolding word_1_wi by (rule set_bit_word_of_int)
lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> bit w n = b \<or> n \<ge> size w"
for w :: "'a::len word"
apply (rule iffI)
apply (rule disjCI)
@ -153,38 +89,36 @@ lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or
apply (erule disjE)
apply clarsimp
apply (rule word_eqI)
apply (clarsimp simp add : test_bit_set_gen)
apply (drule test_bit_size)
apply force
apply (clarsimp simp add : test_bit_set_gen)
apply (auto simp add: word_size)
apply (rule bit_eqI)
apply (simp add: bit_simps)
done
lemma word_clr_le: "w \<ge> set_bit w n False"
for w :: "'a::len word"
apply (simp add: word_set_bit_def word_le_def)
apply (simp add: set_bit_unfold)
apply transfer
apply (rule order_trans)
apply (rule bintr_bin_clr_le)
apply simp
apply (simp add: take_bit_unset_bit_eq unset_bit_less_eq)
done
lemma word_set_ge: "w \<le> set_bit w n True"
for w :: "'a::len word"
apply (simp add: word_set_bit_def word_le_def)
apply (simp add: set_bit_unfold)
apply transfer
apply (rule order_trans [OF _ bintr_bin_set_ge])
apply simp
apply (simp add: take_bit_set_bit_eq set_bit_greater_eq)
done
lemma set_bit_beyond:
"size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word"
by (auto intro: word_eqI simp add: test_bit_set_gen word_size)
by (simp add: word_set_nth_iff)
lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n"
apply (rule word_eqI)
apply (auto simp add: test_bit_set_gen nth_shiftl word_size
simp del: word_set_bit_0 shiftl_1)
apply (auto simp add: word_size bit_simps)
done
lemmas one_bit_pow = trans [OF one_bit_shiftl shiftl_1]
lemma one_bit_pow: "set_bit 0 n True = (2 :: 'a :: len word) ^ n"
by (simp add: one_bit_shiftl shiftl_def)
end

114
lib/Word_Lib/Guide.thy
View File

@ -6,15 +6,28 @@
(*<*)
theory Guide
imports Word_Lib_Sumo Word_64
imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64 Ancient_Numeral
begin
context semiring_bit_operations
begin
lemma bit_eq_iff:
\<open>a = b \<longleftrightarrow> (\<forall>n. 2 ^ n \<noteq> 0 \<longrightarrow> bit a n \<longleftrightarrow> bit b n)\<close>
using bit_eq_iff [of a b] by (simp add: possible_bit_def)
end
notation (output) Generic_set_bit.set_bit (\<open>Generic'_set'_bit.set'_bit\<close>)
hide_const (open) Generic_set_bit.set_bit
no_notation bit (infixl \<open>!!\<close> 100)
(*>*)
section \<open>A short overview over bit operations and word types\<close>
subsection \<open>Basic theories and key ideas\<close>
subsection \<open>Key principles\<close>
text \<open>
When formalizing bit operations, it is tempting to represent
@ -33,7 +46,7 @@ text \<open>
in @{term [source] 0} which can be represented by type \<^typ>\<open>nat\<close> but
only support a restricted set of operations).
The most fundamental ideas are developed in theory \<^theory>\<open>HOL.Parity\<close>
The fundamental principles are developed in theory \<^theory>\<open>HOL.Bit_Operations\<close>
(which is part of \<^theory>\<open>Main\<close>):
\<^item> Multiplication by \<^term>\<open>2 :: int\<close> is a bit shift to the left and
@ -53,11 +66,10 @@ text \<open>
\<^item> Induction rule: @{thm [display, mode=iff] bits_induct [where ?'a = int, no_vars]}
\<^item> Characteristic properties \<^prop>\<open>bit (f x) n \<longleftrightarrow> P x n\<close>
\<^item> Characteristic properties @{prop [source] \<open>bit (f x) n \<longleftrightarrow> P x n\<close>}
are available in fact collection \<^text>\<open>bit_simps\<close>.
On top of this, the following generic operations are provided
after import of theory \<^theory>\<open>HOL-Library.Bit_Operations\<close>:
On top of this, the following generic operations are provided:
\<^item> Singleton \<^term>\<open>n\<close>th bit: \<^term>\<open>(2 :: int) ^ n\<close>
@ -69,19 +81,19 @@ text \<open>
\<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]}
\<^item> Negation: @{thm [mode=iff] bit_not_iff [where ?'a = int, no_vars]}
\<^item> Bitwise negation: @{thm [mode=iff] bit_not_iff_eq [where ?'a = int, no_vars]}
\<^item> And: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]}
\<^item> Bitwise conjunction: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]}
\<^item> Or: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]}
\<^item> Bitwise disjunction: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]}
\<^item> Xor: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]}
\<^item> Bitwise exclusive disjunction: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]}
\<^item> Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]}
\<^item> Setting a single bit: @{thm set_bit_def [where ?'a = int, no_vars]}
\<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}
\<^item> Unsetting a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}
\<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
\<^item> Flipping a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}
\<^item> Signed truncation, or modulus centered around \<^term>\<open>0::int\<close>:
@{thm [display] signed_take_bit_def [where ?'a = int, no_vars]}
@ -89,6 +101,16 @@ text \<open>
\<^item> (Bounded) conversion from and to a list of bits:
@{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
Bit concatenation on \<^typ>\<open>int\<close> as given by
@{thm [display] concat_bit_def [no_vars]}
appears quite
technical but is the logical foundation for the quite natural bit concatenation
on \<^typ>\<open>'a word\<close> (see below).
\<close>
subsection \<open>Core word theory\<close>
text \<open>
Proper word types are introduced in theory \<^theory>\<open>HOL-Library.Word\<close>, with
the following specific operations:
@ -159,22 +181,26 @@ text \<open>
For proofs about words the following default strategies are applicable:
\<^item> Using bit extensionality (facts \<^text>\<open>bit_eq_iff\<close>, \<^text>\<open>bit_eqI\<close>; fact
\<^item> Using bit extensionality (facts \<^text>\<open>bit_eq_iff\<close>, \<^text>\<open>bit_word_eqI\<close>; fact
collection \<^text>\<open>bit_simps\<close>).
\<^item> Using the @{method transfer} method.
\<close>
subsection \<open>More library theories\<close>
text \<open>
Note: currently, the theories listed here are hardly separate
Note: currently, most theories listed here are hardly separate
entities since they import each other in various ways.
Always inspect them to understand what you pull in if you
want to import one.
\<^descr>[Syntax]
\<^descr>[\<^theory>\<open>Word_Lib.Syntax_Bundles\<close>]
Bundles to provide alternative syntax for various bit operations.
\<^descr>[\<^theory>\<open>Word_Lib.Hex_Words\<close>]
Printing word numerals as hexadecimal numerals.
@ -192,6 +218,9 @@ text \<open>
\<^descr>[\<^theory>\<open>Word_Lib.Bitwise\<close>]
Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions.
\<^descr>[\<^theory>\<open>Word_Lib.Bitwise_Signed\<close>]
Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions.
\<^descr>[\<^theory>\<open>Word_Lib.Word_EqI\<close>]
Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions.
@ -226,18 +255,15 @@ text \<open>
\<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]}
\<^descr>[\<^theory>\<open>Word_Lib.Traditional_Infix_Syntax\<close>]
\<^descr>[\<^theory>\<open>Word_Lib.Bit_Shifts_Infix_Syntax\<close>]
Clones of existing operations decorated with
traditional syntax:
Bit shifts decorated with infix syntax:
\<^item> @{thm test_bit_eq_bit [no_vars]}
\<^item> @{thm Bit_Shifts_Infix_Syntax.shiftl_def [no_vars]}
\<^item> @{thm shiftl_eq_push_bit [no_vars]}
\<^item> @{thm Bit_Shifts_Infix_Syntax.shiftr_def [no_vars]}
\<^item> @{thm shiftr_eq_drop_bit [no_vars]}
\<^item> @{thm sshiftr_eq [no_vars]}
\<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]}
\<^descr>[\<^theory>\<open>Word_Lib.Next_and_Prev\<close>] \
@ -281,15 +307,19 @@ text \<open>
\<^descr>[\<^theory>\<open>Word_Lib.Word_32\<close>]
for 32-bit words. This theory is not part of \<^text>\<open>Word_Lib_Sumo\<close>, because it shadows
names from \<^theory>\<open>Word_Lib.Word_64\<close>. They can be used together, but then will have
to use qualified names in applications.
for 32-bit words.
\<^descr>[\<^theory>\<open>Word_Lib.Word_64\<close>]
for 64-bit words. This theory is not part of \<^text>\<open>Word_Lib_Sumo\<close>, because it shadows
names from \<^theory>\<open>Word_Lib.Word_32\<close>. They can be used together, but then will have
to use qualified names in applications.
\<^descr>[\<^theory>\<open>Word_Lib.Machine_Word_32\<close> and \<^theory>\<open>Word_Lib.Machine_Word_64\<close>]
provide lemmas for 32-bit words and 64-bit words under the same name,
which can help to organize applications relying on some form
of genericity.
\<close>
@ -319,7 +349,7 @@ text \<open>
for backward compatibility: start importing this theory when
migrating applications to Isabelle2021, and later sort out
what you really need. You may need to include
\<^theory>\<open>Word_Lib.Word_32\<close> or \<^theory>\<open>Word_Lib.Word_64\<close> separately.
\<^theory>\<open>Word_Lib.Word_64\<close> separately.
\<^descr>[\<^theory>\<open>Word_Lib.Generic_set_bit\<close>]
@ -355,6 +385,36 @@ text \<open>
They are used in applications of \<^text>\<open>Word_Lib\<close>, but should be migrated to there.
\<close>
section \<open>Changelog\<close>
text \<open>
\<^descr>[Changes since AFP 2021] ~
\<^item> Theory \<^theory>\<open>Word_Lib.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>
any longer.
\<^item> Infix syntax for \<^term>\<open>(AND)\<close>, \<^term>\<open>(OR)\<close>, \<^term>\<open>(XOR)\<close> organized in
syntax bundle \<^bundle>\<open>bit_operations_syntax\<close>.
\<^item> Abbreviation \<^abbrev>\<open>max_word\<close> moved from distribution into theory
\<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
\<^item> Operation \<^const>\<open>test_bit\<close> replaced by input abbreviation \<^abbrev>\<open>test_bit\<close>.
\<^item> Abbreviations \<^abbrev>\<open>bin_nth\<close>, \<^abbrev>\<open>bin_last\<close>, \<^abbrev>\<open>bin_rest\<close>,
\<^abbrev>\<open>bintrunc\<close>, \<^abbrev>\<open>sbintrunc\<close>, \<^abbrev>\<open>norm_sint\<close>,
\<^abbrev>\<open>bin_cat\<close> moved into theory \<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
\<^item> Operations \<^abbrev>\<open>bshiftr1\<close>,
\<^abbrev>\<open>setBit\<close>, \<^abbrev>\<open>clearBit\<close> moved from distribution into theory
\<^theory>\<open>Word_Lib.Legacy_Aliases\<close> and replaced by input abbreviations.
\<^item> Operations \<^const>\<open>shiftl1\<close>, \<^const>\<open>shiftr1\<close>, \<^const>\<open>sshiftr1\<close>
moved here from distribution.
\<^item> Operation \<^const>\<open>complement\<close> replaced by input abbreviation \<^abbrev>\<open>complement\<close>.
\<close>
(*<*)
end
(*>*)

18
lib/Word_Lib/Least_significant_bit.thy
View File

@ -11,7 +11,7 @@ section \<open>Operation variant for the least significant bit\<close>
theory Least_significant_bit
imports
"HOL-Library.Word"
Bits_Int
More_Word
begin
class lsb = semiring_bits +
@ -22,14 +22,14 @@ instantiation int :: lsb
begin
definition lsb_int :: \<open>int \<Rightarrow> bool\<close>
where \<open>lsb i = i !! 0\<close> for i :: int
where \<open>lsb i = bit i 0\<close> for i :: int
instance
by standard (simp add: fun_eq_iff lsb_int_def)
end
lemma bin_last_conv_lsb: "bin_last = lsb"
lemma bin_last_conv_lsb: "odd = (lsb :: int \<Rightarrow> bool)"
by (simp add: lsb_odd)
lemma int_lsb_numeral [simp]:
@ -62,9 +62,9 @@ lemma lsb_word_eq:
\<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close>
by (fact lsb_odd)
lemma word_lsb_alt: "lsb w = test_bit w 0"
lemma word_lsb_alt: "lsb w = bit w 0"
for w :: "'a::len word"
by (auto simp: word_test_bit_def word_lsb_def)
by (simp add: lsb_word_eq)
lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
unfolding word_lsb_def by simp
@ -78,12 +78,12 @@ lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
lemma word_lsb_numeral [simp]:
"lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
unfolding word_lsb_alt test_bit_numeral by simp
"lsb (numeral bin :: 'a::len word) \<longleftrightarrow> odd (numeral bin :: int)"
by (simp only: lsb_odd, transfer) rule
lemma word_lsb_neg_numeral [simp]:
"lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
by (simp add: word_lsb_alt)
"lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> odd (- numeral bin :: int)"
by (simp only: lsb_odd, transfer) rule
lemma word_lsb_nat:"lsb w = (unat w mod 2 = 1)"
apply (simp add: word_lsb_def Groebner_Basis.algebra(31))

125
lib/Word_Lib/Legacy_Aliases.thy
View File

@ -10,13 +10,128 @@ theory Legacy_Aliases
imports "HOL-Library.Word"
begin
definition
complement :: "'a :: len word \<Rightarrow> 'a word" where
"complement x \<equiv> NOT x"
context abstract_boolean_algebra
begin
lemma conj_assoc: "(x \<^bold>\<sqinter> y) \<^bold>\<sqinter> z = x \<^bold>\<sqinter> (y \<^bold>\<sqinter> z)"
by (fact conj.assoc)
lemma conj_commute: "x \<^bold>\<sqinter> y = y \<^bold>\<sqinter> x"
by (fact conj.commute)
lemmas conj_left_commute = conj.left_commute
lemmas conj_ac = conj.assoc conj.commute conj.left_commute
lemma conj_one_left: "\<^bold>1 \<^bold>\<sqinter> x = x"
by (fact conj.left_neutral)
lemma conj_left_absorb: "x \<^bold>\<sqinter> (x \<^bold>\<sqinter> y) = x \<^bold>\<sqinter> y"
by (fact conj.left_idem)
lemma conj_absorb: "x \<^bold>\<sqinter> x = x"
by (fact conj.idem)
lemma disj_assoc: "(x \<^bold>\<squnion> y) \<^bold>\<squnion> z = x \<^bold>\<squnion> (y \<^bold>\<squnion> z)"
by (fact disj.assoc)
lemma disj_commute: "x \<^bold>\<squnion> y = y \<^bold>\<squnion> x"
by (fact disj.commute)
lemmas disj_left_commute = disj.left_commute
lemmas disj_ac = disj.assoc disj.commute disj.left_commute
lemma disj_zero_left: "\<^bold>0 \<^bold>\<squnion> x = x"
by (fact disj.left_neutral)
lemma disj_left_absorb: "x \<^bold>\<squnion> (x \<^bold>\<squnion> y) = x \<^bold>\<squnion> y"
by (fact disj.left_idem)
lemma disj_absorb: "x \<^bold>\<squnion> x = x"
by (fact disj.idem)
end
context abstract_boolean_algebra_sym_diff
begin
lemmas xor_assoc = xor.assoc
lemmas xor_commute = xor.commute
lemmas xor_left_commute = xor.left_commute
lemmas xor_ac = xor.assoc xor.commute xor.left_commute
lemma xor_zero_right: "x \<^bold>\<ominus> \<^bold>0 = x"
by (fact xor.comm_neutral)
lemma xor_zero_left: "\<^bold>0 \<^bold>\<ominus> x = x"
by (fact xor.left_neutral)
end
abbreviation (input) test_bit :: \<open>'a::semiring_bits \<Rightarrow> nat \<Rightarrow> bool\<close>
where \<open>test_bit \<equiv> bit\<close>
abbreviation (input) bin_nth :: \<open>int \<Rightarrow> nat \<Rightarrow> bool\<close>
where \<open>bin_nth \<equiv> bit\<close>
abbreviation (input) bin_last :: \<open>int \<Rightarrow> bool\<close>
where \<open>bin_last \<equiv> odd\<close>
abbreviation (input) bin_rest :: \<open>int \<Rightarrow> int\<close>
where \<open>bin_rest w \<equiv> w div 2\<close>
abbreviation (input) bintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>bintrunc \<equiv> take_bit\<close>
abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>sbintrunc \<equiv> signed_take_bit\<close>
abbreviation (input) bin_cat :: \<open>int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>bin_cat k n l \<equiv> concat_bit n l k\<close>
abbreviation (input) norm_sint :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>norm_sint n \<equiv> signed_take_bit (n - 1)\<close>
abbreviation (input) max_word :: \<open>'a::len word\<close>
where \<open>max_word \<equiv> - 1\<close>
abbreviation (input) complement :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>complement \<equiv> not\<close>
lemma complement_mask:
"complement (2 ^ n - 1) = NOT (mask n)"
unfolding complement_def mask_eq_decr_exp by simp
"complement (2 ^ n - 1) = not (mask n)"
unfolding mask_eq_decr_exp by simp
context
includes bit_operations_syntax
begin
abbreviation (input) bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close>
where \<open>bshiftr1 b w \<equiv> w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b) \<close>
end
lemma bit_bshiftr1_iff:
\<open>bit (bshiftr1 b w) n \<longleftrightarrow> b \<and> n = LENGTH('a) - 1 \<or> bit w (Suc n)\<close>
for w :: \<open>'a::len word\<close>
by (auto simp add: bit_simps simp flip: bit_Suc)
abbreviation (input) setBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
where \<open>setBit w n \<equiv> set_bit n w\<close>
abbreviation (input) clearBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
where \<open>clearBit w n \<equiv> unset_bit n w\<close>
lemma bit_setBit_iff:
\<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
for w :: \<open>'a::len word\<close>
by (auto simp add: bit_simps)
lemma bit_clearBit_iff:
\<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
for w :: \<open>'a::len word\<close>
by (auto simp add: bit_simps)
lemmas less_def = less_eq [symmetric]
lemmas le_def = not_less [symmetric, where ?'a = nat]

136
lib/Word_Lib/Machine_Word_32.thy Normal file
View File

@ -0,0 +1,136 @@
(*
* 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)
*)
section "32-Bit Machine Word Setup"
theory Machine_Word_32
imports Machine_Word_32_Basics More_Word Bit_Shifts_Infix_Syntax Rsplit
begin
context
includes bit_operations_syntax
begin
type_synonym machine_word = \<open>machine_word_len word\<close>
lemma word_bits_len_of:
\<open>LENGTH(machine_word_len) = word_bits\<close>
by (simp add: word_bits_conv)
lemma word_bits_size:
"size (w :: machine_word) = word_bits"
by (simp add: word_bits_def word_size)
lemma word_bits_word_size_conv:
\<open>word_bits = word_size * 8\<close>
by (simp add: word_bits_def word_size_def)
lemma word_size_word_size_bits:
\<open>word_size = (2 :: 'a :: semiring_1) ^ word_size_bits\<close>
by (simp add: word_size_def word_size_bits_def)
lemma lt_word_bits_lt_pow:
"sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
by (simp add: word_bits_conv)
lemma if_then_1_else_0:
"((if P then 1 else 0) = (0 :: machine_word)) = (\<not> P)"
by simp
lemma if_then_0_else_1:
"((if P then 0 else 1) = (0 :: machine_word)) = (P)"
by simp
lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
lemma bool_mask [simp]:
\<open>0 < x AND 1 \<longleftrightarrow> x AND 1 = 1\<close> for x :: machine_word
by (rule bool_mask') auto
lemma in_16_range:
"0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: machine_word)) ` S"
"n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: machine_word. r + x * 16) ` S"
by (clarsimp simp: image_def elim!: bexI[rotated])+
lemma le_step_down_word_3:
fixes x :: machine_word
shows "\<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1"
by (fact le_step_down_word_2)
lemma shiftr_1:
"(x::machine_word) >> 1 = 0 \<Longrightarrow> x < 2"
apply transfer
apply (simp add: take_bit_drop_bit)
apply (simp add: drop_bit_Suc)
done
lemma Suc_unat_mask_div:
"Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)"
by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
flip: drop_bit_eq_div word_bits_conv)
lemma ucast_not_helper:
fixes a::"8 word"
assumes a: "a \<noteq> 0xFF"
shows "ucast a \<noteq> (0xFF::machine_word)"
proof
assume "ucast a = (0xFF::machine_word)"
also
have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp
finally
show False using a
apply -
apply (drule up_ucast_inj, simp)
apply simp
done
qed
lemma unat_less_2p_word_bits:
"unat (x :: machine_word) < 2 ^ word_bits"
apply (simp only: word_bits_def)
apply (rule unat_lt2p)
done
lemma unat_less_word_bits:
fixes y :: machine_word
shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
unfolding word_bits_def
by (rule order_less_trans [OF _ unat_lt2p])
lemma unat_mask_2_less_4:
"unat (p AND mask 2 :: machine_word) < 4"
by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)
lemma unat_mult_simple:
\<open>unat (x * y) = unat x * unat y\<close>
if \<open>unat x * unat y < 2 ^ LENGTH(machine_word_len)\<close>
for x y :: machine_word
using that by (simp flip: unat_mult_lem)
lemma upto_2_helper:
"{0..<2 :: machine_word} = {0, 1}"
by (safe; simp) unat_arith
lemma word_ge_min:
\<open>- (2 ^ (word_bits - 1)) \<le> sint x\<close> for x :: machine_word
using sint_ge [of x] by (simp add: word_bits_def)
lemma word_rsplit_0:
"word_rsplit (0 :: machine_word) = replicate (word_bits div 8) (0 :: 8 word)"
by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)
lemma x_less_2_0_1:
fixes x :: machine_word
shows "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
by (rule x_less_2_0_1') auto
end
end

66
lib/Word_Lib/Machine_Word_32_Basics.thy Normal file
View File

@ -0,0 +1,66 @@
(*
* 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)
*)
section \<open>32 bit standard platform-specific word size and alignment.\<close>
theory Machine_Word_32_Basics
imports "HOL-Library.Word" Word_32
begin
type_synonym machine_word_len = 32
definition word_bits :: nat
where
\<open>word_bits = LENGTH(machine_word_len)\<close>
lemma word_bits_conv [code]:
\<open>word_bits = 32\<close>
by (simp add: word_bits_def)
text \<open>The following two are numerals so they can be used as nats and words.\<close>
definition word_size_bits :: \<open>'a :: numeral\<close>
where
\<open>word_size_bits = 2\<close>
definition word_size :: \<open>'a :: numeral\<close>
where
\<open>word_size = 4\<close>
lemma n_less_word_bits:
"(n < word_bits) = (n < 32)"
by (simp add: word_bits_def word_size_def)
lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def]
lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def]
lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def]
lemmas unat_power_lower32 [simp] = unat_power_lower32'[folded word_bits_def]
lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def]
lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def]
lemma of_nat32_0:
"\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
by (erule of_nat_0, simp add: word_bits_def)
lemmas unat_of_nat32 = unat_of_nat32'[folded word_bits_def]
lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def]
lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def]
lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def]
lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def]
end

136
lib/Word_Lib/Machine_Word_64.thy Normal file
View File

@ -0,0 +1,136 @@
(*
* 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)
*)
section "64-Bit Machine Word Setup"
theory Machine_Word_64
imports Machine_Word_64_Basics More_Word Bit_Shifts_Infix_Syntax Rsplit
begin
context
includes bit_operations_syntax
begin
type_synonym machine_word = \<open>machine_word_len word\<close>
lemma word_bits_len_of:
\<open>LENGTH(machine_word_len) = word_bits\<close>
by (simp add: word_bits_conv)
lemma word_bits_size:
"size (w :: machine_word) = word_bits"
by (simp add: word_bits_def word_size)
lemma word_bits_word_size_conv:
\<open>word_bits = word_size * 8\<close>
by (simp add: word_bits_def word_size_def)
lemma word_size_word_size_bits:
\<open>word_size = (2 :: 'a :: semiring_1) ^ word_size_bits\<close>
by (simp add: word_size_def word_size_bits_def)
lemma lt_word_bits_lt_pow:
"sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
by (simp add: word_bits_conv)
lemma if_then_1_else_0:
"((if P then 1 else 0) = (0 :: machine_word)) = (\<not> P)"
by simp
lemma if_then_0_else_1:
"((if P then 0 else 1) = (0 :: machine_word)) = (P)"
by simp
lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
lemma bool_mask [simp]:
\<open>0 < x AND 1 \<longleftrightarrow> x AND 1 = 1\<close> for x :: machine_word
by (rule bool_mask') auto
lemma in_16_range:
"0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: machine_word)) ` S"
"n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: machine_word. r + x * 16) ` S"
by (clarsimp simp: image_def elim!: bexI[rotated])+
lemma le_step_down_word_3:
fixes x :: machine_word
shows "\<lbrakk>x \<le> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<le> y - 1"
by (fact le_step_down_word_2)
lemma shiftr_1:
"(x::machine_word) >> 1 = 0 \<Longrightarrow> x < 2"
apply transfer
apply (simp add: take_bit_drop_bit)
apply (simp add: drop_bit_Suc)
done
lemma Suc_unat_mask_div:
"Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)"
by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp
flip: drop_bit_eq_div word_bits_conv)
lemma ucast_not_helper:
fixes a::"8 word"
assumes a: "a \<noteq> 0xFF"
shows "ucast a \<noteq> (0xFF::machine_word)"
proof
assume "ucast a = (0xFF::machine_word)"
also
have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp
finally
show False using a
apply -
apply (drule up_ucast_inj, simp)
apply simp
done
qed
lemma unat_less_2p_word_bits:
"unat (x :: machine_word) < 2 ^ word_bits"
apply (simp only: word_bits_def)
apply (rule unat_lt2p)
done
lemma unat_less_word_bits:
fixes y :: machine_word
shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
unfolding word_bits_def
by (rule order_less_trans [OF _ unat_lt2p])
lemma unat_mask_2_less_4:
"unat (p AND mask 2 :: machine_word) < 4"
by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)
lemma unat_mult_simple:
\<open>unat (x * y) = unat x * unat y\<close>
if \<open>unat x * unat y < 2 ^ LENGTH(machine_word_len)\<close>
for x y :: machine_word
using that by (simp flip: unat_mult_lem)
lemma upto_2_helper:
"{0..<2 :: machine_word} = {0, 1}"
by (safe; simp) unat_arith
lemma word_ge_min:
\<open>- (2 ^ (word_bits - 1)) \<le> sint x\<close> for x :: machine_word
using sint_ge [of x] by (simp add: word_bits_def)
lemma word_rsplit_0:
"word_rsplit (0 :: machine_word) = replicate (word_bits div 8) (0 :: 8 word)"
by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)
lemma x_less_2_0_1:
fixes x :: machine_word
shows "x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
by (rule x_less_2_0_1') auto
end
end

66
lib/Word_Lib/Machine_Word_64_Basics.thy Normal file
View File

@ -0,0 +1,66 @@
(*
* 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)
*)
section \<open>64 bit standard platform-specific word size and alignment.\<close>
theory Machine_Word_64_Basics
imports "HOL-Library.Word" Word_64
begin
type_synonym machine_word_len = 64
definition word_bits :: nat
where
\<open>word_bits = LENGTH(machine_word_len)\<close>
lemma word_bits_conv [code]:
\<open>word_bits = 64\<close>
by (simp add: word_bits_def)
text \<open>The following two are numerals so they can be used as nats and words.\<close>
definition word_size_bits :: \<open>'a :: numeral\<close>
where
\<open>word_size_bits = 3\<close>
definition word_size :: \<open>'a :: numeral\<close>
where
\<open>word_size = 8\<close>
lemma n_less_word_bits:
"(n < word_bits) = (n < 64)"
by (simp add: word_bits_def word_size_def)
lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def]
lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def]
lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def]
lemmas unat_power_lower64 [simp] = unat_power_lower64'[folded word_bits_def]
lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def]
lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def]
lemma of_nat64_0:
"\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
by (erule of_nat_0, simp add: word_bits_def)
lemmas unat_of_nat64 = unat_of_nat64'[folded word_bits_def]
lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def]
lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def]
lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, folded word_bits_def]
lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
end

6
lib/Word_Lib/Many_More.thy
View File

@ -18,10 +18,16 @@ lemma nat_less_mult_monoish: "\<lbrakk> a < b; c < (d :: nat) \<rbrakk> \<Longri
apply simp
done
context
includes bit_operations_syntax
begin
lemma if_and_helper:
"(If x v v') AND v'' = If x (v AND v'') (v' AND v'')"
by (rule if_distrib)
end
lemma eq_eqI:
"a = b \<Longrightarrow> (a = x) = (b = x)"
by simp

14
lib/Word_Lib/More_Arithmetic.thy
View File

@ -7,14 +7,10 @@
section \<open>Arithmetic lemmas\<close>
theory More_Arithmetic
imports Main "HOL-Library.Type_Length" "HOL-Library.Bit_Operations"
imports Main "HOL-Library.Type_Length"
begin
declare iszero_0 [intro]
declare min.absorb1 [simp] min.absorb2 [simp]
lemma n_less_equal_power_2 [simp]:
lemma n_less_equal_power_2:
"n < 2 ^ n"
by (fact less_exp)
@ -138,4 +134,10 @@ proof -
by simp
qed
lemma msrevs:
"0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
"(k * n + m) mod n = m mod n"
for n :: nat
by simp_all
end

6
lib/Word_Lib/More_Divides.thy
View File

@ -403,13 +403,11 @@ lemma two_pow_div_gt_le:
lemma td_gal_lt:
\<open>0 < c \<Longrightarrow> a < b * c \<longleftrightarrow> a div c < b\<close>
for a b c :: nat
apply (auto dest: less_mult_imp_div_less)
apply (metis div_le_mono div_mult_self_is_m leD leI)
done
by (simp add: div_less_iff_less_mult)
lemma td_gal:
\<open>0 < c \<Longrightarrow> b * c \<le> a \<longleftrightarrow> b \<le> a div c\<close>
for a b c :: nat
by (meson not_le td_gal_lt)
by (simp add: less_eq_div_iff_mult_less_eq)
end

874
lib/Word_Lib/More_Word.thy
View File

File diff suppressed because it is too large Load Diff

212
lib/Word_Lib/More_Word_Operations.thy
View File

@ -13,6 +13,12 @@ theory More_Word_Operations
Reversed_Bit_Lists
More_Misc
Signed_Words
Word_Lemmas
Word_EqI
begin
context
includes bit_operations_syntax
begin
definition
@ -48,6 +54,36 @@ definition
where
"word_ctz w \<equiv> length (takeWhile Not (rev (to_bl w)))"
lemma word_ctz_unfold:
\<open>word_ctz w = length (takeWhile (Not \<circ> bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close>
by (simp add: word_ctz_def rev_to_bl_eq takeWhile_map)
lemma word_ctz_unfold':
\<open>word_ctz w = Min (insert LENGTH('a) {n. bit w n})\<close> for w :: \<open>'a::len word\<close>
proof (cases \<open>\<exists>n. bit w n\<close>)
case True
then obtain n where \<open>bit w n\<close> ..
from \<open>bit w n\<close> show ?thesis
apply (simp add: word_ctz_unfold)
apply (subst Min_eq_length_takeWhile [symmetric])
apply (auto simp add: bit_imp_le_length)
apply (subst Min_insert)
apply auto
apply (subst min.absorb2)
apply (subst Min_le_iff)
apply auto
apply (meson bit_imp_le_length order_less_le)
done
next
case False
then have \<open>bit w = bot\<close>
by auto
then have \<open>word_ctz w = LENGTH('a)\<close>
by (simp add: word_ctz_def rev_to_bl_eq bot_fun_def map_replicate_const)
with \<open>bit w = bot\<close> show ?thesis
by simp
qed
lemma word_ctz_le:
"word_ctz (w :: ('a::len word)) \<le> LENGTH('a)"
apply (clarsimp simp: word_ctz_def)
@ -87,11 +123,11 @@ qed
lemma unat_of_nat_ctz_mw:
"unat (of_nat (word_ctz (w :: 'a :: len word)) :: 'a :: len word) = word_ctz w"
by simp
by (simp add: unsigned_of_nat)
lemma unat_of_nat_ctz_smw:
"unat (of_nat (word_ctz (w :: 'a :: len word)) :: 'a :: len signed word) = word_ctz w"
by simp
by (simp add: unsigned_of_nat)
definition
word_log2 :: "'a::len word \<Rightarrow> nat"
@ -108,7 +144,7 @@ where
definition
sign_extend :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 'a word"
where
"sign_extend n w \<equiv> if w !! n then w OR NOT (mask n) else w AND mask n"
"sign_extend n w \<equiv> if bit w n then w OR NOT (mask n) else w AND mask n"
lemma sign_extend_eq_signed_take_bit:
\<open>sign_extend = signed_take_bit\<close>
@ -119,7 +155,7 @@ proof (rule ext)+
fix q
assume \<open>q < LENGTH('a)\<close>
then show \<open>bit (sign_extend n w) q \<longleftrightarrow> bit (signed_take_bit n w) q\<close>
by (auto simp add: test_bit_eq_bit bit_signed_take_bit_iff
by (auto simp add: bit_signed_take_bit_iff
sign_extend_def bit_and_iff bit_or_iff bit_not_iff bit_mask_iff not_less
exp_eq_0_imp_not_bit not_le min_def)
qed
@ -128,7 +164,7 @@ qed
definition
sign_extended :: "nat \<Rightarrow> 'a::len word \<Rightarrow> bool"
where
"sign_extended n w \<equiv> \<forall>i. n < i \<longrightarrow> i < size w \<longrightarrow> w !! i = w !! n"
"sign_extended n w \<equiv> \<forall>i. n < i \<longrightarrow> i < size w \<longrightarrow> bit w i = bit w n"
lemma ptr_add_0 [simp]:
"ptr_add ref 0 = ref "
@ -193,7 +229,7 @@ lemma bit_word_log2:
\<open>bit w (word_log2 w)\<close> if \<open>w \<noteq> 0\<close>
proof -
from \<open>w \<noteq> 0\<close> have \<open>\<exists>r. bit w r\<close>
by (simp add: bit_eq_iff)
by (auto intro: bit_eqI)
then obtain r where \<open>bit w r\<close> ..
from \<open>w \<noteq> 0\<close> have \<open>word_log2 w = Max {n. bit w n}\<close>
by (simp add: word_log2_unfold)
@ -216,17 +252,17 @@ proof -
qed
lemma word_log2_nth_same:
"w \<noteq> 0 \<Longrightarrow> w !! word_log2 w"
by (drule bit_word_log2) (simp add: test_bit_eq_bit)
"w \<noteq> 0 \<Longrightarrow> bit w (word_log2 w)"
by (drule bit_word_log2) simp
lemma word_log2_nth_not_set:
"\<lbrakk> word_log2 w < i ; i < size w \<rbrakk> \<Longrightarrow> \<not> w !! i"
using word_log2_maximum [of w i] by (auto simp add: test_bit_eq_bit)
"\<lbrakk> word_log2 w < i ; i < size w \<rbrakk> \<Longrightarrow> \<not> bit w i"
using word_log2_maximum [of w i] by auto
lemma word_log2_highest:
assumes a: "w !! i"
assumes a: "bit w i"
shows "i \<le> word_log2 w"
using a by (simp add: test_bit_eq_bit word_log2_maximum)
using a by (simp add: word_log2_maximum)
lemma word_log2_max:
"word_log2 w < size w"
@ -319,7 +355,7 @@ next
case False
have lt0: "unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)" using sz
by (metis shiftr_div_2n' word_shiftr_lt)
by (metis le_add_diff_inverse2 less_mult_imp_div_less order_less_imp_le power_add unsigned_less)
have"2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)" using sz
by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right lt0 nat_le_power_trans nat_less_le)
@ -413,7 +449,7 @@ next
assume asm: "alignUp a n = 0"
have lt0: "unat a div 2 ^ n < 2 ^ (LENGTH('a) - n)" using sz
by (metis shiftr_div_2n' word_shiftr_lt)
by (metis le_add_diff_inverse2 less_mult_imp_div_less order_less_imp_le power_add unsigned_less)
have leq: "2 ^ n * (unat a div 2 ^ n + 1) \<le> 2 ^ LENGTH('a)" using sz
by (metis One_nat_def Suc_leI add.right_neutral add_Suc_right lt0 nat_le_power_trans
@ -438,7 +474,7 @@ next
with leq have "2 ^ n * (unat a div 2 ^ n + 1) = 2 ^ LENGTH('a)"
by (force elim!: le_SucE)
then have "unat a div 2 ^ n = 2 ^ LENGTH('a) div 2 ^ n - 1"
by (metis (no_types, hide_lams) Groups.add_ac(2) add.right_neutral
by (metis (no_types, opaque_lifting) Groups.add_ac(2) add.right_neutral
add_diff_cancel_left' div_le_dividend div_mult_self4 gr_implies_not0
le_neq_implies_less power_eq_0_iff zero_neq_numeral)
then have "unat a div 2 ^ n = 2 ^ (LENGTH('a) - n) - 1"
@ -536,21 +572,26 @@ qed
(* Sign extension from bit n. *)
lemma bin_sign_extend_iff [bit_simps]:
\<open>bit (sign_extend e w) i \<longleftrightarrow> bit w (min e i)\<close>
if \<open>i < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
using that by (simp add: sign_extend_def bit_simps min_def)
lemma sign_extend_bitwise_if:
"i < size w \<Longrightarrow> sign_extend e w !! i \<longleftrightarrow> (if i < e then w !! i else w !! e)"
by (simp add: sign_extend_def neg_mask_test_bit word_size)
"i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (if i < e then bit w i else bit w e)"
by (simp add: word_size bit_simps)
lemma sign_extend_bitwise_if' [word_eqI_simps]:
\<open>i < LENGTH('a) \<Longrightarrow> sign_extend e w !! i \<longleftrightarrow> (if i < e then w !! i else w !! e)\<close>
\<open>i < LENGTH('a) \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (if i < e then bit w i else bit w e)\<close>
for w :: \<open>'a::len word\<close>
using sign_extend_bitwise_if [of i w e] by (simp add: word_size)
lemma sign_extend_bitwise_disj:
"i < size w \<Longrightarrow> sign_extend e w !! i \<longleftrightarrow> i \<le> e \<and> w !! i \<or> e \<le> i \<and> w !! e"
"i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> i \<le> e \<and> bit w i \<or> e \<le> i \<and> bit w e"
by (auto simp: sign_extend_bitwise_if)
lemma sign_extend_bitwise_cases:
"i < size w \<Longrightarrow> sign_extend e w !! i \<longleftrightarrow> (i \<le> e \<longrightarrow> w !! i) \<and> (e \<le> i \<longrightarrow> w !! e)"
"i < size w \<Longrightarrow> bit (sign_extend e w) i \<longleftrightarrow> (i \<le> e \<longrightarrow> bit w i) \<and> (e \<le> i \<longrightarrow> bit w e)"
by (auto simp: sign_extend_bitwise_if)
lemmas sign_extend_bitwise_disj' = sign_extend_bitwise_disj[simplified word_size]
@ -559,8 +600,8 @@ lemmas sign_extend_bitwise_cases' = sign_extend_bitwise_cases[simplified word_si
(* Often, it is easier to reason about an operation which does not overwrite
the bit which determines which mask operation to apply. *)
lemma sign_extend_def':
"sign_extend n w = (if w !! n then w OR NOT (mask (Suc n)) else w AND mask (Suc n))"
by (rule bit_word_eqI) (auto simp add: bit_simps sign_extend_eq_signed_take_bit min_def test_bit_eq_bit less_Suc_eq_le)
"sign_extend n w = (if bit w n then w OR NOT (mask (Suc n)) else w AND mask (Suc n))"
by (rule bit_word_eqI) (auto simp add: bit_simps sign_extend_eq_signed_take_bit min_def less_Suc_eq_le)
lemma sign_extended_sign_extend:
"sign_extended n (sign_extend n w)"
@ -570,10 +611,8 @@ lemma sign_extended_iff_sign_extend:
"sign_extended n w \<longleftrightarrow> sign_extend n w = w"
apply auto
apply (auto simp add: bit_eq_iff)
apply (simp_all add: bit_simps sign_extend_eq_signed_take_bit not_le min_def sign_extended_def test_bit_eq_bit word_size split: if_splits)
using le_imp_less_or_eq apply auto[1]
apply (metis bit_imp_le_length nat_less_le)
apply (metis Suc_leI Suc_n_not_le_n le_trans nat_less_le)
apply (simp_all add: bit_simps sign_extend_eq_signed_take_bit not_le min_def sign_extended_def word_size split: if_splits)
using le_imp_less_or_eq apply auto
done
lemma sign_extended_weaken:
@ -585,7 +624,7 @@ lemma sign_extend_sign_extend_eq:
by (rule bit_word_eqI) (simp add: sign_extend_eq_signed_take_bit bit_simps)
lemma sign_extended_high_bits:
"\<lbrakk> sign_extended e p; j < size p; e \<le> i; i < j \<rbrakk> \<Longrightarrow> p !! i = p !! j"
"\<lbrakk> sign_extended e p; j < size p; e \<le> i; i < j \<rbrakk> \<Longrightarrow> bit p i = bit p j"
by (drule (1) sign_extended_weaken; simp add: sign_extended_def)
lemma sign_extend_eq:
@ -601,11 +640,11 @@ lemma sign_extended_add:
proof (cases "e < size p")
case True
note and_or = is_aligned_add_or[OF p f]
have "\<not> f !! e"
have "\<not> bit f e"
using True e less_2p_is_upper_bits_unset[THEN iffD1, OF f]
by (fastforce simp: word_size)
hence i: "(p + f) !! e = p !! e"
by (simp add: and_or)
hence i: "bit (p + f) e = bit p e"
by (simp add: and_or bit_simps)
have fm: "f AND mask e = f"
by (fastforce intro: subst[where P="\<lambda>f. f AND mask e = f", OF less_mask_eq[OF f]]
simp: mask_twice e)
@ -622,7 +661,7 @@ qed
lemma sign_extended_neq_mask:
"\<lbrakk>sign_extended n ptr; m \<le> n\<rbrakk> \<Longrightarrow> sign_extended n (ptr AND NOT (mask m))"
by (fastforce simp: sign_extended_def word_size neg_mask_test_bit)
by (fastforce simp: sign_extended_def word_size neg_mask_test_bit bit_simps)
definition
"limited_and (x :: 'a :: len word) y \<longleftrightarrow> (x AND y = x)"
@ -642,13 +681,11 @@ lemma limited_and_eq_id:
lemma lshift_limited_and:
"limited_and x z \<Longrightarrow> limited_and (x << n) (z << n)"
unfolding limited_and_def
by (simp add: shiftl_over_and_dist[symmetric])
using push_bit_and [of n x z] by (simp add: limited_and_def shiftl_def)
lemma rshift_limited_and:
"limited_and x z \<Longrightarrow> limited_and (x >> n) (z >> n)"
unfolding limited_and_def
by (simp add: shiftr_over_and_dist[symmetric])
using drop_bit_and [of n x z] by (simp add: limited_and_def shiftr_def)
lemmas limited_and_simps1 = limited_and_eq_0 limited_and_eq_id
@ -660,8 +697,7 @@ lemmas limited_and_simps = limited_and_simps1
limited_and_simps1[OF lshift_limited_and]
limited_and_simps1[OF rshift_limited_and]
limited_and_simps1[OF rshift_limited_and, OF is_aligned_limited_and]
not_one shiftl_shiftr1[unfolded word_size mask_eq_decr_exp]
shiftl_shiftr2[unfolded word_size mask_eq_decr_exp]
not_one_eq
definition
from_bool :: "bool \<Rightarrow> 'a::len word" where
@ -685,8 +721,8 @@ definition
"to_bool \<equiv> (\<noteq>) 0"
lemma to_bool_and_1:
"to_bool (x AND 1) = (x !! 0)"
by (simp add: test_bit_word_eq to_bool_def and_one_eq mod_2_eq_odd)
"to_bool (x AND 1) \<longleftrightarrow> bit x 0"
by (simp add: to_bool_def and_one_eq mod_2_eq_odd)
lemma to_bool_from_bool [simp]:
"to_bool (from_bool r) = r"
@ -768,7 +804,7 @@ lemma aligned_offset_in_range:
apply (simp add: bit_simps)
apply (erule is_alignedE')
apply (auto simp add: bit_simps not_le)[1]
apply (metis less_2p_is_upper_bits_unset test_bit_eq_bit)
apply (metis less_2p_is_upper_bits_unset)
apply (simp only: is_aligned_add_or word_ao_dist flip: neg_mask_in_mask_range)
apply (subgoal_tac \<open>y AND NOT (mask n) = 0\<close>)
apply simp
@ -880,14 +916,19 @@ lemma aligned_mask_ranges_disjoint2:
apply safe
apply (simp only: flip: neg_mask_in_mask_range)
apply (drule_tac x="x AND mask n >> m" in spec)
apply (clarsimp simp: and_mask_less_size wsst_TYs shiftr_less_t2n multiple_mask_trivia neg_mask_twice
word_bw_assocs max_absorb2 shiftr_shiftl1)
apply (erule notE[OF mp])
apply (simp flip: take_bit_eq_mask add: shiftr_def drop_bit_take_bit)
apply transfer
apply simp
apply (simp add: word_size and_mask_less_size)
apply (subst disjunctive_add)
apply (auto simp add: bit_simps word_size intro!: bit_eqI)
done
lemma word_clz_sint_upper[simp]:
"LENGTH('a) \<ge> 3 \<Longrightarrow> sint (of_nat (word_clz (w :: 'a :: len word)) :: 'a sword) \<le> int (LENGTH('a))"
using word_clz_max [of w]
apply (simp add: word_size)
apply (simp add: word_size signed_of_nat)
apply (subst signed_take_bit_int_eq_self)
apply simp_all
apply (metis negative_zle of_nat_numeral semiring_1_class.of_nat_power)
@ -901,9 +942,9 @@ lemma word_clz_sint_lower[simp]:
\<Longrightarrow> - sint (of_nat (word_clz (w :: 'a :: len word)) :: 'a signed word) \<le> int (LENGTH('a))"
apply (subst sint_eq_uint)
using word_clz_max [of w]
apply (simp_all add: word_size)
apply (simp_all add: word_size unsigned_of_nat)
apply (rule not_msb_from_less)
apply (simp add: word_less_nat_alt)
apply (simp add: word_less_nat_alt unsigned_of_nat)
apply (subst take_bit_nat_eq_self)
apply (simp add: le_less_trans)
apply (drule small_powers_of_2)
@ -916,56 +957,6 @@ lemma mask_range_subsetD:
x' \<in> mask_range p n"
using aligned_mask_step by fastforce
lemma nasty_split_lt:
"\<lbrakk> (x :: 'a:: len word) < 2 ^ (m - n); n \<le> m; m < LENGTH('a::len) \<rbrakk>
\<Longrightarrow> x * 2 ^ n + (2 ^ n - 1) \<le> 2 ^ m - 1"
apply (simp only: add_diff_eq)
apply (subst mult_1[symmetric], subst distrib_right[symmetric])
apply (rule word_sub_mono)
apply (rule order_trans)
apply (rule word_mult_le_mono1)
apply (rule inc_le)
apply assumption
apply (subst word_neq_0_conv[symmetric])
apply (rule power_not_zero)
apply simp
apply (subst unat_power_lower, simp)+
apply (subst power_add[symmetric])
apply (rule power_strict_increasing)
apply simp
apply simp
apply (subst power_add[symmetric])
apply simp
apply simp
apply (rule word_sub_1_le)
apply (subst mult.commute)
apply (subst shiftl_t2n[symmetric])
apply (rule word_shift_nonzero)
apply (erule inc_le)
apply simp
apply (unat_arith)
apply (drule word_power_less_1)
apply simp
done
lemma nasty_split_less:
"\<lbrakk>m \<le> n; n \<le> nm; nm < LENGTH('a::len); x < 2 ^ (nm - n)\<rbrakk>
\<Longrightarrow> (x :: 'a word) * 2 ^ n + (2 ^ m - 1) < 2 ^ nm"
apply (simp only: word_less_sub_le[symmetric])
apply (rule order_trans [OF _ nasty_split_lt])
apply (rule word_plus_mono_right)
apply (rule word_sub_mono)
apply (simp add: word_le_nat_alt)
apply simp
apply (simp add: word_sub_1_le[OF power_not_zero])
apply (simp add: word_sub_1_le[OF power_not_zero])
apply (rule is_aligned_no_wrap')
apply (rule is_aligned_mult_triv2)
apply simp
apply (erule order_le_less_trans, simp)
apply simp+
done
lemma add_mult_in_mask_range:
"\<lbrakk> is_aligned (base :: 'a :: len word) n; n < LENGTH('a); bits \<le> n; x < 2 ^ (n - bits) \<rbrakk>
\<Longrightarrow> base + x * 2^bits \<in> mask_range base n"
@ -977,14 +968,27 @@ lemma from_to_bool_last_bit:
by (metis from_bool_to_bool_iff word_and_1)
lemma sint_ctz:
"LENGTH('a) > 2
\<Longrightarrow> 0 \<le> sint (of_nat (word_ctz (x :: 'a :: len word)) :: 'a signed word)
\<and> sint (of_nat (word_ctz x) :: 'a signed word) \<le> int (LENGTH('a))"
apply (subgoal_tac "LENGTH('a) < 2 ^ (LENGTH('a) - 1)")
apply (rule conjI)
apply (metis len_signed order_le_less_trans sint_of_nat_ge_zero word_ctz_le)
apply (metis int_eq_sint len_signed sint_of_nat_le word_ctz_le)
using small_powers_of_2 [of \<open>LENGTH('a)\<close>] by simp
\<open>0 \<le> sint (of_nat (word_ctz (x :: 'a :: len word)) :: 'a signed word)
\<and> sint (of_nat (word_ctz x) :: 'a signed word) \<le> int (LENGTH('a))\<close> (is \<open>?P \<and> ?Q\<close>)
if \<open>LENGTH('a) > 2\<close>
proof
have *: \<open>word_ctz x < 2 ^ (LENGTH('a) - Suc 0)\<close>
using word_ctz_le apply (rule le_less_trans)
using that small_powers_of_2 [of \<open>LENGTH('a)\<close>] apply simp
done
have \<open>int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0\<close>
apply (rule div_pos_pos_trivial)
apply (simp_all add: *)
done
then show ?P by (simp add: signed_of_nat bit_iff_odd)
show ?Q
apply (auto simp add: signed_of_nat)
apply (subst signed_take_bit_int_eq_self)
apply (auto simp add: word_ctz_le * minus_le_iff [of _ \<open>int (word_ctz x)\<close>])
apply (rule order.trans [of _ 0])
apply simp_all
done
qed
lemma unat_of_nat_word_log2:
"LENGTH('a) < 2 ^ LENGTH('b)
@ -1006,4 +1010,6 @@ lemma aligned_mask_diff:
apply (meson aligned_add_mask_less_eq is_aligned_weaken le_less_trans)
done
end
end

101
lib/Word_Lib/Most_significant_bit.thy
View File

@ -11,8 +11,8 @@ section \<open>Dedicated operation for the most significant bit\<close>
theory Most_significant_bit
imports
"HOL-Library.Word"
Bits_Int
Traditional_Infix_Syntax
Bit_Shifts_Infix_Syntax
More_Word
More_Arithmetic
begin
@ -28,13 +28,14 @@ instance ..
end
lemma msb_conv_bin_sign: "msb x \<longleftrightarrow> bin_sign x = -1"
by(simp add: bin_sign_def not_le msb_int_def)
lemma msb_bin_rest [simp]: "msb (x div 2) = msb x"
for x :: int
by (simp add: msb_int_def)
context
includes bit_operations_syntax
begin
lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y"
by(simp add: msb_int_def)
@ -47,14 +48,13 @@ by(simp add: msb_int_def)
lemma int_msb_not [simp]: "msb (NOT (x :: int)) \<longleftrightarrow> \<not> msb x"
by(simp add: msb_int_def not_less)
end
lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x"
by(simp add: msb_int_def)
by (simp add: msb_int_def shiftl_def)
lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x"
by(simp add: msb_int_def)
lemma msb_bin_sc [simp]: "msb (bin_sc n b x) \<longleftrightarrow> msb x"
by(simp add: msb_conv_bin_sign)
by (simp add: msb_int_def shiftr_def)
lemma msb_0 [simp]: "msb (0 :: int) = False"
by(simp add: msb_int_def)
@ -71,24 +71,15 @@ instantiation word :: (len) msb
begin
definition msb_word :: \<open>'a word \<Rightarrow> bool\<close>
where \<open>msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1\<close>
lemma msb_word_eq:
\<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
by (simp add: msb_word_def bin_sign_lem bit_uint_iff)
where msb_word_iff_bit: \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
instance ..
end
lemma msb_word_iff_bit:
\<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - Suc 0)\<close>
for w :: \<open>'a::len word\<close>
by (simp add: msb_word_def bin_sign_def bit_uint_iff)
lemma word_msb_def:
"msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
by (simp add: msb_word_def sint_uint)
lemma msb_word_eq:
\<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
by (simp add: msb_word_iff_bit)
lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
by (simp add: msb_word_eq bit_last_iff)
@ -97,48 +88,46 @@ lemma msb_word_iff_sless_0:
\<open>msb w \<longleftrightarrow> w <s 0\<close>
by (simp add: word_msb_sint word_sless_alt)
lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
by (simp add: word_msb_def bin_sign_lem)
lemma msb_word_of_int:
"msb (word_of_int x::'a::len word) = bit x (LENGTH('a) - 1)"
by (simp add: msb_word_iff_bit bit_simps)
lemma word_msb_numeral [simp]:
"msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
"msb (numeral w::'a::len word) = bit (numeral w :: int) (LENGTH('a) - 1)"
unfolding word_numeral_alt by (rule msb_word_of_int)
lemma word_msb_neg_numeral [simp]:
"msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
"msb (- numeral w::'a::len word) = bit (- numeral w :: int) (LENGTH('a) - 1)"
unfolding word_neg_numeral_alt by (rule msb_word_of_int)
lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
by (simp add: word_msb_def bin_sign_def sint_uint sbintrunc_eq_take_bit)
by (simp add: msb_word_iff_bit)
lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
by (simp add: Suc_le_eq)
by (simp add: msb_word_iff_bit le_Suc_eq)
lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
lemma word_msb_nth: "msb w = bit (uint w) (LENGTH('a) - 1)"
for w :: "'a::len word"
by (simp add: word_msb_def sint_uint bin_sign_lem)
by (simp add: msb_word_iff_bit bit_simps)
lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
lemma msb_nth: "msb w = bit w (LENGTH('a) - 1)"
for w :: "'a::len word"
by (simp add: word_msb_nth word_test_bit_def)
by (fact msb_word_eq)
lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
by (simp add: msb_word_eq not_le)
lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0"
lemma msb_shift: "msb w \<longleftrightarrow> w >> LENGTH('a) - 1 \<noteq> 0"
for w :: "'a::len word"
by (simp add: msb_word_eq shiftr_word_eq bit_iff_odd_drop_bit drop_bit_eq_zero_iff_not_bit_last)
by (simp add: drop_bit_eq_zero_iff_not_bit_last msb_word_eq shiftr_def)
lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
apply (cases \<open>LENGTH('a)\<close>)
apply (simp_all add: msb_word_def bin_sign_def bit_simps word_size)
apply (simp_all add: msb_word_iff_bit word_size)
apply transfer
apply (auto simp add: take_bit_Suc_from_most signed_take_bit_eq_if_positive signed_take_bit_eq_if_negative minus_exp_eq_not_mask ac_simps)
apply (subst disjunctive_add)
apply (simp_all add: bit_simps)
apply (simp add: signed_take_bit_eq_take_bit_minus)
done
lemma word_sle_msb_le: "x <=s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)"
@ -159,15 +148,15 @@ lemma not_msb_from_less:
apply (clarsimp simp add: msb_nth)
apply (drule less_mask_eq)
apply (drule word_eqD, drule(1) iffD2)
apply simp
apply (simp add: bit_simps)
done
lemma sint_eq_uint:
"\<not> msb x \<Longrightarrow> sint x = uint x"
apply (simp add: msb_word_eq)
apply (cases \<open>LENGTH('a)\<close>)
apply (simp_all add: msb_word_iff_bit)
apply transfer
apply auto
apply (smt One_nat_def bintrunc_bintrunc_l bintrunc_sbintrunc' diff_le_self len_gt_0 signed_take_bit_eq_if_positive)
apply (simp add: signed_take_bit_eq_take_bit_minus)
done
lemma scast_eq_ucast:
@ -177,7 +166,7 @@ lemma scast_eq_ucast:
apply (rule bit_word_eqI)
apply (auto simp add: bit_signed_iff bit_unsigned_iff min_def msb_word_eq)
apply (erule notE)
apply (metis le_less_Suc_eq test_bit_bin test_bit_word_eq)
apply (metis le_less_Suc_eq test_bit_bin)
done
lemma msb_ucast_eq:
@ -186,18 +175,20 @@ lemma msb_ucast_eq:
by (simp add: msb_word_eq bit_simps)
lemma msb_big:
"msb (a :: ('a::len) word) = (a \<ge> 2 ^ (LENGTH('a) - Suc 0))"
apply (rule iffI)
apply (clarsimp simp: msb_nth)
apply (drule bang_is_le)
apply simp
\<open>msb a \<longleftrightarrow> 2 ^ (LENGTH('a) - Suc 0) \<le> a\<close>
for a :: \<open>'a::len word\<close>
using bang_is_le [of a \<open>LENGTH('a) - Suc 0\<close>]
apply (auto simp add: msb_nth word_le_not_less)
apply (rule ccontr)
apply (subgoal_tac "a = a AND mask (LENGTH('a) - Suc 0)")
apply (erule notE)
apply (rule ccontr)
apply (clarsimp simp: not_less)
apply (subgoal_tac "a = take_bit (LENGTH('a) - Suc 0) a")
apply (cut_tac and_mask_less' [where w=a and n="LENGTH('a) - Suc 0"])
apply (clarsimp simp: word_not_le [symmetric])
apply clarsimp
apply (rule sym, subst and_mask_eq_iff_shiftr_0)
apply (clarsimp simp: msb_shift)
apply auto
apply (simp flip: take_bit_eq_mask)
apply (rule sym)
apply (simp add: take_bit_eq_self_iff_drop_bit_eq_0 drop_bit_eq_zero_iff_not_bit_last)
done
end

4
lib/Word_Lib/Next_and_Prev.thy
View File

@ -22,7 +22,7 @@ lift_definition word_prev :: \<open>'a::len word \<Rightarrow> 'a word\<close>
lemma word_next_unfold:
\<open>word_next w = (if w = - 1 then - 1 else w + 1)\<close>
by transfer (simp add: take_bit_minus_one_eq_mask flip: take_bit_eq_mask_iff_exp_dvd)
by transfer (simp flip: take_bit_eq_mask_iff_exp_dvd)
lemma word_prev_unfold:
\<open>word_prev w = (if w = 0 then 0 else w - 1)\<close>
@ -32,7 +32,7 @@ lemma [code]:
\<open>Word.the_int (word_next w :: 'a::len word) =
(if w = - 1 then Word.the_int w else Word.the_int w + 1)\<close>
by transfer
(simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 take_bit_incr_eq flip: take_bit_eq_mask_iff_exp_dvd)
(simp add: mask_eq_exp_minus_1 take_bit_incr_eq flip: take_bit_eq_mask_iff_exp_dvd)
lemma [code]:
\<open>Word.the_int (word_prev w :: 'a::len word) =

54
lib/Word_Lib/Norm_Words.thy
View File

@ -7,7 +7,7 @@
section "Normalising Word Numerals"
theory Norm_Words
imports Bits_Int Signed_Words
imports Signed_Words
begin
text \<open>
@ -15,25 +15,28 @@ text \<open>
interval \<open>[0..2^len_of 'a)\<close>. Only for concrete word lengths.
\<close>
lemma bintrunc_numeral:
"(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) x = of_bool (odd x) + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (x div 2)"
by (simp add: numeral_eq_Suc take_bit_Suc mod_2_eq_odd)
lemma neg_num_bintr:
"(- numeral x :: 'a::len word) =
word_of_int (bintrunc (LENGTH('a)) (-numeral x))"
"(- numeral x :: 'a::len word) = word_of_int (take_bit LENGTH('a) (- numeral x))"
by transfer simp
ML \<open>
fun is_refl (Const (@{const_name Pure.eq}, _) $ x $ y) = (x = y)
fun is_refl \<^Const_>\<open>Pure.eq _ for x y\<close> = (x = y)
| is_refl _ = false;
fun signed_dest_wordT (Type (@{type_name word}, [Type (@{type_name signed}, [T])])) = Word_Lib.dest_binT T
fun signed_dest_wordT \<^Type>\<open>word \<^Type>\<open>signed T\<close>\<close> = Word_Lib.dest_binT T
| signed_dest_wordT T = Word_Lib.dest_wordT T
fun typ_size_of t = signed_dest_wordT (type_of (Thm.term_of t));
fun num_len (Const (@{const_name Num.Bit0}, _) $ n) = num_len n + 1
| num_len (Const (@{const_name Num.Bit1}, _) $ n) = num_len n + 1
| num_len (Const (@{const_name Num.One}, _)) = 1
| num_len (Const (@{const_name numeral}, _) $ t) = num_len t
| num_len (Const (@{const_name uminus}, _) $ t) = num_len t
fun num_len \<^Const_>\<open>Num.Bit0 for n\<close> = num_len n + 1
| num_len \<^Const_>\<open>Num.Bit1 for n\<close> = num_len n + 1
| num_len \<^Const_>\<open>Num.One\<close> = 1
| num_len \<^Const_>\<open>numeral _ for t\<close> = num_len t
| num_len \<^Const_>\<open>uminus _ for t\<close> = num_len t
| num_len t = raise TERM ("num_len", [t])
fun unsigned_norm is_neg _ ctxt ct =
@ -43,7 +46,8 @@ ML \<open>
val th = [Thm.reflexive ct, mk_eq btr] MRS transitive_thm
(* will work in context of theory Word as well *)
val ss = simpset_of (@{context} addsimps @{thms bintrunc_numeral})
val ss = simpset_of (@{context} addsimps @{thms bintrunc_numeral} delsimps @{thms take_bit_minus_one_eq_mask})
(* TODO: completely explicitly determined simpset *)
val cnv = simplify (put_simpset ss ctxt) th
in if is_refl (Thm.prop_of cnv) then NONE else SOME cnv end
else NONE)
@ -67,22 +71,24 @@ lemma minus_one_norm:
lemmas minus_one_norm_num =
minus_one_norm [where 'a="'b::len bit0"] minus_one_norm [where 'a="'b::len0 bit1"]
lemma "f (7 :: 2 word) = f 3" by simp
context
begin
lemma "f 7 = f (3 :: 2 word)" by simp
private lemma "f (7 :: 2 word) = f 3" by simp
lemma "f (-2) = f (21 + 1 :: 3 word)" by simp
private lemma "f 7 = f (3 :: 2 word)" by simp
lemma "f (-2) = f (13 + 1 :: 'a::len word)"
private lemma "f (-2) = f (21 + 1 :: 3 word)" by simp
private lemma "f (-2) = f (13 + 1 :: 'a::len word)"
apply simp (* does not touch generic word length *)
oops
lemma "f (-2) = f (0xFFFFFFFE :: 32 word)" by simp
private lemma "f (-2) = f (0xFFFFFFFE :: 32 word)" by simp
lemma "(-1 :: 2 word) = 3" by simp
lemma "f (-2) = f (0xFFFFFFFE :: 32 signed word)" by simp
private lemma "(-1 :: 2 word) = 3" by simp
private lemma "f (-2) = f (0xFFFFFFFE :: 32 signed word)" by simp
text \<open>
We leave @{term "-1"} untouched by default, because it is often useful
@ -95,16 +101,18 @@ context
notes minus_one_norm_num [simp]
begin
lemma "f (-1) = f (15 :: 4 word)" by simp
private lemma "f (-1) = f (15 :: 4 word)" by simp
lemma "f (-1) = f (7 :: 3 word)" by simp
private lemma "f (-1) = f (7 :: 3 word)" by simp
lemma "f (-1) = f (0xFFFF :: 16 word)" by simp
private lemma "f (-1) = f (0xFFFF :: 16 word)" by simp
lemma "f (-1) = f (0xFFFF + 1 :: 'a::len word)"
private lemma "f (-1) = f (0xFFFF + 1 :: 'a::len word)"
apply simp (* does not touch generic -1 *)
oops
end
end
end

11
lib/Word_Lib/ROOT
View File

@ -9,14 +9,23 @@ chapter Lib
session Word_Lib (lib) = HOL +
options [timeout = 300, document=pdf]
sessions
"HOL-Library"
"HOL-Eisbach"
directories (* not in the AFP: *)
"$L4V_ARCH"
theories (* not in the AFP: *)
"Distinct_Prop"
"$L4V_ARCH/WordSetup"
theories [document=false]
More_Arithmetic
Even_More_List
More_Sublist
More_Misc
Strict_part_mono
Many_More
Ancient_Numeral
Examples
theories
Guide
Examples
document_files
"root.tex"

400
lib/Word_Lib/Reversed_Bit_Lists.thy
View File

@ -17,6 +17,12 @@ theory Reversed_Bit_Lists
Even_More_List
"HOL-Library.Sublist"
Aligned
Singleton_Bit_Shifts
Legacy_Aliases
begin
context
includes bit_operations_syntax
begin
lemma horner_sum_of_bool_2_concat:
@ -336,7 +342,7 @@ definition bl_to_bin :: "bool list \<Rightarrow> int"
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
where
Z: "bin_to_bl_aux 0 w bl = bl"
| Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
| Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (w div 2) (odd w # bl)"
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
where "bin_to_bl n w = bin_to_bl_aux n w []"
@ -429,20 +435,20 @@ lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (take_bit n w)"
by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = take_bit n w"
by (auto simp: bin_to_bl_def bin_bl_bin')
lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (take_bit m w) = bin_to_bl n w"
by (auto intro: bl_to_bin_inj)
lemma bin_to_bl_aux_bintr:
"bin_to_bl_aux n (bintrunc m bin) bl =
"bin_to_bl_aux n (take_bit m bin) bl =
replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
apply (induct n arbitrary: m bin bl)
apply clarsimp
@ -455,7 +461,7 @@ lemma bin_to_bl_aux_bintr:
done
lemma bin_to_bl_bintr:
"bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
"bin_to_bl n (take_bit m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
@ -473,25 +479,25 @@ lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
by (simp add: bl_to_bin_def sign_bl_bin')
lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (signed_take_bit n w) = -1)"
by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (signed_take_bit n w) = -1)"
unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
lemma bin_nth_of_bl_aux:
"bin_nth (bl_to_bin_aux bl w) n =
(n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
"bit (bl_to_bin_aux bl w) n =
(n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bit w (n - size bl))"
apply (induction bl arbitrary: w)
apply simp_all
apply safe
apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
done
lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
lemma bin_nth_of_bl: "bit (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
lemma bin_nth_bl: "n < m \<Longrightarrow> bit w n = nth (rev (bin_to_bl m w)) n"
apply (induct n arbitrary: m w)
apply clarsimp
apply (case_tac m, clarsimp)
@ -514,7 +520,7 @@ lemma nth_bin_to_bl_aux:
less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
done
lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bit w (m - Suc n)"
by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
@ -579,26 +585,26 @@ lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
apply simp
done
lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (w div 2)"
apply (unfold bin_to_bl_def)
apply (cases n, clarsimp)
apply clarsimp
apply (auto simp add: bin_to_bl_aux_alt)
done
lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2)"
using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
lemma butlast_rest_bl2bin_aux:
"bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
"bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bl_to_bin_aux bl w div 2"
by (induct bl arbitrary: w) auto
lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bl_to_bin bl div 2"
by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
lemma trunc_bl2bin_aux:
"bintrunc m (bl_to_bin_aux bl w) =
bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
"take_bit m (bl_to_bin_aux bl w) =
bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)"
proof (induct bl arbitrary: w)
case Nil
show ?case by simp
@ -616,13 +622,13 @@ next
qed
qed
lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
lemma trunc_bl2bin: "take_bit m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
by (simp add: bl_to_bin_def trunc_bl2bin_aux)
lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
lemma trunc_bl2bin_len [simp]: "take_bit (length bl) (bl_to_bin bl) = bl_to_bin bl"
by (simp add: trunc_bl2bin)
lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
lemma bl2bin_drop: "bl_to_bin (drop k bl) = take_bit (length bl - k) (bl_to_bin bl)"
apply (rule trans)
prefer 2
apply (rule trunc_bl2bin [symmetric])
@ -630,19 +636,19 @@ lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin
apply auto
done
lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w)"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
done
lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin_aux xs w)"
by (induct xs arbitrary: w) auto
lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin xs)"
unfolding bl_to_bin_def by (erule last_bin_last')
lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
lemma bin_last_last: "odd w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
lemma drop_bin2bl_aux:
@ -694,22 +700,22 @@ lemma bl_bin_bl_rep_drop:
by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)
lemma bl_to_bin_aux_cat:
"bl_to_bin_aux bs (bin_cat w nv v) =
bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
"bl_to_bin_aux bs (concat_bit nv v w) =
concat_bit (nv + length bs) (bl_to_bin_aux bs v) w"
by (rule bit_eqI)
(auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)
lemma bin_to_bl_aux_cat:
"bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
"bin_to_bl_aux (nv + nw) (concat_bit nw w v) bs =
bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)
lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w"
using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
by (simp add: bl_to_bin_def [symmetric])
lemma bin_to_bl_cat:
"bin_to_bl (nv + nw) (bin_cat v nw w) =
"bin_to_bl (nv + nw) (concat_bit nw w v) =
bin_to_bl_aux nv v (bin_to_bl nw w)"
by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
@ -720,15 +726,15 @@ lemmas bin_to_bl_aux_cat_app =
trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
lemma bl_to_bin_app_cat:
"bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
"bl_to_bin (bsa @ bs) = concat_bit (length bs) (bl_to_bin bs) (bl_to_bin bsa)"
by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
lemma bin_to_bl_cat_app:
"bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
"bin_to_bl (n + nw) (concat_bit nw wa w) = bin_to_bl n w @ bin_to_bl nw wa"
by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
lemma bl_to_bin_app_cat_alt: "concat_bit n w (bl_to_bin cs) = bl_to_bin (cs @ bin_to_bl n w)"
by (simp add: bl_to_bin_app_cat)
lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
@ -850,7 +856,7 @@ next
by simp
ultimately show ?case
using Suc [of \<open>bin div 2\<close>]
by simp (simp add: bin_to_bl_aux_alt)
by simp (auto simp add: bin_to_bl_aux_alt)
qed
lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
@ -858,8 +864,7 @@ lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
apply (induction n arbitrary: bin)
apply simp_all
apply (case_tac bin rule: bin_exhaust)
apply simp
apply (simp add: bin_to_bl_aux_alt ac_simps)
apply (simp_all add: bin_to_bl_aux_alt ac_simps)
done
lemma rbl_add:
@ -918,24 +923,23 @@ lemma rbl_mult:
apply clarsimp
apply (case_tac bina rule: bin_exhaust)
apply (case_tac binb rule: bin_exhaust)
apply simp
apply (simp add: bin_to_bl_aux_alt)
apply (simp add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
apply (simp_all add: bin_to_bl_aux_alt)
apply (simp_all add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
done
lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
by (induct xs) auto
by (simp add: length_concat comp_def sum_list_triv)
lemma bin_cat_foldl_lem:
"foldl (\<lambda>u. bin_cat u n) x xs =
bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
"foldl (\<lambda>u k. concat_bit n k u) x xs =
concat_bit (size xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x"
apply (induct xs arbitrary: x)
apply simp
apply (simp (no_asm))
apply (frule asm_rl)
apply (drule meta_spec)
apply (erule trans)
apply (drule_tac x = "bin_cat y n a" in meta_spec)
apply (drule_tac x = "concat_bit n a y" in meta_spec)
apply (simp add: bin_cat_assoc_sym)
done
@ -948,10 +952,10 @@ lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
apply (simp add: bin_cat_foldl_lem [symmetric])
done
lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
lemma bin_last_bl_to_bin: "odd (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])
lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)"
lemma bin_rest_bl_to_bin: "bl_to_bin bs div 2 = bl_to_bin (butlast bs)"
by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)
lemma bl_xor_aux_bin:
@ -1038,12 +1042,9 @@ lemma of_bl_eq:
lemma bshiftr1_eq:
\<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close>
apply transfer
apply auto
apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified])
apply simp
apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len)
apply (simp add: butlast_rest_bl2bin)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps to_bl_eq_rev nth_append rev_nth nth_butlast not_less simp flip: bit_Suc)
apply (metis Suc_pred len_gt_0 less_eq_decr_length_iff not_bit_length verit_la_disequality)
done
lemma length_to_bl_eq:
@ -1088,7 +1089,7 @@ lemma td_bl:
apply (auto dest: sym)
done
interpretation word_bl:
global_interpretation word_bl:
type_definition
"to_bl :: 'a::len word \<Rightarrow> bool list"
of_bl
@ -1115,12 +1116,13 @@ lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
for x :: "'a::len word"
by (fact length_bl_gt_0 [THEN gr_implies_not0])
lemma hd_to_bl_iff:
\<open>hd (to_bl w) \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close>
for w :: \<open>'a::len word\<close>
by (simp add: to_bl_eq_rev hd_map hd_rev)
lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
apply transfer
apply (auto simp add: bin_sign_def)
using bin_sign_lem bl_sbin_sign apply fastforce
using bin_sign_lem bl_sbin_sign apply force
done
by (simp add: hd_to_bl_iff bit_last_iff bin_sign_def)
lemma of_bl_drop':
"lend = length bl - LENGTH('a::len) \<Longrightarrow>
@ -1128,7 +1130,7 @@ lemma of_bl_drop':
by transfer (simp flip: trunc_bl2bin)
lemma test_bit_of_bl:
"(of_bl bl::'a::len word) !! n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)"
"bit (of_bl bl::'a::len word) n = (rev bl ! n \<and> n < LENGTH('a) \<and> n < length bl)"
by transfer (simp add: bin_nth_of_bl ac_simps)
lemma no_of_bl: "(numeral bin ::'a::len word) = of_bl (bin_to_bl (LENGTH('a)) (numeral bin))"
@ -1302,7 +1304,7 @@ lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)"
lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)"
by transfer (simp flip: bl_and_bin)
lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
lemma bin_nth_uint': "bit (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
apply (unfold word_size)
apply (safe elim!: bin_nth_uint_imp)
apply (frule bin_nth_uint_imp)
@ -1311,10 +1313,10 @@ lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (s
lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
lemma test_bit_bl: "bit w n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
by transfer (auto simp add: bin_nth_bl)
lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = bit w (size w - Suc n)"
by (simp add: word_size rev_nth test_bit_bl)
lemma map_bit_interval_eq:
@ -1328,7 +1330,7 @@ proof (rule nth_equalityI)
then have \<open>m < n\<close>
by simp
then have \<open>bit w m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size test_bit_word_eq dest: bit_imp_le_length)
by (auto simp add: nth_takefill not_less rev_nth to_bl_nth word_size dest: bit_imp_le_length)
with \<open>m < n \<close>show \<open>map (bit w) [0..<n] ! m \<longleftrightarrow> takefill False n (rev (to_bl w)) ! m\<close>
by simp
qed
@ -1395,28 +1397,37 @@ lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
lemma bshiftr1_numeral [simp]:
\<open>bshiftr1 b (numeral w :: 'a word) = of_bl (b # butlast (bin_to_bl LENGTH('a::len) (numeral w)))\<close>
by (simp add: bshiftr1_eq)
by (rule bit_word_eqI) (auto simp add: bit_simps rev_nth nth_append nth_butlast nth_bin_to_bl simp flip: bit_Suc)
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
unfolding bshiftr1_eq by (rule word_bl.Abs_inverse) simp
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
by transfer (simp add: bl_to_bin_append)
apply (rule bit_word_eqI)
apply (simp add: bit_simps)
subgoal for n
apply (cases n)
apply simp_all
done
done
lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
for w :: "'a::len word"
proof -
have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
by simp
also have "\<dots> = of_bl (to_bl w @ [False])"
by (rule shiftl1_of_bl)
finally show ?thesis .
qed
apply (rule bit_word_eqI)
apply (simp add: bit_simps)
subgoal for n
apply (cases n)
apply (simp_all add: nth_rev_to_bl)
done
done
lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
for w :: "'a::len word"
by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
lemma to_bl_double_eq:
\<open>to_bl (2 * w) = tl (to_bl w) @ [False]\<close>
using bl_shiftl1 [of w] by (simp add: shiftl1_def ac_simps)
\<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
@ -1438,7 +1449,7 @@ proof (rule bit_word_eqI)
by simp
with \<open>n < LENGTH('a)\<close> show ?thesis
by (simp add: bit_shiftr1_iff bit_of_bl_iff rev_nth nth_butlast
word_size test_bit_word_eq to_bl_nth)
word_size to_bl_nth)
qed
qed
@ -1462,45 +1473,35 @@ proof (rule nth_equalityI)
by simp
then show \<open>to_bl (sshiftr1 w) ! n \<longleftrightarrow> (hd (to_bl w) # butlast (to_bl w)) ! n\<close>
apply (cases n)
apply (simp_all add: to_bl_nth word_size hd_conv_nth test_bit_eq_bit bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
apply (simp_all add: to_bl_nth word_size hd_conv_nth bit_sshiftr1_iff nth_butlast Suc_diff_Suc nth_to_bl)
done
qed simp
lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
for w :: "'a::len word"
apply (unfold shiftr_def)
apply (induct n)
prefer 2
apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
apply (rule butlast_take [THEN trans])
apply (auto simp: word_size)
apply (rule nth_equalityI)
apply (simp_all add: word_size to_bl_nth bit_simps)
done
lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
for w :: "'a::len word"
apply (simp_all add: word_size sshiftr_eq)
apply (rule nth_equalityI)
apply (simp_all add: word_size nth_to_bl bit_signed_drop_bit_iff)
apply (simp_all add: word_size nth_to_bl bit_simps)
done
lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
apply (unfold shiftr_def)
apply (induct n)
prefer 2
apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
apply (rule take_butlast [THEN trans])
apply (auto simp: word_size)
apply (rule nth_equalityI)
apply (auto simp add: word_size to_bl_nth bit_simps dest: bit_imp_le_length)
done
lemma take_sshiftr':
"n \<le> size w \<Longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
for w :: "'a::len word"
apply (auto simp add: sshiftr_eq hd_bl_sign_sint bin_sign_def not_le word_size sint_signed_drop_bit_eq)
apply (cases n)
apply (auto simp add: hd_to_bl_iff bit_simps not_less word_size)
apply (rule nth_equalityI)
apply (auto simp add: nth_to_bl bit_signed_drop_bit_iff bit_last_iff)
apply (rule nth_equalityI)
apply (auto simp add: nth_to_bl bit_signed_drop_bit_iff bit_last_iff)
apply (auto simp add: nth_to_bl bit_simps nth_Cons split: nat.split)
done
lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
@ -1513,17 +1514,13 @@ lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps nth_append)
done
lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
for w :: "'a::len word"
proof -
have "w << n = of_bl (to_bl w) << n"
by simp
also have "\<dots> = of_bl (to_bl w @ replicate n False)"
by (rule shiftl_of_bl)
finally show ?thesis .
qed
by (simp flip: shiftl_of_bl)
lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
by (simp add: shiftl_bl word_rep_drop word_size)
@ -1531,19 +1528,16 @@ lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n)
lemma shiftr1_bl_of:
"length bl \<le> LENGTH('a) \<Longrightarrow>
shiftr1 (of_bl bl::'a::len word) = of_bl (butlast bl)"
by transfer (simp add: butlast_rest_bl2bin trunc_bl2bin)
apply (rule bit_word_eqI)
apply (simp add: bit_simps)
apply (cases bl rule: rev_cases)
apply auto
done
lemma shiftr_bl_of:
"length bl \<le> LENGTH('a) \<Longrightarrow>
(of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)"
apply (unfold shiftr_def)
apply (induct n)
apply clarsimp
apply clarsimp
apply (subst shiftr1_bl_of)
apply simp
apply (simp add: butlast_take)
done
(of_bl bl::'a::len word) >> n = of_bl (take (length bl - n) bl)"
by (rule bit_word_eqI) (auto simp add: bit_simps rev_nth)
lemma shiftr_bl: "x >> n \<equiv> of_bl (take (LENGTH('a) - n) (to_bl x))"
for x :: "'a::len word"
@ -1567,7 +1561,7 @@ lemma aligned_bl_add_size [OF refl]:
done
lemma mask_bl: "mask n = of_bl (replicate n True)"
by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
by (auto simp add: bit_simps intro!: word_eqI)
lemma bl_and_mask':
"to_bl (w AND mask n :: 'a::len word) =
@ -1575,7 +1569,7 @@ lemma bl_and_mask':
drop (LENGTH('a) - n) (to_bl w)"
apply (rule nth_equalityI)
apply simp
apply (clarsimp simp add: to_bl_nth word_size)
apply (clarsimp simp add: to_bl_nth word_size bit_simps)
apply (auto simp add: word_size test_bit_bl nth_append rev_nth)
done
@ -1771,6 +1765,8 @@ declare word_rotl_eqs (1) [simp]
lemmas abl_cong = arg_cong [where f = "of_bl"]
end
locale word_rotate
begin
@ -1823,7 +1819,7 @@ lemmas word_rotl_dt_no_bin' [simp] =
word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
(* FIXME: negative numerals, 0 and 1 *)
lemma max_word_bl: "to_bl (max_word::'a::len word) = replicate LENGTH('a) True"
lemma max_word_bl: "to_bl (- 1::'a::len word) = replicate LENGTH('a) True"
by (fact to_bl_n1)
lemma to_bl_mask:
@ -1842,6 +1838,10 @@ lemma map_replicate_False:
(zip xs (replicate n False)) = replicate n False"
by (induct xs arbitrary: n) auto
context
includes bit_operations_syntax
begin
lemma bl_and_mask:
fixes w :: "'a::len word"
and n :: nat
@ -1890,18 +1890,18 @@ lemma bin_to_bl_or:
lemma word_and_1_bl:
fixes x::"'a::len word"
shows "(x AND 1) = of_bl [x !! 0]"
by (simp add: mod_2_eq_odd test_bit_word_eq and_one_eq)
shows "(x AND 1) = of_bl [bit x 0]"
by (simp add: mod_2_eq_odd and_one_eq)
lemma word_1_and_bl:
fixes x::"'a::len word"
shows "(1 AND x) = of_bl [x !! 0]"
by (simp add: mod_2_eq_odd test_bit_word_eq one_and_eq)
shows "(1 AND x) = of_bl [bit x 0]"
by (simp add: mod_2_eq_odd one_and_eq)
lemma of_bl_drop:
"of_bl (drop n xs) = (of_bl xs AND mask (length xs - n))"
apply (clarsimp simp: bang_eq test_bit_of_bl rev_nth cong: rev_conj_cong)
apply (safe; simp add: word_size to_bl_nth)
apply (rule bit_word_eqI)
apply (auto simp: rev_nth bit_simps cong: rev_conj_cong)
done
lemma to_bl_1:
@ -1959,41 +1959,16 @@ lemma word_lsb_last:
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> LENGTH('a)")
prefer 2
apply (rule_tac x=i in exI)
apply clarsimp
apply (subgoal_tac "\<exists>j < LENGTH('a). j < n \<and> LENGTH('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 - LENGTH('a)" in exI)
apply clarsimp
apply arith
apply (rule_tac x="LENGTH('a) - n + i" in exI)
apply clarsimp
apply arith
done
by (simp add: is_aligned_mask eq_zero_set_bl bl_and_mask word_size)
lemma is_aligned_replicate:
fixes w::"'a::len word"
assumes aligned: "is_aligned w n"
and nv: "n \<le> LENGTH('a)"
shows "to_bl w = (take (LENGTH('a) - n) (to_bl w)) @ replicate n False"
proof -
from nv have rl: "\<And>q. q < 2 ^ (LENGTH('a) - n) \<Longrightarrow>
to_bl (2 ^ n * (of_nat q :: 'a word)) =
drop n (to_bl (of_nat q :: 'a word)) @ replicate n False"
by (metis bl_shiftl le_antisym min_def shiftl_t2n wsst_TYs(3))
show ?thesis using aligned
by (auto simp: rl elim: is_alignedE)
qed
apply (rule nth_equalityI)
using assms apply (simp_all add: nth_append not_less word_size to_bl_nth is_aligned_imp_not_bit)
done
lemma is_aligned_drop:
fixes w::"'a::len word"
@ -2048,9 +2023,12 @@ lemma to_bl_2p:
"n < LENGTH('a) \<Longrightarrow>
to_bl ((2::'a::len word) ^ n) =
replicate (LENGTH('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)
apply (rule nth_equalityI)
apply (auto simp add: nth_append to_bl_nth word_size bit_simps not_less nth_Cons le_diff_conv)
subgoal for i
apply (cases \<open>Suc (i + n) - LENGTH('a)\<close>)
apply simp_all
done
done
lemma xor_2p_to_bl:
@ -2059,22 +2037,10 @@ lemma xor_2p_to_bl:
(if n < LENGTH('a)
then take (LENGTH('a)-Suc n) (to_bl x) @ (\<not>rev (to_bl x)!n) # drop (LENGTH('a)-n) (to_bl x)
else to_bl x)"
proof -
have x: "to_bl x = take (LENGTH('a)-Suc n) (to_bl x) @ drop (LENGTH('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 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)
apply (auto simp add: to_bl_eq_rev take_map drop_map take_rev drop_rev bit_simps)
apply (rule nth_equalityI)
apply (auto simp add: bit_simps rev_nth nth_append Suc_diff_Suc)
done
qed
lemma is_aligned_replicateD:
"\<lbrakk> is_aligned (w::'a::len word) n; n \<le> LENGTH('a) \<rbrakk>
@ -2120,7 +2086,7 @@ lemma of_bl_mult_and_not_mask_eq:
lemma bin_to_bl_of_bl_eq:
"\<lbrakk>is_aligned (a::'a::len word) n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk>
\<Longrightarrow> bin_to_bl (length b) (uint ((a + of_bl b * 2^c) >> c)) = b"
apply (simp flip: push_bit_eq_mult take_bit_eq_mask add: shiftr_eq_drop_bit)
apply (simp flip: push_bit_eq_mult take_bit_eq_mask)
apply (subst disjunctive_add)
apply (auto simp add: bit_simps not_le not_less unsigned_or_eq unsigned_drop_bit_eq
unsigned_push_bit_eq bin_to_bl_or simp flip: bin_to_bl_def)
@ -2130,15 +2096,6 @@ lemma bin_to_bl_of_bl_eq:
apply (auto simp add: nth_bin_to_bl bit_simps rev_nth simp flip: bin_to_bl_def)
done
(* FIXME: move to Word distribution *)
lemma bin_nth_minus_Bit0[simp]:
"0 < n \<Longrightarrow> bin_nth (numeral (num.Bit0 w)) n = bin_nth (numeral w) (n - 1)"
by (cases n; simp)
lemma bin_nth_minus_Bit1[simp]:
"0 < n \<Longrightarrow> bin_nth (numeral (num.Bit1 w)) n = bin_nth (numeral w) (n - 1)"
by (cases n; simp)
(* casting a long word to a shorter word and casting back to the long word
is equal to the original long word -- if the word is small enough.
'l is the longer word.
@ -2174,7 +2131,7 @@ proof -
qed
lemma map_bits_rev_to_bl:
"map ((!!) x) [0..<size x] = rev (to_bl x)"
"map (bit x) [0..<size x] = rev (to_bl x)"
by (auto simp: list_eq_iff_nth_eq test_bit_bl word_size)
lemma of_bl_length2:
@ -2193,4 +2150,91 @@ proof -
by simp
qed
text\<open>Some auxiliaries for sign-shifting by the entire word length or more\<close>
lemma sshiftr_clamp_pos:
assumes
"LENGTH('a) \<le> n"
"0 \<le> sint x"
shows "(x::'a::len word) >>> n = 0"
apply (rule bit_word_eqI)
using assms
apply (auto simp add: bit_simps bit_last_iff)
done
lemma sshiftr_clamp_neg:
assumes
"LENGTH('a) \<le> n"
"sint x < 0"
shows "(x::'a::len word) >>> n = -1"
apply (rule bit_word_eqI)
using assms
apply (auto simp add: bit_simps bit_last_iff)
done
lemma sshiftr_clamp:
assumes "LENGTH('a) \<le> n"
shows "(x::'a::len word) >>> n = x >>> LENGTH('a)"
apply (rule bit_word_eqI)
using assms
apply (auto simp add: bit_simps bit_last_iff)
done
text\<open>
Like @{thm shiftr1_bl_of}, but the precondition is stronger because we need to pick the msb out of
the list.
\<close>
lemma sshiftr1_bl_of:
"length bl = LENGTH('a) \<Longrightarrow>
sshiftr1 (of_bl bl::'a::len word) = of_bl (hd bl # butlast bl)"
apply (rule word_bl.Rep_eqD)
apply (subst bl_sshiftr1[of "of_bl bl :: 'a word"])
by (simp add: word_bl.Abs_inverse)
text\<open>
Like @{thm sshiftr1_bl_of}, with a weaker precondition.
We still get a direct equation for @{term \<open>sshiftr1 (of_bl bl)\<close>}, it's just uglier.
\<close>
lemma sshiftr1_bl_of':
"LENGTH('a) \<le> length bl \<Longrightarrow>
sshiftr1 (of_bl bl::'a::len word) =
of_bl (hd (drop (length bl - LENGTH('a)) bl) # butlast (drop (length bl - LENGTH('a)) bl))"
apply (subst of_bl_drop'[symmetric, of "length bl - LENGTH('a)"])
using sshiftr1_bl_of[of "drop (length bl - LENGTH('a)) bl"]
by auto
text\<open>
Like @{thm shiftr_bl_of}.
\<close>
lemma sshiftr_bl_of:
assumes "length bl = LENGTH('a)"
shows "(of_bl bl::'a::len word) >>> n = of_bl (replicate n (hd bl) @ take (length bl - n) bl)"
proof -
from assms obtain b bs where \<open>bl = b # bs\<close>
by (cases bl) simp_all
then have *: \<open>bl ! 0 \<longleftrightarrow> b\<close> \<open>hd bl \<longleftrightarrow> b\<close>
by simp_all
show ?thesis
apply (rule bit_word_eqI)
using assms * by (auto simp add: bit_simps nth_append rev_nth not_less)
qed
text\<open>Like @{thm shiftr_bl}\<close>
lemma sshiftr_bl: "x >>> n \<equiv> of_bl (replicate n (msb x) @ take (LENGTH('a) - n) (to_bl x))"
for x :: "'a::len word"
unfolding word_msb_alt
by (smt (z3) length_to_bl_eq sshiftr_bl_of word_bl.Rep_inverse)
end
lemma of_bl_drop_eq_take_bit:
\<open>of_bl (drop n xs) = take_bit (length xs - n) (of_bl xs)\<close>
by (simp add: of_bl_drop take_bit_eq_mask)
lemma of_bl_take_to_bl_eq_drop_bit:
\<open>of_bl (take n (to_bl w)) = drop_bit (LENGTH('a) - n) w\<close>
if \<open>n \<le> LENGTH('a)\<close>
for w :: \<open>'a::len word\<close>
using that shiftr_bl [of w \<open>LENGTH('a) - n\<close>] by (simp add: shiftr_def)
end

33
lib/Word_Lib/Rsplit.thy
View File

@ -6,12 +6,14 @@
(* Author: Jeremy Dawson and Gerwin Klein, NICTA *)
section \<open>Splitting words into lists\<close>
theory Rsplit
imports "HOL-Library.Word" Bits_Int
imports "HOL-Library.Word" More_Word Bits_Int
begin
definition word_rsplit :: "'a::len word \<Rightarrow> 'b::len word list"
where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
where "word_rsplit w = map word_of_int (bin_rsplit LENGTH('b) (LENGTH('a), uint w))"
lemma word_rsplit_no:
"(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) =
@ -39,11 +41,11 @@ lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size
lemma test_bit_rsplit:
"sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
k < length sw \<Longrightarrow> bit (rev sw ! k) m = bit w (k * size (hd sw) + m)"
for sw :: "'a::len word list"
apply (unfold word_rsplit_def word_test_bit_def)
apply (rule trans)
apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
apply (rule_tac f = "\<lambda>x. bit x m" in arg_cong)
apply (rule nth_map [symmetric])
apply simp
apply (rule bin_nth_rsplit)
@ -53,12 +55,12 @@ lemma test_bit_rsplit:
defer
apply (rule map_ident [THEN fun_cong])
apply (rule refl [THEN map_cong])
apply simp
apply (simp add: unsigned_of_int take_bit_int_eq_self_iff)
using bin_rsplit_size_sign take_bit_int_eq_self_iff by blast
lemma test_bit_rsplit_alt:
\<open>(word_rsplit w :: 'b::len word list) ! i !! m \<longleftrightarrow>
w !! ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
\<open>bit ((word_rsplit w :: 'b::len word list) ! i) m \<longleftrightarrow>
bit w ((length (word_rsplit w :: 'b::len word list) - Suc i) * size (hd (word_rsplit w :: 'b::len word list)) + m)\<close>
if \<open>i < length (word_rsplit w :: 'b::len word list)\<close> \<open>m < size (hd (word_rsplit w :: 'b::len word list))\<close> \<open>0 < length (word_rsplit w :: 'b::len word list)\<close>
for w :: \<open>'a::len word\<close>
apply (rule trans)
@ -120,12 +122,6 @@ lemma size_word_rsplit_rcat_size:
for ws :: "'a::len word list" and frcw :: "'b::len word"
by (cases \<open>LENGTH('a)\<close>) (simp_all add: word_size length_word_rsplit_exp_size' div_nat_eqI)
lemma msrevs:
"0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
"(k * n + m) mod n = m mod n"
for n :: nat
by (auto simp: add.commute)
lemma word_rsplit_rcat_size [OF refl]:
"word_rcat ws = frcw \<Longrightarrow>
size frcw = length ws * LENGTH('a) \<Longrightarrow> word_rsplit frcw = ws"
@ -152,15 +148,16 @@ lemma word_rsplit_rcat_size [OF refl]:
lemma word_rsplit_upt:
"\<lbrakk> size x = LENGTH('a :: len) * n; n \<noteq> 0 \<rbrakk>
\<Longrightarrow> word_rsplit x = map (\<lambda>i. ucast (x >> i * len_of TYPE ('a)) :: 'a word) (rev [0 ..< n])"
\<Longrightarrow> word_rsplit x = map (\<lambda>i. ucast (x >> (i * LENGTH('a))) :: 'a word) (rev [0 ..< n])"
apply (subgoal_tac "length (word_rsplit x :: 'a word list) = n")
apply (rule nth_equalityI, simp)
apply (intro allI word_eqI impI)
apply (simp add: test_bit_rsplit_alt word_size)
apply (simp add: nth_ucast nth_shiftr rev_nth field_simps)
apply (simp add: length_word_rsplit_exp_size)
apply transfer
apply (metis (no_types, lifting) Nat.add_diff_assoc Suc_leI add_0_left diff_Suc_less div_less len_gt_0 msrevs(1) mult.commute)
apply (simp add: nth_ucast bit_simps rev_nth field_simps)
apply (simp add: length_word_rsplit_exp_size word_size)
apply (subst diff_add_assoc)
apply (simp flip: less_eq_Suc_le)
apply simp
done
end

119
lib/Word_Lib/Signed_Division_Word.thy
View File

@ -52,6 +52,15 @@ lemma signed_mod_arith:
apply simp
done
lemma word_sdiv_div0 [simp]:
"(a :: ('a::len) word) sdiv 0 = 0"
apply (auto simp: sdiv_word_def signed_divide_int_def sgn_if)
done
lemma smod_word_zero [simp]:
\<open>w smod 0 = w\<close> for w :: \<open>'a::len word\<close>
by (simp add: smod_word_def signed_modulo_int_def)
lemma word_sdiv_div1 [simp]:
"(a :: ('a::len) word) sdiv 1 = a"
apply (cases \<open>LENGTH('a)\<close>)
@ -63,10 +72,9 @@ lemma word_sdiv_div1 [simp]:
apply (simp add: take_bit_signed_take_bit)
done
lemma word_sdiv_div0 [simp]:
"(a :: ('a::len) word) sdiv 0 = 0"
apply (auto simp: sdiv_word_def signed_divide_int_def sgn_if)
done
lemma smod_word_one [simp]:
\<open>w smod 1 = 0\<close> for w :: \<open>'a::len word\<close>
by (simp add: smod_word_def signed_modulo_int_def)
lemma word_sdiv_div_minus1 [simp]:
"(a :: ('a::len) word) sdiv -1 = -a"
@ -76,6 +84,78 @@ lemma word_sdiv_div_minus1 [simp]:
apply (metis Suc_pred len_gt_0 signed_take_bit_eq_iff_take_bit_eq signed_take_bit_of_0 take_bit_of_0)
done
lemma smod_word_minus_one [simp]:
\<open>w smod - 1 = 0\<close> for w :: \<open>'a::len word\<close>
by (simp add: smod_word_def signed_modulo_int_def)
lemma one_sdiv_word_eq [simp]:
\<open>1 sdiv w = of_bool (w = 1 \<or> w = - 1) * w\<close> for w :: \<open>'a::len word\<close>
proof (cases \<open>1 < \<bar>sint w\<bar>\<close>)
case True
then show ?thesis
by (auto simp add: sdiv_word_def signed_divide_int_def split: if_splits)
next
case False
then have \<open>\<bar>sint w\<bar> \<le> 1\<close>
by simp
then have \<open>sint w \<in> {- 1, 0, 1}\<close>
by auto
then have \<open>(word_of_int (sint w) :: 'a::len word) \<in> word_of_int ` {- 1, 0, 1}\<close>
by blast
then have \<open>w \<in> {- 1, 0, 1}\<close>
by simp
then show ?thesis by auto
qed
lemma one_smod_word_eq [simp]:
\<open>1 smod w = 1 - of_bool (w = 1 \<or> w = - 1)\<close> for w :: \<open>'a::len word\<close>
using sdiv_smod_id [of 1 w] by auto
lemma minus_one_sdiv_word_eq [simp]:
\<open>- 1 sdiv w = - (1 sdiv w)\<close> for w :: \<open>'a::len word\<close>
apply (auto simp add: sdiv_word_def signed_divide_int_def)
apply transfer
apply simp
done
lemma minus_one_smod_word_eq [simp]:
\<open>- 1 smod w = - (1 smod w)\<close> for w :: \<open>'a::len word\<close>
using sdiv_smod_id [of \<open>- 1\<close> w] by auto
lemma smod_word_alt_def:
"(a :: ('a::len) word) smod b = a - (a sdiv b) * b"
apply (cases \<open>a \<noteq> - (2 ^ (LENGTH('a) - 1)) \<or> b \<noteq> - 1\<close>)
apply (clarsimp simp: smod_word_def sdiv_word_def signed_modulo_int_def
simp flip: wi_hom_sub wi_hom_mult)
apply (clarsimp simp: smod_word_def signed_modulo_int_def)
done
lemmas sdiv_word_numeral_numeral [simp] =
sdiv_word_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas sdiv_word_minus_numeral_numeral [simp] =
sdiv_word_def [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas sdiv_word_numeral_minus_numeral [simp] =
sdiv_word_def [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas sdiv_word_minus_numeral_minus_numeral [simp] =
sdiv_word_def [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_numeral_numeral [simp] =
smod_word_def [of \<open>numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_minus_numeral_numeral [simp] =
smod_word_def [of \<open>- numeral a\<close> \<open>numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_numeral_minus_numeral [simp] =
smod_word_def [of \<open>numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_minus_numeral_minus_numeral [simp] =
smod_word_def [of \<open>- numeral a\<close> \<open>- numeral b\<close>, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas word_sdiv_0 = word_sdiv_div0
lemma sdiv_word_min:
@ -93,15 +173,34 @@ lemma sdiv_word_min:
apply (metis abs_le_iff add.inverse_inverse le_cases le_minus_iff not_le signed_take_bit_int_eq_self_iff signed_take_bit_minus)
done
lemma sdiv_word_max:
\<open>sint a sdiv sint b \<le> 2 ^ (size a - Suc 0)\<close>
for a b :: \<open>'a::len word\<close>
proof (cases \<open>sint a = 0 \<or> sint b = 0 \<or> sgn (sint a) \<noteq> sgn (sint b)\<close>)
case True then show ?thesis
apply (auto simp add: sgn_if not_less signed_divide_int_def split: if_splits)
apply (smt (z3) pos_imp_zdiv_neg_iff zero_le_power)
apply (smt (z3) not_exp_less_eq_0_int pos_imp_zdiv_neg_iff)
done
next
case False
then have \<open>\<bar>sint a\<bar> div \<bar>sint b\<bar> \<le> \<bar>sint a\<bar>\<close>
by (subst nat_le_eq_zle [symmetric]) (simp_all add: div_abs_eq_div_nat)
also have \<open>\<bar>sint a\<bar> \<le> 2 ^ (size a - Suc 0)\<close>
using sint_range_size [of a] by auto
finally show ?thesis
using False by (simp add: signed_divide_int_def)
qed
lemmas word_sdiv_numerals_lhs = sdiv_word_def[where v="numeral x" for x]
sdiv_word_def[where v=0] sdiv_word_def[where v=1]
lemmas word_sdiv_numerals = word_sdiv_numerals_lhs[where w="numeral y" for y]
word_sdiv_numerals_lhs[where w=0] word_sdiv_numerals_lhs[where w=1]
lemma smod_word_mod_0 [simp]:
lemma smod_word_mod_0:
"x smod (0 :: ('a::len) word) = x"
by (clarsimp simp: smod_word_def)
by (fact smod_word_zero)
lemma smod_word_0_mod [simp]:
"0 smod (x :: ('a::len) word) = 0"
@ -139,14 +238,6 @@ lemma smod_word_min:
apply (metis abs_zero add.inverse_inverse add.left_neutral add_mono_thms_linordered_semiring(1) diff_Suc_1 le_cases le_minus_iff linorder_not_less sint_ge zabs_less_one_iff)
done
lemma smod_word_alt_def:
"(a :: ('a::len) word) smod b = a - (a sdiv b) * b"
apply (cases \<open>a \<noteq> - (2 ^ (LENGTH('a) - 1)) \<or> b \<noteq> - 1\<close>)
apply (clarsimp simp: smod_word_def sdiv_word_def signed_modulo_int_def
simp flip: wi_hom_sub wi_hom_mult)
apply (clarsimp simp: smod_word_def signed_modulo_int_def)
done
lemmas word_smod_numerals_lhs = smod_word_def[where v="numeral x" for x]
smod_word_def[where v=0] smod_word_def[where v=1]

17
lib/Word_Lib/Signed_Words.thy
View File

@ -81,7 +81,7 @@ lemma word_le_ucast_sless:
apply simp_all
apply transfer
apply (simp add: signed_take_bit_take_bit)
apply (metis add.commute mask_eq_exp_minus_1 mask_eq_take_bit_minus_one take_bit_incr_eq zle_add1_eq_le)
apply (metis add.commute mask_eq_exp_minus_1 take_bit_incr_eq zle_add1_eq_le)
done
lemma zero_sle_ucast:
@ -93,6 +93,21 @@ lemma zero_sle_ucast:
apply (simp_all add: bit_simps disjunctive_add)
done
lemma nth_w2p_scast:
"(bit (scast ((2::'a::len signed word) ^ n) :: 'a word) m)
\<longleftrightarrow> (bit (((2::'a::len word) ^ n) :: 'a word) m)"
by (simp add: bit_simps)
lemma scast_nop1 [simp]:
"((scast ((of_int x)::('a::len) word))::'a signed word) = of_int x"
by transfer (simp add: take_bit_signed_take_bit)
lemma scast_nop2 [simp]:
"((scast ((of_int x)::('a::len) signed word))::'a word) = of_int x"
by transfer (simp add: take_bit_signed_take_bit)
lemmas scast_nop = scast_nop1 scast_nop2 scast_id
type_synonym 'a sword = "'a signed word"
end

148
lib/Word_Lib/Singleton_Bit_Shifts.thy Normal file
View File

@ -0,0 +1,148 @@
theory Singleton_Bit_Shifts
imports
"HOL-Library.Word"
Bit_Shifts_Infix_Syntax
begin
definition shiftl1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>shiftl1 = push_bit 1\<close>
lemma bit_shiftl1_iff [bit_simps]:
\<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
for w :: \<open>'a::len word\<close>
by (simp only: shiftl1_def bit_push_bit_iff) auto
definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>shiftr1 = drop_bit 1\<close>
lemma bit_shiftr1_iff [bit_simps]:
\<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
for w :: \<open>'a::len word\<close>
by (simp add: shiftr1_def bit_drop_bit_eq)
definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
where \<open>sshiftr1 \<equiv> signed_drop_bit 1\<close>
lemma bit_sshiftr1_iff [bit_simps]:
\<open>bit (sshiftr1 w) n \<longleftrightarrow> bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)\<close>
for w :: \<open>'a::len word\<close>
by (auto simp add: sshiftr1_def bit_signed_drop_bit_iff)
lemma shiftr1_1: "shiftr1 (1::'a::len word) = 0"
by (simp add: shiftr1_def)
lemma sshiftr1_eq:
\<open>sshiftr1 w = word_of_int (sint w div 2)\<close>
by (rule bit_word_eqI) (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)
lemma shiftl1_eq:
\<open>shiftl1 w = word_of_int (2 * uint w)\<close>
by (rule bit_word_eqI) (auto simp add: bit_simps)
lemma shiftr1_eq:
\<open>shiftr1 w = word_of_int (uint w div 2)\<close>
by (rule bit_word_eqI) (simp add: bit_simps flip: bit_Suc)
lemma shiftl1_rev:
"shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
by (rule bit_word_eqI) (auto simp add: bit_simps Suc_diff_Suc simp flip: bit_Suc)
lemma shiftl1_p:
"shiftl1 w = w + w"
for w :: "'a::len word"
by (simp add: shiftl1_def)
lemma shiftr1_bintr:
"(shiftr1 (numeral w) :: 'a::len word) =
word_of_int (take_bit LENGTH('a) (numeral w) div 2)"
by (rule bit_word_eqI) (simp add: bit_simps bit_numeral_iff [where ?'a = int] flip: bit_Suc)
lemma sshiftr1_sbintr:
"(sshiftr1 (numeral w) :: 'a::len word) =
word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)"
apply (cases \<open>LENGTH('a)\<close>)
apply simp_all
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)
done
lemma shiftl1_wi:
"shiftl1 (word_of_int w) = word_of_int (2 * w)"
by (rule bit_word_eqI) (auto simp add: bit_simps)
lemma shiftl1_numeral:
"shiftl1 (numeral w) = numeral (Num.Bit0 w)"
unfolding word_numeral_alt shiftl1_wi by simp
lemma shiftl1_neg_numeral:
"shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
unfolding word_neg_numeral_alt shiftl1_wi by simp
lemma shiftl1_0:
"shiftl1 0 = 0"
by (simp add: shiftl1_def)
lemma shiftl1_def_u:
"shiftl1 w = word_of_int (2 * uint w)"
by (fact shiftl1_eq)
lemma shiftl1_def_s:
"shiftl1 w = word_of_int (2 * sint w)"
by (simp add: shiftl1_def)
lemma shiftr1_0:
"shiftr1 0 = 0"
by (simp add: shiftr1_def)
lemma sshiftr1_0:
"sshiftr1 0 = 0"
by (simp add: sshiftr1_def)
lemma sshiftr1_n1:
"sshiftr1 (- 1) = - 1"
by (simp add: sshiftr1_def)
lemma uint_shiftr1:
"uint (shiftr1 w) = uint w div 2"
by (rule bit_eqI) (simp add: bit_simps flip: bit_Suc)
lemma shiftr1_div_2:
"uint (shiftr1 w) = uint w div 2"
by (fact uint_shiftr1)
lemma sshiftr1_div_2:
"sint (sshiftr1 w) = sint w div 2"
by (rule bit_eqI) (auto simp add: bit_simps ac_simps min_def simp flip: bit_Suc elim: le_SucE)
lemma nth_shiftl1:
"bit (shiftl1 w) n \<longleftrightarrow> n < size w \<and> n > 0 \<and> bit w (n - 1)"
by (auto simp add: word_size bit_simps)
lemma nth_shiftr1:
"bit (shiftr1 w) n = bit w (Suc n)"
by (fact bit_shiftr1_iff)
lemma nth_sshiftr1: "bit (sshiftr1 w) n = (if n = size w - 1 then bit w n else bit w (Suc n))"
by (auto simp add: word_size bit_simps)
lemma shiftl_power:
"(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y"
by (induction x) (simp_all add: shiftl1_def)
lemma le_shiftr1:
\<open>shiftr1 u \<le> shiftr1 v\<close> if \<open>u \<le> v\<close>
using that by (simp add: word_le_nat_alt unat_div div_le_mono shiftr1_def drop_bit_Suc)
lemma le_shiftr1':
"\<lbrakk> shiftr1 u \<le> shiftr1 v ; shiftr1 u \<noteq> shiftr1 v \<rbrakk> \<Longrightarrow> u \<le> v"
by (meson dual_order.antisym le_cases le_shiftr1)
lemma sshiftr_eq_funpow_sshiftr1:
\<open>w >>> n = (sshiftr1 ^^ n) w\<close>
apply (rule sym)
apply (simp add: sshiftr1_def sshiftr_def)
apply (induction n)
apply simp_all
done
end

2
lib/Word_Lib/Strict_part_mono.thy
View File

@ -28,7 +28,7 @@ lemma strict_part_mono_singleton[simp]:
lemma strict_part_mono_lt:
"\<lbrakk> x < f 0; strict_part_mono {.. n :: nat} f \<rbrakk> \<Longrightarrow> \<forall>m \<le> n. x < f m"
by (metis atMost_iff le_0_eq le_cases neq0_conv order.strict_trans strict_part_mono_def)
by (auto simp add: strict_part_mono_def Ball_def intro: order.strict_trans)
lemma strict_part_mono_reverseE:
"\<lbrakk> f n \<le> f m; strict_part_mono {.. N :: nat} f; n \<le> N \<rbrakk> \<Longrightarrow> n \<le> m"

20
lib/Word_Lib/Syntax_Bundles.thy Normal file
View File

@ -0,0 +1,20 @@
(*
* Copyright Florian Haftmann
*
* SPDX-License-Identifier: BSD-2-Clause
*)
section \<open>Syntax bundles for traditional infix syntax\<close>
theory Syntax_Bundles
imports "HOL-Library.Word"
begin
bundle bit_projection_infix_syntax
begin
notation bit (infixl \<open>!!\<close> 100)
end
end

1085
lib/Word_Lib/Traditional_Infix_Syntax.thy
View File

File diff suppressed because it is too large Load Diff

2
lib/Word_Lib/Type_Syntax.thy
View File

@ -18,7 +18,7 @@ struct
fun tr' cnst ctxt typ ts = if Config.get ctxt show_word_types then
case (Term.binder_types typ, Term.body_type typ) of
([Type (@{type_name "word"}, [S])], Type (@{type_name "word"}, [T])) =>
([\<^Type>\<open>word S\<close>], \<^Type>\<open>word T\<close>) =>
list_comb
(Syntax.const cnst $ Syntax_Phases.term_of_typ ctxt S $ Syntax_Phases.term_of_typ ctxt T
, ts)

38
lib/Word_Lib/Typedef_Morphisms.thy
View File

@ -292,7 +292,7 @@ lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))"
for z :: "'a::len word"
apply (unfold unats_def)
apply clarsimp
apply (rule xtrans, rule unat_lt2p, assumption)
apply (metis le_unat_uoi unsigned_less)
done
lemma td_ext_sbin:
@ -346,11 +346,11 @@ lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
interpretation test_bit:
td_ext
"(!!) :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool"
"bit :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool"
set_bits
"{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len)}"
"(\<lambda>h i. h i \<and> i < LENGTH('a::len))"
by standard (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
by standard (auto simp add: bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
lemmas td_nth = test_bit.td_thm
@ -365,4 +365,36 @@ lemma sints_subset:
apply simp
done
lemma uints_mono_iff: "uints l \<subseteq> uints m \<longleftrightarrow> l \<le> m"
using power_increasing_iff[of "2::int" l m]
apply (auto simp: uints_num subset_iff simp del: power_increasing_iff)
apply (meson less_irrefl not_le zero_le_numeral zero_le_power)
done
lemmas uints_monoI = uints_mono_iff[THEN iffD2]
lemma Bit_in_uints_Suc: "of_bool c + 2 * w \<in> uints (Suc m)" if "w \<in> uints m"
using that
by (auto simp: uints_num)
lemma Bit_in_uintsI: "of_bool c + 2 * w \<in> uints m" if "w \<in> uints (m - 1)" "m > 0"
using Bit_in_uints_Suc[OF that(1)] that(2)
by auto
lemma bin_cat_in_uintsI:
\<open>concat_bit n b a \<in> uints m\<close> if \<open>a \<in> uints l\<close> \<open>m \<ge> l + n\<close>
proof -
from \<open>m \<ge> l + n\<close> obtain q where \<open>m = l + n + q\<close>
using le_Suc_ex by blast
then have \<open>(2::int) ^ m = 2 ^ n * 2 ^ (l + q)\<close>
by (simp add: ac_simps power_add)
moreover have \<open>a mod 2 ^ (l + q) = a\<close>
using \<open>a \<in> uints l\<close>
by (auto simp add: uints_def take_bit_eq_mod power_add Divides.mod_mult2_eq)
ultimately have \<open>concat_bit n b a = take_bit m (concat_bit n b a)\<close>
by (simp add: concat_bit_eq take_bit_eq_mod push_bit_eq_mult Divides.mod_mult2_eq)
then show ?thesis
by (simp add: uints_def)
qed
end

6
lib/Word_Lib/Word_16.thy
View File

@ -14,9 +14,15 @@ begin
lemma len16: "len_of (x :: 16 itself) = 16" by simp
context
includes bit_operations_syntax
begin
lemma word16_and_max_simp:
\<open>x AND 0xFFFF = x\<close> for x :: \<open>16 word\<close>
using word_and_full_mask_simp [of x]
by (simp add: numeral_eq_Suc mask_Suc_exp)
end
end

180
lib/Word_Lib/Word_32.thy
View File

@ -16,207 +16,56 @@ theory Word_32
Bitwise
begin
context
includes bit_operations_syntax
begin
type_synonym word32 = "32 word"
lemma len32: "len_of (x :: 32 itself) = 32" by simp
type_synonym sword32 = "32 sword"
type_synonym machine_word_len = 32
type_synonym machine_word = "machine_word_len word"
definition word_bits :: nat
where
"word_bits = LENGTH(machine_word_len)"
text \<open>The following two are numerals so they can be used as nats and words.\<close>
definition word_size_bits :: "'a :: numeral"
where
"word_size_bits = 2"
definition word_size :: "'a :: numeral"
where
"word_size = 4"
lemma word_bits_conv[code]:
"word_bits = 32"
unfolding word_bits_def by simp
lemma word_size_word_size_bits:
"(word_size::nat) = 2 ^ word_size_bits"
unfolding word_size_def word_size_bits_def by simp
lemma word_bits_word_size_conv:
"word_bits = word_size * 8"
unfolding word_bits_def word_size_def by simp
lemma ucast_8_32_inj:
"inj (ucast :: 8 word \<Rightarrow> 32 word)"
by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)
lemma upto_2_helper:
"{0..<2 :: 32 word} = {0, 1}"
by (safe; simp) unat_arith
lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def]
lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def]
lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def]
lemma word_bits_len_of:
"len_of TYPE (32) = word_bits"
by (simp add: word_bits_conv)
lemmas unat_power_lower32' = unat_power_lower[where 'a=32]
lemmas unat_power_lower32 [simp] = unat_power_lower32'[unfolded word_bits_len_of]
lemmas word32_less_sub_le' = word_less_sub_le[where 'a = 32]
lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def]
lemma word_bits_size:
"size (w::word32) = word_bits"
by (simp add: word_bits_def word_size)
lemmas word32_power_less_1' = word_power_less_1[where 'a = 32]
lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def]
lemma of_nat32_0:
"\<lbrakk>of_nat n = (0::word32); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
by (erule of_nat_0, simp add: word_bits_def)
lemma unat_mask_2_less_4:
"unat (p && mask 2 :: word32) < 4"
apply (rule unat_less_helper)
apply (rule order_le_less_trans, rule word_and_le1)
apply (simp add: mask_eq)
done
lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32]
lemmas unat_of_nat32 = unat_of_nat32'[unfolded word_bits_len_of]
lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def]
lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 32, unfolded word_bits_len_of]]
lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def]
lemma n_less_word_bits:
"(n < word_bits) = (n < 32)"
by (simp add: word_bits_def)
lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def]
lemma lt_word_bits_lt_pow:
"sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
by (simp add: word_bits_conv)
lemma unat_less_word_bits:
fixes y :: word32
shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
unfolding word_bits_def
by (rule order_less_trans [OF _ unat_lt2p])
lemmas unat_mask_word32' = unat_mask[where 'a=32]
lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def]
lemma unat_less_2p_word_bits:
"unat (x :: 32 word) < 2 ^ word_bits"
apply (simp only: word_bits_def)
apply (rule unat_lt2p)
done
lemma Suc_unat_mask_div:
"Suc (unat (mask sz div word_size::word32)) = 2 ^ (min sz word_bits - 2)"
apply (case_tac "sz < word_bits")
apply (case_tac "2 \<le> sz")
apply (clarsimp simp: word_size_def word_bits_def min_def mask_eq)
apply (drule (2) Suc_div_unat_helper
[where 'a=32 and sz=sz and us=2, simplified, symmetric])
apply (simp add: not_le word_size_def word_bits_def)
apply (case_tac sz, simp add: unat_word_ariths)
apply (case_tac nat, simp add: unat_word_ariths
unat_mask_word32 min_def word_bits_def)
apply simp
apply (simp add: unat_word_ariths
unat_mask_word32 min_def word_bits_def word_size_def)
done
lemmas word32_minus_one_le' = word_minus_one_le[where 'a=32]
lemmas word32_minus_one_le = word32_minus_one_le'[simplified]
lemma ucast_not_helper:
fixes a::"8 word"
assumes a: "a \<noteq> 0xFF"
shows "ucast a \<noteq> (0xFF::word32)"
proof
assume "ucast a = (0xFF::word32)"
also
have "(0xFF::word32) = ucast (0xFF::8 word)" by simp
finally
show False using a
apply -
apply (drule up_ucast_inj, simp)
apply simp
done
qed
lemma less_4_cases:
"(x::word32) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
apply clarsimp
apply (drule word_less_cases, erule disjE, simp, simp)+
done
lemma unat_ucast_8_32:
fixes x :: "8 word"
shows "unat (ucast x :: word32) = unat x"
by transfer simp
lemma if_then_1_else_0:
"((if P then 1 else 0) = (0 :: word32)) = (\<not> P)"
by simp
lemma if_then_0_else_1:
"((if P then 0 else 1) = (0 :: word32)) = (P)"
by simp
lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
lemma ucast_le_ucast_8_32:
"(ucast x \<le> (ucast y :: word32)) = (x \<le> (y :: 8 word))"
by (simp add: ucast_le_ucast)
lemma in_16_range:
"0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word32)) ` S"
"n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word32. r + x * 16) ` S"
by (clarsimp simp: image_def elim!: bexI[rotated])+
lemma eq_2_32_0:
"(2 ^ 32 :: word32) = 0"
by simp
lemma x_less_2_0_1:
fixes x :: word32 shows
"x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
by (rule x_less_2_0_1') auto
lemmas mask_32_max_word = max_word_mask [symmetric, where 'a=32, simplified]
lemma of_nat32_n_less_equal_power_2:
"n < 32 \<Longrightarrow> ((of_nat n)::32 word) < 2 ^ n"
by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)
lemma word_rsplit_0:
"word_rsplit (0 :: word32) = [0, 0, 0, 0 :: 8 word]"
by (simp add: word_rsplit_def bin_rsplit_def)
lemma unat_ucast_10_32 :
fixes x :: "10 word"
shows "unat (ucast x :: word32) = unat x"
by transfer simp
lemma bool_mask [simp]:
fixes x :: word32
shows "(0 < x && 1) = (x && 1 = 1)"
by (rule bool_mask') auto
lemma word32_bounds:
"- (2 ^ (size (x :: word32) - 1)) = (-2147483648 :: int)"
"((2 ^ (size (x :: word32) - 1)) - 1) = (2147483647 :: int)"
@ -224,9 +73,6 @@ lemma word32_bounds:
"((2 ^ (size (y :: 32 signed word) - 1)) - 1) = (2147483647 :: int)"
by (simp_all add: word_size)
lemma word_ge_min:"sint (x::32 word) \<ge> -2147483648"
by (metis sint_ge word32_bounds(1) word_size)
lemmas signed_arith_ineq_checks_to_eq_word32'
= signed_arith_ineq_checks_to_eq[where 'a=32]
signed_arith_ineq_checks_to_eq[where 'a="32 signed"]
@ -256,7 +102,7 @@ lemma ucast_of_nats [simp]:
"(ucast (of_nat x :: 16 word) :: 16 sword) = (of_nat x)"
"(ucast (of_nat x :: 16 word) :: 8 sword) = (of_nat x)"
"(ucast (of_nat x :: 8 word) :: 8 sword) = (of_nat x)"
by (simp_all add: of_nat_take_bit take_bit_word_eq_self)
by (simp_all add: of_nat_take_bit take_bit_word_eq_self unsigned_of_nat)
lemmas signed_shift_guard_simpler_32'
= power_strict_increasing_iff[where b="2 :: nat" and y=31]
@ -271,15 +117,6 @@ lemmas signed_shift_guard_to_word_32
= signed_shift_guard_to_word[OF word32_31_less(1-2)]
signed_shift_guard_to_word[OF word32_31_less(3-4)]
lemma le_step_down_word_3:
fixes x :: "32 word"
shows "\<lbrakk>x \<le> y; x \<noteq> y; y < 2 ^ 32 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1"
by (rule le_step_down_word_2, assumption+)
lemma shiftr_1:
"(x::word32) >> 1 = 0 \<Longrightarrow> x < 2"
by transfer (simp add: take_bit_drop_bit drop_bit_Suc)
lemma has_zero_byte:
"~~ (((((v::word32) && 0x7f7f7f7f) + 0x7f7f7f7f) || v) || 0x7f7f7f7f) \<noteq> 0
\<Longrightarrow> v && 0xff000000 = 0 \<or> v && 0xff0000 = 0 \<or> v && 0xff00 = 0 \<or> v && 0xff = 0"
@ -309,10 +146,7 @@ qed
lemma unat_of_int_32:
"\<lbrakk>i \<ge> 0; i \<le>2 ^ 31\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword32)) = nat i"
unfolding unat_eq_nat_uint
apply (subst eq_nat_nat_iff)
apply (auto simp add: take_bit_int_eq_self)
done
by (simp add: unsigned_of_int nat_take_bit_eq take_bit_nat_eq_self)
lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified]
@ -339,3 +173,5 @@ lemma word32_and_max_simp:
by (simp add: numeral_eq_Suc mask_Suc_exp)
end
end

175
lib/Word_Lib/Word_64.thy
View File

@ -15,200 +15,54 @@ theory Word_64
More_Word_Operations
begin
context
includes bit_operations_syntax
begin
lemma len64: "len_of (x :: 64 itself) = 64" by simp
type_synonym machine_word_len = 64
type_synonym machine_word = "machine_word_len word"
definition word_bits :: nat
where
"word_bits = LENGTH(machine_word_len)"
text \<open>The following two are numerals so they can be used as nats and words.\<close>
definition word_size_bits :: "'a :: numeral"
where
"word_size_bits = 3"
definition word_size :: "'a :: numeral"
where
"word_size = 8"
lemma word_bits_conv[code]:
"word_bits = 64"
unfolding word_bits_def by simp
lemma word_size_word_size_bits:
"(word_size::nat) = 2 ^ word_size_bits"
unfolding word_size_def word_size_bits_def by simp
lemma word_bits_word_size_conv:
"word_bits = word_size * 8"
unfolding word_bits_def word_size_def by simp
lemma ucast_8_64_inj:
"inj (ucast :: 8 word \<Rightarrow> 64 word)"
by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size)
lemma upto_2_helper:
"{0..<2 :: 64 word} = {0, 1}"
by (safe; simp) unat_arith
lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def]
lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def]
lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def]
lemma word_bits_len_of:
"len_of TYPE (64) = word_bits"
by (simp add: word_bits_conv)
lemmas unat_power_lower64' = unat_power_lower[where 'a=64]
lemmas unat_power_lower64 [simp] = unat_power_lower64'[unfolded word_bits_len_of]
lemmas word64_less_sub_le' = word_less_sub_le[where 'a = 64]
lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def]
lemma word_bits_size:
"size (w::word64) = word_bits"
by (simp add: word_bits_def word_size)
lemmas word64_power_less_1' = word_power_less_1[where 'a = 64]
lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def]
lemma of_nat64_0:
"\<lbrakk>of_nat n = (0::word64); n < 2 ^ word_bits\<rbrakk> \<Longrightarrow> n = 0"
by (erule of_nat_0, simp add: word_bits_def)
lemma unat_mask_2_less_4:
"unat (p && mask 2 :: word64) < 4"
apply (rule unat_less_helper)
apply (rule order_le_less_trans, rule word_and_le1)
apply (simp add: mask_eq)
done
lemmas unat_of_nat64' = unat_of_nat_eq[where 'a=64]
lemmas unat_of_nat64 = unat_of_nat64'[unfolded word_bits_len_of]
lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def]
lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 64, unfolded word_bits_len_of]]
lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def]
lemma n_less_word_bits:
"(n < word_bits) = (n < 64)"
by (simp add: word_bits_def)
lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, folded word_bits_def]
lemma lt_word_bits_lt_pow:
"sz < word_bits \<Longrightarrow> sz < 2 ^ word_bits"
by (simp add: word_bits_conv)
lemma unat_less_word_bits:
fixes y :: word64
shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits"
unfolding word_bits_def
by (rule order_less_trans [OF _ unat_lt2p])
lemmas unat_mask_word64' = unat_mask[where 'a=64]
lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
lemma unat_less_2p_word_bits:
"unat (x :: 64 word) < 2 ^ word_bits"
apply (simp only: word_bits_def)
apply (rule unat_lt2p)
done
lemma Suc_unat_mask_div:
"Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)"
apply (case_tac "sz < word_bits")
apply (case_tac "3 \<le> sz")
apply (clarsimp simp: word_size_def word_bits_def min_def mask_eq)
apply (drule (2) Suc_div_unat_helper
[where 'a=64 and sz=sz and us=3, simplified, symmetric])
apply (simp add: not_le word_size_def word_bits_def)
apply (case_tac sz, simp add: unat_word_ariths)
apply (case_tac nat, simp add: unat_word_ariths
unat_mask_word64 min_def word_bits_def)
apply (case_tac nata, simp add: unat_word_ariths unat_mask_word64 word_bits_def)
apply simp
apply (simp add: unat_word_ariths
unat_mask_word64 min_def word_bits_def word_size_def)
done
lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64]
lemmas word64_minus_one_le = word64_minus_one_le'[simplified]
lemma ucast_not_helper:
fixes a::"8 word"
assumes a: "a \<noteq> 0xFF"
shows "ucast a \<noteq> (0xFF::word64)"
proof
assume "ucast a = (0xFF::word64)"
also
have "(0xFF::word64) = ucast (0xFF::8 word)" by simp
finally
show False using a
apply -
apply (drule up_ucast_inj, simp)
apply simp
done
qed
lemma less_4_cases:
"(x::word64) < 4 \<Longrightarrow> x=0 \<or> x=1 \<or> x=2 \<or> x=3"
apply clarsimp
apply (drule word_less_cases, erule disjE, simp, simp)+
done
lemma if_then_1_else_0:
"((if P then 1 else 0) = (0 :: word64)) = (\<not> P)"
by simp
lemma if_then_0_else_1:
"((if P then 0 else 1) = (0 :: word64)) = (P)"
by simp
lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
lemma ucast_le_ucast_8_64:
"(ucast x \<le> (ucast y :: word64)) = (x \<le> (y :: 8 word))"
by (simp add: ucast_le_ucast)
lemma in_16_range:
"0 \<in> S \<Longrightarrow> r \<in> (\<lambda>x. r + x * (16 :: word64)) ` S"
"n - 1 \<in> S \<Longrightarrow> (r + (16 * n - 16)) \<in> (\<lambda>x :: word64. r + x * 16) ` S"
by (clarsimp simp: image_def elim!: bexI[rotated])+
lemma eq_2_64_0:
"(2 ^ 64 :: word64) = 0"
by simp
lemma x_less_2_0_1:
fixes x :: word64 shows
"x < 2 \<Longrightarrow> x = 0 \<or> x = 1"
by (rule x_less_2_0_1') auto
lemmas mask_64_max_word = max_word_mask [symmetric, where 'a=64, simplified]
lemma of_nat64_n_less_equal_power_2:
"n < 64 \<Longrightarrow> ((of_nat n)::64 word) < 2 ^ n"
by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size)
lemma word_rsplit_0:
"word_rsplit (0 :: word64) = [0, 0, 0, 0, 0, 0, 0, 0 :: 8 word]"
by (simp add: word_rsplit_def bin_rsplit_def)
lemma unat_ucast_10_64 :
fixes x :: "10 word"
shows "unat (ucast x :: word64) = unat x"
by transfer simp
lemma bool_mask [simp]:
fixes x :: word64
shows "(0 < x && 1) = (x && 1 = 1)"
by (rule bool_mask') auto
lemma word64_bounds:
"- (2 ^ (size (x :: word64) - 1)) = (-9223372036854775808 :: int)"
"((2 ^ (size (x :: word64) - 1)) - 1) = (9223372036854775807 :: int)"
@ -216,9 +70,6 @@ lemma word64_bounds:
"((2 ^ (size (y :: 64 signed word) - 1)) - 1) = (9223372036854775807 :: int)"
by (simp_all add: word_size)
lemma word_ge_min:"sint (x::64 word) \<ge> -9223372036854775808"
by (metis sint_ge word64_bounds(1) word_size)
lemmas signed_arith_ineq_checks_to_eq_word64'
= signed_arith_ineq_checks_to_eq[where 'a=64]
signed_arith_ineq_checks_to_eq[where 'a="64 signed"]
@ -245,7 +96,7 @@ lemma ucast_of_nats [simp]:
"(ucast (of_nat x :: word64) :: sword64) = (of_nat x)"
"(ucast (of_nat x :: word64) :: 16 sword) = (of_nat x)"
"(ucast (of_nat x :: word64) :: 8 sword) = (of_nat x)"
by (simp_all add: of_nat_take_bit take_bit_word_eq_self)
by (simp_all add: of_nat_take_bit take_bit_word_eq_self unsigned_of_nat)
lemmas signed_shift_guard_simpler_64'
= power_strict_increasing_iff[where b="2 :: nat" and y=31]
@ -260,15 +111,6 @@ lemmas signed_shift_guard_to_word_64
= signed_shift_guard_to_word[OF word64_31_less(1-2)]
signed_shift_guard_to_word[OF word64_31_less(3-4)]
lemma le_step_down_word_3:
fixes x :: "64 word"
shows "\<lbrakk>x \<le> y; x \<noteq> y; y < 2 ^ 64 - 1\<rbrakk> \<Longrightarrow> x \<le> y - 1"
by (rule le_step_down_word_2, assumption+)
lemma shiftr_1:
"(x::word64) >> 1 = 0 \<Longrightarrow> x < 2"
by transfer (simp add: take_bit_drop_bit drop_bit_Suc)
lemma mask_step_down_64:
\<open>\<exists>x. mask x = b\<close> if \<open>b && 1 = 1\<close>
and \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> for b :: \<open>64word\<close>
@ -293,10 +135,7 @@ qed
lemma unat_of_int_64:
"\<lbrakk>i \<ge> 0; i \<le> 2 ^ 63\<rbrakk> \<Longrightarrow> (unat ((of_int i)::sword64)) = nat i"
unfolding unat_eq_nat_uint
apply (subst eq_nat_nat_iff)
apply (simp_all add: take_bit_int_eq_self)
done
by (simp add: unsigned_of_int nat_take_bit_eq take_bit_nat_eq_self)
lemmas word_ctz_not_minus_1_64 = word_ctz_not_minus_1[where 'a=64, simplified]
@ -306,3 +145,5 @@ lemma word64_and_max_simp:
by (simp add: numeral_eq_Suc mask_Suc_exp)
end
end

8
lib/Word_Lib/Word_8.thy
View File

@ -15,6 +15,10 @@ imports
Word_Lemmas
begin
context
includes bit_operations_syntax
begin
lemma len8: "len_of (x :: 8 itself) = 8" by simp
lemma word8_and_max_simp:
@ -42,7 +46,7 @@ lemma enum_word8_eq:
244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255]\<close> (is \<open>?lhs = ?rhs\<close>)
proof -
have \<open>map unat ?lhs = [0..<256]\<close>
by (simp add: enum_word_def comp_def take_bit_nat_eq_self map_idem_upt_eq)
by (simp add: enum_word_def comp_def take_bit_nat_eq_self map_idem_upt_eq unsigned_of_nat)
also have \<open>\<dots> = map unat ?rhs\<close>
by (simp add: upt_zero_numeral_unfold)
finally show ?thesis
@ -106,3 +110,5 @@ lemma word8_exhaust:
done
end
end

12
lib/Word_Lib/Word_EqI.thy
View File

@ -9,7 +9,7 @@ section "Solving Word Equalities"
theory Word_EqI
imports
More_Word
Traditional_Infix_Syntax
Aligned
"HOL-Eisbach.Eisbach_Tools"
begin
@ -23,23 +23,27 @@ named_theorems word_eqI_simps
lemmas [word_eqI_simps] =
word_ops_nth_size
word_ao_nth
bit_mask_iff
word_size
word_or_zero
neg_mask_test_bit
nth_ucast
nth_w2p nth_shiftl
nth_shiftr
nth_w2p bit_push_bit_iff
bit_drop_bit_eq
less_2p_is_upper_bits_unset
le_mask_high_bits
bang_eq
neg_test_bit
is_up
is_down
is_aligned_nth
neg_mask_le_high_bits
lemmas word_eqI_rule = word_eqI [rule_format]
lemma test_bit_lenD:
"x !! n \<Longrightarrow> n < LENGTH('a) \<and> x !! n" for x :: "'a :: len word"
"bit x n \<Longrightarrow> n < LENGTH('a) \<and> bit x n" for x :: "'a :: len word"
by (fastforce dest: test_bit_size simp: word_size)
method word_eqI uses simp simp_del split split_del cong flip =

1584
lib/Word_Lib/Word_Lemmas.thy
View File

File diff suppressed because it is too large Load Diff

29
lib/Word_Lib/Word_Lib_Sumo.thy
View File

@ -10,8 +10,8 @@ theory Word_Lib_Sumo
imports
"HOL-Library.Word"
Aligned
Ancient_Numeral
Bit_Comprehension
Bit_Shifts_Infix_Syntax
Bits_Int
Bitwise_Signed
Bitwise
@ -32,7 +32,7 @@ imports
Reversed_Bit_Lists
Rsplit
Signed_Words
Traditional_Infix_Syntax
Syntax_Bundles
Typedef_Morphisms
Type_Syntax
Word_EqI
@ -42,13 +42,15 @@ imports
Word_32
Word_Syntax
Signed_Division_Word
Singleton_Bit_Shifts
More_Word_Operations
Many_More
Word_Lemmas_Internal
Word_Lemmas_Prefix
begin
declare word_induct2[case_names zero suc, induct type]
unbundle bit_operations_syntax
unbundle bit_projection_infix_syntax
declare word_induct2[induct type]
declare word_nat_cases[cases type]
declare signed_take_bit_Suc [simp]
@ -58,13 +60,7 @@ lemmas of_int_and_nat = unsigned_of_nat unsigned_of_int signed_of_int signed_of_
bundle no_take_bit
begin
declare of_int_and_nat[simp del]
end
bundle no_0_dvd
begin
declare word_of_int_eq_0_iff[simp del]
declare word_of_nat_eq_0_iff[simp del]
declare of_int_and_nat[simp del]
end
lemmas bshiftr1_def = bshiftr1_eq
@ -103,11 +99,6 @@ lemmas word_prev_def = word_prev_unfold
lemmas is_aligned_def = is_aligned_iff_dvd_nat
lemma shiftl_transfer [transfer_rule]:
includes lifting_syntax
shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)"
by (unfold shiftl_eq_push_bit) transfer_prover
lemmas word_and_max_simps =
word8_and_max_simp
word16_and_max_simp
@ -132,7 +123,7 @@ declare of_nat_diff [simp]
(* Haskellish names/syntax *)
notation (input)
test_bit ("testBit")
bit ("testBit")
lemmas cast_simps = cast_simps ucast_down_bl
@ -140,6 +131,6 @@ lemmas cast_simps = cast_simps ucast_down_bl
lemma nth_ucast:
"(ucast (w::'a::len word)::'b::len word) !! n =
(w !! n \<and> n < min LENGTH('a) LENGTH('b))"
by transfer (simp add: bit_take_bit_iff ac_simps)
by (auto simp add: bit_simps not_le dest: bit_imp_le_length)
end

6
lib/Word_Lib/Word_Syntax.thy
View File

@ -13,6 +13,10 @@ begin
text \<open>Additional bit and type syntax that forces word types.\<close>
context
includes bit_operations_syntax
begin
abbreviation
wordNOT :: "'a::len word \<Rightarrow> 'a word" ("~~ _" [70] 71)
where
@ -34,3 +38,5 @@ where
"a xor b == a XOR b"
end
end

58
lib/Word_Lib/Word_Type_Syntax.thy
View File

@ -1,58 +0,0 @@
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
section "Displaying Phantom Types for Word Operations"
theory Word_Type_Syntax
imports "HOL-Library.Word"
begin
ML \<open>
structure Word_Syntax =
struct
val show_word_types = Attrib.setup_config_bool @{binding show_word_types} (K true)
fun tr' cnst ctxt typ ts = if Config.get ctxt show_word_types then
case (Term.binder_types typ, Term.body_type typ) of
([Type (@{type_name "word"}, [S])], Type (@{type_name "word"}, [T])) =>
list_comb
(Syntax.const cnst $ Syntax_Phases.term_of_typ ctxt S $ Syntax_Phases.term_of_typ ctxt T
, ts)
| _ => raise Match
else raise Match
end
\<close>
syntax
"_Ucast" :: "type \<Rightarrow> type \<Rightarrow> logic" ("(1UCAST/(1'(_ \<rightarrow> _')))")
translations
"UCAST('s \<rightarrow> 't)" => "CONST ucast :: ('s word \<Rightarrow> 't word)"
typed_print_translation
\<open> [(@{const_syntax ucast}, Word_Syntax.tr' @{syntax_const "_Ucast"})] \<close>
syntax
"_Scast" :: "type \<Rightarrow> type \<Rightarrow> logic" ("(1SCAST/(1'(_ \<rightarrow> _')))")
translations
"SCAST('s \<rightarrow> 't)" => "CONST scast :: ('s word \<Rightarrow> 't word)"
typed_print_translation
\<open> [(@{const_syntax scast}, Word_Syntax.tr' @{syntax_const "_Scast"})] \<close>
syntax
"_Revcast" :: "type \<Rightarrow> type \<Rightarrow> logic" ("(1REVCAST/(1'(_ \<rightarrow> _')))")
translations
"REVCAST('s \<rightarrow> 't)" => "CONST revcast :: ('s word \<Rightarrow> 't word)"
typed_print_translation
\<open> [(@{const_syntax revcast}, Word_Syntax.tr' @{syntax_const "_Revcast"})] \<close>
(* Further candidates for showing word sizes, but with different arities:
slice, word_cat, word_split, word_rcat, word_rsplit *)
end

1
lib/Word_Lib/document/root.tex
View File

@ -5,6 +5,7 @@
%
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
% this should be the last package used