--- a/src/HOL/Limits.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Limits.thy Fri Mar 22 10:41:43 2013 +0100
@@ -49,8 +49,18 @@
subsection {* Boundedness *}
-definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
- where "Bfun f F = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
+lemma Bfun_def:
+ "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
+ unfolding Bfun_metric_def norm_conv_dist
+proof safe
+ fix y K assume "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F"
+ moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F"
+ by (intro always_eventually) (metis dist_commute dist_triangle)
+ with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F"
+ by eventually_elim auto
+ with `0 < K` show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
+ by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
+qed auto
lemma BfunI:
assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F"
@@ -67,7 +77,6 @@
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
using assms unfolding Bfun_def by fast
-
subsection {* Convergence to Zero *}
definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
@@ -223,9 +232,6 @@
subsubsection {* Distance and norms *}
-lemma norm_conv_dist: "norm x = dist x 0"
- unfolding dist_norm by simp
-
lemma tendsto_norm [tendsto_intros]:
"(f ---> a) F \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) F"
unfolding norm_conv_dist by (intro tendsto_intros)
--- a/src/HOL/Metric_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Metric_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
@@ -285,6 +285,22 @@
shows "(\<lambda>x. g (f x)) -- a --> l"
by (rule metric_LIM_compose2 [OF f g inj])
+subsubsection {* Boundedness *}
+
+definition Bfun :: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a filter \<Rightarrow> bool" where
+ Bfun_metric_def: "Bfun f F = (\<exists>y. \<exists>K>0. eventually (\<lambda>x. dist (f x) y \<le> K) F)"
+
+abbreviation Bseq :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
+ "Bseq X \<equiv> Bfun X sequentially"
+
+lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially" ..
+
+lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
+ unfolding Bfun_metric_def by (subst eventually_sequentially_seg)
+
+lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
+ unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg)
+
subsection {* Complete metric spaces *}
subsection {* Cauchy sequences *}
@@ -320,6 +336,18 @@
apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
done
+lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
+ unfolding Cauchy_def Bfun_metric_def eventually_sequentially
+ apply (erule_tac x=1 in allE)
+ apply simp
+ apply safe
+ apply (rule_tac x="X M" in exI)
+ apply (rule_tac x=1 in exI)
+ apply (erule_tac x=M in allE)
+ apply simp
+ apply (rule_tac x=M in exI)
+ apply (auto simp: dist_commute)
+ done
subsubsection {* Cauchy Sequences are Convergent *}
--- a/src/HOL/NSA/HSEQ.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/NSA/HSEQ.thy Fri Mar 22 10:41:43 2013 +0100
@@ -343,7 +343,7 @@
text{*Standard Version: easily now proved using equivalence of NS and
standard definitions *}
-lemma convergent_Bseq: "convergent X ==> Bseq X"
+lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
--- a/src/HOL/RealVector.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/RealVector.thy Fri Mar 22 10:41:43 2013 +0100
@@ -665,7 +665,6 @@
using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
qed
-
subsection {* Class instances for real numbers *}
instantiation real :: real_normed_field
@@ -743,6 +742,8 @@
lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
unfolding real_sgn_eq by simp
+lemma norm_conv_dist: "norm x = dist x 0"
+ unfolding dist_norm by simp
subsection {* Bounded Linear and Bilinear Operators *}
--- a/src/HOL/SEQ.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/SEQ.thy Fri Mar 22 10:41:43 2013 +0100
@@ -13,64 +13,6 @@
imports Limits
begin
-subsection {* Defintions of limits *}
-
-definition
- Bseq :: "(nat => 'a::real_normed_vector) => bool" where
- --{*Standard definition for bounded sequence*}
- "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
-
-subsection {* Bounded Sequences *}
-
-lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
-unfolding Bseq_def
-proof (intro exI conjI allI)
- show "0 < max K 1" by simp
-next
- fix n::nat
- have "norm (X n) \<le> K" by (rule K)
- thus "norm (X n) \<le> max K 1" by simp
-qed
-
-lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-unfolding Bseq_def by auto
-
-lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X"
-proof (rule BseqI')
- let ?A = "norm ` X ` {..N}"
- have 1: "finite ?A" by simp
- fix n::nat
- show "norm (X n) \<le> max K (Max ?A)"
- proof (cases rule: linorder_le_cases)
- assume "n \<ge> N"
- hence "norm (X n) \<le> K" using K by simp
- thus "norm (X n) \<le> max K (Max ?A)" by simp
- next
- assume "n \<le> N"
- hence "norm (X n) \<in> ?A" by simp
- with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge)
- thus "norm (X n) \<le> max K (Max ?A)" by simp
- qed
-qed
-
-lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))"
-unfolding Bseq_def by auto
-
-lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X"
-apply (erule BseqE)
-apply (rule_tac N="k" and K="K" in BseqI2')
-apply clarify
-apply (drule_tac x="n - k" in spec, simp)
-done
-
-lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
-unfolding Bfun_def eventually_sequentially
-apply (rule iffI)
-apply (simp add: Bseq_def)
-apply (auto intro: BseqI2')
-done
-
-
subsection {* Limits of Sequences *}
lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
@@ -105,7 +47,7 @@
lemma Bseq_inverse:
fixes a :: "'a::real_normed_div_algebra"
shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
-unfolding Bseq_conv_Bfun by (rule Bfun_inverse)
+ by (rule Bfun_inverse)
lemma LIMSEQ_diff_approach_zero:
fixes L :: "'a::real_normed_vector"
@@ -188,7 +130,25 @@
subsection {* Bounded Monotonic Sequences *}
-text{*Bounded Sequence*}
+subsubsection {* Bounded Sequences *}
+
+lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
+ by (intro BfunI) (auto simp: eventually_sequentially)
+
+lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
+ by (intro BfunI) (auto simp: eventually_sequentially)
+
+lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
+ unfolding Bfun_def eventually_sequentially
+proof safe
+ fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
+ then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
+ by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
+ (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
+qed auto
+
+lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+unfolding Bseq_def by auto
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
by (simp add: Bseq_def)
@@ -280,11 +240,11 @@
(* TODO: delete *)
(* FIXME: one use in NSA/HSEQ.thy *)
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
-unfolding tendsto_def eventually_sequentially
-apply (rule_tac x = "X m" in exI, safe)
-apply (rule_tac x = m in exI, safe)
-apply (drule spec, erule impE, auto)
-done
+ apply (rule_tac x="X m" in exI)
+ apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
+ unfolding eventually_sequentially
+ apply blast
+ done
text {* A monotone sequence converges to its least upper bound. *}
@@ -317,7 +277,7 @@
"Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
-lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
+lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
by (simp add: Bseq_def)
text{*Main monotonicity theorem*}
@@ -354,18 +314,6 @@
apply simp
done
-lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
-apply (simp add: Cauchy_iff)
-apply (drule spec, drule mp, rule zero_less_one, safe)
-apply (drule_tac x="M" in spec, simp)
-apply (drule lemmaCauchy)
-apply (rule_tac k="M" in Bseq_offset)
-apply (simp add: Bseq_def)
-apply (rule_tac x="1 + norm (X M)" in exI)
-apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp)
-apply (simp add: order_less_imp_le)
-done
-
class banach = real_normed_vector + complete_space
instance real :: banach by default
--- a/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
@@ -643,6 +643,17 @@
shows "eventually P sequentially"
using assms by (auto simp: eventually_sequentially)
+lemma eventually_sequentially_seg:
+ "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
+ unfolding eventually_sequentially
+ apply safe
+ apply (rule_tac x="N + k" in exI)
+ apply rule
+ apply (erule_tac x="n - k" in allE)
+ apply auto []
+ apply (rule_tac x=N in exI)
+ apply auto []
+ done
subsubsection {* Standard filters *}
@@ -1354,25 +1365,13 @@
lemma LIMSEQ_ignore_initial_segment:
"f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
-apply (rule topological_tendstoI)
-apply (drule (2) topological_tendstoD)
-apply (simp only: eventually_sequentially)
-apply (erule exE, rename_tac N)
-apply (rule_tac x=N in exI)
-apply simp
-done
+ unfolding tendsto_def
+ by (subst eventually_sequentially_seg[where k=k])
lemma LIMSEQ_offset:
"(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
-apply (rule topological_tendstoI)
-apply (drule (2) topological_tendstoD)
-apply (simp only: eventually_sequentially)
-apply (erule exE, rename_tac N)
-apply (rule_tac x="N + k" in exI)
-apply clarify
-apply (drule_tac x="n - k" in spec)
-apply (simp add: le_diff_conv2)
-done
+ unfolding tendsto_def
+ by (subst (asm) eventually_sequentially_seg[where k=k])
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)