# HG changeset patch # User haftmann # Date 1580580640 -3600 # Node ID 65ffe9e910d49857169788f271cbabb86c40a9a6 # Parent 96d126844adc22692440d51104c6bcd3791ff1fb more specific class assumptions diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Feb 01 19:10:37 2020 +0100 +++ b/src/HOL/Code_Numeral.thy Sat Feb 01 19:10:40 2020 +0100 @@ -299,7 +299,8 @@ instance by (standard; transfer) (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)+ + exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq + even_mask_div_iff)+ end @@ -995,7 +996,8 @@ instance by (standard; transfer) (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)+ + exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq + even_mask_div_iff)+ end diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Euclidean_Division.thy --- a/src/HOL/Euclidean_Division.thy Sat Feb 01 19:10:37 2020 +0100 +++ b/src/HOL/Euclidean_Division.thy Sat Feb 01 19:10:40 2020 +0100 @@ -327,6 +327,26 @@ using div_plus_div_distrib_dvd_left [of c b a] by (simp add: ac_simps) +lemma sum_div_partition: + \(\a\A. f a) div b = (\a\A \ {a. b dvd f a}. f a div b) + (\a\A \ {a. \ b dvd f a}. f a) div b\ + if \finite A\ +proof - + have \A = A \ {a. b dvd f a} \ A \ {a. \ b dvd f a}\ + by auto + then have \(\a\A. f a) = (\a\A \ {a. b dvd f a} \ A \ {a. \ b dvd f a}. f a)\ + by simp + also have \\ = (\a\A \ {a. b dvd f a}. f a) + (\a\A \ {a. \ b dvd f a}. f a)\ + using \finite A\ by (auto intro: sum.union_inter_neutral) + finally have *: \sum f A = sum f (A \ {a. b dvd f a}) + sum f (A \ {a. \ b dvd f a})\ . + define B where B: \B = A \ {a. b dvd f a}\ + with \finite A\ have \finite B\ and \a \ B \ b dvd f a\ for a + by simp_all + then have \(\a\B. f a) div b = (\a\B. f a div b)\ and \b dvd (\a\B. f a)\ + by induction (simp_all add: div_plus_div_distrib_dvd_left) + then show ?thesis using * + by (simp add: B div_plus_div_distrib_dvd_left) +qed + named_theorems mod_simps text \Addition respects modular equivalence.\ @@ -442,6 +462,26 @@ by (simp add: mod_mult_left_eq mod_mult_right_eq) qed +lemma power_diff_power_eq: + \a ^ m div a ^ n = (if n \ m then a ^ (m - n) else 1 div a ^ (n - m))\ + if \a \ 0\ +proof (cases \n \ m\) + case True + with that power_diff [symmetric, of a n m] show ?thesis by simp +next + case False + then obtain q where n: \n = m + Suc q\ + by (auto simp add: not_le dest: less_imp_Suc_add) + then have \a ^ m div a ^ n = (a ^ m * 1) div (a ^ m * a ^ Suc q)\ + by (simp add: power_add ac_simps) + moreover from that have \a ^ m \ 0\ + by simp + ultimately have \a ^ m div a ^ n = 1 div a ^ Suc q\ + by (subst (asm) div_mult_mult1) simp + with False n show ?thesis + by simp +qed + end diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sat Feb 01 19:10:37 2020 +0100 +++ b/src/HOL/Parity.thy Sat Feb 01 19:10:40 2020 +0100 @@ -411,6 +411,10 @@ qed qed +lemma mask_eq_sum_exp_nat: + \2 ^ n - Suc 0 = (\m\{q. q < n}. 2 ^ m)\ + using mask_eq_sum_exp [where ?'a = nat] by simp + context semiring_parity begin @@ -573,6 +577,43 @@ end +context unique_euclidean_semiring_with_nat +begin + +lemma even_mask_div_iff': + \even ((2 ^ m - 1) div 2 ^ n) \ m \ n\ +proof - + have \even ((2 ^ m - 1) div 2 ^ n) \ even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\ + by (simp only: of_nat_div) (simp add: of_nat_diff) + also have \\ \ even ((2 ^ m - Suc 0) div 2 ^ n)\ + by simp + also have \\ \ m \ n\ + proof (cases \m \ n\) + case True + then show ?thesis + by (simp add: Suc_le_lessD) + next + case False + then obtain r where r: \m = n + Suc r\ + using less_imp_Suc_add by fastforce + from r have \{q. q < m} \ {q. 2 ^ n dvd (2::nat) ^ q} = {q. n \ q \ q < m}\ + by (auto simp add: dvd_power_iff_le) + moreover from r have \{q. q < m} \ {q. \ 2 ^ n dvd (2::nat) ^ q} = {q. q < n}\ + by (auto simp add: dvd_power_iff_le) + moreover from False have \{q. n \ q \ q < m \ q \ n} = {n}\ + by auto + then have \odd ((\a\{q. n \ q \ q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)\ + by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff not_less mask_eq_sum_exp_nat [symmetric]) + ultimately have \odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\ + by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all + with False show ?thesis + by (simp add: mask_eq_sum_exp_nat) + qed + finally show ?thesis . +qed + +end + subsection \Instance for \<^typ>\int\\ @@ -627,6 +668,7 @@ and bits_div_by_1 [simp]: \a div 1 = a\ and bits_mod_div_trivial [simp]: \a mod b div b = 0\ and even_succ_div_2 [simp]: \even a \ (1 + a) div 2 = a div 2\ + and even_mask_div_iff: \even ((2 ^ m - 1) div 2 ^ n) \ 2 ^ n = 0 \ m \ n\ and exp_div_exp_eq: \2 ^ m div 2 ^ n = of_bool (2 ^ m \ 0 \ m \ n) * 2 ^ (m - n)\ and div_exp_eq: \a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\ and mod_exp_eq: \a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\ @@ -881,6 +923,9 @@ apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin) apply (simp add: mult.commute) done + 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 qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff) lemma int_bit_induct [case_names zero minus even odd]: @@ -994,6 +1039,9 @@ apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin) apply (simp add: ac_simps) done + 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 qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le) class semiring_bit_shifts = semiring_bits + diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy Sat Feb 01 19:10:37 2020 +0100 +++ b/src/HOL/ex/Bit_Operations.thy Sat Feb 01 19:10:40 2020 +0100 @@ -12,13 +12,9 @@ context semiring_bits begin -(*lemma even_mask_div_iff: - \even ((2 ^ m - 1) div 2 ^ n) \ 2 ^ n = 0 \ m \ n\ - sorry - lemma bit_mask_iff: \bit (2 ^ m - 1) n \ 2 ^ n \ 0 \ n < m\ - by (simp add: bit_def even_mask_div_iff not_le)*) + by (simp add: bit_def even_mask_div_iff not_le) end diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy Sat Feb 01 19:10:37 2020 +0100 +++ b/src/HOL/ex/Word.thy Sat Feb 01 19:10:40 2020 +0100 @@ -548,10 +548,6 @@ (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff, simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) -(*lemma even_mask_div_iff_word: - \even ((2 ^ m - 1) div (2::'a word) ^ n) \ 2 ^ n = (0::'a::len word) \ m \ n\ - by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*) - instance word :: (len) semiring_bits proof show \P a\ if stable: \\a. a div 2 = a \ P a\ @@ -618,6 +614,9 @@ show \a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\ for a :: "'a word" and m n :: nat by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin) + 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) qed context