src/HOL/Library/Topology_Euclidean_Space.thy
 changeset 33269 3b7e2dbbd684 parent 32960 69916a850301
```     1.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
1.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
1.3 @@ -2100,59 +2100,54 @@
1.4    shows "bounded S \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
1.6
1.7 -lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
1.8 -  shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
1.9 +lemma bounded_has_Sup:
1.10 +  fixes S :: "real set"
1.11 +  assumes "bounded S" "S \<noteq> {}"
1.12 +  shows "\<forall>x\<in>S. x <= Sup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> Sup S <= b"
1.13 +proof
1.14 +  fix x assume "x\<in>S"
1.15 +  thus "x \<le> Sup S"
1.16 +    by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
1.17 +next
1.18 +  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
1.19 +    by (metis SupInf.Sup_least)
1.20 +qed
1.21 +
1.22 +lemma Sup_insert:
1.23 +  fixes S :: "real set"
1.24 +  shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
1.25 +by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal)
1.26 +
1.27 +lemma Sup_insert_finite:
1.28 +  fixes S :: "real set"
1.29 +  shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
1.30 +  apply (rule Sup_insert)
1.31 +  apply (rule finite_imp_bounded)
1.32 +  by simp
1.33 +
1.34 +lemma bounded_has_Inf:
1.35 +  fixes S :: "real set"
1.36 +  assumes "bounded S"  "S \<noteq> {}"
1.37 +  shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
1.38  proof
1.39    fix x assume "x\<in>S"
1.40    from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
1.41 -  hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
1.42 -  thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
1.43 -next
1.44 -  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> b" using assms
1.45 -  using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def]
1.46 -  apply (auto simp add: bounded_real)
1.47 -  by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def)
1.48 -qed
1.49 -
1.50 -lemma rsup_insert: assumes "bounded S"
1.51 -  shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))"
1.52 -proof(cases "S={}")
1.53 -  case True thus ?thesis using rsup_finite_in[of "{x}"] by auto
1.54 +  thus "x \<ge> Inf S" using `x\<in>S`
1.55 +    by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
1.56  next
1.57 -  let ?S = "insert x S"
1.58 -  case False
1.59 -  hence *:"\<forall>x\<in>S. x \<le> rsup S" using bounded_has_rsup(1)[of S] using assms by auto
1.60 -  hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto
1.61 -  hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto
1.62 -  moreover
1.63 -  have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto
1.64 -  { fix y assume as:"isUb UNIV (insert x S) y"
1.65 -    hence "max x (rsup S) \<le> y" unfolding isUb_def using rsup_le[OF `S\<noteq>{}`]
1.66 -      unfolding setle_def by auto  }
1.67 -  hence "max x (rsup S) <=* isUb UNIV (insert x S)" unfolding setge_def Ball_def mem_def by auto
1.68 -  hence "isLub UNIV ?S (max x (rsup S))" using ** isLubI2[of UNIV ?S "max x (rsup S)"] unfolding Collect_def by auto
1.69 -  ultimately show ?thesis using real_isLub_unique[of UNIV ?S] using `S\<noteq>{}` by auto
1.70 -qed
1.71 -
1.72 -lemma sup_insert_finite: "finite S \<Longrightarrow> rsup(insert x S) = (if S = {} then x else max x (rsup S))"
1.73 -  apply (rule rsup_insert)
1.74 -  apply (rule finite_imp_bounded)
1.75 -  by simp
1.76 -
1.77 -lemma bounded_has_rinf:
1.78 -  assumes "bounded S"  "S \<noteq> {}"
1.79 -  shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
1.80 -proof
1.81 -  fix x assume "x\<in>S"
1.82 -  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
1.83 -  hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
1.84 -  thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
1.85 -next
1.86 -  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> b" using assms
1.87 -  using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def]
1.88 -  apply (auto simp add: bounded_real)
1.89 -  by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def)
1.90 -qed
1.91 +  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
1.92 +    by (metis SupInf.Inf_greatest)
1.93 +qed
1.94 +
1.95 +lemma Inf_insert:
1.96 +  fixes S :: "real set"
1.97 +  shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
1.98 +by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
1.99 +lemma Inf_insert_finite:
1.100 +  fixes S :: "real set"
1.101 +  shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
1.102 +  by (rule Inf_insert, rule finite_imp_bounded, simp)
1.103 +
1.104
1.105  (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
1.106  lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
1.107 @@ -2161,29 +2156,6 @@
1.108    apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
1.109    done
1.110
1.111 -lemma rinf_insert: assumes "bounded S"
1.112 -  shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs")
1.113 -proof(cases "S={}")
1.114 -  case True thus ?thesis using rinf_finite_in[of "{x}"] by auto
1.115 -next
1.116 -  let ?S = "insert x S"
1.117 -  case False
1.118 -  hence *:"\<forall>x\<in>S. x \<ge> rinf S" using bounded_has_rinf(1)[of S] using assms by auto
1.119 -  hence "min x (rinf S) <=* insert x S" unfolding setge_def by auto
1.120 -  hence "isGlb UNIV ?S (rinf ?S)" using rinf[of ?S] by auto
1.121 -  moreover
1.122 -  have **:"isLb UNIV ?S (min x (rinf S))" unfolding isLb_def setge_def using * by auto
1.123 -  { fix y assume as:"isLb UNIV (insert x S) y"
1.124 -    hence "min x (rinf S) \<ge> y" unfolding isLb_def using rinf_ge[OF `S\<noteq>{}`]
1.125 -      unfolding setge_def by auto  }
1.126 -  hence "isLb UNIV (insert x S) *<= min x (rinf S)" unfolding setle_def Ball_def mem_def by auto
1.127 -  hence "isGlb UNIV ?S (min x (rinf S))" using ** isGlbI2[of UNIV ?S "min x (rinf S)"] unfolding Collect_def by auto
1.128 -  ultimately show ?thesis using real_isGlb_unique[of UNIV ?S] using `S\<noteq>{}` by auto
1.129 -qed
1.130 -
1.131 -lemma inf_insert_finite: "finite S ==> rinf(insert x S) = (if S = {} then x else min x (rinf S))"
1.132 -  by (rule rinf_insert, rule finite_imp_bounded, simp)
1.133 -
1.134  subsection{* Compactness (the definition is the one based on convegent subsequences). *}
1.135
1.136  definition
1.137 @@ -4120,30 +4092,35 @@
1.138    shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
1.139  proof-
1.140    from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
1.141 -  { fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> rsup s - x' < e"
1.142 -    have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto
1.143 -    moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
1.144 -    ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto  }
1.145 -  thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]]
1.146 -    apply(rule_tac x="rsup s" in bexI) by auto
1.147 -qed
1.148 +  { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e"
1.149 +    have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
1.150 +    moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
1.151 +    ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto  }
1.152 +  thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
1.153 +    apply(rule_tac x="Sup s" in bexI) by auto
1.154 +qed
1.155 +
1.156 +lemma Inf:
1.157 +  fixes S :: "real set"
1.158 +  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
1.159 +by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def)
1.160
1.161  lemma compact_attains_inf:
1.162    fixes s :: "real set"
1.163    assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
1.164  proof-
1.165    from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
1.166 -  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s"  "rinf s \<notin> s"  "0 < e"
1.167 -      "\<forall>x'\<in>s. x' = rinf s \<or> \<not> abs (x' - rinf s) < e"
1.168 -    have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto
1.169 +  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s"  "Inf s \<notin> s"  "0 < e"
1.170 +      "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
1.171 +    have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
1.172      moreover
1.173      { fix x assume "x \<in> s"
1.174 -      hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto
1.175 -      have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
1.176 -    hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto
1.177 -    ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto  }
1.178 -  thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]]
1.179 -    apply(rule_tac x="rinf s" in bexI) by auto
1.180 +      hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
1.181 +      have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
1.182 +    hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
1.183 +    ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto  }
1.184 +  thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
1.185 +    apply(rule_tac x="Inf s" in bexI) by auto
1.186  qed
1.187
1.188  lemma continuous_attains_sup:
1.189 @@ -4413,7 +4390,7 @@
1.190
1.191  text{* We can state this in terms of diameter of a set.                          *}
1.192
1.193 -definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
1.194 +definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
1.195    (* TODO: generalize to class metric_space *)
1.196
1.197  lemma diameter_bounded:
1.198 @@ -4427,12 +4404,22 @@
1.199      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)  }
1.200    note * = this
1.201    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
1.202 -    have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
1.203 +    have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
1.204 +      apply auto    (*FIXME: something horrible has happened here!*)
1.205 +      apply atomize
1.206 +      apply safe
1.207 +      apply metis +
1.208 +      done
1.209      have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s` isLubD1[OF lub] unfolding setle_def by auto  }
1.210    moreover
1.211    { fix d::real assume "d>0" "d < diameter s"
1.212      hence "s\<noteq>{}" unfolding diameter_def by auto
1.213 -    hence lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] unfolding setle_def by auto
1.214 +    hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def
1.215 +      apply auto    (*FIXME: something horrible has happened here!*)
1.216 +      apply atomize
1.217 +      apply safe
1.218 +      apply metis +
1.219 +      done
1.220      have "\<exists>d' \<in> ?D. d' > d"
1.221      proof(rule ccontr)
1.222        assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
1.223 @@ -4448,6 +4435,7 @@
1.224  lemma diameter_bounded_bound:
1.225   "bounded s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s ==> norm(x - y) \<le> diameter s"
1.226    using diameter_bounded by blast
1.227 +atp_minimize [atp=remote_vampire] Collect_def Max_ge add_increasing2 add_le_cancel_left diameter_def_raw equation_minus_iff finite finite_imageI norm_imp_pos_and_ge rangeI
1.228
1.229  lemma diameter_compact_attained:
1.230    fixes s :: "'a::real_normed_vector set"
1.231 @@ -4456,8 +4444,8 @@
1.232  proof-
1.233    have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
1.234    then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
1.235 -  hence "diameter s \<le> norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}" "norm (x - y)"]
1.236 -    unfolding setle_def and diameter_def by auto
1.237 +  hence "diameter s \<le> norm (x - y)"
1.238 +    by (force simp add: diameter_def intro!: Sup_least)
1.239    thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto
1.240  qed
1.241
```