# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1395248762 0
# Node ID dc429a5b13c497e7f9d63c303fe5068c584b0af3
# Parent  76ff0a15d2027c72a39cdba09c8c8dea5cf497ac
Some rationalisation of basic lemmas

diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Complex.thy
--- 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 
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Deriv.thy
--- 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
 
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Library/Poly_Deriv.thy
--- 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*}
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- 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)"
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/NSA/HDeriv.thy
--- 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])
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/NSA/HyperDef.thy
--- 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])
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/NSA/NSA.thy
--- 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
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Real.thy
--- 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 *)
 
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Rings.thy
--- 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
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Series.thy
--- 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: 
diff -r 76ff0a15d202 -r dc429a5b13c4 src/HOL/Transcendental.thy
--- 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])