merged

--- a/NEWS	Fri May 28 18:11:34 2021 +0100
+++ b/NEWS	Sat May 29 13:42:26 2021 +0100
@@ -157,6 +157,9 @@
 * Bit operations set_bit, unset_bit and flip_bit are now class
 operations.  INCOMPATIBILITY.
 
+* Abbreviation "max_word" has been moved to session Word_Lib in the AFP.
+See there further the changelog in theory Guide.  INCOMPATIBILITY.
+
 
 *** ML ***
 

--- a/src/HOL/Library/Bit_Operations.thy	Fri May 28 18:11:34 2021 +0100
+++ b/src/HOL/Library/Bit_Operations.thy	Sat May 29 13:42:26 2021 +0100
@@ -202,6 +202,24 @@
   \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
   using bit_unset_bit_iff [of m a 0] by auto
 
+lemma and_exp_eq_0_iff_not_bit:
+  \<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?Q
+  then show ?P
+    by (auto intro: bit_eqI simp add: bit_simps)
+next
+  assume ?P
+  show ?Q
+  proof (rule notI)
+    assume \<open>bit a n\<close>
+    then have \<open>a AND 2 ^ n = 2 ^ n\<close>
+      by (auto intro: bit_eqI simp add: bit_simps)
+    with \<open>?P\<close> show False
+      using \<open>bit a n\<close> exp_eq_0_imp_not_bit by auto
+  qed
+qed
+
 lemmas flip_bit_def = flip_bit_eq_xor
 
 lemma bit_flip_bit_iff [bit_simps]:

--- a/src/HOL/Library/Word.thy	Fri May 28 18:11:34 2021 +0100
+++ b/src/HOL/Library/Word.thy	Sat May 29 13:42:26 2021 +0100
@@ -920,6 +920,16 @@
     by (rule finite_subset)
 qed
 
+lemma bit_numeral_word_iff [simp]:
+  \<open>bit (numeral w :: 'a::len word) n
+    \<longleftrightarrow> n < LENGTH('a) \<and> bit (numeral w :: int) n\<close>
+  by transfer simp
+
+lemma bit_neg_numeral_word_iff [simp]:
+  \<open>bit (- numeral w :: 'a::len word) n
+    \<longleftrightarrow> n < LENGTH('a) \<and> bit (- numeral w :: int) n\<close>
+  by transfer simp
+
 instantiation word :: (len) semiring_bit_shifts
 begin
 
@@ -2168,10 +2178,6 @@
 definition word_rcat :: \<open>'a::len word list \<Rightarrow> 'b::len word\<close>
   where \<open>word_rcat = word_of_int \<circ> horner_sum uint (2 ^ LENGTH('a)) \<circ> rev\<close>
 
-abbreviation (input) max_word :: \<open>'a::len word\<close>
-  \<comment> \<open>Largest representable machine integer.\<close>
-  where "max_word \<equiv> - 1"
-
 
 subsection \<open>More on conversions\<close>
 
@@ -4122,7 +4128,8 @@
   obtains n where "x = of_nat n" and "n < 2^LENGTH('a)"
   by (rule that [of \<open>unat x\<close>]) simp_all
 
-lemma max_word_max [intro!]: "n \<le> max_word"
+lemma max_word_max [intro!]:
+  \<open>n \<le> - 1\<close> for n :: \<open>'a::len word\<close>
   by (fact word_order.extremum)
 
 lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len word)"
@@ -4131,13 +4138,16 @@
 lemma word_pow_0: "(2::'a::len word) ^ LENGTH('a) = 0"
   by (fact word_exp_length_eq_0)
 
-lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
+lemma max_word_wrap: 
+  \<open>x + 1 = 0 \<Longrightarrow> x = - 1\<close> for x :: \<open>'a::len word\<close>
   by (simp add: eq_neg_iff_add_eq_0)
 
-lemma word_and_max: "x AND max_word = x"
+lemma word_and_max:
+  \<open>x AND - 1 = x\<close> for x :: \<open>'a::len word\<close>
   by (fact word_log_esimps)
 
-lemma word_or_max: "x OR max_word = max_word"
+lemma word_or_max:
+  \<open>x OR - 1 = - 1\<close> for x :: \<open>'a::len word\<close>
   by (fact word_log_esimps)
 
 lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
@@ -4152,7 +4162,8 @@
   for x :: "'a::len word"
   by (fact bit.conj_cancel_right)
 
-lemma word_or_not [simp]: "x OR NOT x = max_word"
+lemma word_or_not [simp]:
+  \<open>x OR NOT x = - 1\<close> for x :: \<open>'a::len word\<close>
   by (fact bit.disj_cancel_right)
 
 lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"