# HG changeset patch # User nipkow # Date 1235169963 -3600 # Node ID bd786c37af84da6df4795e1e9cb9b1b1679ed081 # Parent 00d04a562df1a3784716263cdf2e9eaa6a9105e5 Removed redundant lemmas diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 23:46:03 2009 +0100 @@ -77,7 +77,7 @@ @{thm mod_self}, @{thm "zmod_self"}, @{thm mod_by_0}, @{thm div_by_0}, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"}, - @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, + @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, Suc_plus1] addsimps @{thms add_ac} addsimprocs [cancel_div_mod_proc] diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 23:46:03 2009 +0100 @@ -99,7 +99,7 @@ addsimps [refl,nat_mod_add_eq, @{thm "mod_self"}, @{thm "zmod_self"}, @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"}, - @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"}, + @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, @{thm "Suc_plus1"}] addsimps @{thms add_ac} addsimprocs [cancel_div_mod_proc] diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Fri Feb 20 23:46:03 2009 +0100 @@ -448,8 +448,8 @@ declare zmod_zminus2[algebra] declare zdiv_zero[algebra] declare zmod_zero[algebra] -declare zmod_1[algebra] -declare zdiv_1[algebra] +declare mod_by_1[algebra] +declare div_by_1[algebra] declare zmod_minus1_right[algebra] declare zdiv_minus1_right[algebra] declare mod_div_trivial[algebra] diff -r 00d04a562df1 -r bd786c37af84 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/IntDiv.thy Fri Feb 20 23:46:03 2009 +0100 @@ -547,34 +547,6 @@ simproc_setup binary_int_mod ("number_of m mod number_of n :: int") = {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *} -(* The following 8 lemmas are made unnecessary by the above simprocs: *) - -lemmas div_pos_pos_number_of = - div_pos_pos [of "number_of v" "number_of w", standard] - -lemmas div_neg_pos_number_of = - div_neg_pos [of "number_of v" "number_of w", standard] - -lemmas div_pos_neg_number_of = - div_pos_neg [of "number_of v" "number_of w", standard] - -lemmas div_neg_neg_number_of = - div_neg_neg [of "number_of v" "number_of w", standard] - - -lemmas mod_pos_pos_number_of = - mod_pos_pos [of "number_of v" "number_of w", standard] - -lemmas mod_neg_pos_number_of = - mod_neg_pos [of "number_of v" "number_of w", standard] - -lemmas mod_pos_neg_number_of = - mod_pos_neg [of "number_of v" "number_of w", standard] - -lemmas mod_neg_neg_number_of = - mod_neg_neg [of "number_of v" "number_of w", standard] - - lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w", standard] @@ -584,15 +556,6 @@ text{*Special-case simplification *} -lemma zmod_1 [simp]: "a mod (1::int) = 0" -apply (cut_tac a = a and b = 1 in pos_mod_sign) -apply (cut_tac [2] a = a and b = 1 in pos_mod_bound) -apply (auto simp del:pos_mod_bound pos_mod_sign) -done - -lemma zdiv_1 [simp]: "a div (1::int) = a" -by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto) - lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0" apply (cut_tac a = a and b = "-1" in neg_mod_sign) apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound) diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Presburger.thy Fri Feb 20 23:46:03 2009 +0100 @@ -412,14 +412,10 @@ "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" by (rule eq_number_of_eq) -lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \ n dvd m" -unfolding dvd_eq_mod_eq_0[symmetric] .. - -lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \ n dvd m" -unfolding zdvd_iff_zmod_eq_0[symmetric] .. +declare dvd_eq_mod_eq_0[symmetric, presburger] declare mod_1[presburger] declare mod_0[presburger] -declare zmod_1[presburger] +declare mod_by_1[presburger] declare zmod_zero[presburger] declare zmod_self[presburger] declare mod_self[presburger] diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 23:46:03 2009 +0100 @@ -129,7 +129,7 @@ @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, - @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, + @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"}, @{thm "Suc_plus1"}] @ @{thms add_ac} addsimprocs [cancel_div_mod_proc] diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Tools/int_factor_simprocs.ML --- a/src/HOL/Tools/int_factor_simprocs.ML Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Tools/int_factor_simprocs.ML Fri Feb 20 23:46:03 2009 +0100 @@ -216,7 +216,7 @@ (** Final simplification for the CancelFactor simprocs **) val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq - [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}]; + [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; fun cancel_simplify_meta_eq cancel_th ss th = simplify_one ss (([th, cancel_th]) MRS trans); diff -r 00d04a562df1 -r bd786c37af84 src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 21:29:34 2009 +0100 +++ b/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 23:46:03 2009 +0100 @@ -95,7 +95,7 @@ lemma z1pdiv2: "(2 * b + 1) div 2 = (b::int)" by arith -lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2, +lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2, simplified int_one_le_iff_zero_less, simplified, standard] lemma axxbyy: