# HG changeset patch
# User haftmann
# Date 1589044804 0
# Node ID f424e164d75217584b0af76cb5a349cc0b04798f
# Parent  3ef1418d64a6fee7c90ec756869028a093fd8c90
modernized notation for bit operations

diff -r 3ef1418d64a6 -r f424e164d752 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Fri May 08 13:20:02 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Sat May 09 17:20:04 2020 +0000
@@ -1267,7 +1267,7 @@
 instantiation int :: bit_operations
 begin
 
-definition int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)"
+definition int_not_def: "NOT = (\<lambda>x::int. - x - 1)"
 
 function bitAND_int
   where "bitAND_int x y =
@@ -1280,9 +1280,9 @@
 
 declare bitAND_int.simps [simp del]
 
-definition int_or_def: "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
-
-definition int_xor_def: "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
+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"
 
diff -r 3ef1418d64a6 -r f424e164d752 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Fri May 08 13:20:02 2020 +0200
+++ b/src/HOL/Word/Tools/smt_word.ML	Sat May 09 17:20:04 2020 +0000
@@ -104,10 +104,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>bitNOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
-    (\<^term>\<open>bitAND :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
-    (\<^term>\<open>bitOR :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
-    (\<^term>\<open>bitXOR :: '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>shiftl :: 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
diff -r 3ef1418d64a6 -r f424e164d752 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri May 08 13:20:02 2020 +0200
+++ b/src/HOL/Word/Word.thy	Sat May 09 17:20:04 2020 +0000
@@ -375,16 +375,16 @@
 instantiation word :: (len0) bit_operations
 begin
 
-lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT
+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 bitAND
+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 bitOR
+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 bitXOR
+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)"
@@ -4251,19 +4251,19 @@
   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 = bitNOT
+  where conj = "(AND)" and disj = "(OR)" and compl = NOT
     and zero = 0 and one = max_word
   rewrites "word_bool_alg.xor = (XOR)"
 proof -
   interpret boolean_algebra
-    where conj = "(AND)" and disj = "(OR)" and compl = bitNOT
+    where conj = "(AND)" and disj = "(OR)" and compl = NOT
       and zero = 0 and one = max_word
     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) bitNOT 0 max_word" ..
+  show "boolean_algebra (AND) (OR) NOT 0 max_word" ..
   show "xor = (XOR)"
     by (auto simp add: fun_eq_iff word_eq_iff xor_def word_ops_nth_size word_size)
 qed