src/HOL/Library/Topology_Euclidean_Space.thy
 changeset 31533 2cce9283ba72 parent 31532 43e8d4bfde26 child 31534 0de814d2ff95
equal 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`
`  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`