--- a/NEWS Thu Jun 18 09:07:29 2020 +0000
+++ b/NEWS Thu Jun 18 09:07:29 2020 +0000
@@ -48,8 +48,8 @@
* For the natural numbers, Sup {} = 0.
-* Session HOL-Word: Operations "bin_last" and "bin_rest" are now mere
-input abbreviations. INCOMPATIBILITY.
+* Session HOL-Word: Operations "bin_last", "bin_rest" and "max_word"
+are now mere input abbreviations. INCOMPATIBILITY.
* Session HOL-Word: Compound operation "bin_split" simplifies by default
into its components "drop_bit" and "take_bit". Minor INCOMPATIBILITY.
--- a/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:29 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy Thu Jun 18 09:07:29 2020 +0000
@@ -419,7 +419,7 @@
proof (rule ext)+
fix n and k
show \<open>bintrunc n k = take_bit n k\<close>
- by (induction n arbitrary: k) (simp_all add: take_bit_Suc Bit_def)
+ by (induction n arbitrary: k) (simp_all add: take_bit_Suc Bit_def mod_2_eq_odd)
qed
lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n"
@@ -818,7 +818,7 @@
lemma [code]:
"bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))"
"bin_split 0 w = (w, 0)"
- by (simp_all add: Bit_def drop_bit_Suc take_bit_Suc)
+ by (simp_all add: Bit_def drop_bit_Suc take_bit_Suc mod_2_eq_odd)
primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int"
where
@@ -828,7 +828,7 @@
lemma bin_cat_eq_push_bit_add_take_bit:
\<open>bin_cat k n l = push_bit n k + take_bit n l\<close>
by (induction n arbitrary: k l)
- (simp_all add: Bit_def take_bit_Suc push_bit_double)
+ (simp_all add: Bit_def take_bit_Suc push_bit_double mod_2_eq_odd)
lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
by (induct n arbitrary: y) auto
@@ -923,7 +923,7 @@
lemma take_bit_bin_cat_eq:
\<open>take_bit n (bin_cat v n w) = take_bit n w\<close>
by (induct n arbitrary: w)
- (simp_all add: Bit_def take_bit_Suc)
+ (simp_all add: Bit_def take_bit_Suc mod_2_eq_odd)
lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
by (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq bintrunc_eq_take_bit)
@@ -941,7 +941,7 @@
apply (induct n arbitrary: m b c, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
apply (case_tac m)
- apply (auto simp: Let_def drop_bit_Suc take_bit_Suc split: prod.split_asm)
+ apply (auto simp: Let_def drop_bit_Suc take_bit_Suc mod_2_eq_odd split: prod.split_asm)
done
lemma bin_split_trunc1:
@@ -950,7 +950,7 @@
apply (induct n arbitrary: m b c, clarsimp)
apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
apply (case_tac m)
- apply (auto simp: Let_def drop_bit_Suc take_bit_Suc Bit_def split: prod.split_asm)
+ apply (auto simp: Let_def drop_bit_Suc take_bit_Suc Bit_def mod_2_eq_odd split: prod.split_asm)
done
lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
@@ -1008,7 +1008,7 @@
bin_split (numeral bin) w =
(let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w)
in (w1, w2 BIT bin_last w))"
- by (simp add: Bit_def take_bit_rec drop_bit_rec)
+ by (simp add: Bit_def take_bit_rec drop_bit_rec mod_2_eq_odd)
lemma bin_rsplit_aux_simp_alt:
"bin_rsplit_aux n m c bs =
--- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000
+++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:29 2020 +0000
@@ -479,9 +479,9 @@
definition word_rsplit :: "'a::len0 word \<Rightarrow> 'b::len word list"
where "word_rsplit w = map word_of_int (bin_rsplit (LENGTH('b)) (LENGTH('a), uint w))"
-definition max_word :: "'a::len word"
+abbreviation (input) max_word :: \<open>'a::len0 word\<close>
\<comment> \<open>Largest representable machine integer.\<close>
- where "max_word = word_of_int (2 ^ LENGTH('a) - 1)"
+ where "max_word \<equiv> - 1"
subsection \<open>Theorems about typedefs\<close>
@@ -620,6 +620,10 @@
for x :: "'a::len0 word"
using word_uint.Rep [of x] by (simp add: uints_num)
+lemma word_exp_length_eq_0 [simp]:
+ \<open>(2 :: 'a::len0 word) ^ LENGTH('a) = 0\<close>
+ by transfer (simp add: bintrunc_mod2p)
+
lemma sint_ge: "- (2 ^ (LENGTH('a) - 1)) \<le> sint x"
for x :: "'a::len word"
using word_sint.Rep [of x] by (simp add: sints_num)
@@ -2495,7 +2499,7 @@
"clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
by (simp add: clearBit_def)
-lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (LENGTH('a)) True"
+lemma to_bl_n1 [simp]: "to_bl (-1::'a::len0 word) = replicate (LENGTH('a)) True"
apply (rule word_bl.Abs_inverse')
apply simp
apply (rule word_eqI)
@@ -4183,12 +4187,8 @@
obtains n where "x = of_nat n" and "n < 2^LENGTH('a)"
by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
-lemma max_word_eq: "(max_word::'a::len word) = 2^LENGTH('a) - 1"
- by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
-
-lemma max_word_max [simp,intro!]: "n \<le> max_word"
- by (cases n rule: word_int_cases)
- (simp add: max_word_def word_le_def int_word_uint del: minus_mod_self1)
+lemma max_word_max [intro!]: "n \<le> max_word"
+ by (fact word_n1_ge)
lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len0 word)"
by (subst word_uint.Abs_norm [symmetric]) simp
@@ -4201,30 +4201,19 @@
qed
lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
- apply (simp add: max_word_eq)
- apply uint_arith
- apply (auto simp: word_pow_0)
- done
-
-lemma max_word_minus: "max_word = (-1::'a::len word)"
-proof -
- have "-1 + 1 = (0::'a word)"
- by simp
- then show ?thesis
- by (rule max_word_wrap [symmetric])
-qed
-
-lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (LENGTH('a)) True"
- by (subst max_word_minus to_bl_n1)+ simp
-
-lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < LENGTH('a)"
- by (auto simp: test_bit_bl word_size)
-
-lemma word_and_max [simp]: "x AND max_word = x"
- by (rule word_eqI) (simp add: word_ops_nth_size word_size)
-
-lemma word_or_max [simp]: "x OR max_word = max_word"
- by (rule word_eqI) (simp add: word_ops_nth_size word_size)
+ by (simp add: eq_neg_iff_add_eq_0)
+
+lemma max_word_bl: "to_bl (max_word::'a::len0 word) = replicate LENGTH('a) True"
+ by (fact to_bl_n1)
+
+lemma max_test_bit: "(max_word::'a::len0 word) !! n \<longleftrightarrow> n < LENGTH('a)"
+ by (fact nth_minus1)
+
+lemma word_and_max: "x AND max_word = x"
+ by (fact word_log_esimps)
+
+lemma word_or_max: "x OR max_word = max_word"
+ by (fact word_log_esimps)
lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
for x y z :: "'a::len0 word"
@@ -4243,18 +4232,18 @@
global_interpretation word_bool_alg: boolean_algebra
where conj = "(AND)" and disj = "(OR)" and compl = NOT
- and zero = 0 and one = max_word
+ and zero = 0 and one = \<open>- 1 :: 'a::len0 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 = max_word
+ 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 max_word" ..
+ 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
--- a/src/HOL/Word/Word_Examples.thy Thu Jun 18 09:07:29 2020 +0000
+++ b/src/HOL/Word/Word_Examples.thy Thu Jun 18 09:07:29 2020 +0000
@@ -103,8 +103,7 @@
lemma "1 XOR 7 = (6 :: byte)" by simp
lemma "1 XOR 1 = (0 :: byte)" by simp
lemma "NOT 1 = (254 :: byte)" by simp
-lemma "NOT 0 = (255 :: byte)" apply simp oops
-(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
+lemma "NOT 0 = (255 :: byte)" by simp
lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp