# HG changeset patch # User nipkow # Date 1235206706 -3600 # Node ID 60f64f112174239a07de1344bc02abdd0302709b # Parent bd786c37af84da6df4795e1e9cb9b1b1679ed081 removed redundant thms diff -r bd786c37af84 -r 60f64f112174 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Feb 21 09:58:26 2009 +0100 @@ -28,11 +28,9 @@ val imp_le_cong = @{thm imp_le_cong}; val conj_le_cong = @{thm conj_le_cong}; 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 mod_add_left_eq = @{thm mod_add_left_eq} RS sym; +val mod_add_right_eq = @{thm mod_add_right_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; val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; @@ -70,9 +68,8 @@ val (t,np,nh) = prepare_for_linz q g (* Some simpsets for dealing with mod div abs and nat*) val mod_div_simpset = HOL_basic_ss - addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, - nat_mod_add_right_eq, int_mod_add_eq, - int_mod_add_right_eq, int_mod_add_left_eq, + addsimps [refl,nat_mod_add_eq, mod_add_left_eq, + mod_add_right_eq, int_mod_add_eq, nat_div_add_eq, int_div_add_eq, @{thm mod_self}, @{thm "zmod_self"}, @{thm mod_by_0}, @{thm div_by_0}, diff -r bd786c37af84 -r 60f64f112174 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat Feb 21 09:58:26 2009 +0100 @@ -32,11 +32,9 @@ val imp_le_cong = @{thm imp_le_cong}; val conj_le_cong = @{thm conj_le_cong}; 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 mod_add_left_eq = @{thm mod_add_left_eq} RS sym; +val mod_add_right_eq = @{thm mod_add_right_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; val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym; val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2; diff -r bd786c37af84 -r 60f64f112174 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Feb 21 09:58:26 2009 +0100 @@ -47,11 +47,9 @@ val imp_le_cong = @{thm "imp_le_cong"}; val conj_le_cong = @{thm "conj_le_cong"}; 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 mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym; +val mod_add_right_eq = @{thm "mod_add_right_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; val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym; val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2; diff -r bd786c37af84 -r 60f64f112174 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Groebner_Basis.thy Sat Feb 21 09:58:26 2009 +0100 @@ -454,8 +454,8 @@ declare zdiv_minus1_right[algebra] declare mod_div_trivial[algebra] declare mod_mod_trivial[algebra] -declare zmod_zmult_self1[algebra] -declare zmod_zmult_self2[algebra] +declare mod_mult_self2_is_0[algebra] +declare mod_mult_self1_is_0[algebra] declare zmod_eq_0_iff[algebra] declare zdvd_0_left[algebra] declare zdvd1_eq[algebra] diff -r bd786c37af84 -r 60f64f112174 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/IntDiv.thy Sat Feb 21 09:58:26 2009 +0100 @@ -747,41 +747,12 @@ show ?thesis by simp qed -lemma zdiv_zadd_self1: "a \ (0::int) ==> (a+b) div a = b div a + 1" -by (rule div_add_self1) (* already declared [simp] *) - -lemma zdiv_zadd_self2: "a \ (0::int) ==> (b+a) div a = b div a + 1" -by (rule div_add_self2) (* already declared [simp] *) - -lemma zdiv_zmult_self2: "b \ (0::int) ==> (b*a) div b = a" -by (rule div_mult_self1_is_id) (* already declared [simp] *) - -lemma zmod_zmult_self1: "(a*b) mod b = (0::int)" -by (rule mod_mult_self2_is_0) (* already declared [simp] *) - -lemma zmod_zmult_self2: "(b*a) mod b = (0::int)" -by (rule mod_mult_self1_is_0) (* already declared [simp] *) - lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)" by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def) (* REVISIT: should this be generalized to all semiring_div types? *) lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1] -lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c" -by (rule mod_add_left_eq) - -lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c" -by (rule mod_add_right_eq) - -lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)" -by (rule mod_add_self1) (* already declared [simp] *) - -lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)" -by (rule mod_add_self2) (* already declared [simp] *) - -lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)" -by (rule mod_diff_eq) subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *} @@ -896,9 +867,6 @@ apply (auto simp add: mult_commute) done -lemma zmod_zmod_cancel: "n dvd m \ (k::int) mod m mod n = k mod n" -by (rule mod_mod_cancel) - subsection {*Splitting Rules for div and mod*} @@ -1350,8 +1318,8 @@ by (rule mod_diff_right_eq [symmetric]) lemmas zmod_simps = - IntDiv.zmod_zadd_left_eq [symmetric] - IntDiv.zmod_zadd_right_eq [symmetric] + mod_add_left_eq [symmetric] + mod_add_right_eq [symmetric] IntDiv.zmod_zmult1_eq [symmetric] mod_mult_left_eq [symmetric] IntDiv.zpower_zmod @@ -1426,14 +1394,14 @@ assume H: "x mod n = y mod n" hence "x mod n - y mod n = 0" by simp hence "(x mod n - y mod n) mod n = 0" by simp - hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric]) + hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric]) thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0) next assume H: "n dvd x - y" then obtain k where k: "x-y = n*k" unfolding dvd_def by blast hence "x = n*k + y" by simp hence "x mod n = (n*k + y) mod n" by simp - thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq) + thus "x mod n = y mod n" by (simp add: mod_add_left_eq) qed lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \ x" diff -r bd786c37af84 -r 60f64f112174 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Library/Float.thy Sat Feb 21 09:58:26 2009 +0100 @@ -795,7 +795,7 @@ have "x \ y" proof (rule ccontr) assume "\ x \ y" hence "x = y" by auto - have "?X mod y = 0" unfolding `x = y` using zmod_zmult_self2 by auto + have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto thus False using False by auto qed hence "x < y" using `x \ y` by auto diff -r bd786c37af84 -r 60f64f112174 src/HOL/NumberTheory/Chinese.thy --- a/src/HOL/NumberTheory/Chinese.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/NumberTheory/Chinese.thy Sat Feb 21 09:58:26 2009 +0100 @@ -103,7 +103,7 @@ apply (rule trans) apply (rule mod_add_eq) apply simp - apply (rule zmod_zadd_right_eq [symmetric]) + apply (rule mod_add_right_eq [symmetric]) done lemma funsum_zero [rule_format (no_asm)]: @@ -238,20 +238,20 @@ apply safe apply (tactic {* stac (thm "zcong_zmod") 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 "mod_mult_eq" RS sym) 7 *}) - apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) - apply (subgoal_tac [7] + apply (tactic {* stac (thm "mod_mod_cancel") 3 *}) + apply (tactic {* stac (thm "x_sol_lin") 4 *}) + apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *}) + apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *}) + apply (subgoal_tac [6] "0 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i \ [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") - prefer 7 + prefer 6 apply (simp add: zmult_ac) apply (unfold xilin_sol_def) - apply (tactic {* asm_simp_tac @{simpset} 7 *}) - apply (rule_tac [7] ex1_implies_ex [THEN someI_ex]) - apply (rule_tac [7] unique_xi_sol) - apply (rule_tac [4] funprod_zdvd) + apply (tactic {* asm_simp_tac @{simpset} 6 *}) + apply (rule_tac [6] ex1_implies_ex [THEN someI_ex]) + apply (rule_tac [6] unique_xi_sol) + apply (rule_tac [3] funprod_zdvd) apply (unfold m_cond_def) apply (rule funprod_pos [THEN pos_mod_sign]) apply (rule_tac [2] funprod_pos [THEN pos_mod_bound]) diff -r bd786c37af84 -r 60f64f112174 src/HOL/NumberTheory/Gauss.thy --- a/src/HOL/NumberTheory/Gauss.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/NumberTheory/Gauss.thy Sat Feb 21 09:58:26 2009 +0100 @@ -64,14 +64,14 @@ qed lemma p_eq: "p = (2 * (p - 1) div 2) + 1" - using zdiv_zmult_self2 [of 2 "p - 1"] by auto + using div_mult_self1_is_id [of 2 "p - 1"] by auto lemma (in -) zodd_imp_zdiv_eq: "x \ zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)" apply (frule odd_minus_one_even) apply (simp add: zEven_def) apply (subgoal_tac "2 \ 0") - apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2) + apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id) apply (auto simp add: even_div_2_prop2) done diff -r bd786c37af84 -r 60f64f112174 src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/NumberTheory/IntPrimes.thy Sat Feb 21 09:58:26 2009 +0100 @@ -217,7 +217,7 @@ a < m ==> 0 \ b ==> b < m ==> [a = b] (mod m) ==> a = b" apply (unfold zcong_def dvd_def, auto) apply (drule_tac f = "\z. z mod m" in arg_cong) - apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff zmod_zadd_right_eq) + apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq) done lemma zcong_square_zless: @@ -237,7 +237,7 @@ lemma zcong_zless_0: "0 \ a ==> a < m ==> [a = 0] (mod m) ==> a = 0" apply (unfold zcong_def dvd_def, auto) - apply (metis div_pos_pos_trivial linorder_not_less zdiv_zmult_self2 zle_refl zle_trans) + apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id zle_refl zle_trans) done lemma zcong_zless_unique: @@ -302,7 +302,7 @@ lemma zmod_zdvd_zmod: "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" - by (rule zmod_zmod_cancel) + by (rule mod_mod_cancel) subsection {* Extended GCD *} diff -r bd786c37af84 -r 60f64f112174 src/HOL/NumberTheory/Quadratic_Reciprocity.thy --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Sat Feb 21 09:58:26 2009 +0100 @@ -322,7 +322,7 @@ by (rule zdiv_mono1) (insert p_g_2, auto) then show "b \ (q * a) div p" apply (subgoal_tac "p \ 0") - apply (frule zdiv_zmult_self2, force) + apply (frule div_mult_self1_is_id, force) apply (insert p_g_2, auto) done qed @@ -356,7 +356,7 @@ by (rule zdiv_mono1) (insert q_g_2, auto) then show "a \ (p * b) div q" apply (subgoal_tac "q \ 0") - apply (frule zdiv_zmult_self2, force) + apply (frule div_mult_self1_is_id, force) apply (insert q_g_2, auto) done qed diff -r bd786c37af84 -r 60f64f112174 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Sat Feb 21 09:58:26 2009 +0100 @@ -124,8 +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 "mod_add_eq"}, @{thm "zmod_zadd_left_eq"}, - @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] + @{thm "mod_add_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, @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, diff -r bd786c37af84 -r 60f64f112174 src/HOL/Word/BinGeneral.thy --- a/src/HOL/Word/BinGeneral.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Word/BinGeneral.thy Sat Feb 21 09:58:26 2009 +0100 @@ -433,7 +433,7 @@ "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)" apply (induct n) apply clarsimp - apply (subst zmod_zadd_left_eq) + apply (subst mod_add_left_eq) apply (simp add: bin_last_mod) apply (simp add: number_of_eq) apply clarsimp @@ -767,23 +767,23 @@ lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard] lemmas brdmod1s' [symmetric] = - zmod_zadd_left_eq zmod_zadd_right_eq + mod_add_left_eq mod_add_right_eq zmod_zsub_left_eq zmod_zsub_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev lemmas brdmods' [symmetric] = zpower_zmod' [symmetric] - trans [OF zmod_zadd_left_eq zmod_zadd_right_eq] + trans [OF mod_add_left_eq mod_add_right_eq] trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] zmod_uminus' [symmetric] - zmod_zadd_left_eq [where b = "1"] + mod_add_left_eq [where b = "1::int"] zmod_zsub_left_eq [where b = "1"] lemmas bintr_arith1s = - brdmod1s' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard] + brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard] lemmas bintr_ariths = - brdmods' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard] + brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard] lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard] diff -r bd786c37af84 -r 60f64f112174 src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Word/Num_Lemmas.thy Sat Feb 21 09:58:26 2009 +0100 @@ -127,12 +127,12 @@ lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c" apply (unfold diff_int_def) - apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]]) - apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric]) + apply (rule trans [OF _ mod_add_right_eq [symmetric]]) + apply (simp add : zmod_uminus mod_add_right_eq [symmetric]) done lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c" - by (rule zmod_zadd_left_eq [where b = "- b", simplified diff_int_def [symmetric]]) + by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]]) lemma zmod_zsub_self [simp]: "((b :: int) - a) mod a = b mod a" @@ -146,8 +146,8 @@ done lemmas rdmods [symmetric] = zmod_uminus [symmetric] - zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq - zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev + zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq + mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev lemma mod_plus_right: "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))" @@ -169,7 +169,8 @@ lemmas push_mods = push_mods' [THEN eq_reflection, standard] lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard] lemmas mod_simps = - zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection] + mod_mult_self2_is_0 [THEN eq_reflection] + mod_mult_self1_is_0 [THEN eq_reflection] mod_mod_trivial [THEN eq_reflection] lemma nat_mod_eq: diff -r bd786c37af84 -r 60f64f112174 src/HOL/Word/WordGenLib.thy --- a/src/HOL/Word/WordGenLib.thy Fri Feb 20 23:46:03 2009 +0100 +++ b/src/HOL/Word/WordGenLib.thy Sat Feb 21 09:58:26 2009 +0100 @@ -273,7 +273,7 @@ have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp show ?thesis apply (subst x) - apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2) + apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2) apply simp done qed