--- a/src/HOL/Divides.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Divides.thy Tue Sep 06 19:03:41 2011 -0700
@@ -1732,16 +1732,16 @@
1 div z and 1 mod z **)
lemmas div_pos_pos_1_number_of [simp] =
- div_pos_pos [OF int_0_less_1, of "number_of w", standard]
+ div_pos_pos [OF zero_less_one, of "number_of w", standard]
lemmas div_pos_neg_1_number_of [simp] =
- div_pos_neg [OF int_0_less_1, of "number_of w", standard]
+ div_pos_neg [OF zero_less_one, of "number_of w", standard]
lemmas mod_pos_pos_1_number_of [simp] =
- mod_pos_pos [OF int_0_less_1, of "number_of w", standard]
+ mod_pos_pos [OF zero_less_one, of "number_of w", standard]
lemmas mod_pos_neg_1_number_of [simp] =
- mod_pos_neg [OF int_0_less_1, of "number_of w", standard]
+ mod_pos_neg [OF zero_less_one, of "number_of w", standard]
lemmas posDivAlg_eqn_1_number_of [simp] =
@@ -1790,7 +1790,7 @@
apply (subgoal_tac "b*q = r' - r + b'*q'")
prefer 2 apply simp
apply (simp (no_asm_simp) add: right_distrib)
-apply (subst add_commute, rule zadd_zless_mono, arith)
+apply (subst add_commute, rule add_less_le_mono, arith)
apply (rule mult_right_mono, auto)
done
--- a/src/HOL/GCD.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/GCD.thy Tue Sep 06 19:03:41 2011 -0700
@@ -1452,7 +1452,7 @@
by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
-by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
+by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le)
lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
--- a/src/HOL/Import/HOLLightInt.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Import/HOLLightInt.thy Tue Sep 06 19:03:41 2011 -0700
@@ -11,7 +11,7 @@
lemma DEF_int_coprime:
"int_coprime = (\<lambda>u. \<exists>x y. ((fst u) * x) + ((snd u) * y) = int 1)"
apply (auto simp add: fun_eq_iff)
- apply (metis bezout_int zmult_commute)
+ apply (metis bezout_int mult_commute)
by (metis coprime_divisors_nat dvd_triv_left gcd_1_int gcd_add2_int)
lemma INT_FORALL_POS:
@@ -24,7 +24,7 @@
lemma INT_ABS_MUL_1:
"(abs (x * y) = int 1) = (abs x = int 1 \<and> abs y = int 1)"
- by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult zmult_1_right)
+ by simp (metis dvd_mult_right zdvd1_eq abs_zmult_eq_1 abs_mult mult_1_right)
lemma dest_int_rep:
"\<exists>(n :: nat). real (i :: int) = real n \<or> real i = - real n"
@@ -56,19 +56,19 @@
lemma DEF_int_max:
"max = (\<lambda>u ua. floor (max (real u) (real ua)))"
- by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max zle_linear)
+ by (metis floor_real_of_int real_of_int_le_iff sup_absorb1 sup_commute sup_max linorder_linear)
lemma int_max_th:
"real (max (x :: int) y) = max (real x) (real y)"
- by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff zle_linear)
+ by (metis min_max.le_iff_sup min_max.sup_absorb1 real_of_int_le_iff linorder_linear)
lemma DEF_int_min:
"min = (\<lambda>u ua. floor (min (real u) (real ua)))"
- by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
+ by (metis floor_real_of_int inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
lemma int_min_th:
"real (min (x :: int) y) = min (real x) (real y)"
- by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff zle_linear)
+ by (metis inf_absorb1 inf_absorb2 inf_int_def inf_real_def real_of_int_le_iff linorder_linear)
lemma INT_IMAGE:
"(\<exists>n. x = int n) \<or> (\<exists>n. x = - int n)"
@@ -119,7 +119,7 @@
lemma hl_mod_div:
"n \<noteq> (0\<Colon>int) \<Longrightarrow> m = hl_div m n * n + hl_mod m n"
unfolding hl_div_def hl_mod_def
- by auto (metis zmod_zdiv_equality zmult_commute zmult_zminus)
+ by auto (metis zmod_zdiv_equality mult_commute mult_minus_left)
lemma sth:
"(\<forall>(x :: int) y z. x + (y + z) = x + y + z) \<and>
@@ -131,7 +131,7 @@
(\<forall>(x :: int). int 0 * x = int 0) \<and>
(\<forall>(x :: int) y z. x * (y + z) = x * y + x * z) \<and>
(\<forall>(x :: int). x ^ 0 = int 1) \<and> (\<forall>(x :: int) n. x ^ Suc n = x * x ^ n)"
- by (simp_all add: zadd_zmult_distrib2)
+ by (simp_all add: right_distrib)
lemma INT_DIVISION:
"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"
@@ -160,7 +160,7 @@
apply (simp add: hl_mod_def hl_div_def)
apply (case_tac "xa > 0")
apply (simp add: hl_mod_def hl_div_def)
- 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)
+ 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)
apply (simp add: hl_mod_def hl_div_def)
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)
@@ -182,14 +182,14 @@
apply (simp add: hl_mod_def hl_div_def)
apply (metis add_left_cancel mod_div_equality)
apply (simp add: hl_mod_def hl_div_def)
- by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial zadd_commute zminus_zmod zmod_zminus2 zmult_commute)
+ by (metis minus_mult_right mod_mult_self2 mod_pos_pos_trivial add_commute zminus_zmod zmod_zminus2 mult_commute)
lemma DEF_int_gcd:
"int_gcd = (SOME d. \<forall>a b. (int 0) \<le> (d (a, b)) \<and> (d (a, b)) dvd a \<and>
(d (a, b)) dvd b \<and> (\<exists>x y. d (a, b) = (a * x) + (b * y)))"
apply (rule some_equality[symmetric])
apply auto
- apply (metis bezout_int zmult_commute)
+ apply (metis bezout_int mult_commute)
apply (auto simp add: fun_eq_iff)
apply (drule_tac x="a" in spec)
apply (drule_tac x="b" in spec)
--- a/src/HOL/Library/Float.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Library/Float.thy Tue Sep 06 19:03:41 2011 -0700
@@ -719,11 +719,11 @@
shows "real (x div y) \<le> real (x * c div y) * inverse (real c)"
proof -
have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y]
- by (rule zadd_left_mono,
+ by (rule add_left_mono,
auto intro!: mult_nonneg_nonneg
simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`])
hence "real (x div y) * real c \<le> real (x * c div y)"
- unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
+ unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto
hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
using `0 < c` by auto
thus ?thesis unfolding mult_assoc using `0 < c` by auto
@@ -777,7 +777,7 @@
have "?X = y * (?X div y) + ?X mod y" by auto
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])
- also have "\<dots> = y * (?X div y + 1)" unfolding zadd_zmult_distrib2 by auto
+ also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto
finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] .
hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)"
by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
@@ -1144,7 +1144,7 @@
have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
- unfolding pow_split zpower_zadd_distrib by auto
+ unfolding pow_split power_add by auto
finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
using `0 < m` by (rule zdiv_mono1)
hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
@@ -1273,7 +1273,7 @@
next
case False
have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
- 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])
+ 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])
finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
@@ -1361,7 +1361,7 @@
have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l"
proof -
have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto
- 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
+ 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
have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
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
--- a/src/HOL/Nat_Numeral.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Nat_Numeral.thy Tue Sep 06 19:03:41 2011 -0700
@@ -364,7 +364,7 @@
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
apply (rule sym)
-apply (simp add: nat_eq_iff int_Suc)
+apply (simp add: nat_eq_iff)
done
lemma Suc_nat_number_of_add:
--- a/src/HOL/Old_Number_Theory/Chinese.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Chinese.thy Tue Sep 06 19:03:41 2011 -0700
@@ -241,7 +241,7 @@
"0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
\<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
prefer 6
- apply (simp add: zmult_ac)
+ apply (simp add: mult_ac)
apply (unfold xilin_sol_def)
apply (tactic {* asm_simp_tac @{simpset} 6 *})
apply (rule_tac [6] ex1_implies_ex [THEN someI_ex])
--- a/src/HOL/Old_Number_Theory/Euler.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Euler.thy Tue Sep 06 19:03:41 2011 -0700
@@ -67,7 +67,7 @@
then have "[j * j = (a * MultInv p j) * j] (mod p)"
by (auto simp add: zcong_scalar)
then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
- by (auto simp add: zmult_ac)
+ by (auto simp add: mult_ac)
have "[j * j = a] (mod p)"
proof -
from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
@@ -148,7 +148,7 @@
c = "a * (x * MultInv p x)" in zcong_trans, force)
apply (frule_tac p = p and x = x in MultInv_prop2, auto)
apply (metis StandardRes_SRStar_prop3 mult_1_right mult_commute zcong_sym zcong_zmult_prop1)
- apply (auto simp add: zmult_ac)
+ apply (auto simp add: mult_ac)
done
lemma aux1: "[| 0 < x; (x::int) < a; x \<noteq> (a - 1) |] ==> x < a - 1"
@@ -237,7 +237,7 @@
then have "a ^ (nat p) = a ^ (1 + (nat p - 1))"
by (auto simp add: diff_add_assoc)
also have "... = (a ^ 1) * a ^ (nat(p) - 1)"
- by (simp only: zpower_zadd_distrib)
+ by (simp only: power_add)
also have "... = a * a ^ (nat(p) - 1)"
by auto
finally show ?thesis .
@@ -286,7 +286,7 @@
apply (auto simp add: zpower_zpower)
apply (rule zcong_trans)
apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
- 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)
+ 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)
done
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Sep 06 19:03:41 2011 -0700
@@ -257,7 +257,7 @@
apply (subst setprod_insert)
apply (rule_tac [2] Bnor_prod_power_aux)
apply (unfold inj_on_def)
- apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap)
+ apply (simp_all add: mult_ac Bnor_fin Bnor_mem_zle_swap)
done
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Tue Sep 06 19:03:41 2011 -0700
@@ -39,7 +39,7 @@
then have "2 * (a::int) - 2 * (b :: int) = 1"
by arith
then have "2 * (a - b) = 1"
- by (auto simp add: zdiff_zmult_distrib)
+ by (auto simp add: left_diff_distrib)
moreover have "(2 * (a - b)):zEven"
by (auto simp only: zEven_def)
ultimately have False
@@ -66,7 +66,7 @@
then have "2 * a * y - 2 * b = 1"
by arith
then have "2 * (a * y - b) = 1"
- by (auto simp add: zdiff_zmult_distrib)
+ by (auto simp add: left_diff_distrib)
moreover have "(2 * (a * y - b)):zEven"
by (auto simp only: zEven_def)
ultimately have False
@@ -85,7 +85,7 @@
lemma even_plus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x + y \<in> zEven"
apply (auto simp add: zEven_def)
- apply (auto simp only: zadd_zmult_distrib2 [symmetric])
+ apply (auto simp only: right_distrib [symmetric])
done
lemma even_times_either: "x \<in> zEven ==> x * y \<in> zEven"
@@ -93,12 +93,12 @@
lemma even_minus_even: "[| x \<in> zEven; y \<in> zEven |] ==> x - y \<in> zEven"
apply (auto simp add: zEven_def)
- apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
+ apply (auto simp only: right_diff_distrib [symmetric])
done
lemma odd_minus_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x - y \<in> zEven"
apply (auto simp add: zOdd_def zEven_def)
- apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
+ apply (auto simp only: right_diff_distrib [symmetric])
done
lemma even_minus_odd: "[| x \<in> zEven; y \<in> zOdd |] ==> x - y \<in> zOdd"
@@ -109,13 +109,13 @@
lemma odd_minus_even: "[| x \<in> zOdd; y \<in> zEven |] ==> x - y \<in> zOdd"
apply (auto simp add: zOdd_def zEven_def)
- apply (auto simp only: zdiff_zmult_distrib2 [symmetric])
+ apply (auto simp only: right_diff_distrib [symmetric])
done
lemma odd_times_odd: "[| x \<in> zOdd; y \<in> zOdd |] ==> x * y \<in> zOdd"
- apply (auto simp add: zOdd_def zadd_zmult_distrib zadd_zmult_distrib2)
+ apply (auto simp add: zOdd_def left_distrib right_distrib)
apply (rule_tac x = "2 * ka * k + ka + k" in exI)
- apply (auto simp add: zadd_zmult_distrib)
+ apply (auto simp add: left_distrib)
done
lemma odd_iff_not_even: "(x \<in> zOdd) = (~ (x \<in> zEven))"
@@ -195,7 +195,7 @@
finally have "(-1::int)^nat x = (-1)^(2 * nat a + 1)"
by simp
also have "... = ((-1::int)^2)^ (nat a) * (-1)^1"
- by (auto simp add: zpower_zpower [symmetric] zpower_zadd_distrib)
+ by (auto simp add: power_mult power_add)
also have "(-1::int)^2 = 1"
by simp
finally show ?thesis
--- a/src/HOL/Old_Number_Theory/Finite2.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Tue Sep 06 19:03:41 2011 -0700
@@ -38,18 +38,18 @@
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
apply (induct set: finite)
- apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
+ apply (auto simp add: left_distrib right_distrib)
done
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)"
apply (induct set: finite)
- apply (auto simp add: zadd_zmult_distrib2)
+ apply (auto simp add: right_distrib)
done
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A"
- by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
+ by (induct set: finite) (auto simp add: right_distrib)
subsection {* Cardinality of explicit finite sets *}
--- a/src/HOL/Old_Number_Theory/Gauss.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Tue Sep 06 19:03:41 2011 -0700
@@ -344,7 +344,7 @@
apply (elim zcong_trans)
by (simp only: zcong_refl)
also have "y * a + ya * a = a * (y + ya)"
- by (simp add: zadd_zmult_distrib2 zmult_commute)
+ by (simp add: right_distrib mult_commute)
finally have "[a * (y + ya) = 0] (mod p)" .
with p_prime a_nonzero zcong_zprime_prod_zero [of p a "y + ya"]
p_a_relprime
@@ -429,7 +429,7 @@
also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
using finite_E by (induct set: finite) auto
then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
- by (simp add: zmult_commute)
+ by (simp add: mult_commute)
with two show ?thesis
by simp
qed
@@ -444,7 +444,7 @@
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[setprod id A = setprod id F * setprod id D](mod p)"
- by (auto simp add: prod_D_F_eq_prod_A zmult_commute cong del:setprod_cong)
+ by (auto simp add: prod_D_F_eq_prod_A mult_commute cong del:setprod_cong)
then have "[setprod id A = ((-1)^(card E) * setprod id E) *
setprod id D] (mod p)"
apply (rule zcong_trans)
@@ -453,7 +453,7 @@
then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
apply (rule zcong_trans)
apply (insert C_prod_eq_D_times_E, erule subst)
- apply (subst zmult_assoc, auto)
+ apply (subst mult_assoc, auto)
done
then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
apply (rule zcong_trans)
@@ -474,7 +474,7 @@
then have "[setprod id A = ((-1)^(card E) * a^(card A) *
setprod id A)](mod p)"
apply (rule zcong_trans)
- apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant zmult_assoc)
+ apply (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult_assoc)
done
then have a: "[setprod id A * (-1)^(card E) =
((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
--- a/src/HOL/Old_Number_Theory/Int2.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Int2.thy Tue Sep 06 19:03:41 2011 -0700
@@ -51,7 +51,7 @@
have "(x div z) * z \<le> (x div z) * z" by simp
then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith
also have "\<dots> = x"
- by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
+ by (auto simp add: zmod_zdiv_equality [symmetric] mult_ac)
also note `x < y * z`
finally show ?thesis
apply (auto simp add: mult_less_cancel_right)
@@ -115,7 +115,7 @@
lemma zcong_zmult_prop2: "[a = b](mod m) ==>
([c = d * a](mod m) = [c = d * b] (mod m))"
- by (auto simp add: zmult_ac zcong_zmult_prop1)
+ by (auto simp add: mult_ac zcong_zmult_prop1)
lemma zcong_zmult_prop3: "[| zprime p; ~[x = 0] (mod p);
~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)"
@@ -125,7 +125,7 @@
lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
x < m; y < m |] ==> x = y"
- by (metis zcong_not zcong_sym zless_linear)
+ by (metis zcong_not zcong_sym less_linear)
lemma zcong_neg_1_impl_ne_1:
assumes "2 < p" and "[x = -1] (mod p)"
@@ -198,7 +198,7 @@
lemma MultInv_prop2a: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
[(MultInv p x) * x = 1] (mod p)"
- by (auto simp add: MultInv_prop2 zmult_ac)
+ by (auto simp add: MultInv_prop2 mult_ac)
lemma aux_1: "2 < p ==> ((nat p) - 2) = (nat (p - 2))"
by (simp add: nat_diff_distrib)
@@ -227,7 +227,7 @@
apply (insert MultInv_prop2 [of p "MultInv p x"], auto)
apply (drule MultInv_prop2, auto)
apply (drule_tac k = x in zcong_scalar2, auto)
- apply (auto simp add: zmult_ac)
+ apply (auto simp add: mult_ac)
done
lemma MultInv_prop4: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
@@ -244,10 +244,10 @@
m = p and k = x in zcong_scalar)
apply (insert MultInv_prop2 [of p x], simp)
apply (auto simp only: zcong_sym [of "MultInv p x * x"])
- apply (auto simp add: zmult_ac)
+ apply (auto simp add: mult_ac)
apply (drule zcong_trans, auto)
apply (drule_tac a = "x * MultInv p y" and k = y in zcong_scalar, auto)
- apply (insert MultInv_prop2a [of p y], auto simp add: zmult_ac)
+ apply (insert MultInv_prop2a [of p y], auto simp add: mult_ac)
apply (insert zcong_zmult_prop2 [of "y * MultInv p y" 1 p y x])
apply (auto simp add: zcong_sym)
done
@@ -264,19 +264,19 @@
[j * k = a * MultInv p k * k] (mod p) |] ==> [j * k = a] (mod p)"
apply (insert MultInv_prop2a [of p k] zcong_zmult_prop2
[of "MultInv p k * k" 1 p "j * k" a])
- apply (auto simp add: zmult_ac)
+ apply (auto simp add: mult_ac)
done
lemma aux___3: "[j * k = a] (mod p) ==> [(MultInv p j) * j * k =
(MultInv p j) * a] (mod p)"
- by (auto simp add: zmult_assoc zcong_scalar2)
+ by (auto simp add: mult_assoc zcong_scalar2)
lemma aux___4: "[|2 < p; zprime p; ~([j = 0](mod p));
[(MultInv p j) * j * k = (MultInv p j) * a] (mod p) |]
==> [k = a * (MultInv p j)] (mod p)"
apply (insert MultInv_prop2a [of p j] zcong_zmult_prop1
[of "MultInv p j * j" 1 p "MultInv p j * a" k])
- apply (auto simp add: zmult_ac zcong_sym)
+ apply (auto simp add: mult_ac zcong_sym)
done
lemma MultInv_zcong_prop2: "[| 2 < p; zprime p; ~([k = 0](mod p));
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Sep 06 19:03:41 2011 -0700
@@ -43,7 +43,7 @@
lemma zrelprime_zdvd_zmult_aux:
"zgcd n k = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m"
- by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs zmult_1_right)
+ by (metis abs_of_nonneg dvd_triv_right zgcd_greatest_iff zgcd_zmult_distrib2_abs mult_1_right)
lemma zrelprime_zdvd_zmult: "zgcd n k = 1 ==> k dvd m * n ==> k dvd m"
apply (case_tac "0 \<le> m")
@@ -93,7 +93,7 @@
apply (simp add: zgcd_greatest_iff)
apply (rule_tac n = k in zrelprime_zdvd_zmult)
prefer 2
- apply (simp add: zmult_commute)
+ apply (simp add: mult_commute)
apply (metis zgcd_1 zgcd_commute zgcd_left_commute)
done
@@ -142,8 +142,8 @@
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)"
apply (rule_tac b = "b * c" in zcong_trans)
apply (unfold zcong_def)
- apply (metis zdiff_zmult_distrib2 dvd_mult zmult_commute)
- apply (metis zdiff_zmult_distrib2 dvd_mult)
+ apply (metis right_diff_distrib dvd_mult mult_commute)
+ apply (metis right_diff_distrib dvd_mult)
done
lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)"
@@ -165,7 +165,7 @@
apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst)
prefer 4
apply (simp add: zdvd_reduce)
- apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2)
+ apply (simp_all add: left_diff_distrib mult_commute right_diff_distrib)
done
lemma zcong_cancel:
@@ -179,7 +179,7 @@
apply (subst zcong_sym)
apply (unfold zcong_def)
apply (rule_tac [!] zrelprime_zdvd_zmult)
- apply (simp_all add: zdiff_zmult_distrib)
+ apply (simp_all add: left_diff_distrib)
apply (subgoal_tac "m dvd (-(a * k - b * k))")
apply simp
apply (subst dvd_minus_iff, assumption)
@@ -188,7 +188,7 @@
lemma zcong_cancel2:
"0 \<le> m ==>
zgcd k m = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)"
- by (simp add: zmult_commute zcong_cancel)
+ by (simp add: mult_commute zcong_cancel)
lemma zcong_zgcd_zmult_zmod:
"[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd m n = 1
@@ -197,9 +197,9 @@
apply (subgoal_tac "m dvd n * ka")
apply (subgoal_tac "m dvd ka")
apply (case_tac [2] "0 \<le> ka")
- apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
- 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)
- 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)
+ apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left mult_commute zrelprime_zdvd_zmult)
+ 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)
+ 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)
apply (metis dvd_triv_left)
done
@@ -208,7 +208,7 @@
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b"
apply (unfold zcong_def dvd_def, auto)
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong)
- apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff mod_add_right_eq)
+ apply (metis diff_add_cancel mod_pos_pos_trivial add_0 add_commute zmod_eq_0_iff mod_add_right_eq)
done
lemma zcong_square_zless:
@@ -253,7 +253,7 @@
lemma zcong_zmod_aux:
"a - b = (m::int) * (a div m - b div m) + (a mod m - b mod m)"
- by(simp add: zdiff_zmult_distrib2 add_diff_eq eq_diff_eq add_ac)
+ by(simp add: right_diff_distrib add_diff_eq eq_diff_eq add_ac)
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)"
apply (unfold zcong_def)
@@ -261,7 +261,7 @@
apply (rule_tac m = m in zcong_zmod_aux)
apply (rule trans)
apply (rule_tac [2] k = m and m = "a div m - b div m" in zdvd_reduce)
- apply (simp add: zadd_commute)
+ apply (simp add: add_commute)
done
lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)"
@@ -282,7 +282,7 @@
apply (erule disjE)
prefer 2 apply (simp add: zcong_zmod_eq)
txt{*Remainding case: @{term "m<0"}*}
- apply (rule_tac t = m in zminus_zminus [THEN subst])
+ apply (rule_tac t = m in minus_minus [THEN subst])
apply (subst zcong_zminus)
apply (subst zcong_zmod_eq, arith)
apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b])
@@ -324,7 +324,7 @@
apply (case_tac "r' mod r = 0")
prefer 2
apply (frule_tac a = "r'" in pos_mod_sign, auto)
- apply (metis Pair_eq xzgcda.simps zle_refl)
+ apply (metis Pair_eq xzgcda.simps order_refl)
done
lemma xzgcd_correct:
@@ -341,7 +341,7 @@
lemma xzgcda_linear_aux1:
"(a - r * b) * m + (c - r * d) * (n::int) =
(a * m + c * n) - r * (b * m + d * n)"
- by (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc)
+ by (simp add: left_diff_distrib right_distrib mult_assoc)
lemma xzgcda_linear_aux2:
"r' = s' * m + t' * n ==> r = s * m + t * n
@@ -391,7 +391,7 @@
prefer 2
apply simp
apply (unfold zcong_def)
- apply (simp (no_asm) add: zmult_commute)
+ apply (simp (no_asm) add: mult_commute)
done
lemma zcong_lineq_unique:
@@ -407,7 +407,7 @@
apply (cut_tac a = a and n = n in zcong_lineq_ex, auto)
apply (rule_tac x = "x * b mod n" in exI, safe)
apply (simp_all (no_asm_simp))
- apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq zmult_1 zmult_assoc)
+ apply (metis zcong_scalar zcong_zmod zmod_zmult1_eq mult_1 mult_assoc)
done
end
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Tue Sep 06 19:03:41 2011 -0700
@@ -22,7 +22,7 @@
from finite_A have "a * setsum id A = setsum (%x. a * x) A"
by (auto simp add: setsum_const_mult id_def)
also have "setsum (%x. a * x) = setsum (%x. x * a)"
- by (auto simp add: zmult_commute)
+ by (auto simp add: mult_commute)
also have "setsum (%x. x * a) A = setsum id B"
by (simp add: B_def setsum_reindex_id[OF inj_on_xa_A])
also have "... = setsum (%x. p * (x div p) + StandardRes p x) B"
@@ -71,7 +71,7 @@
p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
proof -
have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
- by (auto simp add: zdiff_zmult_distrib)
+ by (auto simp add: left_diff_distrib)
also note QRLemma1
also from QRLemma2 have "p * (\<Sum>x \<in> A. x * a div p) + setsum id D +
setsum id E - setsum id A =
@@ -82,7 +82,7 @@
p * int (card E) + 2 * setsum id E"
by arith
finally show ?thesis
- by (auto simp only: zdiff_zmult_distrib2)
+ by (auto simp only: right_diff_distrib)
qed
lemma QRLemma4: "a \<in> zOdd ==>
@@ -284,7 +284,7 @@
proof -
fix a and b
assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \<le> (q - 1) div 2"
- with zless_linear have "(p * b < q * a) | (p * b = q * a)" by auto
+ with less_linear have "(p * b < q * a) | (p * b = q * a)" by auto
moreover from pb_neq_qa b1 b2 have "(p * b \<noteq> q * a)" by auto
ultimately show "p * b < q * a" by auto
qed
@@ -388,7 +388,7 @@
by (auto simp add: int_distrib)
then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
- by (auto simp add: even3, auto simp add: zmult_ac)
+ by (auto simp add: even3, auto simp add: mult_ac)
also have "((p - 1) * q) div 2 = q * ((p - 1) div 2)"
by (auto simp add: even1 even_prod_div_2)
also have "(((q - 1) * p) + (2 * p)) div 2 = (((q - 1) div 2) * p) + p"
@@ -557,11 +557,11 @@
lemma S1_carda: "int (card(S1)) =
setsum (%j. (j * q) div p) P_set"
- by (auto simp add: S1_card zmult_ac)
+ by (auto simp add: S1_card mult_ac)
lemma S2_carda: "int (card(S2)) =
setsum (%j. (j * p) div q) Q_set"
- by (auto simp add: S2_card zmult_ac)
+ by (auto simp add: S2_card mult_ac)
lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
@@ -610,7 +610,7 @@
by auto
also have "... = (-1::int) ^ (nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set))"
- by (auto simp add: zpower_zadd_distrib)
+ by (auto simp add: power_add)
also have "nat(setsum (%x. ((x * p) div q)) Q_set) +
nat(setsum (%x. ((x * q) div p)) P_set) =
nat((setsum (%x. ((x * p) div q)) Q_set) +
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Tue Sep 06 19:03:41 2011 -0700
@@ -75,7 +75,7 @@
lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
-- {* same as @{text WilsonRuss} *}
apply (unfold zcong_def)
- apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
+ apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
apply (simp add: algebra_simps)
apply (subst dvd_minus_iff)
@@ -213,7 +213,7 @@
lemma reciP_sym: "zprime p ==> symP (reciR p)"
apply (unfold reciR_def symP_def)
- apply (simp add: zmult_commute)
+ apply (simp add: mult_commute)
apply auto
done
@@ -240,7 +240,7 @@
apply (subst setprod_insert)
apply (auto simp add: fin_bijER)
apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
- apply (simp add: zmult_assoc)
+ apply (simp add: mult_assoc)
apply (rule zcong_zmult)
apply auto
done
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Sep 06 19:03:41 2011 -0700
@@ -80,7 +80,7 @@
lemma inv_not_p_minus_1_aux:
"[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)"
apply (unfold zcong_def)
- apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2)
+ apply (simp add: diff_diff_eq diff_diff_eq2 right_diff_distrib)
apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans)
apply (simp add: algebra_simps)
apply (subst dvd_minus_iff)
@@ -123,13 +123,13 @@
nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
apply (subst int_int_eq [symmetric])
apply (simp add: zmult_int [symmetric])
- apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2)
+ apply (simp add: left_diff_distrib right_diff_distrib)
done
lemma zcong_zpower_zmult:
"[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
apply (induct z)
- apply (auto simp add: zpower_zadd_distrib)
+ apply (auto simp add: power_add)
apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
apply (rule_tac [2] zcong_zmult, simp_all)
done
@@ -261,7 +261,7 @@
apply (subgoal_tac [5]
"zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
prefer 5
- apply (simp add: zmult_assoc)
+ apply (simp add: mult_assoc)
apply (rule_tac [5] zcong_zmult)
apply (rule_tac [5] inv_is_inv)
apply (tactic "clarify_tac @{context} 4")
--- a/src/HOL/Presburger.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Presburger.thy Tue Sep 06 19:03:41 2011 -0700
@@ -308,7 +308,7 @@
{fix x
have "P x \<longrightarrow> P (x + i * d)" using step.hyps by blast
also have "\<dots> \<longrightarrow> P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
- by (simp add:int_distrib zadd_ac)
+ by (simp add:int_distrib add_ac)
ultimately have "P x \<longrightarrow> P(x + (i + 1) * d)" by blast}
thus ?case ..
qed
--- a/src/HOL/RealDef.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/RealDef.thy Tue Sep 06 19:03:41 2011 -0700
@@ -1412,7 +1412,7 @@
by (insert real_of_nat_div2 [of n x], simp)
lemma real_of_int_real_of_nat: "real (int n) = real n"
-by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
+by (simp add: real_of_nat_def real_of_int_def)
lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
by (simp add: real_of_int_def real_of_nat_def)