# HG changeset patch # User huffman # Date 1278346491 25200 # Node ID 6432bf0d719117a6e18983d4984c1b0ce38a1ad8 # Parent 8c6bfe10a4ae89c740a58d1c6cb7cd62762e1e6e generalize type of is_interval to class euclidean_space diff -r 8c6bfe10a4ae -r 6432bf0d7191 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jul 05 09:12:35 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Jul 05 09:14:51 2010 -0700 @@ -1940,10 +1940,15 @@ subsection {* Convexity of general and special intervals. *} +lemma convexI: (* TODO: move to Library/Convex.thy *) + assumes "\x y u v. \x \ s; y \ s; 0 \ u; 0 \ v; u + v = 1\ \ u *\<^sub>R x + v *\<^sub>R y \ s" + shows "convex s" +using assms unfolding convex_def by fast + lemma is_interval_convex: - fixes s :: "('a::ordered_euclidean_space) set" + fixes s :: "('a::euclidean_space) set" assumes "is_interval s" shows "convex s" - unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof- +proof (rule convexI) fix x y u v assume as:"x \ s" "y \ s" "0 \ u" "0 \ v" "u + v = (1::real)" hence *:"u = 1 - v" "1 - v \ 0" and **:"v = 1 - u" "1 - u \ 0" by auto { fix a b assume "\ b \ u * a + v * b" @@ -1959,7 +1964,7 @@ using as(3-) DIM_positive[where 'a='a] by(auto simp add:euclidean_simps) qed lemma is_interval_connected: - fixes s :: "('a::ordered_euclidean_space) set" + fixes s :: "('a::euclidean_space) set" shows "is_interval s \ connected s" using is_interval_convex convex_connected by auto diff -r 8c6bfe10a4ae -r 6432bf0d7191 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jul 05 09:12:35 2010 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jul 05 09:14:51 2010 -0700 @@ -5023,7 +5023,7 @@ text {* Intervals in general, including infinite and mixtures of open and closed. *} -definition "is_interval (s::('a::ordered_euclidean_space) set) \ +definition "is_interval (s::('a::euclidean_space) set) \ (\a\s. \b\s. \x. (\i x$$i \ x$$i \ b$$i) \ (b$$i \ x$$i \ x$$i \ a$$i))) \ x \ s)" lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)