remove redundant lemmas
authorhuffman
Tue Mar 27 19:21:05 2012 +0200 (2012-03-27)
changeset 471659344891b504b
parent 47164 6a4c479ba94f
child 47166 108bf76ca00c
remove redundant lemmas
NEWS
src/HOL/Divides.thy
src/HOL/Groebner_Basis.thy
src/HOL/Library/Float.thy
src/HOL/Presburger.thy
     1.1 --- a/NEWS	Tue Mar 27 16:04:51 2012 +0200
     1.2 +++ b/NEWS	Tue Mar 27 19:21:05 2012 +0200
     1.3 @@ -144,6 +144,8 @@
     1.4    zmod_self ~> mod_self
     1.5    zdiv_zero ~> div_0
     1.6    zmod_zero ~> mod_0
     1.7 +  zdiv_zmod_equality ~> div_mod_equality2
     1.8 +  zdiv_zmod_equality2 ~> div_mod_equality
     1.9    zmod_zdiv_trivial ~> mod_div_trivial
    1.10    zdiv_zminus_zminus ~> div_minus_minus
    1.11    zmod_zminus_zminus ~> mod_minus_minus
     2.1 --- a/src/HOL/Divides.thy	Tue Mar 27 16:04:51 2012 +0200
     2.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 19:21:05 2012 +0200
     2.3 @@ -1436,12 +1436,6 @@
     2.4  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
     2.5    by (fact mod_div_equality2 [symmetric])
     2.6  
     2.7 -lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"
     2.8 -  by (fact div_mod_equality2)
     2.9 -
    2.10 -lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
    2.11 -  by (fact div_mod_equality)
    2.12 -
    2.13  text {* Tool setup *}
    2.14  
    2.15  (* FIXME: Theorem list add_0s doesn't exist, because Numeral0 has gone. *)
    2.16 @@ -1456,7 +1450,7 @@
    2.17    val mk_sum = Arith_Data.mk_sum HOLogic.intT;
    2.18    val dest_sum = Arith_Data.dest_sum;
    2.19  
    2.20 -  val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
    2.21 +  val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
    2.22  
    2.23    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
    2.24      (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
     3.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 16:04:51 2012 +0200
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 19:21:05 2012 +0200
     3.3 @@ -53,7 +53,7 @@
     3.4  declare div_by_0[algebra]
     3.5  declare mod_by_0[algebra]
     3.6  declare zmod_zdiv_equality[symmetric,algebra]
     3.7 -declare zdiv_zmod_equality[symmetric, algebra]
     3.8 +declare div_mod_equality2[symmetric, algebra]
     3.9  declare div_minus_minus[algebra]
    3.10  declare mod_minus_minus[algebra]
    3.11  declare div_minus_right[algebra]
     4.1 --- a/src/HOL/Library/Float.thy	Tue Mar 27 16:04:51 2012 +0200
     4.2 +++ b/src/HOL/Library/Float.thy	Tue Mar 27 19:21:05 2012 +0200
     4.3 @@ -488,7 +488,7 @@
     4.4          hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
     4.5          thus ?thesis by auto
     4.6        qed
     4.7 -      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
     4.8 +      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
     4.9        also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto)
    4.10        also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto
    4.11        finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" .
    4.12 @@ -1122,7 +1122,7 @@
    4.13      show ?thesis
    4.14      proof (cases "m mod ?p = 0")
    4.15        case True
    4.16 -      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] .
    4.17 +      have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using mod_div_equality [symmetric] .
    4.18        have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
    4.19          by (auto simp add: pow2_add `0 < ?d` pow_d)
    4.20        thus ?thesis
    4.21 @@ -1130,7 +1130,7 @@
    4.22          by auto
    4.23      next
    4.24        case False
    4.25 -      have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    4.26 +      have "m = m div ?p * ?p + m mod ?p" unfolding mod_div_equality ..
    4.27        also have "\<dots> \<le> (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])
    4.28        finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
    4.29          unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
    4.30 @@ -1156,7 +1156,7 @@
    4.31      case True
    4.32      hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
    4.33      have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    4.34 -    also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    4.35 +    also have "\<dots> \<le> m" unfolding mod_div_equality ..
    4.36      finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
    4.37        unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
    4.38        by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
     5.1 --- a/src/HOL/Presburger.thy	Tue Mar 27 16:04:51 2012 +0200
     5.2 +++ b/src/HOL/Presburger.thy	Tue Mar 27 19:21:05 2012 +0200
     5.3 @@ -405,8 +405,8 @@
     5.4  declare mod_div_equality[presburger]
     5.5  declare mod_mult_self1[presburger]
     5.6  declare mod_mult_self2[presburger]
     5.7 -declare zdiv_zmod_equality2[presburger]
     5.8 -declare zdiv_zmod_equality[presburger]
     5.9 +declare div_mod_equality[presburger]
    5.10 +declare div_mod_equality2[presburger]
    5.11  declare mod2_Suc_Suc[presburger]
    5.12  lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
    5.13  by simp_all