# HG changeset patch # User haftmann # Date 1598036370 0 # Node ID e4aecb0c729687423a6494aaeee6a198cd101db7 # Parent bdf77466b6c8dc93013c024861552b3f20c6304d more lemmas diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Aug 21 18:59:29 2020 +0000 +++ b/src/HOL/Divides.thy Fri Aug 21 18:59:30 2020 +0000 @@ -168,41 +168,6 @@ by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int) -subsubsection \General Properties of div and mod\ - -lemma div_pos_pos_trivial [simp]: - "k div l = 0" if "k \ 0" and "k < l" for k l :: int - using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def) - -lemma mod_pos_pos_trivial [simp]: - "k mod l = k" if "k \ 0" and "k < l" for k l :: int - using that by (simp add: mod_eq_self_iff_div_eq_0) - -lemma div_neg_neg_trivial [simp]: - "k div l = 0" if "k \ 0" and "l < k" for k l :: int - using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def) - -lemma mod_neg_neg_trivial [simp]: - "k mod l = k" if "k \ 0" and "l < k" for k l :: int - using that by (simp add: mod_eq_self_iff_div_eq_0) - -lemma div_pos_neg_trivial: - "k div l = - 1" if "0 < k" and "k + l \ 0" for k l :: int - apply (rule div_int_unique [of _ _ _ "k + l"]) - apply (use that in \auto simp add: eucl_rel_int_iff\) - done - -lemma mod_pos_neg_trivial: - "k mod l = k + l" if "0 < k" and "k + l \ 0" for k l :: int - apply (rule mod_int_unique [of _ _ "- 1"]) - apply (use that in \auto simp add: eucl_rel_int_iff\) - done - -text \There is neither \div_neg_pos_trivial\ nor \mod_neg_pos_trivial\ - because \<^term>\0 div l = 0\ would supersede it.\ - - - subsubsection \Laws for div and mod with Unary Minus\ lemma zminus1_lemma: @@ -662,31 +627,6 @@ using assms by (simp only: power_add eq) auto qed -text \Distributive laws for function \nat\.\ - -lemma nat_div_distrib: - assumes "0 \ x" - shows "nat (x div y) = nat x div nat y" -proof (cases y "0::int" rule: linorder_cases) - case less - with assms show ?thesis - using div_nonneg_neg_le0 by auto -next - case greater - then show ?thesis - by (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int) -qed auto - -(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*) -lemma nat_mod_distrib: - assumes "0 \ x" "0 \ y" - shows "nat (x mod y) = nat x mod nat y" -proof (cases "y = 0") - case False - with assms show ?thesis - by (simp add: nat_eq_iff zmod_int) -qed auto - text\Suggested by Matthias Daum\ lemma int_div_less_self: fixes x::int @@ -1335,4 +1275,6 @@ 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 bdf77466b6c8 -r e4aecb0c7296 src/HOL/Euclidean_Division.thy --- a/src/HOL/Euclidean_Division.thy Fri Aug 21 18:59:29 2020 +0000 +++ b/src/HOL/Euclidean_Division.thy Fri Aug 21 18:59:30 2020 +0000 @@ -1750,6 +1750,67 @@ by (simp only: modulo_int_unfold) simp qed +lemma div_pos_pos_trivial [simp]: + "k div l = 0" if "k \ 0" and "k < l" for k l :: int + using that by (simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def) + +lemma mod_pos_pos_trivial [simp]: + "k mod l = k" if "k \ 0" and "k < l" for k l :: int + using that by (simp add: mod_eq_self_iff_div_eq_0) + +lemma div_neg_neg_trivial [simp]: + "k div l = 0" if "k \ 0" and "l < k" for k l :: int + using that by (cases "k = 0") (simp, simp add: unique_euclidean_semiring_class.div_eq_0_iff division_segment_int_def) + +lemma mod_neg_neg_trivial [simp]: + "k mod l = k" if "k \ 0" and "l < k" for k l :: int + using that by (simp add: mod_eq_self_iff_div_eq_0) + +lemma div_pos_neg_trivial: + "k div l = - 1" if "0 < k" and "k + l \ 0" for k l :: int +proof (cases \l = - k\) + case True + with that show ?thesis + by (simp add: divide_int_def) +next + case False + show ?thesis + apply (rule div_eqI [of _ "k + l"]) + using False that apply (simp_all add: division_segment_int_def) + done +qed + +lemma mod_pos_neg_trivial: + "k mod l = k + l" if "0 < k" and "k + l \ 0" for k l :: int +proof (cases \l = - k\) + case True + with that show ?thesis + by (simp add: divide_int_def) +next + case False + show ?thesis + apply (rule mod_eqI [of _ _ \- 1\]) + using False that apply (simp_all add: division_segment_int_def) + done +qed + +text \There is neither \div_neg_pos_trivial\ nor \mod_neg_pos_trivial\ + because \<^term>\0 div l = 0\ would supersede it.\ + +text \Distributive laws for function \nat\.\ + +lemma nat_div_distrib: + \nat (x div y) = nat x div nat y\ if \0 \ x\ + using that by (simp add: divide_int_def sgn_if) + +lemma nat_div_distrib': + \nat (x div y) = nat x div nat y\ if \0 \ y\ + using that by (simp add: divide_int_def sgn_if) + +lemma nat_mod_distrib: \ \Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't\ + \nat (x mod y) = nat x mod nat y\ if \0 \ x\ \0 \ y\ + using that by (simp add: modulo_int_def sgn_if) + subsection \Special case: euclidean rings containing the natural numbers\ diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Groups_List.thy --- a/src/HOL/Groups_List.thy Fri Aug 21 18:59:29 2020 +0000 +++ b/src/HOL/Groups_List.thy Fri Aug 21 18:59:30 2020 +0000 @@ -455,6 +455,17 @@ end +lemma horner_sum_of_bool_2_less: + \(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\ +proof - + have \(\n = 0.. (\n = 0.. + by (rule sum_mono) simp + also have \\ = 2 ^ length bs - 1\ + by (induction bs) simp_all + finally show ?thesis + by (simp add: horner_sum_eq_sum) +qed + subsection \Further facts about \<^const>\List.n_lists\\ diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Library/Bit_Operations.thy --- a/src/HOL/Library/Bit_Operations.thy Fri Aug 21 18:59:29 2020 +0000 +++ b/src/HOL/Library/Bit_Operations.thy Fri Aug 21 18:59:30 2020 +0000 @@ -9,27 +9,6 @@ Main begin -lemma nat_take_bit_eq: - \nat (take_bit n k) = take_bit n (nat k)\ - if \k \ 0\ - using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq) - -lemma take_bit_eq_self: - \take_bit m n = n\ if \n < 2 ^ m\ for n :: nat - using that by (simp add: take_bit_eq_mod) - -lemma horner_sum_of_bool_2_less: - \(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\ -proof - - have \(\n = 0.. (\n = 0.. - by (rule sum_mono) simp - also have \\ = 2 ^ length bs - 1\ - by (induction bs) simp_all - finally show ?thesis - by (simp add: horner_sum_eq_sum) -qed - - subsection \Bit operations\ class semiring_bit_operations = semiring_bit_shifts + @@ -840,6 +819,87 @@ \bit (signed_take_bit m k) n = bit k (min m n)\ by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def) +lemma signed_take_bit_of_0 [simp]: + \signed_take_bit n 0 = 0\ + by (simp add: signed_take_bit_def) + +lemma signed_take_bit_of_minus_1 [simp]: + \signed_take_bit n (- 1) = - 1\ + by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask) + +lemma signed_take_bit_signed_take_bit [simp]: + \signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\ + by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff) + +lemma signed_take_bit_eq_iff_take_bit_eq: + \signed_take_bit n k = signed_take_bit n l \ take_bit (Suc n) k = take_bit (Suc n) l\ +proof (cases \bit k n \ bit l n\) + case True + moreover have \take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\ + for k :: int + by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask) + ultimately show ?thesis + by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq) +next + case False + then have \signed_take_bit n k \ signed_take_bit n l\ and \take_bit (Suc n) k \ take_bit (Suc n) l\ + by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def) + then show ?thesis + by simp +qed + +lemma take_bit_signed_take_bit: + \take_bit m (signed_take_bit n k) = take_bit m k\ if \m \ Suc n\ + using that by (rule le_SucE; intro bit_eqI) + (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) + +lemma signed_take_bit_add: + \signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\ +proof - + have \take_bit (Suc n) + (take_bit (Suc n) (signed_take_bit n k) + + take_bit (Suc n) (signed_take_bit n l)) = + take_bit (Suc n) (k + l)\ + by (simp add: take_bit_signed_take_bit take_bit_add) + then show ?thesis + by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_add) +qed + +lemma signed_take_bit_diff: + \signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)\ +proof - + have \take_bit (Suc n) + (take_bit (Suc n) (signed_take_bit n k) - + take_bit (Suc n) (signed_take_bit n l)) = + take_bit (Suc n) (k - l)\ + by (simp add: take_bit_signed_take_bit take_bit_diff) + then show ?thesis + by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_diff) +qed + +lemma signed_take_bit_minus: + \signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)\ +proof - + have \take_bit (Suc n) + (- take_bit (Suc n) (signed_take_bit n k)) = + take_bit (Suc n) (- k)\ + by (simp add: take_bit_signed_take_bit take_bit_minus) + then show ?thesis + by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_minus) +qed + +lemma signed_take_bit_mult: + \signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)\ +proof - + have \take_bit (Suc n) + (take_bit (Suc n) (signed_take_bit n k) * + take_bit (Suc n) (signed_take_bit n l)) = + take_bit (Suc n) (k * l)\ + by (simp add: take_bit_signed_take_bit take_bit_mult) + then show ?thesis + by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult) +qed + text \Modulus centered around 0\ lemma signed_take_bit_eq_take_bit_minus: @@ -885,40 +945,6 @@ (simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps) qed -lemma signed_take_bit_of_0 [simp]: - \signed_take_bit n 0 = 0\ - by (simp add: signed_take_bit_def) - -lemma signed_take_bit_of_minus_1 [simp]: - \signed_take_bit n (- 1) = - 1\ - by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask) - -lemma signed_take_bit_eq_iff_take_bit_eq: - \signed_take_bit n k = signed_take_bit n l \ take_bit (Suc n) k = take_bit (Suc n) l\ -proof (cases \bit k n \ bit l n\) - case True - moreover have \take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\ - for k :: int - by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask) - ultimately show ?thesis - by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq) -next - case False - then have \signed_take_bit n k \ signed_take_bit n l\ and \take_bit (Suc n) k \ take_bit (Suc n) l\ - by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def) - then show ?thesis - by simp -qed - -lemma signed_take_bit_signed_take_bit [simp]: - \signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\ - by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff) - -lemma take_bit_signed_take_bit: - \take_bit m (signed_take_bit n k) = take_bit m k\ if \m \ Suc n\ - using that by (rule le_SucE; intro bit_eqI) - (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) - lemma signed_take_bit_take_bit: \signed_take_bit m (take_bit n k) = (if n \ m then take_bit n else signed_take_bit m) k\ by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff) @@ -941,6 +967,10 @@ using that take_bit_less_eq [of \Suc n\ \k + 2 ^ n\] by (simp add: signed_take_bit_eq_take_bit_shift) +lemma signed_take_bit_eq_self: + \signed_take_bit n k = k\ if \- (2 ^ n) \ k\ \k < 2 ^ n\ + using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self) + lemma signed_take_bit_Suc_1 [simp]: \signed_take_bit (Suc n) 1 = 1\ by (simp add: signed_take_bit_Suc) diff -r bdf77466b6c8 -r e4aecb0c7296 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Fri Aug 21 18:59:29 2020 +0000 +++ b/src/HOL/Parity.thy Fri Aug 21 18:59:30 2020 +0000 @@ -1606,6 +1606,11 @@ by simp qed +lemma nat_take_bit_eq: + \nat (take_bit n k) = take_bit n (nat k)\ + if \k \ 0\ + using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq) + lemma not_exp_less_eq_0_int [simp]: \\ 2 ^ n \ (0::int)\ by (simp add: power_le_zero_eq) @@ -1686,6 +1691,27 @@ \take_bit n k < 2 ^ n\ for k :: int by (simp add: take_bit_eq_mod) +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_eq_mod) + +lemma bit_imp_take_bit_positive: + \0 < take_bit m k\ if \n < m\ and \bit k n\ for k :: int +proof (rule ccontr) + assume \\ 0 < take_bit m k\ + then have \take_bit m k = 0\ + by (auto simp add: not_less intro: order_antisym) + then have \bit (take_bit m k) n = bit 0 n\ + by simp + with that show False + by (simp add: bit_take_bit_iff) +qed + +lemma take_bit_mult: + \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_mult_eq) + lemma (in ring_1) of_nat_nat_take_bit_eq [simp]: \of_nat (nat (take_bit n k)) = of_int (take_bit n k)\ by simp