# HG changeset patch
# User haftmann
# Date 1622233283 0
# Node ID 35217bf33215d6481130f41384ad348445209d49
# Parent  493b1ae188dadd3c43a5b6d66c1c99f6cccf10f9
max word moved to Word_Lib in AFP

diff -r 493b1ae188da -r 35217bf33215 NEWS
--- a/NEWS	Wed May 26 18:07:49 2021 +0200
+++ b/NEWS	Fri May 28 20:21:23 2021 +0000
@@ -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 ***
 
diff -r 493b1ae188da -r 35217bf33215 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed May 26 18:07:49 2021 +0200
+++ b/src/HOL/Library/Word.thy	Fri May 28 20:21:23 2021 +0000
@@ -2168,10 +2168,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 +4118,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 +4128,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 +4152,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"