--- a/src/HOL/Complex.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Complex.thy Wed Mar 19 17:06:02 2014 +0000
@@ -634,20 +634,32 @@
lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
by (metis im_complex_div_gt_0 not_le)
-lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
+lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
+apply (cases "finite s")
by (induct s rule: finite_induct) auto
-lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
+lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
+apply (cases "finite s")
+ by (induct s rule: finite_induct) auto
+
+lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
+apply (cases "finite s")
by (induct s rule: finite_induct) auto
-lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
+lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
+ by (metis Complex_setsum')
+
+lemma cnj_setsum: "cnj (setsum f s) = setsum (%x. cnj (f x)) s"
+apply (cases "finite s")
+ by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
+
+lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
+apply (cases "finite s")
by (induct s rule: finite_induct) auto
-lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
- by (metis Complex_setsum')
-
-lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
- by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
+lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
+apply (cases "finite s")
+ by (induct s rule: finite_induct) auto
lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj
--- a/src/HOL/Deriv.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Deriv.thy Wed Mar 19 17:06:02 2014 +0000
@@ -1203,7 +1203,7 @@
lemma DERIV_const_ratio_const2:
fixes f :: "real => real"
shows "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
-apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
+apply (rule_tac c1 = "b-a" in mult_right_cancel [THEN iffD1])
apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc)
done
--- a/src/HOL/Library/Poly_Deriv.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Library/Poly_Deriv.thy Wed Mar 19 17:06:02 2014 +0000
@@ -128,7 +128,7 @@
\<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
apply (drule_tac f = "poly p" in MVT, auto)
apply (rule_tac x = z in exI)
-apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique])
+apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
done
text{*Lemmas for Derivatives*}
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Mar 19 17:06:02 2014 +0000
@@ -1203,8 +1203,8 @@
proof -
have 1: "((\<lambda>i. Im (f i)) ---> Im l) F"
by (metis assms(1) tendsto_Im)
- then have "((\<lambda>i. Im (f i)) ---> 0) F"
- by (smt2 Lim_eventually assms(3) assms(4) complex_is_Real_iff eventually_elim2)
+ then have "((\<lambda>i. Im (f i)) ---> 0) F" using assms
+ by (metis (mono_tags, lifting) Lim_eventually complex_is_Real_iff eventually_mono)
then show ?thesis using 1
by (metis 1 assms(2) complex_is_Real_iff tendsto_unique)
qed
@@ -1233,16 +1233,8 @@
apply (induct n, auto)
by (metis dual_order.trans le_cases le_neq_implies_less norm_triangle_mono)
-(*Replaces the one in Series*)
-lemma summable_comparison_test:
- fixes f:: "nat \<Rightarrow> 'a::banach"
- shows "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
-apply (auto simp: Series.summable_Cauchy)
-apply (drule_tac x = e in spec, auto)
-apply (rule_tac x="max N Na" in exI, auto)
-by (smt2 norm_setsum_bound)
-(*MOVE TO Finite_Cartesian_Product*)
+(*MOVE? But not to Finite_Cartesian_Product*)
lemma sums_vec_nth :
assumes "f sums a"
shows "(\<lambda>x. f x $ i) sums a $ i"
@@ -1255,23 +1247,6 @@
using assms unfolding summable_def
by (blast intro: sums_vec_nth)
-(*REPLACE THE ONES IN COMPLEX.THY*)
-lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
-apply (cases "finite s")
- by (induct s rule: finite_induct) auto
-
-lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
-apply (cases "finite s")
- by (induct s rule: finite_induct) auto
-
-lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
-apply (cases "finite s")
- by (induct s rule: finite_induct) auto
-
-lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
-apply (cases "finite s")
- by (induct s rule: finite_induct) auto
-
lemma sums_Re:
assumes "f sums a"
shows "(\<lambda>x. Re (f x)) sums Re a"
@@ -1306,7 +1281,7 @@
have g: "\<And>n. cmod (g n) = Re (g n)" using assms
by (metis abs_of_nonneg in_Reals_norm)
show ?thesis
- apply (rule summable_comparison_test [where g = "\<lambda>n. norm (g n)" and N=N])
+ apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
using sg
apply (auto simp: summable_def)
apply (rule_tac x="Re s" in exI)
@@ -1324,9 +1299,6 @@
done
-(* ------------------------------------------------------------------------- *)
-(* A kind of complex Taylor theorem. *)
-(* ------------------------------------------------------------------------- *)
lemma setsum_Suc_reindex:
@@ -1334,17 +1306,8 @@
shows "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
by (induct n) auto
-(*REPLACE THE REAL VERSIONS*)
-lemma mult_left_cancel:
- fixes c:: "'a::ring_no_zero_divisors"
- shows "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
-by simp
-lemma mult_right_cancel:
- fixes c:: "'a::ring_no_zero_divisors"
- shows "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
-by simp
-
+text{*A kind of complex Taylor theorem.*}
lemma complex_taylor:
assumes s: "convex s"
and f: "\<And>i x. x \<in> s \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within s)"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Mar 19 17:06:02 2014 +0000
@@ -799,7 +799,7 @@
by (rule norm_cauchy_schwarz)
finally show ?thesis
using False x(1)
- by (auto simp add: real_mult_left_cancel)
+ by (auto simp add: mult_left_cancel)
next
case True
then show ?thesis
--- a/src/HOL/NSA/HDeriv.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/NSA/HDeriv.thy Wed Mar 19 17:06:02 2014 +0000
@@ -362,7 +362,7 @@
nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
apply (subst nonzero_inverse_minus_eq [symmetric])
using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
- apply (simp add: field_simps)
+ apply (simp add: field_simps)
done
ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
- (inverse (star_of x) * inverse (star_of x))"
@@ -451,7 +451,7 @@
apply (drule bspec, auto)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
apply (frule_tac b1 = "hypreal_of_real (D) + y"
- in hypreal_mult_right_cancel [THEN iffD2])
+ in mult_right_cancel [THEN iffD2])
apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
apply assumption
apply (simp add: times_divide_eq_right [symmetric])
--- a/src/HOL/NSA/HyperDef.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/NSA/HyperDef.thy Wed Mar 19 17:06:02 2014 +0000
@@ -168,7 +168,7 @@
declare Abs_star_inject [simp] Abs_star_inverse [simp]
declare equiv_starrel [THEN eq_equiv_class_iff, simp]
-subsection{*@{term hypreal_of_real}:
+subsection{*@{term hypreal_of_real}:
the Injection from @{typ real} to @{typ hypreal}*}
lemma inj_star_of: "inj star_of"
@@ -207,7 +207,7 @@
by (simp only: star_inverse_def starfun_star_n)
lemma star_n_le:
- "star_n X \<le> star_n Y =
+ "star_n X \<le> star_n Y =
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
by (simp only: star_le_def starP2_star_n)
@@ -233,12 +233,6 @@
lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
by auto
-lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
-by auto
-
-lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
-by auto
-
lemma hypreal_omega_gt_zero [simp]: "0 < omega"
by (simp add: omega_def star_n_zero_num star_n_less)
@@ -250,18 +244,18 @@
text{*A few lemmas first*}
-lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
+lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
(\<exists>y. {n::nat. x = real n} = {y})"
by force
lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
-lemma not_ex_hypreal_of_real_eq_omega:
+lemma not_ex_hypreal_of_real_eq_omega:
"~ (\<exists>x. hypreal_of_real x = omega)"
apply (simp add: omega_def)
apply (simp add: star_of_def star_n_eq_iff)
-apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric]
+apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric]
lemma_finite_omega_set [THEN FreeUltrafilterNat.finite])
done
@@ -272,7 +266,7 @@
real number*}
lemma lemma_epsilon_empty_singleton_disj:
- "{n::nat. x = inverse(real(Suc n))} = {} |
+ "{n::nat. x = inverse(real(Suc n))} = {} |
(\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
by auto
@@ -389,7 +383,7 @@
done
lemma hrealpow_three_squares_add_zero_iff [simp]:
- "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) =
+ "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) =
(x = 0 & y = 0 & z = 0)"
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
@@ -462,7 +456,7 @@
"\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
by transfer (rule power_inverse)
-
+
lemma hyperpow_hrabs:
"\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
by transfer (rule power_abs [symmetric])
--- a/src/HOL/NSA/NSA.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/NSA/NSA.thy Wed Mar 19 17:06:02 2014 +0000
@@ -473,7 +473,7 @@
lemma HInfinite_add_ge_zero:
"[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
-by (auto intro!: hypreal_add_zero_less_le_mono
+by (auto intro!: hypreal_add_zero_less_le_mono
simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def)
lemma HInfinite_add_ge_zero2:
@@ -533,7 +533,7 @@
by (erule hnorm_less_Infinitesimal, simp)
lemma Infinitesimal_interval:
- "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]
+ "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]
==> (x::hypreal) \<in> Infinitesimal"
by (auto simp add: Infinitesimal_def abs_less_iff)
@@ -546,7 +546,7 @@
lemma lemma_Infinitesimal_hyperpow:
"[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
apply (unfold Infinitesimal_def)
-apply (auto intro!: hyperpow_Suc_le_self2
+apply (auto intro!: hyperpow_Suc_le_self2
simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
done
@@ -735,7 +735,7 @@
by (simp add: approx_def)
lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"
-by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
+by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
mem_infmal_iff [THEN iffD1] approx_trans2)
lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)"
@@ -995,10 +995,10 @@
apply (simp add: divide_inverse mult_assoc)
done
-lemma Infinitesimal_SReal_divide:
+lemma Infinitesimal_SReal_divide:
"[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
apply (simp add: divide_inverse)
-apply (auto intro!: Infinitesimal_HFinite_mult
+apply (auto intro!: Infinitesimal_HFinite_mult
dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
done
@@ -1205,7 +1205,7 @@
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> x + -t \<le> r"
-apply (subgoal_tac "x \<le> t+r")
+apply (subgoal_tac "x \<le> t+r")
apply (auto intro: lemma_st_part_le1)
done
@@ -1214,7 +1214,7 @@
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> -(x + -t) \<le> r"
-apply (subgoal_tac "(t + -r \<le> x)")
+apply (subgoal_tac "(t + -r \<le> x)")
apply simp
apply (rule lemma_st_part_le2)
apply auto
@@ -1305,7 +1305,7 @@
apply (auto dest: order_less_trans)
done
-lemma HFinite_not_HInfinite:
+lemma HFinite_not_HInfinite:
assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
proof
assume x': "x \<in> HInfinite"
@@ -1404,7 +1404,7 @@
"[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h"
apply (rule approx_trans2)
-apply (auto intro: inverse_add_Infinitesimal_approx
+apply (auto intro: inverse_add_Infinitesimal_approx
simp add: mem_infmal_iff approx_minus_iff [symmetric])
done
@@ -1572,7 +1572,7 @@
lemma less_Infinitesimal_less:
"[| 0 < x; (x::hypreal) \<notin>Infinitesimal; e :Infinitesimal |] ==> e < x"
apply (rule ccontr)
-apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
+apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
done
@@ -1673,7 +1673,7 @@
"[| u \<in> Infinitesimal; v \<in> Infinitesimal;
hypreal_of_real x + u \<le> hypreal_of_real y + v |]
==> x \<le> y"
-by (blast intro: star_of_le [THEN iffD1]
+by (blast intro: star_of_le [THEN iffD1]
intro!: hypreal_of_real_le_add_Infininitesimal_cancel)
lemma hypreal_of_real_less_Infinitesimal_le_zero:
@@ -1721,7 +1721,7 @@
"(x::hypreal)*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_interval2, assumption)
apply (rule_tac [2] zero_le_square, simp)
-apply (insert zero_le_square [of y])
+apply (insert zero_le_square [of y])
apply (insert zero_le_square [of z], simp del:zero_le_square)
done
@@ -1729,7 +1729,7 @@
"(x::hypreal)*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_bounded, assumption)
apply (rule_tac [2] zero_le_square)
-apply (insert zero_le_square [of y])
+apply (insert zero_le_square [of y])
apply (insert zero_le_square [of z], simp del:zero_le_square)
done
@@ -1812,8 +1812,8 @@
lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
by (auto dest!: st_approx_self elim!: approx_trans3)
-lemma approx_st_eq:
- assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
+lemma approx_st_eq:
+ assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
shows "st x = st y"
proof -
have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
@@ -1883,7 +1883,7 @@
lemma st_inverse:
"[| x \<in> HFinite; st x \<noteq> 0 |]
==> st(inverse x) = inverse (st x)"
-apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1])
+apply (rule_tac c1 = "st x" in mult_left_cancel [THEN iffD1])
apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
apply (subst right_inverse, auto)
done
@@ -1897,7 +1897,7 @@
by (blast intro: st_HFinite st_approx_self approx_st_eq)
lemma Infinitesimal_add_st_less:
- "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |]
+ "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |]
==> st x + u < st y"
apply (drule st_SReal)+
apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
@@ -1933,7 +1933,7 @@
lemma st_hrabs: "x \<in> HFinite ==> abs(st x) = st(abs x)"
apply (simp add: linorder_not_le st_zero_le abs_if st_minus
linorder_not_less)
-apply (auto dest!: st_zero_ge [OF order_less_imp_le])
+apply (auto dest!: st_zero_ge [OF order_less_imp_le])
done
@@ -1943,7 +1943,7 @@
subsubsection {* @{term HFinite} *}
lemma HFinite_FreeUltrafilterNat:
- "star_n X \<in> HFinite
+ "star_n X \<in> HFinite
==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
apply (auto simp add: HFinite_def SReal_def)
apply (rule_tac x=r in exI)
@@ -2273,10 +2273,10 @@
"\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
==> star_n X - star_n Y \<in> Infinitesimal"
by (auto intro!: bexI
- dest: FreeUltrafilterNat_inverse_real_of_posnat
+ dest: FreeUltrafilterNat_inverse_real_of_posnat
FreeUltrafilterNat.Int
- intro: order_less_trans FreeUltrafilterNat.subset
- simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff
+ intro: order_less_trans FreeUltrafilterNat.subset
+ simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff
star_n_inverse)
end
--- a/src/HOL/Real.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Real.thy Wed Mar 19 17:06:02 2014 +0000
@@ -974,12 +974,6 @@
text {* BH: These lemmas should not be necessary; they should be
covered by existing simp rules and simplification procedures. *}
-lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
-by simp (* redundant with mult_cancel_left *)
-
-lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
-by simp (* redundant with mult_cancel_right *)
-
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
by simp (* solved by linordered_ring_less_cancel_factor simproc *)
--- a/src/HOL/Rings.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Rings.thy Wed Mar 19 17:06:02 2014 +0000
@@ -376,6 +376,12 @@
thus ?thesis by simp
qed
+lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
+by simp
+
+lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
+by simp
+
end
class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
--- a/src/HOL/Series.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Series.thy Wed Mar 19 17:06:02 2014 +0000
@@ -461,6 +461,10 @@
apply (auto intro: setsum_mono simp add: abs_less_iff)
done
+(*A better argument order*)
+lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
+by (rule summable_comparison_test) auto
+
subsection {* The Ratio Test*}
lemma summable_ratio_test:
--- a/src/HOL/Transcendental.thy Wed Mar 19 14:55:47 2014 +0000
+++ b/src/HOL/Transcendental.thy Wed Mar 19 17:06:02 2014 +0000
@@ -2396,15 +2396,6 @@
thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
qed
-lemma real_mult_inverse_cancel:
- "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
- ==> inverse x * y < inverse x1 * u"
- by (metis field_divide_inverse mult_commute mult_assoc pos_divide_less_eq pos_less_divide_eq)
-
-lemma real_mult_inverse_cancel2:
- "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
- by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
-
lemmas realpow_num_eq_if = power_eq_if
lemma sumr_pos_lt_pair:
@@ -3208,7 +3199,7 @@
lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
apply (rule power_inverse [THEN subst])
- apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
+ apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
apply (auto dest: field_power_not_zero
simp add: power_mult_distrib distrib_right power_divide tan_def
mult_assoc power_inverse [symmetric])