# HG changeset patch # User haftmann # Date 1600336651 0 # Node ID a282abb076424d8ab34111edf9b865ab9202a80e # Parent 5193570b739a22d4403892e071fd4f4c174f4e4d integrated generic conversions into word corpse diff -r 5193570b739a -r a282abb07642 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/Divides.thy Thu Sep 17 09:57:31 2020 +0000 @@ -693,32 +693,6 @@ thus ?lhs by simp qed -lemma take_bit_greater_eq: - \k + 2 ^ n \ take_bit n k\ if \k < 0\ for k :: int -proof - - have \k + 2 ^ n \ take_bit n (k + 2 ^ n)\ - proof (cases \k > - (2 ^ n)\) - case False - then have \k + 2 ^ n \ 0\ - by simp - also note take_bit_nonnegative - finally show ?thesis . - next - case True - with that have \0 \ k + 2 ^ n\ and \k + 2 ^ n < 2 ^ n\ - by simp_all - then show ?thesis - by (simp only: take_bit_eq_mod mod_pos_pos_trivial) - qed - then show ?thesis - by (simp add: take_bit_eq_mod) -qed - -lemma take_bit_less_eq: - \take_bit n k \ k - 2 ^ n\ if \2 ^ n \ k\ and \n > 0\ for k :: int - using that zmod_le_nonneg_dividend [of \k - 2 ^ n\ \2 ^ n\] - by (simp add: take_bit_eq_mod) - subsection \Numeral division with a pragmatic type class\ @@ -1292,6 +1266,32 @@ by (simp add: take_bit_eq_mod) qed +lemma take_bit_int_greater_eq: + \k + 2 ^ n \ take_bit n k\ if \k < 0\ for k :: int +proof - + have \k + 2 ^ n \ take_bit n (k + 2 ^ n)\ + proof (cases \k > - (2 ^ n)\) + case False + then have \k + 2 ^ n \ 0\ + by simp + also note take_bit_nonnegative + finally show ?thesis . + next + case True + with that have \0 \ k + 2 ^ n\ and \k + 2 ^ n < 2 ^ n\ + by simp_all + then show ?thesis + by (simp only: take_bit_eq_mod mod_pos_pos_trivial) + qed + then show ?thesis + by (simp add: take_bit_eq_mod) +qed + +lemma take_bit_int_less_eq: + \take_bit n k \ k - 2 ^ n\ if \2 ^ n \ k\ and \n > 0\ for k :: int + using that zmod_le_nonneg_dividend [of \k - 2 ^ n\ \2 ^ n\] + by (simp add: take_bit_eq_mod) + lemma take_bit_int_less_eq_self_iff: \take_bit n k \ k \ 0 \ k\ (is \?P \ ?Q\) for k :: int @@ -1356,6 +1356,4 @@ lemma zmod_eq_0D [dest!]: "\q. m = d * q" if "m mod d = 0" for m d :: int using that by auto -find_theorems \(?k::int) mod _ = ?k\ - end diff -r 5193570b739a -r a282abb07642 src/HOL/Library/Bit_Operations.thy --- a/src/HOL/Library/Bit_Operations.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/Library/Bit_Operations.thy Thu Sep 17 09:57:31 2020 +0000 @@ -275,6 +275,20 @@ apply (use exp_eq_0_imp_not_bit in blast) done +lemma take_bit_not_eq_mask_diff: + \take_bit n (NOT a) = mask n - take_bit n a\ +proof - + have \take_bit n (NOT a) = take_bit n (NOT (take_bit n a))\ + by (simp add: take_bit_not_take_bit) + also have \\ = mask n AND NOT (take_bit n a)\ + by (simp add: take_bit_eq_mask ac_simps) + also have \\ = mask n - take_bit n a\ + by (subst disjunctive_diff) + (auto simp add: bit_take_bit_iff bit_mask_iff exp_eq_0_imp_not_bit) + finally show ?thesis + by simp +qed + lemma mask_eq_take_bit_minus_one: \mask n = take_bit n (- 1)\ by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute) @@ -1111,6 +1125,11 @@ for k :: int by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps) +lemma signed_take_bit_int_eq_self: + \signed_take_bit n k = k\ if \- (2 ^ n) \ k\ \k < 2 ^ n\ + for k :: int + using that by (simp add: signed_take_bit_int_eq_self_iff) + lemma signed_take_bit_int_less_eq_self_iff: \signed_take_bit n k \ k \ - (2 ^ n) \ k\ for k :: int @@ -1136,13 +1155,13 @@ lemma signed_take_bit_int_greater_eq: \k + 2 ^ Suc n \ signed_take_bit n k\ if \k < - (2 ^ n)\ for k :: int - using that take_bit_greater_eq [of \k + 2 ^ n\ \Suc n\] + using that take_bit_int_greater_eq [of \k + 2 ^ n\ \Suc n\] by (simp add: signed_take_bit_eq_take_bit_shift) lemma signed_take_bit_int_less_eq: \signed_take_bit n k \ k - 2 ^ Suc n\ if \k \ 2 ^ n\ for k :: int - using that take_bit_less_eq [of \Suc n\ \k + 2 ^ n\] + using that take_bit_int_less_eq [of \Suc n\ \k + 2 ^ n\] by (simp add: signed_take_bit_eq_take_bit_shift) lemma signed_take_bit_Suc_bit0 [simp]: diff -r 5193570b739a -r a282abb07642 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/Parity.thy Thu Sep 17 09:57:31 2020 +0000 @@ -1615,10 +1615,22 @@ \bit (push_bit m k) n \ m \ n \ bit k (n - m)\ for k :: int by (auto simp add: bit_push_bit_iff) -lemma take_bit_nat_less_exp: +lemma take_bit_nat_less_exp [simp]: \take_bit n m < 2 ^ n\ for n m ::nat by (simp add: take_bit_eq_mod) +lemma take_bit_nonnegative [simp]: + \take_bit n k \ 0\ for k :: int + by (simp add: take_bit_eq_mod) + +lemma not_take_bit_negative [simp]: + \\ take_bit n k < 0\ for k :: int + by (simp add: not_less) + +lemma take_bit_int_less_exp [simp]: + \take_bit n k < 2 ^ n\ for k :: int + by (simp add: take_bit_eq_mod) + lemma take_bit_nat_eq_self_iff: \take_bit n m = m \ m < 2 ^ n\ (is \?P \ ?Q\) for n m :: nat @@ -1633,23 +1645,9 @@ by (simp add: take_bit_eq_mod) qed -lemma take_bit_nat_less_eq_self: - \take_bit n m \ m\ for n m :: nat - by (simp add: take_bit_eq_mod) - -lemma take_bit_nonnegative [simp]: - \take_bit n k \ 0\ - for k :: int - by (simp add: take_bit_eq_mod) - -lemma not_take_bit_negative [simp]: - \\ take_bit n k < 0\ - for k :: int - by (simp add: not_less) - -lemma take_bit_int_less_exp: - \take_bit n k < 2 ^ n\ for k :: int - by (simp add: take_bit_eq_mod) +lemma take_bit_nat_eq_self: + \take_bit n m = m\ if \m < 2 ^ n\ for m n :: nat + using that by (simp add: take_bit_nat_eq_self_iff) lemma take_bit_int_eq_self_iff: \take_bit n k = k \ 0 \ k \ k < 2 ^ n\ (is \?P \ ?Q\) @@ -1665,6 +1663,30 @@ by (simp add: take_bit_eq_mod) qed +lemma take_bit_int_eq_self: + \take_bit n k = k\ if \0 \ k\ \k < 2 ^ n\ for k :: int + using that by (simp add: take_bit_int_eq_self_iff) + +lemma take_bit_nat_less_eq_self [simp]: + \take_bit n m \ m\ for n m :: nat + by (simp add: take_bit_eq_mod) + +lemma take_bit_nat_less_self_iff: + \take_bit n m < m \ 2 ^ n \ m\ (is \?P \ ?Q\) + for m n :: nat +proof + assume ?P + then have \take_bit n m \ m\ + by simp + then show \?Q\ + by (simp add: take_bit_nat_eq_self_iff) +next + have \take_bit n m < 2 ^ n\ + by (fact take_bit_nat_less_exp) + also assume ?Q + finally show ?P . +qed + class unique_euclidean_semiring_with_bit_shifts = unique_euclidean_semiring_with_nat + semiring_bit_shifts begin diff -r 5193570b739a -r a282abb07642 src/HOL/ROOT --- a/src/HOL/ROOT Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/ROOT Thu Sep 17 09:57:31 2020 +0000 @@ -898,7 +898,6 @@ Word More_Word Word_Examples - Conversions document_files "root.bib" "root.tex" session "HOL-Statespace" in Statespace = HOL + diff -r 5193570b739a -r a282abb07642 src/HOL/SPARK/Examples/RIPEMD-160/F.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Thu Sep 17 09:57:31 2020 +0000 @@ -26,7 +26,7 @@ proof - from H8 have "nat j <= 15" by simp with assms show ?thesis - by (simp add: f_def bwsimps int_word_uint) + by (simp add: f_def bwsimps int_word_uint take_bit_int_eq_self) qed spark_vc function_f_7 @@ -34,7 +34,8 @@ from H7 have "16 <= nat j" by simp moreover from H8 have "nat j <= 31" by simp ultimately show ?thesis using assms - by (simp add: f_def bwsimps int_word_uint) + by (simp only: f_def bwsimps int_word_uint) + (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1) qed spark_vc function_f_8 @@ -42,7 +43,7 @@ from H7 have "32 <= nat j" by simp moreover from H8 have "nat j <= 47" by simp ultimately show ?thesis using assms - by (simp add: f_def bwsimps int_word_uint) + by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1) qed spark_vc function_f_9 @@ -50,7 +51,7 @@ from H7 have "48 <= nat j" by simp moreover from H8 have "nat j <= 63" by simp ultimately show ?thesis using assms - by (simp add: f_def bwsimps int_word_uint) + by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1) qed spark_vc function_f_10 @@ -58,7 +59,7 @@ from H2 have "nat j <= 79" by simp moreover from H12 have "64 <= nat j" by simp ultimately show ?thesis using assms - by (simp add: f_def bwsimps int_word_uint) + by (simp only: f_def bwsimps int_word_uint) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1) qed spark_end diff -r 5193570b739a -r a282abb07642 src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Thu Sep 17 09:57:31 2020 +0000 @@ -63,7 +63,7 @@ proof (cases C) fix a b c d e f::word32 assume "C = (a, b, c, d, e)" - thus ?thesis by (cases a) simp + thus ?thesis by (cases a) (simp add: take_bit_nat_eq_self) qed lemma steps_to_steps': diff -r 5193570b739a -r a282abb07642 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Thu Sep 17 09:57:31 2020 +0000 @@ -253,7 +253,8 @@ show ?thesis unfolding steps'_step[OF \0 <= j\] step_hyp[symmetric] step_both_def step_r_def step_l_def - by (simp add: AL BL CL DL EL AR BR CR DR ER) + using AL CL EL AR CR ER + by (simp add: BL DL BR DR take_bit_int_eq_self_iff take_bit_int_eq_self) qed spark_vc procedure_round_61 @@ -275,12 +276,13 @@ h3 = cd, h4 = ce\\) 0 x" unfolding steps_def - by (simp add: + using uint_word_of_int_id[OF \0 <= ca\ \ca <= ?M\] uint_word_of_int_id[OF \0 <= cb\ \cb <= ?M\] uint_word_of_int_id[OF \0 <= cc\ \cc <= ?M\] uint_word_of_int_id[OF \0 <= cd\ \cd <= ?M\] - uint_word_of_int_id[OF \0 <= ce\ \ce <= ?M\]) + uint_word_of_int_id[OF \0 <= ce\ \ce <= ?M\] + by (simp add: take_bit_int_eq_self_iff take_bit_int_eq_self) let ?rotate_arg_l = "((((ca + f 0 cb cc cd) mod 4294967296 + x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)" @@ -458,7 +460,7 @@ unfolding steps_to_steps' unfolding H1[symmetric] by (simp add: uint_word_ariths(1) mod_simps - uint_word_of_int_id) + uint_word_of_int_id take_bit_int_eq_self) qed spark_end diff -r 5193570b739a -r a282abb07642 src/HOL/Word/Conversions.thy --- a/src/HOL/Word/Conversions.thy Thu Sep 17 09:57:30 2020 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,556 +0,0 @@ -(* Author: Florian Haftmann, TUM -*) - -section \Proof of concept for conversions for algebraically founded bit word types\ - -theory Conversions - imports - Main - "HOL-Library.Type_Length" - "HOL-Library.Bit_Operations" - "HOL-Word.Word" -begin - -hide_const (open) unat uint sint word_of_int ucast scast - -context semiring_bits -begin - -lemma - exp_add_not_zero_imp_left: \2 ^ m \ 0\ - and exp_add_not_zero_imp_right: \2 ^ n \ 0\ if \2 ^ (m + n) \ 0\ -proof - - have \\ (2 ^ m = 0 \ 2 ^ n = 0)\ - proof (rule notI) - assume \2 ^ m = 0 \ 2 ^ n = 0\ - then have \2 ^ (m + n) = 0\ - by (rule disjE) (simp_all add: power_add) - with that show False .. - qed - then show \2 ^ m \ 0\ and \2 ^ n \ 0\ - by simp_all -qed - -lemma exp_not_zero_imp_exp_diff_not_zero: - \2 ^ (n - m) \ 0\ if \2 ^ n \ 0\ -proof (cases \m \ n\) - case True - moreover define q where \q = n - m\ - ultimately have \n = m + q\ - by simp - with that show ?thesis - by (simp add: exp_add_not_zero_imp_right) -next - case False - with that show ?thesis - by simp -qed - -end - - -subsection \Conversions to word\ - -abbreviation word_of_nat :: \nat \ 'a::len word\ - where \word_of_nat \ of_nat\ - -abbreviation word_of_int :: \int \ 'a::len word\ - where \word_of_int \ of_int\ - -lemma Word_eq_word_of_int [simp]: - \Word.Word = word_of_int\ - by (rule ext; transfer) simp - -lemma word_of_nat_eq_iff: - \word_of_nat m = (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ - by transfer (simp add: take_bit_of_nat) - -lemma word_of_int_eq_iff: - \word_of_int k = (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ - by transfer rule - -lemma word_of_nat_less_eq_iff: - \word_of_nat m \ (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ - by transfer (simp add: take_bit_of_nat) - -lemma word_of_int_less_eq_iff: - \word_of_int k \ (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ - by transfer rule - -lemma word_of_nat_less_iff: - \word_of_nat m < (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ - by transfer (simp add: take_bit_of_nat) - -lemma word_of_int_less_iff: - \word_of_int k < (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ - by transfer rule - -lemma word_of_nat_eq_0_iff [simp]: - \word_of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ - using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) - -lemma word_of_int_eq_0_iff [simp]: - \word_of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ - using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) - - -subsection \Conversion from word\ - -subsubsection \Generic unsigned conversion\ - -context semiring_1 -begin - -lift_definition unsigned :: \'b::len word \ 'a\ - is \of_nat \ nat \ take_bit LENGTH('b)\ - by simp - -lemma unsigned_0 [simp]: - \unsigned 0 = 0\ - by transfer simp - -lemma unsigned_1 [simp]: - \unsigned 1 = 1\ - by transfer simp - -end - -context semiring_char_0 -begin - -lemma unsigned_word_eqI: - \v = w\ if \unsigned v = unsigned w\ - using that by transfer (simp add: eq_nat_nat_iff) - -lemma word_eq_iff_unsigned: - \v = w \ unsigned v = unsigned w\ - by (auto intro: unsigned_word_eqI) - -end - -context semiring_bits -begin - -lemma bit_unsigned_iff: - \bit (unsigned w) n \ 2 ^ n \ 0 \ bit w n\ - for w :: \'b::len word\ - by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff) - -end - -context semiring_bit_shifts -begin - -lemma unsigned_push_bit_eq: - \unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\ - for w :: \'b::len word\ -proof (rule bit_eqI) - fix m - assume \2 ^ m \ 0\ - show \bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\ - proof (cases \n \ m\) - case True - with \2 ^ m \ 0\ have \2 ^ (m - n) \ 0\ - by (metis (full_types) diff_add exp_add_not_zero_imp) - with True show ?thesis - by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff ac_simps exp_eq_zero_iff not_le) - next - case False - then show ?thesis - by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff) - qed -qed - -lemma unsigned_take_bit_eq: - \unsigned (take_bit n w) = take_bit n (unsigned w)\ - for w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff) - -end - -context semiring_bit_operations -begin - -lemma unsigned_and_eq: - \unsigned (v AND w) = unsigned v AND unsigned w\ - for v w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff) - -lemma unsigned_or_eq: - \unsigned (v OR w) = unsigned v OR unsigned w\ - for v w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff) - -lemma unsigned_xor_eq: - \unsigned (v XOR w) = unsigned v XOR unsigned w\ - for v w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff) - -end - -context ring_bit_operations -begin - -lemma unsigned_not_eq: - \unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\ - for w :: \'b::len word\ - by (rule bit_eqI) - (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le) - -end - -lemma unsigned_of_nat [simp]: - \unsigned (word_of_nat n :: 'a::len word) = of_nat (take_bit LENGTH('a) n)\ - by transfer (simp add: nat_eq_iff take_bit_of_nat) - -lemma unsigned_of_int [simp]: - \unsigned (word_of_int n :: 'a::len word) = of_int (take_bit LENGTH('a) n)\ - by transfer (simp add: nat_eq_iff take_bit_of_nat) - -context unique_euclidean_semiring_numeral -begin - -lemma unsigned_greater_eq: - \0 \ unsigned w\ for w :: \'b::len word\ - by (transfer fixing: less_eq) simp - -lemma unsigned_less: - \unsigned w < 2 ^ LENGTH('b)\ for w :: \'b::len word\ - by (transfer fixing: less) (simp add: take_bit_int_less_exp) - -end - -context linordered_semidom -begin - -lemma word_less_eq_iff_unsigned: - "a \ b \ unsigned a \ unsigned b" - by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) - -lemma word_less_iff_unsigned: - "a < b \ unsigned a < unsigned b" - by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) - -end - - -subsubsection \Generic signed conversion\ - -context ring_1 -begin - -lift_definition signed :: \'b::len word \ 'a\ - is \of_int \ signed_take_bit (LENGTH('b) - Suc 0)\ - by (simp flip: signed_take_bit_decr_length_iff) - -lemma signed_0 [simp]: - \signed 0 = 0\ - by transfer simp - -lemma signed_1 [simp]: - \signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\ - by (transfer fixing: uminus; cases \LENGTH('b)\) - (simp_all add: sbintrunc_minus_simps) - -lemma signed_minus_1 [simp]: - \signed (- 1 :: 'b::len word) = - 1\ - by (transfer fixing: uminus) simp - -end - -context ring_char_0 -begin - -lemma signed_word_eqI: - \v = w\ if \signed v = signed w\ - using that by transfer (simp flip: signed_take_bit_decr_length_iff) - -lemma word_eq_iff_signed: - \v = w \ signed v = signed w\ - by (auto intro: signed_word_eqI) - -end - -context ring_bit_operations -begin - -lemma bit_signed_iff: - \bit (signed w) n \ 2 ^ n \ 0 \ bit w (min (LENGTH('b) - Suc 0) n)\ - for w :: \'b::len word\ - by (transfer fixing: bit) - (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def) - -lemma signed_push_bit_eq: - \signed (push_bit n w) = signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))\ - for w :: \'b::len word\ -proof (rule bit_eqI) - fix m - assume \2 ^ m \ 0\ - define q where \q = LENGTH('b) - Suc 0\ - then have *: \LENGTH('b) = Suc q\ - by simp - show \bit (signed (push_bit n w)) m \ - bit (signed_take_bit (LENGTH('b) - 1) (push_bit n (signed w :: 'a))) m\ - proof (cases \q \ m\) - case True - moreover define r where \r = m - q\ - ultimately have \m = q + r\ - by simp - moreover from \m = q + r\ \2 ^ m \ 0\ have \2 ^ q \ 0\ \2 ^ r \ 0\ - using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r] - by simp_all - moreover from \2 ^ q \ 0\ have \2 ^ (q - n) \ 0\ - by (rule exp_not_zero_imp_exp_diff_not_zero) - ultimately show ?thesis - by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff - min_def * exp_eq_zero_iff le_diff_conv2) - next - case False - then show ?thesis - using exp_not_zero_imp_exp_diff_not_zero [of m n] - by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff - min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit - exp_eq_zero_iff) - qed -qed - -lemma signed_take_bit_eq: - \signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\ - for w :: \'b::len word\ - by (transfer fixing: take_bit; cases \LENGTH('b)\) - (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq) - -lemma signed_not_eq: - \signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\ - for w :: \'b::len word\ -proof (rule bit_eqI) - fix n - assume \2 ^ n \ 0\ - define q where \q = LENGTH('b) - Suc 0\ - then have *: \LENGTH('b) = Suc q\ - by simp - show \bit (signed (NOT w)) n \ - bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\ - proof (cases \q < n\) - case True - moreover define r where \r = n - Suc q\ - ultimately have \n = r + Suc q\ - by simp - moreover from \2 ^ n \ 0\ \n = r + Suc q\ - have \2 ^ Suc q \ 0\ - using exp_add_not_zero_imp_right by blast - ultimately show ?thesis - by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def - exp_eq_zero_iff) - next - case False - then show ?thesis - by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def - exp_eq_zero_iff) - qed -qed - -lemma signed_and_eq: - \signed (v AND w) = signed v AND signed w\ - for v w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff) - -lemma signed_or_eq: - \signed (v OR w) = signed v OR signed w\ - for v w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff) - -lemma signed_xor_eq: - \signed (v XOR w) = signed v XOR signed w\ - for v w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff) - -end - -lemma signed_of_nat [simp]: - \signed (word_of_nat n :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - Suc 0) (int n))\ - by transfer simp - -lemma signed_of_int [simp]: - \signed (word_of_int n :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - Suc 0) n)\ - by transfer simp - - -subsubsection \Important special cases\ - -abbreviation unat :: \'a::len word \ nat\ - where \unat \ unsigned\ - -abbreviation uint :: \'a::len word \ int\ - where \uint \ unsigned\ - -abbreviation sint :: \'a::len word \ int\ - where \sint \ signed\ - -abbreviation ucast :: \'a::len word \ 'b::len word\ - where \ucast \ unsigned\ - -abbreviation scast :: \'a::len word \ 'b::len word\ - where \scast \ signed\ - -context - includes lifting_syntax -begin - -lemma [transfer_rule]: - \(pcr_word ===> (=)) (nat \ take_bit LENGTH('a)) (unat :: 'a::len word \ nat)\ - using unsigned.transfer [where ?'a = nat] by simp - -lemma [transfer_rule]: - \(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \ int)\ - using unsigned.transfer [where ?'a = int] by (simp add: comp_def) - -lemma [transfer_rule]: - \(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \ int)\ - using signed.transfer [where ?'a = int] by simp - -lemma [transfer_rule]: - \(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \ 'b::len word)\ -proof (rule rel_funI) - fix k :: int and w :: \'a word\ - assume \pcr_word k w\ - then have \w = word_of_int k\ - by (simp add: pcr_word_def cr_word_def relcompp_apply) - moreover have \pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\ - by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) - ultimately show \pcr_word (take_bit LENGTH('a) k) (ucast w)\ - by simp -qed - -lemma [transfer_rule]: - \(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \ 'b::len word)\ -proof (rule rel_funI) - fix k :: int and w :: \'a word\ - assume \pcr_word k w\ - then have \w = word_of_int k\ - by (simp add: pcr_word_def cr_word_def relcompp_apply) - moreover have \pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\ - by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) - ultimately show \pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\ - by simp -qed - -end - -lemma of_nat_unat [simp]: - \of_nat (unat w) = unsigned w\ - by transfer simp - -lemma of_int_uint [simp]: - \of_int (uint w) = unsigned w\ - by transfer simp - -lemma unat_div_distrib: - \unat (v div w) = unat v div unat w\ -proof transfer - fix k l - have \nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \ nat (take_bit LENGTH('a) k)\ - by (rule div_le_dividend) - also have \nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\ - by (simp add: nat_less_iff take_bit_int_less_exp) - finally show \(nat \ take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) = - (nat \ take_bit LENGTH('a)) k div (nat \ take_bit LENGTH('a)) l\ - by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff) -qed - -lemma unat_mod_distrib: - \unat (v mod w) = unat v mod unat w\ -proof transfer - fix k l - have \nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \ nat (take_bit LENGTH('a) k)\ - by (rule mod_less_eq_dividend) - also have \nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\ - by (simp add: nat_less_iff take_bit_int_less_exp) - finally show \(nat \ take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = - (nat \ take_bit LENGTH('a)) k mod (nat \ take_bit LENGTH('a)) l\ - by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff) -qed - -lemma uint_div_distrib: - \uint (v div w) = uint v div uint w\ -proof - - have \int (unat (v div w)) = int (unat v div unat w)\ - by (simp add: unat_div_distrib) - then show ?thesis - by (simp add: of_nat_div) -qed - -lemma uint_mod_distrib: - \uint (v mod w) = uint v mod uint w\ -proof - - have \int (unat (v mod w)) = int (unat v mod unat w)\ - by (simp add: unat_mod_distrib) - then show ?thesis - by (simp add: of_nat_mod) -qed - -lemma of_int_sint [simp]: - \of_int (sint a) = signed a\ - by transfer (simp_all add: take_bit_signed_take_bit) - -lemma sint_greater_eq: - \- (2 ^ (LENGTH('a) - Suc 0)) \ sint w\ for w :: \'a::len word\ -proof (cases \bit w (LENGTH('a) - Suc 0)\) - case True - then show ?thesis - by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps) -next - have *: \- (2 ^ (LENGTH('a) - Suc 0)) \ (0::int)\ - by simp - case False - then show ?thesis - by transfer (auto simp add: signed_take_bit_eq intro: order_trans *) -qed - -lemma sint_less: - \sint w < 2 ^ (LENGTH('a) - Suc 0)\ for w :: \'a::len word\ - by (cases \bit w (LENGTH('a) - Suc 0)\; transfer) - (simp_all add: signed_take_bit_eq signed_take_bit_def take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper) - -context semiring_bit_shifts -begin - -lemma unsigned_ucast_eq: - \unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\ - for w :: \'b::len word\ - by (rule bit_eqI) (simp add: bit_unsigned_iff Conversions.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le) - -end - -context ring_bit_operations -begin - -lemma signed_ucast_eq: - \signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\ - for w :: \'b::len word\ -proof (rule bit_eqI) - fix n - assume \2 ^ n \ 0\ - then have \2 ^ (min (LENGTH('c) - Suc 0) n) \ 0\ - by (simp add: min_def) - (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero) - then show \bit (signed (ucast w :: 'c::len word)) n \ bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\ - by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) -qed - -lemma signed_scast_eq: - \signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\ - for w :: \'b::len word\ -proof (rule bit_eqI) - fix n - assume \2 ^ n \ 0\ - then have \2 ^ (min (LENGTH('c) - Suc 0) n) \ 0\ - by (simp add: min_def) - (metis (mono_tags) diff_diff_cancel local.exp_not_zero_imp_exp_diff_not_zero) - then show \bit (signed (scast w :: 'c::len word)) n \ bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\ - by (simp add: bit_signed_iff bit_unsigned_iff Conversions.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) -qed - -end - -end diff -r 5193570b739a -r a282abb07642 src/HOL/Word/More_Word.thy --- a/src/HOL/Word/More_Word.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/Word/More_Word.thy Thu Sep 17 09:57:31 2020 +0000 @@ -42,6 +42,11 @@ lemmas uint_mod_same = uint_idem lemmas of_nth_def = word_set_bits_def +lemmas of_nat_word_eq_iff = word_of_nat_eq_iff +lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff +lemmas of_int_word_eq_iff = word_of_int_eq_iff +lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff + lemma shiftl_transfer [transfer_rule]: includes lifting_syntax shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)" diff -r 5193570b739a -r a282abb07642 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/Word/Word.thy Thu Sep 17 09:57:31 2020 +0000 @@ -129,16 +129,29 @@ \(2 :: 'a::len word) ^ LENGTH('a) = 0\ by transfer simp +lemma exp_eq_zero_iff: + \2 ^ n = (0 :: 'a::len word) \ n \ LENGTH('a)\ + by transfer simp + subsubsection \Basic code generation setup\ -lift_definition uint :: \'a::len word \ int\ +context +begin + +qualified lift_definition the_int :: \'a::len word \ int\ is \take_bit LENGTH('a)\ . +end + lemma [code abstype]: - \Word.Word (uint w) = w\ + \Word.Word (Word.the_int w) = w\ by transfer simp +lemma Word_eq_word_of_int [code_post, simp]: + \Word.Word = of_int\ + by (rule; transfer) simp + quickcheck_generator word constructors: \0 :: 'a::len word\, @@ -157,71 +170,326 @@ end lemma [code]: - \HOL.equal v w \ HOL.equal (uint v) (uint w)\ + \HOL.equal v w \ HOL.equal (Word.the_int v) (Word.the_int w)\ by transfer (simp add: equal) lemma [code]: - \uint 0 = 0\ + \Word.the_int 0 = 0\ by transfer simp lemma [code]: - \uint 1 = 1\ + \Word.the_int 1 = 1\ by transfer simp lemma [code]: - \uint (v + w) = take_bit LENGTH('a) (uint v + uint w)\ + \Word.the_int (v + w) = take_bit LENGTH('a) (Word.the_int v + Word.the_int w)\ for v w :: \'a::len word\ by transfer (simp add: take_bit_add) lemma [code]: - \uint (- w) = (let k = uint w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\ + \Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\ for w :: \'a::len word\ by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if) lemma [code]: - \uint (v - w) = take_bit LENGTH('a) (uint v - uint w)\ + \Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)\ for v w :: \'a::len word\ by transfer (simp add: take_bit_diff) lemma [code]: - \uint (v * w) = take_bit LENGTH('a) (uint v * uint w)\ + \Word.the_int (v * w) = take_bit LENGTH('a) (Word.the_int v * Word.the_int w)\ for v w :: \'a::len word\ by transfer (simp add: take_bit_mult) subsubsection \Basic conversions\ -lift_definition word_of_int :: \int \ 'a::len word\ - is \\k. k\ . - -lift_definition unat :: \'a::len word \ nat\ - is \nat \ take_bit LENGTH('a)\ +abbreviation word_of_nat :: \nat \ 'a::len word\ + where \word_of_nat \ of_nat\ + +abbreviation word_of_int :: \int \ 'a::len word\ + where \word_of_int \ of_int\ + +lemma word_of_nat_eq_iff: + \word_of_nat m = (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ + by transfer (simp add: take_bit_of_nat) + +lemma word_of_int_eq_iff: + \word_of_int k = (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ + by transfer rule + +lemma word_of_nat_eq_0_iff [simp]: + \word_of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ + using word_of_nat_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) + +lemma word_of_int_eq_0_iff [simp]: + \word_of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ + using word_of_int_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) + +context semiring_1 +begin + +lift_definition unsigned :: \'b::len word \ 'a\ + is \of_nat \ nat \ take_bit LENGTH('b)\ by simp -lift_definition sint :: \'a::len word \ int\ - \ \treats the most-significant bit as a sign bit\ - is \signed_take_bit (LENGTH('a) - 1)\ - by (simp add: signed_take_bit_decr_length_iff) +lemma unsigned_0 [simp]: + \unsigned 0 = 0\ + by transfer simp + +lemma unsigned_1 [simp]: + \unsigned 1 = 1\ + by transfer simp + +lemma unsigned_numeral [simp]: + \unsigned (numeral n :: 'b::len word) = of_nat (take_bit LENGTH('b) (numeral n))\ + by transfer (simp add: nat_take_bit_eq) + +lemma unsigned_neg_numeral [simp]: + \unsigned (- numeral n :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) (- numeral n)))\ + by transfer simp + +end + +context semiring_1 +begin + +lemma unsigned_of_nat [simp]: + \unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)\ + by transfer (simp add: nat_eq_iff take_bit_of_nat) + +lemma unsigned_of_int [simp]: + \unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))\ + by transfer simp + +end + +context semiring_char_0 +begin + +lemma unsigned_word_eqI: + \v = w\ if \unsigned v = unsigned w\ + using that by transfer (simp add: eq_nat_nat_iff) + +lemma word_eq_iff_unsigned: + \v = w \ unsigned v = unsigned w\ + by (auto intro: unsigned_word_eqI) + +end + +context ring_1 +begin + +lift_definition signed :: \'b::len word \ 'a\ + is \of_int \ signed_take_bit (LENGTH('b) - Suc 0)\ + by (simp flip: signed_take_bit_decr_length_iff) + +lemma signed_0 [simp]: + \signed 0 = 0\ + by transfer simp + +lemma signed_1 [simp]: + \signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\ + by (transfer fixing: uminus; cases \LENGTH('b)\) + (simp_all add: sbintrunc_minus_simps) + +lemma signed_minus_1 [simp]: + \signed (- 1 :: 'b::len word) = - 1\ + by (transfer fixing: uminus) simp + +lemma signed_numeral [simp]: + \signed (numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (numeral n))\ + by transfer simp + +lemma signed_neg_numeral [simp]: + \signed (- numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (- numeral n))\ + by transfer simp + +lemma signed_of_nat [simp]: + \signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) (int n))\ + by transfer simp + +lemma signed_of_int [simp]: + \signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) n)\ + by transfer simp + +end + +context ring_char_0 +begin + +lemma signed_word_eqI: + \v = w\ if \signed v = signed w\ + using that by transfer (simp flip: signed_take_bit_decr_length_iff) + +lemma word_eq_iff_signed: + \v = w \ signed v = signed w\ + by (auto intro: signed_word_eqI) + +end + +abbreviation unat :: \'a::len word \ nat\ + where \unat \ unsigned\ + +abbreviation uint :: \'a::len word \ int\ + where \uint \ unsigned\ + +abbreviation sint :: \'a::len word \ int\ + where \sint \ signed\ + +abbreviation ucast :: \'a::len word \ 'b::len word\ + where \ucast \ unsigned\ + +abbreviation scast :: \'a::len word \ 'b::len word\ + where \scast \ signed\ + +context + includes lifting_syntax +begin + +lemma [transfer_rule]: + \(pcr_word ===> (=)) (nat \ take_bit LENGTH('a)) (unat :: 'a::len word \ nat)\ + using unsigned.transfer [where ?'a = nat] by simp + +lemma [transfer_rule]: + \(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \ int)\ + using unsigned.transfer [where ?'a = int] by (simp add: comp_def) + +lemma [transfer_rule]: + \(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \ int)\ + using signed.transfer [where ?'a = int] by simp + +lemma [transfer_rule]: + \(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \ 'b::len word)\ +proof (rule rel_funI) + fix k :: int and w :: \'a word\ + assume \pcr_word k w\ + then have \w = word_of_int k\ + by (simp add: pcr_word_def cr_word_def relcompp_apply) + moreover have \pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\ + by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) + ultimately show \pcr_word (take_bit LENGTH('a) k) (ucast w)\ + by simp +qed + +lemma [transfer_rule]: + \(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \ 'b::len word)\ +proof (rule rel_funI) + fix k :: int and w :: \'a word\ + assume \pcr_word k w\ + then have \w = word_of_int k\ + by (simp add: pcr_word_def cr_word_def relcompp_apply) + moreover have \pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\ + by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) + ultimately show \pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\ + by simp +qed + +end + +lemma of_nat_unat [simp]: + \of_nat (unat w) = unsigned w\ + by transfer simp + +lemma of_int_uint [simp]: + \of_int (uint w) = unsigned w\ + by transfer simp + +lemma of_int_sint [simp]: + \of_int (sint a) = signed a\ + by transfer (simp_all add: take_bit_signed_take_bit) lemma nat_uint_eq [simp]: \nat (uint w) = unat w\ by transfer simp -lemma of_nat_word_eq_iff: - \of_nat m = (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ +text \Aliasses only for code generation\ + +context +begin + +qualified lift_definition of_int :: \int \ 'a::len word\ + is \take_bit LENGTH('a)\ . + +qualified lift_definition of_nat :: \nat \ 'a::len word\ + is \int \ take_bit LENGTH('a)\ . + +qualified lift_definition the_nat :: \'a::len word \ nat\ + is \nat \ take_bit LENGTH('a)\ by simp + +qualified lift_definition the_signed_int :: \'a::len word \ int\ + is \signed_take_bit (LENGTH('a) - Suc 0)\ by (simp add: signed_take_bit_decr_length_iff) + +qualified lift_definition cast :: \'a::len word \ 'b::len word\ + is \take_bit LENGTH('a)\ by simp + +qualified lift_definition signed_cast :: \'a::len word \ 'b::len word\ + is \signed_take_bit (LENGTH('a) - Suc 0)\ by (metis signed_take_bit_decr_length_iff) + +end + +lemma [code_abbrev, simp]: + \Word.the_int = uint\ + by transfer rule + +lemma [code]: + \Word.the_int (Word.of_int k :: 'a::len word) = take_bit LENGTH('a) k\ + by transfer simp + +lemma [code_abbrev, simp]: + \Word.of_int = word_of_int\ + by (rule; transfer) simp + +lemma [code]: + \Word.the_int (Word.of_nat n :: 'a::len word) = take_bit LENGTH('a) (int n)\ by transfer (simp add: take_bit_of_nat) -lemma of_nat_word_eq_0_iff: - \of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ - using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) - -lemma of_int_word_eq_iff: - \of_int k = (of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ - by transfer rule - -lemma of_int_word_eq_0_iff: - \of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ - using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) +lemma [code_abbrev, simp]: + \Word.of_nat = word_of_nat\ + by (rule; transfer) (simp add: take_bit_of_nat) + +lemma [code]: + \Word.the_nat w = nat (Word.the_int w)\ + by transfer simp + +lemma [code_abbrev, simp]: + \Word.the_nat = unat\ + by (rule; transfer) simp + +lemma [code]: + \Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\ + for w :: \'a::len word\ + by transfer simp + +lemma [code_abbrev, simp]: + \Word.the_signed_int = sint\ + by (rule; transfer) simp + +lemma [code]: + \Word.the_int (Word.cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_int w)\ + for w :: \'a::len word\ + by transfer simp + +lemma [code_abbrev, simp]: + \Word.cast = ucast\ + by (rule; transfer) simp + +lemma [code]: + \Word.the_int (Word.signed_cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_signed_int w)\ + for w :: \'a::len word\ + by transfer simp + +lemma [code_abbrev, simp]: + \Word.signed_cast = scast\ + by (rule; transfer) simp + +lemma [code]: + \unsigned w = of_nat (nat (Word.the_int w))\ + by transfer simp + +lemma [code]: + \signed w = of_int (Word.the_signed_int w)\ + by transfer simp subsubsection \Basic ordering\ @@ -248,6 +516,22 @@ interpretation word_coorder: ordering_top \(\)\ \(>)\ \0 :: 'a::len word\ by (standard; transfer) simp +lemma word_of_nat_less_eq_iff: + \word_of_nat m \ (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ + by transfer (simp add: take_bit_of_nat) + +lemma word_of_int_less_eq_iff: + \word_of_int k \ (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ + by transfer rule + +lemma word_of_nat_less_iff: + \word_of_nat m < (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ + by transfer (simp add: take_bit_of_nat) + +lemma word_of_int_less_iff: + \word_of_int k < (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ + by transfer rule + lemma word_le_def [code]: "a \ b \ uint a \ uint b" by transfer rule @@ -331,16 +615,16 @@ lemma word_bit_induct [case_names zero even odd]: \P a\ if word_zero: \P 0\ - and word_even: \\a. P a \ 0 < a \ a < 2 ^ (LENGTH('a) - 1) \ P (2 * a)\ - and word_odd: \\a. P a \ a < 2 ^ (LENGTH('a) - 1) \ P (1 + 2 * a)\ + and word_even: \\a. P a \ 0 < a \ a < 2 ^ (LENGTH('a) - Suc 0) \ P (2 * a)\ + and word_odd: \\a. P a \ a < 2 ^ (LENGTH('a) - Suc 0) \ P (1 + 2 * a)\ for P and a :: \'a::len word\ proof - - define m :: nat where \m = LENGTH('a) - 1\ + define m :: nat where \m = LENGTH('a) - Suc 0\ then have l: \LENGTH('a) = Suc m\ by simp define n :: nat where \n = unat a\ then have \n < 2 ^ LENGTH('a)\ - by (unfold unat_def) (transfer, simp add: take_bit_eq_mod) + by transfer (simp add: take_bit_eq_mod) then have \n < 2 * 2 ^ m\ by (simp add: l) then have \P (of_nat n)\ @@ -355,8 +639,8 @@ with even.IH have \P (of_nat n)\ by simp moreover from \n < 2 ^ m\ even.hyps have \0 < (of_nat n :: 'a word)\ - by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) - moreover from \n < 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ + by (auto simp add: word_greater_zero_iff l) + moreover from \n < 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (simp add: l take_bit_eq_mod) ultimately have \P (2 * of_nat n)\ @@ -369,7 +653,7 @@ by simp with odd.IH have \P (of_nat n)\ by simp - moreover from \Suc n \ 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ + moreover from \Suc n \ 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (simp add: l take_bit_eq_mod) ultimately have \P (1 + 2 * of_nat n)\ @@ -556,6 +840,20 @@ end +lemma bit_word_eqI: + \a = b\ if \\n. n < LENGTH('a) \ bit a n \ bit b n\ + for a b :: \'a::len word\ + using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff) + +lemma bit_imp_le_length: + \n < LENGTH('a)\ if \bit w n\ + for w :: \'a::len word\ + using that by transfer simp + +lemma not_bit_length [simp]: + \\ bit w LENGTH('a)\ for w :: \'a::len word\ + by transfer simp + instantiation word :: (len) semiring_bit_shifts begin @@ -595,45 +893,426 @@ end -lemma bit_word_eqI: - \a = b\ if \\n. n < LENGTH('a) \ bit a n \ bit b n\ - for a b :: \'a::len word\ - using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff) - -lemma bit_imp_le_length: - \n < LENGTH('a)\ if \bit w n\ - for w :: \'a::len word\ - using that by transfer simp - -lemma not_bit_length [simp]: - \\ bit w LENGTH('a)\ for w :: \'a::len word\ +lemma [code]: + \Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\ + for w :: \'a::len word\ + by transfer (simp add: not_le not_less ac_simps min_absorb2) + + +instantiation word :: (len) ring_bit_operations +begin + +lift_definition not_word :: \'a word \ 'a word\ + is not + by (simp add: take_bit_not_iff) + +lift_definition and_word :: \'a word \ 'a word \ 'a word\ + is \and\ + by simp + +lift_definition or_word :: \'a word \ 'a word \ 'a word\ + is or + by simp + +lift_definition xor_word :: \'a word \ 'a word \ 'a word\ + is xor + by simp + +lift_definition mask_word :: \nat \ 'a word\ + 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 + +lemma [code_abbrev]: + \push_bit n 1 = (2 :: 'a::len word) ^ n\ + by (fact push_bit_of_1) + +lemma [code]: + \NOT w = Word.of_int (NOT (Word.the_int w))\ + for w :: \'a::len word\ + by transfer (simp add: take_bit_not_take_bit) + +lemma [code]: + \Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\ by transfer simp +lemma [code]: + \Word.the_int (v OR w) = Word.the_int v OR Word.the_int w\ + by transfer simp + +lemma [code]: + \Word.the_int (v XOR w) = Word.the_int v XOR Word.the_int w\ + by transfer simp + +lemma [code]: + \Word.the_int (mask n :: 'a::len word) = mask (min LENGTH('a) n)\ + by transfer simp + +context + includes lifting_syntax +begin + +lemma set_bit_word_transfer [transfer_rule]: + \((=) ===> pcr_word ===> pcr_word) set_bit set_bit\ + by (unfold set_bit_def) transfer_prover + +lemma unset_bit_word_transfer [transfer_rule]: + \((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\ + by (unfold unset_bit_def) transfer_prover + +lemma flip_bit_word_transfer [transfer_rule]: + \((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\ + by (unfold flip_bit_def) transfer_prover + +lemma signed_take_bit_word_transfer [transfer_rule]: + \((=) ===> pcr_word ===> pcr_word) + (\n k. signed_take_bit n (take_bit LENGTH('a::len) k)) + (signed_take_bit :: nat \ 'a word \ 'a word)\ +proof - + let ?K = \\n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \ bit k n) * NOT (mask n)\ + let ?W = \\n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\ + have \((=) ===> pcr_word ===> pcr_word) ?K ?W\ + by transfer_prover + also have \?K = (\n k. signed_take_bit n (take_bit LENGTH('a::len) k))\ + by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps) + also have \?W = signed_take_bit\ + by (simp add: fun_eq_iff signed_take_bit_def) + finally show ?thesis . +qed + +end + subsection \Conversions including casts\ +subsubsection \Generic unsigned conversion\ + +context semiring_bits +begin + +lemma bit_unsigned_iff: + \bit (unsigned w) n \ 2 ^ n \ 0 \ bit w n\ + for w :: \'b::len word\ + by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff) + +end + +context semiring_bit_shifts +begin + +lemma unsigned_push_bit_eq: + \unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\ + for w :: \'b::len word\ +proof (rule bit_eqI) + fix m + assume \2 ^ m \ 0\ + show \bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\ + proof (cases \n \ m\) + case True + with \2 ^ m \ 0\ have \2 ^ (m - n) \ 0\ + by (metis (full_types) diff_add exp_add_not_zero_imp) + with True show ?thesis + by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff not_le exp_eq_zero_iff ac_simps) + next + case False + then show ?thesis + by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff) + qed +qed + +lemma unsigned_take_bit_eq: + \unsigned (take_bit n w) = take_bit n (unsigned w)\ + for w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff) + +end + +context semiring_bit_operations +begin + +lemma unsigned_and_eq: + \unsigned (v AND w) = unsigned v AND unsigned w\ + for v w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff) + +lemma unsigned_or_eq: + \unsigned (v OR w) = unsigned v OR unsigned w\ + for v w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff) + +lemma unsigned_xor_eq: + \unsigned (v XOR w) = unsigned v XOR unsigned w\ + for v w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff) + +end + +context ring_bit_operations +begin + +lemma unsigned_not_eq: + \unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\ + for w :: \'b::len word\ + by (rule bit_eqI) + (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le) + +end + +context unique_euclidean_semiring_numeral +begin + +lemma unsigned_greater_eq: + \0 \ unsigned w\ for w :: \'b::len word\ + by (transfer fixing: less_eq) simp + +lemma unsigned_less: + \unsigned w < 2 ^ LENGTH('b)\ for w :: \'b::len word\ + by (transfer fixing: less) simp + +end + +context linordered_semidom +begin + +lemma word_less_eq_iff_unsigned: + "a \ b \ unsigned a \ unsigned b" + by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) + +lemma word_less_iff_unsigned: + "a < b \ unsigned a < unsigned b" + by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) + +end + + +subsubsection \Generic signed conversion\ + +context ring_bit_operations +begin + +lemma bit_signed_iff: + \bit (signed w) n \ 2 ^ n \ 0 \ bit w (min (LENGTH('b) - Suc 0) n)\ + for w :: \'b::len word\ + by (transfer fixing: bit) + (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def) + +lemma signed_push_bit_eq: + \signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\ + for w :: \'b::len word\ +proof (rule bit_eqI) + fix m + assume \2 ^ m \ 0\ + define q where \q = LENGTH('b) - Suc 0\ + then have *: \LENGTH('b) = Suc q\ + by simp + show \bit (signed (push_bit n w)) m \ + bit (signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))) m\ + proof (cases \q \ m\) + case True + moreover define r where \r = m - q\ + ultimately have \m = q + r\ + by simp + moreover from \m = q + r\ \2 ^ m \ 0\ have \2 ^ q \ 0\ \2 ^ r \ 0\ + using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r] + by simp_all + moreover from \2 ^ q \ 0\ have \2 ^ (q - n) \ 0\ + by (rule exp_not_zero_imp_exp_diff_not_zero) + ultimately show ?thesis + by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff + min_def * exp_eq_zero_iff le_diff_conv2) + next + case False + then show ?thesis + using exp_not_zero_imp_exp_diff_not_zero [of m n] + by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff + min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit + exp_eq_zero_iff) + qed +qed + +lemma signed_take_bit_eq: + \signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\ + for w :: \'b::len word\ + by (transfer fixing: take_bit; cases \LENGTH('b)\) + (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq) + +lemma signed_not_eq: + \signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\ + for w :: \'b::len word\ +proof (rule bit_eqI) + fix n + assume \2 ^ n \ 0\ + define q where \q = LENGTH('b) - Suc 0\ + then have *: \LENGTH('b) = Suc q\ + by simp + show \bit (signed (NOT w)) n \ + bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\ + proof (cases \q < n\) + case True + moreover define r where \r = n - Suc q\ + ultimately have \n = r + Suc q\ + by simp + moreover from \2 ^ n \ 0\ \n = r + Suc q\ + have \2 ^ Suc q \ 0\ + using exp_add_not_zero_imp_right by blast + ultimately show ?thesis + by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def + exp_eq_zero_iff) + next + case False + then show ?thesis + by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def + exp_eq_zero_iff) + qed +qed + +lemma signed_and_eq: + \signed (v AND w) = signed v AND signed w\ + for v w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff) + +lemma signed_or_eq: + \signed (v OR w) = signed v OR signed w\ + for v w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff) + +lemma signed_xor_eq: + \signed (v XOR w) = signed v XOR signed w\ + for v w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff) + +end + + +subsubsection \More\ + +lemma sint_greater_eq: + \- (2 ^ (LENGTH('a) - Suc 0)) \ sint w\ for w :: \'a::len word\ +proof (cases \bit w (LENGTH('a) - Suc 0)\) + case True + then show ?thesis + by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps) +next + have *: \- (2 ^ (LENGTH('a) - Suc 0)) \ (0::int)\ + by simp + case False + then show ?thesis + by transfer (auto simp add: signed_take_bit_eq intro: order_trans *) +qed + +lemma sint_less: + \sint w < 2 ^ (LENGTH('a) - Suc 0)\ for w :: \'a::len word\ + by (cases \bit w (LENGTH('a) - Suc 0)\; transfer) + (simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper) + +lemma unat_div_distrib: + \unat (v div w) = unat v div unat w\ +proof transfer + fix k l + have \nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \ nat (take_bit LENGTH('a) k)\ + by (rule div_le_dividend) + also have \nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\ + by (simp add: nat_less_iff) + finally show \(nat \ take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) = + (nat \ take_bit LENGTH('a)) k div (nat \ take_bit LENGTH('a)) l\ + by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff) +qed + +lemma unat_mod_distrib: + \unat (v mod w) = unat v mod unat w\ +proof transfer + fix k l + have \nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \ nat (take_bit LENGTH('a) k)\ + by (rule mod_less_eq_dividend) + also have \nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\ + by (simp add: nat_less_iff) + finally show \(nat \ take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = + (nat \ take_bit LENGTH('a)) k mod (nat \ take_bit LENGTH('a)) l\ + by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff) +qed + +lemma uint_div_distrib: + \uint (v div w) = uint v div uint w\ +proof - + have \int (unat (v div w)) = int (unat v div unat w)\ + by (simp add: unat_div_distrib) + then show ?thesis + by (simp add: of_nat_div) +qed + +lemma uint_mod_distrib: + \uint (v mod w) = uint v mod uint w\ +proof - + have \int (unat (v mod w)) = int (unat v mod unat w)\ + by (simp add: unat_mod_distrib) + then show ?thesis + by (simp add: of_nat_mod) +qed + +context semiring_bit_shifts +begin + +lemma unsigned_ucast_eq: + \unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\ + for w :: \'b::len word\ + by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le) + +end + +context ring_bit_operations +begin + +lemma signed_ucast_eq: + \signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\ + for w :: \'b::len word\ +proof (rule bit_eqI) + fix n + assume \2 ^ n \ 0\ + then have \2 ^ (min (LENGTH('c) - Suc 0) n) \ 0\ + by (simp add: min_def) + (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero) + then show \bit (signed (ucast w :: 'c::len word)) n \ bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\ + by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) +qed + +lemma signed_scast_eq: + \signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\ + for w :: \'b::len word\ +proof (rule bit_eqI) + fix n + assume \2 ^ n \ 0\ + then have \2 ^ (min (LENGTH('c) - Suc 0) n) \ 0\ + by (simp add: min_def) + (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero) + then show \bit (signed (scast w :: 'c::len word)) n \ bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\ + by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) +qed + +end + lemma uint_nonnegative: "0 \ uint w" - by transfer simp + by (fact unsigned_greater_eq) lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" for w :: "'a::len word" - by transfer (simp add: take_bit_eq_mod) + by (fact unsigned_less) lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" for w :: "'a::len word" - using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial) + by transfer (simp add: take_bit_eq_mod) lemma word_uint_eqI: "uint a = uint b \ a = b" - by transfer simp + by (fact unsigned_word_eqI) lemma word_uint_eq_iff: "a = b \ uint a = uint b" - using word_uint_eqI by auto - -lemma Word_eq_word_of_int [code_post]: - \Word.Word = word_of_int\ - by rule (transfer, rule) - -lemma uint_word_of_int_eq [code]: + by (fact word_eq_iff_unsigned) + +lemma uint_word_of_int_eq: \uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\ by transfer rule @@ -656,80 +1335,73 @@ fix x :: "'a word" assume "\x. PROP P (word_of_int x)" then have "PROP P (word_of_int (uint x))" . - then show "PROP P x" by (simp add: word_of_int_uint) + then show "PROP P x" + by (simp only: word_of_int_uint) qed -lemma sint_uint [code]: - \sint w = signed_take_bit (LENGTH('a) - 1) (uint w)\ +lemma sint_uint: + \sint w = signed_take_bit (LENGTH('a) - Suc 0) (uint w)\ for w :: \'a::len word\ by (cases \LENGTH('a)\; transfer) (simp_all add: signed_take_bit_take_bit) -lemma unat_eq_nat_uint [code]: +lemma unat_eq_nat_uint: \unat w = nat (uint w)\ by simp -lift_definition ucast :: \'a::len word \ 'b::len word\ - is \take_bit LENGTH('a)\ - by simp - -lemma ucast_eq [code]: +lemma ucast_eq: \ucast w = word_of_int (uint w)\ by transfer simp -lift_definition scast :: \'a::len word \ 'b::len word\ - is \signed_take_bit (LENGTH('a) - 1)\ - by (simp flip: signed_take_bit_decr_length_iff) - -lemma scast_eq [code]: +lemma scast_eq: \scast w = word_of_int (sint w)\ by transfer simp -lemma uint_0_eq [simp]: +lemma uint_0_eq: \uint 0 = 0\ - by transfer simp - -lemma uint_1_eq [simp]: + by (fact unsigned_0) + +lemma uint_1_eq: \uint 1 = 1\ - by transfer simp + by (fact unsigned_1) lemma word_m1_wi: "- 1 = word_of_int (- 1)" - by transfer rule + by simp lemma uint_0_iff: "uint x = 0 \ x = 0" - by (simp add: word_uint_eq_iff) + by (auto simp add: unsigned_word_eqI) lemma unat_0_iff: "unat x = 0 \ x = 0" - by transfer (auto intro: antisym) - -lemma unat_0 [simp]: "unat 0 = 0" - by transfer simp + by (auto simp add: unsigned_word_eqI) + +lemma unat_0: "unat 0 = 0" + by (fact unsigned_0) lemma unat_gt_0: "0 < unat x \ x \ 0" by (auto simp: unat_0_iff [symmetric]) -lemma ucast_0 [simp]: "ucast 0 = 0" - by transfer simp - -lemma sint_0 [simp]: "sint 0 = 0" - by (simp add: sint_uint) - -lemma scast_0 [simp]: "scast 0 = 0" - by transfer simp - -lemma sint_n1 [simp] : "sint (- 1) = - 1" - by transfer simp - -lemma scast_n1 [simp]: "scast (- 1) = - 1" - by transfer simp +lemma ucast_0: "ucast 0 = 0" + by (fact unsigned_0) + +lemma sint_0: "sint 0 = 0" + by (fact signed_0) + +lemma scast_0: "scast 0 = 0" + by (fact signed_0) + +lemma sint_n1: "sint (- 1) = - 1" + by (fact signed_minus_1) + +lemma scast_n1: "scast (- 1) = - 1" + by (fact signed_minus_1) lemma uint_1: "uint (1::'a::len word) = 1" by (fact uint_1_eq) -lemma unat_1 [simp]: "unat (1::'a::len word) = 1" - by transfer simp - -lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" - by transfer simp +lemma unat_1: "unat (1::'a::len word) = 1" + by (fact unsigned_1) + +lemma ucast_1: "ucast (1::'a::len word) = 1" + by (fact unsigned_1) instantiation word :: (len) size begin @@ -851,26 +1523,6 @@ lemmas word_of_int_hom_syms = word_of_int_homs [symmetric] -lemma word_of_nat: "of_nat n = word_of_int (int n)" - by (induct n) (auto simp add : word_of_int_hom_syms) - -lemma word_of_int: "of_int = word_of_int" - apply (rule ext) - apply (case_tac x rule: int_diff_cases) - apply (simp add: word_of_nat wi_hom_sub) - done - -lemma word_of_int_eq: - "word_of_int = of_int" - by (rule ext) (transfer, rule) - -definition udvd :: "'a::len word \ 'a::len word \ bool" (infixl "udvd" 50) - where "a udvd b = (\n\0. uint b = n * uint a)" - -lemma exp_eq_zero_iff: - \2 ^ n = (0 :: 'a::len word) \ n \ LENGTH('a)\ - by transfer simp - lemma double_eq_zero_iff: \2 * a = 0 \ a = 0 \ a = 2 ^ (LENGTH('a) - Suc 0)\ for a :: \'a::len word\ @@ -978,8 +1630,7 @@ subsection \Bit-wise operations\ - -lemma uint_take_bit_eq [code]: +lemma uint_take_bit_eq: \uint (take_bit n w) = take_bit n (uint w)\ by transfer (simp add: ac_simps) @@ -1049,69 +1700,6 @@ \shiftr1 w = word_of_int (uint w div 2)\ by transfer simp -instantiation word :: (len) ring_bit_operations -begin - -lift_definition not_word :: \'a word \ 'a word\ - is not - by (simp add: take_bit_not_iff) - -lift_definition and_word :: \'a word \ 'a word \ 'a word\ - is \and\ - by simp - -lift_definition or_word :: \'a word \ 'a word \ 'a word\ - is or - by simp - -lift_definition xor_word :: \'a word \ 'a word \ 'a word\ - is xor - by simp - -lift_definition mask_word :: \nat \ 'a word\ - 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 - -context - includes lifting_syntax -begin - -lemma set_bit_word_transfer [transfer_rule]: - \((=) ===> pcr_word ===> pcr_word) set_bit set_bit\ - by (unfold set_bit_def) transfer_prover - -lemma unset_bit_word_transfer [transfer_rule]: - \((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\ - by (unfold unset_bit_def) transfer_prover - -lemma flip_bit_word_transfer [transfer_rule]: - \((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\ - by (unfold flip_bit_def) transfer_prover - -lemma signed_take_bit_word_transfer [transfer_rule]: - \((=) ===> pcr_word ===> pcr_word) - (\n k. signed_take_bit n (take_bit LENGTH('a::len) k)) - (signed_take_bit :: nat \ 'a word \ 'a word)\ -proof - - let ?K = \\n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \ bit k n) * NOT (mask n)\ - let ?W = \\n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\ - have \((=) ===> pcr_word ===> pcr_word) ?K ?W\ - by transfer_prover - also have \?K = (\n k. signed_take_bit n (take_bit LENGTH('a::len) k))\ - by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps) - also have \?W = signed_take_bit\ - by (simp add: fun_eq_iff signed_take_bit_def) - finally show ?thesis . -qed - -end - instantiation word :: (len) semiring_bit_syntax begin @@ -1188,11 +1776,14 @@ \shiftl1 w = w << 1\ by transfer (simp add: push_bit_eq_mult ac_simps) -lemma uint_shiftr_eq [code]: +lemma uint_shiftr_eq: \uint (w >> n) = uint w div 2 ^ n\ - for w :: \'a::len word\ by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv) +lemma [code]: + \Word.the_int (w >> n) = drop_bit n (Word.the_int w)\ + by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv) + lemma shiftr1_code [code]: \shiftr1 w = w >> 1\ by transfer (simp add: drop_bit_Suc) @@ -1232,47 +1823,22 @@ \push_bit n w = w << n\ for w :: \'a::len word\ by (simp add: shiftl_word_eq) +lemma [code]: + \drop_bit n w = w >> n\ for w :: \'a::len word\ + by (simp add: shiftr_word_eq) + lemma bit_shiftr_word_iff: \bit (w >> m) n \ bit w (m + n)\ for w :: \'a::len word\ by (simp add: shiftr_word_eq bit_drop_bit_eq) -lemma [code]: - \drop_bit n w = w >> n\ for w :: \'a::len word\ - by (simp add: shiftr_word_eq) - -lemma [code]: - \uint (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (uint w) else uint w)\ - for w :: \'a::len word\ - by transfer (simp add: min_def) - -lemma [code]: - \uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)\ - by transfer simp - -lemma [code_abbrev]: - \push_bit n 1 = (2 :: 'a::len word) ^ n\ - by (fact push_bit_of_1) - lemma - word_not_def [code]: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" + word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" by (transfer, simp add: take_bit_not_take_bit)+ -lemma [code abstract]: - \uint (v AND w) = uint v AND uint w\ - by transfer simp - -lemma [code abstract]: - \uint (v OR w) = uint v OR uint w\ - by transfer simp - -lemma [code abstract]: - \uint (v XOR w) = uint v XOR uint w\ - by transfer simp - lift_definition setBit :: \'a::len word \ nat \ 'a word\ is \\k n. set_bit n k\ by (simp add: take_bit_set_bit_eq) @@ -1327,6 +1893,45 @@ by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp qed +lemma + take_bit_word_Bit0_eq [simp]: \take_bit (numeral n) (numeral (num.Bit0 m) :: 'a::len word) + = 2 * take_bit (pred_numeral n) (numeral m)\ (is ?P) + and take_bit_word_Bit1_eq [simp]: \take_bit (numeral n) (numeral (num.Bit1 m) :: 'a::len word) + = 1 + 2 * take_bit (pred_numeral n) (numeral m)\ (is ?Q) + and take_bit_word_minus_Bit0_eq [simp]: \take_bit (numeral n) (- numeral (num.Bit0 m) :: 'a::len word) + = 2 * take_bit (pred_numeral n) (- numeral m)\ (is ?R) + and take_bit_word_minus_Bit1_eq [simp]: \take_bit (numeral n) (- numeral (num.Bit1 m) :: 'a::len word) + = 1 + 2 * take_bit (pred_numeral n) (- numeral (Num.inc m))\ (is ?S) +proof - + define w :: \'a::len word\ + where \w = numeral m\ + moreover define q :: nat + where \q = pred_numeral n\ + ultimately have num: + \numeral m = w\ + \numeral (num.Bit0 m) = 2 * w\ + \numeral (num.Bit1 m) = 1 + 2 * w\ + \numeral (Num.inc m) = 1 + w\ + \pred_numeral n = q\ + \numeral n = Suc q\ + by (simp_all only: w_def q_def numeral_Bit0 [of m] numeral_Bit1 [of m] ac_simps + numeral_inc numeral_eq_Suc flip: mult_2) + have even: \take_bit (Suc q) (2 * w) = 2 * take_bit q w\ for w :: \'a::len word\ + by (rule bit_word_eqI) + (auto simp add: bit_take_bit_iff bit_double_iff) + have odd: \take_bit (Suc q) (1 + 2 * w) = 1 + 2 * take_bit q w\ for w :: \'a::len word\ + by (rule bit_eqI) + (auto simp add: bit_take_bit_iff bit_double_iff even_bit_succ_iff) + show ?P + using even [of w] by (simp add: num) + show ?Q + using odd [of w] by (simp add: num) + show ?R + using even [of \- w\] by (simp add: num) + show ?S + using odd [of \- (1 + w)\] by (simp add: num) +qed + subsection \Type-definition locale instantiations\ @@ -1396,7 +2001,7 @@ "n = LENGTH('a::len) \ td_ext (unat :: 'a word \ nat) of_nat (unats n) (\i. i mod 2 ^ n)" apply (standard; transfer) - apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_nat_eq_self_iff + apply (simp_all add: unats_def take_bit_of_nat take_bit_nat_eq_self_iff flip: take_bit_eq_mod) done @@ -1424,16 +2029,7 @@ lemma td_ext_sbin: "td_ext (sint :: 'a word \ int) word_of_int (sints (LENGTH('a::len))) (signed_take_bit (LENGTH('a) - 1))" - apply (unfold td_ext_def' sint_uint) - apply (simp add : word_ubin.eq_norm) - apply (cases "LENGTH('a)") - apply (auto simp add : sints_def) - apply (rule sym [THEN trans]) - apply (rule word_ubin.Abs_norm) - apply (simp only: bintrunc_sbintrunc) - apply (drule sym) - apply simp - done + by (standard; transfer) (auto simp add: sints_def) lemma td_ext_sint: "td_ext (sint :: 'a word \ int) word_of_int (sints (LENGTH('a::len))) @@ -1512,11 +2108,16 @@ \mask n = (1 << n) - (1 :: 'a::len word)\ by transfer (simp add: mask_eq_exp_minus_1 push_bit_of_1) -lemma uint_sshiftr_eq [code]: +lemma uint_sshiftr_eq: \uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\ for w :: \'a::len word\ by transfer (simp flip: drop_bit_eq_div) +lemma [code]: + \Word.the_int (w >>> n) = take_bit LENGTH('a) (drop_bit n (Word.the_signed_int w))\ + for w :: \'a::len word\ + by transfer simp + lemma sshift1_code [code]: \sshiftr1 w = w >>> 1\ by transfer (simp add: drop_bit_Suc) @@ -1653,7 +2254,7 @@ by simp qed -lemma uint_word_rotr_eq [code]: +lemma uint_word_rotr_eq: \uint (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (uint w)) (uint (take_bit (n mod LENGTH('a)) w))\ @@ -1663,6 +2264,13 @@ using mod_less_divisor not_less apply blast done +lemma [code]: + \Word.the_int (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) + (drop_bit (n mod LENGTH('a)) (Word.the_int w)) + (Word.the_int (take_bit (n mod LENGTH('a)) w))\ + for w :: \'a::len word\ + using uint_word_rotr_eq [of n w] by simp + subsection \Split and cat operations\ @@ -1895,33 +2503,7 @@ lemma word_eq_iff: "x = y \ (\n?P \ ?Q\) for x y :: "'a::len word" -proof - assume ?P - then show ?Q - by simp -next - assume ?Q - then have *: \bit (uint x) n \ bit (uint y) n\ if \n < LENGTH('a)\ for n - using that by (simp add: word_test_bit_def) - show ?P - proof (rule word_uint_eqI, rule bit_eqI, rule iffI) - fix n - assume \bit (uint x) n\ - then have \n < LENGTH('a)\ - by (simp add: bit_take_bit_iff uint.rep_eq) - with * \bit (uint x) n\ - show \bit (uint y) n\ - by simp - next - fix n - assume \bit (uint y) n\ - then have \n < LENGTH('a)\ - by (simp add: bit_take_bit_iff uint.rep_eq) - with * \bit (uint y) n\ - show \bit (uint x) n\ - by simp - qed -qed + by transfer (auto simp add: bit_eq_iff bit_take_bit_iff) lemma word_eqI: "(\n. n < size u \ u !! n = v !! n) \ u = v" for u :: "'a::len word" @@ -2139,9 +2721,6 @@ subsection \Word Arithmetic\ -lemma udvdI: "0 \ n \ uint b = n * uint a \ a udvd b" - by (auto simp: udvd_def) - lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b @@ -2182,9 +2761,7 @@ and "uint (word_pred a) = (uint a - 1) mod 2 ^ LENGTH('a)" and "uint (0 :: 'a word) = 0 mod 2 ^ LENGTH('a)" and "uint (1 :: 'a word) = 1 mod 2 ^ LENGTH('a)" - apply (simp_all only: word_arith_wis) - apply (simp_all add: word_uint.eq_norm) - done + by (simp_all only: word_arith_wis uint_word_of_int_eq flip: take_bit_eq_mod) lemma uint_word_arith_bintrs: fixes a b :: "'a::len word" @@ -2238,23 +2815,89 @@ subsection \Order on fixed-length words\ -lemma udvd_nat_alt: "a udvd b \ (\n\0. unat b = n * unat a)" - supply nat_uint_eq [simp del] - apply (unfold udvd_def) - apply safe - apply (simp add: unat_eq_nat_uint nat_mult_distrib) - apply (simp add: uint_nat) - apply (rule exI) - apply safe - prefer 2 - apply (erule notE) - apply (rule refl) - apply force +lift_definition udvd :: \'a::len word \ 'a::len word \ bool\ (infixl \udvd\ 50) + is \\k l. take_bit LENGTH('a) k dvd take_bit LENGTH('a) l\ by simp + +lemma udvd_iff_dvd: + \x udvd y \ unat x dvd unat y\ + by transfer (simp add: nat_dvd_iff) + +lemma udvd_iff_dvd_int: + \v udvd w \ uint v dvd uint w\ + by transfer rule + +lemma udvdI [intro]: + \v udvd w\ if \unat w = unat v * unat u\ +proof - + from that have \unat v dvd unat w\ .. + then show ?thesis + by (simp add: udvd_iff_dvd) +qed + +lemma udvdE [elim]: + fixes v w :: \'a::len word\ + assumes \v udvd w\ + obtains u :: \'a word\ where \unat w = unat v * unat u\ +proof (cases \v = 0\) + case True + moreover from True \v udvd w\ have \w = 0\ + by transfer simp + ultimately show thesis + using that by simp +next + case False + then have \unat v > 0\ + by (simp add: unat_gt_0) + from \v udvd w\ have \unat v dvd unat w\ + by (simp add: udvd_iff_dvd) + then obtain n where \unat w = unat v * n\ .. + moreover have \n < 2 ^ LENGTH('a)\ + proof (rule ccontr) + assume \\ n < 2 ^ LENGTH('a)\ + then have \n \ 2 ^ LENGTH('a)\ + by (simp add: not_le) + then have \unat v * n \ 2 ^ LENGTH('a)\ + using \unat v > 0\ mult_le_mono [of 1 \unat v\ \2 ^ LENGTH('a)\ n] + by simp + with \unat w = unat v * n\ unat_lt2p [of w] + show False + by simp + qed + ultimately have \unat w = unat v * unat (word_of_nat n :: 'a word)\ + by (auto simp add: take_bit_nat_eq_self_iff intro: sym) + with that show thesis . +qed + +lemma udvd_imp_mod_eq_0: + \w mod v = 0\ if \v udvd w\ + using that by transfer simp + +lemma mod_eq_0_imp_udvd [intro?]: + \v udvd w\ if \w mod v = 0\ +proof - + from that have \unat (w mod v) = unat 0\ + by simp + then have \unat w mod unat v = 0\ + by (simp add: unat_mod_distrib) + then have \unat v dvd unat w\ .. + then show ?thesis + by (simp add: udvd_iff_dvd) +qed + +lemma udvd_nat_alt: + \a udvd b \ (\n. unat b = n * unat a)\ + by (auto simp add: udvd_iff_dvd) + +lemma udvd_unfold_int: + \a udvd b \ (\n\0. uint b = n * uint a)\ + apply (auto elim!: dvdE simp add: udvd_iff_dvd) + apply (simp only: uint_nat) + apply auto + using of_nat_0_le_iff apply blast + apply (simp only: unat_eq_nat_uint) + apply (simp add: nat_mult_distrib) done -lemma udvd_iff_dvd: "x udvd y \ unat x dvd unat y" - unfolding dvd_def udvd_nat_alt by force - lemma unat_minus_one: \unat (w - 1) = unat w - 1\ if \w \ 0\ proof - @@ -2358,14 +3001,12 @@ lemma uint_split: "P (uint x) = (\i. word_of_int i = x \ 0 \ i \ i < 2^LENGTH('a) \ P i)" for x :: "'a::len word" - by transfer (auto simp add: take_bit_eq_mod take_bit_int_less_exp) + by transfer (auto simp add: take_bit_eq_mod) lemma uint_split_asm: "P (uint x) = (\i. word_of_int i = x \ 0 \ i \ i < 2^LENGTH('a) \ \ P i)" for x :: "'a::len word" - by (auto dest!: word_of_int_inverse - simp: int_word_uint - split: uint_split) + by auto (metis take_bit_int_eq_self_iff) lemmas uint_splits = uint_split uint_split_asm @@ -2569,7 +3210,7 @@ lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left] lemma udvd_minus_le': "xy < k \ z udvd xy \ z udvd k \ xy \ k - z" - apply (unfold udvd_def) + apply (unfold udvd_unfold_int) apply clarify apply (erule (2) udvd_decr0) done @@ -2578,7 +3219,7 @@ "p < a + s \ a \ a + s \ K udvd s \ K udvd p - a \ a \ p \ 0 < K \ p \ p + K \ p + K \ a + s" supply [[simproc del: linordered_ring_less_cancel_factor]] - apply (unfold udvd_def) + apply (unfold udvd_unfold_int) apply clarify apply (simp add: uint_arith_simps split: if_split_asm) prefer 2 @@ -2603,7 +3244,7 @@ word_zero_le [THEN leD, THEN antisym_conv1] lemma word_of_int_nat: "0 \ x \ word_of_int x = of_nat (nat x)" - by (simp add: word_of_int) + by simp text \ note that \iszero_def\ is only for class \comm_semiring_1_cancel\, @@ -2654,10 +3295,10 @@ by simp lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)" - by (simp add: word_of_nat wi_hom_mult) + by (simp add: wi_hom_mult) lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)" - by (simp add: word_of_nat wi_hom_succ ac_simps) + by transfer (simp add: ac_simps) lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0" by simp @@ -2679,10 +3320,10 @@ by (subst Abs_fnat_hom_Suc [symmetric]) simp lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)" - by (simp add: word_div_def word_of_nat zdiv_int uint_nat) - + by (metis of_int_of_nat_eq of_nat_unat of_nat_div word_div_def) + lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)" - by (simp add: word_mod_def word_of_nat zmod_int uint_nat) + by (metis of_int_of_nat_eq of_nat_mod of_nat_unat word_mod_def) lemmas word_arith_nat_defs = word_arith_nat_add word_arith_nat_mult @@ -2758,30 +3399,30 @@ lemma uint_div: \uint (x div y) = uint x div uint y\ - by (metis div_le_dividend le_less_trans mod_less uint_nat unat_lt2p unat_word_ariths(6) zdiv_int) + by (fact uint_div_distrib) lemma unat_div: \unat (x div y) = unat x div unat y\ - by (simp add: uint_div nat_div_distrib flip: nat_uint_eq) + by (fact unat_div_distrib) lemma uint_mod: \uint (x mod y) = uint x mod uint y\ - by (metis (no_types, lifting) le_less_trans mod_by_0 mod_le_divisor mod_less neq0_conv uint_nat unat_lt2p unat_word_ariths(7) zmod_int) + by (fact uint_mod_distrib) lemma unat_mod: \unat (x mod y) = unat x mod unat y\ - by (simp add: uint_mod nat_mod_distrib flip: nat_uint_eq) + by (fact unat_mod_distrib) text \Definition of \unat_arith\ tactic\ lemma unat_split: "P (unat x) \ (\n. of_nat n = x \ n < 2^LENGTH('a) \ P n)" for x :: "'a::len word" - by (auto simp: unat_of_nat) + by auto (metis take_bit_nat_eq_self_iff) lemma unat_split_asm: "P (unat x) \ (\n. of_nat n = x \ n < 2^LENGTH('a) \ \ P n)" for x :: "'a::len word" - by (auto simp: unat_of_nat) + by auto (metis take_bit_nat_eq_self_iff) lemmas of_nat_inverse = word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified] @@ -3236,29 +3877,14 @@ by transfer (simp add: bin_sc_eq) lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \ m = n \ m < LENGTH('a)" - by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin) + by transfer (auto simp add: bit_exp_iff) lemma nth_w2p: "((2::'a::len word) ^ n) !! m \ m = n \ m < LENGTH('a::len)" - by (simp add: test_bit_2p [symmetric] word_of_int [symmetric]) + by transfer (auto simp add: bit_exp_iff) lemma uint_2p: "(0::'a::len word) < 2 ^ n \ uint (2 ^ n::'a::len word) = 2 ^ n" - apply (unfold word_arith_power_alt) - apply (case_tac "LENGTH('a)") - apply clarsimp - apply (case_tac "nat") - apply clarsimp - apply (case_tac "n") - apply clarsimp - apply clarsimp - apply (drule word_gt_0 [THEN iffD1]) - apply (safe intro!: word_eqI) - apply (auto simp add: nth_2p_bin) - apply (erule notE) - apply (simp (no_asm_use) add: uint_word_of_int word_size) - apply (subst mod_pos_pos_trivial) - apply simp - apply (rule power_strict_increasing) - apply simp_all + apply (cases \n < LENGTH('a)\; transfer) + apply auto done lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n" @@ -3487,7 +4113,7 @@ lemma shiftr1_bintr [simp]: "(shiftr1 (numeral w) :: 'a::len word) = word_of_int (bin_rest (take_bit (LENGTH('a)) (numeral w)))" - unfolding shiftr1_eq word_numeral_alt by (simp add: word_ubin.eq_norm) + by transfer simp lemma sshiftr1_sbintr [simp]: "(sshiftr1 (numeral w) :: 'a::len word) = @@ -3624,26 +4250,14 @@ done lemma and_mask_dvd: "2 ^ n dvd uint w \ w AND mask n = 0" - apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p) - apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0) - apply (subst word_uint.norm_Rep [symmetric]) - apply (simp only: bintrunc_bintrunc_min take_bit_eq_mod [symmetric] min_def) - apply auto - done + by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 uint_0_iff) lemma and_mask_dvd_nat: "2 ^ n dvd unat w \ w AND mask n = 0" - apply (simp flip: and_mask_dvd) - apply transfer - using dvd_nat_abs_iff [of _ \take_bit LENGTH('a) k\ for k] - apply simp - done + by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 unat_0_iff uint_0_iff) lemma word_2p_lem: "n < size w \ w < 2 ^ n = (uint w < 2 ^ n)" for w :: "'a::len word" - apply (unfold word_size word_less_alt word_numeral_alt) - apply (auto simp add: word_of_int_power_hom word_uint.eq_norm - simp del: word_of_int_numeral) - done + by transfer simp lemma less_mask_eq: "x < 2 ^ n \ x AND mask n = x" for x :: "'a::len word" @@ -3680,12 +4294,40 @@ "word_succ (a AND mask n) AND mask n = word_succ a AND mask n" "word_pred (a AND mask n) AND mask n = word_pred a AND mask n" using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b] - by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff take_bit_eq_mod mod_simps) + apply (auto simp flip: take_bit_eq_mask) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + done lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n" for x :: \'a::len word\ using word_of_int_Ex [where x=x] - by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff take_bit_eq_mod mod_simps) + apply (auto simp flip: take_bit_eq_mask) + apply transfer + apply (simp add: take_bit_eq_mod mod_simps) + done lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)" by transfer (simp add: take_bit_minus_one_eq_mask) @@ -3912,7 +4554,7 @@ "(word_rsplit (numeral bin :: 'b::len word) :: 'a word list) = map word_of_int (bin_rsplit (LENGTH('a::len)) (LENGTH('b), take_bit (LENGTH('b)) (numeral bin)))" - by (simp add: word_rsplit_def word_ubin.eq_norm) + by (simp add: word_rsplit_def of_nat_take_bit) lemmas word_rsplit_no_cl [simp] = word_rsplit_no [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]] @@ -3943,7 +4585,7 @@ apply (unfold word_split_bin' test_bit_bin) apply (clarify) apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits) - apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq ac_simps bin_nth_uint_imp) + apply (auto simp add: bit_take_bit_iff bit_drop_bit_eq bit_unsigned_iff ac_simps exp_eq_zero_iff dest: bit_imp_le_length) done lemma test_bit_split: @@ -4392,7 +5034,10 @@ (if uint x + uint y < 2^size x then uint x + uint y else uint x + uint y - 2^size x)" - by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size) + apply (simp only: word_arith_wis word_size uint_word_of_int_eq) + apply (auto simp add: not_less take_bit_int_eq_self_iff) + apply (metis not_less uint_plus_if' word_add_def word_ubin.eq_norm) + done lemma unat_plus_if_size: "unat (x + y) = @@ -4408,7 +5053,7 @@ lemma word_neq_0_conv: "w \ 0 \ 0 < w" for w :: "'a::len word" - by (simp add: word_gt_0) + by (fact word_coorder.not_eq_extremum) lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c" for c :: "'a::len word" @@ -4419,7 +5064,10 @@ (if uint y \ uint x then uint x - uint y else uint x - uint y + 2^size x)" - by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size) + apply (simp only: word_arith_wis word_size uint_word_of_int_eq) + apply (auto simp add: take_bit_int_eq_self_iff not_le) + apply (metis not_le uint_sub_if' word_sub_wi word_ubin.eq_norm) + done lemma unat_sub: \unat (a - b) = unat a - unat b\ @@ -4483,38 +5131,57 @@ shows "(x - y) mod b = z' mod b'" using assms [symmetric] by (auto intro: mod_diff_cong) -lemma word_induct_less: "P 0 \ (\n. n < m \ P n \ P (1 + n)) \ P m" - for P :: "'a::len word \ bool" - apply (cases m) - apply atomize - apply (erule rev_mp)+ - apply (rule_tac x=m in spec) - apply (induct_tac n) - apply simp - apply clarsimp - apply (erule impE) - apply clarsimp - apply (erule_tac x=n in allE) - apply (erule impE) - apply (simp add: unat_arith_simps) - apply (clarsimp simp: unat_of_nat) - apply simp - apply (erule_tac x="of_nat na" in allE) - apply (erule impE) - apply (simp add: unat_arith_simps) - apply (clarsimp simp: unat_of_nat) - apply simp - done +lemma word_induct_less: + \P m\ if zero: \P 0\ and less: \\n. n < m \ P n \ P (1 + n)\ + for m :: \'a::len word\ +proof - + define q where \q = unat m\ + with less have \\n. n < word_of_nat q \ P n \ P (1 + n)\ + by simp + then have \P (word_of_nat q :: 'a word)\ + proof (induction q) + case 0 + show ?case + by (simp add: zero) + next + case (Suc q) + show ?case + proof (cases \1 + word_of_nat q = (0 :: 'a word)\) + case True + then show ?thesis + by (simp add: zero) + next + case False + then have *: \word_of_nat q < (word_of_nat (Suc q) :: 'a word)\ + by (simp add: unatSuc word_less_nat_alt) + then have **: \n < (1 + word_of_nat q :: 'a word) \ n \ (word_of_nat q :: 'a word)\ for n + by (metis (no_types, lifting) add.commute inc_le le_less_trans not_less of_nat_Suc) + have \P (word_of_nat q)\ + apply (rule Suc.IH) + apply (rule Suc.prems) + apply (erule less_trans) + apply (rule *) + apply assumption + done + with * have \P (1 + word_of_nat q)\ + by (rule Suc.prems) + then show ?thesis + by simp + qed + qed + with \q = unat m\ show ?thesis + by simp +qed lemma word_induct: "P 0 \ (\n. P n \ P (1 + n)) \ P m" for P :: "'a::len word \ bool" - by (erule word_induct_less) simp + by (rule word_induct_less) lemma word_induct2 [induct type]: "P 0 \ (\n. 1 + n \ 0 \ P n \ P (1 + n)) \ P n" for P :: "'b::len word \ bool" - apply (rule word_induct) - apply simp - apply (case_tac "1 + n = 0") + apply (rule word_induct_less) + apply simp_all + apply (case_tac "1 + na = 0") apply auto done diff -r 5193570b739a -r a282abb07642 src/HOL/ex/Bit_Lists.thy --- a/src/HOL/ex/Bit_Lists.thy Thu Sep 17 09:57:30 2020 +0000 +++ b/src/HOL/ex/Bit_Lists.thy Thu Sep 17 09:57:31 2020 +0000 @@ -5,7 +5,7 @@ theory Bit_Lists imports - "HOL-Word.Conversions" "HOL-Library.More_List" + "HOL-Word.Word" "HOL-Library.More_List" begin subsection \Fragments of algebraic bit representations\