# HG changeset patch
# User haftmann
# Date 1627813234 0
# Node ID 6d7be1227d022ef883064a8b18649bd13a54892f
# Parent  cb64ccdc3ac1a3f3f442ac8d2b8df508d2fbec2e
organize syntax for word operations in bundles

diff -r cb64ccdc3ac1 -r 6d7be1227d02 NEWS
--- 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.
 
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/Library/Bit_Operations.thy
--- 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
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/Library/Tools/smt_word.ML
--- 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"),
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/Library/Word.thy
--- 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>
 
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/Library/Z2.thy
--- 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
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/SMT_Examples/SMT_Word_Examples.thy
--- 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>
 
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
--- 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>
 
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/SPARK/Manual/Reference.thy
--- 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)
 
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/SPARK/SPARK.thy
--- 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]
diff -r cb64ccdc3ac1 -r 6d7be1227d02 src/HOL/ex/Bit_Lists.thy
--- 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>