# HG changeset patch # User huffman # Date 1332868865 -7200 # Node ID 9344891b504b8ea0499d820827aeb01e7fed63e7 # Parent 6a4c479ba94f03195678df906a3dbb4ffc1894e1 remove redundant lemmas diff -r 6a4c479ba94f -r 9344891b504b NEWS --- a/NEWS Tue Mar 27 16:04:51 2012 +0200 +++ b/NEWS Tue Mar 27 19:21:05 2012 +0200 @@ -144,6 +144,8 @@ zmod_self ~> mod_self zdiv_zero ~> div_0 zmod_zero ~> mod_0 + zdiv_zmod_equality ~> div_mod_equality2 + zdiv_zmod_equality2 ~> div_mod_equality zmod_zdiv_trivial ~> mod_div_trivial zdiv_zminus_zminus ~> div_minus_minus zmod_zminus_zminus ~> mod_minus_minus diff -r 6a4c479ba94f -r 9344891b504b src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Mar 27 16:04:51 2012 +0200 +++ b/src/HOL/Divides.thy Tue Mar 27 19:21:05 2012 +0200 @@ -1436,12 +1436,6 @@ lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)" by (fact mod_div_equality2 [symmetric]) -lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k" - by (fact div_mod_equality2) - -lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k" - by (fact div_mod_equality) - text {* Tool setup *} (* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *) @@ -1456,7 +1450,7 @@ val mk_sum = Arith_Data.mk_sum HOLogic.intT; val dest_sum = Arith_Data.dest_sum; - val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}]; + val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}]; val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac})) diff -r 6a4c479ba94f -r 9344891b504b src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Tue Mar 27 16:04:51 2012 +0200 +++ b/src/HOL/Groebner_Basis.thy Tue Mar 27 19:21:05 2012 +0200 @@ -53,7 +53,7 @@ declare div_by_0[algebra] declare mod_by_0[algebra] declare zmod_zdiv_equality[symmetric,algebra] -declare zdiv_zmod_equality[symmetric, algebra] +declare div_mod_equality2[symmetric, algebra] declare div_minus_minus[algebra] declare mod_minus_minus[algebra] declare div_minus_right[algebra] diff -r 6a4c479ba94f -r 9344891b504b src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Tue Mar 27 16:04:51 2012 +0200 +++ b/src/HOL/Library/Float.thy Tue Mar 27 19:21:05 2012 +0200 @@ -488,7 +488,7 @@ hence "x < x - x mod 2 + 2" unfolding algebra_simps by auto thus ?thesis by auto qed - also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto + also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` div_mod_equality[of x 2 0] by auto also have "\ \ 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto) also have "\ = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto finally have "x + 1 \ 2^(1 + nat (bitlen (x div 2)))" . @@ -1122,7 +1122,7 @@ show ?thesis proof (cases "m mod ?p = 0") case True - have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] . + have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using mod_div_equality [symmetric] . have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real] by (auto simp add: pow2_add `0 < ?d` pow_d) thus ?thesis @@ -1130,7 +1130,7 @@ by auto next case False - have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. + have "m = m div ?p * ?p + m mod ?p" unfolding mod_div_equality .. also have "\ \ (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) finally have "real (Float m e) \ real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e] unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric] @@ -1156,7 +1156,7 @@ case True hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp have "m div ?p * ?p \ m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le]) - also have "\ \ m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. + also have "\ \ m" unfolding mod_div_equality .. finally have "real (Float (m div ?p) (e + ?d)) \ real (Float m e)" unfolding real_of_float_simp add_commute[of e] unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric] by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) diff -r 6a4c479ba94f -r 9344891b504b src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Tue Mar 27 16:04:51 2012 +0200 +++ b/src/HOL/Presburger.thy Tue Mar 27 19:21:05 2012 +0200 @@ -405,8 +405,8 @@ declare mod_div_equality[presburger] declare mod_mult_self1[presburger] declare mod_mult_self2[presburger] -declare zdiv_zmod_equality2[presburger] -declare zdiv_zmod_equality[presburger] +declare div_mod_equality[presburger] +declare div_mod_equality2[presburger] declare mod2_Suc_Suc[presburger] lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a" by simp_all