10SN/A(* Title: HOL/Nonstandard_Analysis/HDeriv.thy 26073SN/A Author: Jacques D. Fleuriot 30SN/A Copyright: 1998 University of Cambridge 40SN/A Conversion to Isar and new proofs by Lawrence C Paulson, 2004 50SN/A*) 60SN/A 72362SN/Asection \<open>Differentiation (Nonstandard)\<close> 80SN/A 92362SN/Atheory HDeriv 100SN/A imports HLim 110SN/Abegin 120SN/A 130SN/Atext \<open>Nonstandard Definitions.\<close> 140SN/A 150SN/Adefinition nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" 160SN/A ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 170SN/A where "NSDERIV f x :> D \<longleftrightarrow> 180SN/A (\<forall>h \<in> Infinitesimal - {0}. (( *f* f)(star_of x + h) - star_of (f x)) / h \<approx> star_of D)" 190SN/A 200SN/Adefinition NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 212362SN/A (infixl "NSdifferentiable" 60) 222362SN/A where "f NSdifferentiable x \<longleftrightarrow> (\<exists>D. NSDERIV f x :> D)" 232362SN/A 240SN/Adefinition increment :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> hypreal \<Rightarrow> hypreal" 250SN/A where "increment f x h = 260SN/A (SOME inc. f NSdifferentiable x \<and> inc = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x))" 270SN/A 280SN/A 290SN/Asubsection \<open>Derivatives\<close> 300SN/A 310SN/Alemma DERIV_NS_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 320SN/A by (simp add: DERIV_def LIM_NSLIM_iff) 330SN/A 340SN/Alemma NS_DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 350SN/A by (simp add: DERIV_def LIM_NSLIM_iff) 360SN/A 370SN/Alemma Infinitesimal_of_hypreal: 380SN/A "x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal" 390SN/A by (metis Infinitesimal_of_hypreal_iff of_hypreal_def) 400SN/A 410SN/Alemma of_hypreal_eq_0_iff: "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)" 420SN/A by transfer (rule of_real_eq_0_iff) 430SN/A 440SN/Alemma NSDeriv_unique: 450SN/A assumes "NSDERIV f x :> D" "NSDERIV f x :> E" 460SN/A shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E" 470SN/Aproof - 480SN/A have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}" 490SN/A by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal epsilon_not_zero singletonD) 505466SN/A with assms show ?thesis 510SN/A by (meson approx_trans3 nsderiv_def star_of_approx_iff) 520SN/Aqed 530SN/A 540SN/Atext \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close> 550SN/A 560SN/Atext \<open>First equivalence.\<close> 570SN/Alemma NSDERIV_NSLIM_iff: "(NSDERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 580SN/A by (auto simp add: nsderiv_def NSLIM_def starfun_lambda_cancel mem_infmal_iff) 590SN/A 605466SN/Atext \<open>Second equivalence.\<close> 615466SN/Alemma NSDERIV_NSLIM_iff2: "(NSDERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D" 620SN/A by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric]) 635466SN/A 645466SN/Atext \<open>While we're at it!\<close> 650SN/Alemma NSDERIV_iff2: 665466SN/A "(NSDERIV f x :> D) \<longleftrightarrow> 670SN/A (\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> ( *f* (\<lambda>z. (f z - f x) / (z - x))) w \<approx> star_of D)" 680SN/A by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) 690SN/A 700SN/Alemma NSDERIVD5: 710SN/A "\<lbrakk>NSDERIV f x :> D; u \<approx> hypreal_of_real x\<rbrakk> \<Longrightarrow> 720SN/A ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x)" 730SN/A unfolding NSDERIV_iff2 740SN/A apply (case_tac "u = hypreal_of_real x", auto) 750SN/A by (metis (mono_tags, lifting) HFinite_star_of Infinitesimal_ratio approx_def approx_minus_iff approx_mult_subst approx_star_of_HFinite approx_sym mult_zero_right right_minus_eq) 760SN/A 770SN/Alemma NSDERIVD4: 780SN/A "\<lbrakk>NSDERIV f x :> D; h \<in> Infinitesimal\<rbrakk> 790SN/A \<Longrightarrow> ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h" 800SN/A apply (clarsimp simp add: nsderiv_def) 810SN/A apply (case_tac "h = 0", simp) 820SN/A by (meson DiffI Infinitesimal_approx Infinitesimal_ratio Infinitesimal_star_of_mult2 approx_star_of_HFinite singletonD) 830SN/A 840SN/Atext \<open>Differentiability implies continuity nice and simple "algebraic" proof.\<close> 850SN/Alemma NSDERIV_isNSCont: 860SN/A assumes "NSDERIV f x :> D" shows "isNSCont f x" 870SN/A unfolding isNSCont_NSLIM_iff NSLIM_def 880SN/Aproof clarify 890SN/A fix x' 905466SN/A assume "x' \<noteq> star_of x" "x' \<approx> star_of x" 910SN/A then have m0: "x' - star_of x \<in> Infinitesimal - {0}" 920SN/A using bex_Infinitesimal_iff by auto 930SN/A then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<approx> star_of D" 940SN/A by (metis \<open>x' \<approx> star_of x\<close> add_diff_cancel_left' assms bex_Infinitesimal_iff2 nsderiv_def) 950SN/A then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<in> HFinite" 960SN/A by (metis approx_star_of_HFinite) 970SN/A then show "( *f* f) x' \<approx> star_of (f x)" 980SN/A by (metis (no_types) Diff_iff Infinitesimal_ratio m0 bex_Infinitesimal_iff insert_iff) 990SN/Aqed 1000SN/A 1010SN/Atext \<open>Differentiation rules for combinations of functions 1020SN/A follow from clear, straightforward, algebraic manipulations.\<close> 1030SN/A 1040SN/Atext \<open>Constant function.\<close> 1050SN/A 1060SN/A(* use simple constant nslimit theorem *) 1070SN/Alemma NSDERIV_const [simp]: "NSDERIV (\<lambda>x. k) x :> 0" 1080SN/A by (simp add: NSDERIV_NSLIM_iff) 1090SN/A 1100SN/Atext \<open>Sum of functions- proved easily.\<close> 1110SN/A 1120SN/Alemma NSDERIV_add: 1130SN/A assumes "NSDERIV f x :> Da" "NSDERIV g x :> Db" 1140SN/A shows "NSDERIV (\<lambda>x. f x + g x) x :> Da + Db" 1150SN/Aproof - 1160SN/A have "((\<lambda>x. f x + g x) has_field_derivative Da + Db) (at x)" 1170SN/A using assms DERIV_NS_iff NSDERIV_NSLIM_iff field_differentiable_add by blast 1180SN/A then show ?thesis 1190SN/A by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff) 1200SN/Aqed 1210SN/A 1220SN/Atext \<open>Product of functions - Proof is simple.\<close> 1230SN/A 1240SN/Alemma NSDERIV_mult: 1250SN/A assumes "NSDERIV g x :> Db" "NSDERIV f x :> Da" 1260SN/A shows "NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)" 1270SN/Aproof - 1280SN/A have "(f has_field_derivative Da) (at x)" "(g has_field_derivative Db) (at x)" 1290SN/A using assms by (simp_all add: DERIV_NS_iff NSDERIV_NSLIM_iff) 1300SN/A then have "((\<lambda>a. f a * g a) has_field_derivative Da * g x + Db * f x) (at x)" 1310SN/A using DERIV_mult by blast 1320SN/A then show ?thesis 1330SN/A by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff) 1340SN/Aqed 1350SN/A 1360SN/Atext \<open>Multiplying by a constant.\<close> 1370SN/Alemma NSDERIV_cmult: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. c * f x) x :> c * D" 1380SN/A unfolding times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff 1390SN/A minus_mult_right right_diff_distrib [symmetric] 1400SN/A by (erule NSLIM_const [THEN NSLIM_mult]) 1410SN/A 1420SN/Atext \<open>Negation of function.\<close> 1430SN/Alemma NSDERIV_minus: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. - f x) x :> - D" 1440SN/Aproof (simp add: NSDERIV_NSLIM_iff) 1450SN/A assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 1460SN/A then have deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" 1470SN/A by (rule NSLIM_minus) 1480SN/A have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h" 1490SN/A by (simp add: minus_divide_left) 1500SN/A with deriv have "(\<lambda>h. (- f (x + h) + f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" 1510SN/A by simp 1520SN/A then show "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D \<Longrightarrow> (\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" 1530SN/A by simp 1545466SN/Aqed 1550SN/A 1560SN/Atext \<open>Subtraction.\<close> 1570SN/Alemma NSDERIV_add_minus: 1580SN/A "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + - g x) x :> Da + - Db" 1590SN/A by (blast dest: NSDERIV_add NSDERIV_minus) 1600SN/A 1615466SN/Alemma NSDERIV_diff: 1620SN/A "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da - Db" 1630SN/A using NSDERIV_add_minus [of f x Da g Db] by simp 1640SN/A 1655466SN/Atext \<open>Similarly to the above, the chain rule admits an entirely 1660SN/A straightforward derivation. Compare this with Harrison's 1670SN/A HOL proof of the chain rule, which proved to be trickier and 1680SN/A required an alternative characterisation of differentiability- 1690SN/A the so-called Carathedory derivative. Our main problem is 1700SN/A manipulation of terms.\<close> 1710SN/A 1720SN/A 1730SN/Asubsection \<open>Lemmas\<close> 1740SN/A 1750SN/Alemma NSDERIV_zero: 1760SN/A "\<lbrakk>NSDERIV g x :> D; ( *f* g) (star_of x + y) = star_of (g x); y \<in> Infinitesimal; y \<noteq> 0\<rbrakk> 1770SN/A \<Longrightarrow> D = 0" 1780SN/A by (force simp add: nsderiv_def) 1790SN/A 1800SN/Atext \<open>Can be proved differently using \<open>NSLIM_isCont_iff\<close>.\<close> 1810SN/Alemma NSDERIV_approx: 1820SN/A "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> 1835466SN/A ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0" 1840SN/A by (meson DiffI Infinitesimal_ratio approx_star_of_HFinite mem_infmal_iff nsderiv_def singletonD) 1855466SN/A 1860SN/Atext \<open>From one version of differentiability 1875466SN/A 1880SN/A \<open>f x - f a\<close> 1895466SN/A \<open>-------------- \<approx> Db\<close> 1900SN/A \<open>x - a\<close> 1910SN/A\<close> 1920SN/A 1930SN/Alemma NSDERIVD1: 1940SN/A "\<lbrakk>NSDERIV f (g x) :> Da; 1950SN/A ( *f* g) (star_of x + y) \<noteq> star_of (g x); 1960SN/A ( *f* g) (star_of x + y) \<approx> star_of (g x)\<rbrakk> 1970SN/A \<Longrightarrow> (( *f* f) (( *f* g) (star_of x + y)) - 1980SN/A star_of (f (g x))) / (( *f* g) (star_of x + y) - star_of (g x)) \<approx> 1990SN/A star_of Da" 2000SN/A by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def) 2010SN/A 2020SN/Atext \<open>From other version of differentiability 2030SN/A 2040SN/A \<open>f (x + h) - f x\<close> 2050SN/A \<open>------------------ \<approx> Db\<close> 2060SN/A \<open>h\<close> 2070SN/A\<close> 2080SN/A 2090SN/Alemma NSDERIVD2: "[| NSDERIV g x :> Db; y \<in> Infinitesimal; y \<noteq> 0 |] 2100SN/A ==> (( *f* g) (star_of(x) + y) - star_of(g x)) / y 2110SN/A \<approx> star_of(Db)" 2120SN/A by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) 2130SN/A 2140SN/Atext \<open>This proof uses both definitions of differentiability.\<close> 2150SN/Alemma NSDERIV_chain: 2160SN/A "NSDERIV f (g x) :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (f \<circ> g) x :> Da * Db" 2170SN/A using DERIV_NS_iff DERIV_chain NSDERIV_NSLIM_iff by blast 2180SN/A 2190SN/Atext \<open>Differentiation of natural number powers.\<close> 2200SN/Alemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1" 2210SN/A by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if) 2220SN/A 2230SN/Alemma NSDERIV_cmult_Id [simp]: "NSDERIV ((*) c) x :> c" 2240SN/A using NSDERIV_Id [THEN NSDERIV_cmult] by simp 2250SN/A 2260SN/Alemma NSDERIV_inverse: 2270SN/A fixes x :: "'a::real_normed_field" 2280SN/A assumes "x \<noteq> 0" \<comment> \<open>can't get rid of \<^term>\<open>x \<noteq> 0\<close> because it isn't continuous at zero\<close> 2290SN/A shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))" 2300SN/Aproof - 2310SN/A { 2320SN/A fix h :: "'a star" 2330SN/A assume h_Inf: "h \<in> Infinitesimal" 2340SN/A from this assms have not_0: "star_of x + h \<noteq> 0" 23510089SN/A by (rule Infinitesimal_add_not_zero) 23610089SN/A assume "h \<noteq> 0" 2370SN/A from h_Inf have "h * star_of x \<in> Infinitesimal" 2380SN/A by (rule Infinitesimal_HFinite_mult) simp 23910089SN/A with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx> 2400SN/A inverse (- (star_of x * star_of x))" 24110089SN/A proof - 24210089SN/A have "- (h * star_of x) + - (star_of x * star_of x) \<approx> - (star_of x * star_of x)" 24310089SN/A using \<open>h * star_of x \<in> Infinitesimal\<close> assms bex_Infinitesimal_iff by fastforce 2440SN/A then show ?thesis 2450SN/A by (metis assms mult_eq_0_iff neg_equal_0_iff_equal star_of_approx_inverse star_of_minus star_of_mult) 2460SN/A qed 2470SN/A moreover from not_0 \<open>h \<noteq> 0\<close> assms 2480SN/A have "inverse (- (h * star_of x) + - (star_of x * star_of x)) 2490SN/A = (inverse (star_of x + h) - inverse (star_of x)) / h" 2500SN/A by (simp add: division_ring_inverse_diff inverse_mult_distrib [symmetric] 2510SN/A inverse_minus_eq [symmetric] algebra_simps) 2520SN/A ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx> 2530SN/A - (inverse (star_of x) * inverse (star_of x))" 2540SN/A using assms by simp 2550SN/A } 2560SN/A then show ?thesis by (simp add: nsderiv_def) 2570SN/Aqed 2580SN/A 2590SN/A 2600SN/Asubsubsection \<open>Equivalence of NS and Standard definitions\<close> 2610SN/A 2620SN/Alemma divideR_eq_divide: "x /\<^sub>R y = x / y" 2630SN/A by (simp add: divide_inverse mult.commute) 2640SN/A 2650SN/Atext \<open>Now equivalence between \<open>NSDERIV\<close> and \<open>DERIV\<close>.\<close> 2660SN/Alemma NSDERIV_DERIV_iff: "NSDERIV f x :> D \<longleftrightarrow> DERIV f x :> D" 2670SN/A by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) 2680SN/A 2690SN/Atext \<open>NS version.\<close> 2700SN/Alemma NSDERIV_pow: "NSDERIV (\<lambda>x. x ^ n) x :> real n * (x ^ (n - Suc 0))" 2710SN/A by (simp add: NSDERIV_DERIV_iff DERIV_pow) 2720SN/A 273text \<open>Derivative of inverse.\<close> 274lemma NSDERIV_inverse_fun: 275 "NSDERIV f x :> d \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> 276 NSDERIV (\<lambda>x. inverse (f x)) x :> (- (d * inverse (f x ^ Suc (Suc 0))))" 277 for x :: "'a::{real_normed_field}" 278 by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc) 279 280text \<open>Derivative of quotient.\<close> 281lemma NSDERIV_quotient: 282 fixes x :: "'a::real_normed_field" 283 shows "NSDERIV f x :> d \<Longrightarrow> NSDERIV g x :> e \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow> 284 NSDERIV (\<lambda>y. f y / g y) x :> (d * g x - (e * f x)) / (g x ^ Suc (Suc 0))" 285 by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: power_Suc) 286 287lemma CARAT_NSDERIV: 288 "NSDERIV f x :> l \<Longrightarrow> \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isNSCont g x \<and> g x = l" 289 by (simp add: CARAT_DERIV NSDERIV_DERIV_iff isNSCont_isCont_iff) 290 291lemma hypreal_eq_minus_iff3: "x = y + z \<longleftrightarrow> x + - z = y" 292 for x y z :: hypreal 293 by auto 294 295lemma CARAT_DERIVD: 296 assumes all: "\<forall>z. f z - f x = g z * (z - x)" 297 and nsc: "isNSCont g x" 298 shows "NSDERIV f x :> g x" 299proof - 300 from nsc have "\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> 301 ( *f* g) w * (w - star_of x) / (w - star_of x) \<approx> star_of (g x)" 302 by (simp add: isNSCont_def) 303 with all show ?thesis 304 by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) 305qed 306 307 308subsubsection \<open>Differentiability predicate\<close> 309 310lemma NSdifferentiableD: "f NSdifferentiable x \<Longrightarrow> \<exists>D. NSDERIV f x :> D" 311 by (simp add: NSdifferentiable_def) 312 313lemma NSdifferentiableI: "NSDERIV f x :> D \<Longrightarrow> f NSdifferentiable x" 314 by (force simp add: NSdifferentiable_def) 315 316 317subsection \<open>(NS) Increment\<close> 318 319lemma incrementI: 320 "f NSdifferentiable x \<Longrightarrow> 321 increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)" 322 by (simp add: increment_def) 323 324lemma incrementI2: 325 "NSDERIV f x :> D \<Longrightarrow> 326 increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)" 327 by (erule NSdifferentiableI [THEN incrementI]) 328 329text \<open>The Increment theorem -- Keisler p. 65.\<close> 330lemma increment_thm: 331 assumes "NSDERIV f x :> D" "h \<in> Infinitesimal" "h \<noteq> 0" 332 shows "\<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real D * h + e * h" 333proof - 334 have inc: "increment f x h = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)" 335 using assms(1) incrementI2 by auto 336 have "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h \<approx> hypreal_of_real D" 337 by (simp add: NSDERIVD2 assms) 338 then obtain y where "y \<in> Infinitesimal" 339 "(( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x)) / h = hypreal_of_real D + y" 340 by (metis bex_Infinitesimal_iff2) 341 then have "increment f x h / h = hypreal_of_real D + y" 342 by (metis inc) 343 then show ?thesis 344 by (metis (no_types) \<open>y \<in> Infinitesimal\<close> \<open>h \<noteq> 0\<close> distrib_right mult.commute nonzero_mult_div_cancel_left times_divide_eq_right) 345qed 346 347lemma increment_approx_zero: "NSDERIV f x :> D \<Longrightarrow> h \<approx> 0 \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> increment f x h \<approx> 0" 348 by (simp add: NSDERIV_approx incrementI2 mem_infmal_iff) 349 350end 351