# HG changeset patch # User hoelzl # Date 1383641099 -3600 # Node ID 6a967667fd45de6363df8ecb4b4717b3f9fb8b4c # Parent 71c701dc5bf95e2cf0387f309272f591a06c31e9 use INF and SUP on conditionally complete lattices in multivariate analysis diff -r 71c701dc5bf9 -r 6a967667fd45 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 05 09:44:59 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 05 09:44:59 2013 +0100 @@ -1209,7 +1209,7 @@ apply (subst inf_commute) apply (subst SUP_inf) apply (intro SUP_cong[OF refl]) - apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union) + apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union) apply (simp add: INF_def del: inf_ereal_def) done diff -r 71c701dc5bf9 -r 6a967667fd45 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:44:59 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Nov 05 09:44:59 2013 +0100 @@ -1972,22 +1972,25 @@ subsection {* Infimum Distance *} -definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \ A})" - -lemma bdd_below_infdist[intro, simp]: "bdd_below {dist x a|a. a \ A}" +definition "infdist x A = (if A = {} then 0 else INF a:A. dist x a)" + +lemma bdd_below_infdist[intro, simp]: "bdd_below (dist x`A)" by (auto intro!: zero_le_dist) -lemma infdist_notempty: "A \ {} \ infdist x A = Inf {dist x a|a. a \ A}" +lemma infdist_notempty: "A \ {} \ infdist x A = (INF a:A. dist x a)" by (simp add: infdist_def) lemma infdist_nonneg: "0 \ infdist x A" - by (auto simp add: infdist_def intro: cInf_greatest) - -lemma infdist_le: "a \ A \ d = dist x a \ infdist x A \ d" - using assms by (auto intro: cInf_lower simp add: infdist_def) + by (auto simp add: infdist_def intro: cINF_greatest) + +lemma infdist_le: "a \ A \ infdist x A \ dist x a" + by (auto intro: cINF_lower simp add: infdist_def) + +lemma infdist_le2: "a \ A \ dist x a \ d \ infdist x A \ d" + by (auto intro!: cINF_lower2 simp add: infdist_def) lemma infdist_zero[simp]: "a \ A \ infdist a A = 0" - by (auto intro!: antisym infdist_nonneg infdist_le) + by (auto intro!: antisym infdist_nonneg infdist_le2) lemma infdist_triangle: "infdist x A \ infdist y A + dist x y" proof (cases "A = {}") @@ -2006,9 +2009,8 @@ by auto show "infdist x A \ d" unfolding infdist_notempty[OF `A \ {}`] - proof (rule cInf_lower2) - show "dist x a \ {dist x a |a. a \ A}" - using `a \ A` by auto + proof (rule cINF_lower2) + show "a \ A" by fact show "dist x a \ d" unfolding d by (rule dist_triangle) qed simp @@ -2024,7 +2026,7 @@ assume inf: "\d. d \ {dist x y + dist y a |a. a \ A} \ i \ d" then have "i - dist x y \ infdist y A" unfolding infdist_notempty[OF `A \ {}`] using `a \ A` - by (intro cInf_greatest) (auto simp: field_simps) + by (intro cINF_greatest) (auto simp: field_simps) then show "i \ dist x y + infdist y A" by simp qed @@ -2063,7 +2065,7 @@ assume "\ (\y\A. dist y x < e)" then have "infdist x A \ e" using `a \ A` unfolding infdist_def - by (force simp: dist_commute intro: cInf_greatest) + by (force simp: dist_commute intro: cINF_greatest) with x `e > 0` show False by auto qed qed @@ -5701,28 +5703,27 @@ text {* We can state this in terms of diameter of a set. *} -definition "diameter s = (if s = {} then 0::real else Sup {dist x y | x y. x \ s \ y \ s})" +definition diameter :: "'a::metric_space set \ real" where + "diameter S = (if S = {} then 0 else SUP (x,y):S\S. dist x y)" lemma diameter_bounded_bound: fixes s :: "'a :: metric_space set" assumes s: "bounded s" "x \ s" "y \ s" shows "dist x y \ diameter s" proof - - let ?D = "{dist x y |x y. x \ s \ y \ s}" from s obtain z d where z: "\x. x \ s \ dist z x \ d" unfolding bounded_def by auto - have "dist x y \ Sup ?D" - proof (rule cSup_upper) - show "bdd_above ?D" - unfolding bdd_above_def - proof (safe intro!: exI) - fix a b - assume "a \ s" "b \ s" - with z[of a] z[of b] dist_triangle[of a b z] - show "dist a b \ 2 * d" - by (simp add: dist_commute) - qed - qed (insert s, auto) + have "bdd_above (split dist ` (s\s))" + proof (intro bdd_aboveI, safe) + fix a b + assume "a \ s" "b \ s" + with z[of a] z[of b] dist_triangle[of a b z] + show "dist a b \ 2 * d" + by (simp add: dist_commute) + qed + moreover have "(x,y) \ s\s" using s by auto + ultimately have "dist x y \ (SUP (x,y):s\s. dist x y)" + by (rule cSUP_upper2) simp with `x \ s` show ?thesis by (auto simp add: diameter_def) qed @@ -5733,16 +5734,12 @@ and d: "0 < d" "d < diameter s" shows "\x\s. \y\s. d < dist x y" proof (rule ccontr) - let ?D = "{dist x y |x y. x \ s \ y \ s}" assume contr: "\ ?thesis" - moreover - from d have "s \ {}" - by (auto simp: diameter_def) - then have "?D \ {}" by auto - ultimately have "Sup ?D \ d" - by (intro cSup_least) (auto simp: not_less) - with `d < diameter s` `s \ {}` show False - by (auto simp: diameter_def) + moreover have "s \ {}" + using d by (auto simp add: diameter_def) + ultimately have "diameter s \ d" + by (auto simp: not_less diameter_def intro!: cSUP_least) + with `d < diameter s` show False by auto qed lemma diameter_bounded: @@ -5765,7 +5762,7 @@ then have "diameter s \ dist x y" unfolding diameter_def apply clarsimp - apply (rule cSup_least) + apply (rule cSUP_least) apply fast+ done then show ?thesis