# HG changeset patch
# User hoelzl
# Date 1396456501 -7200
# Node ID 2704ca85be986fe7d134cc871d4083da749360ca
# Parent  0646f63a02b7b0647695af89bbce084f6c190ce3
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names

diff -r 0646f63a02b7 -r 2704ca85be98 NEWS
--- a/NEWS	Wed Apr 02 17:47:56 2014 +0200
+++ b/NEWS	Wed Apr 02 18:35:01 2014 +0200
@@ -563,6 +563,11 @@
     explicit set-comprehensions with eucl_less for other (half-) open
     intervals.
 
+  - renamed theorems:
+    derivative_linear         ~>  has_derivative_bounded_linear
+    derivative_is_linear      ~>  has_derivative_linear
+    bounded_linear_imp_linear ~>  bounded_linear.linear
+
 
 *** Scala ***
 
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Complex.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -339,6 +339,21 @@
 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
   by (cases x) simp
 
+
+lemma abs_sqrt_wlog:
+  fixes x::"'a::linordered_idom"
+  assumes "\<And>x::'a. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
+by (metis abs_ge_zero assms power2_abs)
+
+lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> sqrt 2 * norm z"
+  unfolding complex_norm_def
+  apply (rule abs_sqrt_wlog [where x="Re z"])
+  apply (rule abs_sqrt_wlog [where x="Im z"])
+  apply (rule power2_le_imp_le)
+  apply (simp_all add: power2_sum add_commute sum_squares_bound real_sqrt_mult [symmetric])
+  done
+
+
 text {* Properties of complex signum. *}
 
 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
@@ -370,6 +385,20 @@
 lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
 lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
 
+lemma continuous_Re: "continuous_on X Re"
+  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
+            continuous_on_cong continuous_on_id)
+
+lemma continuous_Im: "continuous_on X Im"
+  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
+            continuous_on_cong continuous_on_id)
+
+lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
+  by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const)
+
+lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
+  by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const)
+
 lemma tendsto_Complex [tendsto_intros]:
   assumes "(f ---> a) F" and "(g ---> b) F"
   shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
@@ -387,6 +416,20 @@
        (simp add: dist_norm real_sqrt_sum_squares_less)
 qed
 
+
+lemma tendsto_complex_iff:
+  "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
+proof -
+  have f: "f = (\<lambda>x. Complex (Re (f x)) (Im (f x)))" and x: "x = Complex (Re x) (Im x)"
+    by simp_all
+  show ?thesis
+    apply (subst f)
+    apply (subst x)
+    apply (intro iffI tendsto_Complex conjI)
+    apply (simp_all add: tendsto_Re tendsto_Im)
+    done
+qed
+
 instance complex :: banach
 proof
   fix X :: "nat \<Rightarrow> complex"
@@ -489,6 +532,9 @@
 lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
   by (simp add: complex_eq_iff)
 
+lemma cnj_setsum: "cnj (setsum f s) = (\<Sum>x\<in>s. cnj (f x))"
+  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_add)
+
 lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
   by (simp add: complex_eq_iff)
 
@@ -501,6 +547,9 @@
 lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
   by (simp add: complex_eq_iff)
 
+lemma cnj_setprod: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
+  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_mult)
+
 lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
   by (simp add: complex_inverse_def)
 
@@ -562,6 +611,12 @@
 lemmas isCont_cnj [simp] =
   bounded_linear.isCont [OF bounded_linear_cnj]
 
+lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
+  by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
+
+lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
+  by (simp add: sums_def lim_cnj cnj_setsum [symmetric])
+
 
 subsection{*Basic Lemmas*}
 
@@ -641,31 +696,43 @@
   by (metis im_complex_div_gt_0 not_le)
 
 lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
-apply (cases "finite s")
-  by (induct s rule: finite_induct) auto
+  by (induct s rule: infinite_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
+  by (induct s rule: infinite_finite_induct) auto
+
+lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
+  unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
+  
+lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
+  unfolding sums_complex_iff by blast
+
+lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
+  unfolding sums_complex_iff by blast
+
+lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
+  unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
+
+lemma summable_complex_of_real [simp]: "summable (\<lambda>n. complex_of_real (f n)) \<longleftrightarrow> summable f"
+  unfolding summable_complex_iff by simp
+
+lemma summable_Re: "summable f \<Longrightarrow> summable (\<lambda>x. Re (f x))"
+  unfolding summable_complex_iff by blast
+
+lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
+  unfolding summable_complex_iff by blast
 
 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
+  by (induct s rule: infinite_finite_induct) auto
 
 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
+  by (induct s rule: infinite_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
+  by (induct s rule: infinite_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 
@@ -677,6 +744,27 @@
 lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
   by (metis Re_complex_of_real Reals_cases norm_of_real)
 
+lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
+  by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
+
+lemma series_comparison_complex:
+  fixes f:: "nat \<Rightarrow> 'a::banach"
+  assumes sg: "summable g"
+     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
+     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
+  shows "summable f"
+proof -
+  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])
+    using sg
+    apply (auto simp: summable_def)
+    apply (rule_tac x="Re s" in exI)
+    apply (auto simp: g sums_Re)
+    apply (metis fg g)
+    done
+qed
 
 subsection{*Finally! Polar Form for Complex Numbers*}
 
@@ -888,4 +976,5 @@
 lemmas complex_Re_Im_cancel_iff = complex_eq_iff
 lemmas complex_equality = complex_eqI
 
+
 end
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Deriv.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -61,6 +61,9 @@
 lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
   by (simp add: has_derivative_def)
 
+lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
+  using bounded_linear.linear[OF has_derivative_bounded_linear] .
+
 lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
   by (simp add: has_derivative_def tendsto_const)
 
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -10,46 +10,10 @@
 
 subsection {*Complex number lemmas *}
 
-lemma abs_sqrt_wlog:
-  fixes x::"'a::linordered_idom"
-  assumes "!!x::'a. x\<ge>0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
-by (metis abs_ge_zero assms power2_abs)
-
-lemma complex_abs_le_norm: "abs(Re z) + abs(Im z) \<le> sqrt(2) * norm z"
-proof (cases z)
-  case (Complex x y)
-  show ?thesis
-    apply (rule power2_le_imp_le)
-    apply (auto simp: real_sqrt_mult [symmetric] Complex)
-    apply (rule abs_sqrt_wlog [where x=x])
-    apply (rule abs_sqrt_wlog [where x=y])
-    apply (simp add: power2_sum add_commute sum_squares_bound)
-    done
-qed
-
-lemma continuous_Re: "continuous_on X Re"
-  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
-            continuous_on_cong continuous_on_id)
-
-lemma continuous_Im: "continuous_on X Im"
-  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
-            continuous_on_cong continuous_on_id)
-
-lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
-  by (auto simp add: closed_segment_def open_segment_def)
-
-lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
-  by (auto simp add: has_derivative_def bounded_linear_Re)
-
-lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
-  by (auto simp add: has_derivative_def bounded_linear_Im)
-
 lemma fact_cancel:
   fixes c :: "'a::real_field"
   shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
-  apply (subst frac_eq_eq [OF of_nat_fact_not_zero of_nat_fact_not_zero])
-  apply (simp add: algebra_simps of_nat_mult)
-  done
+  by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
 
 lemma
   shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
@@ -65,9 +29,6 @@
   by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
             isCont_Im isCont_ident isCont_const)+
 
-lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
-  by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
-
 lemma closed_complex_Reals: "closed (Reals :: complex set)"
 proof -
   have "(Reals :: complex set) = {z. Im z = 0}"
@@ -78,16 +39,15 @@
 
 
 lemma linear_times:
-  fixes c::"'a::{real_algebra,real_vector}" shows "linear (\<lambda>x. c * x)"
+  fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
   by (auto simp: linearI distrib_left)
 
 lemma bilinear_times:
-  fixes c::"'a::{real_algebra,real_vector}" shows "bilinear (\<lambda>x y::'a. x*y)"
-  unfolding bilinear_def
-  by (auto simp: distrib_left distrib_right intro!: linearI)
+  fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
+  by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
 
 lemma linear_cnj: "linear cnj"
-  by (auto simp: linearI cnj_def)
+  using bounded_linear.linear[OF bounded_linear_cnj] .
 
 lemma tendsto_mult_left:
   fixes c::"'a::real_normed_algebra" 
@@ -152,7 +112,7 @@
 lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
-  by (metis bounded_linear.uniformly_continuous_on[of "\<lambda>x. x * c"] bounded_linear_mult_left) 
+  using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . 
 
 lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
@@ -164,8 +124,7 @@
   by (rule continuous_norm [OF continuous_ident])
 
 lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm"
-  by (metis continuous_on_eq continuous_on_id continuous_on_norm)
-
+  by (intro continuous_on_id continuous_on_norm)
 
 subsection{*DERIV stuff*}
 
@@ -184,8 +143,7 @@
       and "\<forall>x\<in>(s - k). DERIV f x :> 0"
     obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
 using has_derivative_zero_connected_constant [OF assms(1-4)] assms
-by (metis DERIV_const Derivative.has_derivative_const Diff_iff at_within_open 
-          frechet_derivative_at has_field_derivative_def)
+by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def)
 
 lemma DERIV_zero_constant:
   fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
@@ -255,7 +213,7 @@
     obtains c where "(f has_derivative (\<lambda>x. x * c)) F"
 proof -
   obtain c where "f' = (\<lambda>x. x * c)"
-    by (metis assms derivative_linear real_bounded_linear)
+    by (metis assms has_derivative_bounded_linear real_bounded_linear)
   then show ?thesis
     by (metis assms that)
 qed
@@ -336,15 +294,14 @@
 lemma complex_differentiable_const:
   "(\<lambda>z. c) complex_differentiable F"
   unfolding complex_differentiable_def has_field_derivative_def
-  apply (rule exI [where x=0])
-  by (metis Derivative.has_derivative_const lambda_zero) 
+  by (rule exI [where x=0])
+     (metis has_derivative_const lambda_zero) 
 
 lemma complex_differentiable_id:
   "(\<lambda>z. z) complex_differentiable F"
   unfolding complex_differentiable_def has_field_derivative_def
-  apply (rule exI [where x=1])
-  apply (simp add: lambda_one [symmetric])
-  done
+  by (rule exI [where x=1])
+     (simp add: lambda_one [symmetric])
 
 lemma complex_differentiable_minus:
     "f complex_differentiable F \<Longrightarrow> (\<lambda>z. -(f z)) complex_differentiable F"
@@ -484,10 +441,9 @@
   by (metis DERIV_power)
 
 lemma holomorphic_on_setsum:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s)
-           \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
   unfolding holomorphic_on_def
-  apply (induct I rule: finite_induct) 
+  apply (induct I rule: infinite_finite_induct) 
   apply (force intro: DERIV_const DERIV_add)+
   done
 
@@ -580,9 +536,6 @@
 
 subsection{*Caratheodory characterization.*}
 
-(*REPLACE the original version. BUT IN WHICH FILE??*)
-thm Deriv.CARAT_DERIV
-
 lemma complex_differentiable_caratheodory_at:
   "f complex_differentiable (at z) \<longleftrightarrow>
          (\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> continuous (at z) g)"
@@ -796,9 +749,8 @@
 by (induct n) (auto simp: analytic_on_const analytic_on_mult)
 
 lemma analytic_on_setsum:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s)
-           \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
-  by (induct I rule: finite_induct) (auto simp: analytic_on_const analytic_on_add)
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
+  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
 
 subsection{*analyticity at a point.*}
 
@@ -1025,12 +977,6 @@
 
 subsection{*Further useful properties of complex conjugation*}
 
-lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
-  by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
-
-lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
-  by (simp add: sums_def lim_cnj cnj_setsum [symmetric])
-
 lemma continuous_within_cnj: "continuous (at z within s) cnj"
 by (metis bounded_linear_cnj linear_continuous_within)
 
@@ -1043,12 +989,11 @@
   fixes l::complex
   assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   shows  "l \<in> \<real>"
-proof (rule Lim_in_closed_set)
-  show "closed (\<real>::complex set)"
-    by (rule closed_complex_Reals)
+proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
   show "eventually (\<lambda>x. f x \<in> \<real>) F"
     using assms(3, 4) by (auto intro: eventually_mono)
-qed fact+
+qed
+
 lemma real_lim_sequentially:
   fixes l::complex
   shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
@@ -1079,66 +1024,11 @@
 using assms unfolding summable_def
 by (blast intro: sums_vec_nth)
 
-lemma sums_Re:
-  assumes "f sums a"
-  shows "(\<lambda>x. Re (f x)) sums Re a"
-using assms 
-by (auto simp: sums_def Re_setsum [symmetric] isCont_tendsto_compose [of a Re])
-
-lemma sums_Im:
-  assumes "f sums a"
-  shows "(\<lambda>x. Im (f x)) sums Im a"
-using assms 
-by (auto simp: sums_def Im_setsum [symmetric] isCont_tendsto_compose [of a Im])
-
-lemma summable_Re:
-  assumes "summable f"
-  shows "summable (\<lambda>x. Re (f x))"
-using assms unfolding summable_def
-by (blast intro: sums_Re)
-
-lemma summable_Im:
-  assumes "summable f"
-  shows "summable (\<lambda>x. Im (f x))"
-using assms unfolding summable_def
-by (blast intro: sums_Im)
-
-lemma series_comparison_complex:
-  fixes f:: "nat \<Rightarrow> 'a::banach"
-  assumes sg: "summable g"
-     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
-     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
-  shows "summable f"
-proof -
-  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])
-    using sg
-    apply (auto simp: summable_def)
-    apply (rule_tac x="Re s" in exI)
-    apply (auto simp: g sums_Re)
-    apply (metis fg g)
-    done
-qed
-
-lemma summable_complex_of_real [simp]:
-  "summable (\<lambda>n. complex_of_real (f n)) = summable f"
-apply (auto simp: Series.summable_Cauchy)  
-apply (drule_tac x = e in spec, auto)
-apply (rule_tac x=N in exI)
-apply (auto simp: of_real_setsum [symmetric])
-done
-
-
-
-
 lemma setsum_Suc_reindex:
   fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
     shows  "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>i. f (Suc i)) {0..n}"
 by (induct n) auto
 
-
 text{*A kind of complex Taylor theorem.*}
 lemma complex_taylor:
   assumes s: "convex s" 
@@ -1238,22 +1128,22 @@
 
 text{* Something more like the traditional MVT for real components.*}
 lemma complex_mvt_line:
-  assumes "\<And>u. u \<in> closed_segment w z ==> (f has_field_derivative f'(u)) (at u)"
+  assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
     shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
 proof -
   have twz: "\<And>t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)"
     by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib)
+  note assms[unfolded has_field_derivative_def, has_derivative_intros]
   show ?thesis
     apply (cut_tac mvt_simple
                      [of 0 1 "Re o f o (\<lambda>t. (1 - t) *\<^sub>R w +  t *\<^sub>R z)"
                       "\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>t. t *\<^sub>R (z - w))"])
     apply auto
     apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI)
-    apply (simp add: open_segment_def)
-    apply (auto simp add: twz)
-    apply (rule has_derivative_at_within)
-    apply (intro has_derivative_intros has_derivative_add [OF has_derivative_const, simplified])+
-    apply (rule assms [unfolded has_field_derivative_def])
+    apply (auto simp add: open_segment_def twz) []
+    apply (intro has_derivative_eq_intros has_derivative_at_within)
+    apply simp_all
+    apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib)
     apply (force simp add: twz closed_segment_def)
     done
 qed
@@ -1309,24 +1199,4 @@
     done
 qed
 
-text{*Relations among convergence and absolute convergence for power series.*}
-lemma abel_lemma:
-  fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
-  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm(a n) * r0^n \<le> M"
-    shows "summable (\<lambda>n. norm(a(n)) * r^n)"
-proof (rule summable_comparison_test' [of "\<lambda>n. M * (r / r0)^n"])
-  show "summable (\<lambda>n. M * (r / r0) ^ n)"
-    using assms 
-    by (auto simp add: summable_mult summable_geometric)
-  next
-    fix n
-    show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
-      using r r0 M [of n]
-      apply (auto simp add: abs_mult field_simps power_divide)
-      apply (cases "r=0", simp)
-      apply (cases n, auto)
-      done
-qed
-
-
 end
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -5875,14 +5875,6 @@
     by (induct set: finite, simp, simp add: convex_hull_set_plus)
 qed simp
 
-lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
-proof -
-  assume "bounded_linear f"
-  then interpret f: bounded_linear f .
-  show "linear f"
-    by (simp add: f.add f.scaleR linear_iff)
-qed
-
 lemma convex_hull_eq_real_cbox:
   fixes x y :: real assumes "x \<le> y"
   shows "convex hull {x, y} = cbox x y"
@@ -6295,6 +6287,9 @@
 
 lemmas segment = open_segment_def closed_segment_def
 
+lemma open_closed_segment: "u \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
+  by (auto simp add: closed_segment_def open_segment_def)
+
 definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
 
 lemma midpoint_refl: "midpoint x x = x"
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -9,16 +9,6 @@
 imports Brouwer_Fixpoint Operator_Norm
 begin
 
-lemma bounded_linear_imp_linear: (* TODO: move elsewhere *)
-  assumes "bounded_linear f"
-  shows "linear f"
-proof -
-  interpret f: bounded_linear f
-    using assms .
-  show ?thesis
-    by (simp add: f.add f.scaleR linear_iff)
-qed
-
 lemma netlimit_at_vector: (* TODO: move *)
   fixes a :: "'a::real_normed_vector"
   shows "netlimit (at a) = a"
@@ -37,22 +27,15 @@
 (* Because I do not want to type this all the time *)
 lemmas linear_linear = linear_conv_bounded_linear[symmetric]
 
-lemma derivative_linear[dest]: "(f has_derivative f') net \<Longrightarrow> bounded_linear f'"
-  unfolding has_derivative_def by auto
-
-lemma derivative_is_linear: "(f has_derivative f') net \<Longrightarrow> linear f'"
-  by (rule derivative_linear [THEN bounded_linear_imp_linear])
+declare has_derivative_bounded_linear[dest]
 
 subsection {* Derivatives *}
 
 subsubsection {* Combining theorems. *}
 
 lemmas has_derivative_id = has_derivative_ident
-lemmas has_derivative_const = has_derivative_const
 lemmas has_derivative_neg = has_derivative_minus
-lemmas has_derivative_add = has_derivative_add
 lemmas has_derivative_sub = has_derivative_diff
-lemmas has_derivative_setsum = has_derivative_setsum
 lemmas scaleR_right_has_derivative = has_derivative_scaleR_right
 lemmas scaleR_left_has_derivative = has_derivative_scaleR_left
 lemmas inner_right_has_derivative = has_derivative_inner_right
@@ -176,11 +159,6 @@
     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
 qed
 
-lemma CARAT_DERIV: (*FIXME: REPLACES THE ONE IN Deriv.thy*)
-  "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"
-by (rule DERIV_caratheodory_within)
-
-
 subsubsection {* Limit transformation for derivatives *}
 
 lemma has_derivative_transform_within:
@@ -275,7 +253,7 @@
 
 lemma linear_frechet_derivative: "f differentiable net \<Longrightarrow> linear (frechet_derivative f net)"
   unfolding frechet_derivative_works has_derivative_def
-  by (auto intro: bounded_linear_imp_linear)
+  by (auto intro: bounded_linear.linear)
 
 
 subsection {* Differentiability implies continuity *}
@@ -322,14 +300,14 @@
     (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
     eventually_at dist_norm diff_add_eq_diff_diff
-  by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq)
+  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
 
 lemma has_derivative_within_alt2:
   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
     (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
     eventually_at dist_norm diff_add_eq_diff_diff
-  by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq)
+  by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
 
 lemma has_derivative_at_alt:
   "(f has_derivative f') (at x) \<longleftrightarrow>
@@ -372,6 +350,7 @@
 
 subsection {* Uniqueness of derivative *}
 
+
 text {*
  The general result is a bit messy because we need approachability of the
  limit point from any direction. But OK for nontrivial intervals etc.
@@ -854,7 +833,7 @@
   proof -
     case goal1
     have "norm (f' x y) \<le> onorm (f' x) * norm y"
-      by (rule onorm[OF derivative_linear[OF assms(2)[rule_format,OF goal1]]])
+      by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]])
     also have "\<dots> \<le> B * norm y"
       apply (rule mult_right_mono)
       using assms(3)[rule_format,OF goal1]
@@ -881,7 +860,7 @@
 lemma has_derivative_zero_constant:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   assumes "convex s"
-    and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
+    and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
   shows "\<exists>c. \<forall>x\<in>s. f x = c"
 proof -
   { fix x y assume "x \<in> s" "y \<in> s"
@@ -896,14 +875,34 @@
 lemma has_derivative_zero_unique:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   assumes "convex s"
-    and "a \<in> s"
-    and "f a = c"
-    and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
-    and "x \<in> s"
-  shows "f x = c"
-  using has_derivative_zero_constant[OF assms(1,4)]
-  using assms(2-3,5)
-  by auto
+    and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
+    and "x \<in> s" "y \<in> s"
+  shows "f x = f y"
+  using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force
+
+lemma has_derivative_zero_unique_connected:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
+  assumes "open s" "connected s"
+  assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
+  assumes "x \<in> s" "y \<in> s"
+  shows "f x = f y"
+proof (rule connected_local_const[where f=f, OF `connected s` `x\<in>s` `y\<in>s`])
+  show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)"
+  proof
+    fix a assume "a \<in> s"
+    with `open s` obtain e where "0 < e" "ball a e \<subseteq> s"
+      by (rule openE)
+    then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
+      by (intro has_derivative_zero_constant)
+         (auto simp: at_within_open[OF _ open_ball] f convex_ball)
+    with `0<e` have "\<forall>x\<in>ball a e. f a = f x"
+      by auto
+    then show "eventually (\<lambda>b. f a = f b) (at a within s)"
+      using `0<e` unfolding eventually_at_topological
+      by (intro exI[of _ "ball a e"]) auto
+  qed
+qed
+
 
 
 subsection {* Differentiability of inverse function (most basic form) *}
@@ -1546,11 +1545,11 @@
           apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
           apply (rule has_derivative_at_within)
           using assms(5) and `u \<in> s` `a \<in> s`
-          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] derivative_linear)
+          apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
           done
         have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
           apply (rule_tac[!] bounded_linear_sub)
-          apply (rule_tac[!] derivative_linear)
+          apply (rule_tac[!] has_derivative_bounded_linear)
           using assms(5) `u \<in> s` `a \<in> s`
           apply auto
           done
@@ -1773,18 +1772,18 @@
     proof
       fix x' y z :: 'a
       fix c :: real
-      note lin = assms(2)[rule_format,OF `x\<in>s`,THEN derivative_linear]
+      note lin = assms(2)[rule_format,OF `x\<in>s`,THEN has_derivative_bounded_linear]
       show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'"
         apply (rule tendsto_unique[OF trivial_limit_sequentially])
         apply (rule lem3[rule_format])
-        unfolding lin[THEN bounded_linear_imp_linear, THEN linear_cmul]
+        unfolding lin[THEN bounded_linear.linear, THEN linear_cmul]
         apply (intro tendsto_intros)
         apply (rule lem3[rule_format])
         done
       show "g' x (y + z) = g' x y + g' x z"
         apply (rule tendsto_unique[OF trivial_limit_sequentially])
         apply (rule lem3[rule_format])
-        unfolding lin[THEN bounded_linear_imp_linear, THEN linear_add]
+        unfolding lin[THEN bounded_linear.linear, THEN linear_add]
         apply (rule tendsto_add)
         apply (rule lem3[rule_format])+
         done
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -752,6 +752,12 @@
   shows "norm (setsum f A) \<le> (\<Sum>i\<in>A. norm (f i))"
   by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
 
+lemma setsum_norm_le:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+  shows "norm (setsum f S) \<le> setsum g S"
+  by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg)
+
 lemma abs_norm_cancel [simp]:
   fixes a :: "'a::real_normed_vector"
   shows "\<bar>norm a\<bar> = norm a"
@@ -1158,6 +1164,8 @@
   show ?thesis by (auto intro: order_less_imp_le)
 qed
 
+lemma linear: "linear f" ..
+
 end
 
 lemma bounded_linear_intro:
diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed Apr 02 17:47:56 2014 +0200
+++ b/src/HOL/Series.thy	Wed Apr 02 18:35:01 2014 +0200
@@ -463,7 +463,7 @@
 
 (*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
+  by (rule summable_comparison_test) auto
 
 subsection {* The Ratio Test*}
 
@@ -502,6 +502,27 @@
 
 end
 
+text{*Relations among convergence and absolute convergence for power series.*}
+
+lemma abel_lemma:
+  fixes a :: "nat \<Rightarrow> 'a::real_normed_vector"
+  assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
+    shows "summable (\<lambda>n. norm (a n) * r^n)"
+proof (rule summable_comparison_test')
+  show "summable (\<lambda>n. M * (r / r0) ^ n)"
+    using assms 
+    by (auto simp add: summable_mult summable_geometric)
+next
+  fix n
+  show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
+    using r r0 M [of n]
+    apply (auto simp add: abs_mult field_simps power_divide)
+    apply (cases "r=0", simp)
+    apply (cases n, auto)
+    done
+qed
+
+
 text{*Summability of geometric series for real algebras*}
 
 lemma complete_algebra_summable_geometric: