998 |
998 |
999 lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> |
999 lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> |
1000 is xor |
1000 is xor |
1001 by simp |
1001 by simp |
1002 |
1002 |
1003 instance proof |
1003 lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close> |
1004 fix a b :: \<open>'a word\<close> and n :: nat |
1004 is mask |
1005 show \<open>- a = NOT (a - 1)\<close> |
1005 . |
1006 by transfer (simp add: minus_eq_not_minus_1) |
1006 |
1007 show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close> |
1007 instance by (standard; transfer) |
1008 by transfer (simp add: bit_not_iff) |
1008 (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 |
1009 show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close> |
1009 bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) |
1010 by transfer (auto simp add: bit_and_iff) |
|
1011 show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close> |
|
1012 by transfer (auto simp add: bit_or_iff) |
|
1013 show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close> |
|
1014 by transfer (auto simp add: bit_xor_iff) |
|
1015 qed |
|
1016 |
1010 |
1017 end |
1011 end |
1018 |
1012 |
1019 context |
1013 context |
1020 includes lifting_syntax |
1014 includes lifting_syntax |
1170 by (simp add: shiftr_word_eq) |
1164 by (simp add: shiftr_word_eq) |
1171 |
1165 |
1172 lemma [code]: |
1166 lemma [code]: |
1173 \<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close> |
1167 \<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close> |
1174 by (fact take_bit_eq_mask) |
1168 by (fact take_bit_eq_mask) |
|
1169 |
|
1170 lemma [code]: |
|
1171 \<open>mask (Suc n) = push_bit n (1 :: 'a word) OR mask n\<close> |
|
1172 \<open>mask 0 = (0 :: 'a::len word)\<close> |
|
1173 by (simp_all add: mask_Suc_exp push_bit_of_1) |
1175 |
1174 |
1176 lemma [code_abbrev]: |
1175 lemma [code_abbrev]: |
1177 \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> |
1176 \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> |
1178 by (fact push_bit_of_1) |
1177 by (fact push_bit_of_1) |
1179 |
1178 |
1287 |
1286 |
1288 lift_definition bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close> |
1287 lift_definition bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close> |
1289 is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close> |
1288 is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a) - Suc 0)\<close> |
1290 by (fact arg_cong) |
1289 by (fact arg_cong) |
1291 |
1290 |
1292 lift_definition mask :: \<open>nat \<Rightarrow> 'a::len word\<close> |
|
1293 is \<open>take_bit LENGTH('a) \<circ> Bit_Operations.mask\<close> . |
|
1294 |
|
1295 lemma sshiftr1_eq: |
1291 lemma sshiftr1_eq: |
1296 \<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close> |
1292 \<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close> |
1297 by transfer simp |
1293 by transfer simp |
1298 |
1294 |
1299 lemma bshiftr1_eq: |
1295 lemma bshiftr1_eq: |
1326 done |
1322 done |
1327 done |
1323 done |
1328 qed |
1324 qed |
1329 |
1325 |
1330 lemma mask_eq: |
1326 lemma mask_eq: |
1331 \<open>mask n = (1 << n) - 1\<close> |
1327 \<open>mask n = (1 << n) - (1 :: 'a::len word)\<close> |
1332 by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) |
1328 by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) |
1333 |
1329 |
1334 lemma uint_sshiftr_eq [code]: |
1330 lemma uint_sshiftr_eq [code]: |
1335 \<open>uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\<close> |
1331 \<open>uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\<close> |
1336 for w :: \<open>'a::len word\<close> |
1332 for w :: \<open>'a::len word\<close> |
1975 by transfer simp |
1971 by transfer simp |
1976 |
1972 |
1977 lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))" |
1973 lemma nth_ucast: "(ucast w::'a::len word) !! n = (w !! n \<and> n < LENGTH('a))" |
1978 by transfer (simp add: bit_take_bit_iff ac_simps) |
1974 by transfer (simp add: bit_take_bit_iff ac_simps) |
1979 |
1975 |
1980 context |
|
1981 includes lifting_syntax |
|
1982 begin |
|
1983 |
|
1984 lemma transfer_rule_mask_word [transfer_rule]: |
|
1985 \<open>((=) ===> pcr_word) Bit_Operations.mask Bit_Operations.mask\<close> |
|
1986 by (simp only: mask_eq_exp_minus_1 [abs_def]) transfer_prover |
|
1987 |
|
1988 end |
|
1989 |
|
1990 lemma ucast_mask_eq: |
1976 lemma ucast_mask_eq: |
1991 \<open>ucast (Bit_Operations.mask n :: 'b word) = Bit_Operations.mask (min LENGTH('b::len) n)\<close> |
1977 \<open>ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\<close> |
1992 by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff) |
1978 by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff) |
1993 |
1979 |
1994 \<comment> \<open>literal u(s)cast\<close> |
1980 \<comment> \<open>literal u(s)cast\<close> |
1995 lemma ucast_bintr [simp]: |
1981 lemma ucast_bintr [simp]: |
1996 "ucast (numeral w :: 'a::len word) = |
1982 "ucast (numeral w :: 'a::len word) = |
4073 |
4059 |
4074 |
4060 |
4075 subsubsection \<open>Mask\<close> |
4061 subsubsection \<open>Mask\<close> |
4076 |
4062 |
4077 lemma minus_1_eq_mask: |
4063 lemma minus_1_eq_mask: |
4078 \<open>- 1 = (Bit_Operations.mask LENGTH('a) :: 'a::len word)\<close> |
4064 \<open>- 1 = (mask LENGTH('a) :: 'a::len word)\<close> |
4079 by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff) |
4065 by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff) |
4080 |
|
4081 lemma mask_eq_mask [code]: |
|
4082 \<open>mask = Bit_Operations.mask\<close> |
|
4083 by (rule ext, transfer) simp |
|
4084 |
4066 |
4085 lemma mask_eq_decr_exp: |
4067 lemma mask_eq_decr_exp: |
4086 \<open>mask n = 2 ^ n - 1\<close> |
4068 \<open>mask n = 2 ^ n - (1 :: 'a::len word)\<close> |
4087 by (simp add: mask_eq_mask mask_eq_exp_minus_1) |
4069 by (fact mask_eq_exp_minus_1) |
4088 |
4070 |
4089 lemma mask_Suc_rec: |
4071 lemma mask_Suc_rec: |
4090 \<open>mask (Suc n) = 2 * mask n + 1\<close> |
4072 \<open>mask (Suc n) = 2 * mask n + (1 :: 'a::len word)\<close> |
4091 by (simp add: mask_eq_mask mask_eq_exp_minus_1) |
4073 by (simp add: mask_eq_exp_minus_1) |
4092 |
4074 |
4093 context |
4075 context |
4094 begin |
4076 begin |
4095 |
4077 |
4096 qualified lemma bit_mask_iff: |
4078 qualified lemma bit_mask_iff: |
4097 \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close> |
4079 \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close> |
4098 by (simp add: mask_eq_mask bit_mask_iff exp_eq_zero_iff not_le) |
4080 by (simp add: bit_mask_iff exp_eq_zero_iff not_le) |
4099 |
4081 |
4100 end |
4082 end |
4101 |
4083 |
4102 lemma nth_mask [simp]: |
4084 lemma nth_mask [simp]: |
4103 \<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close> |
4085 \<open>(mask n :: 'a::len word) !! i \<longleftrightarrow> i < n \<and> i < size (mask n :: 'a word)\<close> |
4186 |
4168 |
4187 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]] |
4169 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]] |
4188 |
4170 |
4189 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size] |
4171 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size] |
4190 |
4172 |
4191 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n" |
4173 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2 ^ n" |
|
4174 for x :: \<open>'a::len word\<close> |
4192 unfolding word_size by (erule and_mask_less') |
4175 unfolding word_size by (erule and_mask_less') |
4193 |
4176 |
4194 lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n" |
4177 lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n" |
4195 for c x :: "'a::len word" |
4178 for c x :: "'a::len word" |
4196 by (auto simp: word_mod_def uint_2p and_mask_mod_2p) |
4179 by (auto simp: word_mod_def uint_2p and_mask_mod_2p) |
4210 "word_pred (a AND mask n) AND mask n = word_pred a AND mask n" |
4193 "word_pred (a AND mask n) AND mask n = word_pred a AND mask n" |
4211 using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b] |
4194 using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b] |
4212 by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps) |
4195 by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps) |
4213 |
4196 |
4214 lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n" |
4197 lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n" |
|
4198 for x :: \<open>'a::len word\<close> |
4215 using word_of_int_Ex [where x=x] |
4199 using word_of_int_Ex [where x=x] |
4216 by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps) |
4200 by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps) |
4217 |
4201 |
4218 lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)" |
4202 lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)" |
4219 by transfer (simp add: take_bit_minus_one_eq_mask) |
4203 by transfer (simp add: take_bit_minus_one_eq_mask) |
5363 |
5347 |
5364 lemma test_bit_1' [simp]: |
5348 lemma test_bit_1' [simp]: |
5365 "(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0" |
5349 "(1 :: 'a :: len word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0" |
5366 by simp |
5350 by simp |
5367 |
5351 |
5368 lemma mask_0 [simp]: |
|
5369 "mask 0 = 0" |
|
5370 by (simp add: Word.mask_def) |
|
5371 |
|
5372 lemma shiftl0: |
5352 lemma shiftl0: |
5373 "x << 0 = (x :: 'a :: len word)" |
5353 "x << 0 = (x :: 'a :: len word)" |
5374 by (fact shiftl_x_0) |
5354 by (fact shiftl_x_0) |
5375 |
5355 |
5376 lemma mask_1: "mask 1 = 1" |
5356 lemma mask_1: "mask 1 = 1" |
5377 by transfer (simp add: min_def mask_Suc_exp) |
5357 by transfer (simp add: min_def mask_Suc_exp) |
5378 |
5358 |
5379 lemma mask_Suc_0: "mask (Suc 0) = 1" |
5359 lemma mask_Suc_0: "mask (Suc 0) = 1" |
5380 using mask_1 by simp |
5360 using mask_1 by simp |
5381 |
5361 |
5382 lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + 1" |
5362 lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + (1 :: 'a::len word)" |
5383 by (simp add: mask_Suc_rec numeral_eq_Suc) |
5363 by (simp add: mask_Suc_rec numeral_eq_Suc) |
5384 |
5364 |
5385 lemma bin_last_bintrunc: "bin_last (bintrunc l n) = (l > 0 \<and> bin_last n)" |
5365 lemma bin_last_bintrunc: "bin_last (bintrunc l n) = (l > 0 \<and> bin_last n)" |
5386 by simp |
5366 by simp |
5387 |
5367 |