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)
```