# HG changeset patch
# User huffman
# Date 1159664832 -7200
# Node ID 35574b9b59aa3b7bbc308cca8c09b631793bf23d
# Parent  0e25916068675640eec0b3ddc9f40941ba511036
generalize more DERIV proofs

diff -r 0e2591606867 -r 35574b9b59aa src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Sat Sep 30 21:39:31 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sun Oct 01 03:07:12 2006 +0200
@@ -788,6 +788,98 @@
 lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) /# (z-x)) -- x --> D)"
 by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff')
 
+lemma inverse_diff_inverse:
+  "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
+   \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
+by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
+
+lemma DERIV_inverse_lemma:
+  "\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_div_algebra)\<rbrakk>
+   \<Longrightarrow> (inverse a - inverse b) /# h
+     = - (inverse a * ((a - b) /# h) * inverse b)"
+by (simp add: inverse_diff_inverse)
+
+lemma LIM_equal2:
+  assumes 1: "0 < R"
+  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+apply (unfold LIM_def, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="min s R" in exI, safe)
+apply (simp add: 1)
+apply (simp add: 2)
+done
+
+lemma DERIV_inverse':
+  fixes f :: "real \<Rightarrow> 'a::real_normed_div_algebra"
+  assumes der: "DERIV f x :> D"
+  assumes neq: "f x \<noteq> 0"
+  shows "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * D * inverse (f x))"
+    (is "DERIV _ _ :> ?E")
+proof (unfold DERIV_iff2)
+  from der have lim_f: "f -- x --> f x"
+    by (rule DERIV_isCont [unfolded isCont_def])
+
+  from neq have "0 < norm (f x)" by simp
+  with LIM_D [OF lim_f] obtain s
+    where s: "0 < s"
+    and less_fx: "\<And>z. \<lbrakk>z \<noteq> x; norm (z - x) < s\<rbrakk>
+                  \<Longrightarrow> norm (f z - f x) < norm (f x)"
+    by fast
+
+  show "(\<lambda>z. (inverse (f z) - inverse (f x)) /# (z - x)) -- x --> ?E"
+  proof (rule LIM_equal2 [OF s])
+    fix z :: real
+    assume "z \<noteq> x" "norm (z - x) < s"
+    hence "norm (f z - f x) < norm (f x)" by (rule less_fx)
+    hence "f z \<noteq> 0" by auto
+    thus "(inverse (f z) - inverse (f x)) /# (z - x) =
+          - (inverse (f z) * ((f z - f x) /# (z - x)) * inverse (f x))"
+      using neq by (rule DERIV_inverse_lemma)
+  next
+    from der have "(\<lambda>z. (f z - f x) /# (z - x)) -- x --> D"
+      by (unfold DERIV_iff2)
+    thus "(\<lambda>z. - (inverse (f z) * ((f z - f x) /# (z - x)) * inverse (f x)))
+          -- x --> ?E"
+      by (intro LIM_mult2 LIM_inverse LIM_minus LIM_const lim_f neq)
+  qed
+qed
+
+lemma DERIV_divide:
+  fixes D E :: "'a::{real_normed_div_algebra,field}"
+  shows "\<lbrakk>DERIV f x :> D; DERIV g x :> E; g x \<noteq> 0\<rbrakk>
+         \<Longrightarrow> DERIV (\<lambda>x. f x / g x) x :> (D * g x - f x * E) / (g x * g x)"
+apply (subgoal_tac "f x * - (inverse (g x) * E * inverse (g x)) +
+          D * inverse (g x) = (D * g x - f x * E) / (g x * g x)")
+apply (erule subst)
+apply (unfold divide_inverse)
+apply (erule DERIV_mult')
+apply (erule (1) DERIV_inverse')
+apply (simp add: left_diff_distrib nonzero_inverse_mult_distrib)
+apply (simp add: mult_ac)
+done
+
+lemma DERIV_power_Suc:
+  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower}"
+  assumes f: "DERIV f x :> D"
+  shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (of_nat n + 1) *# (D * f x ^ n)"
+proof (induct n)
+case 0
+  show ?case by (simp add: power_Suc f)
+case (Suc k)
+  from DERIV_mult' [OF f Suc] show ?case
+    apply (simp only: of_nat_Suc scaleR_left_distrib scaleR_one)
+    apply (simp only: power_Suc right_distrib mult_scaleR_right mult_ac)
+    done
+qed
+
+lemma DERIV_power:
+  fixes f :: "real \<Rightarrow> 'a::{real_normed_algebra,recpower}"
+  assumes f: "DERIV f x :> D"
+  shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n *# (D * f x ^ (n - Suc 0))"
+by (cases "n", simp, simp add: DERIV_power_Suc f)
+
+
 (* ------------------------------------------------------------------------ *)
 (* Caratheodory formulation of derivative at a point: standard proof        *)
 (* ------------------------------------------------------------------------ *)
@@ -816,6 +908,48 @@
                cong: LIM_equal [rule_format])
 qed
 
+lemma LIM_compose:
+  assumes f: "f -- a --> l"
+  assumes g: "isCont g l"
+  shows "(\<lambda>x. g (f x)) -- a --> g l"
+proof (rule LIM_I)
+  fix r::real assume r: "0 < r"
+  obtain s where s: "0 < s"
+    and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y - l) < s\<rbrakk> \<Longrightarrow> norm (g y - g l) < r"
+    using LIM_D [OF g [unfolded isCont_def] r] by fast
+  obtain t where t: "0 < t"
+    and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - l) < s"
+    using LIM_D [OF f s] by fast
+
+  show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - g l) < r"
+  proof (rule exI, safe)
+    show "0 < t" using t .
+  next
+    fix x assume "x \<noteq> a" and "norm (x - a) < t"
+    hence "norm (f x - l) < s" by (rule less_s)
+    thus "norm (g (f x) - g l) < r"
+      using r less_r by (case_tac "f x = l", simp_all)
+  qed
+qed
+
+lemma DERIV_chain':
+  assumes f: "DERIV f x :> D"
+  assumes g: "DERIV g (f x) :> E"
+  shows "DERIV (\<lambda>x. g (f x)) x :> D *# E"
+proof (unfold DERIV_iff2)
+  obtain d where d: "\<forall>y. g y - g (f x) = (y - f x) *# d y"
+    and cont_d: "isCont d (f x)" and dfx: "d (f x) = E"
+    using CARAT_DERIV [THEN iffD1, OF g] by fast
+  from f have "f -- x --> f x"
+    by (rule DERIV_isCont [unfolded isCont_def])
+  hence "(\<lambda>z. d (f z)) -- x --> d (f x)"
+    using cont_d by (rule LIM_compose)
+  hence "(\<lambda>z. ((f z - f x) /# (z - x)) *# d (f z))
+          -- x --> D *# d (f x)"
+    by (rule LIM_scaleR [OF f [unfolded DERIV_iff2]])
+  thus "(\<lambda>z. (g (f z) - g (f x)) /# (z - x)) -- x --> D *# E"
+    by (simp add: d dfx real_scaleR_def)
+qed
 
 
 subsubsection {* Nonstandard proofs *}
@@ -1136,16 +1270,13 @@
 (* LIM_mult2 follows from a NS proof          *)
 
 lemma DERIV_cmult:
-      "DERIV f x :> D ==> DERIV (%x. c * f x :: real) x :> c*D"
-apply (simp only: deriv_def times_divide_eq_right [symmetric]
-                  divideR_eq_divide
-                  NSDERIV_NSLIM_iff minus_mult_right right_diff_distrib [symmetric])
-apply (erule LIM_const [THEN LIM_mult2])
-done
+  fixes f :: "real \<Rightarrow> 'a::real_normed_algebra" shows
+      "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
+by (drule DERIV_mult' [OF DERIV_const], simp)
 
 (* standard version *)
 lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
-by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain)
+by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
 
 lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db"
 by (auto dest: DERIV_chain simp add: o_def)
@@ -1157,12 +1288,8 @@
 by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp)
 
 lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
-apply (induct "n")
-apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
-apply (auto simp add: real_of_nat_Suc left_distrib)
-apply (case_tac "0 < n")
-apply (drule_tac x = x in realpow_minus_mult)
-apply (auto simp add: mult_assoc add_commute)
+apply (cut_tac DERIV_power [OF DERIV_Id])
+apply (simp add: real_scaleR_def real_of_nat_def)
 done
 
 (* NS version *)
@@ -1172,15 +1299,12 @@
 text{*Power of -1*}
 
 lemma DERIV_inverse: "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
-by (simp add: NSDERIV_inverse NSDERIV_DERIV_iff [symmetric] del: realpow_Suc)
+by (drule DERIV_inverse' [OF DERIV_Id], simp)
 
 text{*Derivative of inverse*}
 lemma DERIV_inverse_fun: "[| DERIV f x :> d; f(x) \<noteq> 0 |]
       ==> DERIV (%x. inverse(f x)::real) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
-apply (simp only: mult_commute [of d] minus_mult_left power_inverse)
-apply (fold o_def)
-apply (blast intro!: DERIV_chain DERIV_inverse)
-done
+by (drule (1) DERIV_inverse', simp add: mult_ac)
 
 lemma NSDERIV_inverse_fun: "[| NSDERIV f x :> d; f(x) \<noteq> 0 |]
       ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
@@ -1189,13 +1313,7 @@
 text{*Derivative of quotient*}
 lemma DERIV_quotient: "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
        ==> DERIV (%y. f(y) / (g y) :: real) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
-apply (drule_tac f = g in DERIV_inverse_fun)
-apply (drule_tac [2] DERIV_mult)
-apply (assumption+)
-apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
-                 mult_ac diff_def
-     del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric])
-done
+by (drule (2) DERIV_divide, simp add: mult_commute)
 
 lemma NSDERIV_quotient: "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)