Removed redundant lemmas
authornipkow
Fri Feb 20 23:46:03 2009 +0100 (2009-02-20)
changeset 30031bd786c37af84
parent 30030 00d04a562df1
child 30033 e54d4d41fe8f
child 30034 60f64f112174
Removed redundant lemmas
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Groebner_Basis.thy
src/HOL/IntDiv.thy
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/int_factor_simprocs.ML
src/HOL/Word/Num_Lemmas.thy
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Feb 20 21:29:34 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Feb 20 23:46:03 2009 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  				  @{thm mod_self}, @{thm "zmod_self"},
     1.5  				  @{thm mod_by_0}, @{thm div_by_0},
     1.6  				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
     1.7 -				  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.8 +				  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.9  				  Suc_plus1]
    1.10  			addsimps @{thms add_ac}
    1.11  			addsimprocs [cancel_div_mod_proc]
     2.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Feb 20 21:29:34 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri Feb 20 23:46:03 2009 +0100
     2.3 @@ -99,7 +99,7 @@
     2.4                          addsimps [refl,nat_mod_add_eq, 
     2.5                                    @{thm "mod_self"}, @{thm "zmod_self"},
     2.6                                    @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
     2.7 -                                  @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, @{thm "mod_1"},
     2.8 +                                  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     2.9                                    @{thm "Suc_plus1"}]
    2.10                          addsimps @{thms add_ac}
    2.11                          addsimprocs [cancel_div_mod_proc]
     3.1 --- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 21:29:34 2009 +0100
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 23:46:03 2009 +0100
     3.3 @@ -448,8 +448,8 @@
     3.4  declare zmod_zminus2[algebra]
     3.5  declare zdiv_zero[algebra]
     3.6  declare zmod_zero[algebra]
     3.7 -declare zmod_1[algebra]
     3.8 -declare zdiv_1[algebra]
     3.9 +declare mod_by_1[algebra]
    3.10 +declare div_by_1[algebra]
    3.11  declare zmod_minus1_right[algebra]
    3.12  declare zdiv_minus1_right[algebra]
    3.13  declare mod_div_trivial[algebra]
     4.1 --- a/src/HOL/IntDiv.thy	Fri Feb 20 21:29:34 2009 +0100
     4.2 +++ b/src/HOL/IntDiv.thy	Fri Feb 20 23:46:03 2009 +0100
     4.3 @@ -547,34 +547,6 @@
     4.4  simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
     4.5    {* K (divmod_proc (@{thm divmod_rel_mod_eq})) *}
     4.6  
     4.7 -(* The following 8 lemmas are made unnecessary by the above simprocs: *)
     4.8 -
     4.9 -lemmas div_pos_pos_number_of =
    4.10 -    div_pos_pos [of "number_of v" "number_of w", standard]
    4.11 -
    4.12 -lemmas div_neg_pos_number_of =
    4.13 -    div_neg_pos [of "number_of v" "number_of w", standard]
    4.14 -
    4.15 -lemmas div_pos_neg_number_of =
    4.16 -    div_pos_neg [of "number_of v" "number_of w", standard]
    4.17 -
    4.18 -lemmas div_neg_neg_number_of =
    4.19 -    div_neg_neg [of "number_of v" "number_of w", standard]
    4.20 -
    4.21 -
    4.22 -lemmas mod_pos_pos_number_of =
    4.23 -    mod_pos_pos [of "number_of v" "number_of w", standard]
    4.24 -
    4.25 -lemmas mod_neg_pos_number_of =
    4.26 -    mod_neg_pos [of "number_of v" "number_of w", standard]
    4.27 -
    4.28 -lemmas mod_pos_neg_number_of =
    4.29 -    mod_pos_neg [of "number_of v" "number_of w", standard]
    4.30 -
    4.31 -lemmas mod_neg_neg_number_of =
    4.32 -    mod_neg_neg [of "number_of v" "number_of w", standard]
    4.33 -
    4.34 -
    4.35  lemmas posDivAlg_eqn_number_of [simp] =
    4.36      posDivAlg_eqn [of "number_of v" "number_of w", standard]
    4.37  
    4.38 @@ -584,15 +556,6 @@
    4.39  
    4.40  text{*Special-case simplification *}
    4.41  
    4.42 -lemma zmod_1 [simp]: "a mod (1::int) = 0"
    4.43 -apply (cut_tac a = a and b = 1 in pos_mod_sign)
    4.44 -apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
    4.45 -apply (auto simp del:pos_mod_bound pos_mod_sign)
    4.46 -done
    4.47 -
    4.48 -lemma zdiv_1 [simp]: "a div (1::int) = a"
    4.49 -by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
    4.50 -
    4.51  lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
    4.52  apply (cut_tac a = a and b = "-1" in neg_mod_sign)
    4.53  apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
     5.1 --- a/src/HOL/Presburger.thy	Fri Feb 20 21:29:34 2009 +0100
     5.2 +++ b/src/HOL/Presburger.thy	Fri Feb 20 23:46:03 2009 +0100
     5.3 @@ -412,14 +412,10 @@
     5.4    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
     5.5    by (rule eq_number_of_eq)
     5.6  
     5.7 -lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
     5.8 -unfolding dvd_eq_mod_eq_0[symmetric] ..
     5.9 -
    5.10 -lemma zmod_eq0_zdvd_iff[presburger]: "(m::int) mod n = 0 \<longleftrightarrow> n dvd m"
    5.11 -unfolding zdvd_iff_zmod_eq_0[symmetric] ..
    5.12 +declare dvd_eq_mod_eq_0[symmetric, presburger]
    5.13  declare mod_1[presburger] 
    5.14  declare mod_0[presburger]
    5.15 -declare zmod_1[presburger]
    5.16 +declare mod_by_1[presburger]
    5.17  declare zmod_zero[presburger]
    5.18  declare zmod_self[presburger]
    5.19  declare mod_self[presburger]
     6.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Feb 20 21:29:34 2009 +0100
     6.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Feb 20 23:46:03 2009 +0100
     6.3 @@ -129,7 +129,7 @@
     6.4    @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
     6.5       @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
     6.6       @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
     6.7 -     @{thm "div_0"}, @{thm "mod_0"}, @{thm "zdiv_1"}, @{thm "zmod_1"}, @{thm "div_1"}, 
     6.8 +     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
     6.9       @{thm "mod_1"}, @{thm "Suc_plus1"}]
    6.10    @ @{thms add_ac}
    6.11   addsimprocs [cancel_div_mod_proc]
     7.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Fri Feb 20 21:29:34 2009 +0100
     7.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Fri Feb 20 23:46:03 2009 +0100
     7.3 @@ -216,7 +216,7 @@
     7.4  
     7.5  (** Final simplification for the CancelFactor simprocs **)
     7.6  val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
     7.7 -  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}];
     7.8 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
     7.9  
    7.10  fun cancel_simplify_meta_eq cancel_th ss th =
    7.11      simplify_one ss (([th, cancel_th]) MRS trans);
     8.1 --- a/src/HOL/Word/Num_Lemmas.thy	Fri Feb 20 21:29:34 2009 +0100
     8.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Fri Feb 20 23:46:03 2009 +0100
     8.3 @@ -95,7 +95,7 @@
     8.4  lemma z1pdiv2:
     8.5    "(2 * b + 1) div 2 = (b::int)" by arith
     8.6  
     8.7 -lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,
     8.8 +lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
     8.9    simplified int_one_le_iff_zero_less, simplified, standard]
    8.10    
    8.11  lemma axxbyy: