# HG changeset patch # User huffman # Date 1332854869 -7200 # Node ID 978c00c20a59a94514c68bda7eccb5fd0d77652d # Parent d64fa2ca54b8fda6e69ee35483018c103b0ae02a generalize some theorems about div/mod diff -r d64fa2ca54b8 -r 978c00c20a59 NEWS --- a/NEWS Tue Mar 27 14:49:56 2012 +0200 +++ b/NEWS Tue Mar 27 15:27:49 2012 +0200 @@ -145,6 +145,12 @@ zdiv_zero ~> div_0 zmod_zero ~> mod_0 zmod_zdiv_trivial ~> mod_div_trivial + zdiv_zminus_zminus ~> div_minus_minus + zmod_zminus_zminus ~> mod_minus_minus + zdiv_zminus2 ~> div_minus_right + zmod_zminus2 ~> mod_minus_right + mod_mult_distrib ~> mult_mod_left + mod_mult_distrib2 ~> mult_mod_right * More default pred/set conversions on a couple of relation operations and predicates. Consolidation of some relation theorems: diff -r d64fa2ca54b8 -r 978c00c20a59 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Divides.thy Tue Mar 27 15:27:49 2012 +0200 @@ -343,6 +343,12 @@ "(a * c) mod (b * c) = (a mod b) * c" using mod_mult_mult1 [of c a b] by (simp add: mult_commute) +lemma mult_mod_left: "(a mod b) * c = (a * c) mod (b * c)" + by (fact mod_mult_mult2 [symmetric]) + +lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)" + by (fact mod_mult_mult1 [symmetric]) + lemma dvd_mod: "k dvd m \ k dvd n \ k dvd (m mod n)" unfolding dvd_def by (auto simp add: mod_mult_mult1) @@ -444,6 +450,19 @@ apply simp done +lemma div_minus_minus [simp]: "(-a) div (-b) = a div b" + using div_mult_mult1 [of "- 1" a b] + unfolding neg_equal_0_iff_equal by simp + +lemma mod_minus_minus [simp]: "(-a) mod (-b) = - (a mod b)" + using mod_mult_mult1 [of "- 1" a b] by simp + +lemma div_minus_right: "a div (-b) = (-a) div b" + using div_minus_minus [of "-a" b] by simp + +lemma mod_minus_right: "a mod (-b) = - ((-a) mod b)" + using mod_minus_minus [of "-a" b] by simp + end @@ -712,12 +731,6 @@ lemma mod_1 [simp]: "m mod Suc 0 = 0" by (induct m) (simp_all add: mod_geq) -lemma mod_mult_distrib: "(m mod n) * (k\nat) = (m * k) mod (n * k)" - by (fact mod_mult_mult2 [symmetric]) (* FIXME: generalize *) - -lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)" - by (fact mod_mult_mult1 [symmetric]) (* FIXME: generalize *) - (* a simple rearrangement of mod_div_equality: *) lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)" using mod_div_equality2 [of n m] by arith @@ -1489,15 +1502,6 @@ text{*There is no @{text mod_neg_pos_trivial}.*} -(*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) -lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)" - using div_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *) - -(*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) -lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))" - using mod_mult_mult1 [of "-1" a b] by simp (* FIXME: generalize *) - - subsubsection {* Laws for div and mod with Unary Minus *} lemma zminus1_lemma: @@ -1524,21 +1528,15 @@ shows "- k mod l \ 0 \ k mod l \ 0" unfolding zmod_zminus1_eq_if by auto -lemma zdiv_zminus2: "a div (-b) = (-a::int) div b" - using zdiv_zminus_zminus [of "-a" b] by simp (* FIXME: generalize *) - -lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)" - using zmod_zminus_zminus [of "-a" b] by simp (* FIXME: generalize*) - lemma zdiv_zminus2_eq_if: "b \ (0::int) ==> a div (-b) = (if a mod b = 0 then - (a div b) else - (a div b) - 1)" -by (simp add: zdiv_zminus1_eq_if zdiv_zminus2) +by (simp add: zdiv_zminus1_eq_if div_minus_right) lemma zmod_zminus2_eq_if: "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)" -by (simp add: zmod_zminus1_eq_if zmod_zminus2) +by (simp add: zmod_zminus1_eq_if mod_minus_right) lemma zmod_zminus2_not_zero: fixes k l :: int @@ -2024,7 +2022,7 @@ have "(1 + 2 * (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)" by (rule pos_zdiv_mult_2, simp add: A) thus ?thesis - by (simp only: R zdiv_zminus_zminus diff_minus + by (simp only: R div_minus_minus diff_minus minus_add_distrib [symmetric] mult_minus_right) qed @@ -2072,7 +2070,7 @@ from assms have "0 \ - a" by auto then have "(1 + 2 * (- b - 1)) mod (2 * (- a)) = 1 + 2 * ((- b - 1) mod (- a))" by (rule pos_zmod_mult_2) - then show ?thesis by (simp add: zmod_zminus2 algebra_simps) + then show ?thesis by (simp add: mod_minus_right algebra_simps) (simp add: diff_minus add_ac) qed @@ -2131,7 +2129,7 @@ lemma neg_imp_zdiv_nonneg_iff: "b < (0::int) ==> (0 \ a div b) = (a \ (0::int))" -apply (subst zdiv_zminus_zminus [symmetric]) +apply (subst div_minus_minus [symmetric]) apply (subst pos_imp_zdiv_nonneg_iff, auto) done diff -r d64fa2ca54b8 -r 978c00c20a59 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Groebner_Basis.thy Tue Mar 27 15:27:49 2012 +0200 @@ -54,10 +54,10 @@ declare mod_by_0[algebra] declare zmod_zdiv_equality[symmetric,algebra] declare zdiv_zmod_equality[symmetric, algebra] -declare zdiv_zminus_zminus[algebra] -declare zmod_zminus_zminus[algebra] -declare zdiv_zminus2[algebra] -declare zmod_zminus2[algebra] +declare div_minus_minus[algebra] +declare mod_minus_minus[algebra] +declare div_minus_right[algebra] +declare mod_minus_right[algebra] declare div_0[algebra] declare mod_0[algebra] declare mod_by_1[algebra] diff -r d64fa2ca54b8 -r 978c00c20a59 src/HOL/Import/HOL_Light/HOLLightInt.thy --- a/src/HOL/Import/HOL_Light/HOLLightInt.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy Tue Mar 27 15:27:49 2012 +0200 @@ -162,7 +162,7 @@ apply (simp add: hl_mod_def hl_div_def) apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute) apply (simp add: hl_mod_def hl_div_def) - by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2) + by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff div_minus_right) lemma DEF_rem: "hl_mod = (SOME r. \m n. if n = int 0 then @@ -182,7 +182,7 @@ apply (simp add: hl_mod_def hl_div_def) apply (metis add_left_cancel mod_div_equality) apply (simp add: hl_mod_def hl_div_def) - by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute) + by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod mod_minus_right mult_commute) lemma DEF_int_gcd: "int_gcd = (SOME d. \a b. (int 0) \ (d (a, b)) \ (d (a, b)) dvd a \ diff -r d64fa2ca54b8 -r 978c00c20a59 src/HOL/Library/Char_nat.thy --- a/src/HOL/Library/Char_nat.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Library/Char_nat.thy Tue Mar 27 15:27:49 2012 +0200 @@ -158,7 +158,7 @@ unfolding 256 mult_assoc [symmetric] mod_mult_self3 .. show ?thesis by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair - nat_of_nibble_of_nat mod_mult_distrib + nat_of_nibble_of_nat mult_mod_left n aux3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256) qed diff -r d64fa2ca54b8 -r 978c00c20a59 src/HOL/Library/Target_Numeral.thy --- a/src/HOL/Library/Target_Numeral.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Library/Target_Numeral.thy Tue Mar 27 15:27:49 2012 +0200 @@ -296,7 +296,7 @@ have aux2: "\q::int. - int_of k = int_of l * q \ int_of k = int_of l * - q" by auto show ?thesis by (simp add: prod_eq_iff Target_Numeral.int_eq_iff prod_case_beta aux1) - (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if zdiv_zminus2 zmod_zminus2 aux2) + (auto simp add: zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right aux2) qed lemma div_int_code [code]: diff -r d64fa2ca54b8 -r 978c00c20a59 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Tue Mar 27 14:49:56 2012 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Tue Mar 27 15:27:49 2012 +0200 @@ -72,7 +72,7 @@ lemma nat_mult_dvd_cancel_disj[simp]: "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))" -by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric]) +by (auto simp: dvd_eq_mod_eq_0 mod_mult_mult1) lemma nat_mult_dvd_cancel1: "0 < k \ (k*m) dvd (k*n::nat) = (m dvd n)" by(auto)