--- 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"
--- 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"),
--- 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