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.5    by (simp add: bounded_iff)
     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