--- a/NEWS Thu Sep 08 00:23:23 2011 +0200
+++ b/NEWS Wed Sep 07 19:24:28 2011 -0700
@@ -319,6 +319,7 @@
* Theory Complex_Main: Several redundant theorems have been removed or
replaced by more general versions. INCOMPATIBILITY.
+ real_of_int_real_of_nat ~> real_of_int_of_nat_eq
real_0_le_divide_iff ~> zero_le_divide_iff
realpow_two_disj ~> power2_eq_iff
real_squared_diff_one_factored ~> square_diff_one_factored
--- a/src/HOL/Algebra/IntRing.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Algebra/IntRing.thy Wed Sep 07 19:24:28 2011 -0700
@@ -35,8 +35,8 @@
apply (rule abelian_groupI, simp_all)
defer 1
apply (rule comm_monoidI, simp_all)
- apply (rule zadd_zmult_distrib)
-apply (fast intro: zadd_zminus_inverse2)
+ apply (rule left_distrib)
+apply (fast intro: left_minus)
done
(*
@@ -298,7 +298,7 @@
from this obtain x
where "1 = x * p" by best
from this [symmetric]
- have "p * x = 1" by (subst zmult_commute)
+ have "p * x = 1" by (subst mult_commute)
hence "\<bar>p * x\<bar> = 1" by simp
hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
from this and prime
--- a/src/HOL/Algebra/UnivPoly.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Sep 07 19:24:28 2011 -0700
@@ -1818,7 +1818,7 @@
lemma INTEG_cring: "cring INTEG"
by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
- zadd_zminus_inverse2 zadd_zmult_distrib)
+ left_minus left_distrib)
lemma INTEG_id_eval:
"UP_pre_univ_prop INTEG INTEG id"
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Wed Sep 07 19:24:28 2011 -0700
@@ -77,10 +77,10 @@
boogie_vc max (examine: L_14_5c L_14_5b L_14_5a)
proof boogie_cases
case L_14_5c
- thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
+ thus ?case by (metis less_le_not_le zle_add1_eq_le less_linear)
next
case L_14_5b
- thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq)
+ thus ?case by (metis less_le_not_le xt1(10) linorder_linear zless_add1_eq)
next
case L_14_5a
note max0 = `max0 = array 0`
--- a/src/HOL/Code_Numeral.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Code_Numeral.thy Wed Sep 07 19:24:28 2011 -0700
@@ -274,7 +274,7 @@
then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)"
by simp
then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)"
- unfolding int_mult zadd_int [symmetric] by simp
+ unfolding of_nat_mult of_nat_add by simp
then show ?thesis by (auto simp add: int_of_def mult_ac)
qed
--- a/src/HOL/Complex.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Complex.thy Wed Sep 07 19:24:28 2011 -0700
@@ -621,13 +621,6 @@
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
by (simp add: rcis_def cis_def)
-lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
-proof -
- have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
- by (simp only: power_mult_distrib right_distrib)
- thus ?thesis by simp
-qed
-
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
by (simp add: rcis_def cis_def norm_mult)
@@ -656,22 +649,11 @@
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
by (simp add: rcis_def)
-lemma complex_of_real_minus_one:
- "complex_of_real (-(1::real)) = -(1::complex)"
- by (simp add: complex_of_real_def complex_one_def)
-
lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
by (simp add: mult_assoc [symmetric])
-
-lemma cis_real_of_nat_Suc_mult:
- "cis (real (Suc n) * a) = cis a * cis (real n * a)"
- by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
-
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
-apply (induct_tac "n")
-apply (auto simp add: cis_real_of_nat_Suc_mult)
-done
+ by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
by (simp add: rcis_def power_mult_distrib DeMoivre)
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Sep 07 19:24:28 2011 -0700
@@ -295,7 +295,7 @@
unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
also have "\<dots> < pow2 (?E div 2) * 2"
by (rule mult_strict_left_mono, auto intro: E_mod_pow)
- also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
+ also have "\<dots> = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto
finally show ?thesis by auto
qed
finally show ?thesis
--- a/src/HOL/Decision_Procs/Cooper.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Sep 07 19:24:28 2011 -0700
@@ -1318,7 +1318,7 @@
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
- apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
+ apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
@@ -1330,7 +1330,7 @@
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
- apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
+ apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
--- a/src/HOL/GCD.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/GCD.thy Wed Sep 07 19:24:28 2011 -0700
@@ -485,16 +485,16 @@
done
lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
-by (metis gcd_red_int mod_add_self1 zadd_commute)
+by (metis gcd_red_int mod_add_self1 add_commute)
lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
-by (metis gcd_add1_int gcd_commute_int zadd_commute)
+by (metis gcd_add1_int gcd_commute_int add_commute)
lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
-by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
+by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute)
(* to do: differences, and all variations of addition rules
@@ -1030,8 +1030,7 @@
apply (subst mod_div_equality [of m n, symmetric])
(* applying simp here undoes the last substitution!
what is procedure cancel_div_mod? *)
- apply (simp only: field_simps zadd_int [symmetric]
- zmult_int [symmetric])
+ apply (simp only: field_simps of_nat_add of_nat_mult)
done
qed
@@ -1237,7 +1236,7 @@
lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
by (simp add: lcm_int_def lcm_nat_def zdiv_int
- zmult_int [symmetric] gcd_int_def)
+ of_nat_mult gcd_int_def)
lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
unfolding lcm_nat_def
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Sep 07 19:24:28 2011 -0700
@@ -93,7 +93,7 @@
have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
- unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even)
+ unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even)
apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed
subsection {* The odd/even result for faces of complete vertices, generalized. *}
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Sep 07 19:24:28 2011 -0700
@@ -4590,7 +4590,7 @@
hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto
hence "b : S1" using T_def b_def by auto
hence False using b_def assms unfolding rel_frontier_def by auto
-} ultimately show ?thesis using zless_le by auto
+} ultimately show ?thesis using less_le by auto
qed
--- a/src/HOL/NSA/NSComplex.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/NSA/NSComplex.thy Wed Sep 07 19:24:28 2011 -0700
@@ -561,8 +561,7 @@
"!!a. hcis (hypreal_of_nat (Suc n) * a) =
hcis a * hcis (hypreal_of_nat n * a)"
apply transfer
-apply (fold real_of_nat_def)
-apply (rule cis_real_of_nat_Suc_mult)
+apply (simp add: left_distrib cis_mult)
done
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
@@ -574,7 +573,7 @@
lemma hcis_hypreal_of_hypnat_Suc_mult:
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
hcis a * hcis (hypreal_of_hypnat n * a)"
-by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
+by transfer (simp add: left_distrib cis_mult)
lemma NSDeMoivre_ext:
"!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
--- a/src/HOL/Number_Theory/Primes.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Wed Sep 07 19:24:28 2011 -0700
@@ -174,7 +174,7 @@
EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
unfolding prime_int_altdef dvd_def
apply auto
- by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
+ by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
n > 0 --> (p dvd x^n --> p dvd x)"
@@ -220,7 +220,7 @@
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
proof
assume "?L" thus "?R"
- by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
+ by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
next
assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
qed
@@ -272,7 +272,7 @@
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
apply (rule prime_imp_coprime_int, assumption)
apply (unfold prime_int_altdef)
- apply (metis int_one_le_iff_zero_less zless_le)
+ apply (metis int_one_le_iff_zero_less less_le)
done
lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Sep 07 19:24:28 2011 -0700
@@ -766,7 +766,7 @@
lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
- multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
+ multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
--- a/src/HOL/Old_Number_Theory/Fib.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy Wed Sep 07 19:24:28 2011 -0700
@@ -87,7 +87,7 @@
else fib (Suc n) * fib (Suc n) + 1)"
apply (rule int_int_eq [THEN iffD1])
apply (simp add: fib_Cassini_int)
- apply (subst zdiff_int [symmetric])
+ apply (subst of_nat_diff)
apply (insert fib_Suc_gr_0 [of n], simp_all)
done
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Wed Sep 07 19:24:28 2011 -0700
@@ -699,7 +699,7 @@
lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
by (simp del: minus_mult_right [symmetric]
add: minus_mult_right nat_mult_distrib zgcd_def abs_if
- mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
+ mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult)
lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
by (simp add: abs_if zgcd_zmult_distrib2)
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Wed Sep 07 19:24:28 2011 -0700
@@ -122,7 +122,7 @@
lemma inv_inv_aux: "5 \<le> p ==>
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: of_nat_mult)
apply (simp add: left_diff_distrib right_diff_distrib)
done
--- a/src/HOL/RealDef.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/RealDef.thy Wed Sep 07 19:24:28 2011 -0700
@@ -1411,16 +1411,13 @@
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
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)
-
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)
lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
apply (subgoal_tac "real(int(nat x)) = real(nat x)")
apply force
- apply (simp only: real_of_int_real_of_nat)
+ apply (simp only: real_of_int_of_nat_eq)
done
lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
@@ -1534,7 +1531,7 @@
"real (number_of v :: nat) =
(if neg (number_of v :: int) then 0
else (number_of v :: real))"
-by (simp add: real_of_int_real_of_nat [symmetric])
+by (simp add: real_of_int_of_nat_eq [symmetric])
declaration {*
K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]
--- a/src/HOL/Word/Misc_Numeric.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Wed Sep 07 19:24:28 2011 -0700
@@ -312,7 +312,7 @@
apply safe
apply (simp add: dvd_eq_mod_eq_0 [symmetric])
apply (drule le_iff_add [THEN iffD1])
- apply (force simp: zpower_zadd_distrib)
+ apply (force simp: power_add)
apply (rule mod_pos_pos_trivial)
apply (simp)
apply (rule power_strict_increasing)
--- a/src/HOL/Word/Word.thy Thu Sep 08 00:23:23 2011 +0200
+++ b/src/HOL/Word/Word.thy Wed Sep 07 19:24:28 2011 -0700
@@ -1257,7 +1257,7 @@
word_of_int_Ex [of b]
word_of_int_Ex [of c]
by (auto simp: word_of_int_hom_syms [symmetric]
- zadd_0_right add_commute add_assoc add_left_commute
+ add_0_right add_commute add_assoc add_left_commute
mult_commute mult_assoc mult_left_commute
left_distrib right_distrib)
@@ -4219,7 +4219,7 @@
apply (rule rotater_eqs)
apply (simp add: word_size nat_mod_distrib)
apply (rule int_eq_0_conv [THEN iffD1])
- apply (simp only: zmod_int zadd_int [symmetric])
+ apply (simp only: zmod_int of_nat_add)
apply (simp add: rdmods)
done