src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 51475 ebf9d4fd00ba parent 51473 1210309fddab child 51478 270b21f3ae0a
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -1401,7 +1401,7 @@
1.4      show "(\<lambda>n. f (S n)) ----> Inf (f ` ({x<..} \<inter> I))"
1.5      proof (rule LIMSEQ_I, rule ccontr)
1.6        fix r :: real assume "0 < r"
1.7 -      with Inf_close[of "f ` ({x<..} \<inter> I)" r]
1.8 +      with cInf_close[of "f ` ({x<..} \<inter> I)" r]
1.9        obtain y where y: "x < y" "y \<in> I" "f y < Inf (f ` ({x <..} \<inter> I)) + r" by auto
1.10        from `x < y` have "0 < y - x" by auto
1.11        from S(2)[THEN LIMSEQ_D, OF this]
1.12 @@ -1409,7 +1409,7 @@
1.13
1.14        assume "\<not> (\<exists>N. \<forall>n\<ge>N. norm (f (S n) - Inf (f ` ({x<..} \<inter> I))) < r)"
1.15        moreover have "\<And>n. Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
1.16 -        using S bnd by (intro Inf_lower[where z=K]) auto
1.17 +        using S bnd by (intro cInf_lower[where z=K]) auto
1.18        ultimately obtain n where n: "N \<le> n" "r + Inf (f ` ({x<..} \<inter> I)) \<le> f (S n)"
1.19          by (auto simp: not_less field_simps)
1.20        with N[OF n(1)] mono[OF _ `y \<in> I`, of "S n"] S(1)[THEN spec, of n] y
1.21 @@ -1727,11 +1727,11 @@
1.22    unfolding closure_approachable
1.23  proof safe
1.24    have *: "\<forall>x\<in>S. Inf S \<le> x"
1.25 -    using Inf_lower_EX[of _ S] assms by metis
1.26 +    using cInf_lower_EX[of _ S] assms by metis
1.27
1.28    fix e :: real assume "0 < e"
1.29    then obtain x where x: "x \<in> S" "x < Inf S + e"
1.30 -    using Inf_close `S \<noteq> {}` by auto
1.31 +    using cInf_close `S \<noteq> {}` by auto
1.32    moreover then have "x > Inf S - e" using * by auto
1.33    ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
1.34    then show "\<exists>x\<in>S. dist x (Inf S) < e"
1.35 @@ -1785,13 +1785,13 @@
1.36
1.37  lemma infdist_nonneg:
1.38    shows "0 \<le> infdist x A"
1.39 -  using assms by (auto simp add: infdist_def)
1.40 +  using assms by (auto simp add: infdist_def intro: cInf_greatest)
1.41
1.42  lemma infdist_le:
1.43    assumes "a \<in> A"
1.44    assumes "d = dist x a"
1.45    shows "infdist x A \<le> d"
1.46 -  using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
1.47 +  using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
1.48
1.49  lemma infdist_zero[simp]:
1.50    assumes "a \<in> A" shows "infdist a A = 0"
1.51 @@ -1807,13 +1807,13 @@
1.52  next
1.53    assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
1.54    have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
1.55 -  proof
1.56 +  proof (rule cInf_greatest)
1.57      from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
1.58      fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
1.59      then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
1.60      show "infdist x A \<le> d"
1.61        unfolding infdist_notempty[OF `A \<noteq> {}`]
1.62 -    proof (rule Inf_lower2)
1.63 +    proof (rule cInf_lower2)
1.64        show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
1.65        show "dist x a \<le> d" unfolding d by (rule dist_triangle)
1.66        fix d assume "d \<in> {dist x a |a. a \<in> A}"
1.67 @@ -1822,20 +1822,19 @@
1.68      qed
1.69    qed
1.70    also have "\<dots> = dist x y + infdist y A"
1.71 -  proof (rule Inf_eq, safe)
1.72 +  proof (rule cInf_eq, safe)
1.73      fix a assume "a \<in> A"
1.74      thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
1.75    next
1.76      fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
1.77      hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
1.78 -      by (intro Inf_greatest) (auto simp: field_simps)
1.79 +      by (intro cInf_greatest) (auto simp: field_simps)
1.80      thus "i \<le> dist x y + infdist y A" by simp
1.81    qed
1.82    finally show ?thesis by simp
1.83  qed
1.84
1.85 -lemma
1.86 -  in_closure_iff_infdist_zero:
1.87 +lemma in_closure_iff_infdist_zero:
1.88    assumes "A \<noteq> {}"
1.89    shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
1.90  proof
1.91 @@ -1859,13 +1858,12 @@
1.92      assume "\<not> (\<exists>y\<in>A. dist y x < e)"
1.93      hence "infdist x A \<ge> e" using `a \<in> A`
1.94        unfolding infdist_def
1.95 -      by (force simp: dist_commute)
1.96 +      by (force simp: dist_commute intro: cInf_greatest)
1.97      with x `0 < e` show False by auto
1.98    qed
1.99  qed
1.100
1.101 -lemma
1.102 -  in_closed_iff_infdist_zero:
1.103 +lemma in_closed_iff_infdist_zero:
1.104    assumes "closed A" "A \<noteq> {}"
1.105    shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
1.106  proof -
1.107 @@ -2326,16 +2324,19 @@
1.108  proof
1.109    fix x assume "x\<in>S"
1.110    thus "x \<le> Sup S"
1.111 -    by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
1.112 +    by (metis cSup_upper abs_le_D1 assms(1) bounded_real)
1.113  next
1.114    show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
1.115 -    by (metis SupInf.Sup_least)
1.116 +    by (metis cSup_least)
1.117  qed
1.118
1.119  lemma Sup_insert:
1.120    fixes S :: "real set"
1.121    shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
1.122 -by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal)
1.123 +  apply (subst cSup_insert_If)
1.124 +  apply (rule bounded_has_Sup(1)[of S, rule_format])
1.125 +  apply (auto simp: sup_max)
1.126 +  done
1.127
1.128  lemma Sup_insert_finite:
1.129    fixes S :: "real set"
1.130 @@ -2352,16 +2353,19 @@
1.131    fix x assume "x\<in>S"
1.132    from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
1.133    thus "x \<ge> Inf S" using `x\<in>S`
1.134 -    by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
1.135 +    by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
1.136  next
1.137    show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
1.138 -    by (metis SupInf.Inf_greatest)
1.139 +    by (metis cInf_greatest)
1.140  qed
1.141
1.142  lemma Inf_insert:
1.143    fixes S :: "real set"
1.144    shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
1.145 -by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
1.146 +  apply (subst cInf_insert_if)
1.147 +  apply (rule bounded_has_Inf(1)[of S, rule_format])
1.148 +  apply (auto simp: inf_min)
1.149 +  done
1.150
1.151  lemma Inf_insert_finite:
1.152    fixes S :: "real set"
1.153 @@ -3125,7 +3129,7 @@
1.154
1.155  lemma cauchy_def:
1.156    "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
1.157 -unfolding Cauchy_def by blast
1.158 +unfolding Cauchy_def by metis
1.159
1.160  fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
1.161    "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
1.162 @@ -5197,7 +5201,7 @@
1.163    from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
1.164      unfolding bounded_def by auto
1.165    have "dist x y \<le> Sup ?D"
1.166 -  proof (rule Sup_upper, safe)
1.167 +  proof (rule cSup_upper, safe)
1.168      fix a b assume "a \<in> s" "b \<in> s"
1.169      with z[of a] z[of b] dist_triangle[of a b z]
1.170      show "dist a b \<le> 2 * d"
1.171 @@ -5219,7 +5223,7 @@
1.172      by (auto simp: diameter_def)
1.173    then have "?D \<noteq> {}" by auto
1.174    ultimately have "Sup ?D \<le> d"
1.175 -    by (intro Sup_least) (auto simp: not_less)
1.176 +    by (intro cSup_least) (auto simp: not_less)
1.177    with `d < diameter s` `s \<noteq> {}` show False
1.178      by (auto simp: diameter_def)
1.179  qed
1.180 @@ -5239,7 +5243,7 @@
1.181    then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
1.182      using compact_sup_maxdistance[OF assms] by auto
1.183    hence "diameter s \<le> dist x y"
1.184 -    unfolding diameter_def by clarsimp (rule Sup_least, fast+)
1.185 +    unfolding diameter_def by clarsimp (rule cSup_least, fast+)
1.186    thus ?thesis
1.187      by (metis b diameter_bounded_bound order_antisym xys)
1.188  qed
1.189 @@ -6675,5 +6679,4 @@
1.190
1.191  declare tendsto_const [intro] (* FIXME: move *)
1.192
1.193 -
1.194  end
```