src/HOL/Library/Topology_Euclidean_Space.thy
changeset 31533 2cce9283ba72
parent 31532 43e8d4bfde26
child 31534 0de814d2ff95
equal deleted inserted replaced
31532:43e8d4bfde26 31533:2cce9283ba72
  1343     by (simp add: eventually_False)
  1343     by (simp add: eventually_False)
  1344 qed
  1344 qed
  1345 
  1345 
  1346 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
  1346 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
  1347 
  1347 
       
  1348 lemma Lim_dist_ubound:
       
  1349   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
       
  1350   shows "dist a l <= e"
       
  1351 proof (rule ccontr)
       
  1352   assume "\<not> dist a l \<le> e"
       
  1353   then have "0 < dist a l - e" by simp
       
  1354   with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
       
  1355     by (rule tendstoD)
       
  1356   with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
       
  1357     by (rule eventually_conjI)
       
  1358   then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
       
  1359     using assms(1) eventually_happens by auto
       
  1360   hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
       
  1361     by (rule add_le_less_mono)
       
  1362   hence "dist a (f w) + dist (f w) l < dist a l"
       
  1363     by simp
       
  1364   also have "\<dots> \<le> dist a (f w) + dist (f w) l"
       
  1365     by (rule dist_triangle)
       
  1366   finally show False by simp
       
  1367 qed
       
  1368 
  1348 lemma Lim_norm_ubound:
  1369 lemma Lim_norm_ubound:
  1349   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
  1370   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
  1350   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
  1371   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
  1351   shows "norm(l) <= e"
  1372   shows "norm(l) <= e"
  1352 proof (rule ccontr)
  1373 proof (rule ccontr)
  1959 
  1980 
  1960 subsection{* Boundedness. *}
  1981 subsection{* Boundedness. *}
  1961 
  1982 
  1962   (* FIXME: This has to be unified with BSEQ!! *)
  1983   (* FIXME: This has to be unified with BSEQ!! *)
  1963 definition
  1984 definition
  1964   bounded :: "'a::real_normed_vector set \<Rightarrow> bool" where
  1985   bounded :: "'a::metric_space set \<Rightarrow> bool" where
  1965   "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x <= a)"
  1986   "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
       
  1987 
       
  1988 lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
       
  1989 unfolding bounded_def
       
  1990 apply safe
       
  1991 apply (rule_tac x="dist a x + e" in exI, clarify)
       
  1992 apply (drule (1) bspec)
       
  1993 apply (erule order_trans [OF dist_triangle add_left_mono])
       
  1994 apply auto
       
  1995 done
       
  1996 
       
  1997 lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
       
  1998 unfolding bounded_any_center [where a=0]
       
  1999 by (simp add: dist_norm)
  1966 
  2000 
  1967 lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
  2001 lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
  1968 lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
  2002 lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
  1969   by (metis bounded_def subset_eq)
  2003   by (metis bounded_def subset_eq)
  1970 
  2004 
  1971 lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)"
  2005 lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)"
  1972   by (metis bounded_subset interior_subset)
  2006   by (metis bounded_subset interior_subset)
  1973 
  2007 
  1974 lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)"
  2008 lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)"
  1975 proof-
  2009 proof-
  1976   from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto
  2010   from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" unfolding bounded_def by auto
  1977   { fix x assume "x\<in>closure S"
  2011   { fix y assume "y \<in> closure S"
  1978     then obtain xa where xa:"\<forall>n. xa n \<in> S"  "(xa ---> x) sequentially" unfolding closure_sequential by auto
  2012     then obtain f where f: "\<forall>n. f n \<in> S"  "(f ---> y) sequentially"
  1979     have "\<forall>n. xa n \<in> S \<longrightarrow> norm (xa n) \<le> a" using a by simp
  2013       unfolding closure_sequential by auto
  1980     hence "eventually (\<lambda>n. norm (xa n) \<le> a) sequentially"
  2014     have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
  1981       by (rule eventually_mono, simp add: xa(1))
  2015     hence "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
  1982     have "norm x \<le> a"
  2016       by (rule eventually_mono, simp add: f(1))
  1983       apply (rule Lim_norm_ubound[of sequentially xa x a])
  2017     have "dist x y \<le> a"
       
  2018       apply (rule Lim_dist_ubound [of sequentially f])
  1984       apply (rule trivial_limit_sequentially)
  2019       apply (rule trivial_limit_sequentially)
  1985       apply (rule xa(2))
  2020       apply (rule f(2))
  1986       apply fact
  2021       apply fact
  1987       done
  2022       done
  1988   }
  2023   }
  1989   thus ?thesis unfolding bounded_def by auto
  2024   thus ?thesis unfolding bounded_def by auto
  1990 qed
  2025 qed
  1991 
  2026 
  1992 lemma bounded_cball[simp,intro]: "bounded (cball x e)"
  2027 lemma bounded_cball[simp,intro]: "bounded (cball x e)"
  1993   apply (simp add: bounded_def)
  2028   apply (simp add: bounded_def)
  1994   apply (rule exI[where x="norm x + e"])
  2029   apply (rule_tac x=x in exI)
  1995   apply (clarsimp simp add: Ball_def dist_norm, rename_tac y)
  2030   apply (rule_tac x=e in exI)
  1996   apply (subgoal_tac "norm y - norm x \<le> e", simp)
  2031   apply auto
  1997   apply (rule order_trans [OF norm_triangle_ineq2])
       
  1998   apply (simp add: norm_minus_commute)
       
  1999   done
  2032   done
  2000 
  2033 
  2001 lemma bounded_ball[simp,intro]: "bounded(ball x e)"
  2034 lemma bounded_ball[simp,intro]: "bounded(ball x e)"
  2002   by (metis ball_subset_cball bounded_cball bounded_subset)
  2035   by (metis ball_subset_cball bounded_cball bounded_subset)
  2003 
  2036 
  2004 lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
  2037 lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
  2005 proof-
  2038 proof-
  2006   { fix x F assume as:"bounded F"
  2039   { fix a F assume as:"bounded F"
  2007     then obtain a where "\<forall>x\<in>F. norm x \<le> a" unfolding bounded_def by auto
  2040     then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
  2008     hence "bounded (insert x F)" unfolding bounded_def by(auto intro!: add exI[of _ "max a (norm x)"])
  2041     hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
       
  2042     hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
  2009   }
  2043   }
  2010   thus ?thesis using finite_induct[of S bounded]  using bounded_empty assms by auto
  2044   thus ?thesis using finite_induct[of S bounded]  using bounded_empty assms by auto
  2011 qed
  2045 qed
  2012 
  2046 
  2013 lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
  2047 lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
  2014   apply (auto simp add: bounded_def)
  2048   apply (auto simp add: bounded_def)
  2015   by (rule_tac x="max a aa" in exI, auto)
  2049   apply (rename_tac x y r s)
       
  2050   apply (rule_tac x=x in exI)
       
  2051   apply (rule_tac x="max r (dist x y + s)" in exI)
       
  2052   apply (rule ballI, rename_tac z, safe)
       
  2053   apply (drule (1) bspec, simp)
       
  2054   apply (drule (1) bspec)
       
  2055   apply (rule min_max.le_supI2)
       
  2056   apply (erule order_trans [OF dist_triangle add_left_mono])
       
  2057   done
  2016 
  2058 
  2017 lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
  2059 lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
  2018   by (induct rule: finite_induct[of F], auto)
  2060   by (induct rule: finite_induct[of F], auto)
  2019 
  2061 
  2020 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
  2062 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
  2021   apply (simp add: bounded_def)
  2063   apply (simp add: bounded_iff)
  2022   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
  2064   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
  2023   by metis arith
  2065   by metis arith
  2024 
  2066 
  2025 lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
  2067 lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
  2026   by (metis Int_lower1 Int_lower2 bounded_subset)
  2068   by (metis Int_lower1 Int_lower2 bounded_subset)
  2064   fixes S :: "(real ^ 'n::finite) set"
  2106   fixes S :: "(real ^ 'n::finite) set"
  2065   shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *s x) ` S)"
  2107   shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *s x) ` S)"
  2066   apply (rule bounded_linear_image, assumption)
  2108   apply (rule bounded_linear_image, assumption)
  2067   by (rule linear_compose_cmul, rule linear_id[unfolded id_def])
  2109   by (rule linear_compose_cmul, rule linear_id[unfolded id_def])
  2068 
  2110 
  2069 lemma bounded_translation: assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
  2111 lemma bounded_translation:
       
  2112   fixes S :: "'a::real_normed_vector set"
       
  2113   assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
  2070 proof-
  2114 proof-
  2071   from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
  2115   from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
  2072   { fix x assume "x\<in>S"
  2116   { fix x assume "x\<in>S"
  2073     hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto
  2117     hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto
  2074   }
  2118   }
  2080 text{* Some theorems on sups and infs using the notion "bounded". *}
  2124 text{* Some theorems on sups and infs using the notion "bounded". *}
  2081 
  2125 
  2082 lemma bounded_vec1:
  2126 lemma bounded_vec1:
  2083   fixes S :: "real set"
  2127   fixes S :: "real set"
  2084   shows "bounded(vec1 ` S) \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
  2128   shows "bounded(vec1 ` S) \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
  2085   by (simp add: bounded_def forall_vec1 norm_vec1 vec1_in_image_vec1)
  2129   by (simp add: bounded_iff forall_vec1 norm_vec1 vec1_in_image_vec1)
  2086 
  2130 
  2087 lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \<noteq> {}"
  2131 lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \<noteq> {}"
  2088   shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
  2132   shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
  2089 proof
  2133 proof
  2090   fix x assume "x\<in>S"
  2134   fix x assume "x\<in>S"
  2246   assumes "bounded s" and "\<forall>n. (x::nat \<Rightarrow>real^'a::finite) n \<in> s"
  2290   assumes "bounded s" and "\<forall>n. (x::nat \<Rightarrow>real^'a::finite) n \<in> s"
  2247   shows "\<forall>d.
  2291   shows "\<forall>d.
  2248         \<exists>l::(real^'a::finite). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
  2292         \<exists>l::(real^'a::finite). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
  2249         (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
  2293         (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
  2250 proof-
  2294 proof-
  2251   obtain b where b:"\<forall>x\<in>s. norm x \<le> b" using assms(1)[unfolded bounded_def] by auto
  2295   obtain b where b:"\<forall>x\<in>s. norm x \<le> b" using assms(1)[unfolded bounded_iff] by auto
  2252   { { fix i::'a
  2296   { { fix i::'a
  2253       { fix n::nat
  2297       { fix n::nat
  2254 	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 }
  2298 	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 }
  2255       hence "\<forall>n. \<bar>x n $ i\<bar> \<le> b" by auto
  2299       hence "\<forall>n. \<bar>x n $ i\<bar> \<le> b" by auto
  2256     } note b' = this
  2300     } note b' = this
  2362 
  2406 
  2363 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
  2407 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
  2364 proof-
  2408 proof-
  2365   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
  2409   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
  2366   hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
  2410   hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
  2367   { fix n::nat assume "n\<ge>N"
       
  2368     hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
       
  2369       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)
       
  2370   }
       
  2371   hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
       
  2372   moreover
  2411   moreover
  2373   have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto
  2412   have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto
  2374   then obtain a where a:"\<forall>x\<in>s ` {0..N}. norm x \<le> a" unfolding bounded_def by auto
  2413   then obtain a where a:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> a"
  2375   ultimately show "?thesis" unfolding bounded_def
  2414     unfolding bounded_any_center [where a="s N"] by auto
  2376     apply(rule_tac x="max a (norm (s N) + 1)" in exI) apply auto
  2415   ultimately show "?thesis"
       
  2416     unfolding bounded_any_center [where a="s N"]
       
  2417     apply(rule_tac x="max a 1" in exI) apply auto
  2377     apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
  2418     apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
  2378 qed
  2419 qed
  2379 
  2420 
  2380 lemma compact_imp_complete: assumes "compact s" shows "complete s"
  2421 lemma compact_imp_complete: assumes "compact s" shows "complete s"
  2381 proof-
  2422 proof-
  2437 next
  2478 next
  2438   assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto
  2479   assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto
  2439 qed
  2480 qed
  2440 
  2481 
  2441 lemma convergent_imp_bounded:
  2482 lemma convergent_imp_bounded:
  2442   fixes s :: "nat \<Rightarrow> 'a::real_normed_vector"
  2483   fixes s :: "nat \<Rightarrow> 'a::metric_space"
  2443     (* FIXME: generalize to metric_space *)
       
  2444   shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
  2484   shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
  2445   using convergent_imp_cauchy[of s]
  2485   using convergent_imp_cauchy[of s]
  2446   using cauchy_imp_bounded[of s]
  2486   using cauchy_imp_bounded[of s]
  2447   unfolding image_def
  2487   unfolding image_def
  2448   by auto
  2488   by auto
  2571   ultimately show False using g(2) using finite_subset by auto
  2611   ultimately show False using g(2) using finite_subset by auto
  2572 qed
  2612 qed
  2573 
  2613 
  2574 subsection{* Complete the chain of compactness variants. *}
  2614 subsection{* Complete the chain of compactness variants. *}
  2575 
  2615 
  2576 primrec helper_2::"(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> nat \<Rightarrow> 'a" where
  2616 primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
  2577   "helper_2 beyond 0 = beyond 0" |
  2617   "helper_2 beyond 0 = beyond 0" |
  2578   "helper_2 beyond (Suc n) = beyond (norm (helper_2 beyond n) + 1 )"
  2618   "helper_2 beyond (Suc n) = beyond (dist arbitrary (helper_2 beyond n) + 1 )"
  2579 
  2619 
  2580 lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::real_normed_vector set"
  2620 lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
  2581   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
  2621   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
  2582   shows "bounded s"
  2622   shows "bounded s"
  2583 proof(rule ccontr)
  2623 proof(rule ccontr)
  2584   assume "\<not> bounded s"
  2624   assume "\<not> bounded s"
  2585   then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> norm (beyond a) \<le> a"
  2625   then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist arbitrary (beyond a) \<le> a"
  2586     unfolding bounded_def apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> norm x \<le> a"] by auto
  2626     unfolding bounded_any_center [where a=arbitrary]
  2587   hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. norm (beyond a) > a" unfolding linorder_not_le by auto
  2627     apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist arbitrary x \<le> a"] by auto
       
  2628   hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist arbitrary (beyond a) > a"
       
  2629     unfolding linorder_not_le by auto
  2588   def x \<equiv> "helper_2 beyond"
  2630   def x \<equiv> "helper_2 beyond"
  2589 
  2631 
  2590   { fix m n ::nat assume "m<n"
  2632   { fix m n ::nat assume "m<n"
  2591     hence "norm (x m) + 1 < norm (x n)"
  2633     hence "dist arbitrary (x m) + 1 < dist arbitrary (x n)"
  2592     proof(induct n)
  2634     proof(induct n)
  2593       case 0 thus ?case by auto
  2635       case 0 thus ?case by auto
  2594     next
  2636     next
  2595       case (Suc n)
  2637       case (Suc n)
  2596       have *:"norm (x n) + 1 < norm (x (Suc n))" unfolding x_def and helper_2.simps
  2638       have *:"dist arbitrary (x n) + 1 < dist arbitrary (x (Suc n))"
  2597 	using beyond(2)[of "norm (helper_2 beyond n) + 1"] by auto
  2639         unfolding x_def and helper_2.simps
       
  2640 	using beyond(2)[of "dist arbitrary (helper_2 beyond n) + 1"] by auto
  2598       thus ?case proof(cases "m < n")
  2641       thus ?case proof(cases "m < n")
  2599 	case True thus ?thesis using Suc and * by auto
  2642 	case True thus ?thesis using Suc and * by auto
  2600       next
  2643       next
  2601 	case False hence "m = n" using Suc(2) by auto
  2644 	case False hence "m = n" using Suc(2) by auto
  2602 	thus ?thesis using * by auto
  2645 	thus ?thesis using * by auto
  2604     qed  } note * = this
  2647     qed  } note * = this
  2605   { fix m n ::nat assume "m\<noteq>n"
  2648   { fix m n ::nat assume "m\<noteq>n"
  2606     have "1 < dist (x m) (x n)"
  2649     have "1 < dist (x m) (x n)"
  2607     proof(cases "m<n")
  2650     proof(cases "m<n")
  2608       case True
  2651       case True
  2609       hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
  2652       hence "1 < dist arbitrary (x n) - dist arbitrary (x m)" using *[of m n] by auto
  2610       thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_norm using norm_triangle_sub[of "x n" "x m"] by auto
  2653       thus ?thesis using dist_triangle [of arbitrary "x n" "x m"] by arith
  2611     next
  2654     next
  2612       case False hence "n<m" using `m\<noteq>n` by auto
  2655       case False hence "n<m" using `m\<noteq>n` by auto
  2613       hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
  2656       hence "1 < dist arbitrary (x m) - dist arbitrary (x n)" using *[of n m] by auto
  2614       thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_norm using norm_triangle_sub[of "x m" "x n"] by auto
  2657       thus ?thesis using dist_triangle2 [of arbitrary "x m" "x n"] by arith
  2615     qed  } note ** = this
  2658     qed  } note ** = this
  2616   { fix a b assume "x a = x b" "a \<noteq> b"
  2659   { fix a b assume "x a = x b" "a \<noteq> b"
  2617     hence False using **[of a b] by auto  }
  2660     hence False using **[of a b] by auto  }
  2618   hence "inj x" unfolding inj_on_def by auto
  2661   hence "inj x" unfolding inj_on_def by auto
  2619   moreover
  2662   moreover
  2718 next
  2761 next
  2719   assume ?rhs thus ?lhs using bounded_closed_imp_compact by auto
  2762   assume ?rhs thus ?lhs using bounded_closed_imp_compact by auto
  2720 qed
  2763 qed
  2721 
  2764 
  2722 lemma compact_imp_bounded:
  2765 lemma compact_imp_bounded:
  2723   fixes s :: "'a::real_normed_vector set" (* TODO: generalize to metric_space *)
  2766   fixes s :: "'a::metric_space set"
  2724   shows "compact s ==> bounded s"
  2767   shows "compact s ==> bounded s"
  2725 proof -
  2768 proof -
  2726   assume "compact s"
  2769   assume "compact s"
  2727   hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
  2770   hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
  2728     by (rule compact_imp_heine_borel)
  2771     by (rule compact_imp_heine_borel)
  4184   using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
  4227   using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
  4185 
  4228 
  4186 subsection{* Preservation properties for pasted sets.                                  *}
  4229 subsection{* Preservation properties for pasted sets.                                  *}
  4187 
  4230 
  4188 lemma bounded_pastecart:
  4231 lemma bounded_pastecart:
       
  4232   fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
  4189   assumes "bounded s" "bounded t"
  4233   assumes "bounded s" "bounded t"
  4190   shows "bounded { pastecart x y | x y . (x \<in> s \<and> y \<in> t)}"
  4234   shows "bounded { pastecart x y | x y . (x \<in> s \<and> y \<in> t)}"
  4191 proof-
  4235 proof-
  4192   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
  4236   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
  4193   { fix x y assume "x\<in>s" "y\<in>t"
  4237   { fix x y assume "x\<in>s" "y\<in>t"
  4194     hence "norm x \<le> a" "norm y \<le> b" using ab by auto
  4238     hence "norm x \<le> a" "norm y \<le> b" using ab by auto
  4195     hence "norm (pastecart x y) \<le> a + b" using norm_pastecart[of x y] by auto }
  4239     hence "norm (pastecart x y) \<le> a + b" using norm_pastecart[of x y] by auto }
  4196   thus ?thesis unfolding bounded_def by auto
  4240   thus ?thesis unfolding bounded_iff by auto
  4197 qed
  4241 qed
  4198 
  4242 
  4199 lemma closed_pastecart:
  4243 lemma closed_pastecart:
  4200   fixes s :: "(real ^ 'a::finite) set" (* FIXME: generalize *)
  4244   fixes s :: "(real ^ 'a::finite) set" (* FIXME: generalize *)
  4201   assumes "closed s"  "closed t"
  4245   assumes "closed s"  "closed t"
  4299 qed
  4343 qed
  4300 
  4344 
  4301 text{* We can state this in terms of diameter of a set.                          *}
  4345 text{* We can state this in terms of diameter of a set.                          *}
  4302 
  4346 
  4303 definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
  4347 definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
       
  4348   (* TODO: generalize to class metric_space *)
  4304 
  4349 
  4305 lemma diameter_bounded:
  4350 lemma diameter_bounded:
  4306   assumes "bounded s"
  4351   assumes "bounded s"
  4307   shows "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
  4352   shows "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
  4308         "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
  4353         "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
  4309 proof-
  4354 proof-
  4310   let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
  4355   let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
  4311   obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_def] by auto
  4356   obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
  4312   { fix x y assume "x \<in> s" "y \<in> s"
  4357   { fix x y assume "x \<in> s" "y \<in> s"
  4313     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)  }
  4358     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)  }
  4314   note * = this
  4359   note * = this
  4315   { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
  4360   { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
  4316     have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
  4361     have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
  4751   { fix x::"real^'n" assume x:"\<forall>i. a $ i \<le> x $ i \<and> x $ i \<le> b $ i"
  4796   { fix x::"real^'n" assume x:"\<forall>i. a $ i \<le> x $ i \<and> x $ i \<le> b $ i"
  4752     { fix i
  4797     { fix i
  4753       have "\<bar>x$i\<bar> \<le> \<bar>a$i\<bar> + \<bar>b$i\<bar>" using x[THEN spec[where x=i]] by auto  }
  4798       have "\<bar>x$i\<bar> \<le> \<bar>a$i\<bar> + \<bar>b$i\<bar>" using x[THEN spec[where x=i]] by auto  }
  4754     hence "(\<Sum>i\<in>UNIV. \<bar>x $ i\<bar>) \<le> ?b" by(rule setsum_mono)
  4799     hence "(\<Sum>i\<in>UNIV. \<bar>x $ i\<bar>) \<le> ?b" by(rule setsum_mono)
  4755     hence "norm x \<le> ?b" using norm_le_l1[of x] by auto  }
  4800     hence "norm x \<le> ?b" using norm_le_l1[of x] by auto  }
  4756   thus ?thesis unfolding interval and bounded_def by auto
  4801   thus ?thesis unfolding interval and bounded_iff by auto
  4757 qed
  4802 qed
  4758 
  4803 
  4759 lemma bounded_interval: fixes a :: "real^'n::finite" shows
  4804 lemma bounded_interval: fixes a :: "real^'n::finite" shows
  4760  "bounded {a .. b} \<and> bounded {a<..<b}"
  4805  "bounded {a .. b} \<and> bounded {a<..<b}"
  4761   using bounded_closed_interval[of a b]
  4806   using bounded_closed_interval[of a b]
  5176 
  5221 
  5177 lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
  5222 lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
  5178   assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
  5223   assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
  5179   shows "\<exists>l. (s ---> l) sequentially"
  5224   shows "\<exists>l. (s ---> l) sequentially"
  5180 proof-
  5225 proof-
  5181   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
  5226   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
  5182   { fix m::nat
  5227   { fix m::nat
  5183     have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
  5228     have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
  5184       apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
  5229       apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
  5185   hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
  5230   hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
  5186   then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] by auto
  5231   then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] by auto