# HG changeset patch # User haftmann # Date 1581245192 0 # Node ID e83fe2c31088ecf978ecd45f1ee5de9062aa36ee # Parent 7ae4dcf332ae9a52a47b45ad773385b3145acda3 rule concerning bit (push_bit ...) diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sun Feb 09 10:21:01 2020 +0000 +++ b/src/HOL/Code_Numeral.thy Sun Feb 09 10:46:32 2020 +0000 @@ -300,7 +300,7 @@ (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq - even_mask_div_iff)+ + even_mask_div_iff even_mult_exp_div_exp_iff)+ end @@ -997,7 +997,7 @@ (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq - even_mask_div_iff)+ + even_mask_div_iff even_mult_exp_div_exp_iff)+ end diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sun Feb 09 10:21:01 2020 +0000 +++ b/src/HOL/Parity.thy Sun Feb 09 10:46:32 2020 +0000 @@ -674,6 +674,7 @@ and mod_exp_eq: \a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\ and mult_exp_mod_exp_eq: \m \ n \ (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\ and div_exp_mod_exp_eq: \a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\ + and even_mult_exp_div_exp_iff: \even (a * 2 ^ m div 2 ^ n) \ m > n \ 2 ^ n = 0 \ (m \ n \ even (a div 2 ^ (n - m)))\ begin lemma bits_div_by_0 [simp]: @@ -958,6 +959,11 @@ show \even ((2 ^ m - (1::nat)) div 2 ^ n) \ 2 ^ n = (0::nat) \ m \ n\ for m n :: nat using even_mask_div_iff' [where ?'a = nat, of m n] by simp + show \even (q * 2 ^ m div 2 ^ n) \ n < m \ (2::nat) ^ n = 0 \ m \ n \ even (q div 2 ^ (n - m))\ + for m n q r :: nat + apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex) + apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc) + done qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff) lemma int_bit_induct [case_names zero minus even odd]: @@ -1074,6 +1080,11 @@ show \even ((2 ^ m - (1::int)) div 2 ^ n) \ 2 ^ n = (0::int) \ m \ n\ for m n :: nat using even_mask_div_iff' [where ?'a = int, of m n] by simp + show \even (k * 2 ^ m div 2 ^ n) \ n < m \ (2::int) ^ n = 0 \ m \ n \ even (k div 2 ^ (n - m))\ + for m n :: nat and k l :: int + apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex) + apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2)) + done qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le) class semiring_bit_shifts = semiring_bits + @@ -1250,6 +1261,14 @@ by simp qed +lemma even_push_bit_iff [simp]: + \even (push_bit n a) \ n \ 0 \ even a\ + by (simp add: push_bit_eq_mult) auto + +lemma bit_push_bit_iff: + \bit (push_bit m a) n \ n \ m \ 2 ^ n \ 0 \ (n < m \ bit a (n - m))\ + by (auto simp add: bit_def push_bit_eq_mult even_mult_exp_div_exp_iff) + lemma bit_drop_bit_eq: \bit (drop_bit n a) = bit a \ (+) n\ by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div) @@ -1298,35 +1317,11 @@ lemma bit_push_bit_iff_nat: \bit (push_bit m q) n \ m \ n \ bit q (n - m)\ for q :: nat -proof (cases \m \ n\) - case True - then obtain r where \n = m + r\ - using le_Suc_ex by blast - with True show ?thesis - by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \2 ^ m\]) -next - case False - then obtain r where \m = Suc (n + r)\ - using less_imp_Suc_add not_le by blast - with False show ?thesis - by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \2 ^ n\]) -qed + by (auto simp add: bit_push_bit_iff) lemma bit_push_bit_iff_int: \bit (push_bit m k) n \ m \ n \ bit k (n - m)\ for k :: int -proof (cases \m \ n\) - case True - then obtain r where \n = m + r\ - using le_Suc_ex by blast - with True show ?thesis - by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \2 ^ m\]) -next - case False - then obtain r where \m = Suc (n + r)\ - using less_imp_Suc_add not_le by blast - with False show ?thesis - by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \2 ^ n\]) -qed + by (auto simp add: bit_push_bit_iff) class unique_euclidean_semiring_with_bit_shifts = unique_euclidean_semiring_with_nat + semiring_bit_shifts @@ -1421,13 +1416,7 @@ lemma bit_push_bit_iff_of_nat_iff: \bit (push_bit m (of_nat r)) n \ m \ n \ bit (of_nat r) (n - m)\ -proof - - from bit_push_bit_iff_nat - have \bit (of_nat (push_bit m r)) n \ m \ n \ bit (of_nat r) (n - m)\ - by simp - then show ?thesis - by (simp add: of_nat_push_bit) -qed + by (auto simp add: bit_push_bit_iff) end @@ -1463,12 +1452,12 @@ \drop_bit n (- 1 :: int) = - 1\ by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int) -lemma take_bit_uminus: +lemma take_bit_minus: "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int by (simp add: take_bit_eq_mod mod_minus_eq) -lemma take_bit_minus: +lemma take_bit_diff: "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" for k l :: int by (simp add: take_bit_eq_mod mod_diff_eq) @@ -1478,4 +1467,9 @@ for k :: int by (simp add: take_bit_eq_mod) +lemma drop_bit_push_bit_int: + \drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\ for k :: int + by (cases \m \ n\) (auto simp add: mult.left_commute [of _ \2 ^ n\] mult.commute [of _ \2 ^ n\] mult.assoc + mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add) + end diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy Sun Feb 09 10:21:01 2020 +0000 +++ b/src/HOL/ex/Bit_Operations.thy Sun Feb 09 10:46:32 2020 +0000 @@ -9,15 +9,6 @@ Main begin -context semiring_bit_shifts -begin - -(*lemma bit_push_bit_iff: - \bit (push_bit m a) n \ n \ m \ 2 ^ n \ 0 \ bit a (n - m)\*) - -end - - subsection \Bit operations in suitable algebraic structures\ class semiring_bit_operations = semiring_bit_shifts + diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy Sun Feb 09 10:21:01 2020 +0000 +++ b/src/HOL/ex/Word.thy Sun Feb 09 10:46:32 2020 +0000 @@ -105,11 +105,11 @@ lift_definition uminus_word :: "'a word \ 'a word" is uminus - by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus) + by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus) lift_definition minus_word :: "'a word \ 'a word \ 'a word" is minus - by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus) + by (subst take_bit_diff [symmetric]) (simp add: take_bit_diff) lift_definition times_word :: "'a word \ 'a word \ 'a word" is times @@ -617,6 +617,17 @@ show \even ((2 ^ m - 1) div (2::'a word) ^ n) \ 2 ^ n = (0::'a word) \ m \ n\ for m n :: nat by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) + show \even (a * 2 ^ m div 2 ^ n) \ n < m \ (2::'a word) ^ n = 0 \ m \ n \ even (a div 2 ^ (n - m))\ + for a :: \'a word\ and m n :: nat + proof transfer + show \even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \ + n < m + \ take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0 + \ (m \ n \ even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\ + for m n :: nat and k l :: int + by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult + simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m]) + qed qed context