--- a/NEWS Sat Jul 31 23:15:17 2021 +0200
+++ b/NEWS Sun Aug 01 10:20:34 2021 +0000
@@ -183,6 +183,9 @@
* Combinator "Fun.swap" resolved into a mere input abbreviation in
separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
+* Infix syntax for bit operations AND, OR, XOR is now organized in
+bundle bit_operations_syntax. INCOMPATIBILITY.
+
* Bit operations set_bit, unset_bit and flip_bit are now class
operations. INCOMPATIBILITY.
--- a/src/HOL/Library/Bit_Operations.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/Library/Bit_Operations.thy Sun Aug 01 10:20:34 2021 +0000
@@ -2087,4 +2087,19 @@
| class_instance int :: semiring_bit_shifts \<rightharpoonup>
(SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bit_shifts and (Scala) Bit_Operations.semiring_bit_shifts
+no_notation
+ "and" (infixr \<open>AND\<close> 64)
+ and or (infixr \<open>OR\<close> 59)
+ and xor (infixr \<open>XOR\<close> 59)
+
+bundle bit_operations_syntax
+begin
+
+notation
+ "and" (infixr \<open>AND\<close> 64)
+ and or (infixr \<open>OR\<close> 59)
+ and xor (infixr \<open>XOR\<close> 59)
+
end
+
+end
--- a/src/HOL/Library/Tools/smt_word.ML Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/Library/Tools/smt_word.ML Sun Aug 01 10:20:34 2021 +0000
@@ -130,10 +130,10 @@
(\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"),
(\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"),
(\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"),
- (\<^term>\<open>NOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
- (\<^term>\<open>(AND) :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
- (\<^term>\<open>(OR) :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
- (\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
+ (\<^term>\<open>not :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
+ (\<^term>\<open>and :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
+ (\<^term>\<open>or :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
+ (\<^term>\<open>xor :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
(\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
fold (add_word_fun shift) [
(\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
--- a/src/HOL/Library/Word.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/Library/Word.thy Sun Aug 01 10:20:34 2021 +0000
@@ -1033,6 +1033,10 @@
for w :: \<open>'a::len word\<close>
by transfer (simp add: take_bit_not_take_bit)
+context
+ includes bit_operations_syntax
+begin
+
lemma [code]:
\<open>Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\<close>
by transfer simp
@@ -1095,6 +1099,8 @@
end
+end
+
subsection \<open>Conversions including casts\<close>
@@ -1158,6 +1164,10 @@
context semiring_bit_operations
begin
+context
+ includes bit_operations_syntax
+begin
+
lemma unsigned_and_eq:
\<open>unsigned (v AND w) = unsigned v AND unsigned w\<close>
for v w :: \<open>'b::len word\<close>
@@ -1175,9 +1185,15 @@
end
+end
+
context ring_bit_operations
begin
+context
+ includes bit_operations_syntax
+begin
+
lemma unsigned_not_eq:
\<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close>
for w :: \<open>'b::len word\<close>
@@ -1186,6 +1202,8 @@
end
+end
+
context unique_euclidean_semiring_numeral
begin
@@ -1294,6 +1312,10 @@
qed
qed
+context
+ includes bit_operations_syntax
+begin
+
lemma signed_and_eq:
\<open>signed (v AND w) = signed v AND signed w\<close>
for v w :: \<open>'b::len word\<close>
@@ -1311,6 +1333,8 @@
end
+end
+
subsubsection \<open>More\<close>
@@ -1770,6 +1794,10 @@
subsection \<open>Bit-wise operations\<close>
+context
+ includes bit_operations_syntax
+begin
+
lemma uint_take_bit_eq:
\<open>uint (take_bit n w) = take_bit n (uint w)\<close>
by transfer (simp add: ac_simps)
@@ -3332,12 +3360,18 @@
for x :: "'a::len word"
unfolding word_size by (rule card_word)
+end
+
instance word :: (len) finite
by standard (simp add: UNIV_eq)
subsection \<open>Bitwise Operations on Words\<close>
+context
+ includes bit_operations_syntax
+begin
+
lemma word_wi_log_defs:
"NOT (word_of_int a) = word_of_int (NOT a)"
"word_of_int a AND word_of_int b = word_of_int (a AND b)"
@@ -3943,6 +3977,8 @@
lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
+end
+
subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
@@ -3950,6 +3986,10 @@
locale word_rotate
begin
+context
+ includes bit_operations_syntax
+begin
+
lemma word_rot_logs:
"word_rotl n (NOT v) = NOT (word_rotl n v)"
"word_rotr n (NOT v) = NOT (word_rotr n v)"
@@ -3963,6 +4003,8 @@
end
+end
+
lemmas word_rot_logs = word_rotate.word_rot_logs
lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
@@ -3976,6 +4018,10 @@
subsection \<open>Maximum machine word\<close>
+context
+ includes bit_operations_syntax
+begin
+
lemma word_int_cases:
fixes x :: "'a::len word"
obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^LENGTH('a)"
@@ -4248,6 +4294,8 @@
if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that)
+end
+
subsection \<open>SMT support\<close>
--- a/src/HOL/Library/Z2.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/Library/Z2.thy Sun Aug 01 10:20:34 2021 +0000
@@ -178,6 +178,10 @@
instantiation bit :: semiring_bit_operations
begin
+context
+ includes bit_operations_syntax
+begin
+
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
where [simp]: \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit
@@ -199,17 +203,19 @@
definition flip_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
where [simp]: \<open>flip_bit n b = of_bool ((n = 0) \<noteq> odd b)\<close> for b :: bit
+end
+
instance
by standard auto
end
lemma add_bit_eq_xor [simp, code]:
- \<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close>
+ \<open>(+) = (Bit_Operations.xor :: bit \<Rightarrow> _)\<close>
by (auto simp add: fun_eq_iff)
lemma mult_bit_eq_and [simp, code]:
- \<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close>
+ \<open>(*) = (Bit_Operations.and :: bit \<Rightarrow> _)\<close>
by (simp add: fun_eq_iff)
instantiation bit :: field
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Sun Aug 01 10:20:34 2021 +0000
@@ -35,6 +35,10 @@
section \<open>Bit-level logic\<close>
+context
+ includes bit_operations_syntax
+begin
+
lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by smt
lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by smt
lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by smt
@@ -52,6 +56,8 @@
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by smt
lemma "w < 256 \<Longrightarrow> (w :: 16 word) AND 0x00FF = w" by smt
+end
+
section \<open>Combined integer-bitvector properties\<close>
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sun Aug 01 10:20:34 2021 +0000
@@ -8,6 +8,7 @@
imports "HOL-Library.Word"
begin
+unbundle bit_operations_syntax
\<comment> \<open>all operations are defined on 32-bit words\<close>
--- a/src/HOL/SPARK/Manual/Reference.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy Sun Aug 01 10:20:34 2021 +0000
@@ -3,6 +3,8 @@
imports "HOL-SPARK.SPARK"
begin
+unbundle bit_operations_syntax
+
lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n" for x :: int
by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod)
--- a/src/HOL/SPARK/SPARK.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/SPARK/SPARK.thy Sun Aug 01 10:20:34 2021 +0000
@@ -12,9 +12,9 @@
text \<open>Bitwise logical operators\<close>
spark_proof_functions
- bit__and (integer, integer) : integer = "(AND)"
- bit__or (integer, integer) : integer = "(OR)"
- bit__xor (integer, integer) : integer = "(XOR)"
+ bit__and (integer, integer) : integer = Bit_Operations.and
+ bit__or (integer, integer) : integer = Bit_Operations.or
+ bit__xor (integer, integer) : integer = Bit_Operations.xor
lemmas [simp] =
OR_upper [of _ 8, simplified zle_diff1_eq [symmetric], simplified]
--- a/src/HOL/ex/Bit_Lists.thy Sat Jul 31 23:15:17 2021 +0200
+++ b/src/HOL/ex/Bit_Lists.thy Sun Aug 01 10:20:34 2021 +0000
@@ -106,8 +106,6 @@
and of_bits :: "bool list \<Rightarrow> 'a"
assumes of_bits_of [simp]: "of_bits (bits_of a) = a"
-text \<open>Unclear whether a \<^typ>\<open>bool\<close> instantiation is needed or not\<close>
-
instantiation nat :: bit_representation
begin
@@ -307,7 +305,8 @@
subsection \<open>Bit representations with bit operations\<close>
-class semiring_bit_representation = semiring_bit_operations + bit_representation +
+class semiring_bit_representation = semiring_bit_operations + bit_representation
+ opening bit_operations_syntax +
assumes and_eq: "length bs = length cs \<Longrightarrow>
of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)"
and or_eq: "length bs = length cs \<Longrightarrow>
@@ -325,7 +324,7 @@
bit_and_iff bit_or_iff bit_xor_iff)
instance int :: ring_bit_representation
-proof
+including bit_operations_syntax proof
{
fix bs cs :: \<open>bool list\<close>
assume \<open>length bs = length cs\<close>