1.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 05 09:12:35 2010 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jul 05 09:14:51 2010 -0700
     1.3 @@ -1940,10 +1940,15 @@
     1.4  
     1.5  subsection {* Convexity of general and special intervals. *}
     1.6  
     1.7 +lemma convexI: (* TODO: move to Library/Convex.thy *)
     1.8 +  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"
     1.9 +  shows "convex s"
    1.10 +using assms unfolding convex_def by fast
    1.11 +
    1.12  lemma is_interval_convex:
    1.13 -  fixes s :: "('a::ordered_euclidean_space) set"
    1.14 +  fixes s :: "('a::euclidean_space) set"
    1.15    assumes "is_interval s" shows "convex s"
    1.16 -  unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
    1.17 +proof (rule convexI)
    1.18    fix x y u v assume as:"x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
    1.19    hence *:"u = 1 - v" "1 - v \<ge> 0" and **:"v = 1 - u" "1 - u \<ge> 0" by auto
    1.20    { fix a b assume "\<not> b \<le> u * a + v * b"
    1.21 @@ -1959,7 +1964,7 @@
    1.22      using as(3-) DIM_positive[where 'a='a] by(auto simp add:euclidean_simps) qed
    1.23  
    1.24  lemma is_interval_connected:
    1.25 -  fixes s :: "('a::ordered_euclidean_space) set"
    1.26 +  fixes s :: "('a::euclidean_space) set"
    1.27    shows "is_interval s \<Longrightarrow> connected s"
    1.28    using is_interval_convex convex_connected by auto
    1.29  

     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jul 05 09:12:35 2010 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jul 05 09:14:51 2010 -0700
     2.3 @@ -5023,7 +5023,7 @@
     2.4  
     2.5  text {* Intervals in general, including infinite and mixtures of open and closed. *}
     2.6  
     2.7 -definition "is_interval (s::('a::ordered_euclidean_space) set) \<longleftrightarrow>
     2.8 +definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
     2.9    (\<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)"
    2.10  
    2.11  lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)