--- a/CONTRIBUTORS Thu Jun 18 09:07:30 2020 +0000
+++ b/CONTRIBUTORS Thu Jun 18 09:07:30 2020 +0000
@@ -7,7 +7,10 @@
--------------------------------------
* May 2020: Florian Haftmann
- HOL-Word bases on library theory of generic bit operations.
+ HOL-Word based on library theory of generic bit operations.
+
+* May 2020: Florian Haftmann
+ Generic algebraically founded bit operations NOT, AND, OR, XOR.
Contributions to Isabelle2020
--- a/NEWS Thu Jun 18 09:07:30 2020 +0000
+++ b/NEWS Thu Jun 18 09:07:30 2020 +0000
@@ -50,8 +50,12 @@
* Library theory "Bit_Operations" with generic bit operations.
-* Session HOL-Word: Bit operations are based on library
-theory "Bit_Operations". INCOMPATIBILITY.
+* Session HOL-Word: Type word is restricted to bit strings consisting
+of at least one bit. INCOMPATIBILITY.
+
+* Session HOL-Word: Bit operations NOT, AND, OR, XOR are based on
+generic algebraic bit operations from HOL-Library.Bit_Operations.
+INCOMPATIBILITY.
* Session HOL-Word: Compound operation "bin_split" simplifies by default
into its components "drop_bit" and "take_bit". INCOMPATIBILITY.
--- a/src/HOL/Library/Z2.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Library/Z2.thy Thu Jun 18 09:07:30 2020 +0000
@@ -5,7 +5,7 @@
section \<open>The Field of Integers mod 2\<close>
theory Z2
-imports Main
+imports Main "HOL-Library.Bit_Operations"
begin
text \<open>
@@ -218,6 +218,42 @@
end
+instantiation bit :: ring_bit_operations
+begin
+
+definition not_bit :: \<open>bit \<Rightarrow> bit\<close>
+ where \<open>NOT b = of_bool (even b)\<close> for b :: bit
+
+definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
+ where \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit
+
+definition or_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
+ where \<open>b OR c = of_bool (odd b \<or> odd c)\<close> for b c :: bit
+
+definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
+ where \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit
+
+instance
+ by standard (auto simp add: and_bit_def or_bit_def xor_bit_def not_bit_def add_eq_0_iff)
+
+end
+
+lemma add_bit_eq_xor:
+ \<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close>
+ by (auto simp add: fun_eq_iff plus_bit_def xor_bit_def)
+
+lemma mult_bit_eq_and:
+ \<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close>
+ by (simp add: fun_eq_iff times_bit_def and_bit_def split: bit.split)
+
+lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
+ for b :: bit
+ by (cases b) simp_all
+
+lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
+ for a b :: bit
+ by (cases a; cases b) simp_all
+
hide_const (open) set
--- a/src/HOL/Word/Bits.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Bits.thy Thu Jun 18 09:07:30 2020 +0000
@@ -5,15 +5,11 @@
section \<open>Syntactic type classes for bit operations\<close>
theory Bits
- imports Main
+ imports Main "HOL-Library.Bit_Operations"
begin
class bit_operations =
- fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT")
- and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
- and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
- and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
- and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
+ fixes shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
and lsb :: "'a \<Rightarrow> bool"
--- a/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:30 2020 +0000
@@ -1193,23 +1193,6 @@
instantiation int :: bit_operations
begin
-definition int_not_def: "NOT = (\<lambda>x::int. - x - 1)"
-
-function bitAND_int
- where "bitAND_int x y =
- (if x = 0 then 0 else if x = -1 then y
- else (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
- by pat_completeness simp
-
-termination
- by (relation \<open>measure (nat \<circ> abs \<circ> fst)\<close>) simp_all
-
-declare bitAND_int.simps [simp del]
-
-definition int_or_def: "(OR) = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
-
-definition int_xor_def: "(XOR) = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
-
definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
definition "lsb i = i !! 0" for i :: int
@@ -1237,8 +1220,10 @@
subsubsection \<open>Basic simplification rules\<close>
+lemmas int_not_def = not_int_def
+
lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
- by (cases b) (simp_all add: int_not_def Bit_def)
+ by (simp add: not_int_def Bit_def)
lemma int_not_simps [simp]:
"NOT (0::int) = -1"
@@ -1247,49 +1232,49 @@
"NOT (numeral w::int) = - numeral (w + Num.One)"
"NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
"NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
- unfolding int_not_def by simp_all
-
-lemma int_not_not [simp]: "NOT (NOT x) = x"
+ by (simp_all add: not_int_def)
+
+lemma int_not_not: "NOT (NOT x) = x"
for x :: int
- unfolding int_not_def by simp
+ by (fact bit.double_compl)
lemma int_and_0 [simp]: "0 AND x = 0"
for x :: int
- by (simp add: bitAND_int.simps)
+ by (fact bit.conj_zero_left)
lemma int_and_m1 [simp]: "-1 AND x = x"
for x :: int
- by (simp add: bitAND_int.simps)
+ by (fact bit.conj_one_left)
lemma int_and_Bits [simp]: "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
- by (subst bitAND_int.simps) (simp add: Bit_eq_0_iff Bit_eq_m1_iff)
+ using and_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
lemma int_or_zero [simp]: "0 OR x = x"
for x :: int
- by (simp add: int_or_def)
+ by (fact bit.disj_zero_left)
lemma int_or_minus1 [simp]: "-1 OR x = -1"
for x :: int
- by (simp add: int_or_def)
+ by (fact bit.disj_one_left)
lemma int_or_Bits [simp]: "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
- by (simp add: int_or_def)
+ using or_int_rec [of \<open>x BIT b\<close> \<open>y BIT c\<close>] by (auto simp add: Bit_B0_2t Bit_B1_2t)
lemma int_xor_zero [simp]: "0 XOR x = x"
for x :: int
- by (simp add: int_xor_def)
+ by (fact bit.xor_zero_left)
lemma int_xor_Bits [simp]: "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
- unfolding int_xor_def by auto
+ 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)
subsubsection \<open>Binary destructors\<close>
lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
- by (cases x rule: bin_exhaust) simp
+ by (fact not_int_div_2)
lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
- by (cases x rule: bin_exhaust) simp
+ by simp
lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
@@ -1306,8 +1291,7 @@
lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
-lemma bin_last_XOR [simp]:
- "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
+lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
lemma bin_nth_ops:
@@ -1315,32 +1299,32 @@
"\<And>x y. bin_nth (x OR y) n \<longleftrightarrow> bin_nth x n \<or> bin_nth y n"
"\<And>x y. bin_nth (x XOR y) n \<longleftrightarrow> bin_nth x n \<noteq> bin_nth y n"
"\<And>x. bin_nth (NOT x) n \<longleftrightarrow> \<not> bin_nth x n"
- by (induct n) (auto simp add: bit_Suc)
+ by (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)
subsubsection \<open>Derived properties\<close>
lemma int_xor_minus1 [simp]: "-1 XOR x = NOT x"
for x :: int
- by (auto simp add: bin_eq_iff bin_nth_ops)
+ by (fact bit.xor_one_left)
lemma int_xor_extra_simps [simp]:
"w XOR 0 = w"
"w XOR -1 = NOT w"
for w :: int
- by (auto simp add: bin_eq_iff bin_nth_ops)
+ by simp_all
lemma int_or_extra_simps [simp]:
"w OR 0 = w"
"w OR -1 = -1"
for w :: int
- by (auto simp add: bin_eq_iff bin_nth_ops)
+ by simp_all
lemma int_and_extra_simps [simp]:
"w AND 0 = 0"
"w AND -1 = w"
for w :: int
- by (auto simp add: bin_eq_iff bin_nth_ops)
+ by simp_all
text \<open>Commutativity of the above.\<close>
lemma bin_ops_comm:
@@ -1348,14 +1332,14 @@
shows int_and_comm: "x AND y = y AND x"
and int_or_comm: "x OR y = y OR x"
and int_xor_comm: "x XOR y = y XOR x"
- by (auto simp add: bin_eq_iff bin_nth_ops)
+ by (simp_all add: ac_simps)
lemma bin_ops_same [simp]:
"x AND x = x"
"x OR x = x"
"x XOR x = 0"
for x :: int
- by (auto simp add: bin_eq_iff bin_nth_ops)
+ by simp_all
lemmas bin_log_esimps =
int_and_extra_simps int_or_extra_simps int_xor_extra_simps
@@ -1822,69 +1806,61 @@
by(simp_all add: int_not_def) arith+
lemma bbw_ao_dist2: "(x :: int) AND (y OR z) = x AND y OR x AND z"
-by(metis int_and_comm bbw_ao_dist)
+ by (fact bit.conj_disj_distrib)
lemmas int_and_ac = bbw_lcs(1) int_and_comm int_and_assoc
lemma int_nand_same [simp]: fixes x :: int shows "x AND NOT x = 0"
-by(induct x y\<equiv>"NOT x" rule: bitAND_int.induct)(subst bitAND_int.simps, clarsimp)
+ by simp
lemma int_nand_same_middle: fixes x :: int shows "x AND y AND NOT x = 0"
-by (metis bbw_lcs(1) int_and_0 int_nand_same)
+ by (simp add: bit_eq_iff bit_and_iff bit_not_iff)
lemma and_xor_dist: fixes x :: int shows
"x AND (y XOR z) = (x AND y) XOR (x AND z)"
- by (simp add: int_xor_def bbw_ao_dist2 bbw_not_dist int_and_comm int_nand_same_middle)
-
-lemma int_and_lt0 [simp]: fixes x y :: int shows
- "x AND y < 0 \<longleftrightarrow> x < 0 \<and> y < 0"
-by(induct x y rule: bitAND_int.induct)(subst bitAND_int.simps, simp)
-
-lemma int_and_ge0 [simp]: fixes x y :: int shows
- "x AND y \<ge> 0 \<longleftrightarrow> x \<ge> 0 \<or> y \<ge> 0"
-by (metis int_and_lt0 linorder_not_less)
-
+ by (fact bit.conj_xor_distrib)
+
+lemma int_and_lt0 [simp]:
+ \<open>x AND y < 0 \<longleftrightarrow> x < 0 \<and> y < 0\<close> for x y :: int
+ by (fact and_negative_int_iff)
+
+lemma int_and_ge0 [simp]:
+ \<open>x AND y \<ge> 0 \<longleftrightarrow> x \<ge> 0 \<or> y \<ge> 0\<close> for x y :: int
+ by (fact and_nonnegative_int_iff)
+
lemma int_and_1: fixes x :: int shows "x AND 1 = x mod 2"
-by(subst bitAND_int.simps)(simp add: Bit_def bin_last_def zmod_minus1)
+ by (fact and_one_eq)
lemma int_1_and: fixes x :: int shows "1 AND x = x mod 2"
-by(subst int_and_comm)(simp add: int_and_1)
-
-lemma int_or_lt0 [simp]: fixes x y :: int shows
- "x OR y < 0 \<longleftrightarrow> x < 0 \<or> y < 0"
-by(simp add: int_or_def)
-
-lemma int_xor_lt0 [simp]: fixes x y :: int shows
- "x XOR y < 0 \<longleftrightarrow> ((x < 0) \<noteq> (y < 0))"
-by(auto simp add: int_xor_def)
-
-lemma int_xor_ge0 [simp]: fixes x y :: int shows
- "x XOR y \<ge> 0 \<longleftrightarrow> ((x \<ge> 0) \<longleftrightarrow> (y \<ge> 0))"
-by (metis int_xor_lt0 linorder_not_le)
-
+ by (fact one_and_eq)
+
+lemma int_or_lt0 [simp]:
+ \<open>x OR y < 0 \<longleftrightarrow> x < 0 \<or> y < 0\<close> for x y :: int
+ by (fact or_negative_int_iff)
+
+lemma int_or_ge0 [simp]:
+ \<open>x OR y \<ge> 0 \<longleftrightarrow> x \<ge> 0 \<and> y \<ge> 0\<close> for x y :: int
+ by (fact or_nonnegative_int_iff)
+
+lemma int_xor_lt0 [simp]:
+ \<open>x XOR y < 0 \<longleftrightarrow> (x < 0) \<noteq> (y < 0)\<close> for x y :: int
+ by (fact xor_negative_int_iff)
+
+lemma int_xor_ge0 [simp]:
+ \<open>x XOR y \<ge> 0 \<longleftrightarrow> (x \<ge> 0 \<longleftrightarrow> y \<ge> 0)\<close> for x y :: int
+ by (fact xor_nonnegative_int_iff)
+
lemma even_conv_AND:
\<open>even i \<longleftrightarrow> i AND 1 = 0\<close> for i :: int
-proof -
- obtain x b where \<open>i = x BIT b\<close>
- by (cases i rule: bin_exhaust)
- then have "i AND 1 = 0 BIT b"
- by (simp add: BIT_special_simps(2) [symmetric] del: BIT_special_simps(2))
- then show ?thesis
- using \<open>i = x BIT b\<close> by (cases b) simp_all
-qed
+ by (simp add: and_one_eq mod2_eq_if)
lemma bin_last_conv_AND:
"bin_last i \<longleftrightarrow> i AND 1 \<noteq> 0"
- by (simp add: even_conv_AND)
+ by (simp add: and_one_eq mod2_eq_if)
lemma bitval_bin_last:
"of_bool (bin_last i) = i AND 1"
-proof -
- obtain x b where "i = x BIT b" by(cases i rule: bin_exhaust)
- hence "i AND 1 = 0 BIT b"
- by(simp add: BIT_special_simps(2)[symmetric] del: BIT_special_simps(2))
- thus ?thesis by(cases b)(simp_all add: bin_last_conv_AND)
-qed
+ by (simp add: and_one_eq mod2_eq_if)
lemma bin_sign_and:
"bin_sign (i AND j) = - (bin_sign i * bin_sign j)"
@@ -1902,8 +1878,6 @@
subsection \<open>Setting and clearing bits\<close>
-
-
lemma int_lsb_BIT [simp]: fixes x :: int shows
"lsb (x BIT b) \<longleftrightarrow> b"
by(simp add: lsb_int_def)
--- a/src/HOL/Word/Bits_Z2.thy Thu Jun 18 09:07:30 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-(* Title: HOL/Word/Bits_Z2.thy
- Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
-*)
-
-section \<open>Bit operations in $\cal Z_2$\<close>
-
-theory Bits_Z2
- imports Bits "HOL-Library.Z2"
-begin
-
-instantiation bit :: bit_operations
-begin
-
-primrec bitNOT_bit
- where
- "NOT 0 = (1::bit)"
- | "NOT 1 = (0::bit)"
-
-primrec bitAND_bit
- where
- "0 AND y = (0::bit)"
- | "1 AND y = (y::bit)"
-
-primrec bitOR_bit
- where
- "0 OR y = (y::bit)"
- | "1 OR y = (1::bit)"
-
-primrec bitXOR_bit
- where
- "0 XOR y = (y::bit)"
- | "1 XOR y = (NOT y :: bit)"
-
-instance ..
-
-end
-
-lemmas bit_simps =
- bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
-
-lemma bit_extra_simps [simp]:
- "x AND 0 = 0"
- "x AND 1 = x"
- "x OR 1 = 1"
- "x OR 0 = x"
- "x XOR 1 = NOT x"
- "x XOR 0 = x"
- for x :: bit
- by (cases x; auto)+
-
-lemma bit_ops_comm:
- "x AND y = y AND x"
- "x OR y = y OR x"
- "x XOR y = y XOR x"
- for x :: bit
- by (cases y; auto)+
-
-lemma bit_ops_same [simp]:
- "x AND x = x"
- "x OR x = x"
- "x XOR x = 0"
- for x :: bit
- by (cases x; auto)+
-
-lemma bit_not_not [simp]: "NOT (NOT x) = x"
- for x :: bit
- by (cases x) auto
-
-lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
- for b c :: bit
- by (induct b) simp_all
-
-lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
- for b c :: bit
- by (induct b) simp_all
-
-lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
- for b :: bit
- by (induct b) simp_all
-
-lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
- for a b :: bit
- by (induct a) simp_all
-
-lemma bit_nand_same [simp]: "x AND NOT x = 0"
- for x :: bit
- by (cases x) simp_all
-
-end
--- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:30 2020 +0000
@@ -8,8 +8,8 @@
imports
"HOL-Library.Type_Length"
"HOL-Library.Boolean_Algebra"
+ "HOL-Library.Bit_Operations"
Bits_Int
- Bits_Z2
Bit_Comprehension
Misc_Typedef
Misc_Arithmetic
@@ -468,6 +468,12 @@
end
+interpretation word_order: ordering_top \<open>(\<le>)\<close> \<open>(<)\<close> \<open>- 1 :: 'a::len word\<close>
+ by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1)
+
+interpretation word_coorder: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0 :: 'a::len word\<close>
+ by (standard; transfer) simp
+
lemma word_le_def [code]:
"a \<le> b \<longleftrightarrow> uint a \<le> uint b"
by transfer rule
@@ -796,21 +802,44 @@
apply (auto simp add: not_le dest: less_2_cases)
done
+instantiation word :: (len) ring_bit_operations
+begin
+
+lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close>
+ is not
+ by (simp add: take_bit_not_iff)
+
+lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is \<open>and\<close>
+ by simp
+
+lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is or
+ by simp
+
+lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+ is xor
+ by simp
+
+instance proof
+ fix a b :: \<open>'a word\<close> and n :: nat
+ show \<open>- a = NOT (a - 1)\<close>
+ by transfer (simp add: minus_eq_not_minus_1)
+ show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+ by transfer (simp add: bit_not_iff)
+ show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+ by transfer (auto simp add: bit_and_iff)
+ show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+ by transfer (auto simp add: bit_or_iff)
+ show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+ by transfer (auto simp add: bit_xor_iff)
+qed
+
+end
+
instantiation word :: (len) bit_operations
begin
-lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is NOT
- by (metis bin_trunc_not)
-
-lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is \<open>(AND)\<close>
- by (metis bin_trunc_and)
-
-lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is \<open>(OR)\<close>
- by (metis bin_trunc_or)
-
-lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is \<open>(XOR)\<close>
- by (metis bin_trunc_xor)
-
definition word_test_bit_def: "test_bit a = bin_nth (uint a)"
definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
@@ -877,8 +906,7 @@
and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)"
and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
- by (simp_all flip: bitNOT_word.abs_eq bitAND_word.abs_eq
- bitOR_word.abs_eq bitXOR_word.abs_eq)
+ by (transfer, simp add: take_bit_not_take_bit)+
definition setBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"
where "setBit w n = set_bit w n True"
@@ -886,6 +914,20 @@
definition clearBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"
where "clearBit w n = set_bit w n False"
+definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close>
+ where [code_abbrev]: \<open>even_word = even\<close>
+
+lemma even_word_iff [code]:
+ \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
+ by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def)
+
+definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
+ where [code_abbrev]: \<open>bit_word = bit\<close>
+
+lemma bit_word_iff [code]:
+ \<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
+ by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
+
subsection \<open>Shift operations\<close>
@@ -1394,6 +1436,10 @@
thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>!
\<close>
+lemma bit_ucast_iff:
+ \<open>Parity.bit (ucast a :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a::len) \<and> Parity.bit a n\<close>
+ by (simp add: ucast_def, transfer) (auto simp add: bit_take_bit_iff)
+
lemma ucast_id: "ucast w = w"
by (auto simp: ucast_def)
@@ -1407,6 +1453,10 @@
by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
(fast elim!: bin_nth_uint_imp)
+lemma ucast_mask_eq:
+ \<open>ucast (Bit_Operations.mask n :: 'b word) = Bit_Operations.mask (min LENGTH('b::len) n)\<close>
+ by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff)
+
\<comment> \<open>literal u(s)cast\<close>
lemma ucast_bintr [simp]:
"ucast (numeral w :: 'a::len word) =
@@ -1752,7 +1802,7 @@
lemma word_n1_ge [simp]: "y \<le> -1"
for y :: "'a::len word"
- by (simp only: word_le_def word_m1_wi word_uint.eq_norm m1mod2k) auto
+ by (fact word_order.extremum)
lemmas word_not_simps [simp] =
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
@@ -2676,11 +2726,17 @@
"x XOR (-1::'a::len word) = NOT x"
by (transfer, simp)+
-lemma uint_or: "uint (x OR y) = uint x OR uint y"
- by (transfer, simp add: bin_trunc_ao)
-
-lemma uint_and: "uint (x AND y) = uint x AND uint y"
- by (transfer, simp add: bin_trunc_ao)
+lemma uint_and:
+ \<open>uint (x AND y) = uint x AND uint y\<close>
+ by transfer simp
+
+lemma uint_or:
+ \<open>uint (x OR y) = uint x OR uint y\<close>
+ by transfer simp
+
+lemma uint_xor:
+ \<open>uint (x XOR y) = uint x XOR uint y\<close>
+ by transfer simp
lemma test_bit_wi [simp]:
"(word_of_int x :: 'a::len word) !! n \<longleftrightarrow> n < LENGTH('a) \<and> bin_nth x n"
@@ -2751,7 +2807,7 @@
for x :: "'a::len word"
by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
-lemma word_log_esimps [simp]:
+lemma word_log_esimps:
"x AND 0 = 0"
"x AND -1 = x"
"x OR 0 = x"
@@ -2765,20 +2821,20 @@
"0 XOR x = x"
"-1 XOR x = NOT x"
for x :: "'a::len word"
- by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
+ by simp_all
lemma word_not_dist:
"NOT (x OR y) = NOT x AND NOT y"
"NOT (x AND y) = NOT x OR NOT y"
for x :: "'a::len word"
- by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
+ by simp_all
lemma word_bw_same:
"x AND x = x"
"x OR x = x"
"x XOR x = 0"
for x :: "'a::len word"
- by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
+ by simp_all
lemma word_ao_absorbs [simp]:
"x AND (y OR x) = x"
@@ -2794,7 +2850,7 @@
lemma word_not_not [simp]: "NOT (NOT x) = x"
for x :: "'a::len word"
- by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
+ by simp
lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z"
for x :: "'a::len word"
@@ -3566,7 +3622,7 @@
lemma aligned_bl_add_size [OF refl]:
"size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
take m (to_bl y) = replicate m False \<Longrightarrow>
- to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
+ to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" for x :: \<open>'a::len word\<close>
apply (subgoal_tac "x AND y = 0")
prefer 2
apply (rule word_bl.Rep_eqD)
@@ -3583,9 +3639,17 @@
subsubsection \<open>Mask\<close>
+lemma minus_1_eq_mask:
+ \<open>- 1 = (Bit_Operations.mask LENGTH('a) :: 'a::len word)\<close>
+ by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff)
+
+lemma mask_eq_mask:
+ \<open>mask = Bit_Operations.mask\<close>
+ by (simp add: fun_eq_iff mask_eq_exp_minus_1 mask_def shiftl_word_eq push_bit_eq_mult)
+
lemma mask_eq:
\<open>mask n = 2 ^ n - 1\<close>
- by (simp add: mask_def shiftl_word_eq push_bit_eq_mult)
+ by (simp add: mask_eq_mask mask_eq_exp_minus_1)
lemma mask_Suc_rec:
\<open>mask (Suc n) = 2 * mask n + 1\<close>
@@ -3596,7 +3660,7 @@
qualified lemma bit_mask_iff [simp]:
\<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < m\<close>
- by (simp add: mask_eq bit_mask_iff exp_eq_zero_iff not_le)
+ by (simp add: mask_eq_mask bit_mask_iff exp_eq_zero_iff not_le)
end
@@ -4695,17 +4759,13 @@
by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
lemma max_word_max [intro!]: "n \<le> max_word"
- by (fact word_n1_ge)
+ by (fact word_order.extremum)
lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len word)"
by (subst word_uint.Abs_norm [symmetric]) simp
lemma word_pow_0: "(2::'a::len word) ^ LENGTH('a) = 0"
-proof -
- have "word_of_int (2 ^ LENGTH('a)) = (0::'a word)"
- by (rule word_of_int_2p_len)
- then show ?thesis by (simp add: word_of_int_2p)
-qed
+ by (fact word_exp_length_eq_0)
lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
by (simp add: eq_neg_iff_add_eq_0)
@@ -4737,24 +4797,6 @@
lemma word_or_not [simp]: "x OR NOT x = max_word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
-global_interpretation word_bool_alg: boolean_algebra
- where conj = "(AND)" and disj = "(OR)" and compl = NOT
- and zero = 0 and one = \<open>- 1 :: 'a::len word\<close>
- rewrites "word_bool_alg.xor = (XOR)"
-proof -
- interpret boolean_algebra
- where conj = "(AND)" and disj = "(OR)" and compl = NOT
- and zero = 0 and one = \<open>- 1 :: 'a word\<close>
- apply standard
- apply (simp_all add: word_bw_assocs word_bw_comms word_bw_lcs)
- apply (fact word_ao_dist2)
- apply (fact word_oa_dist2)
- done
- show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)" ..
- show "xor = (XOR)"
- by (auto simp add: fun_eq_iff word_eq_iff xor_def word_ops_nth_size word_size)
-qed
-
lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
for x y :: "'a::len word"
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
@@ -5039,15 +5081,15 @@
lemma test_bit_1' [simp]:
"(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
- by (cases n) (simp_all only: one_word_def test_bit_wi, simp_all)
+ by simp
lemma mask_0 [simp]:
"mask 0 = 0"
by (simp add: Word.mask_def)
-lemma shiftl0 [simp]:
+lemma shiftl0:
"x << 0 = (x :: 'a :: len word)"
- by (metis shiftl_rev shiftr_x_0 word_rev_gal)
+ by (fact shiftl_x_0)
lemma mask_1: "mask 1 = 1"
by (simp add: mask_def)
--- a/src/HOL/Word/Word_Bitwise.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Word_Bitwise.thy Thu Jun 18 09:07:30 2020 +0000
@@ -101,6 +101,7 @@
by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
+ for x :: \<open>'a::len word\<close>
by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)
lemma rbl_word_cat: