# HG changeset patch
# User haftmann
# Date 1596533585 0
# Node ID 41393ecb57ace7ccd69e36f6a377678f50d4512a
# Parent  e4d42f5766dc30fdb7ed0d870bc7eb3d690c0369
uniform mask operation

diff -r e4d42f5766dc -r 41393ecb57ac NEWS
--- 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.
diff -r e4d42f5766dc -r 41393ecb57ac src/HOL/Library/Bit_Operations.thy
--- 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
 
diff -r e4d42f5766dc -r 41393ecb57ac src/HOL/Library/Z2.thy
--- 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
 
diff -r e4d42f5766dc -r 41393ecb57ac src/HOL/Word/Word.thy
--- 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)"
diff -r e4d42f5766dc -r 41393ecb57ac src/HOL/ex/Word.thy
--- 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