# HG changeset patch # User huffman # Date 1162595526 -3600 # Node ID 8fb49f668511db18e6d56f43925cba7569f82fa8 # Parent 0742fc979c674e437dae6f44f53cb691d83ff7b9 moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs diff -r 0742fc979c67 -r 8fb49f668511 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sat Nov 04 00:11:11 2006 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Sat Nov 04 00:12:06 2006 +0100 @@ -3,10 +3,9 @@ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Conversion to Isar and new proofs by Lawrence C Paulson, 2004 - GMVT by Benjamin Porter, 2005 *) -header{*Limits, Continuity and Differentiation*} +header{* Limits and Continuity *} theory Lim imports SEQ @@ -34,28 +33,6 @@ "isNSCont f a = (\y. y @= star_of a --> ( *f* f) y @= star_of (f a))" - deriv :: "[real \ 'a::real_normed_vector, real, 'a] \ bool" - --{*Differentiation: D is derivative of function f at x*} - ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) - "DERIV f x :> D = ((%h. (f(x + h) - f x) /# h) -- 0 --> D)" - - nsderiv :: "[real=>real,real,real] => bool" - ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) - "NSDERIV f x :> D = (\h \ Infinitesimal - {0}. - (( *f* f)(hypreal_of_real x + h) - - hypreal_of_real (f x))/h @= hypreal_of_real D)" - - differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) - "f differentiable x = (\D. DERIV f x :> D)" - - NSdifferentiable :: "[real=>real,real] => bool" - (infixl "NSdifferentiable" 60) - "f NSdifferentiable x = (\D. NSDERIV f x :> D)" - - increment :: "[real=>real,real,hypreal] => hypreal" - "increment f x h = (@inc. f NSdifferentiable x & - inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))" - isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" "isUCont f = (\r>0. \s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r)" @@ -63,16 +40,6 @@ "isNSUCont f = (\x y. x @= y --> ( *f* f) x @= ( *f* f) y)" -consts - Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" -primrec - "Bolzano_bisect P a b 0 = (a,b)" - "Bolzano_bisect P a b (Suc n) = - (let (x,y) = Bolzano_bisect P a b n - in if P(x, (x+y)/2) then ((x+y)/2, y) - else (x, (x+y)/2))" - - subsection {* Limits of Functions *} subsubsection {* Purely standard proofs *} @@ -92,7 +59,7 @@ ==> \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r" by (simp add: LIM_eq) -lemma LIM_shift: "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" +lemma LIM_offset: "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" apply (rule LIM_I) apply (drule_tac r="r" in LIM_D, safe) apply (rule_tac x="s" in exI, safe) @@ -680,249 +647,9 @@ by transfer qed -subsection {* Derivatives *} - -subsubsection {* Purely standard proofs *} - -lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/#h) -- 0 --> D)" -by (simp add: deriv_def) - -lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/#h) -- 0 --> D" -by (simp add: deriv_def) - -lemma DERIV_const [simp]: "DERIV (\x. k) x :> 0" -by (simp add: deriv_def) - -lemma DERIV_Id [simp]: "DERIV (\x. x) x :> 1" -by (simp add: deriv_def real_scaleR_def cong: LIM_cong) - -lemma add_diff_add: - fixes a b c d :: "'a::ab_group_add" - shows "(a + c) - (b + d) = (a - b) + (c - d)" -by simp - -lemma DERIV_add: - "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + g x) x :> D + E" -by (simp only: deriv_def add_diff_add scaleR_right_distrib LIM_add) - -lemma DERIV_minus: - "DERIV f x :> D \ DERIV (\x. - f x) x :> - D" -by (simp only: deriv_def minus_diff_minus scaleR_minus_right LIM_minus) - -lemma DERIV_diff: - "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x - g x) x :> D - E" -by (simp only: diff_def DERIV_add DERIV_minus) - -lemma DERIV_add_minus: - "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + - g x) x :> D + - E" -by (simp only: DERIV_add DERIV_minus) - -lemma DERIV_isCont: "DERIV f x :> D \ isCont f x" -proof (unfold isCont_iff) - assume "DERIV f x :> D" - hence "(\h. (f(x+h) - f(x)) /# h) -- 0 --> D" - by (rule DERIV_D) - hence "(\h. h *# ((f(x+h) - f(x)) /# h)) -- 0 --> 0 *# D" - by (intro LIM_scaleR LIM_self) - hence "(\h. (f(x+h) - f(x))) -- 0 --> 0" - by (simp cong: LIM_cong) - thus "(\h. f(x+h)) -- 0 --> f(x)" - by (simp add: LIM_def) -qed - -lemma DERIV_mult_lemma: - fixes a b c d :: "'a::real_algebra" - shows "(a * b - c * d) /# h = a * ((b - d) /# h) + ((a - c) /# h) * d" -by (simp add: diff_minus scaleR_right_distrib [symmetric] ring_distrib) - -lemma DERIV_mult': - fixes f g :: "real \ 'a::real_normed_algebra" - assumes f: "DERIV f x :> D" - assumes g: "DERIV g x :> E" - shows "DERIV (\x. f x * g x) x :> f x * E + D * g x" -proof (unfold deriv_def) - from f have "isCont f x" - by (rule DERIV_isCont) - hence "(\h. f(x+h)) -- 0 --> f x" - by (simp only: isCont_iff) - hence "(\h. f(x+h) * ((g(x+h) - g x) /# h) + - ((f(x+h) - f x) /# h) * g x) - -- 0 --> f x * E + D * g x" - by (intro LIM_add LIM_mult2 LIM_const DERIV_D f g) - thus "(\h. (f(x+h) * g(x+h) - f x * g x) /# h) - -- 0 --> f x * E + D * g x" - by (simp only: DERIV_mult_lemma) -qed - -lemma DERIV_mult: - fixes f g :: "real \ 'a::{real_normed_algebra,comm_ring}" shows - "[| DERIV f x :> Da; DERIV g x :> Db |] - ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" -by (drule (1) DERIV_mult', simp only: mult_commute add_commute) - -lemma DERIV_unique: - "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E" -apply (simp add: deriv_def) -apply (blast intro: LIM_unique) -done - -text{*Differentiation of finite sum*} - -lemma DERIV_sumr [rule_format (no_asm)]: - "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) - --> DERIV (%x. \n=m.. (\r=m.. D) = - ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)" -apply (rule iffI) -apply (drule_tac k="- a" in LIM_shift) -apply (simp add: diff_minus) -apply (drule_tac k="a" in LIM_shift) -apply (simp add: add_commute) -done - -lemma DERIV_LIM_iff': - "((%h::real. (f(a + h) - f(a)) /# h) -- 0 --> D) = - ((%x. (f(x)-f(a)) /# (x-a)) -- a --> D)" -apply (rule iffI) -apply (drule_tac k="- a" in LIM_shift) -apply (simp add: diff_minus) -apply (drule_tac k="a" in LIM_shift) -apply (simp add: add_commute) -done - -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: - "\(a::'a::division_ring) \ 0; b \ 0\ - \ 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: - "\a \ 0; b \ (0::'a::real_normed_div_algebra)\ - \ (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: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" - shows "g -- a --> l \ 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 \ 'a::real_normed_div_algebra" - assumes der: "DERIV f x :> D" - assumes neq: "f x \ 0" - shows "DERIV (\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: "\z. \z \ x; norm (z - x) < s\ - \ norm (f z - f x) < norm (f x)" - by fast - - show "(\z. (inverse (f z) - inverse (f x)) /# (z - x)) -- x --> ?E" - proof (rule LIM_equal2 [OF s]) - fix z :: real - assume "z \ x" "norm (z - x) < s" - hence "norm (f z - f x) < norm (f x)" by (rule less_fx) - hence "f z \ 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 "(\z. (f z - f x) /# (z - x)) -- x --> D" - by (unfold DERIV_iff2) - thus "(\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 "\DERIV f x :> D; DERIV g x :> E; g x \ 0\ - \ DERIV (\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 \ 'a::{real_normed_algebra,recpower}" - assumes f: "DERIV f x :> D" - shows "DERIV (\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 \ 'a::{real_normed_algebra,recpower}" - assumes f: "DERIV f x :> D" - shows "DERIV (\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 *) -(* ------------------------------------------------------------------------ *) - -lemma CARAT_DERIV: - "(DERIV f x :> l) = - (\g. (\z. f z - f x = (z-x) *# g z) & isCont g x & g x = l)" - (is "?lhs = ?rhs") -proof - assume der: "DERIV f x :> l" - show "\g. (\z. f z - f x = (z-x) *# g z) \ isCont g x \ g x = l" - proof (intro exI conjI) - let ?g = "(%z. if z = x then l else (f z - f x) /# (z-x))" - show "\z. f z - f x = (z-x) *# ?g z" by (simp) - show "isCont ?g x" using der - by (simp add: isCont_iff DERIV_iff diff_minus - cong: LIM_equal [rule_format]) - show "?g x = l" by simp - qed -next - assume "?rhs" - then obtain g where - "(\z. f z - f x = (z-x) *# g z)" and "isCont g x" and "g x = l" by blast - thus "(DERIV f x :> l)" - by (auto simp add: isCont_iff DERIV_iff diff_minus - cong: LIM_equal [rule_format]) -qed - lemma LIM_compose: + assumes g: "isCont g l" assumes f: "f -- a --> l" - assumes g: "isCont g l" shows "(\x. g (f x)) -- a --> g l" proof (rule LIM_I) fix r::real assume r: "0 < r" @@ -944,1510 +671,28 @@ qed qed -lemma DERIV_chain': - assumes f: "DERIV f x :> D" - assumes g: "DERIV g (f x) :> E" - shows "DERIV (\x. g (f x)) x :> D *# E" -proof (unfold DERIV_iff2) - obtain d where d: "\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 "(\z. d (f z)) -- x --> d (f x)" - using cont_d by (rule LIM_compose) - hence "(\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 "(\z. (g (f z) - g (f x)) /# (z - x)) -- x --> D *# E" - by (simp add: d dfx real_scaleR_def) -qed - - -subsubsection {* Nonstandard proofs *} - -lemma DERIV_NS_iff: - "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/#h) -- 0 --NS> D)" -by (simp add: deriv_def LIM_NSLIM_iff) - -lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/#h) -- 0 --NS> D" -by (simp add: deriv_def LIM_NSLIM_iff) - -lemma NSDeriv_unique: - "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E" -apply (simp add: nsderiv_def) -apply (cut_tac Infinitesimal_epsilon hypreal_epsilon_not_zero) -apply (auto dest!: bspec [where x=epsilon] - intro!: inj_hypreal_of_real [THEN injD] - dest: approx_trans3) -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 --NS> D)" -apply (simp add: nsderiv_def NSLIM_def, auto) -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 --NS> D)" -by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff diff_minus [symmetric] - LIM_NSLIM_iff [symmetric]) - -(* while we're at it! *) -lemma NSDERIV_iff2: - "(NSDERIV f x :> D) = - (\w. - w \ hypreal_of_real x & w \ hypreal_of_real x --> - ( *f* (%z. (f z - f x) / (z-x))) w \ hypreal_of_real D)" -by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) - -(*FIXME DELETE*) -lemma hypreal_not_eq_minus_iff: "(x \ a) = (x - a \ (0::hypreal))" -by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) - -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 (auto simp add: NSDERIV_iff2) -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 add: - 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 (auto simp add: nsderiv_def) -apply (case_tac "h = (0::hypreal) ") -apply (auto simp add: diff_minus) -apply (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: diff_minus) -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 (auto simp add: nsderiv_def) -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 diff_minus) -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 - hypreal_of_real x" in bspec) - prefer 2 apply (simp add: add_assoc [symmetric]) -apply (auto simp add: mem_infmal_iff [symmetric] add_commute) -apply (drule_tac c = "xa - hypreal_of_real x" in approx_mult1) -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: mult_assoc) -apply (drule_tac x3=D in - HFinite_hypreal_of_real [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)" -by (simp add: NSDERIV_NSLIM_iff) - -text{*Sum of functions- proved easily*} - -lemma NSDERIV_add: "[| 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 (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec) -apply (drule_tac b = "hypreal_of_real Da" and d = "hypreal_of_real Db" in approx_add) -apply (auto simp add: diff_def add_ac) -done - -text{*Product of functions - Proof is trivial but tedious - and long due to rearrangement of terms*} - -lemma lemma_nsderiv1: "((a::hypreal)*b) - (c*d) = (b*(a - c)) + (c*(b - d))" -by (simp add: right_diff_distrib) - -lemma lemma_nsderiv2: "[| (x - y) / z = hypreal_of_real D + yb; z \ 0; - z \ Infinitesimal; yb \ Infinitesimal |] - ==> x - y \ 0" -apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption) -apply (erule_tac V = "(x - y) / z = hypreal_of_real D + yb" in thin_rl) -apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add - simp add: mult_assoc mem_infmal_iff [symmetric]) -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 (simp (no_asm) add: add_divide_distrib diff_divide_distrib) -apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ -apply (auto simp add: times_divide_eq_right [symmetric] - simp del: times_divide_eq) -apply (drule_tac D = Db in lemma_nsderiv2, assumption+) -apply (drule_tac - approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) -apply (auto intro!: approx_add_mono1 - simp add: left_distrib right_distrib mult_commute add_assoc) -apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)" - in add_commute [THEN subst]) -apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] - Infinitesimal_add Infinitesimal_mult - Infinitesimal_hypreal_of_real_mult - Infinitesimal_hypreal_of_real_mult2 - simp add: add_assoc [symmetric]) -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" -proof (simp add: NSDERIV_NSLIM_iff) - assume "(\h. (f (x + h) - f x) / h) -- 0 --NS> D" - hence deriv: "(\h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D" - by (rule NSLIM_minus) - have "\h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h" - by (simp add: minus_divide_left) - with deriv - show "(\h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp -qed - -text{*Subtraction*} -lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db" -by (blast dest: NSDERIV_add NSDERIV_minus) - -lemma NSDERIV_diff: - "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] - ==> NSDERIV (%x. f x - g x) x :> Da-Db" -apply (simp add: diff_minus) -apply (blast intro: NSDERIV_add_minus) -done - -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.*} - - -(* lemmas *) -lemma NSDERIV_zero: - "[| NSDERIV g x :> D; - ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x); - xa \ Infinitesimal; - xa \ 0 - |] ==> D = 0" -apply (simp add: nsderiv_def) -apply (drule bspec, auto) -done - -(* can be proved differently using NSLIM_isCont_iff *) -lemma NSDERIV_approx: - "[| NSDERIV f x :> D; h \ Infinitesimal; h \ 0 |] - ==> ( *f* f) (hypreal_of_real(x) + h) - hypreal_of_real(f x) \ 0" -apply (simp add: nsderiv_def) -apply (simp add: mem_infmal_iff [symmetric]) -apply (rule Infinitesimal_ratio) -apply (rule_tac [3] approx_hypreal_of_real_HFinite, auto) -done - -(*--------------------------------------------------------------- - from one version of differentiability - - f(x) - f(a) - --------------- \ Db - x - a - ---------------------------------------------------------------*) -lemma NSDERIVD1: "[| NSDERIV f (g x) :> Da; - ( *f* g) (hypreal_of_real(x) + xa) \ hypreal_of_real (g x); - ( *f* g) (hypreal_of_real(x) + xa) \ hypreal_of_real (g x) - |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) - - hypreal_of_real (f (g x))) - / (( *f* g) (hypreal_of_real(x) + xa) - hypreal_of_real (g x)) - \ hypreal_of_real(Da)" -by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric]) - -(*-------------------------------------------------------------- - from other version of differentiability - - f(x + h) - f(x) - ----------------- \ Db - h - --------------------------------------------------------------*) -lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \ Infinitesimal; xa \ 0 |] - ==> (( *f* g) (hypreal_of_real(x) + xa) - hypreal_of_real(g x)) / xa - \ hypreal_of_real(Db)" -by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) - -lemma lemma_chain: "(z::hypreal) \ 0 ==> x*y = (x*inverse(z))*(z*y)" -by auto - -text{*This proof uses both definitions of differentiability.*} -lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |] - ==> NSDERIV (f o 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) (hypreal_of_real (x) + xa) = hypreal_of_real (g x) ") -apply (drule_tac g = g in NSDERIV_zero) -apply (auto simp add: divide_inverse) -apply (rule_tac z1 = "( *f* g) (hypreal_of_real (x) + xa) - hypreal_of_real (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst]) -apply (erule hypreal_not_eq_minus_iff [THEN iffD1]) -apply (rule approx_mult_hypreal_of_real) -apply (simp_all add: divide_inverse [symmetric]) -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 divide_self del: divide_self_if) - -lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c" -by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp) - -(*Can't get rid of x \ 0 because it isn't continuous at zero*) -lemma NSDERIV_inverse: - "x \ 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))" -apply (simp add: nsderiv_def) -apply (rule ballI, simp, clarify) -apply (frule (1) Infinitesimal_add_not_zero) -apply (simp add: add_commute) -(*apply (auto simp add: starfun_inverse_inverse realpow_two - simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*) -apply (simp add: inverse_add inverse_mult_distrib [symmetric] - inverse_minus_eq [symmetric] add_ac mult_ac diff_def - del: inverse_mult_distrib inverse_minus_eq - minus_mult_left [symmetric] minus_mult_right [symmetric]) -apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib - del: minus_mult_left [symmetric] minus_mult_right [symmetric]) -apply (rule_tac y = "inverse (- hypreal_of_real x * hypreal_of_real x)" in approx_trans) -apply (rule inverse_add_Infinitesimal_approx2) -apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal - simp add: inverse_minus_eq [symmetric] HFinite_minus_iff) -apply (rule Infinitesimal_HFinite_mult2, auto) -done - -subsubsection {* Equivalence of NS and Standard definitions *} - -lemma divideR_eq_divide [simp]: "x /# y = x / y" -by (simp add: real_scaleR_def divide_inverse mult_commute) - -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) - -(* let's do the standard proof though theorem *) -(* LIM_mult2 follows from a NS proof *) - -lemma DERIV_cmult: - fixes f :: "real \ '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 (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) - -(*derivative of linear multiplication*) -lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" -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 (cut_tac DERIV_power [OF DERIV_Id]) -apply (simp add: real_scaleR_def real_of_nat_def) -done - -(* NS version *) -lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" -by (simp add: NSDERIV_DERIV_iff DERIV_pow) - -text{*Power of -1*} - -lemma DERIV_inverse: "x \ 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))" -by (drule DERIV_inverse' [OF DERIV_Id], simp) - -text{*Derivative of inverse*} -lemma DERIV_inverse_fun: "[| DERIV f x :> d; f(x) \ 0 |] - ==> DERIV (%x. inverse(f x)::real) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" -by (drule (1) DERIV_inverse', simp add: mult_ac) - -lemma NSDERIV_inverse_fun: "[| NSDERIV f x :> d; f(x) \ 0 |] - ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" -by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc) - -text{*Derivative of quotient*} -lemma DERIV_quotient: "[| DERIV f x :> d; DERIV g x :> e; g(x) \ 0 |] - ==> DERIV (%y. f(y) / (g y) :: real) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" -by (drule (2) DERIV_divide, simp add: mult_commute) - -lemma NSDERIV_quotient: "[| NSDERIV f x :> d; DERIV 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: realpow_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 - real_scaleR_def mult_commute) - -lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::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 \ hypreal_of_real x \ w \ hypreal_of_real x \ - ( *f* g) w * (w - hypreal_of_real x) / (w - hypreal_of_real x) \ - hypreal_of_real (g x)" - by (simp add: diff_minus isNSCont_def) - thus ?thesis using all - by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) -qed - -subsubsection {* Differentiability predicate *} - -lemma differentiableD: "f differentiable x ==> \D. DERIV f x :> D" -by (simp add: differentiable_def) - -lemma differentiableI: "DERIV f x :> D ==> f differentiable x" -by (force simp add: differentiable_def) - -lemma NSdifferentiableD: "f NSdifferentiable x ==> \D. NSDERIV f x :> D" -by (simp add: NSdifferentiable_def) - -lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x" -by (force simp add: NSdifferentiable_def) - -lemma differentiable_const: "(\z. a) differentiable x" - apply (unfold differentiable_def) - apply (rule_tac x=0 in exI) - apply simp - done - -lemma differentiable_sum: - assumes "f differentiable x" - and "g differentiable x" - shows "(\x. f x + g x) differentiable x" -proof - - from prems have "\D. DERIV f x :> D" by (unfold differentiable_def) - then obtain df where "DERIV f x :> df" .. - moreover from prems have "\D. DERIV g x :> D" by (unfold differentiable_def) - then obtain dg where "DERIV g x :> dg" .. - ultimately have "DERIV (\x. f x + g x) x :> df + dg" by (rule DERIV_add) - hence "\D. DERIV (\x. f x + g x) x :> D" by auto - thus ?thesis by (fold differentiable_def) -qed - -lemma differentiable_diff: - assumes "f differentiable x" - and "g differentiable x" - shows "(\x. f x - g x) differentiable x" -proof - - from prems have "f differentiable x" by simp - moreover - from prems have "\D. DERIV g x :> D" by (unfold differentiable_def) - then obtain dg where "DERIV g x :> dg" .. - then have "DERIV (\x. - g x) x :> -dg" by (rule DERIV_minus) - hence "\D. DERIV (\x. - g x) x :> D" by auto - hence "(\x. - g x) differentiable x" by (fold differentiable_def) - ultimately - show ?thesis - by (auto simp: real_diff_def dest: differentiable_sum) -qed - -lemma differentiable_mult: - assumes "f differentiable x" - and "g differentiable x" - shows "(\x. f x * g x) differentiable x" -proof - - from prems have "\D. DERIV f x :> D" by (unfold differentiable_def) - then obtain df where "DERIV f x :> df" .. - moreover from prems have "\D. DERIV g x :> D" by (unfold differentiable_def) - then obtain dg where "DERIV g x :> dg" .. - ultimately have "DERIV (\x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult) - hence "\D. DERIV (\x. f x * g x) x :> D" by auto - thus ?thesis by (fold differentiable_def) -qed - -subsection {*(NS) Increment*} -lemma incrementI: - "f NSdifferentiable x ==> - increment f x h = ( *f* f) (hypreal_of_real(x) + h) - - hypreal_of_real (f x)" -by (simp add: increment_def) - -lemma incrementI2: "NSDERIV f x :> D ==> - increment f x h = ( *f* f) (hypreal_of_real(x) + h) - - hypreal_of_real (f x)" -apply (erule NSdifferentiableI [THEN incrementI]) -done - -(* 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 hypreal_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 -apply (simp add: times_divide_eq_right [symmetric]) -apply (auto simp add: left_distrib) -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, - auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric]) -apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) -done - -subsection {* Nested Intervals and Bisection *} - -text{*Lemmas about nested intervals and proof by bisection (cf.Harrison). - All considerably tidied by lcp.*} - -lemma lemma_f_mono_add [rule_format (no_asm)]: "(\n. (f::nat=>real) n \ f (Suc n)) --> f m \ f(m + no)" -apply (induct "no") -apply (auto intro: order_trans) -done - -lemma f_inc_g_dec_Beq_f: "[| \n. f(n) \ f(Suc n); - \n. g(Suc n) \ g(n); - \n. f(n) \ g(n) |] - ==> Bseq (f :: nat \ real)" -apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI) -apply (induct_tac "n") -apply (auto intro: order_trans) -apply (rule_tac y = "g (Suc na)" in order_trans) -apply (induct_tac [2] "na") -apply (auto intro: order_trans) -done - -lemma f_inc_g_dec_Beq_g: "[| \n. f(n) \ f(Suc n); - \n. g(Suc n) \ g(n); - \n. f(n) \ g(n) |] - ==> Bseq (g :: nat \ real)" -apply (subst Bseq_minus_iff [symmetric]) -apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f) -apply auto -done - -lemma f_inc_imp_le_lim: - fixes f :: "nat \ real" - shows "\\n. f n \ f (Suc n); convergent f\ \ f n \ lim f" -apply (rule linorder_not_less [THEN iffD1]) -apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc) -apply (drule real_less_sum_gt_zero) -apply (drule_tac x = "f n + - lim f" in spec, safe) -apply (drule_tac P = "%na. no\na --> ?Q na" and x = "no + n" in spec, auto) -apply (subgoal_tac "lim f \ f (no + n) ") -apply (drule_tac no=no and m=n in lemma_f_mono_add) -apply (auto simp add: add_commute) -apply (induct_tac "no") -apply simp -apply (auto intro: order_trans simp add: diff_minus abs_if) -done - -lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)" -apply (rule LIMSEQ_minus [THEN limI]) -apply (simp add: convergent_LIMSEQ_iff) -done - -lemma g_dec_imp_lim_le: - fixes g :: "nat \ real" - shows "\\n. g (Suc n) \ g(n); convergent g\ \ lim g \ g n" -apply (subgoal_tac "- (g n) \ - (lim g) ") -apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim) -apply (auto simp add: lim_uminus convergent_minus_iff [symmetric]) -done - -lemma lemma_nest: "[| \n. f(n) \ f(Suc n); - \n. g(Suc n) \ g(n); - \n. f(n) \ g(n) |] - ==> \l m :: real. l \ m & ((\n. f(n) \ l) & f ----> l) & - ((\n. m \ g(n)) & g ----> m)" -apply (subgoal_tac "monoseq f & monoseq g") -prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc) -apply (subgoal_tac "Bseq f & Bseq g") -prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g) -apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff) -apply (rule_tac x = "lim f" in exI) -apply (rule_tac x = "lim g" in exI) -apply (auto intro: LIMSEQ_le) -apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff) -done - -lemma lemma_nest_unique: "[| \n. f(n) \ f(Suc n); - \n. g(Suc n) \ g(n); - \n. f(n) \ g(n); - (%n. f(n) - g(n)) ----> 0 |] - ==> \l::real. ((\n. f(n) \ l) & f ----> l) & - ((\n. l \ g(n)) & g ----> l)" -apply (drule lemma_nest, auto) -apply (subgoal_tac "l = m") -apply (drule_tac [2] X = f in LIMSEQ_diff) -apply (auto intro: LIMSEQ_unique) -done - -text{*The universal quantifiers below are required for the declaration - of @{text Bolzano_nest_unique} below.*} - -lemma Bolzano_bisect_le: - "a \ b ==> \n. fst (Bolzano_bisect P a b n) \ snd (Bolzano_bisect P a b n)" -apply (rule allI) -apply (induct_tac "n") -apply (auto simp add: Let_def split_def) -done - -lemma Bolzano_bisect_fst_le_Suc: "a \ b ==> - \n. fst(Bolzano_bisect P a b n) \ fst (Bolzano_bisect P a b (Suc n))" -apply (rule allI) -apply (induct_tac "n") -apply (auto simp add: Bolzano_bisect_le Let_def split_def) -done - -lemma Bolzano_bisect_Suc_le_snd: "a \ b ==> - \n. snd(Bolzano_bisect P a b (Suc n)) \ snd (Bolzano_bisect P a b n)" -apply (rule allI) -apply (induct_tac "n") -apply (auto simp add: Bolzano_bisect_le Let_def split_def) -done - -lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" -apply (auto) -apply (drule_tac f = "%u. (1/2) *u" in arg_cong) -apply (simp) -done - -lemma Bolzano_bisect_diff: - "a \ b ==> - snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = - (b-a) / (2 ^ n)" -apply (induct "n") -apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def) -done - -lemmas Bolzano_nest_unique = - lemma_nest_unique - [OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le] - - -lemma not_P_Bolzano_bisect: - assumes P: "!!a b c. [| P(a,b); P(b,c); a \ b; b \ c|] ==> P(a,c)" - and notP: "~ P(a,b)" - and le: "a \ b" - shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))" -proof (induct n) - case 0 thus ?case by simp - next - case (Suc n) - thus ?case - by (auto simp del: surjective_pairing [symmetric] - simp add: Let_def split_def Bolzano_bisect_le [OF le] - P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"]) -qed - -(*Now we re-package P_prem as a formula*) -lemma not_P_Bolzano_bisect': - "[| \a b c. P(a,b) & P(b,c) & a \ b & b \ c --> P(a,c); - ~ P(a,b); a \ b |] ==> - \n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))" -by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE]) - - - -lemma lemma_BOLZANO: - "[| \a b c. P(a,b) & P(b,c) & a \ b & b \ c --> P(a,c); - \x. \d::real. 0 < d & - (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)); - a \ b |] - ==> P(a,b)" -apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+) -apply (rule LIMSEQ_minus_cancel) -apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero) -apply (rule ccontr) -apply (drule not_P_Bolzano_bisect', assumption+) -apply (rename_tac "l") -apply (drule_tac x = l in spec, clarify) -apply (simp add: LIMSEQ_def) -apply (drule_tac P = "%r. 0 ?Q r" and x = "d/2" in spec) -apply (drule_tac P = "%r. 0 ?Q r" and x = "d/2" in spec) -apply (drule real_less_half_sum, auto) -apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec) -apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec) -apply safe -apply (simp_all (no_asm_simp)) -apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l)" in order_le_less_trans) -apply (simp (no_asm_simp) add: abs_if) -apply (rule real_sum_of_halves [THEN subst]) -apply (rule add_strict_mono) -apply (simp_all add: diff_minus [symmetric]) -done - - -lemma lemma_BOLZANO2: "((\a b c. (a \ b & b \ c & P(a,b) & P(b,c)) --> P(a,c)) & - (\x. \d::real. 0 < d & - (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)))) - --> (\a b. a \ b --> P(a,b))" -apply clarify -apply (blast intro: lemma_BOLZANO) -done - - -subsection {* Intermediate Value Theorem *} - -text {*Prove Contrapositive by Bisection*} - -lemma IVT: "[| f(a::real) \ (y::real); y \ f(b); - a \ b; - (\x. a \ x & x \ b --> isCont f x) |] - ==> \x. a \ x & x \ b & f(x) = y" -apply (rule contrapos_pp, assumption) -apply (cut_tac P = "% (u,v) . a \ u & u \ v & v \ b --> ~ (f (u) \ y & y \ f (v))" in lemma_BOLZANO2) -apply safe -apply simp_all -apply (simp add: isCont_iff LIM_def) -apply (rule ccontr) -apply (subgoal_tac "a \ x & x \ b") - prefer 2 - apply simp - apply (drule_tac P = "%d. 0 ?P d" and x = 1 in spec, arith) -apply (drule_tac x = x in spec)+ -apply simp -apply (drule_tac P = "%r. ?P r --> (\s>0. ?Q r s) " and x = "\y - f x\" in spec) -apply safe -apply simp -apply (drule_tac x = s in spec, clarify) -apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe) -apply (drule_tac x = "ba-x" in spec) -apply (simp_all add: abs_if) -apply (drule_tac x = "aa-x" in spec) -apply (case_tac "x \ aa", simp_all) -done - -lemma IVT2: "[| f(b::real) \ (y::real); y \ f(a); - a \ b; - (\x. a \ x & x \ b --> isCont f x) - |] ==> \x. a \ x & x \ b & f(x) = y" -apply (subgoal_tac "- f a \ -y & -y \ - f b", clarify) -apply (drule IVT [where f = "%x. - f x"], assumption) -apply (auto intro: isCont_minus) -done - -(*HOL style here: object-level formulations*) -lemma IVT_objl: "(f(a::real) \ (y::real) & y \ f(b) & a \ b & - (\x. a \ x & x \ b --> isCont f x)) - --> (\x. a \ x & x \ b & f(x) = y)" -apply (blast intro: IVT) -done - -lemma IVT2_objl: "(f(b::real) \ (y::real) & y \ f(a) & a \ b & - (\x. a \ x & x \ b --> isCont f x)) - --> (\x. a \ x & x \ b & f(x) = y)" -apply (blast intro: IVT2) -done - -text{*By bisection, function continuous on closed interval is bounded above*} - -lemma isCont_bounded: - "[| a \ b; \x. a \ x & x \ b --> isCont f x |] - ==> \M::real. \x::real. a \ x & x \ b --> f(x) \ M" -apply (cut_tac P = "% (u,v) . a \ u & u \ v & v \ b --> (\M. \x. u \ x & x \ v --> f x \ M)" in lemma_BOLZANO2) -apply safe -apply simp_all -apply (rename_tac x xa ya M Ma) -apply (cut_tac x = M and y = Ma in linorder_linear, safe) -apply (rule_tac x = Ma in exI, clarify) -apply (cut_tac x = xb and y = xa in linorder_linear, force) -apply (rule_tac x = M in exI, clarify) -apply (cut_tac x = xb and y = xa in linorder_linear, force) -apply (case_tac "a \ x & x \ b") -apply (rule_tac [2] x = 1 in exI) -prefer 2 apply force -apply (simp add: LIM_def isCont_iff) -apply (drule_tac x = x in spec, auto) -apply (erule_tac V = "\M. \x. a \ x & x \ b & ~ f x \ M" in thin_rl) -apply (drule_tac x = 1 in spec, auto) -apply (rule_tac x = s in exI, clarify) -apply (rule_tac x = "\f x\ + 1" in exI, clarify) -apply (drule_tac x = "xa-x" in spec) -apply (auto simp add: abs_ge_self) -done - -text{*Refine the above to existence of least upper bound*} - -lemma lemma_reals_complete: "((\x. x \ S) & (\y. isUb UNIV S (y::real))) --> - (\t. isLub UNIV S t)" -by (blast intro: reals_complete) - -lemma isCont_has_Ub: "[| a \ b; \x. a \ x & x \ b --> isCont f x |] - ==> \M::real. (\x::real. a \ x & x \ b --> f(x) \ M) & - (\N. N < M --> (\x. a \ x & x \ b & N < f(x)))" -apply (cut_tac S = "Collect (%y. \x. a \ x & x \ b & y = f x)" - in lemma_reals_complete) -apply auto -apply (drule isCont_bounded, assumption) -apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def) -apply (rule exI, auto) -apply (auto dest!: spec simp add: linorder_not_less) -done - -text{*Now show that it attains its upper bound*} - -lemma isCont_eq_Ub: - assumes le: "a \ b" - and con: "\x::real. a \ x & x \ b --> isCont f x" - shows "\M::real. (\x. a \ x & x \ b --> f(x) \ M) & - (\x. a \ x & x \ b & f(x) = M)" -proof - - from isCont_has_Ub [OF le con] - obtain M where M1: "\x. a \ x \ x \ b \ f x \