1(* Title: HOL/Nonstandard_Analysis/HDeriv.thy 2 Author: Jacques D. Fleuriot 3 Copyright: 1998 University of Cambridge 4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 5*) 6 7section \<open>Differentiation (Nonstandard)\<close> 8 9theory HDeriv 10 imports HLim 11begin 12 13text \<open>Nonstandard Definitions.\<close> 14 15definition nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" 16 ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 17 where "NSDERIV f x :> D \<longleftrightarrow> 18 (\<forall>h \<in> Infinitesimal - {0}. (( *f* f)(star_of x + h) - star_of (f x)) / h \<approx> star_of D)" 19 20definition NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 21 (infixl "NSdifferentiable" 60) 22 where "f NSdifferentiable x \<longleftrightarrow> (\<exists>D. NSDERIV f x :> D)" 23 24definition increment :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> hypreal \<Rightarrow> hypreal" 25 where "increment f x h = 26 (SOME inc. f NSdifferentiable x \<and> inc = ( *f* f) (hypreal_of_real x + h) - hypreal_of_real (f x))" 27 28 29subsection \<open>Derivatives\<close> 30 31lemma DERIV_NS_iff: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 32 by (simp add: DERIV_def LIM_NSLIM_iff) 33 34lemma NS_DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 35 by (simp add: DERIV_def LIM_NSLIM_iff) 36 37lemma Infinitesimal_of_hypreal: 38 "x \<in> Infinitesimal \<Longrightarrow> (( *f* of_real) x::'a::real_normed_div_algebra star) \<in> Infinitesimal" 39 by (metis Infinitesimal_of_hypreal_iff of_hypreal_def) 40 41lemma of_hypreal_eq_0_iff: "\<And>x. (( *f* of_real) x = (0::'a::real_algebra_1 star)) = (x = 0)" 42 by transfer (rule of_real_eq_0_iff) 43 44lemma NSDeriv_unique: 45 assumes "NSDERIV f x :> D" "NSDERIV f x :> E" 46 shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E" 47proof - 48 have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}" 49 by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal epsilon_not_zero singletonD) 50 with assms show ?thesis 51 by (meson approx_trans3 nsderiv_def star_of_approx_iff) 52qed 53 54text \<open>First \<open>NSDERIV\<close> in terms of \<open>NSLIM\<close>.\<close> 55 56text \<open>First equivalence.\<close> 57lemma NSDERIV_NSLIM_iff: "(NSDERIV f x :> D) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 58 by (auto simp add: nsderiv_def NSLIM_def starfun_lambda_cancel mem_infmal_iff) 59 60text \<open>Second equivalence.\<close> 61lemma NSDERIV_NSLIM_iff2: "(NSDERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D" 62 by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric]) 63 64text \<open>While we're at it!\<close> 65lemma NSDERIV_iff2: 66 "(NSDERIV f x :> D) \<longleftrightarrow> 67 (\<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)" 68 by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) 69 70lemma NSDERIVD5: 71 "\<lbrakk>NSDERIV f x :> D; u \<approx> hypreal_of_real x\<rbrakk> \<Longrightarrow> 72 ( *f* (\<lambda>z. f z - f x)) u \<approx> hypreal_of_real D * (u - hypreal_of_real x)" 73 unfolding NSDERIV_iff2 74 apply (case_tac "u = hypreal_of_real x", auto) 75 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) 76 77lemma NSDERIVD4: 78 "\<lbrakk>NSDERIV f x :> D; h \<in> Infinitesimal\<rbrakk> 79 \<Longrightarrow> ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x) \<approx> hypreal_of_real D * h" 80 apply (clarsimp simp add: nsderiv_def) 81 apply (case_tac "h = 0", simp) 82 by (meson DiffI Infinitesimal_approx Infinitesimal_ratio Infinitesimal_star_of_mult2 approx_star_of_HFinite singletonD) 83 84text \<open>Differentiability implies continuity nice and simple "algebraic" proof.\<close> 85lemma NSDERIV_isNSCont: 86 assumes "NSDERIV f x :> D" shows "isNSCont f x" 87 unfolding isNSCont_NSLIM_iff NSLIM_def 88proof clarify 89 fix x' 90 assume "x' \<noteq> star_of x" "x' \<approx> star_of x" 91 then have m0: "x' - star_of x \<in> Infinitesimal - {0}" 92 using bex_Infinitesimal_iff by auto 93 then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<approx> star_of D" 94 by (metis \<open>x' \<approx> star_of x\<close> add_diff_cancel_left' assms bex_Infinitesimal_iff2 nsderiv_def) 95 then have "(( *f* f) x' - star_of (f x)) / (x' - star_of x) \<in> HFinite" 96 by (metis approx_star_of_HFinite) 97 then show "( *f* f) x' \<approx> star_of (f x)" 98 by (metis (no_types) Diff_iff Infinitesimal_ratio m0 bex_Infinitesimal_iff insert_iff) 99qed 100 101text \<open>Differentiation rules for combinations of functions 102 follow from clear, straightforward, algebraic manipulations.\<close> 103 104text \<open>Constant function.\<close> 105 106(* use simple constant nslimit theorem *) 107lemma NSDERIV_const [simp]: "NSDERIV (\<lambda>x. k) x :> 0" 108 by (simp add: NSDERIV_NSLIM_iff) 109 110text \<open>Sum of functions- proved easily.\<close> 111 112lemma NSDERIV_add: 113 assumes "NSDERIV f x :> Da" "NSDERIV g x :> Db" 114 shows "NSDERIV (\<lambda>x. f x + g x) x :> Da + Db" 115proof - 116 have "((\<lambda>x. f x + g x) has_field_derivative Da + Db) (at x)" 117 using assms DERIV_NS_iff NSDERIV_NSLIM_iff field_differentiable_add by blast 118 then show ?thesis 119 by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff) 120qed 121 122text \<open>Product of functions - Proof is simple.\<close> 123 124lemma NSDERIV_mult: 125 assumes "NSDERIV g x :> Db" "NSDERIV f x :> Da" 126 shows "NSDERIV (\<lambda>x. f x * g x) x :> (Da * g x) + (Db * f x)" 127proof - 128 have "(f has_field_derivative Da) (at x)" "(g has_field_derivative Db) (at x)" 129 using assms by (simp_all add: DERIV_NS_iff NSDERIV_NSLIM_iff) 130 then have "((\<lambda>a. f a * g a) has_field_derivative Da * g x + Db * f x) (at x)" 131 using DERIV_mult by blast 132 then show ?thesis 133 by (simp add: DERIV_NS_iff NSDERIV_NSLIM_iff) 134qed 135 136text \<open>Multiplying by a constant.\<close> 137lemma NSDERIV_cmult: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. c * f x) x :> c * D" 138 unfolding times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff 139 minus_mult_right right_diff_distrib [symmetric] 140 by (erule NSLIM_const [THEN NSLIM_mult]) 141 142text \<open>Negation of function.\<close> 143lemma NSDERIV_minus: "NSDERIV f x :> D \<Longrightarrow> NSDERIV (\<lambda>x. - f x) x :> - D" 144proof (simp add: NSDERIV_NSLIM_iff) 145 assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D" 146 then have deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" 147 by (rule NSLIM_minus) 148 have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h" 149 by (simp add: minus_divide_left) 150 with deriv have "(\<lambda>h. (- f (x + h) + f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" 151 by simp 152 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" 153 by simp 154qed 155 156text \<open>Subtraction.\<close> 157lemma NSDERIV_add_minus: 158 "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x + - g x) x :> Da + - Db" 159 by (blast dest: NSDERIV_add NSDERIV_minus) 160 161lemma NSDERIV_diff: 162 "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da - Db" 163 using NSDERIV_add_minus [of f x Da g Db] by simp 164 165text \<open>Similarly to the above, the chain rule admits an entirely 166 straightforward derivation. Compare this with Harrison's 167 HOL proof of the chain rule, which proved to be trickier and 168 required an alternative characterisation of differentiability- 169 the so-called Carathedory derivative. Our main problem is 170 manipulation of terms.\<close> 171 172 173subsection \<open>Lemmas\<close> 174 175lemma NSDERIV_zero: 176 "\<lbrakk>NSDERIV g x :> D; ( *f* g) (star_of x + y) = star_of (g x); y \<in> Infinitesimal; y \<noteq> 0\<rbrakk> 177 \<Longrightarrow> D = 0" 178 by (force simp add: nsderiv_def) 179 180text \<open>Can be proved differently using \<open>NSLIM_isCont_iff\<close>.\<close> 181lemma NSDERIV_approx: 182 "NSDERIV f x :> D \<Longrightarrow> h \<in> Infinitesimal \<Longrightarrow> h \<noteq> 0 \<Longrightarrow> 183 ( *f* f) (star_of x + h) - star_of (f x) \<approx> 0" 184 by (meson DiffI Infinitesimal_ratio approx_star_of_HFinite mem_infmal_iff nsderiv_def singletonD) 185 186text \<open>From one version of differentiability 187 188 \<open>f x - f a\<close> 189 \<open>-------------- \<approx> Db\<close> 190 \<open>x - a\<close> 191\<close> 192 193lemma NSDERIVD1: 194 "\<lbrakk>NSDERIV f (g x) :> Da; 195 ( *f* g) (star_of x + y) \<noteq> star_of (g x); 196 ( *f* g) (star_of x + y) \<approx> star_of (g x)\<rbrakk> 197 \<Longrightarrow> (( *f* f) (( *f* g) (star_of x + y)) - 198 star_of (f (g x))) / (( *f* g) (star_of x + y) - star_of (g x)) \<approx> 199 star_of Da" 200 by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def) 201 202text \<open>From other version of differentiability 203 204 \<open>f (x + h) - f x\<close> 205 \<open>------------------ \<approx> Db\<close> 206 \<open>h\<close> 207\<close> 208 209lemma NSDERIVD2: "[| NSDERIV g x :> Db; y \<in> Infinitesimal; y \<noteq> 0 |] 210 ==> (( *f* g) (star_of(x) + y) - star_of(g x)) / y 211 \<approx> star_of(Db)" 212 by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) 213 214text \<open>This proof uses both definitions of differentiability.\<close> 215lemma NSDERIV_chain: 216 "NSDERIV f (g x) :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (f \<circ> g) x :> Da * Db" 217 using DERIV_NS_iff DERIV_chain NSDERIV_NSLIM_iff by blast 218 219text \<open>Differentiation of natural number powers.\<close> 220lemma NSDERIV_Id [simp]: "NSDERIV (\<lambda>x. x) x :> 1" 221 by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if) 222 223lemma NSDERIV_cmult_Id [simp]: "NSDERIV ((*) c) x :> c" 224 using NSDERIV_Id [THEN NSDERIV_cmult] by simp 225 226lemma NSDERIV_inverse: 227 fixes x :: "'a::real_normed_field" 228 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> 229 shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))" 230proof - 231 { 232 fix h :: "'a star" 233 assume h_Inf: "h \<in> Infinitesimal" 234 from this assms have not_0: "star_of x + h \<noteq> 0" 235 by (rule Infinitesimal_add_not_zero) 236 assume "h \<noteq> 0" 237 from h_Inf have "h * star_of x \<in> Infinitesimal" 238 by (rule Infinitesimal_HFinite_mult) simp 239 with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx> 240 inverse (- (star_of x * star_of x))" 241 proof - 242 have "- (h * star_of x) + - (star_of x * star_of x) \<approx> - (star_of x * star_of x)" 243 using \<open>h * star_of x \<in> Infinitesimal\<close> assms bex_Infinitesimal_iff by fastforce 244 then show ?thesis 245 by (metis assms mult_eq_0_iff neg_equal_0_iff_equal star_of_approx_inverse star_of_minus star_of_mult) 246 qed 247 moreover from not_0 \<open>h \<noteq> 0\<close> assms 248 have "inverse (- (h * star_of x) + - (star_of x * star_of x)) 249 = (inverse (star_of x + h) - inverse (star_of x)) / h" 250 by (simp add: division_ring_inverse_diff inverse_mult_distrib [symmetric] 251 inverse_minus_eq [symmetric] algebra_simps) 252 ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx> 253 - (inverse (star_of x) * inverse (star_of x))" 254 using assms by simp 255 } 256 then show ?thesis by (simp add: nsderiv_def) 257qed 258 259 260subsubsection \<open>Equivalence of NS and Standard definitions\<close> 261 262lemma divideR_eq_divide: "x /\<^sub>R y = x / y" 263 by (simp add: divide_inverse mult.commute) 264 265text \<open>Now equivalence between \<open>NSDERIV\<close> and \<open>DERIV\<close>.\<close> 266lemma NSDERIV_DERIV_iff: "NSDERIV f x :> D \<longleftrightarrow> DERIV f x :> D" 267 by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) 268 269text \<open>NS version.\<close> 270lemma NSDERIV_pow: "NSDERIV (\<lambda>x. x ^ n) x :> real n * (x ^ (n - Suc 0))" 271 by (simp add: NSDERIV_DERIV_iff DERIV_pow) 272 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