1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 17 15:50:56 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jan 15 19:28:48 2013 -0800
     1.3 @@ -2152,7 +2152,9 @@
     1.4    unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
     1.5    using assms by auto
     1.6  
     1.7 -lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
     1.8 +lemma bounded_empty [simp]: "bounded {}"
     1.9 +  by (simp add: bounded_def)
    1.10 +
    1.11  lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
    1.12    by (metis bounded_def subset_eq)
    1.13  
    1.14 @@ -2188,17 +2190,6 @@
    1.15  lemma bounded_ball[simp,intro]: "bounded(ball x e)"
    1.16    by (metis ball_subset_cball bounded_cball bounded_subset)
    1.17  
    1.18 -lemma finite_imp_bounded[intro]:
    1.19 -  fixes S :: "'a::metric_space set" assumes "finite S" shows "bounded S"
    1.20 -proof-
    1.21 -  { fix a and F :: "'a set" assume as:"bounded F"
    1.22 -    then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
    1.23 -    hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
    1.24 -    hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
    1.25 -  }
    1.26 -  thus ?thesis using finite_induct[of S bounded]  using bounded_empty assms by auto
    1.27 -qed
    1.28 -
    1.29  lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
    1.30    apply (auto simp add: bounded_def)
    1.31    apply (rename_tac x y r s)
    1.32 @@ -2214,6 +2205,16 @@
    1.33  lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
    1.34    by (induct rule: finite_induct[of F], auto)
    1.35  
    1.36 +lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"
    1.37 +proof -
    1.38 +  have "\<forall>y\<in>{x}. dist x y \<le> 0" by simp
    1.39 +  hence "bounded {x}" unfolding bounded_def by fast
    1.40 +  thus ?thesis by (metis insert_is_Un bounded_Un)
    1.41 +qed
    1.42 +
    1.43 +lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
    1.44 +  by (induct set: finite, simp_all)
    1.45 +
    1.46  lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
    1.47    apply (simp add: bounded_iff)
    1.48    apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
    1.49 @@ -2226,9 +2227,6 @@
    1.50  apply (metis Diff_subset bounded_subset)
    1.51  done
    1.52  
    1.53 -lemma bounded_insert[intro]:"bounded(insert x S) \<longleftrightarrow> bounded S"
    1.54 -  by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI)
    1.55 -
    1.56  lemma not_bounded_UNIV[simp, intro]:
    1.57    "\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
    1.58  proof(auto simp add: bounded_pos not_le)
    1.59 @@ -5063,14 +5061,14 @@
    1.60  qed
    1.61  
    1.62  lemma continuous_attains_sup:
    1.63 -  fixes f :: "'a::metric_space \<Rightarrow> real"
    1.64 +  fixes f :: "'a::topological_space \<Rightarrow> real"
    1.65    shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
    1.66          ==> (\<exists>x \<in> s. \<forall>y \<in> s.  f y \<le> f x)"
    1.67    using compact_attains_sup[of "f ` s"]
    1.68    using compact_continuous_image[of s f] by auto
    1.69  
    1.70  lemma continuous_attains_inf:
    1.71 -  fixes f :: "'a::metric_space \<Rightarrow> real"
    1.72 +  fixes f :: "'a::topological_space \<Rightarrow> real"
    1.73    shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
    1.74          \<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
    1.75    using compact_attains_inf[of "f ` s"]