# Theory HDeriv

theory HDeriv
imports HLim
```(*  Title:      HOL/Nonstandard_Analysis/HDeriv.thy
Author:     Jacques D. Fleuriot
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

section ‹Differentiation (Nonstandard)›

theory HDeriv
imports HLim
begin

text ‹Nonstandard Definitions.›

definition nsderiv :: "['a::real_normed_field ⇒ 'a, 'a, 'a] ⇒ bool"
("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
where "NSDERIV f x :> D ⟷
(∀h ∈ Infinitesimal - {0}. (( *f* f)(star_of x + h) - star_of (f x)) / h ≈ star_of D)"

definition NSdifferentiable :: "['a::real_normed_field ⇒ 'a, 'a] ⇒ bool"
(infixl "NSdifferentiable" 60)
where "f NSdifferentiable x ⟷ (∃D. NSDERIV f x :> D)"

definition increment :: "(real ⇒ real) ⇒ real ⇒ hypreal ⇒ hypreal"
where "increment f x h =
(SOME inc. f NSdifferentiable x ∧ inc = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x))"

subsection ‹Derivatives›

lemma DERIV_NS_iff: "(DERIV f x :> D) ⟷ (λh. (f (x + h) - f x) / h) ─0→⇩N⇩S D"

lemma NS_DERIV_D: "DERIV f x :> D ⟹ (λh. (f (x + h) - f x) / h) ─0→⇩N⇩S D"

lemma hnorm_of_hypreal: "⋀r. hnorm (( *f* of_real) r::'a::real_normed_div_algebra star) = ¦r¦"
by transfer (rule norm_of_real)

lemma Infinitesimal_of_hypreal:
"x ∈ Infinitesimal ⟹ (( *f* of_real) x::'a::real_normed_div_algebra star) ∈ Infinitesimal"
apply (rule InfinitesimalI2)
apply (drule (1) InfinitesimalD2)
done

lemma of_hypreal_eq_0_iff: "⋀x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)"
by transfer (rule of_real_eq_0_iff)

lemma NSDeriv_unique: "NSDERIV f x :> D ⟹ NSDERIV f x :> E ⟹ D = E"
apply (subgoal_tac "( *f* of_real) ε ∈ Infinitesimal - {0::'a star}")
apply (simp only: nsderiv_def)
apply (drule (1) bspec)+
apply (drule (1) approx_trans3)
apply simp
done

text ‹First ‹NSDERIV› in terms of ‹NSLIM›.›

text ‹First equivalence.›
lemma NSDERIV_NSLIM_iff: "(NSDERIV f x :> D) ⟷ (λh. (f (x + h) - f x) / h) ─0→⇩N⇩S D"
apply (auto simp add: nsderiv_def NSLIM_def)
apply (drule_tac x = xa in bspec)
apply (rule_tac [3] ccontr)
apply (drule_tac [3] x = h in spec)
apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
done

text ‹Second equivalence.›
lemma NSDERIV_NSLIM_iff2: "(NSDERIV f x :> D) ⟷ (λz. (f z - f x) / (z - x)) ─x→⇩N⇩S D"
by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])

text ‹While we're at it!›
lemma NSDERIV_iff2:
"(NSDERIV f x :> D) ⟷
(∀w. w ≠ star_of x ∧ w ≈ star_of x ⟶ ( *f* (λz. (f z - f x) / (z - x))) w ≈ star_of D)"

(* FIXME delete *)
lemma hypreal_not_eq_minus_iff: "x ≠ a ⟷ x - a ≠ (0::'a::ab_group_add)"
by auto

lemma NSDERIVD5:
"(NSDERIV f x :> D) ⟹
(∀u. u ≈ hypreal_of_real x ⟶
( *f* (λz. f z - f x)) u ≈ hypreal_of_real D * (u - hypreal_of_real x))"
apply (case_tac "u = hypreal_of_real x", auto)
apply (drule_tac x = u in spec, auto)
apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
apply (subgoal_tac [2] "( *f* (λz. z - x)) u ≠ (0::hypreal) ")
apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
Infinitesimal_subset_HFinite [THEN subsetD])
done

lemma NSDERIVD4:
"(NSDERIV f x :> D) ⟹
(∀h ∈ Infinitesimal.
( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) ≈ hypreal_of_real D * h)"
apply (case_tac "h = 0")
apply auto
apply (drule_tac x = h in bspec)
apply (drule_tac [2] c = h in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
done

lemma NSDERIVD3:
"(NSDERIV f x :> D) ⟹
∀h ∈ Infinitesimal - {0}.
(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) ≈ hypreal_of_real D * h"
apply (rule ccontr, drule_tac x = h in bspec)
apply (drule_tac [2] c = h in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
done

text ‹Differentiability implies continuity nice and simple "algebraic" proof.›
lemma NSDERIV_isNSCont: "NSDERIV f x :> D ⟹ isNSCont f x"
apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
apply (drule approx_minus_iff [THEN iffD1])
apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
apply (drule_tac x = "xa - star_of x" in bspec)
apply (drule_tac c = "xa - star_of x" in approx_mult1)
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
apply (drule_tac x3=D in
HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult, THEN mem_infmal_iff [THEN iffD1]])
apply (auto simp add: mult.commute intro: approx_trans approx_minus_iff [THEN iffD2])
done

text ‹Differentiation rules for combinations of functions
follow from clear, straightforard, algebraic manipulations.›

text ‹Constant function.›

(* use simple constant nslimit theorem *)
lemma NSDERIV_const [simp]: "NSDERIV (λx. k) x :> 0"

text ‹Sum of functions- proved easily.›

"NSDERIV f x :> Da ⟹ NSDERIV g x :> Db ⟹ NSDERIV (λx. f x + g x) x :> Da + Db"
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
apply (auto simp add: ac_simps algebra_simps)
done

text ‹Product of functions - Proof is trivial but tedious
and long due to rearrangement of terms.›

lemma lemma_nsderiv1: "(a * b) - (c * d) = (b * (a - c)) + (c * (b - d))"
for a b c d :: "'a::comm_ring star"

lemma lemma_nsderiv2: "(x - y) / z = star_of D + yb ⟹ z ≠ 0 ⟹
z ∈ Infinitesimal ⟹ yb ∈ Infinitesimal ⟹ x - y ≈ 0"
for x y z :: "'a::real_normed_field star"
apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
done

lemma NSDERIV_mult:
"NSDERIV f x :> Da ⟹ NSDERIV g x :> Db ⟹
NSDERIV (λx. f x * g x) x :> (Da * g x) + (Db * f x)"
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nsderiv1)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
apply (auto simp add: times_divide_eq_right [symmetric]
simp del: times_divide_eq_right times_divide_eq_left)
apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
apply (rule_tac b1 = "star_of Db * star_of (f x)" in add.commute [THEN subst])
apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
done

text ‹Multiplying by a constant.›
lemma NSDERIV_cmult: "NSDERIV f x :> D ⟹ NSDERIV (λx. c * f x) x :> c * D"
apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
minus_mult_right right_diff_distrib [symmetric])
apply (erule NSLIM_const [THEN NSLIM_mult])
done

text ‹Negation of function.›
lemma NSDERIV_minus: "NSDERIV f x :> D ⟹ NSDERIV (λx. - f x) x :> - D"
assume "(λh. (f (x + h) - f x) / h) ─0→⇩N⇩S D"
then have deriv: "(λh. - ((f(x+h) - f x) / h)) ─0→⇩N⇩S - D"
by (rule NSLIM_minus)
have "∀h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
with deriv have "(λh. (- f (x + h) + f x) / h) ─0→⇩N⇩S - D"
by simp
then show "(λh. (f (x + h) - f x) / h) ─0→⇩N⇩S D ⟹ (λh. (f x - f (x + h)) / h) ─0→⇩N⇩S - D"
by simp
qed

text ‹Subtraction.›
"NSDERIV f x :> Da ⟹ NSDERIV g x :> Db ⟹ NSDERIV (λx. f x + - g x) x :> Da + - Db"

lemma NSDERIV_diff:
"NSDERIV f x :> Da ⟹ NSDERIV g x :> Db ⟹ NSDERIV (λx. f x - g x) x :> Da - Db"
using NSDERIV_add_minus [of f x Da g Db] by simp

text ‹Similarly to the above, the chain rule admits an entirely
straightforward derivation. Compare this with Harrison's
HOL proof of the chain rule, which proved to be trickier and
required an alternative characterisation of differentiability-
the so-called Carathedory derivative. Our main problem is
manipulation of terms.›

subsection ‹Lemmas›

lemma NSDERIV_zero:
"NSDERIV g x :> D ⟹ ( *f* g) (star_of x + xa) = star_of (g x) ⟹
xa ∈ Infinitesimal ⟹ xa ≠ 0 ⟹ D = 0"
apply (drule bspec)
apply auto
done

text ‹Can be proved differently using ‹NSLIM_isCont_iff›.›
lemma NSDERIV_approx:
"NSDERIV f x :> D ⟹ h ∈ Infinitesimal ⟹ h ≠ 0 ⟹
( *f* f) (star_of x + h) - star_of (f x) ≈ 0"
apply (rule Infinitesimal_ratio)
apply (rule_tac [3] approx_star_of_HFinite, auto)
done

text ‹From one version of differentiability

‹f x - f a›
‹-------------- ≈ Db›
‹x - a›
›

lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da;
( *f* g) (star_of(x) + xa) ≠ star_of (g x);
( *f* g) (star_of(x) + xa) ≈ star_of (g x)
|] ==> (( *f* f) (( *f* g) (star_of(x) + xa))
- star_of (f (g x)))
/ (( *f* g) (star_of(x) + xa) - star_of (g x))
≈ star_of(Da)"
by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)

text ‹From other version of differentiability

‹f (x + h) - f x›
‹------------------ ≈ Db›
‹h›
›

lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa ∈ Infinitesimal; xa ≠ 0 |]
==> (( *f* g) (star_of(x) + xa) - star_of(g x)) / xa
≈ star_of(Db)"
by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel)

lemma lemma_chain: "z ≠ 0 ⟹ x * y = (x * inverse z) * (z * y)"
for x y z :: "'a::real_normed_field star"
proof -
assume z: "z ≠ 0"
have "x * y = x * (inverse z * z) * y" by (simp add: z)
then show ?thesis by (simp add: mult.assoc)
qed

text ‹This proof uses both definitions of differentiability.›
lemma NSDERIV_chain:
"NSDERIV f (g x) :> Da ⟹ NSDERIV g x :> Db ⟹ NSDERIV (f ∘ g) x :> Da * Db"
apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff [symmetric])
apply clarify
apply (frule_tac f = g in NSDERIV_approx)
apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
apply (drule_tac g = g in NSDERIV_zero)
apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
in lemma_chain [THEN ssubst])
apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
apply (rule approx_mult_star_of)
apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2])
apply (blast intro: NSDERIVD2)
done

text ‹Differentiation of natural number powers.›
lemma NSDERIV_Id [simp]: "NSDERIV (λx. x) x :> 1"
by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)

lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
using NSDERIV_Id [THEN NSDERIV_cmult] by simp

lemma NSDERIV_inverse:
fixes x :: "'a::real_normed_field"
assumes "x ≠ 0" ― ‹can't get rid of @{term "x ≠ 0"} because it isn't continuous at zero›
shows "NSDERIV (λx. inverse x) x :> - (inverse x ^ Suc (Suc 0))"
proof -
{
fix h :: "'a star"
assume h_Inf: "h ∈ Infinitesimal"
from this assms have not_0: "star_of x + h ≠ 0"
assume "h ≠ 0"
from h_Inf have "h * star_of x ∈ Infinitesimal"
by (rule Infinitesimal_HFinite_mult) simp
with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) ≈
inverse (- (star_of x * star_of x))"
apply -
apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
done
moreover from not_0 ‹h ≠ 0› assms
have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
(inverse (star_of x + h) - inverse (star_of x)) / h"
apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
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
done
ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h ≈
- (inverse (star_of x) * inverse (star_of x))"
using assms by simp
}
then show ?thesis by (simp add: nsderiv_def)
qed

subsubsection ‹Equivalence of NS and Standard definitions›

lemma divideR_eq_divide: "x /⇩R y = x / y"

text ‹Now equivalence between ‹NSDERIV› and ‹DERIV›.›
lemma NSDERIV_DERIV_iff: "NSDERIV f x :> D ⟷ DERIV f x :> D"
by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)

text ‹NS version.›
lemma NSDERIV_pow: "NSDERIV (λx. x ^ n) x :> real n * (x ^ (n - Suc 0))"

text ‹Derivative of inverse.›
lemma NSDERIV_inverse_fun:
"NSDERIV f x :> d ⟹ f x ≠ 0 ⟹
NSDERIV (λx. inverse (f x)) x :> (- (d * inverse (f x ^ Suc (Suc 0))))"
for x :: "'a::{real_normed_field}"
by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)

text ‹Derivative of quotient.›
lemma NSDERIV_quotient:
fixes x :: "'a::real_normed_field"
shows "NSDERIV f x :> d ⟹ NSDERIV g x :> e ⟹ g x ≠ 0 ⟹
NSDERIV (λy. f y / g y) x :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))"
by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: power_Suc)

lemma CARAT_NSDERIV:
"NSDERIV f x :> l ⟹ ∃g. (∀z. f z - f x = g z * (z - x)) ∧ isNSCont g x ∧ g x = l"
by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV mult.commute)

lemma hypreal_eq_minus_iff3: "x = y + z ⟷ x + - z = y"
for x y z :: hypreal
by auto

lemma CARAT_DERIVD:
assumes all: "∀z. f z - f x = g z * (z - x)"
and nsc: "isNSCont g x"
shows "NSDERIV f x :> g x"
proof -
from nsc have "∀w. w ≠ star_of x ∧ w ≈ star_of x ⟶
( *f* g) w * (w - star_of x) / (w - star_of x) ≈ star_of (g x)"
with all show ?thesis
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
qed

subsubsection ‹Differentiability predicate›

lemma NSdifferentiableD: "f NSdifferentiable x ⟹ ∃D. NSDERIV f x :> D"

lemma NSdifferentiableI: "NSDERIV f x :> D ⟹ f NSdifferentiable x"

subsection ‹(NS) Increment›

lemma incrementI:
"f NSdifferentiable x ⟹
increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"

lemma incrementI2:
"NSDERIV f x :> D ⟹
increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)"
by (erule NSdifferentiableI [THEN incrementI])

text ‹The Increment theorem -- Keisler p. 65.›
lemma increment_thm:
"NSDERIV f x :> D ⟹ h ∈ Infinitesimal ⟹ h ≠ 0 ⟹
∃e ∈ Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
apply (frule_tac h = h in incrementI2, simp add: nsderiv_def)
apply (drule bspec, auto)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify)
apply (frule_tac b1 = "hypreal_of_real D + y" 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
done

lemma increment_thm2:
"NSDERIV f x :> D ⟹ h ≈ 0 ⟹ h ≠ 0 ⟹
∃e ∈ Infinitesimal. increment f x h = hypreal_of_real D * h + e * h"
by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm)

lemma increment_approx_zero: "NSDERIV f x :> D ⟹ h ≈ 0 ⟹ h ≠ 0 ⟹ increment f x h ≈ 0"
apply (drule increment_thm2)
simp add: distrib_right [symmetric] mem_infmal_iff [symmetric])
apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
done

end
```