# HG changeset patch # User haftmann # Date 1629576735 0 # Node ID afe3c8ae1624b50a8305b5c0e88f1ab683fa9fdf # Parent 304f22435bc7e7f710dcbfb36243a87ea57a04f5 consolidation of rules for bit operations diff -r 304f22435bc7 -r afe3c8ae1624 NEWS --- a/NEWS Fri Aug 20 17:57:57 2021 +0200 +++ b/NEWS Sat Aug 21 20:12:15 2021 +0000 @@ -206,6 +206,10 @@ in classes (semi)ring_bit_operations, class semiring_bit_shifts is gone. +* Expressions of the form "NOT (numeral _)" are not simplified by +default any longer. INCOMPATIBILITY, use not_one_eq and not_numeral_eq +as simp rule explicitly if needed. + * Abbreviation "max_word" has been moved to session Word_Lib in the AFP, as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1", "setBit", "clearBit". See there further the changelog in theory Guide. diff -r 304f22435bc7 -r afe3c8ae1624 src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Fri Aug 20 17:57:57 2021 +0200 +++ b/src/HOL/Bit_Operations.thy Sat Aug 21 20:12:15 2021 +0000 @@ -758,6 +758,10 @@ \a XOR 1 = a + of_bool (even a) - of_bool (odd a)\ using one_xor_eq [of a] by (simp add: ac_simps) +lemma xor_self_eq [simp]: + \a XOR a = 0\ + by (rule bit_eqI) (simp add: bit_simps) + lemma bit_iff_odd_drop_bit: \bit a n \ odd (drop_bit n a)\ by (simp add: bit_iff_odd drop_bit_eq_div) @@ -1319,7 +1323,7 @@ \bit (- 2) n \ 2 ^ n \ 0 \ n > 0\ by (simp add: bit_minus_iff bit_1_iff) -lemma not_one [simp]: +lemma not_one_eq: \NOT 1 = - 2\ by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff) @@ -1464,7 +1468,7 @@ \NOT k div 2 = NOT (k div 2)\ for k :: int by (cases k) (simp_all add: not_int_def divide_int_def nat_add_distrib) -lemma bit_not_int_iff [bit_simps]: +lemma bit_not_int_iff: \bit (NOT k) n \ \ bit k n\ for k :: int by (simp add: bit_not_int_iff' not_int_def) @@ -2057,6 +2061,11 @@ else \k mod 2 - l mod 2\ + 2 * ((k div 2) XOR (l div 2)))\ for k l :: int by (auto simp add: xor_int_rec [of k l] not_int_def elim!: oddE) +lemma bit_minus_int_iff: + \bit (- k) n \ bit (NOT (k - 1)) n\ + for k :: int + by (simp add: bit_simps) + subsection \Instance \<^typ>\nat\\ @@ -2215,7 +2224,7 @@ lemma [code]: \unset_bit 0 m = 2 * (m div 2)\ - \unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\ + \unset_bit (Suc n) m = m mod 2 + 2 * unset_bit n (m div 2)\ for m n :: nat by (simp_all add: unset_bit_Suc) @@ -2308,10 +2317,6 @@ \of_nat (drop_bit m n) = drop_bit m (of_nat n)\ by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div) -lemma bit_push_bit_iff_of_nat_iff [bit_simps]: - \bit (push_bit m (of_nat r)) n \ m \ n \ bit (of_nat r) (n - m)\ - by (auto simp add: bit_push_bit_iff) - lemma take_bit_sum: "take_bit n a = (\k = 0..Symbolic computations on numeral expressions\ + +context unique_euclidean_semiring_with_bit_operations +begin + +lemma bit_numeral_iff: + \bit (numeral m) n \ bit (numeral m :: nat) n\ + using bit_of_nat_iff_bit [of \numeral m\ n] by simp + +lemma bit_numeral_Bit0_Suc_iff [simp]: + \bit (numeral (Num.Bit0 m)) (Suc n) \ bit (numeral m) n\ + by (simp add: bit_Suc numeral_Bit0_div_2) + +lemma bit_numeral_Bit1_Suc_iff [simp]: + \bit (numeral (Num.Bit1 m)) (Suc n) \ bit (numeral m) n\ + by (simp add: bit_Suc numeral_Bit1_div_2) + +lemma bit_numeral_rec: + \bit (numeral (Num.Bit0 w)) n \ (case n of 0 \ False | Suc m \ bit (numeral w) m)\ + \bit (numeral (Num.Bit1 w)) n \ (case n of 0 \ True | Suc m \ bit (numeral w) m)\ + by (cases n; simp)+ + +lemma bit_numeral_simps [simp]: + \\ bit 1 (numeral n)\ + \bit (numeral (Num.Bit0 w)) (numeral n) \ bit (numeral w) (pred_numeral n)\ + \bit (numeral (Num.Bit1 w)) (numeral n) \ bit (numeral w) (pred_numeral n)\ + by (simp_all add: bit_1_iff numeral_eq_Suc) + +lemma and_numerals [simp]: + \1 AND numeral (Num.Bit0 y) = 0\ + \1 AND numeral (Num.Bit1 y) = 1\ + \numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = 2 * (numeral x AND numeral y)\ + \numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = 2 * (numeral x AND numeral y)\ + \numeral (Num.Bit0 x) AND 1 = 0\ + \numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = 2 * (numeral x AND numeral y)\ + \numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + 2 * (numeral x AND numeral y)\ + \numeral (Num.Bit1 x) AND 1 = 1\ + by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits) + +fun and_num :: \num \ num \ num option\ \<^marker>\contributor \Andreas Lochbihler\\ +where + \and_num num.One num.One = Some num.One\ +| \and_num num.One (num.Bit0 n) = None\ +| \and_num num.One (num.Bit1 n) = Some num.One\ +| \and_num (num.Bit0 m) num.One = None\ +| \and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\ +| \and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\ +| \and_num (num.Bit1 m) num.One = Some num.One\ +| \and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\ +| \and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \ Some num.One | Some n' \ Some (num.Bit1 n'))\ + +lemma numeral_and_num: + \numeral m AND numeral n = (case and_num m n of None \ 0 | Some n' \ numeral n')\ + by (induction m n rule: and_num.induct) (simp_all add: split: option.split) + +lemma and_num_eq_None_iff: + \and_num m n = None \ numeral m AND numeral n = 0\ + by (simp add: numeral_and_num split: option.split) + +lemma and_num_eq_Some_iff: + \and_num m n = Some q \ numeral m AND numeral n = numeral q\ + by (simp add: numeral_and_num split: option.split) + +lemma or_numerals [simp]: + \1 OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\ + \1 OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\ + \numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = 2 * (numeral x OR numeral y)\ + \numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + 2 * (numeral x OR numeral y)\ + \numeral (Num.Bit0 x) OR 1 = numeral (Num.Bit1 x)\ + \numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + 2 * (numeral x OR numeral y)\ + \numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + 2 * (numeral x OR numeral y)\ + \numeral (Num.Bit1 x) OR 1 = numeral (Num.Bit1 x)\ + by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits) + +fun or_num :: \num \ num \ num\ \<^marker>\contributor \Andreas Lochbihler\\ +where + \or_num num.One num.One = num.One\ +| \or_num num.One (num.Bit0 n) = num.Bit1 n\ +| \or_num num.One (num.Bit1 n) = num.Bit1 n\ +| \or_num (num.Bit0 m) num.One = num.Bit1 m\ +| \or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\ +| \or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\ +| \or_num (num.Bit1 m) num.One = num.Bit1 m\ +| \or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\ +| \or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\ + +lemma numeral_or_num: + \numeral m OR numeral n = numeral (or_num m n)\ + by (induction m n rule: or_num.induct) simp_all + +lemma numeral_or_num_eq: + \numeral (or_num m n) = numeral m OR numeral n\ + by (simp add: numeral_or_num) + +lemma xor_numerals [simp]: + \1 XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\ + \1 XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\ + \numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = 2 * (numeral x XOR numeral y)\ + \numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + 2 * (numeral x XOR numeral y)\ + \numeral (Num.Bit0 x) XOR 1 = numeral (Num.Bit1 x)\ + \numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + 2 * (numeral x XOR numeral y)\ + \numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = 2 * (numeral x XOR numeral y)\ + \numeral (Num.Bit1 x) XOR 1 = numeral (Num.Bit0 x)\ + by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits) + +fun xor_num :: \num \ num \ num option\ \<^marker>\contributor \Andreas Lochbihler\\ +where + \xor_num num.One num.One = None\ +| \xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\ +| \xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\ +| \xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\ +| \xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\ +| \xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \ num.One | Some n' \ num.Bit1 n')\ +| \xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\ +| \xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \ num.One | Some n' \ num.Bit1 n')\ +| \xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\ + +lemma numeral_xor_num: + \numeral m XOR numeral n = (case xor_num m n of None \ 0 | Some n' \ numeral n')\ + by (induction m n rule: xor_num.induct) (simp_all split: option.split) + +lemma xor_num_eq_None_iff: + \xor_num m n = None \ numeral m XOR numeral n = 0\ + by (simp add: numeral_xor_num split: option.split) + +lemma xor_num_eq_Some_iff: + \xor_num m n = Some q \ numeral m XOR numeral n = numeral q\ + by (simp add: numeral_xor_num split: option.split) + +end + +context ring_bit_operations +begin + +lemma minus_numeral_inc_eq: + \- numeral (Num.inc n) = NOT (numeral n)\ + by (simp add: not_eq_complement sub_inc_One_eq add_One) + +lemma sub_one_eq_not_neg: + \Num.sub n num.One = NOT (- numeral n)\ + by (simp add: not_eq_complement) + +lemma minus_numeral_eq_not_sub_one: + \- numeral n = NOT (Num.sub n num.One)\ + by (simp add: not_eq_complement) + +lemma not_numeral_eq: + \NOT (numeral n) = - numeral (Num.inc n)\ + by (simp add: minus_numeral_inc_eq) + +lemma not_minus_numeral_eq [simp]: + \NOT (- numeral n) = Num.sub n num.One\ + by (simp add: sub_one_eq_not_neg) + +lemma minus_not_numeral_eq [simp]: + \- (NOT (numeral n)) = numeral (Num.inc n)\ + by (simp add: not_numeral_eq) + +end + +lemma bit_minus_numeral_int [simp]: + \bit (- numeral (num.Bit0 w) :: int) (numeral n) \ bit (- numeral w :: int) (pred_numeral n)\ + \bit (- numeral (num.Bit1 w) :: int) (numeral n) \ \ bit (numeral w :: int) (pred_numeral n)\ + by (simp_all add: bit_minus_iff bit_not_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq) + +lemma and_not_numerals [simp]: + \1 AND NOT 1 = (0 :: int)\ + \1 AND NOT (numeral (Num.Bit0 n)) = (1 :: int)\ + \1 AND NOT (numeral (Num.Bit1 n)) = (0 :: int)\ + \numeral (Num.Bit0 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\ + \numeral (Num.Bit0 m) AND NOT (numeral (Num.Bit0 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\ + \numeral (Num.Bit0 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\ + \numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\ + \numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\ + \numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\ + by (simp_all add: bit_eq_iff) (auto simp add: bit_simps bit_Suc bit_numeral_rec BitM_inc_eq split: nat.splits) + +lemma and_not_not_numerals [simp]: + \NOT 1 AND NOT 1 = NOT (1 :: int)\ + \NOT 1 AND NOT (numeral n) = NOT (1 OR numeral n :: int)\ + \NOT (numeral m) AND NOT 1 = NOT (numeral m OR 1 :: int)\ + \NOT (numeral m) AND NOT (numeral n) = NOT (numeral m OR numeral n :: int)\ + by simp_all + +lemma and_minus_numerals [simp]: + \- 1 AND k = k\ + \k AND - 1 = k\ + \- numeral n AND k = NOT (neg_numeral_class.sub n num.One) AND k\ + \k AND - numeral n = k AND NOT (neg_numeral_class.sub n num.One)\ for k :: int + by (simp_all add: minus_numeral_eq_not_sub_one) + +fun and_not_num :: \num \ num \ num option\ \<^marker>\contributor \Andreas Lochbihler\\ +where + \and_not_num num.One num.One = None\ +| \and_not_num num.One (num.Bit0 n) = Some num.One\ +| \and_not_num num.One (num.Bit1 n) = None\ +| \and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\ +| \and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\ +| \and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\ +| \and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\ +| \and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \ Some num.One | Some n' \ Some (num.Bit1 n'))\ +| \and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\ + +lemma int_numeral_and_not_num: + \numeral m AND NOT (numeral n) = (case and_not_num m n of None \ 0 :: int | Some n' \ numeral n')\ + by (induction m n rule: and_not_num.induct) (simp_all split: option.split) + +lemma int_numeral_not_and_num: + \NOT (numeral m) AND numeral n = (case and_not_num n m of None \ 0 :: int | Some n' \ numeral n')\ + using int_numeral_and_not_num [of n m] by (simp add: ac_simps) + +lemma and_not_num_eq_None_iff: + \and_not_num m n = None \ numeral m AND NOT (numeral n) = (0 :: int)\ + by (simp add: int_numeral_and_not_num split: option.split) + +lemma and_not_num_eq_Some_iff: + \and_not_num m n = Some q \ numeral m AND NOT (numeral n) = (numeral q :: int)\ + by (simp add: int_numeral_and_not_num split: option.split) + +lemma or_not_numerals [simp]: + \1 OR NOT 1 = NOT (0 :: int)\ + \1 OR NOT (numeral (Num.Bit0 n)) = NOT (numeral (Num.Bit0 n) :: int)\ + \1 OR NOT (numeral (Num.Bit1 n)) = NOT (numeral (Num.Bit0 n) :: int)\ + \numeral (Num.Bit0 m) OR NOT (1 :: int) = NOT (1 :: int)\ + \numeral (Num.Bit0 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\ + \numeral (Num.Bit0 m) OR NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m OR NOT (numeral n))\ + \numeral (Num.Bit1 m) OR NOT (1 :: int) = NOT (0 :: int)\ + \numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\ + \numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit1 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\ + by (simp_all add: bit_eq_iff) (simp_all add: bit_simps bit_Suc bit_numeral_rec split: nat.splits) + +lemma or_and_numerals [simp]: + \NOT 1 OR 1 = NOT (0 :: int)\ + \NOT 1 OR numeral n = numeral n OR NOT (1 :: int)\ + \NOT (numeral m) OR 1 = 1 OR NOT (numeral m :: int)\ + \NOT (numeral m) OR (numeral n) = numeral n OR NOT (numeral m :: int)\ + by (simp_all add: ac_simps) + +lemma or_not_not_numerals [simp]: + \NOT 1 OR NOT 1 = NOT (1 :: int)\ + \NOT 1 OR NOT (numeral n) = NOT (1 AND numeral n :: int)\ + \NOT (numeral m) OR NOT 1 = NOT (numeral m AND 1 :: int)\ + \NOT (numeral m) OR NOT (numeral n) = NOT (numeral m AND numeral n :: int)\ + by simp_all + +lemma or_minus_numerals [simp]: + \- 1 OR k = - 1\ + \k OR - 1 = - 1\ + \- numeral n OR k = NOT (neg_numeral_class.sub n num.One) OR k\ + \k OR - numeral n = k OR NOT (neg_numeral_class.sub n num.One)\ for k :: int + by (simp_all add: minus_numeral_eq_not_sub_one) + +fun or_not_num_neg :: \num \ num \ num\ \<^marker>\contributor \Andreas Lochbihler\\ +where + \or_not_num_neg num.One num.One = num.One\ +| \or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\ +| \or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\ +| \or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\ +| \or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\ +| \or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\ +| \or_not_num_neg (num.Bit1 n) num.One = num.One\ +| \or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\ +| \or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\ + +lemma int_numeral_or_not_num_neg: + \numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\ + apply (induction m n rule: or_not_num_neg.induct) + apply simp_all + apply (simp_all add: not_one_eq not_numeral_eq) + done + +lemma int_numeral_not_or_num_neg: + \NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\ + using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps) + +lemma numeral_or_not_num_eq: + \numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\ + using int_numeral_or_not_num_neg [of m n] by simp + +lemma xor_minus_numerals [simp]: + \- 1 XOR k = NOT k\ + \k XOR - 1 = NOT k\ + \- numeral n XOR k = NOT (neg_numeral_class.sub n num.One XOR k)\ + \k XOR - numeral n = NOT (k XOR (neg_numeral_class.sub n num.One))\ for k :: int + by (simp_all add: minus_numeral_eq_not_sub_one) + + subsection \More properties\ lemma take_bit_eq_mask_iff: @@ -2425,6 +2717,10 @@ \of_int (NOT k) = NOT (of_int k)\ by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff) +lemma of_int_not_numeral: + \of_int (NOT (numeral k)) = NOT (numeral k)\ + by (simp add: local.of_int_not_eq) + lemma of_int_and_eq: \of_int (k AND l) = of_int k AND of_int l\ by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff) @@ -2547,157 +2843,6 @@ by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff dest: sym not_sym intro: less_trans [of k 0 \2 ^ n\]) -lemma minus_numeral_inc_eq: - \- numeral (Num.inc n) = NOT (numeral n :: int)\ - by (simp add: not_int_def sub_inc_One_eq add_One) - -lemma sub_one_eq_not_neg: - \Num.sub n num.One = NOT (- numeral n :: int)\ - by (simp add: not_int_def) - -lemma bit_numeral_int_iff [bit_simps]: - \bit (numeral m :: int) n \ bit (numeral m :: nat) n\ - using bit_of_nat_iff_bit [of \numeral m\ n] by simp - -lemma bit_minus_int_iff [bit_simps]: - \bit (- k) n \ \ bit (k - 1) n\ - for k :: int - using bit_not_int_iff' [of \k - 1\] by simp - -lemma bit_numeral_int_simps [simp]: - \bit (1 :: int) (numeral n) \ bit (0 :: int) (pred_numeral n)\ - \bit (numeral (num.Bit0 w) :: int) (numeral n) \ bit (numeral w :: int) (pred_numeral n)\ - \bit (numeral (num.Bit1 w) :: int) (numeral n) \ bit (numeral w :: int) (pred_numeral n)\ - \bit (numeral (Num.BitM w) :: int) (numeral n) \ \ bit (- numeral w :: int) (pred_numeral n)\ - \bit (- numeral (num.Bit0 w) :: int) (numeral n) \ bit (- numeral w :: int) (pred_numeral n)\ - \bit (- numeral (num.Bit1 w) :: int) (numeral n) \ \ bit (numeral w :: int) (pred_numeral n)\ - \bit (- numeral (Num.BitM w) :: int) (numeral n) \ bit (- (numeral w) :: int) (pred_numeral n)\ - by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff) - -lemma bit_numeral_Bit0_Suc_iff [simp]: - \bit (numeral (Num.Bit0 m) :: int) (Suc n) \ bit (numeral m :: int) n\ - by (simp add: bit_Suc) - -lemma bit_numeral_Bit1_Suc_iff [simp]: - \bit (numeral (Num.Bit1 m) :: int) (Suc n) \ bit (numeral m :: int) n\ - by (simp add: bit_Suc) - -lemma int_not_numerals [simp]: - \NOT (numeral (Num.Bit0 n) :: int) = - numeral (Num.Bit1 n)\ - \NOT (numeral (Num.Bit1 n) :: int) = - numeral (Num.inc (num.Bit1 n))\ - \NOT (numeral (Num.BitM n) :: int) = - numeral (num.Bit0 n)\ - \NOT (- numeral (Num.Bit0 n) :: int) = numeral (Num.BitM n)\ - \NOT (- numeral (Num.Bit1 n) :: int) = numeral (Num.Bit0 n)\ - by (simp_all add: not_int_def add_One inc_BitM_eq) - -text \FIXME: The rule sets below are very large (24 rules for each - operator). Is there a simpler way to do this?\ - -context -begin - -private lemma eqI: - \k = l\ - if num: \\n. bit k (numeral n) \ bit l (numeral n)\ - and even: \even k \ even l\ - for k l :: int -proof (rule bit_eqI) - fix n - show \bit k n \ bit l n\ - proof (cases n) - case 0 - with even show ?thesis - by simp - next - case (Suc n) - with num [of \num_of_nat (Suc n)\] show ?thesis - by (simp only: numeral_num_of_nat) - qed -qed - -lemma int_and_numerals [simp]: - \numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\ - \numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)\ - \numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)\ - \numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)\ - \numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\ - \numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))\ - \numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)\ - \numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))\ - \- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)\ - \- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)\ - \- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)\ - \- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)\ - \- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)\ - \- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))\ - \- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)\ - \- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))\ - \(1::int) AND numeral (Num.Bit0 y) = 0\ - \(1::int) AND numeral (Num.Bit1 y) = 1\ - \(1::int) AND - numeral (Num.Bit0 y) = 0\ - \(1::int) AND - numeral (Num.Bit1 y) = 1\ - \numeral (Num.Bit0 x) AND (1::int) = 0\ - \numeral (Num.Bit1 x) AND (1::int) = 1\ - \- numeral (Num.Bit0 x) AND (1::int) = 0\ - \- numeral (Num.Bit1 x) AND (1::int) = 1\ - by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI) - -lemma int_or_numerals [simp]: - \numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)\ - \numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\ - \numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)\ - \numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)\ - \numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)\ - \numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\ - \numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)\ - \numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))\ - \- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)\ - \- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)\ - \- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\ - \- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)\ - \- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)\ - \- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))\ - \- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)\ - \- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))\ - \(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\ - \(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)\ - \(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\ - \(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)\ - \numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)\ - \numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)\ - \- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)\ - \- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)\ - by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI) - -lemma int_xor_numerals [simp]: - \numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)\ - \numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\ - \numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)\ - \numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)\ - \numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)\ - \numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))\ - \numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)\ - \numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))\ - \- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)\ - \- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)\ - \- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\ - \- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)\ - \- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)\ - \- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))\ - \- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)\ - \- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))\ - \(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)\ - \(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)\ - \(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)\ - \(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))\ - \numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)\ - \numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)\ - \- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)\ - \- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))\ - by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI) - -end - context semiring_bit_operations begin @@ -3368,129 +3513,6 @@ qed -subsection \Symbolic computations on numeral expressions\ \<^marker>\contributor \Andreas Lochbihler\\ - -fun and_num :: \num \ num \ num option\ -where - \and_num num.One num.One = Some num.One\ -| \and_num num.One (num.Bit0 n) = None\ -| \and_num num.One (num.Bit1 n) = Some num.One\ -| \and_num (num.Bit0 m) num.One = None\ -| \and_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\ -| \and_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_num m n)\ -| \and_num (num.Bit1 m) num.One = Some num.One\ -| \and_num (num.Bit1 m) (num.Bit0 n) = map_option num.Bit0 (and_num m n)\ -| \and_num (num.Bit1 m) (num.Bit1 n) = (case and_num m n of None \ Some num.One | Some n' \ Some (num.Bit1 n'))\ - -fun and_not_num :: \num \ num \ num option\ -where - \and_not_num num.One num.One = None\ -| \and_not_num num.One (num.Bit0 n) = Some num.One\ -| \and_not_num num.One (num.Bit1 n) = None\ -| \and_not_num (num.Bit0 m) num.One = Some (num.Bit0 m)\ -| \and_not_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (and_not_num m n)\ -| \and_not_num (num.Bit0 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\ -| \and_not_num (num.Bit1 m) num.One = Some (num.Bit0 m)\ -| \and_not_num (num.Bit1 m) (num.Bit0 n) = (case and_not_num m n of None \ Some num.One | Some n' \ Some (num.Bit1 n'))\ -| \and_not_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (and_not_num m n)\ - -fun or_num :: \num \ num \ num\ -where - \or_num num.One num.One = num.One\ -| \or_num num.One (num.Bit0 n) = num.Bit1 n\ -| \or_num num.One (num.Bit1 n) = num.Bit1 n\ -| \or_num (num.Bit0 m) num.One = num.Bit1 m\ -| \or_num (num.Bit0 m) (num.Bit0 n) = num.Bit0 (or_num m n)\ -| \or_num (num.Bit0 m) (num.Bit1 n) = num.Bit1 (or_num m n)\ -| \or_num (num.Bit1 m) num.One = num.Bit1 m\ -| \or_num (num.Bit1 m) (num.Bit0 n) = num.Bit1 (or_num m n)\ -| \or_num (num.Bit1 m) (num.Bit1 n) = num.Bit1 (or_num m n)\ - -fun or_not_num_neg :: \num \ num \ num\ -where - \or_not_num_neg num.One num.One = num.One\ -| \or_not_num_neg num.One (num.Bit0 m) = num.Bit1 m\ -| \or_not_num_neg num.One (num.Bit1 m) = num.Bit1 m\ -| \or_not_num_neg (num.Bit0 n) num.One = num.Bit0 num.One\ -| \or_not_num_neg (num.Bit0 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\ -| \or_not_num_neg (num.Bit0 n) (num.Bit1 m) = num.Bit0 (or_not_num_neg n m)\ -| \or_not_num_neg (num.Bit1 n) num.One = num.One\ -| \or_not_num_neg (num.Bit1 n) (num.Bit0 m) = Num.BitM (or_not_num_neg n m)\ -| \or_not_num_neg (num.Bit1 n) (num.Bit1 m) = Num.BitM (or_not_num_neg n m)\ - -fun xor_num :: \num \ num \ num option\ -where - \xor_num num.One num.One = None\ -| \xor_num num.One (num.Bit0 n) = Some (num.Bit1 n)\ -| \xor_num num.One (num.Bit1 n) = Some (num.Bit0 n)\ -| \xor_num (num.Bit0 m) num.One = Some (num.Bit1 m)\ -| \xor_num (num.Bit0 m) (num.Bit0 n) = map_option num.Bit0 (xor_num m n)\ -| \xor_num (num.Bit0 m) (num.Bit1 n) = Some (case xor_num m n of None \ num.One | Some n' \ num.Bit1 n')\ -| \xor_num (num.Bit1 m) num.One = Some (num.Bit0 m)\ -| \xor_num (num.Bit1 m) (num.Bit0 n) = Some (case xor_num m n of None \ num.One | Some n' \ num.Bit1 n')\ -| \xor_num (num.Bit1 m) (num.Bit1 n) = map_option num.Bit0 (xor_num m n)\ - -lemma int_numeral_and_num: - \numeral m AND numeral n = (case and_num m n of None \ 0 :: int | Some n' \ numeral n')\ - by (induction m n rule: and_num.induct) (simp_all split: option.split) - -lemma and_num_eq_None_iff: - \and_num m n = None \ numeral m AND numeral n = (0::int)\ - by (simp add: int_numeral_and_num split: option.split) - -lemma and_num_eq_Some_iff: - \and_num m n = Some q \ numeral m AND numeral n = (numeral q :: int)\ - by (simp add: int_numeral_and_num split: option.split) - -lemma int_numeral_and_not_num: - \numeral m AND NOT (numeral n) = (case and_not_num m n of None \ 0 :: int | Some n' \ numeral n')\ - by (induction m n rule: and_not_num.induct) (simp_all add: add_One BitM_inc_eq not_int_def split: option.split) - -lemma int_numeral_not_and_num: - \NOT (numeral m) AND numeral n = (case and_not_num n m of None \ 0 :: int | Some n' \ numeral n')\ - using int_numeral_and_not_num [of n m] by (simp add: ac_simps) - -lemma and_not_num_eq_None_iff: - \and_not_num m n = None \ numeral m AND NOT (numeral n) = (0::int)\ - by (simp add: int_numeral_and_not_num split: option.split) - -lemma and_not_num_eq_Some_iff: - \and_not_num m n = Some q \ numeral m AND NOT (numeral n) = (numeral q :: int)\ - by (simp add: int_numeral_and_not_num split: option.split) - -lemma int_numeral_or_num: - \numeral m OR numeral n = (numeral (or_num m n) :: int)\ - by (induction m n rule: or_num.induct) simp_all - -lemma numeral_or_num_eq: - \numeral (or_num m n) = (numeral m OR numeral n :: int)\ - by (simp add: int_numeral_or_num) - -lemma int_numeral_or_not_num_neg: - \numeral m OR NOT (numeral n :: int) = - numeral (or_not_num_neg m n)\ - by (induction m n rule: or_not_num_neg.induct) (simp_all add: add_One BitM_inc_eq not_int_def) - -lemma int_numeral_not_or_num_neg: - \NOT (numeral m) OR (numeral n :: int) = - numeral (or_not_num_neg n m)\ - using int_numeral_or_not_num_neg [of n m] by (simp add: ac_simps) - -lemma numeral_or_not_num_eq: - \numeral (or_not_num_neg m n) = - (numeral m OR NOT (numeral n :: int))\ - using int_numeral_or_not_num_neg [of m n] by simp - -lemma int_numeral_xor_num: - \numeral m XOR numeral n = (case xor_num m n of None \ 0 :: int | Some n' \ numeral n')\ - by (induction m n rule: xor_num.induct) (simp_all split: option.split) - -lemma xor_num_eq_None_iff: - \xor_num m n = None \ numeral m XOR numeral n = (0::int)\ - by (simp add: int_numeral_xor_num split: option.split) - -lemma xor_num_eq_Some_iff: - \xor_num m n = Some q \ numeral m XOR numeral n = (numeral q :: int)\ - by (simp add: int_numeral_xor_num split: option.split) - - subsection \Key ideas of bit operations\ text \ diff -r 304f22435bc7 -r afe3c8ae1624 src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Fri Aug 20 17:57:57 2021 +0200 +++ b/src/HOL/Library/Word.thy Sat Aug 21 20:12:15 2021 +0000 @@ -3394,7 +3394,11 @@ "1 XOR - numeral b = word_of_int (1 XOR - numeral b)" "numeral a XOR 1 = word_of_int (numeral a XOR 1)" "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)" - by (transfer, simp)+ + apply (simp_all add: word_uint_eq_iff unsigned_not_eq unsigned_and_eq unsigned_or_eq unsigned_xor_eq not_one_eq of_nat_take_bit ac_simps) + apply (simp_all add: minus_numeral_eq_not_sub_one) + apply (simp_all only: sub_one_eq_not_neg bit.xor_compl_right take_bit_xor bit.double_compl) + apply simp_all + done text \Special cases for when one of the arguments equals -1.\ @@ -3408,6 +3412,10 @@ "x XOR (-1::'a::len word) = NOT x" by (transfer, simp)+ +lemma word_of_int_not_numeral_eq [simp]: + \(word_of_int (NOT (numeral bin)) :: 'a::len word) = - numeral bin - 1\ + by transfer (simp add: not_eq_complement) + lemma uint_and: \uint (x AND y) = uint x AND uint y\ by transfer simp