uniform mask operation
authorhaftmann
Tue Aug 04 09:33:05 2020 +0000 (6 weeks ago)
changeset 7208241393ecb57ac
parent 72081 e4d42f5766dc
child 72083 3ec876181527
child 72084 df99d26efeeb
uniform mask operation
NEWS
src/HOL/Library/Bit_Operations.thy
src/HOL/Library/Z2.thy
src/HOL/Word/Word.thy
src/HOL/ex/Word.thy
     1.1 --- a/NEWS	Tue Aug 04 09:24:00 2020 +0000
     1.2 +++ b/NEWS	Tue Aug 04 09:33:05 2020 +0000
     1.3 @@ -83,6 +83,13 @@
     1.4  * Session HOL-Word: Compound operation "bin_split" simplifies by default
     1.5  into its components "drop_bit" and "take_bit".  INCOMPATIBILITY.
     1.6  
     1.7 +* Session HOL-Word: Uniform polymorphic "mask" operation for both
     1.8 +types int and word.  INCOMPATIBILITY
     1.9 +
    1.10 +* Session HOL-Word: Operations lsb, msb and set_bit are separated
    1.11 +into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14  * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
    1.15  "bintrunc", "sbintrunc", "norm_sint", "bin_cat" and "max_word" are now
    1.16  mere input abbreviations.  Minor INCOMPATIBILITY.
    1.17 @@ -90,10 +97,6 @@
    1.18  * Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
    1.19  Minor INCOMPATIBILITY.
    1.20  
    1.21 -* Session HOL-Word: Operations lsb, msb and set_bit are separated
    1.22 -into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
    1.23 -INCOMPATIBILITY.
    1.24 -
    1.25  * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" commands
    1.26  are in working order again, as opposed to outputting "GaveUp" on nearly
    1.27  all problems.
     2.1 --- a/src/HOL/Library/Bit_Operations.thy	Tue Aug 04 09:24:00 2020 +0000
     2.2 +++ b/src/HOL/Library/Bit_Operations.thy	Tue Aug 04 09:33:05 2020 +0000
     2.3 @@ -15,9 +15,11 @@
     2.4    fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>AND\<close> 64)
     2.5      and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>OR\<close>  59)
     2.6      and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>XOR\<close> 59)
     2.7 +    and mask :: \<open>nat \<Rightarrow> 'a\<close>
     2.8    assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
     2.9      and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
    2.10      and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
    2.11 +    and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
    2.12  begin
    2.13  
    2.14  text \<open>
    2.15 @@ -93,9 +95,6 @@
    2.16    \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
    2.17    by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
    2.18  
    2.19 -definition mask :: \<open>nat \<Rightarrow> 'a\<close>
    2.20 -  where mask_eq_exp_minus_1: \<open>mask n = 2 ^ n - 1\<close>
    2.21 -
    2.22  lemma bit_mask_iff:
    2.23    \<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
    2.24    by (simp add: mask_eq_exp_minus_1 bit_mask_iff)
    2.25 @@ -104,25 +103,33 @@
    2.26    \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
    2.27    using bit_mask_iff [of n 0] by auto
    2.28  
    2.29 -lemma mask_0 [simp, code]:
    2.30 +lemma mask_0 [simp]:
    2.31    \<open>mask 0 = 0\<close>
    2.32    by (simp add: mask_eq_exp_minus_1)
    2.33  
    2.34 -lemma mask_Suc_exp [code]:
    2.35 +lemma mask_Suc_0 [simp]:
    2.36 +  \<open>mask (Suc 0) = 1\<close>
    2.37 +  by (simp add: mask_eq_exp_minus_1 add_implies_diff sym)
    2.38 +
    2.39 +lemma mask_Suc_exp:
    2.40    \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
    2.41    by (rule bit_eqI)
    2.42      (auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq)
    2.43  
    2.44  lemma mask_Suc_double:
    2.45 -  \<open>mask (Suc n) = 2 * mask n OR 1\<close>
    2.46 +  \<open>mask (Suc n) = 1 OR 2 * mask n\<close>
    2.47  proof (rule bit_eqI)
    2.48    fix q
    2.49    assume \<open>2 ^ q \<noteq> 0\<close>
    2.50 -  show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (2 * mask n OR 1) q\<close>
    2.51 +  show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (1 OR 2 * mask n) q\<close>
    2.52      by (cases q)
    2.53        (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)
    2.54  qed
    2.55  
    2.56 +lemma mask_numeral:
    2.57 +  \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
    2.58 +  by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)
    2.59 +
    2.60  lemma take_bit_eq_mask:
    2.61    \<open>take_bit n a = a AND mask n\<close>
    2.62    by (rule bit_eqI)
    2.63 @@ -495,6 +502,9 @@
    2.64    \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close> for k l :: int
    2.65    by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff)
    2.66  
    2.67 +definition mask_int :: \<open>nat \<Rightarrow> int\<close>
    2.68 +  where \<open>mask n = (2 :: int) ^ n - 1\<close>
    2.69 +
    2.70  instance proof
    2.71    fix k l :: int and n :: nat
    2.72    show \<open>- k = NOT (k - 1)\<close>
    2.73 @@ -505,7 +515,7 @@
    2.74      by (fact bit_or_int_iff)
    2.75    show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
    2.76      by (fact bit_xor_int_iff)
    2.77 -qed (simp_all add: bit_not_int_iff)
    2.78 +qed (simp_all add: bit_not_int_iff mask_int_def)
    2.79  
    2.80  end
    2.81  
    2.82 @@ -976,6 +986,9 @@
    2.83  definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
    2.84    where \<open>m XOR n = nat (int m XOR int n)\<close> for m n :: nat
    2.85  
    2.86 +definition mask_nat :: \<open>nat \<Rightarrow> nat\<close>
    2.87 +  where \<open>mask n = (2 :: nat) ^ n - 1\<close>
    2.88 +
    2.89  instance proof
    2.90    fix m n q :: nat
    2.91    show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
    2.92 @@ -984,7 +997,7 @@
    2.93      by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff)
    2.94    show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
    2.95      by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff)
    2.96 -qed
    2.97 +qed (simp add: mask_nat_def)
    2.98  
    2.99  end
   2.100  
   2.101 @@ -1044,19 +1057,12 @@
   2.102  lift_definition xor_integer ::  \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close>
   2.103    is xor .
   2.104  
   2.105 -instance proof
   2.106 -  fix k l :: \<open>integer\<close> and n :: nat
   2.107 -  show \<open>- k = NOT (k - 1)\<close>
   2.108 -    by transfer (simp add: minus_eq_not_minus_1)
   2.109 -  show \<open>bit (NOT k) n \<longleftrightarrow> (2 :: integer) ^ n \<noteq> 0 \<and> \<not> bit k n\<close>
   2.110 -    by transfer (fact bit_not_iff)
   2.111 -  show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
   2.112 -    by transfer (fact bit_and_iff)
   2.113 -  show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
   2.114 -    by transfer (fact bit_or_iff)
   2.115 -  show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
   2.116 -    by transfer (fact bit_xor_iff)
   2.117 -qed
   2.118 +lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close>
   2.119 +  is mask .
   2.120 +
   2.121 +instance by (standard; transfer)
   2.122 +  (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1
   2.123 +    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
   2.124  
   2.125  end
   2.126  
   2.127 @@ -1072,15 +1078,11 @@
   2.128  lift_definition xor_natural ::  \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close>
   2.129    is xor .
   2.130  
   2.131 -instance proof
   2.132 -  fix m n :: \<open>natural\<close> and q :: nat
   2.133 -  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
   2.134 -    by transfer (fact bit_and_iff)
   2.135 -  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
   2.136 -    by transfer (fact bit_or_iff)
   2.137 -  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
   2.138 -    by transfer (fact bit_xor_iff)
   2.139 -qed
   2.140 +lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close>
   2.141 +  is mask .
   2.142 +
   2.143 +instance by (standard; transfer)
   2.144 +  (simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff)
   2.145  
   2.146  end
   2.147  
     3.1 --- a/src/HOL/Library/Z2.thy	Tue Aug 04 09:24:00 2020 +0000
     3.2 +++ b/src/HOL/Library/Z2.thy	Tue Aug 04 09:33:05 2020 +0000
     3.3 @@ -187,6 +187,9 @@
     3.4  definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
     3.5    where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit
     3.6  
     3.7 +definition mask_bit :: \<open>nat \<Rightarrow> bit\<close>
     3.8 +  where [simp]: \<open>mask_bit n = of_bool (n > 0)\<close>
     3.9 +
    3.10  instance
    3.11    by standard auto
    3.12  
     4.1 --- a/src/HOL/Word/Word.thy	Tue Aug 04 09:24:00 2020 +0000
     4.2 +++ b/src/HOL/Word/Word.thy	Tue Aug 04 09:33:05 2020 +0000
     4.3 @@ -1000,19 +1000,13 @@
     4.4    is xor
     4.5    by simp
     4.6  
     4.7 -instance proof
     4.8 -  fix a b :: \<open>'a word\<close> and n :: nat
     4.9 -  show \<open>- a = NOT (a - 1)\<close>
    4.10 -    by transfer (simp add: minus_eq_not_minus_1)
    4.11 -  show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
    4.12 -    by transfer (simp add: bit_not_iff)
    4.13 -  show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
    4.14 -    by transfer (auto simp add: bit_and_iff)
    4.15 -  show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
    4.16 -    by transfer (auto simp add: bit_or_iff)
    4.17 -  show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
    4.18 -    by transfer (auto simp add: bit_xor_iff)
    4.19 -qed
    4.20 +lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
    4.21 +  is mask
    4.22 +  .
    4.23 +
    4.24 +instance by (standard; transfer)
    4.25 +  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
    4.26 +    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
    4.27  
    4.28  end
    4.29  
    4.30 @@ -1173,6 +1167,11 @@
    4.31    \<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close>
    4.32    by (fact take_bit_eq_mask)
    4.33  
    4.34 +lemma [code]:
    4.35 +  \<open>mask (Suc n) = push_bit n (1 :: 'a word) OR mask n\<close>
    4.36 +  \<open>mask 0 = (0 :: 'a::len word)\<close>
    4.37 +  by (simp_all add: mask_Suc_exp push_bit_of_1)
    4.38 +
    4.39  lemma [code_abbrev]:
    4.40    \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
    4.41    by (fact push_bit_of_1)
    4.42 @@ -1289,9 +1288,6 @@
    4.43    is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close>
    4.44    by (fact arg_cong)
    4.45  
    4.46 -lift_definition mask :: \<open>nat \<Rightarrow> 'a::len word\<close>
    4.47 -  is \<open>take_bit LENGTH('a) \<circ> Bit_Operations.mask\<close> .
    4.48 -
    4.49  lemma sshiftr1_eq:
    4.50    \<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close>
    4.51    by transfer simp
    4.52 @@ -1328,7 +1324,7 @@
    4.53  qed
    4.54  
    4.55  lemma mask_eq:
    4.56 -  \<open>mask n = (1 << n) - 1\<close>
    4.57 +  \<open>mask n = (1 << n) - (1 :: 'a::len word)\<close>
    4.58    by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) 
    4.59  
    4.60  lemma uint_sshiftr_eq [code]:
    4.61 @@ -1977,18 +1973,8 @@
    4.62  lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))"
    4.63    by transfer (simp add: bit_take_bit_iff ac_simps)
    4.64  
    4.65 -context
    4.66 -  includes lifting_syntax
    4.67 -begin
    4.68 -
    4.69 -lemma transfer_rule_mask_word [transfer_rule]:
    4.70 -  \<open>((=) ===> pcr_word) Bit_Operations.mask Bit_Operations.mask\<close>
    4.71 -  by (simp only: mask_eq_exp_minus_1 [abs_def]) transfer_prover
    4.72 -
    4.73 -end
    4.74 -
    4.75  lemma ucast_mask_eq:
    4.76 -  \<open>ucast (Bit_Operations.mask n :: 'b word) = Bit_Operations.mask (min LENGTH('b::len) n)\<close>
    4.77 +  \<open>ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\<close>
    4.78    by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff)
    4.79  
    4.80  \<comment> \<open>literal u(s)cast\<close>
    4.81 @@ -4075,27 +4061,23 @@
    4.82  subsubsection \<open>Mask\<close>
    4.83  
    4.84  lemma minus_1_eq_mask:
    4.85 -  \<open>- 1 = (Bit_Operations.mask LENGTH('a) :: 'a::len word)\<close>
    4.86 +  \<open>- 1 = (mask LENGTH('a) :: 'a::len word)\<close>
    4.87    by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff)
    4.88 -  
    4.89 -lemma mask_eq_mask [code]:
    4.90 -  \<open>mask = Bit_Operations.mask\<close>
    4.91 -  by (rule ext, transfer) simp
    4.92  
    4.93  lemma mask_eq_decr_exp:
    4.94 -  \<open>mask n = 2 ^ n - 1\<close>
    4.95 -  by (simp add: mask_eq_mask mask_eq_exp_minus_1)
    4.96 +  \<open>mask n = 2 ^ n - (1 :: 'a::len word)\<close>
    4.97 +  by (fact mask_eq_exp_minus_1)
    4.98  
    4.99  lemma mask_Suc_rec:
   4.100 -  \<open>mask (Suc n) = 2 * mask n + 1\<close>
   4.101 -  by (simp add: mask_eq_mask mask_eq_exp_minus_1)
   4.102 +  \<open>mask (Suc n) = 2 * mask n + (1 :: 'a::len word)\<close>
   4.103 +  by (simp add: mask_eq_exp_minus_1)
   4.104  
   4.105  context
   4.106  begin
   4.107  
   4.108  qualified lemma bit_mask_iff:
   4.109    \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
   4.110 -  by (simp add: mask_eq_mask bit_mask_iff exp_eq_zero_iff not_le)
   4.111 +  by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
   4.112  
   4.113  end
   4.114  
   4.115 @@ -4188,7 +4170,8 @@
   4.116  
   4.117  lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
   4.118  
   4.119 -lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
   4.120 +lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2 ^ n"
   4.121 +  for x :: \<open>'a::len word\<close>
   4.122    unfolding word_size by (erule and_mask_less')
   4.123  
   4.124  lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
   4.125 @@ -4212,6 +4195,7 @@
   4.126    by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
   4.127  
   4.128  lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
   4.129 +  for x :: \<open>'a::len word\<close>
   4.130    using word_of_int_Ex [where x=x]
   4.131    by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
   4.132  
   4.133 @@ -5365,10 +5349,6 @@
   4.134    "(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
   4.135    by simp
   4.136  
   4.137 -lemma mask_0 [simp]:
   4.138 -  "mask 0 = 0"
   4.139 -  by (simp add: Word.mask_def)
   4.140 -
   4.141  lemma shiftl0:
   4.142    "x << 0 = (x :: 'a :: len word)"
   4.143    by (fact shiftl_x_0)
   4.144 @@ -5379,7 +5359,7 @@
   4.145  lemma mask_Suc_0: "mask (Suc 0) = 1"
   4.146    using mask_1 by simp
   4.147  
   4.148 -lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + 1"
   4.149 +lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + (1 :: 'a::len word)"
   4.150    by (simp add: mask_Suc_rec numeral_eq_Suc)
   4.151  
   4.152  lemma bin_last_bintrunc: "bin_last (bintrunc l n) = (l > 0 \<and> bin_last n)"
     5.1 --- a/src/HOL/ex/Word.thy	Tue Aug 04 09:24:00 2020 +0000
     5.2 +++ b/src/HOL/ex/Word.thy	Tue Aug 04 09:33:05 2020 +0000
     5.3 @@ -644,19 +644,12 @@
     5.4    is xor
     5.5    by simp
     5.6  
     5.7 -instance proof
     5.8 -  fix a b :: \<open>'a word\<close> and n :: nat
     5.9 -  show \<open>- a = NOT (a - 1)\<close>
    5.10 -    by transfer (simp add: minus_eq_not_minus_1)
    5.11 -  show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
    5.12 -    by transfer (simp add: bit_not_iff)
    5.13 -  show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
    5.14 -    by transfer (auto simp add: bit_and_iff)
    5.15 -  show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
    5.16 -    by transfer (auto simp add: bit_or_iff)
    5.17 -  show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
    5.18 -    by transfer (auto simp add: bit_xor_iff)
    5.19 -qed
    5.20 +lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
    5.21 +  is mask .
    5.22 +
    5.23 +instance by (standard; transfer)
    5.24 +  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
    5.25 +    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
    5.26  
    5.27  end
    5.28