avoid using legacy theorem names
authorhuffman
Tue Sep 06 19:03:41 2011 -0700 (2011-09-06)
changeset 44766d4d33a4d7548
parent 44765 d96550db3d77
child 44767 233f30abb040
avoid using legacy theorem names
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Import/HOLLightInt.thy
src/HOL/Library/Float.thy
src/HOL/Nat_Numeral.thy
src/HOL/Old_Number_Theory/Chinese.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/EulerFermat.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/Finite2.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/Int2.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Old_Number_Theory/WilsonBij.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
src/HOL/Presburger.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Divides.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Divides.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -1732,16 +1732,16 @@
     1.4      1 div z and 1 mod z **)
     1.5  
     1.6  lemmas div_pos_pos_1_number_of [simp] =
     1.7 -    div_pos_pos [OF int_0_less_1, of "number_of w", standard]
     1.8 +    div_pos_pos [OF zero_less_one, of "number_of w", standard]
     1.9  
    1.10  lemmas div_pos_neg_1_number_of [simp] =
    1.11 -    div_pos_neg [OF int_0_less_1, of "number_of w", standard]
    1.12 +    div_pos_neg [OF zero_less_one, of "number_of w", standard]
    1.13  
    1.14  lemmas mod_pos_pos_1_number_of [simp] =
    1.15 -    mod_pos_pos [OF int_0_less_1, of "number_of w", standard]
    1.16 +    mod_pos_pos [OF zero_less_one, of "number_of w", standard]
    1.17  
    1.18  lemmas mod_pos_neg_1_number_of [simp] =
    1.19 -    mod_pos_neg [OF int_0_less_1, of "number_of w", standard]
    1.20 +    mod_pos_neg [OF zero_less_one, of "number_of w", standard]
    1.21  
    1.22  
    1.23  lemmas posDivAlg_eqn_1_number_of [simp] =
    1.24 @@ -1790,7 +1790,7 @@
    1.25  apply (subgoal_tac "b*q = r' - r + b'*q'")
    1.26   prefer 2 apply simp
    1.27  apply (simp (no_asm_simp) add: right_distrib)
    1.28 -apply (subst add_commute, rule zadd_zless_mono, arith)
    1.29 +apply (subst add_commute, rule add_less_le_mono, arith)
    1.30  apply (rule mult_right_mono, auto)
    1.31  done
    1.32  
     2.1 --- a/src/HOL/GCD.thy	Tue Sep 06 16:30:39 2011 -0700
     2.2 +++ b/src/HOL/GCD.thy	Tue Sep 06 19:03:41 2011 -0700
     2.3 @@ -1452,7 +1452,7 @@
     2.4  by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
     2.5  
     2.6  lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
     2.7 -by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
     2.8 +by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le)
     2.9  
    2.10  lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
    2.11  by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
     3.1 --- a/src/HOL/Import/HOLLightInt.thy	Tue Sep 06 16:30:39 2011 -0700
     3.2 +++ b/src/HOL/Import/HOLLightInt.thy	Tue Sep 06 19:03:41 2011 -0700
     3.3 @@ -11,7 +11,7 @@
     3.4  lemma DEF_int_coprime:
     3.5    "int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
     3.6    apply (auto simp add: fun_eq_iff)
     3.7 -  apply (metis bezout_int zmult_commute)
     3.8 +  apply (metis bezout_int mult_commute)
     3.9    by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
    3.10  
    3.11  lemma INT_FORALL_POS:
    3.12 @@ -24,7 +24,7 @@
    3.13  
    3.14  lemma INT_ABS_MUL_1:
    3.15    "(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
    3.16 -  by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult zmult_1_right)
    3.17 +  by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult mult_1_right)
    3.18  
    3.19  lemma dest_int_rep:
    3.20    "\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
    3.21 @@ -56,19 +56,19 @@
    3.22  
    3.23  lemma DEF_int_max:
    3.24    "max = (\<lambda>u ua. floor (max (real u) (real ua)))"
    3.25 -  by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max zle_linear)
    3.26 +  by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max linorder_linear)
    3.27  
    3.28  lemma int_max_th:
    3.29    "real (max (x :: int) y) = max (real x) (real y)"
    3.30 -  by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff zle_linear)
    3.31 +  by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff linorder_linear)
    3.32  
    3.33  lemma DEF_int_min:
    3.34    "min = (\<lambda>u ua. floor (min (real u) (real ua)))"
    3.35 -  by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
    3.36 +  by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
    3.37  
    3.38  lemma int_min_th:
    3.39    "real (min (x :: int) y) = min (real x) (real y)"
    3.40 -  by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
    3.41 +  by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
    3.42  
    3.43  lemma INT_IMAGE:
    3.44    "(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
    3.45 @@ -119,7 +119,7 @@
    3.46  lemma hl_mod_div:
    3.47    "n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
    3.48    unfolding hl_div_def hl_mod_def
    3.49 -  by auto (metis zmod_zdiv_equality zmult_commute zmult_zminus)
    3.50 +  by auto (metis zmod_zdiv_equality mult_commute mult_minus_left)
    3.51  
    3.52  lemma sth:
    3.53    "(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
    3.54 @@ -131,7 +131,7 @@
    3.55     (\<forall>(x :: int). int 0 * x = int 0) \<and>
    3.56     (\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
    3.57     (\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
    3.58 -  by (simp_all add: zadd_zmult_distrib2)
    3.59 +  by (simp_all add: right_distrib)
    3.60  
    3.61  lemma INT_DIVISION:
    3.62    "n ~= int 0 \<Longrightarrow> m = hl_div m n * n + hl_mod m n \<and> int 0 \<le> hl_mod m n \<and> hl_mod m n < abs n"
    3.63 @@ -160,7 +160,7 @@
    3.64    apply (simp add: hl_mod_def hl_div_def)
    3.65    apply (case_tac "xa > 0")
    3.66    apply (simp add: hl_mod_def hl_div_def)
    3.67 -  apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le zadd_0 zdiv_eq_0_iff zmult_commute)
    3.68 +  apply (metis comm_semiring_1_class.normalizing_semiring_rules(24) div_mult_self2 not_less_iff_gr_or_eq order_less_le add_0 zdiv_eq_0_iff mult_commute)
    3.69    apply (simp add: hl_mod_def hl_div_def)
    3.70    by (metis add.comm_neutral add_pos_nonneg div_mult_self1 less_minus_iff minus_add minus_add_cancel minus_minus mult_zero_right not_square_less_zero zdiv_eq_0_iff zdiv_zminus2)
    3.71  
    3.72 @@ -182,14 +182,14 @@
    3.73    apply (simp add: hl_mod_def hl_div_def)
    3.74    apply (metis add_left_cancel mod_div_equality)
    3.75    apply (simp add: hl_mod_def hl_div_def)
    3.76 -  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial zadd_commute zminus_zmod zmod_zminus2 zmult_commute)
    3.77 +  by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
    3.78  
    3.79  lemma DEF_int_gcd:
    3.80    "int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
    3.81         (d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
    3.82    apply (rule some_equality[symmetric])
    3.83    apply auto
    3.84 -  apply (metis bezout_int zmult_commute)
    3.85 +  apply (metis bezout_int mult_commute)
    3.86    apply (auto simp add: fun_eq_iff)
    3.87    apply (drule_tac x="a" in spec)
    3.88    apply (drule_tac x="b" in spec)
     4.1 --- a/src/HOL/Library/Float.thy	Tue Sep 06 16:30:39 2011 -0700
     4.2 +++ b/src/HOL/Library/Float.thy	Tue Sep 06 19:03:41 2011 -0700
     4.3 @@ -719,11 +719,11 @@
     4.4    shows "real (x div y) \<le> real (x * c div y) * inverse (real c)"
     4.5  proof -
     4.6    have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y]
     4.7 -    by (rule zadd_left_mono, 
     4.8 +    by (rule add_left_mono, 
     4.9          auto intro!: mult_nonneg_nonneg 
    4.10               simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`])
    4.11    hence "real (x div y) * real c \<le> real (x * c div y)" 
    4.12 -    unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
    4.13 +    unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto
    4.14    hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
    4.15      using `0 < c` by auto
    4.16    thus ?thesis unfolding mult_assoc using `0 < c` by auto
    4.17 @@ -777,7 +777,7 @@
    4.18  
    4.19      have "?X = y * (?X div y) + ?X mod y" by auto
    4.20      also have "\<dots> \<le> y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le])
    4.21 -    also have "\<dots> = y * (?X div y + 1)" unfolding zadd_zmult_distrib2 by auto
    4.22 +    also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto
    4.23      finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] .
    4.24      hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)" 
    4.25        by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
    4.26 @@ -1144,7 +1144,7 @@
    4.27      have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
    4.28        using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
    4.29      also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
    4.30 -      unfolding pow_split zpower_zadd_distrib by auto
    4.31 +      unfolding pow_split power_add by auto
    4.32      finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
    4.33        using `0 < m` by (rule zdiv_mono1)
    4.34      hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
    4.35 @@ -1273,7 +1273,7 @@
    4.36      next
    4.37        case False
    4.38        have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    4.39 -      also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib zmult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    4.40 +      also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    4.41        finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
    4.42          unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
    4.43          by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
    4.44 @@ -1361,7 +1361,7 @@
    4.45      have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l"
    4.46      proof -
    4.47        have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto
    4.48 -      hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding zmult_1 real_of_int_less_iff[symmetric] by auto
    4.49 +      hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding mult_1 real_of_int_less_iff[symmetric] by auto
    4.50        
    4.51        have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
    4.52        also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto
     5.1 --- a/src/HOL/Nat_Numeral.thy	Tue Sep 06 16:30:39 2011 -0700
     5.2 +++ b/src/HOL/Nat_Numeral.thy	Tue Sep 06 19:03:41 2011 -0700
     5.3 @@ -364,7 +364,7 @@
     5.4  
     5.5  lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
     5.6  apply (rule sym)
     5.7 -apply (simp add: nat_eq_iff int_Suc)
     5.8 +apply (simp add: nat_eq_iff)
     5.9  done
    5.10  
    5.11  lemma Suc_nat_number_of_add:
     6.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy	Tue Sep 06 16:30:39 2011 -0700
     6.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy	Tue Sep 06 19:03:41 2011 -0700
     6.3 @@ -241,7 +241,7 @@
     6.4            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
     6.5            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
     6.6           prefer 6
     6.7 -         apply (simp add: zmult_ac)
     6.8 +         apply (simp add: mult_ac)
     6.9          apply (unfold xilin_sol_def)
    6.10          apply (tactic {* asm_simp_tac @{simpset} 6 *})
    6.11          apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
     7.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Tue Sep 06 16:30:39 2011 -0700
     7.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Tue Sep 06 19:03:41 2011 -0700
     7.3 @@ -67,7 +67,7 @@
     7.4    then have "[j * j = (a * MultInv p j) * j] (mod p)"
     7.5      by (auto simp add: zcong_scalar)
     7.6    then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
     7.7 -    by (auto simp add: zmult_ac)
     7.8 +    by (auto simp add: mult_ac)
     7.9    have "[j * j = a] (mod p)"
    7.10    proof -
    7.11      from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
    7.12 @@ -148,7 +148,7 @@
    7.13                     c = "a * (x * MultInv p x)" in  zcong_trans, force)
    7.14    apply (frule_tac p = p and x = x in MultInv_prop2, auto)
    7.15  apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
    7.16 -  apply (auto simp add: zmult_ac)
    7.17 +  apply (auto simp add: mult_ac)
    7.18    done
    7.19  
    7.20  lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
    7.21 @@ -237,7 +237,7 @@
    7.22    then have "a ^ (nat p) =  a ^ (1 + (nat p - 1))"
    7.23      by (auto simp add: diff_add_assoc)
    7.24    also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
    7.25 -    by (simp only: zpower_zadd_distrib)
    7.26 +    by (simp only: power_add)
    7.27    also have "... = a * a ^ (nat(p) - 1)"
    7.28      by auto
    7.29    finally show ?thesis .
    7.30 @@ -286,7 +286,7 @@
    7.31    apply (auto simp add: zpower_zpower) 
    7.32    apply (rule zcong_trans)
    7.33    apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
    7.34 -  apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one zmult_1 aux__2)
    7.35 +  apply (metis Little_Fermat even_div_2_prop2 mult_Bit0 number_of_is_id odd_minus_one_even one_is_num_one mult_1 aux__2)
    7.36    done
    7.37  
    7.38  
     8.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Tue Sep 06 16:30:39 2011 -0700
     8.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Tue Sep 06 19:03:41 2011 -0700
     8.3 @@ -257,7 +257,7 @@
     8.4    apply (subst setprod_insert)
     8.5      apply (rule_tac [2] Bnor_prod_power_aux)
     8.6       apply (unfold inj_on_def)
     8.7 -     apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap)
     8.8 +     apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
     8.9    done
    8.10  
    8.11  
     9.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Tue Sep 06 16:30:39 2011 -0700
     9.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Tue Sep 06 19:03:41 2011 -0700
     9.3 @@ -39,7 +39,7 @@
     9.4      then have "2 * (a::int) - 2 * (b :: int) = 1"
     9.5        by arith
     9.6      then have "2 * (a - b) = 1"
     9.7 -      by (auto simp add: zdiff_zmult_distrib)
     9.8 +      by (auto simp add: left_diff_distrib)
     9.9      moreover have "(2 * (a - b)):zEven"
    9.10        by (auto simp only: zEven_def)
    9.11      ultimately have False
    9.12 @@ -66,7 +66,7 @@
    9.13    then have "2 * a * y - 2 * b = 1"
    9.14      by arith
    9.15    then have "2 * (a * y - b) = 1"
    9.16 -    by (auto simp add: zdiff_zmult_distrib)
    9.17 +    by (auto simp add: left_diff_distrib)
    9.18    moreover have "(2 * (a * y - b)):zEven"
    9.19      by (auto simp only: zEven_def)
    9.20    ultimately have False
    9.21 @@ -85,7 +85,7 @@
    9.22  
    9.23  lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
    9.24    apply (auto simp add: zEven_def)
    9.25 -  apply (auto simp only: zadd_zmult_distrib2 [symmetric])
    9.26 +  apply (auto simp only: right_distrib [symmetric])
    9.27    done
    9.28  
    9.29  lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
    9.30 @@ -93,12 +93,12 @@
    9.31  
    9.32  lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"
    9.33    apply (auto simp add: zEven_def)
    9.34 -  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
    9.35 +  apply (auto simp only: right_diff_distrib [symmetric])
    9.36    done
    9.37  
    9.38  lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
    9.39    apply (auto simp add: zOdd_def zEven_def)
    9.40 -  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
    9.41 +  apply (auto simp only: right_diff_distrib [symmetric])
    9.42    done
    9.43  
    9.44  lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
    9.45 @@ -109,13 +109,13 @@
    9.46  
    9.47  lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
    9.48    apply (auto simp add: zOdd_def zEven_def)
    9.49 -  apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
    9.50 +  apply (auto simp only: right_diff_distrib [symmetric])
    9.51    done
    9.52  
    9.53  lemma odd_times_odd: "[| x \<in> zOdd;  y \<in> zOdd |] ==> x * y \<in> zOdd"
    9.54 -  apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
    9.55 +  apply (auto simp add: zOdd_def left_distrib right_distrib)
    9.56    apply (rule_tac x = "2 * ka * k + ka + k" in exI)
    9.57 -  apply (auto simp add: zadd_zmult_distrib)
    9.58 +  apply (auto simp add: left_distrib)
    9.59    done
    9.60  
    9.61  lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
    9.62 @@ -195,7 +195,7 @@
    9.63    finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
    9.64      by simp
    9.65    also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
    9.66 -    by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib)
    9.67 +    by (auto simp add: power_mult power_add)
    9.68    also have "(-1::int)^2 = 1"
    9.69      by simp
    9.70    finally show ?thesis
    10.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Tue Sep 06 16:30:39 2011 -0700
    10.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Tue Sep 06 19:03:41 2011 -0700
    10.3 @@ -38,18 +38,18 @@
    10.4  
    10.5  lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
    10.6    apply (induct set: finite)
    10.7 -  apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
    10.8 +  apply (auto simp add: left_distrib right_distrib)
    10.9    done
   10.10  
   10.11  lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
   10.12      int(c) * int(card X)"
   10.13    apply (induct set: finite)
   10.14 -  apply (auto simp add: zadd_zmult_distrib2)
   10.15 +  apply (auto simp add: right_distrib)
   10.16    done
   10.17  
   10.18  lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
   10.19      c * setsum f A"
   10.20 -  by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
   10.21 +  by (induct set: finite) (auto simp add: right_distrib)
   10.22  
   10.23  
   10.24  subsection {* Cardinality of explicit finite sets *}
    11.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Tue Sep 06 16:30:39 2011 -0700
    11.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Tue Sep 06 19:03:41 2011 -0700
    11.3 @@ -344,7 +344,7 @@
    11.4      apply (elim zcong_trans)
    11.5      by (simp only: zcong_refl)
    11.6    also have "y * a + ya * a = a * (y + ya)"
    11.7 -    by (simp add: zadd_zmult_distrib2 zmult_commute)
    11.8 +    by (simp add: right_distrib mult_commute)
    11.9    finally have "[a * (y + ya) = 0] (mod p)" .
   11.10    with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
   11.11      p_a_relprime
   11.12 @@ -429,7 +429,7 @@
   11.13    also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
   11.14      using finite_E by (induct set: finite) auto
   11.15    then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
   11.16 -    by (simp add: zmult_commute)
   11.17 +    by (simp add: mult_commute)
   11.18    with two show ?thesis
   11.19      by simp
   11.20  qed
   11.21 @@ -444,7 +444,7 @@
   11.22    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   11.23  proof -
   11.24    have "[setprod id A = setprod id F * setprod id D](mod p)"
   11.25 -    by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
   11.26 +    by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
   11.27    then have "[setprod id A = ((-1)^(card E) * setprod id E) *
   11.28        setprod id D] (mod p)"
   11.29      apply (rule zcong_trans)
   11.30 @@ -453,7 +453,7 @@
   11.31    then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
   11.32      apply (rule zcong_trans)
   11.33      apply (insert C_prod_eq_D_times_E, erule subst)
   11.34 -    apply (subst zmult_assoc, auto)
   11.35 +    apply (subst mult_assoc, auto)
   11.36      done
   11.37    then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
   11.38      apply (rule zcong_trans)
   11.39 @@ -474,7 +474,7 @@
   11.40    then have "[setprod id A = ((-1)^(card E) * a^(card A) *
   11.41        setprod id A)](mod p)"
   11.42      apply (rule zcong_trans)
   11.43 -    apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant zmult_assoc)
   11.44 +    apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult_assoc)
   11.45      done
   11.46    then have a: "[setprod id A * (-1)^(card E) =
   11.47        ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
    12.1 --- a/src/HOL/Old_Number_Theory/Int2.thy	Tue Sep 06 16:30:39 2011 -0700
    12.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy	Tue Sep 06 19:03:41 2011 -0700
    12.3 @@ -51,7 +51,7 @@
    12.4    have "(x div z) * z \<le> (x div z) * z" by simp
    12.5    then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith 
    12.6    also have "\<dots> = x"
    12.7 -    by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
    12.8 +    by (auto simp add: zmod_zdiv_equality [symmetric] mult_ac)
    12.9    also note `x < y * z`
   12.10    finally show ?thesis
   12.11      apply (auto simp add: mult_less_cancel_right)
   12.12 @@ -115,7 +115,7 @@
   12.13  
   12.14  lemma zcong_zmult_prop2: "[a = b](mod m) ==>
   12.15      ([c = d * a](mod m) = [c = d * b] (mod m))"
   12.16 -  by (auto simp add: zmult_ac zcong_zmult_prop1)
   12.17 +  by (auto simp add: mult_ac zcong_zmult_prop1)
   12.18  
   12.19  lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
   12.20      ~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
   12.21 @@ -125,7 +125,7 @@
   12.22  
   12.23  lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
   12.24      x < m; y < m |] ==> x = y"
   12.25 -  by (metis zcong_not zcong_sym zless_linear)
   12.26 +  by (metis zcong_not zcong_sym less_linear)
   12.27  
   12.28  lemma zcong_neg_1_impl_ne_1:
   12.29    assumes "2 < p" and "[x = -1] (mod p)"
   12.30 @@ -198,7 +198,7 @@
   12.31  
   12.32  lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   12.33      [(MultInv p x) * x = 1] (mod p)"
   12.34 -  by (auto simp add: MultInv_prop2 zmult_ac)
   12.35 +  by (auto simp add: MultInv_prop2 mult_ac)
   12.36  
   12.37  lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
   12.38    by (simp add: nat_diff_distrib)
   12.39 @@ -227,7 +227,7 @@
   12.40    apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
   12.41    apply (drule MultInv_prop2, auto)
   12.42    apply (drule_tac k = x in zcong_scalar2, auto)
   12.43 -  apply (auto simp add: zmult_ac)
   12.44 +  apply (auto simp add: mult_ac)
   12.45    done
   12.46  
   12.47  lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
   12.48 @@ -244,10 +244,10 @@
   12.49      m = p and k = x in zcong_scalar)
   12.50    apply (insert MultInv_prop2 [of p x], simp)
   12.51    apply (auto simp only: zcong_sym [of "MultInv p x * x"])
   12.52 -  apply (auto simp add:  zmult_ac)
   12.53 +  apply (auto simp add: mult_ac)
   12.54    apply (drule zcong_trans, auto)
   12.55    apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
   12.56 -  apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
   12.57 +  apply (insert MultInv_prop2a [of p y], auto simp add: mult_ac)
   12.58    apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
   12.59    apply (auto simp add: zcong_sym)
   12.60    done
   12.61 @@ -264,19 +264,19 @@
   12.62      [j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
   12.63    apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
   12.64      [of "MultInv p k * k" 1 p "j * k" a])
   12.65 -  apply (auto simp add: zmult_ac)
   12.66 +  apply (auto simp add: mult_ac)
   12.67    done
   12.68  
   12.69  lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
   12.70       (MultInv p j) * a] (mod p)"
   12.71 -  by (auto simp add: zmult_assoc zcong_scalar2)
   12.72 +  by (auto simp add: mult_assoc zcong_scalar2)
   12.73  
   12.74  lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
   12.75      [(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
   12.76         ==> [k = a * (MultInv p j)] (mod p)"
   12.77    apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
   12.78      [of "MultInv p j * j" 1 p "MultInv p j * a" k])
   12.79 -  apply (auto simp add: zmult_ac zcong_sym)
   12.80 +  apply (auto simp add: mult_ac zcong_sym)
   12.81    done
   12.82  
   12.83  lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
    13.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Sep 06 16:30:39 2011 -0700
    13.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Tue Sep 06 19:03:41 2011 -0700
    13.3 @@ -43,7 +43,7 @@
    13.4  
    13.5  lemma zrelprime_zdvd_zmult_aux:
    13.6       "zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
    13.7 -    by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
    13.8 +    by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs mult_1_right)
    13.9  
   13.10  lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
   13.11    apply (case_tac "0 \<le> m")
   13.12 @@ -93,7 +93,7 @@
   13.13    apply (simp add: zgcd_greatest_iff)
   13.14    apply (rule_tac n = k in zrelprime_zdvd_zmult)
   13.15     prefer 2
   13.16 -   apply (simp add: zmult_commute)
   13.17 +   apply (simp add: mult_commute)
   13.18    apply (metis zgcd_1 zgcd_commute zgcd_left_commute)
   13.19    done
   13.20  
   13.21 @@ -142,8 +142,8 @@
   13.22      "[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
   13.23    apply (rule_tac b = "b * c" in zcong_trans)
   13.24     apply (unfold zcong_def)
   13.25 -  apply (metis zdiff_zmult_distrib2 dvd_mult zmult_commute)
   13.26 -  apply (metis zdiff_zmult_distrib2 dvd_mult)
   13.27 +  apply (metis right_diff_distrib dvd_mult mult_commute)
   13.28 +  apply (metis right_diff_distrib dvd_mult)
   13.29    done
   13.30  
   13.31  lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
   13.32 @@ -165,7 +165,7 @@
   13.33      apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst)
   13.34       prefer 4
   13.35       apply (simp add: zdvd_reduce)
   13.36 -    apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2)
   13.37 +    apply (simp_all add: left_diff_distrib mult_commute right_diff_distrib)
   13.38    done
   13.39  
   13.40  lemma zcong_cancel:
   13.41 @@ -179,7 +179,7 @@
   13.42     apply (subst zcong_sym)
   13.43     apply (unfold zcong_def)
   13.44     apply (rule_tac [!] zrelprime_zdvd_zmult)
   13.45 -     apply (simp_all add: zdiff_zmult_distrib)
   13.46 +     apply (simp_all add: left_diff_distrib)
   13.47    apply (subgoal_tac "m dvd (-(a * k - b * k))")
   13.48     apply simp
   13.49    apply (subst dvd_minus_iff, assumption)
   13.50 @@ -188,7 +188,7 @@
   13.51  lemma zcong_cancel2:
   13.52    "0 \<le> m ==>
   13.53      zgcd k m = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
   13.54 -  by (simp add: zmult_commute zcong_cancel)
   13.55 +  by (simp add: mult_commute zcong_cancel)
   13.56  
   13.57  lemma zcong_zgcd_zmult_zmod:
   13.58    "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
   13.59 @@ -197,9 +197,9 @@
   13.60    apply (subgoal_tac "m dvd n * ka")
   13.61     apply (subgoal_tac "m dvd ka")
   13.62      apply (case_tac [2] "0 \<le> ka")
   13.63 -  apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
   13.64 -  apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
   13.65 -  apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_antisym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
   13.66 +  apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
   13.67 +  apply (metis abs_dvd_iff abs_of_nonneg add_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs mult_1_right mult_commute)
   13.68 +  apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff order_antisym linorder_linear order_refl mult_commute zrelprime_zdvd_zmult)
   13.69    apply (metis dvd_triv_left)
   13.70    done
   13.71  
   13.72 @@ -208,7 +208,7 @@
   13.73      a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
   13.74    apply (unfold zcong_def dvd_def, auto)
   13.75    apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
   13.76 -  apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq)
   13.77 +  apply (metis diff_add_cancel mod_pos_pos_trivial add_0 add_commute zmod_eq_0_iff mod_add_right_eq)
   13.78    done
   13.79  
   13.80  lemma zcong_square_zless:
   13.81 @@ -253,7 +253,7 @@
   13.82  
   13.83  lemma zcong_zmod_aux:
   13.84       "a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
   13.85 -  by(simp add: zdiff_zmult_distrib2 add_diff_eq eq_diff_eq add_ac)
   13.86 +  by(simp add: right_diff_distrib add_diff_eq eq_diff_eq add_ac)
   13.87  
   13.88  lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
   13.89    apply (unfold zcong_def)
   13.90 @@ -261,7 +261,7 @@
   13.91    apply (rule_tac m = m in zcong_zmod_aux)
   13.92    apply (rule trans)
   13.93     apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
   13.94 -  apply (simp add: zadd_commute)
   13.95 +  apply (simp add: add_commute)
   13.96    done
   13.97  
   13.98  lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)"
   13.99 @@ -282,7 +282,7 @@
  13.100    apply (erule disjE)  
  13.101     prefer 2 apply (simp add: zcong_zmod_eq)
  13.102    txt{*Remainding case: @{term "m<0"}*}
  13.103 -  apply (rule_tac t = m in zminus_zminus [THEN subst])
  13.104 +  apply (rule_tac t = m in minus_minus [THEN subst])
  13.105    apply (subst zcong_zminus)
  13.106    apply (subst zcong_zmod_eq, arith)
  13.107    apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
  13.108 @@ -324,7 +324,7 @@
  13.109    apply (case_tac "r' mod r = 0")
  13.110     prefer 2
  13.111     apply (frule_tac a = "r'" in pos_mod_sign, auto)
  13.112 -  apply (metis Pair_eq xzgcda.simps zle_refl)
  13.113 +  apply (metis Pair_eq xzgcda.simps order_refl)
  13.114    done
  13.115  
  13.116  lemma xzgcd_correct:
  13.117 @@ -341,7 +341,7 @@
  13.118  lemma xzgcda_linear_aux1:
  13.119    "(a - r * b) * m + (c - r * d) * (n::int) =
  13.120     (a * m + c * n) - r * (b * m + d * n)"
  13.121 -  by (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
  13.122 +  by (simp add: left_diff_distrib right_distrib mult_assoc)
  13.123  
  13.124  lemma xzgcda_linear_aux2:
  13.125    "r' = s' * m + t' * n ==> r = s * m + t * n
  13.126 @@ -391,7 +391,7 @@
  13.127     prefer 2
  13.128     apply simp
  13.129    apply (unfold zcong_def)
  13.130 -  apply (simp (no_asm) add: zmult_commute)
  13.131 +  apply (simp (no_asm) add: mult_commute)
  13.132    done
  13.133  
  13.134  lemma zcong_lineq_unique:
  13.135 @@ -407,7 +407,7 @@
  13.136    apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
  13.137    apply (rule_tac x = "x * b mod n" in exI, safe)
  13.138      apply (simp_all (no_asm_simp))
  13.139 -  apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq zmult_1 zmult_assoc)
  13.140 +  apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq mult_1 mult_assoc)
  13.141    done
  13.142  
  13.143  end
    14.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Tue Sep 06 16:30:39 2011 -0700
    14.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Tue Sep 06 19:03:41 2011 -0700
    14.3 @@ -22,7 +22,7 @@
    14.4    from finite_A have "a * setsum id A = setsum (%x. a * x) A"
    14.5      by (auto simp add: setsum_const_mult id_def)
    14.6    also have "setsum (%x. a * x) = setsum (%x. x * a)"
    14.7 -    by (auto simp add: zmult_commute)
    14.8 +    by (auto simp add: mult_commute)
    14.9    also have "setsum (%x. x * a) A = setsum id B"
   14.10      by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
   14.11    also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
   14.12 @@ -71,7 +71,7 @@
   14.13      p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
   14.14  proof -
   14.15    have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
   14.16 -    by (auto simp add: zdiff_zmult_distrib)
   14.17 +    by (auto simp add: left_diff_distrib)
   14.18    also note QRLemma1
   14.19    also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
   14.20       setsum id E - setsum id A =
   14.21 @@ -82,7 +82,7 @@
   14.22        p * int (card E) + 2 * setsum id E"
   14.23      by arith
   14.24    finally show ?thesis
   14.25 -    by (auto simp only: zdiff_zmult_distrib2)
   14.26 +    by (auto simp only: right_diff_distrib)
   14.27  qed
   14.28  
   14.29  lemma QRLemma4: "a \<in> zOdd ==>
   14.30 @@ -284,7 +284,7 @@
   14.31  proof -
   14.32    fix a and b
   14.33    assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
   14.34 -  with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
   14.35 +  with less_linear have "(p * b < q * a) | (p * b = q * a)" by auto
   14.36    moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
   14.37    ultimately show "p * b < q * a" by auto
   14.38  qed
   14.39 @@ -388,7 +388,7 @@
   14.40      by (auto simp add: int_distrib)
   14.41    then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
   14.42      apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
   14.43 -    by (auto simp add: even3, auto simp add: zmult_ac)
   14.44 +    by (auto simp add: even3, auto simp add: mult_ac)
   14.45    also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
   14.46      by (auto simp add: even1 even_prod_div_2)
   14.47    also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
   14.48 @@ -557,11 +557,11 @@
   14.49  
   14.50  lemma S1_carda: "int (card(S1)) =
   14.51      setsum (%j. (j * q) div p) P_set"
   14.52 -  by (auto simp add: S1_card zmult_ac)
   14.53 +  by (auto simp add: S1_card mult_ac)
   14.54  
   14.55  lemma S2_carda: "int (card(S2)) =
   14.56      setsum (%j. (j * p) div q) Q_set"
   14.57 -  by (auto simp add: S2_card zmult_ac)
   14.58 +  by (auto simp add: S2_card mult_ac)
   14.59  
   14.60  lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
   14.61      (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
   14.62 @@ -610,7 +610,7 @@
   14.63      by auto
   14.64    also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
   14.65                     nat(setsum (%x. ((x * q) div p)) P_set))"
   14.66 -    by (auto simp add: zpower_zadd_distrib)
   14.67 +    by (auto simp add: power_add)
   14.68    also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
   14.69        nat(setsum (%x. ((x * q) div p)) P_set) =
   14.70          nat((setsum (%x. ((x * p) div q)) Q_set) +
    15.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Tue Sep 06 16:30:39 2011 -0700
    15.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Tue Sep 06 19:03:41 2011 -0700
    15.3 @@ -75,7 +75,7 @@
    15.4  lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    15.5    -- {* same as @{text WilsonRuss} *}
    15.6    apply (unfold zcong_def)
    15.7 -  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
    15.8 +  apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
    15.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   15.10     apply (simp add: algebra_simps)
   15.11    apply (subst dvd_minus_iff)
   15.12 @@ -213,7 +213,7 @@
   15.13  
   15.14  lemma reciP_sym: "zprime p ==> symP (reciR p)"
   15.15    apply (unfold reciR_def symP_def)
   15.16 -  apply (simp add: zmult_commute)
   15.17 +  apply (simp add: mult_commute)
   15.18    apply auto
   15.19    done
   15.20  
   15.21 @@ -240,7 +240,7 @@
   15.22      apply (subst setprod_insert)
   15.23        apply (auto simp add: fin_bijER)
   15.24    apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
   15.25 -   apply (simp add: zmult_assoc)
   15.26 +   apply (simp add: mult_assoc)
   15.27    apply (rule zcong_zmult)
   15.28     apply auto
   15.29    done
    16.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Sep 06 16:30:39 2011 -0700
    16.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Tue Sep 06 19:03:41 2011 -0700
    16.3 @@ -80,7 +80,7 @@
    16.4  lemma inv_not_p_minus_1_aux:
    16.5      "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
    16.6    apply (unfold zcong_def)
    16.7 -  apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
    16.8 +  apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
    16.9    apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
   16.10     apply (simp add: algebra_simps)
   16.11    apply (subst dvd_minus_iff)
   16.12 @@ -123,13 +123,13 @@
   16.13      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
   16.14    apply (subst int_int_eq [symmetric])
   16.15    apply (simp add: zmult_int [symmetric])
   16.16 -  apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
   16.17 +  apply (simp add: left_diff_distrib right_diff_distrib)
   16.18    done
   16.19  
   16.20  lemma zcong_zpower_zmult:
   16.21      "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
   16.22    apply (induct z)
   16.23 -   apply (auto simp add: zpower_zadd_distrib)
   16.24 +   apply (auto simp add: power_add)
   16.25    apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
   16.26     apply (rule_tac [2] zcong_zmult, simp_all)
   16.27    done
   16.28 @@ -261,7 +261,7 @@
   16.29        apply (subgoal_tac [5]
   16.30          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
   16.31         prefer 5
   16.32 -       apply (simp add: zmult_assoc)
   16.33 +       apply (simp add: mult_assoc)
   16.34        apply (rule_tac [5] zcong_zmult)
   16.35         apply (rule_tac [5] inv_is_inv)
   16.36           apply (tactic "clarify_tac @{context} 4")
    17.1 --- a/src/HOL/Presburger.thy	Tue Sep 06 16:30:39 2011 -0700
    17.2 +++ b/src/HOL/Presburger.thy	Tue Sep 06 19:03:41 2011 -0700
    17.3 @@ -308,7 +308,7 @@
    17.4    {fix x
    17.5      have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
    17.6      also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
    17.7 -      by (simp add:int_distrib zadd_ac)
    17.8 +      by (simp add:int_distrib add_ac)
    17.9      ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
   17.10    thus ?case ..
   17.11  qed
    18.1 --- a/src/HOL/RealDef.thy	Tue Sep 06 16:30:39 2011 -0700
    18.2 +++ b/src/HOL/RealDef.thy	Tue Sep 06 19:03:41 2011 -0700
    18.3 @@ -1412,7 +1412,7 @@
    18.4  by (insert real_of_nat_div2 [of n x], simp)
    18.5  
    18.6  lemma real_of_int_real_of_nat: "real (int n) = real n"
    18.7 -by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
    18.8 +by (simp add: real_of_nat_def real_of_int_def)
    18.9  
   18.10  lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
   18.11  by (simp add: real_of_int_def real_of_nat_def)