--- a/NEWS Tue Aug 04 09:24:00 2020 +0000
+++ b/NEWS Tue Aug 04 09:33:05 2020 +0000
@@ -83,6 +83,13 @@
* Session HOL-Word: Compound operation "bin_split" simplifies by default
into its components "drop_bit" and "take_bit". INCOMPATIBILITY.
+* Session HOL-Word: Uniform polymorphic "mask" operation for both
+types int and word. INCOMPATIBILITY
+
+* Session HOL-Word: Operations lsb, msb and set_bit are separated
+into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
+INCOMPATIBILITY.
+
* Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
"bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now
mere input abbreviations. Minor INCOMPATIBILITY.
@@ -90,10 +97,6 @@
* Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
Minor INCOMPATIBILITY.
-* Session HOL-Word: Operations lsb, msb and set_bit are separated
-into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
-INCOMPATIBILITY.
-
* Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
are in working order again, as opposed to outputting "GaveUp" on nearly
all problems.
--- a/src/HOL/Library/Bit_Operations.thy Tue Aug 04 09:24:00 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy Tue Aug 04 09:33:05 2020 +0000
@@ -15,9 +15,11 @@
fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>AND\<close> 64)
and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>OR\<close> 59)
and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>XOR\<close> 59)
+ and mask :: \<open>nat \<Rightarrow> 'a\<close>
assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+ and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
begin
text \<open>
@@ -93,9 +95,6 @@
\<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
-definition mask :: \<open>nat \<Rightarrow> 'a\<close>
- where mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
-
lemma bit_mask_iff:
\<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
@@ -104,25 +103,33 @@
\<open>even (mask n) \<longleftrightarrow> n = 0\<close>
using bit_mask_iff [of n 0] by auto
-lemma mask_0 [simp, code]:
+lemma mask_0 [simp]:
\<open>mask 0 = 0\<close>
by (simp add: mask_eq_exp_minus_1)
-lemma mask_Suc_exp [code]:
+lemma mask_Suc_0 [simp]:
+ \<open>mask (Suc 0) = 1\<close>
+ by (simp add: mask_eq_exp_minus_1 add_implies_diff sym)
+
+lemma mask_Suc_exp:
\<open>mask (Suc n) = 2 ^ n OR mask n\<close>
by (rule bit_eqI)
(auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq)
lemma mask_Suc_double:
- \<open>mask (Suc n) = 2 * mask n OR 1\<close>
+ \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
proof (rule bit_eqI)
fix q
assume \<open>2 ^ q \<noteq> 0\<close>
- show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (2 * mask n OR 1) q\<close>
+ show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (1 OR 2 * mask n) q\<close>
by (cases q)
(simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2)
qed
+lemma mask_numeral:
+ \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
+ by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)
+
lemma take_bit_eq_mask:
\<open>take_bit n a = a AND mask n\<close>
by (rule bit_eqI)
@@ -495,6 +502,9 @@
\<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close> for k l :: int
by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff)
+definition mask_int :: \<open>nat \<Rightarrow> int\<close>
+ where \<open>mask n = (2 :: int) ^ n - 1\<close>
+
instance proof
fix k l :: int and n :: nat
show \<open>- k = NOT (k - 1)\<close>
@@ -505,7 +515,7 @@
by (fact bit_or_int_iff)
show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
by (fact bit_xor_int_iff)
-qed (simp_all add: bit_not_int_iff)
+qed (simp_all add: bit_not_int_iff mask_int_def)
end
@@ -976,6 +986,9 @@
definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
where \<open>m XOR n = nat (int m XOR int n)\<close> for m n :: nat
+definition mask_nat :: \<open>nat \<Rightarrow> nat\<close>
+ where \<open>mask n = (2 :: nat) ^ n - 1\<close>
+
instance proof
fix m n q :: nat
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
@@ -984,7 +997,7 @@
by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff)
show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff)
-qed
+qed (simp add: mask_nat_def)
end
@@ -1044,19 +1057,12 @@
lift_definition xor_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
is xor .
-instance proof
- fix k l :: \<open>integer\<close> and n :: nat
- show \<open>- k = NOT (k - 1)\<close>
- by transfer (simp add: minus_eq_not_minus_1)
- show \<open>bit (NOT k) n \<longleftrightarrow> (2 :: integer) ^ n \<noteq> 0 \<and> \<not> bit k n\<close>
- by transfer (fact bit_not_iff)
- show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
- by transfer (fact bit_and_iff)
- show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
- by transfer (fact bit_or_iff)
- show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
- by transfer (fact bit_xor_iff)
-qed
+lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close>
+ is mask .
+
+instance by (standard; transfer)
+ (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+ bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
end
@@ -1072,15 +1078,11 @@
lift_definition xor_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
is xor .
-instance proof
- fix m n :: \<open>natural\<close> and q :: nat
- show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
- by transfer (fact bit_and_iff)
- show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
- by transfer (fact bit_or_iff)
- show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
- by transfer (fact bit_xor_iff)
-qed
+lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close>
+ is mask .
+
+instance by (standard; transfer)
+ (simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff)
end
--- a/src/HOL/Library/Z2.thy Tue Aug 04 09:24:00 2020 +0000
+++ b/src/HOL/Library/Z2.thy Tue Aug 04 09:33:05 2020 +0000
@@ -187,6 +187,9 @@
definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit
+definition mask_bit :: \<open>nat \<Rightarrow> bit\<close>
+ where [simp]: \<open>mask_bit n = of_bool (n > 0)\<close>
+
instance
by standard auto
--- a/src/HOL/Word/Word.thy Tue Aug 04 09:24:00 2020 +0000
+++ b/src/HOL/Word/Word.thy Tue Aug 04 09:33:05 2020 +0000
@@ -1000,19 +1000,13 @@
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
+lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
+ is mask
+ .
+
+instance by (standard; transfer)
+ (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+ bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
end
@@ -1173,6 +1167,11 @@
\<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close>
by (fact take_bit_eq_mask)
+lemma [code]:
+ \<open>mask (Suc n) = push_bit n (1 :: 'a word) OR mask n\<close>
+ \<open>mask 0 = (0 :: 'a::len word)\<close>
+ by (simp_all add: mask_Suc_exp push_bit_of_1)
+
lemma [code_abbrev]:
\<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
by (fact push_bit_of_1)
@@ -1289,9 +1288,6 @@
is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close>
by (fact arg_cong)
-lift_definition mask :: \<open>nat \<Rightarrow> 'a::len word\<close>
- is \<open>take_bit LENGTH('a) \<circ> Bit_Operations.mask\<close> .
-
lemma sshiftr1_eq:
\<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close>
by transfer simp
@@ -1328,7 +1324,7 @@
qed
lemma mask_eq:
- \<open>mask n = (1 << n) - 1\<close>
+ \<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1)
lemma uint_sshiftr_eq [code]:
@@ -1977,18 +1973,8 @@
lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
by transfer (simp add: bit_take_bit_iff ac_simps)
-context
- includes lifting_syntax
-begin
-
-lemma transfer_rule_mask_word [transfer_rule]:
- \<open>((=) ===> pcr_word) Bit_Operations.mask Bit_Operations.mask\<close>
- by (simp only: mask_eq_exp_minus_1 [abs_def]) transfer_prover
-
-end
-
lemma ucast_mask_eq:
- \<open>ucast (Bit_Operations.mask n :: 'b word) = Bit_Operations.mask (min LENGTH('b::len) n)\<close>
+ \<open>ucast (mask n :: 'b word) = 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>
@@ -4075,27 +4061,23 @@
subsubsection \<open>Mask\<close>
lemma minus_1_eq_mask:
- \<open>- 1 = (Bit_Operations.mask LENGTH('a) :: 'a::len word)\<close>
+ \<open>- 1 = (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 [code]:
- \<open>mask = Bit_Operations.mask\<close>
- by (rule ext, transfer) simp
lemma mask_eq_decr_exp:
- \<open>mask n = 2 ^ n - 1\<close>
- by (simp add: mask_eq_mask mask_eq_exp_minus_1)
+ \<open>mask n = 2 ^ n - (1 :: 'a::len word)\<close>
+ by (fact mask_eq_exp_minus_1)
lemma mask_Suc_rec:
- \<open>mask (Suc n) = 2 * mask n + 1\<close>
- by (simp add: mask_eq_mask mask_eq_exp_minus_1)
+ \<open>mask (Suc n) = 2 * mask n + (1 :: 'a::len word)\<close>
+ by (simp add: mask_eq_exp_minus_1)
context
begin
qualified lemma bit_mask_iff:
\<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
- by (simp add: mask_eq_mask bit_mask_iff exp_eq_zero_iff not_le)
+ by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
end
@@ -4188,7 +4170,8 @@
lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
-lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
+lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2 ^ n"
+ for x :: \<open>'a::len word\<close>
unfolding word_size by (erule and_mask_less')
lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
@@ -4212,6 +4195,7 @@
by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
+ for x :: \<open>'a::len word\<close>
using word_of_int_Ex [where x=x]
by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
@@ -5365,10 +5349,6 @@
"(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
by simp
-lemma mask_0 [simp]:
- "mask 0 = 0"
- by (simp add: Word.mask_def)
-
lemma shiftl0:
"x << 0 = (x :: 'a :: len word)"
by (fact shiftl_x_0)
@@ -5379,7 +5359,7 @@
lemma mask_Suc_0: "mask (Suc 0) = 1"
using mask_1 by simp
-lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + 1"
+lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + (1 :: 'a::len word)"
by (simp add: mask_Suc_rec numeral_eq_Suc)
lemma bin_last_bintrunc: "bin_last (bintrunc l n) = (l > 0 \<and> bin_last n)"
--- a/src/HOL/ex/Word.thy Tue Aug 04 09:24:00 2020 +0000
+++ b/src/HOL/ex/Word.thy Tue Aug 04 09:33:05 2020 +0000
@@ -644,19 +644,12 @@
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
+lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
+ is mask .
+
+instance by (standard; transfer)
+ (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+ bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
end