author huffman Thu, 28 Sep 2006 04:03:43 +0200 changeset 20755 956a0377a408 parent 20754 9c053a494dc6 child 20756 fec7f5834ffe
reorganize sections
 src/HOL/Hyperreal/Lim.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 02:50:07 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Sep 28 04:03:43 2006 +0200
@@ -73,8 +73,9 @@
else (x, (x+y)/2))"

+subsection {* Limits of Functions *}

-subsection{*Some Purely Standard Proofs*}
+subsubsection {* Purely standard proofs *}

lemma LIM_eq:
"f -- a --> L =
@@ -141,7 +142,6 @@
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
by (simp only: diff_minus LIM_add LIM_minus)

-
lemma LIM_const_not_eq:
fixes a :: "'a::real_normed_div_algebra"
shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
@@ -211,8 +211,7 @@
done

-
-subsection{*Relationships Between Standard and Nonstandard Concepts*}
+subsubsection {* Purely nonstandard proofs *}

lemma NSLIM_I:
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
@@ -224,6 +223,92 @@
\<Longrightarrow> starfun f x \<approx> star_of L"

+text{*Proving properties of limits using nonstandard definition.
+      The properties hold for standard limits as well!*}
+
+lemma NSLIM_mult:
+  fixes l m :: "'a::real_normed_algebra"
+  shows "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
+by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
+
+     "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
+
+lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
+
+lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
+
+lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
+
+lemma NSLIM_inverse:
+  fixes L :: "'a::real_normed_div_algebra"
+  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
+      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
+apply (drule spec)
+done
+
+lemma NSLIM_zero:
+  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
+proof -
+  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
+    by (rule NSLIM_add_minus [OF f NSLIM_const])
+  thus ?thesis by simp
+qed
+
+lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
+apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
+done
+
+lemma NSLIM_const_not_eq:
+  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
+  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
+apply (rule_tac x="star_of a + epsilon" in exI)
+apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
+done
+
+lemma NSLIM_not_zero:
+  fixes a :: real
+  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
+by (rule NSLIM_const_not_eq)
+
+lemma NSLIM_const_eq:
+  fixes a :: real
+  shows "(%x. k) -- a --NS> L ==> k = L"
+apply (rule ccontr)
+apply (blast dest: NSLIM_const_not_eq)
+done
+
+text{* can actually be proved more easily by unfolding the definition!*}
+lemma NSLIM_unique:
+  fixes a :: real
+  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
+apply (drule NSLIM_minus)
+apply (auto dest!: NSLIM_const_eq [symmetric])
+done
+
+lemma NSLIM_mult_zero:
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+by (drule NSLIM_mult, auto)
+
+lemma NSLIM_self: "(%x. x) -- a --NS> a"
+
+subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
+
lemma LIM_NSLIM:
assumes f: "f -- a --> L" shows "f -- a --NS> L"
proof (rule NSLIM_I)
@@ -282,14 +367,7 @@
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
by (blast intro: LIM_NSLIM NSLIM_LIM)

-text{*Proving properties of limits using nonstandard definition.
-      The properties hold for standard limits as well!*}
-
-lemma NSLIM_mult:
-  fixes l m :: "'a::real_normed_algebra"
-  shows "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
-by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
+subsubsection {* Derived theorems about @{term LIM} *}

lemma LIM_mult2:
fixes l m :: "'a::real_normed_algebra"
@@ -297,115 +375,38 @@
==> (%x. f(x) * g(x)) -- x --> (l * m)"

-     "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
-
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"

-
-lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
-
lemma LIM_const2: "(%x. k) -- x --> k"

-lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
-
lemma LIM_minus2: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"

-
-lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
-
lemma LIM_add_minus2: "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"

-
-lemma NSLIM_inverse:
-  fixes L :: "'a::real_normed_div_algebra"
-  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
-      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
-apply (drule spec)
-done
-
lemma LIM_inverse:
fixes L :: "'a::real_normed_div_algebra"
shows "[| f -- a --> L; L \<noteq> 0 |]
==> (%x. inverse(f(x))) -- a --> (inverse L)"

-
-lemma NSLIM_zero:
-  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
-proof -
-  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
-    by (rule NSLIM_add_minus [OF f NSLIM_const])
-  thus ?thesis by simp
-qed
-
lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"

-lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
-apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
-done
-
lemma LIM_zero_cancel: "(%x. f(x) - l) -- x --> 0 ==> f -- x --> l"
apply (drule_tac g = "%x. l" and M = l in LIM_add)
done

-lemma NSLIM_const_not_eq:
-  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
-  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
-apply (rule_tac x="star_of a + epsilon" in exI)
-apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
-done
-
-lemma NSLIM_not_zero:
-  fixes a :: real
-  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
-by (rule NSLIM_const_not_eq)
-
-lemma NSLIM_const_eq:
-  fixes a :: real
-  shows "(%x. k) -- a --NS> L ==> k = L"
-apply (rule ccontr)
-apply (blast dest: NSLIM_const_not_eq)
-done
-
-text{* can actually be proved more easily by unfolding the definition!*}
-lemma NSLIM_unique:
-  fixes a :: real
-  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
-apply (drule NSLIM_minus)
-apply (auto dest!: NSLIM_const_eq [symmetric])
-done
-
lemma LIM_unique2:
fixes a :: real
shows "[| f -- a --> L; f -- a --> M |] ==> L = M"

-
-lemma NSLIM_mult_zero:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
-by (drule NSLIM_mult, auto)
-
(* we can use the corresponding thm LIM_mult2 *)
(* for standard definition of limit           *)

@@ -415,13 +416,7 @@
by (drule LIM_mult2, auto)

-lemma NSLIM_self: "(%x. x) -- a --NS> a"
-
-
-subsection{* Derivatives and Continuity: NS and Standard properties*}
-
-subsubsection{*Continuity*}
+subsection {* Continuity *}

lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
@@ -592,7 +587,8 @@
qed "isCont_isopen_iff";
*******************************************************************)

-text{*Uniform continuity*}
+subsection {* Uniform Continuity *}
+
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"

@@ -654,7 +650,8 @@
by transfer
qed

-text{*Derivatives*}
+subsection {* Derivatives *}
+
lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"

@@ -668,7 +665,6 @@
lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"

-
subsubsection{*Uniqueness*}

lemma DERIV_unique:
@@ -686,20 +682,6 @@
dest: approx_trans3)
done

-subsubsection{*Differentiable*}
-
-lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
-
-lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
-
-lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
-
-lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
-
subsubsection{*Alternative definition for differentiability*}

lemma DERIV_LIM_iff:
@@ -749,9 +731,9 @@
by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)

-subsection{*Equivalence of NS and standard definitions of differentiation*}
+subsubsection{*Equivalence of NS and standard definitions of differentiation*}

-subsubsection{*First NSDERIV in terms of NSLIM*}
+text {*First NSDERIV in terms of NSLIM*}

text{*first equivalence *}
lemma NSDERIV_NSLIM_iff:
@@ -850,6 +832,7 @@
by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
NSDERIV_isNSCont)

+subsubsection {* Derivatives of various functions *}

text{*Differentiation rules for combinations of functions
@@ -980,47 +963,6 @@
done

-text{*(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)"
-apply (erule NSdifferentiableI [THEN incrementI])
-done
-
-(* The Increment theorem -- Keisler p. 65 *)
-lemma increment_thm: "[| NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 |]
-      ==> \<exists>e \<in> 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
-done
-
-lemma increment_thm2:
-     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
-      ==> \<exists>e \<in> 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 \<approx> 0; h \<noteq> 0 |]
-      ==> increment f x h \<approx> 0"
-apply (drule increment_thm2,
-apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
-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
@@ -1245,6 +1187,114 @@
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
qed

+subsubsection {* Differentiability predicate *}
+
+lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
+
+lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
+
+lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
+
+lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x"
+
+lemma differentiable_const: "(\<lambda>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 "(\<lambda>x. f x + g x) differentiable x"
+proof -
+  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
+  then obtain df where "DERIV f x :> df" ..
+  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+  then obtain dg where "DERIV g x :> dg" ..
+  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
+  hence "\<exists>D. DERIV (\<lambda>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 "(\<lambda>x. f x - g x) differentiable x"
+proof -
+  from prems have "f differentiable x" by simp
+  moreover
+  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+  then obtain dg where "DERIV g x :> dg" ..
+  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
+  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
+  hence "(\<lambda>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 "(\<lambda>x. f x * g x) differentiable x"
+proof -
+  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
+  then obtain df where "DERIV f x :> df" ..
+  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
+  then obtain dg where "DERIV g x :> dg" ..
+  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
+  hence "\<exists>D. DERIV (\<lambda>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)"
+
+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 \<in> Infinitesimal; h \<noteq> 0 |]
+      ==> \<exists>e \<in> 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
+done
+
+lemma increment_thm2:
+     "[| NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 |]
+      ==> \<exists>e \<in> 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 \<approx> 0; h \<noteq> 0 |]
+      ==> increment f x h \<approx> 0"
+apply (drule increment_thm2,
+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.*}

@@ -1436,7 +1486,9 @@
done

-subsection{*Intermediate Value Theorem: Prove Contrapositive by Bisection*}
+subsection {* Intermediate Value Theorem *}
+
+text {*Prove Contrapositive by Bisection*}

lemma IVT: "[| f(a::real) \<le> (y::real); y \<le> f(b);
a \<le> b;
@@ -1487,7 +1539,7 @@
apply (blast intro: IVT2)
done

-subsection{*By bisection, function continuous on closed interval is bounded above*}
+text{*By bisection, function continuous on closed interval is bounded above*}

lemma isCont_bounded:
"[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
@@ -1605,7 +1657,7 @@
done

-subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
+text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}

lemma DERIV_left_inc:
assumes der: "DERIV f x :> l"
@@ -2089,59 +2141,6 @@
qed
qed

-
-lemma differentiable_const: "(\<lambda>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 "(\<lambda>x. f x + g x) differentiable x"
-proof -
-  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
-  then obtain df where "DERIV f x :> df" ..
-  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
-  then obtain dg where "DERIV g x :> dg" ..
-  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
-  hence "\<exists>D. DERIV (\<lambda>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 "(\<lambda>x. f x - g x) differentiable x"
-proof -
-  from prems have "f differentiable x" by simp
-  moreover
-  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
-  then obtain dg where "DERIV g x :> dg" ..
-  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
-  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
-  hence "(\<lambda>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 "(\<lambda>x. f x * g x) differentiable x"
-proof -
-  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
-  then obtain df where "DERIV f x :> df" ..
-  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
-  then obtain dg where "DERIV g x :> dg" ..
-  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
-  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
-  thus ?thesis by (fold differentiable_def)
-qed
-
-
theorem GMVT:
assumes alb: "a < b"
and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"```