Some rationalisation of basic lemmas
authorpaulson <lp15@cam.ac.uk>
Wed Mar 19 17:06:02 2014 +0000 (2014-03-19)
changeset 56217dc429a5b13c4
parent 56216 76ff0a15d202
child 56218 1c3f1f2431f9
Some rationalisation of basic lemmas
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Library/Poly_Deriv.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Mar 19 14:55:47 2014 +0000
     1.2 +++ b/src/HOL/Complex.thy	Wed Mar 19 17:06:02 2014 +0000
     1.3 @@ -634,20 +634,32 @@
     1.4  lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
     1.5    by (metis im_complex_div_gt_0 not_le)
     1.6  
     1.7 -lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
     1.8 +lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
     1.9 +apply (cases "finite s")
    1.10    by (induct s rule: finite_induct) auto
    1.11  
    1.12 -lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
    1.13 +lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
    1.14 +apply (cases "finite s")
    1.15 +  by (induct s rule: finite_induct) auto
    1.16 +
    1.17 +lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
    1.18 +apply (cases "finite s")
    1.19    by (induct s rule: finite_induct) auto
    1.20  
    1.21 -lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
    1.22 +lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
    1.23 +  by (metis Complex_setsum')
    1.24 +
    1.25 +lemma cnj_setsum: "cnj (setsum f s) = setsum (%x. cnj (f x)) s"
    1.26 +apply (cases "finite s")
    1.27 +  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
    1.28 +
    1.29 +lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
    1.30 +apply (cases "finite s")
    1.31    by (induct s rule: finite_induct) auto
    1.32  
    1.33 -lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
    1.34 -  by (metis Complex_setsum')
    1.35 -
    1.36 -lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
    1.37 -  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
    1.38 +lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
    1.39 +apply (cases "finite s")
    1.40 +  by (induct s rule: finite_induct) auto
    1.41  
    1.42  lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
    1.43  by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj 
     2.1 --- a/src/HOL/Deriv.thy	Wed Mar 19 14:55:47 2014 +0000
     2.2 +++ b/src/HOL/Deriv.thy	Wed Mar 19 17:06:02 2014 +0000
     2.3 @@ -1203,7 +1203,7 @@
     2.4  lemma DERIV_const_ratio_const2:
     2.5    fixes f :: "real => real"
     2.6    shows "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
     2.7 -apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
     2.8 +apply (rule_tac c1 = "b-a" in mult_right_cancel [THEN iffD1])
     2.9  apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc)
    2.10  done
    2.11  
     3.1 --- a/src/HOL/Library/Poly_Deriv.thy	Wed Mar 19 14:55:47 2014 +0000
     3.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Wed Mar 19 17:06:02 2014 +0000
     3.3 @@ -128,7 +128,7 @@
     3.4       \<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
     3.5  apply (drule_tac f = "poly p" in MVT, auto)
     3.6  apply (rule_tac x = z in exI)
     3.7 -apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique])
     3.8 +apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
     3.9  done
    3.10  
    3.11  text{*Lemmas for Derivatives*}
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Mar 19 14:55:47 2014 +0000
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Mar 19 17:06:02 2014 +0000
     4.3 @@ -1203,8 +1203,8 @@
     4.4  proof -
     4.5    have 1: "((\<lambda>i. Im (f i)) ---> Im l) F"
     4.6      by (metis assms(1) tendsto_Im) 
     4.7 -  then have  "((\<lambda>i. Im (f i)) ---> 0) F"
     4.8 -    by (smt2 Lim_eventually assms(3) assms(4) complex_is_Real_iff eventually_elim2)
     4.9 +  then have  "((\<lambda>i. Im (f i)) ---> 0) F" using assms
    4.10 +    by (metis (mono_tags, lifting) Lim_eventually complex_is_Real_iff eventually_mono)
    4.11    then show ?thesis using 1
    4.12      by (metis 1 assms(2) complex_is_Real_iff tendsto_unique) 
    4.13  qed
    4.14 @@ -1233,16 +1233,8 @@
    4.15  apply (induct n, auto)
    4.16  by (metis dual_order.trans le_cases le_neq_implies_less norm_triangle_mono)
    4.17  
    4.18 -(*Replaces the one in Series*)
    4.19 -lemma summable_comparison_test:
    4.20 -  fixes f:: "nat \<Rightarrow> 'a::banach" 
    4.21 -  shows "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
    4.22 -apply (auto simp: Series.summable_Cauchy)  
    4.23 -apply (drule_tac x = e in spec, auto)
    4.24 -apply (rule_tac x="max N Na" in exI, auto)
    4.25 -by (smt2 norm_setsum_bound)
    4.26  
    4.27 -(*MOVE TO Finite_Cartesian_Product*)
    4.28 +(*MOVE? But not to Finite_Cartesian_Product*)
    4.29  lemma sums_vec_nth :
    4.30    assumes "f sums a"
    4.31    shows "(\<lambda>x. f x $ i) sums a $ i"
    4.32 @@ -1255,23 +1247,6 @@
    4.33  using assms unfolding summable_def
    4.34  by (blast intro: sums_vec_nth)
    4.35  
    4.36 -(*REPLACE THE ONES IN COMPLEX.THY*)
    4.37 -lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
    4.38 -apply (cases "finite s")
    4.39 -  by (induct s rule: finite_induct) auto
    4.40 -
    4.41 -lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
    4.42 -apply (cases "finite s")
    4.43 -  by (induct s rule: finite_induct) auto
    4.44 -
    4.45 -lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
    4.46 -apply (cases "finite s")
    4.47 -  by (induct s rule: finite_induct) auto
    4.48 -
    4.49 -lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
    4.50 -apply (cases "finite s")
    4.51 -  by (induct s rule: finite_induct) auto
    4.52 -
    4.53  lemma sums_Re:
    4.54    assumes "f sums a"
    4.55    shows "(\<lambda>x. Re (f x)) sums Re a"
    4.56 @@ -1306,7 +1281,7 @@
    4.57    have g: "\<And>n. cmod (g n) = Re (g n)" using assms
    4.58      by (metis abs_of_nonneg in_Reals_norm)
    4.59    show ?thesis
    4.60 -    apply (rule summable_comparison_test [where g = "\<lambda>n. norm (g n)" and N=N])
    4.61 +    apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
    4.62      using sg
    4.63      apply (auto simp: summable_def)
    4.64      apply (rule_tac x="Re s" in exI)
    4.65 @@ -1324,9 +1299,6 @@
    4.66  done
    4.67  
    4.68  
    4.69 -(* ------------------------------------------------------------------------- *)
    4.70 -(* A kind of complex Taylor theorem.                                         *)
    4.71 -(* ------------------------------------------------------------------------- *)
    4.72  
    4.73  
    4.74  lemma setsum_Suc_reindex:
    4.75 @@ -1334,17 +1306,8 @@
    4.76      shows  "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
    4.77  by (induct n) auto
    4.78  
    4.79 -(*REPLACE THE REAL VERSIONS*)
    4.80 -lemma mult_left_cancel:
    4.81 -  fixes c:: "'a::ring_no_zero_divisors"
    4.82 -  shows "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
    4.83 -by simp 
    4.84  
    4.85 -lemma mult_right_cancel:
    4.86 -  fixes c:: "'a::ring_no_zero_divisors"
    4.87 -  shows "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
    4.88 -by simp 
    4.89 -
    4.90 +text{*A kind of complex Taylor theorem.*}
    4.91  lemma complex_taylor:
    4.92    assumes s: "convex s" 
    4.93        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)"
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Mar 19 14:55:47 2014 +0000
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Mar 19 17:06:02 2014 +0000
     5.3 @@ -799,7 +799,7 @@
     5.4        by (rule norm_cauchy_schwarz)
     5.5      finally show ?thesis
     5.6        using False x(1)
     5.7 -      by (auto simp add: real_mult_left_cancel)
     5.8 +      by (auto simp add: mult_left_cancel)
     5.9    next
    5.10      case True
    5.11      then show ?thesis
     6.1 --- a/src/HOL/NSA/HDeriv.thy	Wed Mar 19 14:55:47 2014 +0000
     6.2 +++ b/src/HOL/NSA/HDeriv.thy	Wed Mar 19 17:06:02 2014 +0000
     6.3 @@ -362,7 +362,7 @@
     6.4          nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
     6.5        apply (subst nonzero_inverse_minus_eq [symmetric])
     6.6        using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
     6.7 -      apply (simp add: field_simps) 
     6.8 +      apply (simp add: field_simps)
     6.9        done
    6.10      ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
    6.11        - (inverse (star_of x) * inverse (star_of x))"
    6.12 @@ -451,7 +451,7 @@
    6.13  apply (drule bspec, auto)
    6.14  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
    6.15  apply (frule_tac b1 = "hypreal_of_real (D) + y"
    6.16 -        in hypreal_mult_right_cancel [THEN iffD2])
    6.17 +        in mult_right_cancel [THEN iffD2])
    6.18  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)
    6.19  apply assumption
    6.20  apply (simp add: times_divide_eq_right [symmetric])
     7.1 --- a/src/HOL/NSA/HyperDef.thy	Wed Mar 19 14:55:47 2014 +0000
     7.2 +++ b/src/HOL/NSA/HyperDef.thy	Wed Mar 19 17:06:02 2014 +0000
     7.3 @@ -168,7 +168,7 @@
     7.4  declare Abs_star_inject [simp] Abs_star_inverse [simp]
     7.5  declare equiv_starrel [THEN eq_equiv_class_iff, simp]
     7.6  
     7.7 -subsection{*@{term hypreal_of_real}: 
     7.8 +subsection{*@{term hypreal_of_real}:
     7.9              the Injection from @{typ real} to @{typ hypreal}*}
    7.10  
    7.11  lemma inj_star_of: "inj star_of"
    7.12 @@ -207,7 +207,7 @@
    7.13  by (simp only: star_inverse_def starfun_star_n)
    7.14  
    7.15  lemma star_n_le:
    7.16 -      "star_n X \<le> star_n Y =  
    7.17 +      "star_n X \<le> star_n Y =
    7.18         ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
    7.19  by (simp only: star_le_def starP2_star_n)
    7.20  
    7.21 @@ -233,12 +233,6 @@
    7.22  lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
    7.23  by auto
    7.24  
    7.25 -lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
    7.26 -by auto
    7.27 -    
    7.28 -lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
    7.29 -by auto
    7.30 -
    7.31  lemma hypreal_omega_gt_zero [simp]: "0 < omega"
    7.32  by (simp add: omega_def star_n_zero_num star_n_less)
    7.33  
    7.34 @@ -250,18 +244,18 @@
    7.35  
    7.36  text{*A few lemmas first*}
    7.37  
    7.38 -lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
    7.39 +lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |
    7.40        (\<exists>y. {n::nat. x = real n} = {y})"
    7.41  by force
    7.42  
    7.43  lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
    7.44  by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
    7.45  
    7.46 -lemma not_ex_hypreal_of_real_eq_omega: 
    7.47 +lemma not_ex_hypreal_of_real_eq_omega:
    7.48        "~ (\<exists>x. hypreal_of_real x = omega)"
    7.49  apply (simp add: omega_def)
    7.50  apply (simp add: star_of_def star_n_eq_iff)
    7.51 -apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] 
    7.52 +apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric]
    7.53              lemma_finite_omega_set [THEN FreeUltrafilterNat.finite])
    7.54  done
    7.55  
    7.56 @@ -272,7 +266,7 @@
    7.57   real number*}
    7.58  
    7.59  lemma lemma_epsilon_empty_singleton_disj:
    7.60 -     "{n::nat. x = inverse(real(Suc n))} = {} |  
    7.61 +     "{n::nat. x = inverse(real(Suc n))} = {} |
    7.62        (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
    7.63  by auto
    7.64  
    7.65 @@ -389,7 +383,7 @@
    7.66  done
    7.67  
    7.68  lemma hrealpow_three_squares_add_zero_iff [simp]:
    7.69 -     "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
    7.70 +     "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) =
    7.71        (x = 0 & y = 0 & z = 0)"
    7.72  by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
    7.73  
    7.74 @@ -462,7 +456,7 @@
    7.75    "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
    7.76     \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
    7.77  by transfer (rule power_inverse)
    7.78 -  
    7.79 +
    7.80  lemma hyperpow_hrabs:
    7.81    "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
    7.82  by transfer (rule power_abs [symmetric])
     8.1 --- a/src/HOL/NSA/NSA.thy	Wed Mar 19 14:55:47 2014 +0000
     8.2 +++ b/src/HOL/NSA/NSA.thy	Wed Mar 19 17:06:02 2014 +0000
     8.3 @@ -473,7 +473,7 @@
     8.4  
     8.5  lemma HInfinite_add_ge_zero:
     8.6       "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
     8.7 -by (auto intro!: hypreal_add_zero_less_le_mono 
     8.8 +by (auto intro!: hypreal_add_zero_less_le_mono
     8.9         simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def)
    8.10  
    8.11  lemma HInfinite_add_ge_zero2:
    8.12 @@ -533,7 +533,7 @@
    8.13  by (erule hnorm_less_Infinitesimal, simp)
    8.14  
    8.15  lemma Infinitesimal_interval:
    8.16 -      "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |] 
    8.17 +      "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]
    8.18         ==> (x::hypreal) \<in> Infinitesimal"
    8.19  by (auto simp add: Infinitesimal_def abs_less_iff)
    8.20  
    8.21 @@ -546,7 +546,7 @@
    8.22  lemma lemma_Infinitesimal_hyperpow:
    8.23       "[| (x::hypreal) \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
    8.24  apply (unfold Infinitesimal_def)
    8.25 -apply (auto intro!: hyperpow_Suc_le_self2 
    8.26 +apply (auto intro!: hyperpow_Suc_le_self2
    8.27            simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
    8.28  done
    8.29  
    8.30 @@ -735,7 +735,7 @@
    8.31  by (simp add: approx_def)
    8.32  
    8.33  lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"
    8.34 -by (blast intro: Infinitesimal_minus_iff [THEN iffD2] 
    8.35 +by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
    8.36                      mem_infmal_iff [THEN iffD1] approx_trans2)
    8.37  
    8.38  lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)"
    8.39 @@ -995,10 +995,10 @@
    8.40  apply (simp add: divide_inverse mult_assoc)
    8.41  done
    8.42  
    8.43 -lemma Infinitesimal_SReal_divide: 
    8.44 +lemma Infinitesimal_SReal_divide:
    8.45    "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
    8.46  apply (simp add: divide_inverse)
    8.47 -apply (auto intro!: Infinitesimal_HFinite_mult 
    8.48 +apply (auto intro!: Infinitesimal_HFinite_mult
    8.49              dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
    8.50  done
    8.51  
    8.52 @@ -1205,7 +1205,7 @@
    8.53           isLub Reals {s. s \<in> Reals & s < x} t;
    8.54           r \<in> Reals; 0 < r |]
    8.55        ==> x + -t \<le> r"
    8.56 -apply (subgoal_tac "x \<le> t+r") 
    8.57 +apply (subgoal_tac "x \<le> t+r")
    8.58  apply (auto intro: lemma_st_part_le1)
    8.59  done
    8.60  
    8.61 @@ -1214,7 +1214,7 @@
    8.62           isLub Reals {s. s \<in> Reals & s < x} t;
    8.63           r \<in> Reals;  0 < r |]
    8.64        ==> -(x + -t) \<le> r"
    8.65 -apply (subgoal_tac "(t + -r \<le> x)") 
    8.66 +apply (subgoal_tac "(t + -r \<le> x)")
    8.67  apply simp
    8.68  apply (rule lemma_st_part_le2)
    8.69  apply auto
    8.70 @@ -1305,7 +1305,7 @@
    8.71  apply (auto dest: order_less_trans)
    8.72  done
    8.73  
    8.74 -lemma HFinite_not_HInfinite: 
    8.75 +lemma HFinite_not_HInfinite:
    8.76    assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
    8.77  proof
    8.78    assume x': "x \<in> HInfinite"
    8.79 @@ -1404,7 +1404,7 @@
    8.80       "[| x \<in> HFinite - Infinitesimal;
    8.81           h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h"
    8.82  apply (rule approx_trans2)
    8.83 -apply (auto intro: inverse_add_Infinitesimal_approx 
    8.84 +apply (auto intro: inverse_add_Infinitesimal_approx
    8.85              simp add: mem_infmal_iff approx_minus_iff [symmetric])
    8.86  done
    8.87  
    8.88 @@ -1572,7 +1572,7 @@
    8.89  lemma less_Infinitesimal_less:
    8.90       "[| 0 < x;  (x::hypreal) \<notin>Infinitesimal;  e :Infinitesimal |] ==> e < x"
    8.91  apply (rule ccontr)
    8.92 -apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval] 
    8.93 +apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
    8.94              dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
    8.95  done
    8.96  
    8.97 @@ -1673,7 +1673,7 @@
    8.98       "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
    8.99           hypreal_of_real x + u \<le> hypreal_of_real y + v |]
   8.100        ==> x \<le> y"
   8.101 -by (blast intro: star_of_le [THEN iffD1] 
   8.102 +by (blast intro: star_of_le [THEN iffD1]
   8.103            intro!: hypreal_of_real_le_add_Infininitesimal_cancel)
   8.104  
   8.105  lemma hypreal_of_real_less_Infinitesimal_le_zero:
   8.106 @@ -1721,7 +1721,7 @@
   8.107       "(x::hypreal)*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
   8.108  apply (rule Infinitesimal_interval2, assumption)
   8.109  apply (rule_tac [2] zero_le_square, simp)
   8.110 -apply (insert zero_le_square [of y]) 
   8.111 +apply (insert zero_le_square [of y])
   8.112  apply (insert zero_le_square [of z], simp del:zero_le_square)
   8.113  done
   8.114  
   8.115 @@ -1729,7 +1729,7 @@
   8.116       "(x::hypreal)*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite"
   8.117  apply (rule HFinite_bounded, assumption)
   8.118  apply (rule_tac [2] zero_le_square)
   8.119 -apply (insert zero_le_square [of y]) 
   8.120 +apply (insert zero_le_square [of y])
   8.121  apply (insert zero_le_square [of z], simp del:zero_le_square)
   8.122  done
   8.123  
   8.124 @@ -1812,8 +1812,8 @@
   8.125  lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
   8.126  by (auto dest!: st_approx_self elim!: approx_trans3)
   8.127  
   8.128 -lemma approx_st_eq: 
   8.129 -  assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y" 
   8.130 +lemma approx_st_eq:
   8.131 +  assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
   8.132    shows "st x = st y"
   8.133  proof -
   8.134    have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
   8.135 @@ -1883,7 +1883,7 @@
   8.136  lemma st_inverse:
   8.137       "[| x \<in> HFinite; st x \<noteq> 0 |]
   8.138        ==> st(inverse x) = inverse (st x)"
   8.139 -apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1])
   8.140 +apply (rule_tac c1 = "st x" in mult_left_cancel [THEN iffD1])
   8.141  apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
   8.142  apply (subst right_inverse, auto)
   8.143  done
   8.144 @@ -1897,7 +1897,7 @@
   8.145  by (blast intro: st_HFinite st_approx_self approx_st_eq)
   8.146  
   8.147  lemma Infinitesimal_add_st_less:
   8.148 -     "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |] 
   8.149 +     "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |]
   8.150        ==> st x + u < st y"
   8.151  apply (drule st_SReal)+
   8.152  apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
   8.153 @@ -1933,7 +1933,7 @@
   8.154  lemma st_hrabs: "x \<in> HFinite ==> abs(st x) = st(abs x)"
   8.155  apply (simp add: linorder_not_le st_zero_le abs_if st_minus
   8.156     linorder_not_less)
   8.157 -apply (auto dest!: st_zero_ge [OF order_less_imp_le]) 
   8.158 +apply (auto dest!: st_zero_ge [OF order_less_imp_le])
   8.159  done
   8.160  
   8.161  
   8.162 @@ -1943,7 +1943,7 @@
   8.163  subsubsection {* @{term HFinite} *}
   8.164  
   8.165  lemma HFinite_FreeUltrafilterNat:
   8.166 -    "star_n X \<in> HFinite 
   8.167 +    "star_n X \<in> HFinite
   8.168       ==> \<exists>u. {n. norm (X n) < u} \<in> FreeUltrafilterNat"
   8.169  apply (auto simp add: HFinite_def SReal_def)
   8.170  apply (rule_tac x=r in exI)
   8.171 @@ -2273,10 +2273,10 @@
   8.172       "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
   8.173        ==> star_n X - star_n Y \<in> Infinitesimal"
   8.174  by (auto intro!: bexI
   8.175 -         dest: FreeUltrafilterNat_inverse_real_of_posnat 
   8.176 +         dest: FreeUltrafilterNat_inverse_real_of_posnat
   8.177                 FreeUltrafilterNat.Int
   8.178 -         intro: order_less_trans FreeUltrafilterNat.subset 
   8.179 -         simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff 
   8.180 +         intro: order_less_trans FreeUltrafilterNat.subset
   8.181 +         simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff
   8.182                     star_n_inverse)
   8.183  
   8.184  end
     9.1 --- a/src/HOL/Real.thy	Wed Mar 19 14:55:47 2014 +0000
     9.2 +++ b/src/HOL/Real.thy	Wed Mar 19 17:06:02 2014 +0000
     9.3 @@ -974,12 +974,6 @@
     9.4  text {* BH: These lemmas should not be necessary; they should be
     9.5  covered by existing simp rules and simplification procedures. *}
     9.6  
     9.7 -lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
     9.8 -by simp (* redundant with mult_cancel_left *)
     9.9 -
    9.10 -lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
    9.11 -by simp (* redundant with mult_cancel_right *)
    9.12 -
    9.13  lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
    9.14  by simp (* solved by linordered_ring_less_cancel_factor simproc *)
    9.15  
    10.1 --- a/src/HOL/Rings.thy	Wed Mar 19 14:55:47 2014 +0000
    10.2 +++ b/src/HOL/Rings.thy	Wed Mar 19 17:06:02 2014 +0000
    10.3 @@ -376,6 +376,12 @@
    10.4    thus ?thesis by simp
    10.5  qed
    10.6  
    10.7 +lemma mult_left_cancel: "c \<noteq> 0 \<Longrightarrow> (c*a=c*b) = (a=b)"
    10.8 +by simp 
    10.9 +
   10.10 +lemma mult_right_cancel: "c \<noteq> 0 \<Longrightarrow> (a*c=b*c) = (a=b)"
   10.11 +by simp 
   10.12 +
   10.13  end
   10.14  
   10.15  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
    11.1 --- a/src/HOL/Series.thy	Wed Mar 19 14:55:47 2014 +0000
    11.2 +++ b/src/HOL/Series.thy	Wed Mar 19 17:06:02 2014 +0000
    11.3 @@ -461,6 +461,10 @@
    11.4    apply (auto intro: setsum_mono simp add: abs_less_iff)
    11.5    done
    11.6  
    11.7 +(*A better argument order*)
    11.8 +lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
    11.9 +by (rule summable_comparison_test) auto
   11.10 +
   11.11  subsection {* The Ratio Test*}
   11.12  
   11.13  lemma summable_ratio_test: 
    12.1 --- a/src/HOL/Transcendental.thy	Wed Mar 19 14:55:47 2014 +0000
    12.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 19 17:06:02 2014 +0000
    12.3 @@ -2396,15 +2396,6 @@
    12.4    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
    12.5  qed
    12.6  
    12.7 -lemma real_mult_inverse_cancel:
    12.8 -     "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
    12.9 -      ==> inverse x * y < inverse x1 * u"
   12.10 -  by (metis field_divide_inverse mult_commute mult_assoc pos_divide_less_eq pos_less_divide_eq)
   12.11 -
   12.12 -lemma real_mult_inverse_cancel2:
   12.13 -     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
   12.14 -  by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
   12.15 -
   12.16  lemmas realpow_num_eq_if = power_eq_if
   12.17  
   12.18  lemma sumr_pos_lt_pair:
   12.19 @@ -3208,7 +3199,7 @@
   12.20  
   12.21  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
   12.22    apply (rule power_inverse [THEN subst])
   12.23 -  apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
   12.24 +  apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
   12.25    apply (auto dest: field_power_not_zero
   12.26            simp add: power_mult_distrib distrib_right power_divide tan_def
   12.27                      mult_assoc power_inverse [symmetric])