--- a/src/HOL/Hyperreal/Lim.thy Thu Sep 28 04:03:43 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Thu Sep 28 06:21:06 2006 +0200
@@ -92,6 +92,14 @@
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
by (simp add: LIM_eq)
+lemma LIM_shift: "f -- a --> L \<Longrightarrow> (\<lambda>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)
+apply (drule_tac x="x + k" in spec)
+apply (simp add: compare_rls)
+done
+
lemma LIM_const [simp]: "(%x. k) -- x --> k"
by (simp add: LIM_def)
@@ -652,27 +660,74 @@
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_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 DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D"
by (simp add: deriv_def)
-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)
-
-subsubsection{*Uniqueness*}
-
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{*Alternative definition for differentiability*}
+
+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)
+
+(* ------------------------------------------------------------------------ *)
+(* Caratheodory formulation of derivative at a point: standard proof *)
+(* ------------------------------------------------------------------------ *)
+
+lemma CARAT_DERIV:
+ "(DERIV f x :> l) =
+ (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
+ (is "?lhs = ?rhs")
+proof
+ assume der: "DERIV f x :> l"
+ show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
+ proof (intro exI conjI)
+ let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
+ show "\<forall>z. f z - f x = ?g z * (z-x)" 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
+ "(\<forall>z. f z - f x = g z * (z-x))" 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
+
+
+
+subsubsection {* Purely 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)
@@ -682,57 +737,6 @@
dest: approx_trans3)
done
-subsubsection{*Alternative definition for differentiability*}
-
-lemma DERIV_LIM_iff:
- "((%h::real. (f(a + h) - f(a)) / h) -- 0 --> D) =
- ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
-proof (intro iffI LIM_I)
- fix r::real
- assume r: "0<r"
- assume "(\<lambda>h. (f (a + h) - f a) / h) -- 0 --> D"
- from LIM_D [OF this r]
- obtain s
- where s: "0 < s"
- and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s --> \<bar>(f (a + x) - f a) / x - D\<bar> < r"
- by auto
- show "\<exists>s. 0 < s \<and>
- (\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm ((f x - f a) / (x-a) - D) < r)"
- proof (intro exI conjI strip)
- show "0 < s" by (rule s)
- next
- fix x::real
- assume "x \<noteq> a \<and> norm (x-a) < s"
- with s_lt [THEN spec [where x="x-a"]]
- show "norm ((f x - f a) / (x-a) - D) < r" by auto
- qed
-next
- fix r::real
- assume r: "0<r"
- assume "(\<lambda>x. (f x - f a) / (x-a)) -- a --> D"
- from LIM_D [OF this r]
- obtain s
- where s: "0 < s"
- and s_lt: "\<forall>x. x \<noteq> a & \<bar>x-a\<bar> < s --> \<bar>(f x - f a)/(x-a) - D\<bar> < r"
- by auto
- show "\<exists>s. 0 < s \<and>
- (\<forall>x. x \<noteq> 0 & norm (x - 0) < s --> norm ((f (a + x) - f a) / x - D) < r)"
- proof (intro exI conjI strip)
- show "0 < s" by (rule s)
- next
- fix x::real
- assume "x \<noteq> 0 \<and> norm (x - 0) < s"
- with s_lt [THEN spec [where x="x+a"]]
- show "norm ((f (a + x) - f a) / x - D) < r" by (auto simp add: add_ac)
- qed
-qed
-
-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)
-
-
-subsubsection{*Equivalence of NS and standard definitions of differentiation*}
-
text {*First NSDERIV in terms of NSLIM*}
text{*first equivalence *}
@@ -804,10 +808,6 @@
simp add: mult_assoc diff_minus)
done
-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)
-
text{*Differentiability implies continuity
nice and simple "algebraic" proof*}
lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
@@ -827,13 +827,6 @@
intro: approx_trans approx_minus_iff [THEN iffD2])
done
-text{*Now Sandard proof*}
-lemma DERIV_isCont: "DERIV f x :> D ==> isCont f x"
-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
follow from clear, straightforard, algebraic
manipulations*}
@@ -843,12 +836,8 @@
lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)"
by (simp add: NSDERIV_NSLIM_iff)
-lemma DERIV_const [simp]: "(DERIV (%x. k) x :> 0)"
-by (simp add: NSDERIV_DERIV_iff [symmetric])
-
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)
@@ -857,12 +846,6 @@
apply (auto simp add: diff_def add_ac)
done
-(* Standard theorem *)
-lemma DERIV_add: "[| DERIV f x :> Da; DERIV g x :> Db |]
- ==> DERIV (%x. f x + g x) x :> Da + Db"
-apply (simp add: NSDERIV_add NSDERIV_DERIV_iff [symmetric])
-done
-
text{*Product of functions - Proof is trivial but tedious
and long due to rearrangement of terms*}
@@ -879,7 +862,6 @@
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)
@@ -903,11 +885,6 @@
simp add: add_assoc [symmetric])
done
-lemma DERIV_mult:
- "[| DERIV f x :> Da; DERIV g x :> Db |]
- ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
-by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric])
-
text{*Multiplying by a constant*}
lemma NSDERIV_cmult: "NSDERIV f x :> D
==> NSDERIV (%x. c * f x) x :> c*D"
@@ -916,16 +893,6 @@
apply (erule NSLIM_const [THEN NSLIM_mult])
done
-(* let's do the standard proof though theorem *)
-(* LIM_mult2 follows from a NS proof *)
-
-lemma DERIV_cmult:
- "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
-apply (simp only: deriv_def times_divide_eq_right [symmetric]
- NSDERIV_NSLIM_iff minus_mult_right right_diff_distrib [symmetric])
-apply (erule LIM_const [THEN LIM_mult2])
-done
-
text{*Negation of function*}
lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
proof (simp add: NSDERIV_NSLIM_iff)
@@ -938,17 +905,10 @@
show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
qed
-
-lemma DERIV_minus: "DERIV f x :> D ==> DERIV (%x. -(f x)) x :> -D"
-by (simp add: NSDERIV_minus NSDERIV_DERIV_iff [symmetric])
-
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 DERIV_add_minus: "[| DERIV f x :> Da; DERIV g x :> Db |] ==> DERIV (%x. f x + -g x) x :> Da + -Db"
-by (blast dest: DERIV_add DERIV_minus)
-
lemma NSDERIV_diff:
"[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
==> NSDERIV (%x. f x - g x) x :> Da-Db"
@@ -956,13 +916,6 @@
apply (blast intro: NSDERIV_add_minus)
done
-lemma DERIV_diff:
- "[| DERIV f x :> Da; DERIV g x :> Db |]
- ==> DERIV (%x. f x - g x) x :> Da-Db"
-apply (simp add: diff_minus)
-apply (blast intro: DERIV_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
@@ -1042,44 +995,12 @@
apply (blast intro: NSDERIVD2)
done
-(* standard version *)
-lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
-by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain)
-
-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)
-
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)
-(*derivative of the identity function*)
-lemma DERIV_Id [simp]: "DERIV (%x. x) x :> 1"
-by (simp add: NSDERIV_DERIV_iff [symmetric])
-
-lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
-
-(*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 NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
-by (simp add: NSDERIV_DERIV_iff)
-
-lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
-apply (induct "n")
-apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
-apply (auto simp add: real_of_nat_Suc left_distrib)
-apply (case_tac "0 < n")
-apply (drule_tac x = x in realpow_minus_mult)
-apply (auto simp add: mult_assoc add_commute)
-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*}
+by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp)
(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*)
lemma NSDERIV_inverse:
@@ -1103,8 +1024,85 @@
apply (rule Infinitesimal_HFinite_mult2, auto)
done
+subsubsection {* Equivalence of NS and Standard definitions *}
+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)
+text{*Now Standard proof*}
+lemma DERIV_isCont: "DERIV f x :> D ==> isCont f x"
+by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric]
+ NSDERIV_isNSCont)
+
+lemma DERIV_const [simp]: "(DERIV (%x. k) x :> 0)"
+by (simp add: NSDERIV_DERIV_iff [symmetric])
+
+(* Standard theorem *)
+lemma DERIV_add: "[| DERIV f x :> Da; DERIV g x :> Db |]
+ ==> DERIV (%x. f x + g x) x :> Da + Db"
+apply (simp add: NSDERIV_add NSDERIV_DERIV_iff [symmetric])
+done
+
+lemma DERIV_mult:
+ "[| DERIV f x :> Da; DERIV g x :> Db |]
+ ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
+by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric])
+
+(* let's do the standard proof though theorem *)
+(* LIM_mult2 follows from a NS proof *)
+
+lemma DERIV_cmult:
+ "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
+apply (simp only: deriv_def times_divide_eq_right [symmetric]
+ NSDERIV_NSLIM_iff minus_mult_right right_diff_distrib [symmetric])
+apply (erule LIM_const [THEN LIM_mult2])
+done
+
+lemma DERIV_minus: "DERIV f x :> D ==> DERIV (%x. -(f x)) x :> -D"
+by (simp add: NSDERIV_minus NSDERIV_DERIV_iff [symmetric])
+
+lemma DERIV_add_minus: "[| DERIV f x :> Da; DERIV g x :> Db |] ==> DERIV (%x. f x + -g x) x :> Da + -Db"
+by (blast dest: DERIV_add DERIV_minus)
+
+lemma DERIV_diff:
+ "[| DERIV f x :> Da; DERIV g x :> Db |]
+ ==> DERIV (%x. f x - g x) x :> Da-Db"
+apply (simp add: diff_minus)
+apply (blast intro: DERIV_add_minus)
+done
+
+(* standard version *)
+lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
+by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain)
+
+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 the identity function*)
+lemma DERIV_Id [simp]: "DERIV (%x. x) x :> 1"
+by (simp add: NSDERIV_DERIV_iff [symmetric])
+
+lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard]
+
+(*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 (induct "n")
+apply (drule_tac [2] DERIV_Id [THEN DERIV_mult])
+apply (auto simp add: real_of_nat_Suc left_distrib)
+apply (case_tac "0 < n")
+apply (drule_tac x = x in realpow_minus_mult)
+apply (auto simp add: mult_assoc add_commute)
+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 \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))"
by (simp add: NSDERIV_inverse NSDERIV_DERIV_iff [symmetric] del: realpow_Suc)
@@ -1137,35 +1135,6 @@
- (e*f(x))) / (g(x) ^ Suc (Suc 0))"
by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
-(* ------------------------------------------------------------------------ *)
-(* Caratheodory formulation of derivative at a point: standard proof *)
-(* ------------------------------------------------------------------------ *)
-
-lemma CARAT_DERIV:
- "(DERIV f x :> l) =
- (\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) & isCont g x & g x = l)"
- (is "?lhs = ?rhs")
-proof
- assume der: "DERIV f x :> l"
- show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
- proof (intro exI conjI)
- let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
- show "\<forall>z. f z - f x = ?g z * (z-x)" 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
- "(\<forall>z. f z - f x = g z * (z-x))" 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 CARAT_NSDERIV: "NSDERIV f x :> l ==>
\<exists>g. (\<forall>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)