removed redundant thms
authornipkow
Sat Feb 21 09:58:26 2009 +0100 (2009-02-21)
changeset 3003460f64f112174
parent 30031 bd786c37af84
child 30035 7f4d475a6c50
removed redundant thms
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Groebner_Basis.thy
src/HOL/IntDiv.thy
src/HOL/Library/Float.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Word/BinGeneral.thy
src/HOL/Word/Num_Lemmas.thy
src/HOL/Word/WordGenLib.thy
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Feb 20 23:46:03 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Feb 21 09:58:26 2009 +0100
     1.3 @@ -28,11 +28,9 @@
     1.4  val imp_le_cong = @{thm imp_le_cong};
     1.5  val conj_le_cong = @{thm conj_le_cong};
     1.6  val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     1.7 -val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     1.8 -val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
     1.9 +val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    1.10 +val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    1.11  val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    1.12 -val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    1.13 -val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    1.14  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    1.15  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    1.16  
    1.17 @@ -70,9 +68,8 @@
    1.18      val (t,np,nh) = prepare_for_linz q g
    1.19      (* Some simpsets for dealing with mod div abs and nat*)
    1.20      val mod_div_simpset = HOL_basic_ss 
    1.21 -			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
    1.22 -				  nat_mod_add_right_eq, int_mod_add_eq, 
    1.23 -				  int_mod_add_right_eq, int_mod_add_left_eq,
    1.24 +			addsimps [refl,nat_mod_add_eq, mod_add_left_eq, 
    1.25 +				  mod_add_right_eq, int_mod_add_eq, 
    1.26  				  nat_div_add_eq, int_div_add_eq,
    1.27  				  @{thm mod_self}, @{thm "zmod_self"},
    1.28  				  @{thm mod_by_0}, @{thm div_by_0},
     2.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Feb 20 23:46:03 2009 +0100
     2.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sat Feb 21 09:58:26 2009 +0100
     2.3 @@ -32,11 +32,9 @@
     2.4  val imp_le_cong = @{thm imp_le_cong};
     2.5  val conj_le_cong = @{thm conj_le_cong};
     2.6  val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
     2.7 -val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     2.8 -val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
     2.9 +val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    2.10 +val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
    2.11  val int_mod_add_eq = @{thm mod_add_eq} RS sym;
    2.12 -val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
    2.13 -val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
    2.14  val nat_div_add_eq = @{thm div_add1_eq} RS sym;
    2.15  val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
    2.16  val ZDIVISION_BY_ZERO_MOD = @{thm DIVISION_BY_ZERO} RS conjunct2;
     3.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Fri Feb 20 23:46:03 2009 +0100
     3.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Feb 21 09:58:26 2009 +0100
     3.3 @@ -47,11 +47,9 @@
     3.4  val imp_le_cong = @{thm "imp_le_cong"};
     3.5  val conj_le_cong = @{thm "conj_le_cong"};
     3.6  val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
     3.7 -val nat_mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
     3.8 -val nat_mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
     3.9 +val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
    3.10 +val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
    3.11  val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
    3.12 -val int_mod_add_left_eq = @{thm "zmod_zadd_left_eq"} RS sym;
    3.13 -val int_mod_add_right_eq = @{thm "zmod_zadd_right_eq"} RS sym;
    3.14  val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
    3.15  val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
    3.16  val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
     4.1 --- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 23:46:03 2009 +0100
     4.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Feb 21 09:58:26 2009 +0100
     4.3 @@ -454,8 +454,8 @@
     4.4  declare zdiv_minus1_right[algebra]
     4.5  declare mod_div_trivial[algebra]
     4.6  declare mod_mod_trivial[algebra]
     4.7 -declare zmod_zmult_self1[algebra]
     4.8 -declare zmod_zmult_self2[algebra]
     4.9 +declare mod_mult_self2_is_0[algebra]
    4.10 +declare mod_mult_self1_is_0[algebra]
    4.11  declare zmod_eq_0_iff[algebra]
    4.12  declare zdvd_0_left[algebra]
    4.13  declare zdvd1_eq[algebra]
     5.1 --- a/src/HOL/IntDiv.thy	Fri Feb 20 23:46:03 2009 +0100
     5.2 +++ b/src/HOL/IntDiv.thy	Sat Feb 21 09:58:26 2009 +0100
     5.3 @@ -747,41 +747,12 @@
     5.4    show ?thesis by simp
     5.5  qed
     5.6  
     5.7 -lemma zdiv_zadd_self1: "a \<noteq> (0::int) ==> (a+b) div a = b div a + 1"
     5.8 -by (rule div_add_self1) (* already declared [simp] *)
     5.9 -
    5.10 -lemma zdiv_zadd_self2: "a \<noteq> (0::int) ==> (b+a) div a = b div a + 1"
    5.11 -by (rule div_add_self2) (* already declared [simp] *)
    5.12 -
    5.13 -lemma zdiv_zmult_self2: "b \<noteq> (0::int) ==> (b*a) div b = a"
    5.14 -by (rule div_mult_self1_is_id) (* already declared [simp] *)
    5.15 -
    5.16 -lemma zmod_zmult_self1: "(a*b) mod b = (0::int)"
    5.17 -by (rule mod_mult_self2_is_0) (* already declared [simp] *)
    5.18 -
    5.19 -lemma zmod_zmult_self2: "(b*a) mod b = (0::int)"
    5.20 -by (rule mod_mult_self1_is_0) (* already declared [simp] *)
    5.21 -
    5.22  lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
    5.23  by (simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
    5.24  
    5.25  (* REVISIT: should this be generalized to all semiring_div types? *)
    5.26  lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
    5.27  
    5.28 -lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
    5.29 -by (rule mod_add_left_eq)
    5.30 -
    5.31 -lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"
    5.32 -by (rule mod_add_right_eq)
    5.33 -
    5.34 -lemma zmod_zadd_self1: "(a+b) mod a = b mod (a::int)"
    5.35 -by (rule mod_add_self1) (* already declared [simp] *)
    5.36 -
    5.37 -lemma zmod_zadd_self2: "(b+a) mod a = b mod (a::int)"
    5.38 -by (rule mod_add_self2) (* already declared [simp] *)
    5.39 -
    5.40 -lemma zmod_zdiff1_eq: "(a - b) mod c = (a mod c - b mod c) mod (c::int)"
    5.41 -by (rule mod_diff_eq)
    5.42  
    5.43  subsection{*Proving  @{term "a div (b*c) = (a div b) div c"} *}
    5.44  
    5.45 @@ -896,9 +867,6 @@
    5.46  apply (auto simp add: mult_commute)
    5.47  done
    5.48  
    5.49 -lemma zmod_zmod_cancel: "n dvd m \<Longrightarrow> (k::int) mod m mod n = k mod n"
    5.50 -by (rule mod_mod_cancel)
    5.51 -
    5.52  
    5.53  subsection {*Splitting Rules for div and mod*}
    5.54  
    5.55 @@ -1350,8 +1318,8 @@
    5.56  by (rule mod_diff_right_eq [symmetric])
    5.57  
    5.58  lemmas zmod_simps =
    5.59 -  IntDiv.zmod_zadd_left_eq  [symmetric]
    5.60 -  IntDiv.zmod_zadd_right_eq [symmetric]
    5.61 +  mod_add_left_eq  [symmetric]
    5.62 +  mod_add_right_eq [symmetric]
    5.63    IntDiv.zmod_zmult1_eq     [symmetric]
    5.64    mod_mult_left_eq          [symmetric]
    5.65    IntDiv.zpower_zmod
    5.66 @@ -1426,14 +1394,14 @@
    5.67    assume H: "x mod n = y mod n"
    5.68    hence "x mod n - y mod n = 0" by simp
    5.69    hence "(x mod n - y mod n) mod n = 0" by simp 
    5.70 -  hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
    5.71 +  hence "(x - y) mod n = 0" by (simp add: mod_diff_eq[symmetric])
    5.72    thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
    5.73  next
    5.74    assume H: "n dvd x - y"
    5.75    then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
    5.76    hence "x = n*k + y" by simp
    5.77    hence "x mod n = (n*k + y) mod n" by simp
    5.78 -  thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
    5.79 +  thus "x mod n = y mod n" by (simp add: mod_add_left_eq)
    5.80  qed
    5.81  
    5.82  lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y  mod n" and xy:"y \<le> x"
     6.1 --- a/src/HOL/Library/Float.thy	Fri Feb 20 23:46:03 2009 +0100
     6.2 +++ b/src/HOL/Library/Float.thy	Sat Feb 21 09:58:26 2009 +0100
     6.3 @@ -795,7 +795,7 @@
     6.4      have "x \<noteq> y"
     6.5      proof (rule ccontr)
     6.6        assume "\<not> x \<noteq> y" hence "x = y" by auto
     6.7 -      have "?X mod y = 0" unfolding `x = y` using zmod_zmult_self2 by auto
     6.8 +      have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
     6.9        thus False using False by auto
    6.10      qed
    6.11      hence "x < y" using `x \<le> y` by auto
     7.1 --- a/src/HOL/NumberTheory/Chinese.thy	Fri Feb 20 23:46:03 2009 +0100
     7.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Sat Feb 21 09:58:26 2009 +0100
     7.3 @@ -103,7 +103,7 @@
     7.4    apply (rule trans)
     7.5     apply (rule mod_add_eq)
     7.6    apply simp
     7.7 -  apply (rule zmod_zadd_right_eq [symmetric])
     7.8 +  apply (rule mod_add_right_eq [symmetric])
     7.9    done
    7.10  
    7.11  lemma funsum_zero [rule_format (no_asm)]:
    7.12 @@ -238,20 +238,20 @@
    7.13    apply safe
    7.14      apply (tactic {* stac (thm "zcong_zmod") 3 *})
    7.15      apply (tactic {* stac (thm "mod_mult_eq") 3 *})
    7.16 -    apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
    7.17 -      apply (tactic {* stac (thm "x_sol_lin") 5 *})
    7.18 -        apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *})
    7.19 -        apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
    7.20 -        apply (subgoal_tac [7]
    7.21 +    apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
    7.22 +      apply (tactic {* stac (thm "x_sol_lin") 4 *})
    7.23 +        apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
    7.24 +        apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
    7.25 +        apply (subgoal_tac [6]
    7.26            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
    7.27            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
    7.28 -         prefer 7
    7.29 +         prefer 6
    7.30           apply (simp add: zmult_ac)
    7.31          apply (unfold xilin_sol_def)
    7.32 -        apply (tactic {* asm_simp_tac @{simpset} 7 *})
    7.33 -        apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
    7.34 -        apply (rule_tac [7] unique_xi_sol)
    7.35 -           apply (rule_tac [4] funprod_zdvd)
    7.36 +        apply (tactic {* asm_simp_tac @{simpset} 6 *})
    7.37 +        apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
    7.38 +        apply (rule_tac [6] unique_xi_sol)
    7.39 +           apply (rule_tac [3] funprod_zdvd)
    7.40              apply (unfold m_cond_def)
    7.41              apply (rule funprod_pos [THEN pos_mod_sign])
    7.42              apply (rule_tac [2] funprod_pos [THEN pos_mod_bound])
     8.1 --- a/src/HOL/NumberTheory/Gauss.thy	Fri Feb 20 23:46:03 2009 +0100
     8.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Sat Feb 21 09:58:26 2009 +0100
     8.3 @@ -64,14 +64,14 @@
     8.4  qed
     8.5  
     8.6  lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
     8.7 -  using zdiv_zmult_self2 [of 2 "p - 1"] by auto
     8.8 +  using div_mult_self1_is_id [of 2 "p - 1"] by auto
     8.9  
    8.10  
    8.11  lemma (in -) zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
    8.12    apply (frule odd_minus_one_even)
    8.13    apply (simp add: zEven_def)
    8.14    apply (subgoal_tac "2 \<noteq> 0")
    8.15 -  apply (frule_tac b = "2 :: int" and a = "x - 1" in zdiv_zmult_self2)
    8.16 +  apply (frule_tac b = "2 :: int" and a = "x - 1" in div_mult_self1_is_id)
    8.17    apply (auto simp add: even_div_2_prop2)
    8.18    done
    8.19  
     9.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Fri Feb 20 23:46:03 2009 +0100
     9.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Sat Feb 21 09:58:26 2009 +0100
     9.3 @@ -217,7 +217,7 @@
     9.4      a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
     9.5    apply (unfold zcong_def dvd_def, auto)
     9.6    apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
     9.7 -  apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff zmod_zadd_right_eq)
     9.8 +  apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq)
     9.9    done
    9.10  
    9.11  lemma zcong_square_zless:
    9.12 @@ -237,7 +237,7 @@
    9.13  lemma zcong_zless_0:
    9.14      "0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0"
    9.15    apply (unfold zcong_def dvd_def, auto)
    9.16 -  apply (metis div_pos_pos_trivial linorder_not_less zdiv_zmult_self2 zle_refl zle_trans)
    9.17 +  apply (metis div_pos_pos_trivial linorder_not_less div_mult_self1_is_id zle_refl zle_trans)
    9.18    done
    9.19  
    9.20  lemma zcong_zless_unique:
    9.21 @@ -302,7 +302,7 @@
    9.22  
    9.23  lemma zmod_zdvd_zmod:
    9.24      "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)"
    9.25 -  by (rule zmod_zmod_cancel) 
    9.26 +  by (rule mod_mod_cancel) 
    9.27  
    9.28  
    9.29  subsection {* Extended GCD *}
    10.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Fri Feb 20 23:46:03 2009 +0100
    10.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Sat Feb 21 09:58:26 2009 +0100
    10.3 @@ -322,7 +322,7 @@
    10.4        by (rule zdiv_mono1) (insert p_g_2, auto)
    10.5      then show "b \<le> (q * a) div p"
    10.6        apply (subgoal_tac "p \<noteq> 0")
    10.7 -      apply (frule zdiv_zmult_self2, force)
    10.8 +      apply (frule div_mult_self1_is_id, force)
    10.9        apply (insert p_g_2, auto)
   10.10        done
   10.11    qed
   10.12 @@ -356,7 +356,7 @@
   10.13        by (rule zdiv_mono1) (insert q_g_2, auto)
   10.14      then show "a \<le> (p * b) div q"
   10.15        apply (subgoal_tac "q \<noteq> 0")
   10.16 -      apply (frule zdiv_zmult_self2, force)
   10.17 +      apply (frule div_mult_self1_is_id, force)
   10.18        apply (insert q_g_2, auto)
   10.19        done
   10.20    qed
    11.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Feb 20 23:46:03 2009 +0100
    11.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sat Feb 21 09:58:26 2009 +0100
    11.3 @@ -124,8 +124,7 @@
    11.4    @ map (symmetric o mk_meta_eq) 
    11.5      [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, 
    11.6       @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
    11.7 -     @{thm "mod_add_eq"}, @{thm "zmod_zadd_left_eq"}, 
    11.8 -     @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
    11.9 +     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   11.10    @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
   11.11       @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
   11.12       @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
    12.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Feb 20 23:46:03 2009 +0100
    12.2 +++ b/src/HOL/Word/BinGeneral.thy	Sat Feb 21 09:58:26 2009 +0100
    12.3 @@ -433,7 +433,7 @@
    12.4    "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
    12.5    apply (induct n)
    12.6     apply clarsimp
    12.7 -   apply (subst zmod_zadd_left_eq)
    12.8 +   apply (subst mod_add_left_eq)
    12.9     apply (simp add: bin_last_mod)
   12.10     apply (simp add: number_of_eq)
   12.11    apply clarsimp
   12.12 @@ -767,23 +767,23 @@
   12.13  lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard]
   12.14  
   12.15  lemmas brdmod1s' [symmetric] = 
   12.16 -  zmod_zadd_left_eq zmod_zadd_right_eq 
   12.17 +  mod_add_left_eq mod_add_right_eq 
   12.18    zmod_zsub_left_eq zmod_zsub_right_eq 
   12.19    zmod_zmult1_eq zmod_zmult1_eq_rev 
   12.20  
   12.21  lemmas brdmods' [symmetric] = 
   12.22    zpower_zmod' [symmetric]
   12.23 -  trans [OF zmod_zadd_left_eq zmod_zadd_right_eq] 
   12.24 +  trans [OF mod_add_left_eq mod_add_right_eq] 
   12.25    trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
   12.26    trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 
   12.27    zmod_uminus' [symmetric]
   12.28 -  zmod_zadd_left_eq [where b = "1"]
   12.29 +  mod_add_left_eq [where b = "1::int"]
   12.30    zmod_zsub_left_eq [where b = "1"]
   12.31  
   12.32  lemmas bintr_arith1s =
   12.33 -  brdmod1s' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
   12.34 +  brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
   12.35  lemmas bintr_ariths =
   12.36 -  brdmods' [where c="2^n", folded pred_def succ_def bintrunc_mod2p, standard]
   12.37 +  brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard]
   12.38  
   12.39  lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard] 
   12.40  
    13.1 --- a/src/HOL/Word/Num_Lemmas.thy	Fri Feb 20 23:46:03 2009 +0100
    13.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Sat Feb 21 09:58:26 2009 +0100
    13.3 @@ -127,12 +127,12 @@
    13.4  
    13.5  lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
    13.6    apply (unfold diff_int_def)
    13.7 -  apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]])
    13.8 -  apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])
    13.9 +  apply (rule trans [OF _ mod_add_right_eq [symmetric]])
   13.10 +  apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
   13.11    done
   13.12  
   13.13  lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
   13.14 -  by (rule zmod_zadd_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
   13.15 +  by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
   13.16  
   13.17  lemma zmod_zsub_self [simp]: 
   13.18    "((b :: int) - a) mod a = b mod a"
   13.19 @@ -146,8 +146,8 @@
   13.20    done
   13.21  
   13.22  lemmas rdmods [symmetric] = zmod_uminus [symmetric]
   13.23 -  zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq
   13.24 -  zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
   13.25 +  zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
   13.26 +  mod_add_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev
   13.27  
   13.28  lemma mod_plus_right:
   13.29    "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
   13.30 @@ -169,7 +169,8 @@
   13.31  lemmas push_mods = push_mods' [THEN eq_reflection, standard]
   13.32  lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]
   13.33  lemmas mod_simps = 
   13.34 -  zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection]
   13.35 +  mod_mult_self2_is_0 [THEN eq_reflection]
   13.36 +  mod_mult_self1_is_0 [THEN eq_reflection]
   13.37    mod_mod_trivial [THEN eq_reflection]
   13.38  
   13.39  lemma nat_mod_eq:
    14.1 --- a/src/HOL/Word/WordGenLib.thy	Fri Feb 20 23:46:03 2009 +0100
    14.2 +++ b/src/HOL/Word/WordGenLib.thy	Sat Feb 21 09:58:26 2009 +0100
    14.3 @@ -273,7 +273,7 @@
    14.4    have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
    14.5    show ?thesis
    14.6      apply (subst x)
    14.7 -    apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2)
    14.8 +    apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
    14.9      apply simp
   14.10      done
   14.11  qed