# HG changeset patch
# User huffman
# Date 1244506522 25200
# Node ID 2cce9283ba7207fe0353f55fdd38ab8c5a5d3f0a
# Parent  43e8d4bfde2640c2a439671eb3d47d407912e46b
generalize constant 'bounded' to class metric_space

diff -r 43e8d4bfde26 -r 2cce9283ba72 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Mon Jun 08 15:46:14 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Mon Jun 08 17:15:22 2009 -0700
@@ -781,7 +781,7 @@
   using convex_Inter[unfolded Ball_def mem_def] by auto
 
 lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)"
-proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def by auto
+proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
   show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
     unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
     unfolding subset_eq mem_cball dist_norm using B by auto qed
@@ -2049,7 +2049,7 @@
       case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm)
 	using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
     next guess a using UNIV_witness[where 'a = 'n] ..
-      obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_def by auto
+      obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
       hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis a" in ballE) defer apply(erule_tac x="basis a" in ballE)
 	unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def])
       case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
diff -r 43e8d4bfde26 -r 2cce9283ba72 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 15:46:14 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Jun 08 17:15:22 2009 -0700
@@ -1345,6 +1345,27 @@
 
 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
 
+lemma Lim_dist_ubound:
+  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
+  shows "dist a l <= e"
+proof (rule ccontr)
+  assume "\<not> dist a l \<le> e"
+  then have "0 < dist a l - e" by simp
+  with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
+    by (rule tendstoD)
+  with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
+    by (rule eventually_conjI)
+  then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
+    using assms(1) eventually_happens by auto
+  hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
+    by (rule add_le_less_mono)
+  hence "dist a (f w) + dist (f w) l < dist a l"
+    by simp
+  also have "\<dots> \<le> dist a (f w) + dist (f w) l"
+    by (rule dist_triangle)
+  finally show False by simp
+qed
+
 lemma Lim_norm_ubound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
@@ -1961,8 +1982,21 @@
 
   (* FIXME: This has to be unified with BSEQ!! *)
 definition
-  bounded :: "'a::real_normed_vector set \<Rightarrow> bool" where
-  "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x <= a)"
+  bounded :: "'a::metric_space set \<Rightarrow> bool" where
+  "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
+
+lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
+unfolding bounded_def
+apply safe
+apply (rule_tac x="dist a x + e" in exI, clarify)
+apply (drule (1) bspec)
+apply (erule order_trans [OF dist_triangle add_left_mono])
+apply auto
+done
+
+lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
+unfolding bounded_any_center [where a=0]
+by (simp add: dist_norm)
 
 lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
 lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
@@ -1973,16 +2007,17 @@
 
 lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)"
 proof-
-  from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto
-  { fix x assume "x\<in>closure S"
-    then obtain xa where xa:"\<forall>n. xa n \<in> S"  "(xa ---> x) sequentially" unfolding closure_sequential by auto
-    have "\<forall>n. xa n \<in> S \<longrightarrow> norm (xa n) \<le> a" using a by simp
-    hence "eventually (\<lambda>n. norm (xa n) \<le> a) sequentially"
-      by (rule eventually_mono, simp add: xa(1))
-    have "norm x \<le> a"
-      apply (rule Lim_norm_ubound[of sequentially xa x a])
+  from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" unfolding bounded_def by auto
+  { fix y assume "y \<in> closure S"
+    then obtain f where f: "\<forall>n. f n \<in> S"  "(f ---> y) sequentially"
+      unfolding closure_sequential by auto
+    have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
+    hence "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
+      by (rule eventually_mono, simp add: f(1))
+    have "dist x y \<le> a"
+      apply (rule Lim_dist_ubound [of sequentially f])
       apply (rule trivial_limit_sequentially)
-      apply (rule xa(2))
+      apply (rule f(2))
       apply fact
       done
   }
@@ -1991,11 +2026,9 @@
 
 lemma bounded_cball[simp,intro]: "bounded (cball x e)"
   apply (simp add: bounded_def)
-  apply (rule exI[where x="norm x + e"])
-  apply (clarsimp simp add: Ball_def dist_norm, rename_tac y)
-  apply (subgoal_tac "norm y - norm x \<le> e", simp)
-  apply (rule order_trans [OF norm_triangle_ineq2])
-  apply (simp add: norm_minus_commute)
+  apply (rule_tac x=x in exI)
+  apply (rule_tac x=e in exI)
+  apply auto
   done
 
 lemma bounded_ball[simp,intro]: "bounded(ball x e)"
@@ -2003,22 +2036,31 @@
 
 lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
 proof-
-  { fix x F assume as:"bounded F"
-    then obtain a where "\<forall>x\<in>F. norm x \<le> a" unfolding bounded_def by auto
-    hence "bounded (insert x F)" unfolding bounded_def by(auto intro!: add exI[of _ "max a (norm x)"])
+  { fix a F assume as:"bounded F"
+    then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
+    hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
+    hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
   }
   thus ?thesis using finite_induct[of S bounded]  using bounded_empty assms by auto
 qed
 
 lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
   apply (auto simp add: bounded_def)
-  by (rule_tac x="max a aa" in exI, auto)
+  apply (rename_tac x y r s)
+  apply (rule_tac x=x in exI)
+  apply (rule_tac x="max r (dist x y + s)" in exI)
+  apply (rule ballI, rename_tac z, safe)
+  apply (drule (1) bspec, simp)
+  apply (drule (1) bspec)
+  apply (rule min_max.le_supI2)
+  apply (erule order_trans [OF dist_triangle add_left_mono])
+  done
 
 lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
   by (induct rule: finite_induct[of F], auto)
 
 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
-  apply (simp add: bounded_def)
+  apply (simp add: bounded_iff)
   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
   by metis arith
 
@@ -2066,7 +2108,9 @@
   apply (rule bounded_linear_image, assumption)
   by (rule linear_compose_cmul, rule linear_id[unfolded id_def])
 
-lemma bounded_translation: assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
+lemma bounded_translation:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
 proof-
   from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
   { fix x assume "x\<in>S"
@@ -2082,7 +2126,7 @@
 lemma bounded_vec1:
   fixes S :: "real set"
   shows "bounded(vec1 ` S) \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
-  by (simp add: bounded_def forall_vec1 norm_vec1 vec1_in_image_vec1)
+  by (simp add: bounded_iff forall_vec1 norm_vec1 vec1_in_image_vec1)
 
 lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \<noteq> {}"
   shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
@@ -2248,7 +2292,7 @@
         \<exists>l::(real^'a::finite). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
         (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
 proof-
-  obtain b where b:"\<forall>x\<in>s. norm x \<le> b" using assms(1)[unfolded bounded_def] by auto
+  obtain b where b:"\<forall>x\<in>s. norm x \<le> b" using assms(1)[unfolded bounded_iff] by auto
   { { fix i::'a
       { fix n::nat
 	have "\<bar>x n $ i\<bar> \<le> b" using b[THEN bspec[where x="x n"]] and component_le_norm[of "x n" i] and assms(2)[THEN spec[where x=n]] by auto }
@@ -2364,16 +2408,13 @@
 proof-
   from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
   hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
-  { fix n::nat assume "n\<ge>N"
-    hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
-      using norm_triangle_sub[of "s N" "s n"] by (auto, metis norm_minus_commute le_add_right_mono norm_triangle_sub real_less_def)
-  }
-  hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
   moreover
   have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto
-  then obtain a where a:"\<forall>x\<in>s ` {0..N}. norm x \<le> a" unfolding bounded_def by auto
-  ultimately show "?thesis" unfolding bounded_def
-    apply(rule_tac x="max a (norm (s N) + 1)" in exI) apply auto
+  then obtain a where a:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> a"
+    unfolding bounded_any_center [where a="s N"] by auto
+  ultimately show "?thesis"
+    unfolding bounded_any_center [where a="s N"]
+    apply(rule_tac x="max a 1" in exI) apply auto
     apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
 qed
 
@@ -2439,8 +2480,7 @@
 qed
 
 lemma convergent_imp_bounded:
-  fixes s :: "nat \<Rightarrow> 'a::real_normed_vector"
-    (* FIXME: generalize to metric_space *)
+  fixes s :: "nat \<Rightarrow> 'a::metric_space"
   shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
   using convergent_imp_cauchy[of s]
   using cauchy_imp_bounded[of s]
@@ -2573,28 +2613,31 @@
 
 subsection{* Complete the chain of compactness variants. *}
 
-primrec helper_2::"(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> nat \<Rightarrow> 'a" where
+primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_2 beyond 0 = beyond 0" |
-  "helper_2 beyond (Suc n) = beyond (norm (helper_2 beyond n) + 1 )"
-
-lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::real_normed_vector set"
+  "helper_2 beyond (Suc n) = beyond (dist arbitrary (helper_2 beyond n) + 1 )"
+
+lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
   shows "bounded s"
 proof(rule ccontr)
   assume "\<not> bounded s"
-  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> norm (beyond a) \<le> a"
-    unfolding bounded_def apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> norm x \<le> a"] by auto
-  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. norm (beyond a) > a" unfolding linorder_not_le by auto
+  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist arbitrary (beyond a) \<le> a"
+    unfolding bounded_any_center [where a=arbitrary]
+    apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist arbitrary x \<le> a"] by auto
+  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist arbitrary (beyond a) > a"
+    unfolding linorder_not_le by auto
   def x \<equiv> "helper_2 beyond"
 
   { fix m n ::nat assume "m<n"
-    hence "norm (x m) + 1 < norm (x n)"
+    hence "dist arbitrary (x m) + 1 < dist arbitrary (x n)"
     proof(induct n)
       case 0 thus ?case by auto
     next
       case (Suc n)
-      have *:"norm (x n) + 1 < norm (x (Suc n))" unfolding x_def and helper_2.simps
-	using beyond(2)[of "norm (helper_2 beyond n) + 1"] by auto
+      have *:"dist arbitrary (x n) + 1 < dist arbitrary (x (Suc n))"
+        unfolding x_def and helper_2.simps
+	using beyond(2)[of "dist arbitrary (helper_2 beyond n) + 1"] by auto
       thus ?case proof(cases "m < n")
 	case True thus ?thesis using Suc and * by auto
       next
@@ -2606,12 +2649,12 @@
     have "1 < dist (x m) (x n)"
     proof(cases "m<n")
       case True
-      hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
-      thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_norm using norm_triangle_sub[of "x n" "x m"] by auto
+      hence "1 < dist arbitrary (x n) - dist arbitrary (x m)" using *[of m n] by auto
+      thus ?thesis using dist_triangle [of arbitrary "x n" "x m"] by arith
     next
       case False hence "n<m" using `m\<noteq>n` by auto
-      hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
-      thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_norm using norm_triangle_sub[of "x m" "x n"] by auto
+      hence "1 < dist arbitrary (x m) - dist arbitrary (x n)" using *[of n m] by auto
+      thus ?thesis using dist_triangle2 [of arbitrary "x m" "x n"] by arith
     qed  } note ** = this
   { fix a b assume "x a = x b" "a \<noteq> b"
     hence False using **[of a b] by auto  }
@@ -2720,7 +2763,7 @@
 qed
 
 lemma compact_imp_bounded:
-  fixes s :: "'a::real_normed_vector set" (* TODO: generalize to metric_space *)
+  fixes s :: "'a::metric_space set"
   shows "compact s ==> bounded s"
 proof -
   assume "compact s"
@@ -4186,14 +4229,15 @@
 subsection{* Preservation properties for pasted sets.                                  *}
 
 lemma bounded_pastecart:
+  fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
   assumes "bounded s" "bounded t"
   shows "bounded { pastecart x y | x y . (x \<in> s \<and> y \<in> t)}"
 proof-
-  obtain a b where ab:"\<forall>x\<in>s. norm x \<le> a" "\<forall>x\<in>t. norm x \<le> b" using assms[unfolded bounded_def] by auto
+  obtain a b where ab:"\<forall>x\<in>s. norm x \<le> a" "\<forall>x\<in>t. norm x \<le> b" using assms[unfolded bounded_iff] by auto
   { fix x y assume "x\<in>s" "y\<in>t"
     hence "norm x \<le> a" "norm y \<le> b" using ab by auto
     hence "norm (pastecart x y) \<le> a + b" using norm_pastecart[of x y] by auto }
-  thus ?thesis unfolding bounded_def by auto
+  thus ?thesis unfolding bounded_iff by auto
 qed
 
 lemma closed_pastecart:
@@ -4301,6 +4345,7 @@
 text{* We can state this in terms of diameter of a set.                          *}
 
 definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
+  (* TODO: generalize to class metric_space *)
 
 lemma diameter_bounded:
   assumes "bounded s"
@@ -4308,7 +4353,7 @@
         "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
 proof-
   let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
-  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_def] by auto
+  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
   { fix x y assume "x \<in> s" "y \<in> s"
     hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
   note * = this
@@ -4753,7 +4798,7 @@
       have "\<bar>x$i\<bar> \<le> \<bar>a$i\<bar> + \<bar>b$i\<bar>" using x[THEN spec[where x=i]] by auto  }
     hence "(\<Sum>i\<in>UNIV. \<bar>x $ i\<bar>) \<le> ?b" by(rule setsum_mono)
     hence "norm x \<le> ?b" using norm_le_l1[of x] by auto  }
-  thus ?thesis unfolding interval and bounded_def by auto
+  thus ?thesis unfolding interval and bounded_iff by auto
 qed
 
 lemma bounded_interval: fixes a :: "real^'n::finite" shows
@@ -5178,7 +5223,7 @@
   assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
   shows "\<exists>l. (s ---> l) sequentially"
 proof-
-  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_def abs_dest_vec1] by auto
+  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
   { fix m::nat
     have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
       apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }