# HG changeset patch # User nipkow # Date 1234892897 -3600 # Node ID cdf12a1cb96389079a11ca3e8b699403957565fc # Parent 0a51765d2084067b97deb094ce10881988d52c55 Cleaned up IntDiv and removed subsumed lemmas. diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Algebra/IntRing.thy Tue Feb 17 18:48:17 2009 +0100 @@ -407,7 +407,7 @@ hence "b mod m = (x * m + a) mod m" by simp also - have "\ = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq) + have "\ = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq) also have "\ = a mod m" by simp finally diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Feb 17 18:48:17 2009 +0100 @@ -30,7 +30,7 @@ val nat_mod_add_eq = @{thm mod_add1_eq} RS sym; val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym; val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym; -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym; +val int_mod_add_eq = @{thm mod_add_eq} RS sym; val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym; val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym; val nat_div_add_eq = @{thm div_add1_eq} RS sym; diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Feb 17 18:48:17 2009 +0100 @@ -34,7 +34,7 @@ val nat_mod_add_eq = @{thm mod_add1_eq} RS sym; val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym; val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym; -val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym; +val int_mod_add_eq = @{thm mod_add_eq} RS sym; val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym; val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym; val nat_div_add_eq = @{thm div_add1_eq} RS sym; diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Feb 17 18:48:17 2009 +0100 @@ -49,7 +49,7 @@ val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym; val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym; val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym; -val int_mod_add_eq = @{thm "zmod_zadd1_eq"} RS sym; +val int_mod_add_eq = @{thm "mod_add_eq"} RS sym; val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym; val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym; val nat_div_add_eq = @{thm "div_add1_eq"} RS sym; diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Divides.thy Tue Feb 17 18:48:17 2009 +0100 @@ -173,7 +173,7 @@ qed lemma dvd_imp_mod_0: "a dvd b \ b mod a = 0" -by (unfold dvd_def, auto) +by (rule dvd_eq_mod_eq_0[THEN iffD1]) lemma dvd_div_mult_self: "a dvd b \ (b div a) * a = b" by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0) diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/IntDiv.thy Tue Feb 17 18:48:17 2009 +0100 @@ -451,9 +451,6 @@ lemma zmod_zero [simp]: "(0::int) mod b = 0" by (simp add: mod_def divmod_def) -lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1" -by (simp add: div_def divmod_def) - lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1" by (simp add: mod_def divmod_def) @@ -729,18 +726,6 @@ apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod]) done -lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c" -apply (rule trans) -apply (rule_tac s = "b*a mod c" in trans) -apply (rule_tac [2] zmod_zmult1_eq) -apply (simp_all add: mult_commute) -done - -lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c" -apply (rule zmod_zmult1_eq' [THEN trans]) -apply (rule zmod_zmult1_eq) -done - lemma zdiv_zmult_self1 [simp]: "b \ (0::int) ==> (a*b) div b = a" by (simp add: zdiv_zmult1_eq) @@ -749,11 +734,6 @@ apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial) done -lemma zmod_zmod_trivial: "(a mod b) mod b = a mod (b::int)" -apply (case_tac "b = 0", simp) -apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial) -done - text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *} lemma zadd1_lemma: @@ -768,11 +748,6 @@ apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_div) done -lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c" -apply (case_tac "c = 0", simp) -apply (blast intro: zadd1_lemma [OF divmod_rel_div_mod divmod_rel_div_mod] divmod_rel_mod) -done - instance int :: ring_div proof fix a b c :: int @@ -971,7 +946,7 @@ P(n div k :: int)(n mod k) = (\i j. 0\j & j P i j)" apply (rule iffI, clarify) apply (erule_tac P="P ?x ?y" in rev_mp) - apply (subst zmod_zadd1_eq) + apply (subst mod_add_eq) apply (subst zdiv_zadd1_eq) apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial) txt{*converse direction*} @@ -984,7 +959,7 @@ P(n div k :: int)(n mod k) = (\i j. k0 & n = k*i + j --> P i j)" apply (rule iffI, clarify) apply (erule_tac P="P ?x ?y" in rev_mp) - apply (subst zmod_zadd1_eq) + apply (subst mod_add_eq) apply (subst zdiv_zadd1_eq) apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial) txt{*converse direction*} @@ -1057,11 +1032,6 @@ simp) done -(*Not clear why this must be proved separately; probably number_of causes - simplification problems*) -lemma not_0_le_lemma: "~ 0 \ x ==> x \ (0::int)" -by auto - lemma zdiv_number_of_Bit0 [simp]: "number_of (Int.Bit0 v) div number_of (Int.Bit0 w) = number_of v div (number_of w :: int)" @@ -1088,7 +1058,7 @@ apply (rule_tac [2] mult_left_mono) apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq pos_mod_bound) -apply (subst zmod_zadd1_eq) +apply (subst mod_add_eq) apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial) apply (rule mod_pos_pos_trivial) apply (auto simp add: mod_pos_pos_trivial ring_distribs) @@ -1111,7 +1081,7 @@ (2::int) * (number_of v mod number_of w)" apply (simp only: number_of_eq numeral_simps) apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 - not_0_le_lemma neg_zmod_mult_2 add_ac) + neg_zmod_mult_2 add_ac) done lemma zmod_number_of_Bit1 [simp]: @@ -1121,7 +1091,7 @@ else 2 * ((number_of v + (1::int)) mod number_of w) - 1)" apply (simp only: number_of_eq numeral_simps) apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 - not_0_le_lemma neg_zmod_mult_2 add_ac) + neg_zmod_mult_2 add_ac) done @@ -1131,7 +1101,7 @@ apply (subgoal_tac "a div b \ -1", force) apply (rule order_trans) apply (rule_tac a' = "-1" in zdiv_mono1) -apply (auto simp add: zdiv_minus1) +apply (auto simp add: div_eq_minus1) done lemma div_nonneg_neg_le0: "[| (0::int) \ a; b < 0 |] ==> a div b \ 0" @@ -1379,7 +1349,7 @@ apply (induct "y", auto) apply (rule zmod_zmult1_eq [THEN trans]) apply (simp (no_asm_simp)) -apply (rule zmod_zmult_distrib [symmetric]) +apply (rule mod_mult_eq [symmetric]) done lemma zdiv_int: "int (a div b) = (int a) div (int b)" @@ -1420,7 +1390,7 @@ IntDiv.zmod_zadd_left_eq [symmetric] IntDiv.zmod_zadd_right_eq [symmetric] IntDiv.zmod_zmult1_eq [symmetric] - IntDiv.zmod_zmult1_eq' [symmetric] + mod_mult_left_eq [symmetric] IntDiv.zpower_zmod zminus_zmod zdiff_zmod_left zdiff_zmod_right diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/NumberTheory/Chinese.thy --- a/src/HOL/NumberTheory/Chinese.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/NumberTheory/Chinese.thy Tue Feb 17 18:48:17 2009 +0100 @@ -101,7 +101,7 @@ apply (induct l) apply auto apply (rule trans) - apply (rule zmod_zadd1_eq) + apply (rule mod_add_eq) apply simp apply (rule zmod_zadd_right_eq [symmetric]) done @@ -237,10 +237,10 @@ apply (unfold lincong_sol_def) apply safe apply (tactic {* stac (thm "zcong_zmod") 3 *}) - apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *}) + apply (tactic {* stac (thm "mod_mult_eq") 3 *}) apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) apply (tactic {* stac (thm "x_sol_lin") 5 *}) - apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) + apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *}) apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) apply (subgoal_tac [7] "0 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/NumberTheory/IntPrimes.thy Tue Feb 17 18:48:17 2009 +0100 @@ -88,7 +88,7 @@ lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k) n = zgcd m n" apply (rule zgcd_eq [THEN trans]) - apply (simp add: zmod_zadd1_eq) + apply (simp add: mod_add_eq) apply (rule zgcd_eq [symmetric]) done diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/NumberTheory/Residues.thy --- a/src/HOL/NumberTheory/Residues.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/NumberTheory/Residues.thy Tue Feb 17 18:48:17 2009 +0100 @@ -53,7 +53,7 @@ lemma StandardRes_prop4: "2 < m ==> [StandardRes m x * StandardRes m y = (x * y)] (mod m)" by (auto simp add: StandardRes_def zcong_zmod_eq - zmod_zmult_distrib [of x y m]) + mod_mult_eq [of x y m]) lemma StandardRes_lbound: "0 < p ==> 0 \ StandardRes p x" by (auto simp add: StandardRes_def pos_mod_sign) diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Tools/Qelim/presburger.ML Tue Feb 17 18:48:17 2009 +0100 @@ -124,7 +124,7 @@ @ map (symmetric o mk_meta_eq) [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, - @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, + @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"}, @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Word/Num_Lemmas.thy Tue Feb 17 18:48:17 2009 +0100 @@ -121,8 +121,8 @@ lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c" apply (unfold diff_int_def) - apply (rule trans [OF _ zmod_zadd1_eq [symmetric]]) - apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric]) + apply (rule trans [OF _ mod_add_eq [symmetric]]) + apply (simp add: zmod_uminus mod_add_eq [symmetric]) done lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c" @@ -162,8 +162,8 @@ lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric], THEN mod_plus_right [THEN iffD2], standard, simplified] -lemmas push_mods' = zmod_zadd1_eq [standard] - zmod_zmult_distrib [standard] zmod_zsub_distrib [standard] +lemmas push_mods' = mod_add_eq [standard] + mod_mult_eq [standard] zmod_zsub_distrib [standard] zmod_uminus [symmetric, standard] lemmas push_mods = push_mods' [THEN eq_reflection, standard] diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Word/WordGenLib.thy --- a/src/HOL/Word/WordGenLib.thy Mon Feb 16 19:35:52 2009 -0800 +++ b/src/HOL/Word/WordGenLib.thy Tue Feb 17 18:48:17 2009 +0100 @@ -293,9 +293,9 @@ shows "(x + y) mod b = z' mod b'" proof - from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'" - by (simp add: zmod_zadd1_eq[symmetric]) + by (simp add: mod_add_eq[symmetric]) also have "\ = (x' + y') mod b'" - by (simp add: zmod_zadd1_eq[symmetric]) + by (simp add: mod_add_eq[symmetric]) finally show ?thesis by (simp add: 4) qed