--- a/src/HOL/Hyperreal/Lim.thy Thu Apr 12 02:59:44 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Thu Apr 12 03:37:30 2007 +0200
@@ -8,10 +8,10 @@
header{* Limits and Continuity *}
theory Lim
-imports HSEQ
+imports SEQ
begin
-text{*Standard and Nonstandard Definitions*}
+text{*Standard Definitions*}
definition
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
@@ -21,29 +21,13 @@
--> norm (f x - L) < r)"
definition
- NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
- ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
- "f -- a --NS> L =
- (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
-
-definition
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
"isCont f a = (f -- a --> (f a))"
definition
- isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
- --{*NS definition dispenses with limit notions*}
- "isNSCont f a = (\<forall>y. y @= star_of a -->
- ( *f* f) y @= star_of (f a))"
-
-definition
isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
"isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
-definition
- isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
-
subsection {* Limits of Functions *}
@@ -374,6 +358,8 @@
shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
by (induct n, simp, simp add: power_Suc LIM_mult f)
+subsubsection {* Derived theorems about @{term LIM} *}
+
lemma LIM_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
assumes r: "0 < r"
@@ -436,175 +422,6 @@
shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
by (rule LIM_inverse_fun [THEN LIM_compose])
-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)
- \<Longrightarrow> f -- a --NS> L"
-by (simp add: NSLIM_def)
-
-lemma NSLIM_D:
- "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
- \<Longrightarrow> starfun f x \<approx> star_of L"
-by (simp add: NSLIM_def)
-
-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)
-
-lemma starfun_scaleR [simp]:
- "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
-by transfer (rule refl)
-
-lemma NSLIM_scaleR:
- "[| 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_scaleR_HFinite)
-
-lemma NSLIM_add:
- "[| 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_add)
-
-lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
-by (simp add: NSLIM_def)
-
-lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
-by (simp add: NSLIM_def)
-
-lemma NSLIM_diff:
- "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
-by (simp only: diff_def NSLIM_add NSLIM_minus)
-
-lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
-by (simp only: NSLIM_add NSLIM_minus)
-
-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 (simp add: NSLIM_def, clarify)
-apply (drule spec)
-apply (auto simp add: star_of_approx_inverse)
-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_diff [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)
-apply (auto simp add: diff_minus add_assoc)
-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 (simp add: NSLIM_def)
-apply (rule_tac x="star_of a + epsilon" in exI)
-apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
- simp add: hypreal_epsilon_not_zero)
-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 (drule NSLIM_add, assumption)
-apply (auto dest!: NSLIM_const_eq [symmetric])
-apply (simp add: diff_def [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"
-by (simp add: NSLIM_def)
-
-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)
- fix x
- assume neq: "x \<noteq> star_of a"
- assume approx: "x \<approx> star_of a"
- have "starfun f x - star_of L \<in> Infinitesimal"
- proof (rule InfinitesimalI2)
- fix r::real assume r: "0 < r"
- from LIM_D [OF f r]
- obtain s where s: "0 < s" and
- less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
- by fast
- from less_r have less_r':
- "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
- \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
- by transfer
- from approx have "x - star_of a \<in> Infinitesimal"
- by (unfold approx_def)
- hence "hnorm (x - star_of a) < star_of s"
- using s by (rule InfinitesimalD2)
- with neq show "hnorm (starfun f x - star_of L) < star_of r"
- by (rule less_r')
- qed
- thus "starfun f x \<approx> star_of L"
- by (unfold approx_def)
-qed
-
-lemma NSLIM_LIM:
- assumes f: "f -- a --NS> L" shows "f -- a --> L"
-proof (rule LIM_I)
- fix r::real assume r: "0 < r"
- have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
- \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
- proof (rule exI, safe)
- show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
- next
- fix x assume neq: "x \<noteq> star_of a"
- assume "hnorm (x - star_of a) < epsilon"
- with Infinitesimal_epsilon
- have "x - star_of a \<in> Infinitesimal"
- by (rule hnorm_less_Infinitesimal)
- hence "x \<approx> star_of a"
- by (unfold approx_def)
- with f neq have "starfun f x \<approx> star_of L"
- by (rule NSLIM_D)
- hence "starfun f x - star_of L \<in> Infinitesimal"
- by (unfold approx_def)
- thus "hnorm (starfun f x - star_of L) < star_of r"
- using r by (rule InfinitesimalD2)
- qed
- thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
- by transfer
-qed
-
-theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
-by (blast intro: LIM_NSLIM NSLIM_LIM)
-
subsection {* Continuity *}
@@ -675,193 +492,15 @@
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
-subsubsection {* Nonstandard proofs *}
-
-lemma isNSContD:
- "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
-by (simp add: isNSCont_def)
-
-lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
-by (simp add: isNSCont_def NSLIM_def)
-
-lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
-apply (simp add: isNSCont_def NSLIM_def, auto)
-apply (case_tac "y = star_of a", auto)
-done
-
-text{*NS continuity can be defined using NS Limit in
- similar fashion to standard def of continuity*}
-lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
-by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
-
-text{*Hence, NS continuity can be given
- in terms of standard limit*}
-lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
-by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
-
-text{*Moreover, it's trivial now that NS continuity
- is equivalent to standard continuity*}
-lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
-apply (simp add: isCont_def)
-apply (rule isNSCont_LIM_iff)
-done
-
-text{*Standard continuity ==> NS continuity*}
-lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
-by (erule isNSCont_isCont_iff [THEN iffD2])
-
-text{*NS continuity ==> Standard continuity*}
-lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
-by (erule isNSCont_isCont_iff [THEN iffD1])
-
-text{*Alternative definition of continuity*}
-(* Prove equivalence between NS limits - *)
-(* seems easier than using standard def *)
-lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
-apply (simp add: NSLIM_def, auto)
-apply (drule_tac x = "star_of a + x" in spec)
-apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
-apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
-apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
- prefer 2 apply (simp add: add_commute diff_def [symmetric])
-apply (rule_tac x = x in star_cases)
-apply (rule_tac [2] x = x in star_cases)
-apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
-done
-
-lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
-by (rule NSLIM_h_iff)
-
-lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
-by (simp add: isNSCont_def)
-
-lemma isNSCont_inverse:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
- shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
-by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
-
-lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
-by (simp add: isNSCont_def)
-
-lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
-apply (simp add: isNSCont_def)
-apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
-done
-
lemma isCont_abs [simp]: "isCont abs (a::real)"
-by (auto simp add: isNSCont_isCont_iff [symmetric])
+by (rule isCont_rabs [OF isCont_Id])
-(****************************************************************
-(%* Leave as commented until I add topology theory or remove? *%)
-(%*------------------------------------------------------------
- Elementary topology proof for a characterisation of
- continuity now: a function f is continuous if and only
- if the inverse image, {x. f(x) \<in> A}, of any open set A
- is always an open set
- ------------------------------------------------------------*%)
-Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
- ==> isNSopen {x. f x \<in> A}"
-by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
-by (dtac (mem_monad_approx RS approx_sym);
-by (dres_inst_tac [("x","a")] spec 1);
-by (dtac isNSContD 1 THEN assume_tac 1)
-by (dtac bspec 1 THEN assume_tac 1)
-by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
-by (blast_tac (claset() addIs [starfun_mem_starset]);
-qed "isNSCont_isNSopen";
-
-Goalw [isNSCont_def]
- "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
-\ ==> isNSCont f x";
-by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
- (approx_minus_iff RS iffD2)],simpset() addsimps
- [Infinitesimal_def,SReal_iff]));
-by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
-by (etac (isNSopen_open_interval RSN (2,impE));
-by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
-by (dres_inst_tac [("x","x")] spec 1);
-by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
- simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
-qed "isNSopen_isNSCont";
-
-Goal "(\<forall>x. isNSCont f x) = \
-\ (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
-by (blast_tac (claset() addIs [isNSCont_isNSopen,
- isNSopen_isNSCont]);
-qed "isNSCont_isNSopen_iff";
-
-(%*------- Standard version of same theorem --------*%)
-Goal "(\<forall>x. isCont f x) = \
-\ (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
-by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
- simpset() addsimps [isNSopen_isopen_iff RS sym,
- isNSCont_isCont_iff RS sym]));
-qed "isCont_isopen_iff";
-*******************************************************************)
-
subsection {* Uniform Continuity *}
-lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
-by (simp add: isNSUCont_def)
-
lemma isUCont_isCont: "isUCont f ==> isCont f x"
by (simp add: isUCont_def isCont_def LIM_def, meson)
-lemma isUCont_isNSUCont:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- assumes f: "isUCont f" shows "isNSUCont f"
-proof (unfold isNSUCont_def, safe)
- fix x y :: "'a star"
- assume approx: "x \<approx> y"
- have "starfun f x - starfun f y \<in> Infinitesimal"
- proof (rule InfinitesimalI2)
- fix r::real assume r: "0 < r"
- with f obtain s where s: "0 < s" and
- less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
- by (auto simp add: isUCont_def)
- from less_r have less_r':
- "\<And>x y. hnorm (x - y) < star_of s
- \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
- by transfer
- from approx have "x - y \<in> Infinitesimal"
- by (unfold approx_def)
- hence "hnorm (x - y) < star_of s"
- using s by (rule InfinitesimalD2)
- thus "hnorm (starfun f x - starfun f y) < star_of r"
- by (rule less_r')
- qed
- thus "starfun f x \<approx> starfun f y"
- by (unfold approx_def)
-qed
-
-lemma isNSUCont_isUCont:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- assumes f: "isNSUCont f" shows "isUCont f"
-proof (unfold isUCont_def, safe)
- fix r::real assume r: "0 < r"
- have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
- \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
- proof (rule exI, safe)
- show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
- next
- fix x y :: "'a star"
- assume "hnorm (x - y) < epsilon"
- with Infinitesimal_epsilon
- have "x - y \<in> Infinitesimal"
- by (rule hnorm_less_Infinitesimal)
- hence "x \<approx> y"
- by (unfold approx_def)
- with f have "starfun f x \<approx> starfun f y"
- by (simp add: isNSUCont_def)
- hence "starfun f x - starfun f y \<in> Infinitesimal"
- by (unfold approx_def)
- thus "hnorm (starfun f x - starfun f y) < star_of r"
- using r by (rule InfinitesimalD2)
- qed
- thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
- by transfer
-qed
subsection {* Relation of LIM and LIMSEQ *}