1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:59 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:59 2013 +0100
     1.3 @@ -1209,7 +1209,7 @@
     1.4    apply (subst inf_commute)
     1.5    apply (subst SUP_inf)
     1.6    apply (intro SUP_cong[OF refl])
     1.7 -  apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
     1.8 +  apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
     1.9    apply (simp add: INF_def del: inf_ereal_def)
    1.10    done
    1.11  

     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:59 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:59 2013 +0100
     2.3 @@ -1972,22 +1972,25 @@
     2.4  
     2.5  subsection {* Infimum Distance *}
     2.6  
     2.7 -definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
     2.8 -
     2.9 -lemma bdd_below_infdist[intro, simp]: "bdd_below {dist x a|a. a \<in> A}"
    2.10 +definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
    2.11 +
    2.12 +lemma bdd_below_infdist[intro, simp]: "bdd_below (dist x`A)"
    2.13    by (auto intro!: zero_le_dist)
    2.14  
    2.15 -lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
    2.16 +lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"
    2.17    by (simp add: infdist_def)
    2.18  
    2.19  lemma infdist_nonneg: "0 \<le> infdist x A"
    2.20 -  by (auto simp add: infdist_def intro: cInf_greatest)
    2.21 -
    2.22 -lemma infdist_le: "a \<in> A \<Longrightarrow> d = dist x a \<Longrightarrow> infdist x A \<le> d"
    2.23 -  using assms by (auto intro: cInf_lower simp add: infdist_def)
    2.24 +  by (auto simp add: infdist_def intro: cINF_greatest)
    2.25 +
    2.26 +lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
    2.27 +  by (auto intro: cINF_lower simp add: infdist_def)
    2.28 +
    2.29 +lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
    2.30 +  by (auto intro!: cINF_lower2 simp add: infdist_def)
    2.31  
    2.32  lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
    2.33 -  by (auto intro!: antisym infdist_nonneg infdist_le)
    2.34 +  by (auto intro!: antisym infdist_nonneg infdist_le2)
    2.35  
    2.36  lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
    2.37  proof (cases "A = {}")
    2.38 @@ -2006,9 +2009,8 @@
    2.39        by auto
    2.40      show "infdist x A \<le> d"
    2.41        unfolding infdist_notempty[OF `A \<noteq> {}`]
    2.42 -    proof (rule cInf_lower2)
    2.43 -      show "dist x a \<in> {dist x a |a. a \<in> A}"
    2.44 -        using `a \<in> A` by auto
    2.45 +    proof (rule cINF_lower2)
    2.46 +      show "a \<in> A" by fact
    2.47        show "dist x a \<le> d"
    2.48          unfolding d by (rule dist_triangle)
    2.49      qed simp
    2.50 @@ -2024,7 +2026,7 @@
    2.51      assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
    2.52      then have "i - dist x y \<le> infdist y A"
    2.53        unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
    2.54 -      by (intro cInf_greatest) (auto simp: field_simps)
    2.55 +      by (intro cINF_greatest) (auto simp: field_simps)
    2.56      then show "i \<le> dist x y + infdist y A"
    2.57        by simp
    2.58    qed
    2.59 @@ -2063,7 +2065,7 @@
    2.60      assume "\<not> (\<exists>y\<in>A. dist y x < e)"
    2.61      then have "infdist x A \<ge> e" using `a \<in> A`
    2.62        unfolding infdist_def
    2.63 -      by (force simp: dist_commute intro: cInf_greatest)
    2.64 +      by (force simp: dist_commute intro: cINF_greatest)
    2.65      with x `e > 0` show False by auto
    2.66    qed
    2.67  qed
    2.68 @@ -5701,28 +5703,27 @@
    2.69  
    2.70  text {* We can state this in terms of diameter of a set. *}
    2.71  
    2.72 -definition "diameter s = (if s = {} then 0::real else Sup {dist x y | x y. x \<in> s \<and> y \<in> s})"
    2.73 +definition diameter :: "'a::metric_space set \<Rightarrow> real" where
    2.74 +  "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
    2.75  
    2.76  lemma diameter_bounded_bound:
    2.77    fixes s :: "'a :: metric_space set"
    2.78    assumes s: "bounded s" "x \<in> s" "y \<in> s"
    2.79    shows "dist x y \<le> diameter s"
    2.80  proof -
    2.81 -  let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
    2.82    from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
    2.83      unfolding bounded_def by auto
    2.84 -  have "dist x y \<le> Sup ?D"
    2.85 -  proof (rule cSup_upper)
    2.86 -    show "bdd_above ?D"
    2.87 -      unfolding bdd_above_def
    2.88 -    proof (safe intro!: exI)
    2.89 -      fix a b
    2.90 -      assume "a \<in> s" "b \<in> s"
    2.91 -      with z[of a] z[of b] dist_triangle[of a b z]
    2.92 -      show "dist a b \<le> 2 * d"
    2.93 -        by (simp add: dist_commute)
    2.94 -    qed
    2.95 -  qed (insert s, auto)
    2.96 +  have "bdd_above (split dist ` (s\<times>s))"
    2.97 +  proof (intro bdd_aboveI, safe)
    2.98 +    fix a b
    2.99 +    assume "a \<in> s" "b \<in> s"
   2.100 +    with z[of a] z[of b] dist_triangle[of a b z]
   2.101 +    show "dist a b \<le> 2 * d"
   2.102 +      by (simp add: dist_commute)
   2.103 +  qed
   2.104 +  moreover have "(x,y) \<in> s\<times>s" using s by auto
   2.105 +  ultimately have "dist x y \<le> (SUP (x,y):s\<times>s. dist x y)"
   2.106 +    by (rule cSUP_upper2) simp
   2.107    with `x \<in> s` show ?thesis
   2.108      by (auto simp add: diameter_def)
   2.109  qed
   2.110 @@ -5733,16 +5734,12 @@
   2.111      and d: "0 < d" "d < diameter s"
   2.112    shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
   2.113  proof (rule ccontr)
   2.114 -  let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
   2.115    assume contr: "\<not> ?thesis"
   2.116 -  moreover
   2.117 -  from d have "s \<noteq> {}"
   2.118 -    by (auto simp: diameter_def)
   2.119 -  then have "?D \<noteq> {}" by auto
   2.120 -  ultimately have "Sup ?D \<le> d"
   2.121 -    by (intro cSup_least) (auto simp: not_less)
   2.122 -  with `d < diameter s` `s \<noteq> {}` show False
   2.123 -    by (auto simp: diameter_def)
   2.124 +  moreover have "s \<noteq> {}"
   2.125 +    using d by (auto simp add: diameter_def)
   2.126 +  ultimately have "diameter s \<le> d"
   2.127 +    by (auto simp: not_less diameter_def intro!: cSUP_least)
   2.128 +  with `d < diameter s` show False by auto
   2.129  qed
   2.130  
   2.131  lemma diameter_bounded:
   2.132 @@ -5765,7 +5762,7 @@
   2.133    then have "diameter s \<le> dist x y"
   2.134      unfolding diameter_def
   2.135      apply clarsimp
   2.136 -    apply (rule cSup_least)
   2.137 +    apply (rule cSUP_least)
   2.138      apply fast+
   2.139      done
   2.140    then show ?thesis