# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1395670949 0
# Node ID 918432e3fcfa6d48a8e2a77fc88e4f624979c80f
# Parent  3d79c132e657ebbf44be57b73167b1b5c4091de3
rearranging some deriv theorems

diff -r 3d79c132e657 -r 918432e3fcfa src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/Deriv.thy	Mon Mar 24 14:22:29 2014 +0000
@@ -168,6 +168,9 @@
 lemma has_derivative_subset: "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
   by (auto simp add: has_derivative_iff_norm intro: tendsto_within_subset)
 
+lemmas has_derivative_within_subset = has_derivative_subset 
+
+
 subsection {* Continuity *}
 
 lemma has_derivative_continuous:
@@ -477,6 +480,8 @@
 lemma differentiable_subset: "f differentiable (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f differentiable (at x within t)"
   unfolding differentiable_def by (blast intro: has_derivative_subset)
 
+lemmas differentiable_within_subset = differentiable_subset
+
 lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_ident)
 
@@ -541,6 +546,11 @@
 lemma has_field_derivative_imp_has_derivative: "(f has_field_derivative D) F \<Longrightarrow> (f has_derivative op * D) F"
   by (simp add: has_field_derivative_def)
 
+lemma DERIV_subset: 
+  "(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s 
+   \<Longrightarrow> (f has_field_derivative f') (at x within t)"
+  by (simp add: has_field_derivative_def has_derivative_within_subset)
+
 abbreviation (input)
   deriv :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
@@ -597,32 +607,47 @@
 lemma DERIV_ident [simp]: "((\<lambda>x. x) has_field_derivative 1) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_ident]) auto
 
-lemma DERIV_add:
+lemma field_differentiable_add:
+  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
+    shows "((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
+  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
+  using assms 
+  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
+
+corollary DERIV_add:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x + g x) has_field_derivative D + E) (at x within s)"
-  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
-     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
+  by (rule field_differentiable_add)
+
+lemma field_differentiable_minus:
+  assumes "(f has_field_derivative f') F" 
+    shows "((\<lambda>z. - (f z)) has_field_derivative -f') F"
+  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
+  using assms 
+  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
 
-lemma DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)"
-  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus]) 
-     (auto simp: field_simps mult_commute_abs dest: has_field_derivative_imp_has_derivative)
+corollary DERIV_minus: "(f has_field_derivative D) (at x within s) \<Longrightarrow> ((\<lambda>x. - f x) has_field_derivative -D) (at x within s)"
+  by (rule field_differentiable_minus)
 
-lemma DERIV_diff:
+lemma field_differentiable_diff:
+  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
+    shows "((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
+by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
+
+corollary DERIV_diff:
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
   ((\<lambda>x. f x - g x) has_field_derivative D - E) (at x within s)"
-  by (rule has_derivative_imp_has_field_derivative[OF has_derivative_diff])
-     (auto simp: field_simps dest: has_field_derivative_imp_has_derivative)
-
-lemma DERIV_add_minus:
-  "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
-  ((\<lambda>x. f x + - g x) has_field_derivative D + - E) (at x within s)"
-  by (simp only: DERIV_add DERIV_minus)
+  by (rule field_differentiable_diff)
 
 lemma DERIV_continuous: "(f has_field_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (drule has_derivative_continuous[OF has_field_derivative_imp_has_derivative]) simp
 
-lemma DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
-  by (auto dest!: DERIV_continuous)
+corollary DERIV_isCont: "DERIV f x :> D \<Longrightarrow> isCont f x"
+  by (rule DERIV_continuous)
+
+lemma DERIV_continuous_on:
+  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative D) (at x)) \<Longrightarrow> continuous_on s f"
+  by (metis DERIV_continuous continuous_at_imp_continuous_on)
 
 lemma DERIV_mult':
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
@@ -1243,19 +1268,18 @@
 (* A function with positive derivative is increasing. 
    A simple proof using the MVT, by Jeremy Avigad. And variants.
 *)
-lemma DERIV_pos_imp_increasing:
+lemma DERIV_pos_imp_increasing_open:
   fixes a::real and b::real and f::"real => real"
-  assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
+  assumes "a < b" and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (EX y. DERIV f x :> y & y > 0)"
+      and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
   shows "f a < f b"
 proof (rule ccontr)
   assume f: "~ f a < f b"
   have "EX l z. a < z & z < b & DERIV f z :> l
       & f b - f a = (b - a) * l"
     apply (rule MVT)
-      using assms
-      apply auto
-      apply (metis DERIV_isCont)
-     apply (metis differentiableI less_le)
+      using assms Deriv.differentiableI
+      apply force+
     done
   then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
       and "f b - f a = (b - a) * l"
@@ -1263,9 +1287,15 @@
   with assms f have "~(l > 0)"
     by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
   with assms z show False
-    by (metis DERIV_unique less_le)
+    by (metis DERIV_unique)
 qed
 
+lemma DERIV_pos_imp_increasing:
+  fixes a::real and b::real and f::"real => real"
+  assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
+  shows "f a < f b"
+by (metis DERIV_pos_imp_increasing_open [of a b f] assms DERIV_continuous less_imp_le)
+
 lemma DERIV_nonneg_imp_nondecreasing:
   fixes a::real and b::real and f::"real => real"
   assumes "a \<le> b" and
@@ -1295,21 +1325,28 @@
     by (metis DERIV_unique order_less_imp_le)
 qed
 
+lemma DERIV_neg_imp_decreasing_open:
+  fixes a::real and b::real and f::"real => real"
+  assumes "a < b" and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (EX y. DERIV f x :> y & y < 0)"
+      and con: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+  shows "f a > f b"
+proof -
+  have "(%x. -f x) a < (%x. -f x) b"
+    apply (rule DERIV_pos_imp_increasing_open [of a b "%x. -f x"])
+    using assms
+    apply auto
+    apply (metis field_differentiable_minus neg_0_less_iff_less)
+    done
+  thus ?thesis
+    by simp
+qed
+
 lemma DERIV_neg_imp_decreasing:
   fixes a::real and b::real and f::"real => real"
   assumes "a < b" and
     "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y < 0)"
   shows "f a > f b"
-proof -
-  have "(%x. -f x) a < (%x. -f x) b"
-    apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"])
-    using assms
-    apply auto
-    apply (metis DERIV_minus neg_0_less_iff_less)
-    done
-  thus ?thesis
-    by simp
-qed
+by (metis DERIV_neg_imp_decreasing_open [of a b f] assms DERIV_continuous less_imp_le)
 
 lemma DERIV_nonpos_imp_nonincreasing:
   fixes a::real and b::real and f::"real => real"
diff -r 3d79c132e657 -r 918432e3fcfa src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 24 14:22:29 2014 +0000
@@ -253,16 +253,6 @@
 
 subsection{*DERIV stuff*}
 
-(*move some premises to a sensible order. Use more \<And> symbols.*)
-
-lemma DERIV_continuous_on: "\<lbrakk>\<And>x. x \<in> s \<Longrightarrow> DERIV f x :> D\<rbrakk> \<Longrightarrow> continuous_on s f"
-  by (metis DERIV_continuous continuous_at_imp_continuous_on)
-
-lemma DERIV_subset: 
-  "(f has_field_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s 
-   \<Longrightarrow> (f has_field_derivative f') (at x within t)"
-  by (simp add: has_field_derivative_def has_derivative_within_subset)
-
 lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
   by auto
 
@@ -496,28 +486,6 @@
   apply (simp add: lambda_one [symmetric])
   done
 
-(*DERIV_minus*)
-lemma field_differentiable_minus:
-  assumes "(f has_field_derivative f') F" 
-    shows "((\<lambda>z. - (f z)) has_field_derivative -f') F"
-  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_minus])
-  using assms 
-  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
-
-(*DERIV_add*)
-lemma field_differentiable_add:
-  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
-    shows "((\<lambda>z. f z + g z) has_field_derivative f' + g') F"
-  apply (rule has_derivative_imp_has_field_derivative[OF has_derivative_add])
-  using assms 
-  by (auto simp: has_field_derivative_def field_simps mult_commute_abs)
-
-(*DERIV_diff*)
-lemma field_differentiable_diff:
-  assumes "(f has_field_derivative f') F" "(g has_field_derivative g') F"
-    shows "((\<lambda>z. f z - g z) has_field_derivative f' - g') F"
-by (simp only: assms diff_conv_add_uminus field_differentiable_add field_differentiable_minus)
-
 lemma complex_differentiable_minus:
     "f complex_differentiable F \<Longrightarrow> (\<lambda>z. -(f z)) complex_differentiable F"
   using assms unfolding complex_differentiable_def
diff -r 3d79c132e657 -r 918432e3fcfa src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 24 14:22:29 2014 +0000
@@ -289,20 +289,6 @@
   unfolding differentiable_on_def continuous_on_eq_continuous_within
   using differentiable_imp_continuous_within by blast
 
-lemma has_derivative_within_subset:
-  "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
-    (f has_derivative f') (at x within t)"
-  unfolding has_derivative_within
-  using tendsto_within_subset
-  by blast
-
-lemma differentiable_within_subset:
-  "f differentiable (at x within t) \<Longrightarrow> s \<subseteq> t \<Longrightarrow>
-    f differentiable (at x within s)"
-  unfolding differentiable_def
-  using has_derivative_within_subset
-  by blast
-
 lemma differentiable_on_subset:
   "f differentiable_on t \<Longrightarrow> s \<subseteq> t \<Longrightarrow> f differentiable_on s"
   unfolding differentiable_on_def
diff -r 3d79c132e657 -r 918432e3fcfa src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/Transcendental.thy	Mon Mar 24 14:22:29 2014 +0000
@@ -3745,7 +3745,7 @@
             have "DERIV (\<lambda> x. suminf (?c x)) x :> (inverse (1 + x\<^sup>2))"
               unfolding suminf_c'_eq_geom
               by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
-            from DERIV_add_minus[OF this DERIV_arctan]
+            from DERIV_diff [OF this DERIV_arctan]
             show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
               by auto
           qed