# HG changeset patch
# User haftmann
# Date 1592471250 0
# Node ID 3e162c63371a79271344fa5b27e029a6be7acd5c
# Parent  a4bffc0de967913a0973cf4a4d5d49e16bbf3d4c
build bit operations on word on library theory on bit operations

diff -r a4bffc0de967 -r 3e162c63371a CONTRIBUTORS
--- 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
diff -r a4bffc0de967 -r 3e162c63371a NEWS
--- 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.
diff -r a4bffc0de967 -r 3e162c63371a src/HOL/Library/Z2.thy
--- 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
 
diff -r a4bffc0de967 -r 3e162c63371a src/HOL/Word/Bits.thy
--- 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"
diff -r a4bffc0de967 -r 3e162c63371a src/HOL/Word/Bits_Int.thy
--- 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)
diff -r a4bffc0de967 -r 3e162c63371a src/HOL/Word/Bits_Z2.thy
--- 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
diff -r a4bffc0de967 -r 3e162c63371a src/HOL/Word/Word.thy
--- 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)
diff -r a4bffc0de967 -r 3e162c63371a src/HOL/Word/Word_Bitwise.thy
--- 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: