# HG changeset patch
# User hoelzl
# Date 1363945303 -3600
# Node ID 1e9e68247ad1af5d48bd35784d494e7d842770d9
# Parent  1210309fddab2ff9f8ad3dec3c8b925abc236cbc
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

diff -r 1210309fddab -r 1e9e68247ad1 src/HOL/Limits.thy
--- 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)
diff -r 1210309fddab -r 1e9e68247ad1 src/HOL/Metric_Spaces.thy
--- 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 *}
 
diff -r 1210309fddab -r 1e9e68247ad1 src/HOL/NSA/HSEQ.thy
--- 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*}
diff -r 1210309fddab -r 1e9e68247ad1 src/HOL/RealVector.thy
--- 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 *}
 
diff -r 1210309fddab -r 1e9e68247ad1 src/HOL/SEQ.thy
--- 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
diff -r 1210309fddab -r 1e9e68247ad1 src/HOL/Topological_Spaces.thy
--- 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)