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