--- a/src/HOL/Big_Operators.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Big_Operators.thy Tue May 18 06:28:42 2010 -0700
@@ -673,7 +673,7 @@
proof induct
case empty thus ?case by simp
next
- case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
+ case (insert x A) thus ?case by auto
qed
next
case False thus ?thesis by (simp add: setsum_def)
--- a/src/HOL/Groups.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Groups.thy Tue May 18 06:28:42 2010 -0700
@@ -605,7 +605,7 @@
then show ?thesis by simp
qed
-lemma add_nonneg_nonneg:
+lemma add_nonneg_nonneg [simp]:
assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
proof -
have "0 + 0 \<le> a + b"
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue May 18 06:28:42 2010 -0700
@@ -214,23 +214,8 @@
hence "\<exists>z. ?P z n" ..}
moreover
{assume o: "odd n"
- from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
- have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
- Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
- ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
- also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
- apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
- by (simp add: power2_eq_square)
- finally
- have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
- Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
- 1"
- apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
- using right_inverse[OF b']
- by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
have th0: "cmod (complex_of_real (cmod b) / b) = 1"
- apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
- by (simp add: real_sqrt_mult[symmetric] th0)
+ using b by (simp add: norm_divide)
from o have "\<exists>m. n = Suc (2*m)" by presburger+
then obtain m where m: "n = Suc (2*m)" by blast
from unimodular_reduce_norm[OF th0] o
--- a/src/HOL/Library/Lattice_Algebras.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy Tue May 18 06:28:42 2010 -0700
@@ -405,21 +405,15 @@
done
}
note b = this[OF refl[of a] refl[of b]]
- note addm = add_mono[of "0::'a" _ "0::'a", simplified]
- note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
have xy: "- ?x <= ?y"
apply (simp)
- apply (rule_tac y="0::'a" in order_trans)
- apply (rule addm2)
- apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
- apply (rule addm)
+ apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
done
have yx: "?y <= ?x"
apply (simp add:diff_def)
- apply (rule_tac y=0 in order_trans)
- apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
- apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
+ apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
+ apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
done
have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
--- a/src/HOL/MacLaurin.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/MacLaurin.thy Tue May 18 06:28:42 2010 -0700
@@ -383,6 +383,11 @@
text{*It is unclear why so many variant results are needed.*}
+lemma sin_expansion_lemma:
+ "sin (x + real (Suc m) * pi / 2) =
+ cos (x + real (m) * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+
lemma Maclaurin_sin_expansion2:
"\<exists>t. abs t \<le> abs x &
sin x =
@@ -394,7 +399,7 @@
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
@@ -414,7 +419,6 @@
apply (blast intro: elim:);
done
-
lemma Maclaurin_sin_expansion3:
"[| n > 0; 0 < x |] ==>
\<exists>t. 0 < t & t < x &
@@ -426,7 +430,7 @@
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -444,7 +448,7 @@
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -459,6 +463,10 @@
(if even m then -1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1"
by (induct "n", auto)
+lemma cos_expansion_lemma:
+ "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
+
lemma Maclaurin_cos_expansion:
"\<exists>t. abs t \<le> abs x &
cos x =
@@ -470,7 +478,7 @@
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
apply (case_tac "n", simp)
apply (simp del: setsum_op_ivl_Suc)
apply (rule ccontr, simp)
@@ -493,7 +501,7 @@
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -512,7 +520,7 @@
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
--- a/src/HOL/NSA/NSCA.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy Tue May 18 06:28:42 2010 -0700
@@ -279,13 +279,9 @@
"\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"
apply (rule Infinitesimal_hcmod_iff [THEN iffD2])
apply (simp add: hcmod_i)
-apply (rule Infinitesimal_sqrt)
apply (rule Infinitesimal_add)
apply (erule Infinitesimal_hrealpow, simp)
apply (erule Infinitesimal_hrealpow, simp)
-apply (rule add_nonneg_nonneg)
-apply (rule zero_le_power2)
-apply (rule zero_le_power2)
done
lemma hcomplex_Infinitesimal_iff:
--- a/src/HOL/Nat.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Nat.thy Tue May 18 06:28:42 2010 -0700
@@ -1294,15 +1294,11 @@
begin
lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
- apply (induct m, simp_all)
- apply (erule order_trans)
- apply (rule ord_le_eq_trans [OF _ add_commute])
- apply (rule less_add_one [THEN less_imp_le])
- done
+ by (induct m) simp_all
lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
apply (induct m n rule: diff_induct, simp_all)
- apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
+ apply (rule add_pos_nonneg [OF zero_less_one zero_le_imp_of_nat])
done
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
--- a/src/HOL/RealDef.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/RealDef.thy Tue May 18 06:28:42 2010 -0700
@@ -1620,14 +1620,6 @@
"(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
by (rule sum_power2_eq_zero_iff)
-text {* FIXME: declare this [simp] for all types, or not at all *}
-lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
-by (rule sum_power2_ge_zero)
-
-text {* FIXME: declare this [simp] for all types, or not at all *}
-lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
-by (intro add_nonneg_nonneg zero_le_power2)
-
lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
by (rule_tac y = 0 in order_trans, auto)
--- a/src/HOL/Rings.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Rings.thy Tue May 18 06:28:42 2010 -0700
@@ -956,7 +956,7 @@
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
by (auto simp add: abs_if not_less)
(auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
- auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
+ auto intro!: less_imp_le add_neg_neg)
qed (auto simp add: abs_if)
lemma zero_le_square [simp]: "0 \<le> a * a"
--- a/src/HOL/Transcendental.thy Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Transcendental.thy Tue May 18 06:28:42 2010 -0700
@@ -2580,18 +2580,6 @@
lemma tan_60: "tan (pi / 3) = sqrt 3"
unfolding tan_def by (simp add: sin_60 cos_60)
-text{*NEEDED??*}
-lemma [simp]:
- "sin (x + 1 / 2 * real (Suc m) * pi) =
- cos (x + 1 / 2 * real (m) * pi)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
-
-text{*NEEDED??*}
-lemma [simp]:
- "sin (x + real (Suc m) * pi / 2) =
- cos (x + real (m) * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
-
lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
by (auto intro!: DERIV_intros)
@@ -2620,16 +2608,6 @@
apply (subst sin_add, simp)
done
-(*NEEDED??*)
-lemma [simp]:
- "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
-apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
-done
-
-(*NEEDED??*)
-lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
-
lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)