# 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 "\<And>x y u v. \<lbrakk>x \<in> s; y \<in> s; 0 \<le> u; 0 \<le> v; u + v = 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> 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 \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
   hence *:"u = 1 - v" "1 - v \<ge> 0" and **:"v = 1 - u" "1 - u \<ge> 0" by auto
   { fix a b assume "\<not> b \<le> 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 \<Longrightarrow> 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) \<longleftrightarrow>
+definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i<DIM('a). ((a$$i \<le> x$$i \<and> x$$i \<le> b$$i) \<or> (b$$i \<le> x$$i \<and> x$$i \<le> a$$i))) \<longrightarrow> x \<in> s)"
 
 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)