# HG changeset patch # User kleing # Date 1139743741 -3600 # Node ID 5652a536b7e8f2c78e617208b5f8c57b5250c360 # Parent 0e6ec4fd204c6b3c8f0bafa6776fe489c778a906 * include generalised MVT in HyperReal (contributed by Benjamin Porter) * add non-denumerability of continuum in Real, includes closed intervals on real (contributed by Benjamin Porter, #22 in http://www.cs.ru.nl/~freek/100/) diff -r 0e6ec4fd204c -r 5652a536b7e8 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sun Feb 12 10:42:19 2006 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Sun Feb 12 12:29:01 2006 +0100 @@ -3,6 +3,7 @@ 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*} @@ -15,16 +16,16 @@ constdefs LIM :: "[real=>real,real,real] => bool" - ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) + ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) "f -- a --> L == \r > 0. \s > 0. \x. x \ a & \x + -a\ < s - --> \f x + -L\ < r" + --> \f x + -L\ < r" NSLIM :: "[real=>real,real,real] => bool" - ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) + ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) "f -- a --NS> L == (\x. (x \ hypreal_of_real a & - x @= hypreal_of_real a --> - ( *f* f) x @= hypreal_of_real L))" + x @= hypreal_of_real a --> + ( *f* f) x @= hypreal_of_real L))" isCont :: "[real=>real,real] => bool" "isCont f a == (f -- a --> (f a))" @@ -32,29 +33,29 @@ isNSCont :: "[real=>real,real] => bool" --{*NS definition dispenses with limit notions*} "isNSCont f a == (\y. y @= hypreal_of_real a --> - ( *f* f) y @= hypreal_of_real (f a))" + ( *f* f) y @= hypreal_of_real (f a))" deriv:: "[real=>real,real,real] => bool" --{*Differentiation: D is derivative of function f at x*} - ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) + ("(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 (_)/ (_)/ :> (_))" [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)" + (( *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" + 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))" + inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))" isUCont :: "(real=>real) => bool" "isUCont f == \r > 0. \s > 0. \x y. \x + -y\ < s --> \f x + -f y\ < r" @@ -133,7 +134,7 @@ lemma LIM_diff: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m" -by (simp add: diff_minus LIM_add_minus) +by (simp add: diff_minus LIM_add_minus) lemma LIM_const_not_eq: "k \ L ==> ~ ((%x. k) -- a --> L)" @@ -146,7 +147,7 @@ assume s: "0 a < s/2 + a" by arith next - from s show "\s / 2 + a - a\ < s" by (simp add: abs_if) + from s show "\s / 2 + a - a\ < s" by (simp add: abs_if) next from s show "~ \k-L\ < L-k" by (simp add: abs_if) } qed @@ -159,7 +160,7 @@ assume s: "0 a < s/2 + a" by arith next - from s show "\s / 2 + a - a\ < s" by (simp add: abs_if) + from s show "\s / 2 + a - a\ < s" by (simp add: abs_if) next from s show "~ \k-L\ < k-L" by (simp add: abs_if) } qed @@ -167,11 +168,11 @@ lemma LIM_const_eq: "(%x. k) -- x --> L ==> k = L" apply (rule ccontr) -apply (blast dest: LIM_const_not_eq) +apply (blast dest: LIM_const_not_eq) done lemma LIM_unique: "[| f -- a --> L; f -- a --> M |] ==> L = M" -apply (drule LIM_diff, assumption) +apply (drule LIM_diff, assumption) apply (auto dest!: LIM_const_eq) done @@ -198,7 +199,7 @@ assume "x \ a \ \x-a\ < min fs gs" with fs_lt gs_lt have "\f x\ < 1" and "\g x\ < r" by (auto simp add: fs_lt) - hence "\f x\ * \g x\ < 1*r" by (rule abs_mult_less) + hence "\f x\ * \g x\ < 1*r" by (rule abs_mult_less) thus "\f x\ * \g x\ < r" by simp qed qed @@ -228,7 +229,7 @@ apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe) apply (rule_tac x = xa in star_cases) apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff) -apply (rule bexI [OF _ Rep_star_star_n], clarify) +apply (rule bexI [OF _ Rep_star_star_n], clarify) apply (drule_tac x = u in spec, clarify) apply (drule_tac x = s in spec, clarify) apply (subgoal_tac "\n::nat. (Xa n) \ x & \(Xa n) + - x\ < s --> \f (Xa n) + - L\ < u") @@ -594,7 +595,7 @@ lemma lemma_LIMu: "\s>0.\z y. \z + - y\ < s & r \ \f z + -f y\ ==> \n::nat. \z y. \z + -y\ < inverse(real(Suc n)) & r \ \f z + -f y\" apply clarify -apply (cut_tac n1 = n +apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) done @@ -772,8 +773,8 @@ 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: diff_minus - approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] - Infinitesimal_subset_HFinite [THEN subsetD]) + approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] + Infinitesimal_subset_HFinite [THEN subsetD]) done lemma NSDERIVD4: @@ -881,7 +882,7 @@ ==> 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) + simp add: starfun_lambda_cancel lemma_nsderiv1) apply (simp (no_asm) add: add_divide_distrib) apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ apply (auto simp add: times_divide_eq_right [symmetric] @@ -1330,7 +1331,7 @@ 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)" +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) @@ -1498,7 +1499,7 @@ lemma isCont_has_Ub: "[| a \ b; \x. a \ x & x \ b --> isCont f x |] ==> \M. (\x. 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)" +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) @@ -1601,12 +1602,12 @@ assume "0 < h" "h < s" with all [of h] show "f x < f (x+h)" proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] - split add: split_if_asm) + split add: split_if_asm) assume "~ (f (x+h) - f x) / h < l" and h: "0 < h" with l have "0 < (f (x+h) - f x) / h" by arith thus "f x < f (x+h)" - by (simp add: pos_less_divide_eq h) + by (simp add: pos_less_divide_eq h) qed qed qed @@ -1630,12 +1631,12 @@ assume "0 < h" "h < s" with all [of "-h"] show "f x < f (x-h)" proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] - split add: split_if_asm) + split add: split_if_asm) assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" with l have "0 < (f (x-h) - f x) / h" by arith thus "f x < f (x-h)" - by (simp add: pos_less_divide_eq h) + by (simp add: pos_less_divide_eq h) qed qed qed @@ -1742,9 +1743,9 @@ hence ax': "ay. \x'-y\ < d \ a \ y \ y \ b" - by blast + by blast hence bound': "\y. \x'-y\ < d \ f x' \ f y" using x'_min - by blast + by blast from differentiableD [OF dif [OF ax'b]] obtain l where der: "DERIV f x' :> l" .. have "l=0" by (rule DERIV_local_min [OF der d bound']) @@ -1759,7 +1760,7 @@ obtain r where ar: "a < r" and rb: "r < b" by blast from lemma_interval [OF ar rb] obtain d where d: "0y. \r-y\ < d \ a \ y \ y \ b" - by blast + by blast have eq_fb: "\z. a \ z --> z \ b --> f z = f b" proof (clarify) fix z::real @@ -1798,7 +1799,7 @@ hence ba: "b-a \ 0" by arith show ?thesis by (rule real_mult_left_cancel [OF ba, THEN iffD1], - simp add: right_diff_distrib, + simp add: right_diff_distrib, simp add: left_diff_distrib) qed @@ -1888,10 +1889,10 @@ done lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)" -by (simp) +by (simp) lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)" -by (simp) +by (simp) text{*Gallileo's "trick": average velocity = av. of end velocities*} @@ -2060,6 +2061,319 @@ qed qed + +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 + + +theorem GMVT: + assumes alb: "a < b" + and fc: "\x. a \ x \ x \ b \ isCont f x" + and fd: "\x. a < x \ x < b \ f differentiable x" + and gc: "\x. a \ x \ x \ b \ isCont g x" + and gd: "\x. a < x \ x < b \ g differentiable x" + shows "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ a < c \ c < b \ ((f b - f a) * g'c) = ((g b - g a) * f'c)" +proof - + let ?h = "\x. (f b - f a)*(g x) - (g b - g a)*(f x)" + from prems have "a < b" by simp + moreover have "\x. a \ x \ x \ b \ isCont ?h x" + proof - + have "\x. a <= x \ x <= b \ isCont (\x. f b - f a) x" by simp + with gc have "\x. a <= x \ x <= b \ isCont (\x. (f b - f a) * g x) x" + by (auto intro: isCont_mult) + moreover + have "\x. a <= x \ x <= b \ isCont (\x. g b - g a) x" by simp + with fc have "\x. a <= x \ x <= b \ isCont (\x. (g b - g a) * f x) x" + by (auto intro: isCont_mult) + ultimately show ?thesis + by (fastsimp intro: isCont_diff) + qed + moreover + have "\x. a < x \ x < b \ ?h differentiable x" + proof - + have "\x. a < x \ x < b \ (\x. f b - f a) differentiable x" by (simp add: differentiable_const) + with gd have "\x. a < x \ x < b \ (\x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult) + moreover + have "\x. a < x \ x < b \ (\x. g b - g a) differentiable x" by (simp add: differentiable_const) + with fd have "\x. a < x \ x < b \ (\x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult) + ultimately show ?thesis by (simp add: differentiable_diff) + qed + ultimately have "\l z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" by (rule MVT) + then obtain l where ldef: "\z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" .. + then obtain c where cdef: "a < c \ c < b \ DERIV ?h c :> l \ ?h b - ?h a = (b - a) * l" .. + + from cdef have cint: "a < c \ c < b" by auto + with gd have "g differentiable c" by simp + hence "\D. DERIV g c :> D" by (rule differentiableD) + then obtain g'c where g'cdef: "DERIV g c :> g'c" .. + + from cdef have "a < c \ c < b" by auto + with fd have "f differentiable c" by simp + hence "\D. DERIV f c :> D" by (rule differentiableD) + then obtain f'c where f'cdef: "DERIV f c :> f'c" .. + + from cdef have "DERIV ?h c :> l" by auto + moreover + { + from g'cdef have "DERIV (\x. (f b - f a) * g x) c :> g'c * (f b - f a)" + apply (insert DERIV_const [where k="f b - f a"]) + apply (drule meta_spec [of _ c]) + apply (drule DERIV_mult [where f="(\x. f b - f a)" and g=g]) + by simp_all + moreover from f'cdef have "DERIV (\x. (g b - g a) * f x) c :> f'c * (g b - g a)" + apply (insert DERIV_const [where k="g b - g a"]) + apply (drule meta_spec [of _ c]) + apply (drule DERIV_mult [where f="(\x. g b - g a)" and g=f]) + by simp_all + ultimately have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" + by (simp add: DERIV_diff) + } + ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) + + { + from cdef have "?h b - ?h a = (b - a) * l" by auto + also with leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp + finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp + } + moreover + { + have "?h b - ?h a = + ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - + ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" + by (simp add: mult_ac add_ac real_diff_mult_distrib) + hence "?h b - ?h a = 0" by auto + } + ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto + with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp + hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp + hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac) + + with g'cdef f'cdef cint show ?thesis by auto +qed + + +lemma LIMSEQ_SEQ_conv1: + assumes "X -- a --> L" + shows "\S. (\n. S n \ a) \ S ----> a \ (\n. X (S n)) ----> L" +proof - + { + from prems have Xdef: "\r > 0. \s > 0. \x. x \ a & \x + -a\ < s --> \X x + -L\ < r" by (unfold LIM_def) + + fix S + assume as: "(\n. S n \ a) \ S ----> a" + then have "S ----> a" by auto + then have Sdef: "(\r. 0 < r --> (\no. \n. no \ n --> \S n + -a\ < r))" by (unfold LIMSEQ_def) + { + fix r + from Xdef have Xdef2: "0 < r --> (\s > 0. \x. x \ a \ \x + -a\ < s --> \X x + -L\ < r)" by simp + { + assume rgz: "0 < r" + + from Xdef2 rgz have "\s > 0. \x. x \ a \ \x + -a\ < s --> \X x + -L\ < r" by simp + then obtain s where sdef: "s > 0 \ (\x. x\a \ \x + -a\ < s \ \X x + -L\ < r)" by auto + then have aux: "\x. x\a \ \x + -a\ < s \ \X x + -L\ < r" by auto + { + fix n + from aux have "S n \ a \ \S n + -a\ < s \ \X (S n) + -L\ < r" by simp + with as have imp2: "\S n + -a\ < s --> \X (S n) + -L\ < r" by auto + } + hence "\n. \S n + -a\ < s --> \X (S n) + -L\ < r" .. + moreover + from Sdef sdef have imp1: "\no. \n. no \ n --> \S n + -a\ < s" by auto + then obtain no where "\n. no \ n --> \S n + -a\ < s" by auto + ultimately have "\n. no \ n \ \X (S n) + -L\ < r" by simp + hence "\no. \n. no \ n \ \X (S n) + -L\ < r" by auto + } + } + hence "(\r. 0 < r --> (\no. \n. no \ n --> \X (S n) + -L\ < r))" by simp + hence "(\n. X (S n)) ----> L" by (fold LIMSEQ_def) + } + thus ?thesis by simp +qed + +lemma LIMSEQ_SEQ_conv2: + assumes "\S. (\n. S n \ a) \ S ----> a \ (\n. X (S n)) ----> L" + shows "X -- a --> L" +proof (rule ccontr) + assume "\ (X -- a --> L)" + hence "\ (\r > 0. \s > 0. \x. x \ a & \x + -a\ < s --> \X x + -L\ < r)" by (unfold LIM_def) + hence "\r > 0. \s > 0. \x. \(x \ a \ \x + -a\ < s --> \X x + -L\ < r)" by simp + hence "\r > 0. \s > 0. \x. (x \ a \ \x + -a\ < s \ \X x + -L\ \ r)" by (simp add: linorder_not_less) + then obtain r where rdef: "r > 0 \ (\s > 0. \x. (x \ a \ \x + -a\ < s \ \X x + -L\ \ r))" by auto + + let ?F = "\n::nat. SOME x. x\a \ \x + -a\ < inverse (real (Suc n)) \ \X x + -L\ \ r" + have "?F ----> a" + proof - + { + fix e::real + assume "0 < e" + (* choose no such that inverse (real (Suc n)) < e *) + have "\no. inverse (real (Suc no)) < e" by (rule reals_Archimedean) + then obtain m where nodef: "inverse (real (Suc m)) < e" by auto + { + fix n + assume mlen: "m \ n" + then have + "inverse (real (Suc n)) \ inverse (real (Suc m))" + by auto + moreover have + "\?F n + -a\ < inverse (real (Suc n))" + proof - + from rdef have + "\x. x\a \ \x + -a\ < inverse (real (Suc n)) \ \X x + -L\ \ r" + by simp + hence + "(?F n)\a \ \(?F n) + -a\ < inverse (real (Suc n)) \ \X (?F n) + -L\ \