# HG changeset patch # User huffman # Date 1315361021 25200 # Node ID d4d33a4d7548ac41287e70deb4a211b142af9077 # Parent d96550db3d77f7736532d62ea0876af58507b533 avoid using legacy theorem names diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Divides.thy --- 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 diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/GCD.thy --- 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 \ m=0 \ 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 \ m=1 \ n=1" by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat) diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Import/HOLLightInt.thy --- 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 = (\u. \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 \ 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: "\(n :: nat). real (i :: int) = real n \ real i = - real n" @@ -56,19 +56,19 @@ lemma DEF_int_max: "max = (\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 = (\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: "(\n. x = int n) \ (\n. x = - int n)" @@ -119,7 +119,7 @@ lemma hl_mod_div: "n \ (0\int) \ 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: "(\(x :: int) y z. x + (y + z) = x + y + z) \ @@ -131,7 +131,7 @@ (\(x :: int). int 0 * x = int 0) \ (\(x :: int) y z. x * (y + z) = x * y + x * z) \ (\(x :: int). x ^ 0 = int 1) \ (\(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 \ m = hl_div m n * n + hl_mod m n \ int 0 \ hl_mod m n \ 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. \a b. (int 0) \ (d (a, b)) \ (d (a, b)) dvd a \ (d (a, b)) dvd b \ (\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) diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Library/Float.thy --- 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) \ real (x * c div y) * inverse (real c)" proof - have "c * (x div y) + 0 \ 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 \ 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) \ 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 "\ \ y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le]) - also have "\ = y * (?X div y + 1)" unfolding zadd_zmult_distrib2 by auto + also have "\ = y * (?X div y + 1)" unfolding right_distrib by auto finally have "real ?X \ 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) \ real y * real (?X div y + 1) / (real y * 2^?l)" by (rule divide_right_mono, simp only: `0 \ real y * 2^?l`) @@ -1144,7 +1144,7 @@ have "2^(prec - 1) * m \ 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto also have "\ = 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 \ 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1) hence "2^(prec - 1) \ 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 "\ \ (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 "\ \ (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) \ 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 \ 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)) \ 1 * 2^(nat ?l)" unfolding zmult_1 real_of_int_less_iff[symmetric] by auto + hence mod_uneq: "real (m mod 2^(nat ?l)) \ 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 "\ = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Nat_Numeral.thy --- 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: diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/Chinese.thy --- 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 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i \ [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") prefer 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]) diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/Euler.thy --- 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 \ (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 diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/EulerFermat.thy --- 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 diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/EvenOdd.thy --- 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 \ zEven; y \ zEven |] ==> x + y \ 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 \ zEven ==> x * y \ zEven" @@ -93,12 +93,12 @@ lemma even_minus_even: "[| x \ zEven; y \ zEven |] ==> x - y \ 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 \ zOdd; y \ zOdd |] ==> x - y \ 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 \ zEven; y \ zOdd |] ==> x - y \ zOdd" @@ -109,13 +109,13 @@ lemma odd_minus_even: "[| x \ zOdd; y \ zEven |] ==> x - y \ 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 \ zOdd; y \ zOdd |] ==> x * y \ 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 \ zOdd) = (~ (x \ 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 diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/Finite2.thy --- 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 *} diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/Gauss.thy --- 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)" diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/Int2.thy --- 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 \ (x div z) * z" by simp then have "(x div z) * z \ (x div z) * z + x mod z" using modth by arith also have "\ = 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)); diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/IntPrimes.thy --- 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 \ 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 \ 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 \ 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 \ 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 \ b ==> b < m ==> [a = b] (mod m) ==> a = b" apply (unfold zcong_def dvd_def, auto) apply (drule_tac f = "\z. z mod m" in arg_cong) - apply (metis diff_add_cancel mod_pos_pos_trivial zadd_0 zadd_commute zmod_eq_0_iff 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 diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy --- 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 * (\x \ 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 \ zOdd ==> @@ -284,7 +284,7 @@ proof - fix a and b assume "~ q * a < p * b" and b1: "0 < b" and b2: "b \ (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 \ 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) + diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/WilsonBij.thy --- 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) * \A) (1 * 1) p") - apply (simp add: zmult_assoc) + apply (simp add: mult_assoc) apply (rule zcong_zmult) apply auto done diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Old_Number_Theory/WilsonRuss.thy --- 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) \ [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 * (\x\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") diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/Presburger.thy --- 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 \ P (x + i * d)" using step.hyps by blast also have "\ \ 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 \ P(x + (i + 1) * d)" by blast} thus ?case .. qed diff -r d96550db3d77 -r d4d33a4d7548 src/HOL/RealDef.thy --- 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)