src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 54258 adfc759263ab
parent 54230 b1d955791529
child 54259 71c701dc5bf9
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:57 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:44:58 2013 +0100
     1.3 @@ -1909,17 +1909,17 @@
     1.4  
     1.5  lemma closure_contains_Inf:
     1.6    fixes S :: "real set"
     1.7 -  assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
     1.8 +  assumes "S \<noteq> {}" "bdd_below S"
     1.9    shows "Inf S \<in> closure S"
    1.10  proof -
    1.11    have *: "\<forall>x\<in>S. Inf S \<le> x"
    1.12 -    using cInf_lower_EX[of _ S] assms by metis
    1.13 +    using cInf_lower[of _ S] assms by metis
    1.14    {
    1.15      fix e :: real
    1.16      assume "e > 0"
    1.17      then have "Inf S < Inf S + e" by simp
    1.18      with assms obtain x where "x \<in> S" "x < Inf S + e"
    1.19 -      by (subst (asm) cInf_less_iff[of _ B]) auto
    1.20 +      by (subst (asm) cInf_less_iff) auto
    1.21      with * have "\<exists>x\<in>S. dist x (Inf S) < e"
    1.22        by (intro bexI[of _ x]) (auto simp add: dist_real_def)
    1.23    }
    1.24 @@ -1928,12 +1928,9 @@
    1.25  
    1.26  lemma closed_contains_Inf:
    1.27    fixes S :: "real set"
    1.28 -  assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
    1.29 -    and "closed S"
    1.30 -  shows "Inf S \<in> S"
    1.31 +  shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
    1.32    by (metis closure_contains_Inf closure_closed assms)
    1.33  
    1.34 -
    1.35  lemma not_trivial_limit_within_ball:
    1.36    "\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
    1.37    (is "?lhs = ?rhs")
    1.38 @@ -1977,27 +1974,20 @@
    1.39  
    1.40  definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
    1.41  
    1.42 +lemma bdd_below_infdist[intro, simp]: "bdd_below {dist x a|a. a \<in> A}"
    1.43 +  by (auto intro!: zero_le_dist)
    1.44 +
    1.45  lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
    1.46    by (simp add: infdist_def)
    1.47  
    1.48  lemma infdist_nonneg: "0 \<le> infdist x A"
    1.49    by (auto simp add: infdist_def intro: cInf_greatest)
    1.50  
    1.51 -lemma infdist_le:
    1.52 -  assumes "a \<in> A"
    1.53 -    and "d = dist x a"
    1.54 -  shows "infdist x A \<le> d"
    1.55 -  using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
    1.56 -
    1.57 -lemma infdist_zero[simp]:
    1.58 -  assumes "a \<in> A"
    1.59 -  shows "infdist a A = 0"
    1.60 -proof -
    1.61 -  from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0"
    1.62 -    by auto
    1.63 -  with infdist_nonneg[of a A] assms show "infdist a A = 0"
    1.64 -    by auto
    1.65 -qed
    1.66 +lemma infdist_le: "a \<in> A \<Longrightarrow> d = dist x a \<Longrightarrow> infdist x A \<le> d"
    1.67 +  using assms by (auto intro: cInf_lower simp add: infdist_def)
    1.68 +
    1.69 +lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
    1.70 +  by (auto intro!: antisym infdist_nonneg infdist_le)
    1.71  
    1.72  lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
    1.73  proof (cases "A = {}")
    1.74 @@ -2021,13 +2011,7 @@
    1.75          using `a \<in> A` by auto
    1.76        show "dist x a \<le> d"
    1.77          unfolding d by (rule dist_triangle)
    1.78 -      fix d
    1.79 -      assume "d \<in> {dist x a |a. a \<in> A}"
    1.80 -      then obtain a where "a \<in> A" "d = dist x a"
    1.81 -        by auto
    1.82 -      then show "infdist x A \<le> d"
    1.83 -        by (rule infdist_le)
    1.84 -    qed
    1.85 +    qed simp
    1.86    qed
    1.87    also have "\<dots> = dist x y + infdist y A"
    1.88    proof (rule cInf_eq, safe)
    1.89 @@ -2651,11 +2635,19 @@
    1.90  
    1.91  text{* Some theorems on sups and infs using the notion "bounded". *}
    1.92  
    1.93 -lemma bounded_real:
    1.94 -  fixes S :: "real set"
    1.95 -  shows "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x \<le> a)"
    1.96 +lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
    1.97    by (simp add: bounded_iff)
    1.98  
    1.99 +lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: real set)"
   1.100 +  by (auto simp: bounded_def bdd_above_def dist_real_def)
   1.101 +     (metis abs_le_D1 abs_minus_commute diff_le_eq)
   1.102 +
   1.103 +lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)"
   1.104 +  by (auto simp: bounded_def bdd_below_def dist_real_def)
   1.105 +     (metis abs_le_D1 add_commute diff_le_eq)
   1.106 +
   1.107 +(* TODO: remove the following lemmas about Inf and Sup, is now in conditionally complete lattice *)
   1.108 +
   1.109  lemma bounded_has_Sup:
   1.110    fixes S :: "real set"
   1.111    assumes "bounded S"
   1.112 @@ -2663,22 +2655,14 @@
   1.113    shows "\<forall>x\<in>S. x \<le> Sup S"
   1.114      and "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
   1.115  proof
   1.116 -  fix x
   1.117 -  assume "x\<in>S"
   1.118 -  then show "x \<le> Sup S"
   1.119 -    by (metis cSup_upper abs_le_D1 assms(1) bounded_real)
   1.120 -next
   1.121    show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b"
   1.122      using assms by (metis cSup_least)
   1.123 -qed
   1.124 +qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
   1.125  
   1.126  lemma Sup_insert:
   1.127    fixes S :: "real set"
   1.128    shows "bounded S \<Longrightarrow> Sup (insert x S) = (if S = {} then x else max x (Sup S))"
   1.129 -  apply (subst cSup_insert_If)
   1.130 -  apply (rule bounded_has_Sup(1)[of S, rule_format])
   1.131 -  apply (auto simp: sup_max)
   1.132 -  done
   1.133 +  by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
   1.134  
   1.135  lemma Sup_insert_finite:
   1.136    fixes S :: "real set"
   1.137 @@ -2695,24 +2679,14 @@
   1.138    shows "\<forall>x\<in>S. x \<ge> Inf S"
   1.139      and "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
   1.140  proof
   1.141 -  fix x
   1.142 -  assume "x \<in> S"
   1.143 -  from assms(1) obtain a where a: "\<forall>x\<in>S. \<bar>x\<bar> \<le> a"
   1.144 -    unfolding bounded_real by auto
   1.145 -  then show "x \<ge> Inf S" using `x \<in> S`
   1.146 -    by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
   1.147 -next
   1.148    show "\<forall>b. (\<forall>x\<in>S. x \<ge> b) \<longrightarrow> Inf S \<ge> b"
   1.149      using assms by (metis cInf_greatest)
   1.150 -qed
   1.151 +qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
   1.152  
   1.153  lemma Inf_insert:
   1.154    fixes S :: "real set"
   1.155    shows "bounded S \<Longrightarrow> Inf (insert x S) = (if S = {} then x else min x (Inf S))"
   1.156 -  apply (subst cInf_insert_if)
   1.157 -  apply (rule bounded_has_Inf(1)[of S, rule_format])
   1.158 -  apply (auto simp: inf_min)
   1.159 -  done
   1.160 +  by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_if)
   1.161  
   1.162  lemma Inf_insert_finite:
   1.163    fixes S :: "real set"
   1.164 @@ -5738,12 +5712,16 @@
   1.165    from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
   1.166      unfolding bounded_def by auto
   1.167    have "dist x y \<le> Sup ?D"
   1.168 -  proof (rule cSup_upper, safe)
   1.169 -    fix a b
   1.170 -    assume "a \<in> s" "b \<in> s"
   1.171 -    with z[of a] z[of b] dist_triangle[of a b z]
   1.172 -    show "dist a b \<le> 2 * d"
   1.173 -      by (simp add: dist_commute)
   1.174 +  proof (rule cSup_upper)
   1.175 +    show "bdd_above ?D"
   1.176 +      unfolding bdd_above_def
   1.177 +    proof (safe intro!: exI)
   1.178 +      fix a b
   1.179 +      assume "a \<in> s" "b \<in> s"
   1.180 +      with z[of a] z[of b] dist_triangle[of a b z]
   1.181 +      show "dist a b \<le> 2 * d"
   1.182 +        by (simp add: dist_commute)
   1.183 +    qed
   1.184    qed (insert s, auto)
   1.185    with `x \<in> s` show ?thesis
   1.186      by (auto simp add: diameter_def)