removed dependencies on theory Ordered_Euclidean_Space
authorimmler
Tue Mar 18 10:12:58 2014 +0100 (2014-03-18)
changeset 56189c4daa97ac57a
parent 56188 0268784f60da
child 56190 f0d2609c4cdc
removed dependencies on theory Ordered_Euclidean_Space
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 18 10:12:57 2014 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Mar 18 10:12:58 2014 +0100
     1.3 @@ -331,25 +331,6 @@
     1.4    using setsum_norm_allsubsets_bound[OF assms]
     1.5    by (simp add: DIM_cart Basis_real_def)
     1.6  
     1.7 -instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
     1.8 -begin
     1.9 -
    1.10 -definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
    1.11 -definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
    1.12 -definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
    1.13 -definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
    1.14 -definition "abs x = (\<chi> i. abs (x $ i))"
    1.15 -
    1.16 -instance
    1.17 -  apply default
    1.18 -  unfolding euclidean_representation_setsum'
    1.19 -  apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
    1.20 -    Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
    1.21 -    inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
    1.22 -  done
    1.23 -
    1.24 -end
    1.25 -
    1.26  subsection {* Matrix operations *}
    1.27  
    1.28  text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *}
     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 18 10:12:57 2014 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Mar 18 10:12:58 2014 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  theory Convex_Euclidean_Space
     2.6  imports
     2.7 -  Ordered_Euclidean_Space
     2.8 +  Topology_Euclidean_Space
     2.9    "~~/src/HOL/Library/Convex"
    2.10    "~~/src/HOL/Library/Set_Algebras"
    2.11  begin
    2.12 @@ -3369,7 +3369,7 @@
    2.13    have "box a b \<noteq> {}"
    2.14      using assms
    2.15      unfolding set_eq_iff
    2.16 -    by (auto intro!: exI[of _ "(a + b) / 2"] simp: box)
    2.17 +    by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
    2.18    then show ?thesis
    2.19      using interior_rel_interior_gen[of "cbox a b", symmetric]
    2.20      by (simp split: split_if_asm del: box_real add: box_real[symmetric] interior_cbox)
    2.21 @@ -5672,7 +5672,7 @@
    2.22  
    2.23  lemma convex_box: "convex (cbox a b)" "convex (box a (b::'a::euclidean_space))"
    2.24    apply (rule_tac[!] is_interval_convex)+
    2.25 -  using is_interval_interval
    2.26 +  using is_interval_box is_interval_cbox
    2.27    apply auto
    2.28    done
    2.29  
     3.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Tue Mar 18 10:12:57 2014 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Tue Mar 18 10:12:58 2014 +0100
     3.3 @@ -740,7 +740,7 @@
     3.4        using ab startfin abab assms(3)
     3.5        using assms(9-)
     3.6        unfolding assms
     3.7 -      apply (auto simp add: field_simps box)
     3.8 +      apply (auto simp add: field_simps box_def)
     3.9        done
    3.10      then show "path_image ?P1 \<subseteq> cbox ?a ?b" .
    3.11      have "path_image ?P2 \<subseteq> cbox ?a ?b"
    3.12 @@ -752,7 +752,7 @@
    3.13        using ab startfin abab assms(4)
    3.14        using assms(9-)
    3.15        unfolding assms
    3.16 -      apply (auto simp add: field_simps box)
    3.17 +      apply (auto simp add: field_simps box_def)
    3.18        done
    3.19      then show "path_image ?P2 \<subseteq> cbox ?a ?b" .
    3.20      show "a $ 1 - 2 = a $ 1 - 2"
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 18 10:12:57 2014 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 18 10:12:58 2014 +0100
     4.3 @@ -223,9 +223,6 @@
     4.4    using nonempty_Basis
     4.5    by (fastforce simp add: set_eq_iff mem_box)
     4.6  
     4.7 -lemma One_nonneg: "0 \<le> (One::'a::ordered_euclidean_space)"
     4.8 -  by (auto intro: setsum_nonneg)
     4.9 -
    4.10  lemma interior_subset_union_intervals:
    4.11    assumes "i = cbox a b"
    4.12      and "j = cbox c d"
    4.13 @@ -516,13 +513,6 @@
    4.14  lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
    4.15    by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
    4.16  
    4.17 -lemma content_closed_interval:
    4.18 -  fixes a :: "'a::ordered_euclidean_space"
    4.19 -  assumes "a \<le> b"
    4.20 -  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
    4.21 -  using content_cbox[of a b] assms
    4.22 -  by (simp add: cbox_interval eucl_le[where 'a='a])
    4.23 -
    4.24  lemma content_singleton[simp]: "content {a} = 0"
    4.25  proof -
    4.26    have "content (cbox a a) = 0"
    4.27 @@ -1173,7 +1163,7 @@
    4.28  lemma elementary_bounded[dest]:
    4.29    fixes s :: "'a::euclidean_space set"
    4.30    shows "p division_of s \<Longrightarrow> bounded s"
    4.31 -  unfolding division_of_def by (metis bounded_Union bounded_interval)
    4.32 +  unfolding division_of_def by (metis bounded_Union bounded_cbox)
    4.33  
    4.34  lemma elementary_subset_cbox:
    4.35    "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
    4.36 @@ -1998,7 +1988,7 @@
    4.37  subsection {* The set we're concerned with must be closed. *}
    4.38  
    4.39  lemma division_of_closed:
    4.40 -  fixes i :: "'n::ordered_euclidean_space set"
    4.41 +  fixes i :: "'n::euclidean_space set"
    4.42    shows "s division_of i \<Longrightarrow> closed i"
    4.43    unfolding division_of_def by fastforce
    4.44  
    4.45 @@ -3759,7 +3749,7 @@
    4.46      apply (rule tagged_division_union[OF assms(1-2)])
    4.47      unfolding interval_split[OF k] interior_cbox
    4.48      using k
    4.49 -    apply (auto simp add: box elim!: ballE[where x=k])
    4.50 +    apply (auto simp add: box_def elim!: ballE[where x=k])
    4.51      done
    4.52  qed
    4.53  
    4.54 @@ -7131,12 +7121,6 @@
    4.55    apply (rule has_integral_const)
    4.56    done
    4.57  
    4.58 -lemma integrable_const_ivl[intro]:
    4.59 -  fixes a::"'a::ordered_euclidean_space"
    4.60 -  shows "(\<lambda>x. c) integrable_on {a .. b}"
    4.61 -  unfolding cbox_interval[symmetric]
    4.62 -  by (rule integrable_const)
    4.63 -
    4.64  lemma integral_has_vector_derivative:
    4.65    fixes f :: "real \<Rightarrow> 'a::banach"
    4.66    assumes "continuous_on {a .. b} f"
    4.67 @@ -9046,7 +9030,7 @@
    4.68    }
    4.69    assume "\<exists>a b. s = cbox a b"
    4.70    then guess a b by (elim exE) note s=this
    4.71 -  from bounded_interval[of a b, THEN conjunct1, unfolded bounded_pos] guess B ..
    4.72 +  from bounded_cbox[of a b, unfolded bounded_pos] guess B ..
    4.73    note B = conjunctD2[OF this,rule_format] show ?thesis
    4.74      apply safe
    4.75    proof -
    4.76 @@ -9603,14 +9587,6 @@
    4.77    apply auto
    4.78    done
    4.79  
    4.80 -lemma integrable_on_subinterval:
    4.81 -  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
    4.82 -  assumes "f integrable_on s"
    4.83 -    and "{a .. b} \<subseteq> s"
    4.84 -  shows "f integrable_on {a .. b}"
    4.85 -  using integrable_on_subcbox[of f s a b] assms
    4.86 -  by (simp add: cbox_interval)
    4.87 -
    4.88  
    4.89  subsection {* A straddling criterion for integrability *}
    4.90  
     5.1 --- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Mar 18 10:12:57 2014 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Mar 18 10:12:58 2014 +0100
     5.3 @@ -1,5 +1,5 @@
     5.4  theory Multivariate_Analysis
     5.5 -imports Fashoda Extended_Real_Limits Determinants
     5.6 +imports Fashoda Extended_Real_Limits Determinants Ordered_Euclidean_Space
     5.7  begin
     5.8  
     5.9  end
     6.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Mar 18 10:12:57 2014 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Tue Mar 18 10:12:58 2014 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4  theory Ordered_Euclidean_Space
     6.5  imports
     6.6 -  Topology_Euclidean_Space
     6.7 +  Cartesian_Euclidean_Space
     6.8    "~~/src/HOL/Library/Product_Order"
     6.9  begin
    6.10  
    6.11 @@ -174,707 +174,6 @@
    6.12        inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
    6.13        eucl_le[where 'a='b] abs_prod_def abs_inner)
    6.14  
    6.15 -
    6.16 -subsection {* Boxes *}
    6.17 -
    6.18 -lemma box:
    6.19 -  fixes a :: "'a::euclidean_space"
    6.20 -  shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
    6.21 -    and "cbox a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
    6.22 -  by (auto simp add:set_eq_iff box_def cbox_def)
    6.23 -
    6.24 -lemma mem_box:
    6.25 -  fixes a :: "'a::euclidean_space"
    6.26 -  shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
    6.27 -    and "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)"
    6.28 -  using box[of a b]
    6.29 -  by auto
    6.30 -
    6.31 -lemma box_eq_empty:
    6.32 -  fixes a :: "'a::euclidean_space"
    6.33 -  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
    6.34 -    and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
    6.35 -proof -
    6.36 -  {
    6.37 -    fix i x
    6.38 -    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
    6.39 -    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
    6.40 -      unfolding mem_box by (auto simp: box_def)
    6.41 -    then have "a\<bullet>i < b\<bullet>i" by auto
    6.42 -    then have False using as by auto
    6.43 -  }
    6.44 -  moreover
    6.45 -  {
    6.46 -    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
    6.47 -    let ?x = "(1/2) *\<^sub>R (a + b)"
    6.48 -    {
    6.49 -      fix i :: 'a
    6.50 -      assume i: "i \<in> Basis"
    6.51 -      have "a\<bullet>i < b\<bullet>i"
    6.52 -        using as[THEN bspec[where x=i]] i by auto
    6.53 -      then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
    6.54 -        by (auto simp: inner_add_left)
    6.55 -    }
    6.56 -    then have "box a b \<noteq> {}"
    6.57 -      using mem_box(1)[of "?x" a b] by auto
    6.58 -  }
    6.59 -  ultimately show ?th1 by blast
    6.60 -
    6.61 -  {
    6.62 -    fix i x
    6.63 -    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
    6.64 -    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
    6.65 -      unfolding mem_box by auto
    6.66 -    then have "a\<bullet>i \<le> b\<bullet>i" by auto
    6.67 -    then have False using as by auto
    6.68 -  }
    6.69 -  moreover
    6.70 -  {
    6.71 -    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
    6.72 -    let ?x = "(1/2) *\<^sub>R (a + b)"
    6.73 -    {
    6.74 -      fix i :: 'a
    6.75 -      assume i:"i \<in> Basis"
    6.76 -      have "a\<bullet>i \<le> b\<bullet>i"
    6.77 -        using as[THEN bspec[where x=i]] i by auto
    6.78 -      then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i"
    6.79 -        by (auto simp: inner_add_left)
    6.80 -    }
    6.81 -    then have "cbox a b \<noteq> {}"
    6.82 -      using mem_box(2)[of "?x" a b] by auto
    6.83 -  }
    6.84 -  ultimately show ?th2 by blast
    6.85 -qed
    6.86 -
    6.87 -lemma box_ne_empty:
    6.88 -  fixes a :: "'a::euclidean_space"
    6.89 -  shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
    6.90 -  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
    6.91 -  unfolding box_eq_empty[of a b] by fastforce+
    6.92 -
    6.93 -lemma
    6.94 -  fixes a :: "'a::euclidean_space"
    6.95 -  shows cbox_sing: "cbox a a = {a}"
    6.96 -    and box_sing: "box a a = {}"
    6.97 -  unfolding set_eq_iff mem_box eq_iff [symmetric]
    6.98 -  by (auto intro!: euclidean_eqI[where 'a='a])
    6.99 -     (metis all_not_in_conv nonempty_Basis)
   6.100 -
   6.101 -lemma subset_box_imp:
   6.102 -  fixes a :: "'a::euclidean_space"
   6.103 -  shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> cbox a b"
   6.104 -    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> box a b"
   6.105 -    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> cbox a b"
   6.106 -     and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
   6.107 -  unfolding subset_eq[unfolded Ball_def] unfolding mem_box
   6.108 -   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
   6.109 -
   6.110 -lemma box_subset_cbox:
   6.111 -  fixes a :: "'a::euclidean_space"
   6.112 -  shows "box a b \<subseteq> cbox a b"
   6.113 -  unfolding subset_eq [unfolded Ball_def] mem_box
   6.114 -  by (fast intro: less_imp_le)
   6.115 -
   6.116 -lemma subset_box:
   6.117 -  fixes a :: "'a::euclidean_space"
   6.118 -  shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
   6.119 -    and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
   6.120 -    and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   6.121 -    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   6.122 -proof -
   6.123 -  show ?th1
   6.124 -    unfolding subset_eq and Ball_def and mem_box
   6.125 -    by (auto intro: order_trans)
   6.126 -  show ?th2
   6.127 -    unfolding subset_eq and Ball_def and mem_box
   6.128 -    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   6.129 -  {
   6.130 -    assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   6.131 -    then have "box c d \<noteq> {}"
   6.132 -      unfolding box_eq_empty by auto
   6.133 -    fix i :: 'a
   6.134 -    assume i: "i \<in> Basis"
   6.135 -    (** TODO combine the following two parts as done in the HOL_light version. **)
   6.136 -    {
   6.137 -      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   6.138 -      assume as2: "a\<bullet>i > c\<bullet>i"
   6.139 -      {
   6.140 -        fix j :: 'a
   6.141 -        assume j: "j \<in> Basis"
   6.142 -        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
   6.143 -          apply (cases "j = i")
   6.144 -          using as(2)[THEN bspec[where x=j]] i
   6.145 -          apply (auto simp add: as2)
   6.146 -          done
   6.147 -      }
   6.148 -      then have "?x\<in>box c d"
   6.149 -        using i unfolding mem_box by auto
   6.150 -      moreover
   6.151 -      have "?x \<notin> cbox a b"
   6.152 -        unfolding mem_box
   6.153 -        apply auto
   6.154 -        apply (rule_tac x=i in bexI)
   6.155 -        using as(2)[THEN bspec[where x=i]] and as2 i
   6.156 -        apply auto
   6.157 -        done
   6.158 -      ultimately have False using as by auto
   6.159 -    }
   6.160 -    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
   6.161 -    moreover
   6.162 -    {
   6.163 -      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   6.164 -      assume as2: "b\<bullet>i < d\<bullet>i"
   6.165 -      {
   6.166 -        fix j :: 'a
   6.167 -        assume "j\<in>Basis"
   6.168 -        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
   6.169 -          apply (cases "j = i")
   6.170 -          using as(2)[THEN bspec[where x=j]]
   6.171 -          apply (auto simp add: as2)
   6.172 -          done
   6.173 -      }
   6.174 -      then have "?x\<in>box c d"
   6.175 -        unfolding mem_box by auto
   6.176 -      moreover
   6.177 -      have "?x\<notin>cbox a b"
   6.178 -        unfolding mem_box
   6.179 -        apply auto
   6.180 -        apply (rule_tac x=i in bexI)
   6.181 -        using as(2)[THEN bspec[where x=i]] and as2 using i
   6.182 -        apply auto
   6.183 -        done
   6.184 -      ultimately have False using as by auto
   6.185 -    }
   6.186 -    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
   6.187 -    ultimately
   6.188 -    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
   6.189 -  } note part1 = this
   6.190 -  show ?th3
   6.191 -    unfolding subset_eq and Ball_def and mem_box
   6.192 -    apply (rule, rule, rule, rule)
   6.193 -    apply (rule part1)
   6.194 -    unfolding subset_eq and Ball_def and mem_box
   6.195 -    prefer 4
   6.196 -    apply auto
   6.197 -    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
   6.198 -    done
   6.199 -  {
   6.200 -    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   6.201 -    fix i :: 'a
   6.202 -    assume i:"i\<in>Basis"
   6.203 -    from as(1) have "box c d \<subseteq> cbox a b"
   6.204 -      using box_subset_cbox[of a b] by auto
   6.205 -    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   6.206 -      using part1 and as(2) using i by auto
   6.207 -  } note * = this
   6.208 -  show ?th4
   6.209 -    unfolding subset_eq and Ball_def and mem_box
   6.210 -    apply (rule, rule, rule, rule)
   6.211 -    apply (rule *)
   6.212 -    unfolding subset_eq and Ball_def and mem_box
   6.213 -    prefer 4
   6.214 -    apply auto
   6.215 -    apply (erule_tac x=xa in allE, simp)+
   6.216 -    done
   6.217 -qed
   6.218 -
   6.219 -lemma inter_interval:
   6.220 -  fixes a :: "'a::euclidean_space"
   6.221 -  shows "cbox a b \<inter> cbox c d =
   6.222 -    cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
   6.223 -  unfolding set_eq_iff and Int_iff and mem_box
   6.224 -  by auto
   6.225 -
   6.226 -lemma disjoint_interval:
   6.227 -  fixes a::"'a::euclidean_space"
   6.228 -  shows "cbox a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
   6.229 -    and "cbox a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
   6.230 -    and "box a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
   6.231 -    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
   6.232 -proof -
   6.233 -  let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
   6.234 -  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
   6.235 -      (\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)"
   6.236 -    by blast
   6.237 -  note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
   6.238 -  show ?th1 unfolding * by (intro **) auto
   6.239 -  show ?th2 unfolding * by (intro **) auto
   6.240 -  show ?th3 unfolding * by (intro **) auto
   6.241 -  show ?th4 unfolding * by (intro **) auto
   6.242 -qed
   6.243 -
   6.244 -(* Moved box_subset_cbox a bit upwards *)
   6.245 -
   6.246 -lemma open_box[intro]:
   6.247 -  fixes a b :: "'a::euclidean_space"
   6.248 -  shows "open (box a b)"
   6.249 -proof -
   6.250 -  have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
   6.251 -    by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
   6.252 -      linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
   6.253 -  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
   6.254 -    by (auto simp add: box)
   6.255 -  finally show "open (box a b)" .
   6.256 -qed
   6.257 -
   6.258 -lemma closed_cbox[intro]:
   6.259 -  fixes a b :: "'a::euclidean_space"
   6.260 -  shows "closed (cbox a b)"
   6.261 -proof -
   6.262 -  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
   6.263 -    by (intro closed_INT ballI continuous_closed_vimage allI
   6.264 -      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
   6.265 -  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
   6.266 -    by (auto simp add: cbox_def)
   6.267 -  finally show "closed (cbox a b)" .
   6.268 -qed
   6.269 -
   6.270 -lemma interior_cbox [intro]:
   6.271 -  fixes a b :: "'a::euclidean_space"
   6.272 -  shows "interior (cbox a b) = box a b" (is "?L = ?R")
   6.273 -proof(rule subset_antisym)
   6.274 -  show "?R \<subseteq> ?L"
   6.275 -    using box_subset_cbox open_box
   6.276 -    by (rule interior_maximal)
   6.277 -  {
   6.278 -    fix x
   6.279 -    assume "x \<in> interior (cbox a b)"
   6.280 -    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
   6.281 -    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
   6.282 -      unfolding open_dist and subset_eq by auto
   6.283 -    {
   6.284 -      fix i :: 'a
   6.285 -      assume i: "i \<in> Basis"
   6.286 -      have "dist (x - (e / 2) *\<^sub>R i) x < e"
   6.287 -        and "dist (x + (e / 2) *\<^sub>R i) x < e"
   6.288 -        unfolding dist_norm
   6.289 -        apply auto
   6.290 -        unfolding norm_minus_cancel
   6.291 -        using norm_Basis[OF i] `e>0`
   6.292 -        apply auto
   6.293 -        done
   6.294 -      then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i"
   6.295 -        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
   6.296 -          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
   6.297 -        unfolding mem_box
   6.298 -        using i
   6.299 -        by blast+
   6.300 -      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
   6.301 -        using `e>0` i
   6.302 -        by (auto simp: inner_diff_left inner_Basis inner_add_left)
   6.303 -    }
   6.304 -    then have "x \<in> box a b"
   6.305 -      unfolding mem_box by auto
   6.306 -  }
   6.307 -  then show "?L \<subseteq> ?R" ..
   6.308 -qed
   6.309 -
   6.310 -lemma bounded_cbox:
   6.311 -  fixes a :: "'a::euclidean_space"
   6.312 -  shows "bounded (cbox a b)"
   6.313 -proof -
   6.314 -  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   6.315 -  {
   6.316 -    fix x :: "'a"
   6.317 -    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   6.318 -    {
   6.319 -      fix i :: 'a
   6.320 -      assume "i \<in> Basis"
   6.321 -      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   6.322 -        using x[THEN bspec[where x=i]] by auto
   6.323 -    }
   6.324 -    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
   6.325 -      apply -
   6.326 -      apply (rule setsum_mono)
   6.327 -      apply auto
   6.328 -      done
   6.329 -    then have "norm x \<le> ?b"
   6.330 -      using norm_le_l1[of x] by auto
   6.331 -  }
   6.332 -  then show ?thesis
   6.333 -    unfolding box and bounded_iff by auto
   6.334 -qed
   6.335 -
   6.336 -lemma bounded_interval:
   6.337 -  fixes a :: "'a::euclidean_space"
   6.338 -  shows "bounded (cbox a b) \<and> bounded (box a b)"
   6.339 -  using bounded_cbox[of a b]
   6.340 -  using box_subset_cbox[of a b]
   6.341 -  using bounded_subset[of "cbox a b" "box a b"]
   6.342 -  by simp
   6.343 -
   6.344 -lemma not_interval_univ:
   6.345 -  fixes a :: "'a::euclidean_space"
   6.346 -  shows "cbox a b \<noteq> UNIV \<and> box a b \<noteq> UNIV"
   6.347 -  using bounded_interval[of a b] by auto
   6.348 -
   6.349 -lemma compact_cbox:
   6.350 -  fixes a :: "'a::euclidean_space"
   6.351 -  shows "compact (cbox a b)"
   6.352 -  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_interval[of a b]
   6.353 -  by (auto simp: compact_eq_seq_compact_metric)
   6.354 -
   6.355 -lemma open_interval_midpoint:
   6.356 -  fixes a :: "'a::euclidean_space"
   6.357 -  assumes "box a b \<noteq> {}"
   6.358 -  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
   6.359 -proof -
   6.360 -  {
   6.361 -    fix i :: 'a
   6.362 -    assume "i \<in> Basis"
   6.363 -    then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
   6.364 -      using assms[unfolded box_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
   6.365 -  }
   6.366 -  then show ?thesis unfolding mem_box by auto
   6.367 -qed
   6.368 -
   6.369 -lemma open_closed_interval_convex:
   6.370 -  fixes x :: "'a::euclidean_space"
   6.371 -  assumes x: "x \<in> box a b"
   6.372 -    and y: "y \<in> cbox a b"
   6.373 -    and e: "0 < e" "e \<le> 1"
   6.374 -  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
   6.375 -proof -
   6.376 -  {
   6.377 -    fix i :: 'a
   6.378 -    assume i: "i \<in> Basis"
   6.379 -    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
   6.380 -      unfolding left_diff_distrib by simp
   6.381 -    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   6.382 -      apply (rule add_less_le_mono)
   6.383 -      using e unfolding mult_less_cancel_left and mult_le_cancel_left
   6.384 -      apply simp_all
   6.385 -      using x unfolding mem_box using i
   6.386 -      apply simp
   6.387 -      using y unfolding mem_box using i
   6.388 -      apply simp
   6.389 -      done
   6.390 -    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
   6.391 -      unfolding inner_simps by auto
   6.392 -    moreover
   6.393 -    {
   6.394 -      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
   6.395 -        unfolding left_diff_distrib by simp
   6.396 -      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   6.397 -        apply (rule add_less_le_mono)
   6.398 -        using e unfolding mult_less_cancel_left and mult_le_cancel_left
   6.399 -        apply simp_all
   6.400 -        using x
   6.401 -        unfolding mem_box
   6.402 -        using i
   6.403 -        apply simp
   6.404 -        using y
   6.405 -        unfolding mem_box
   6.406 -        using i
   6.407 -        apply simp
   6.408 -        done
   6.409 -      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   6.410 -        unfolding inner_simps by auto
   6.411 -    }
   6.412 -    ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   6.413 -      by auto
   6.414 -  }
   6.415 -  then show ?thesis
   6.416 -    unfolding mem_box by auto
   6.417 -qed
   6.418 -
   6.419 -notation
   6.420 -  eucl_less (infix "<e" 50)
   6.421 -
   6.422 -lemma closure_open_interval:
   6.423 -  fixes a :: "'a::euclidean_space"
   6.424 -   assumes "box a b \<noteq> {}"
   6.425 -  shows "closure (box a b) = cbox a b"
   6.426 -proof -
   6.427 -  have ab: "a <e b"
   6.428 -    using assms by (simp add: eucl_less_def box_ne_empty)
   6.429 -  let ?c = "(1 / 2) *\<^sub>R (a + b)"
   6.430 -  {
   6.431 -    fix x
   6.432 -    assume as:"x \<in> cbox a b"
   6.433 -    def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
   6.434 -    {
   6.435 -      fix n
   6.436 -      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
   6.437 -      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
   6.438 -        unfolding inverse_le_1_iff by auto
   6.439 -      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
   6.440 -        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
   6.441 -        by (auto simp add: algebra_simps)
   6.442 -      then have "f n <e b" and "a <e f n"
   6.443 -        using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
   6.444 -        unfolding f_def by (auto simp: box eucl_less_def)
   6.445 -      then have False
   6.446 -        using fn unfolding f_def using xc by auto
   6.447 -    }
   6.448 -    moreover
   6.449 -    {
   6.450 -      assume "\<not> (f ---> x) sequentially"
   6.451 -      {
   6.452 -        fix e :: real
   6.453 -        assume "e > 0"
   6.454 -        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
   6.455 -          using real_arch_inv[of e]
   6.456 -          apply (auto simp add: Suc_pred')
   6.457 -          apply (rule_tac x="n - 1" in exI)
   6.458 -          apply auto
   6.459 -          done
   6.460 -        then obtain N :: nat where "inverse (real (N + 1)) < e"
   6.461 -          by auto
   6.462 -        then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
   6.463 -          apply auto
   6.464 -          apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
   6.465 -            real_of_nat_Suc real_of_nat_Suc_gt_zero)
   6.466 -          done
   6.467 -        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
   6.468 -      }
   6.469 -      then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
   6.470 -        unfolding LIMSEQ_def by(auto simp add: dist_norm)
   6.471 -      then have "(f ---> x) sequentially"
   6.472 -        unfolding f_def
   6.473 -        using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   6.474 -        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
   6.475 -        by auto
   6.476 -    }
   6.477 -    ultimately have "x \<in> closure (box a b)"
   6.478 -      using as and open_interval_midpoint[OF assms]
   6.479 -      unfolding closure_def
   6.480 -      unfolding islimpt_sequential
   6.481 -      by (cases "x=?c") (auto simp: in_box_eucl_less)
   6.482 -  }
   6.483 -  then show ?thesis
   6.484 -    using closure_minimal[OF box_subset_cbox, of a b] by blast
   6.485 -qed
   6.486 -
   6.487 -lemma bounded_subset_open_interval_symmetric:
   6.488 -  fixes s::"('a::euclidean_space) set"
   6.489 -  assumes "bounded s"
   6.490 -  shows "\<exists>a. s \<subseteq> box (-a) a"
   6.491 -proof -
   6.492 -  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
   6.493 -    using assms[unfolded bounded_pos] by auto
   6.494 -  def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
   6.495 -  {
   6.496 -    fix x
   6.497 -    assume "x \<in> s"
   6.498 -    fix i :: 'a
   6.499 -    assume i: "i \<in> Basis"
   6.500 -    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
   6.501 -      using b[THEN bspec[where x=x], OF `x\<in>s`]
   6.502 -      using Basis_le_norm[OF i, of x]
   6.503 -      unfolding inner_simps and a_def
   6.504 -      by auto
   6.505 -  }
   6.506 -  then show ?thesis
   6.507 -    by (auto intro: exI[where x=a] simp add: box)
   6.508 -qed
   6.509 -
   6.510 -lemma bounded_subset_open_interval:
   6.511 -  fixes s :: "('a::euclidean_space) set"
   6.512 -  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   6.513 -  by (auto dest!: bounded_subset_open_interval_symmetric)
   6.514 -
   6.515 -lemma bounded_subset_cbox_symmetric:
   6.516 -  fixes s :: "('a::euclidean_space) set"
   6.517 -   assumes "bounded s"
   6.518 -  shows "\<exists>a. s \<subseteq> cbox (-a) a"
   6.519 -proof -
   6.520 -  obtain a where "s \<subseteq> box (-a) a"
   6.521 -    using bounded_subset_open_interval_symmetric[OF assms] by auto
   6.522 -  then show ?thesis
   6.523 -    using box_subset_cbox[of "-a" a] by auto
   6.524 -qed
   6.525 -
   6.526 -lemma bounded_subset_cbox:
   6.527 -  fixes s :: "('a::euclidean_space) set"
   6.528 -  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b"
   6.529 -  using bounded_subset_cbox_symmetric[of s] by auto
   6.530 -
   6.531 -lemma frontier_closed_interval:
   6.532 -  fixes a b :: "'a::euclidean_space"
   6.533 -  shows "frontier (cbox a b) = cbox a b - box a b"
   6.534 -  unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
   6.535 -
   6.536 -lemma frontier_open_interval:
   6.537 -  fixes a b :: "'a::euclidean_space"
   6.538 -  shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
   6.539 -proof (cases "box a b = {}")
   6.540 -  case True
   6.541 -  then show ?thesis
   6.542 -    using frontier_empty by auto
   6.543 -next
   6.544 -  case False
   6.545 -  then show ?thesis
   6.546 -    unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_box]
   6.547 -    by auto
   6.548 -qed
   6.549 -
   6.550 -lemma inter_interval_mixed_eq_empty:
   6.551 -  fixes a :: "'a::euclidean_space"
   6.552 -   assumes "box c d \<noteq> {}"
   6.553 -  shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   6.554 -  unfolding closure_open_interval[OF assms, symmetric]
   6.555 -  unfolding open_inter_closure_eq_empty[OF open_box] ..
   6.556 -
   6.557 -lemma diameter_closed_interval:
   6.558 -  fixes a b::"'a::ordered_euclidean_space"
   6.559 -  shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b"
   6.560 -  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
   6.561 -     simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm)
   6.562 -
   6.563 -text {* Intervals in general, including infinite and mixtures of open and closed. *}
   6.564 -
   6.565 -definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   6.566 -  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   6.567 -
   6.568 -lemma is_interval_interval: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   6.569 -  "is_interval (box a b)" (is ?th2) proof -
   6.570 -  show ?th1 ?th2  unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
   6.571 -    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
   6.572 -
   6.573 -lemma is_interval_empty:
   6.574 - "is_interval {}"
   6.575 -  unfolding is_interval_def
   6.576 -  by simp
   6.577 -
   6.578 -lemma is_interval_univ:
   6.579 - "is_interval UNIV"
   6.580 -  unfolding is_interval_def
   6.581 -  by simp
   6.582 -
   6.583 -lemma mem_is_intervalI:
   6.584 -  assumes "is_interval s"
   6.585 -  assumes "a \<in> s" "b \<in> s"
   6.586 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i"
   6.587 -  shows "x \<in> s"
   6.588 -  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
   6.589 -
   6.590 -lemma interval_subst:
   6.591 -  fixes S::"'a::ordered_euclidean_space set"
   6.592 -  assumes "is_interval S"
   6.593 -  assumes "x \<in> S" "y j \<in> S"
   6.594 -  assumes "j \<in> Basis"
   6.595 -  shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
   6.596 -  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
   6.597 -
   6.598 -lemma mem_box_componentwiseI:
   6.599 -  fixes S::"'a::ordered_euclidean_space set"
   6.600 -  assumes "is_interval S"
   6.601 -  assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
   6.602 -  shows "x \<in> S"
   6.603 -proof -
   6.604 -  from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
   6.605 -    by auto
   6.606 -  with finite_Basis obtain s and bs::"'a list" where
   6.607 -    s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S" and
   6.608 -    bs: "set bs = Basis" "distinct bs"
   6.609 -    by (metis finite_distinct_list)
   6.610 -  from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
   6.611 -  def y \<equiv> "rec_list
   6.612 -    (s j)
   6.613 -    (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
   6.614 -  have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
   6.615 -    using bs by (auto simp add: s(1)[symmetric] euclidean_representation)
   6.616 -  also have [symmetric]: "y bs = \<dots>"
   6.617 -    using bs(2) bs(1)[THEN equalityD1]
   6.618 -    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
   6.619 -  also have "y bs \<in> S"
   6.620 -    using bs(1)[THEN equalityD1]
   6.621 -    apply (induct bs)
   6.622 -    apply (auto simp: y_def j)
   6.623 -    apply (rule interval_subst[OF assms(1)])
   6.624 -    apply (auto simp: s)
   6.625 -    done
   6.626 -  finally show ?thesis .
   6.627 -qed
   6.628 -
   6.629 -lemma eucl_less_eq_halfspaces:
   6.630 -  fixes a :: "'a\<Colon>euclidean_space"
   6.631 -  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   6.632 -    "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   6.633 -  by (auto simp: eucl_less_def)
   6.634 -
   6.635 -lemma eucl_le_eq_halfspaces:
   6.636 -  fixes a :: "'a\<Colon>euclidean_space"
   6.637 -  shows "{x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
   6.638 -    "{x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
   6.639 -  by auto
   6.640 -
   6.641 -lemma open_Collect_eucl_less[simp, intro]:
   6.642 -  fixes a :: "'a\<Colon>euclidean_space"
   6.643 -  shows "open {x. x <e a}"
   6.644 -    "open {x. a <e x}"
   6.645 -  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
   6.646 -
   6.647 -lemma closed_Collect_eucl_le[simp, intro]:
   6.648 -  fixes a :: "'a\<Colon>euclidean_space"
   6.649 -  shows "closed {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i}"
   6.650 -    "closed {x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i}"
   6.651 -  unfolding eucl_le_eq_halfspaces
   6.652 -  by (simp_all add: closed_INT closed_Collect_le)
   6.653 -
   6.654 -lemma image_affinity_cbox: fixes m::real
   6.655 -  fixes a b c :: "'a::euclidean_space"
   6.656 -  shows "(\<lambda>x. m *\<^sub>R x + c) ` cbox a b =
   6.657 -    (if cbox a b = {} then {}
   6.658 -     else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
   6.659 -     else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))"
   6.660 -proof (cases "m = 0")
   6.661 -  case True
   6.662 -  {
   6.663 -    fix x
   6.664 -    assume "\<forall>i\<in>Basis. x \<bullet> i \<le> c \<bullet> i" "\<forall>i\<in>Basis. c \<bullet> i \<le> x \<bullet> i"
   6.665 -    then have "x = c"
   6.666 -      apply -
   6.667 -      apply (subst euclidean_eq_iff)
   6.668 -      apply (auto intro: order_antisym)
   6.669 -      done
   6.670 -  }
   6.671 -  moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
   6.672 -    unfolding True by (auto simp add: cbox_sing)
   6.673 -  ultimately show ?thesis using True by (auto simp: cbox_def)
   6.674 -next
   6.675 -  case False
   6.676 -  {
   6.677 -    fix y
   6.678 -    assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m > 0"
   6.679 -    then have "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
   6.680 -      by (auto simp: inner_distrib)
   6.681 -  }
   6.682 -  moreover
   6.683 -  {
   6.684 -    fix y
   6.685 -    assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m < 0"
   6.686 -    then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
   6.687 -      by (auto simp add: mult_left_mono_neg inner_distrib)
   6.688 -  }
   6.689 -  moreover
   6.690 -  {
   6.691 -    fix y
   6.692 -    assume "m > 0" and "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> y \<bullet> i" and "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
   6.693 -    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   6.694 -      unfolding image_iff Bex_def mem_box
   6.695 -      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   6.696 -      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   6.697 -      done
   6.698 -  }
   6.699 -  moreover
   6.700 -  {
   6.701 -    fix y
   6.702 -    assume "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i" "m < 0"
   6.703 -    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   6.704 -      unfolding image_iff Bex_def mem_box
   6.705 -      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   6.706 -      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   6.707 -      done
   6.708 -  }
   6.709 -  ultimately show ?thesis using False by (auto simp: cbox_def)
   6.710 -qed
   6.711 -
   6.712 -lemma image_smult_cbox:"(\<lambda>x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
   6.713 -  (if cbox a b = {} then {} else if 0 \<le> m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>R a))"
   6.714 -  using image_affinity_cbox[of m 0 a b] by auto
   6.715 -
   6.716  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
   6.717  
   6.718  lemma
   6.719 @@ -900,6 +199,12 @@
   6.720    shows "closed {a..}"
   6.721    by (simp add: eucl_le_atLeast[symmetric])
   6.722  
   6.723 +lemma bounded_closed_interval:
   6.724 +  fixes a :: "'a::ordered_euclidean_space"
   6.725 +  shows "bounded {a .. b}"
   6.726 +  using bounded_cbox[of a b]
   6.727 +  by (metis interval_cbox)
   6.728 +
   6.729  lemma image_affinity_interval: fixes m::real
   6.730    fixes a b c :: "'a::ordered_euclidean_space"
   6.731    shows "(\<lambda>x. m *\<^sub>R x + c) ` {a..b} =
   6.732 @@ -914,7 +219,55 @@
   6.733    using image_smult_cbox[of m a b]
   6.734    by (simp add: cbox_interval)
   6.735  
   6.736 +lemma is_interval_closed_interval:
   6.737 +  "is_interval {a .. (b::'a::ordered_euclidean_space)}"
   6.738 +  by (metis cbox_interval is_interval_cbox)
   6.739 +
   6.740  no_notation
   6.741    eucl_less (infix "<e" 50)
   6.742  
   6.743 +lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
   6.744 +  by (auto intro: setsum_nonneg)
   6.745 +
   6.746 +lemma content_closed_interval:
   6.747 +  fixes a :: "'a::ordered_euclidean_space"
   6.748 +  assumes "a \<le> b"
   6.749 +  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   6.750 +  using content_cbox[of a b] assms
   6.751 +  by (simp add: cbox_interval eucl_le[where 'a='a])
   6.752 +
   6.753 +lemma integrable_const_ivl[intro]:
   6.754 +  fixes a::"'a::ordered_euclidean_space"
   6.755 +  shows "(\<lambda>x. c) integrable_on {a .. b}"
   6.756 +  unfolding cbox_interval[symmetric]
   6.757 +  by (rule integrable_const)
   6.758 +
   6.759 +lemma integrable_on_subinterval:
   6.760 +  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   6.761 +  assumes "f integrable_on s"
   6.762 +    and "{a .. b} \<subseteq> s"
   6.763 +  shows "f integrable_on {a .. b}"
   6.764 +  using integrable_on_subcbox[of f s a b] assms
   6.765 +  by (simp add: cbox_interval)
   6.766 +
   6.767 +instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
   6.768 +begin
   6.769 +
   6.770 +definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
   6.771 +definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
   6.772 +definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
   6.773 +definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
   6.774 +definition "abs x = (\<chi> i. abs (x $ i))"
   6.775 +
   6.776 +instance
   6.777 +  apply default
   6.778 +  unfolding euclidean_representation_setsum'
   6.779 +  apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
   6.780 +    Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
   6.781 +    inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
   6.782 +  done
   6.783 +
   6.784  end
   6.785 +
   6.786 +end
   6.787 +
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 18 10:12:57 2014 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 18 10:12:58 2014 +0100
     7.3 @@ -822,6 +822,9 @@
     7.4    unfolding dist_norm norm_eq_sqrt_inner setL2_def
     7.5    by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
     7.6  
     7.7 +
     7.8 +subsection {* Boxes *}
     7.9 +
    7.10  definition (in euclidean_space) eucl_less (infix "<e" 50)
    7.11    where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
    7.12  
    7.13 @@ -926,6 +929,285 @@
    7.14    then show ?thesis by (auto simp: I_def)
    7.15  qed
    7.16  
    7.17 +lemma box_eq_empty:
    7.18 +  fixes a :: "'a::euclidean_space"
    7.19 +  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
    7.20 +    and "(cbox a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
    7.21 +proof -
    7.22 +  {
    7.23 +    fix i x
    7.24 +    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
    7.25 +    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
    7.26 +      unfolding mem_box by (auto simp: box_def)
    7.27 +    then have "a\<bullet>i < b\<bullet>i" by auto
    7.28 +    then have False using as by auto
    7.29 +  }
    7.30 +  moreover
    7.31 +  {
    7.32 +    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
    7.33 +    let ?x = "(1/2) *\<^sub>R (a + b)"
    7.34 +    {
    7.35 +      fix i :: 'a
    7.36 +      assume i: "i \<in> Basis"
    7.37 +      have "a\<bullet>i < b\<bullet>i"
    7.38 +        using as[THEN bspec[where x=i]] i by auto
    7.39 +      then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
    7.40 +        by (auto simp: inner_add_left)
    7.41 +    }
    7.42 +    then have "box a b \<noteq> {}"
    7.43 +      using mem_box(1)[of "?x" a b] by auto
    7.44 +  }
    7.45 +  ultimately show ?th1 by blast
    7.46 +
    7.47 +  {
    7.48 +    fix i x
    7.49 +    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>cbox a b"
    7.50 +    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
    7.51 +      unfolding mem_box by auto
    7.52 +    then have "a\<bullet>i \<le> b\<bullet>i" by auto
    7.53 +    then have False using as by auto
    7.54 +  }
    7.55 +  moreover
    7.56 +  {
    7.57 +    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
    7.58 +    let ?x = "(1/2) *\<^sub>R (a + b)"
    7.59 +    {
    7.60 +      fix i :: 'a
    7.61 +      assume i:"i \<in> Basis"
    7.62 +      have "a\<bullet>i \<le> b\<bullet>i"
    7.63 +        using as[THEN bspec[where x=i]] i by auto
    7.64 +      then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i"
    7.65 +        by (auto simp: inner_add_left)
    7.66 +    }
    7.67 +    then have "cbox a b \<noteq> {}"
    7.68 +      using mem_box(2)[of "?x" a b] by auto
    7.69 +  }
    7.70 +  ultimately show ?th2 by blast
    7.71 +qed
    7.72 +
    7.73 +lemma box_ne_empty:
    7.74 +  fixes a :: "'a::euclidean_space"
    7.75 +  shows "cbox a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
    7.76 +  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
    7.77 +  unfolding box_eq_empty[of a b] by fastforce+
    7.78 +
    7.79 +lemma
    7.80 +  fixes a :: "'a::euclidean_space"
    7.81 +  shows cbox_sing: "cbox a a = {a}"
    7.82 +    and box_sing: "box a a = {}"
    7.83 +  unfolding set_eq_iff mem_box eq_iff [symmetric]
    7.84 +  by (auto intro!: euclidean_eqI[where 'a='a])
    7.85 +     (metis all_not_in_conv nonempty_Basis)
    7.86 +
    7.87 +lemma subset_box_imp:
    7.88 +  fixes a :: "'a::euclidean_space"
    7.89 +  shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> cbox a b"
    7.90 +    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> cbox c d \<subseteq> box a b"
    7.91 +    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> cbox a b"
    7.92 +     and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
    7.93 +  unfolding subset_eq[unfolded Ball_def] unfolding mem_box
    7.94 +   by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
    7.95 +
    7.96 +lemma box_subset_cbox:
    7.97 +  fixes a :: "'a::euclidean_space"
    7.98 +  shows "box a b \<subseteq> cbox a b"
    7.99 +  unfolding subset_eq [unfolded Ball_def] mem_box
   7.100 +  by (fast intro: less_imp_le)
   7.101 +
   7.102 +lemma subset_box:
   7.103 +  fixes a :: "'a::euclidean_space"
   7.104 +  shows "cbox c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
   7.105 +    and "cbox c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
   7.106 +    and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   7.107 +    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   7.108 +proof -
   7.109 +  show ?th1
   7.110 +    unfolding subset_eq and Ball_def and mem_box
   7.111 +    by (auto intro: order_trans)
   7.112 +  show ?th2
   7.113 +    unfolding subset_eq and Ball_def and mem_box
   7.114 +    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   7.115 +  {
   7.116 +    assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   7.117 +    then have "box c d \<noteq> {}"
   7.118 +      unfolding box_eq_empty by auto
   7.119 +    fix i :: 'a
   7.120 +    assume i: "i \<in> Basis"
   7.121 +    (** TODO combine the following two parts as done in the HOL_light version. **)
   7.122 +    {
   7.123 +      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   7.124 +      assume as2: "a\<bullet>i > c\<bullet>i"
   7.125 +      {
   7.126 +        fix j :: 'a
   7.127 +        assume j: "j \<in> Basis"
   7.128 +        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
   7.129 +          apply (cases "j = i")
   7.130 +          using as(2)[THEN bspec[where x=j]] i
   7.131 +          apply (auto simp add: as2)
   7.132 +          done
   7.133 +      }
   7.134 +      then have "?x\<in>box c d"
   7.135 +        using i unfolding mem_box by auto
   7.136 +      moreover
   7.137 +      have "?x \<notin> cbox a b"
   7.138 +        unfolding mem_box
   7.139 +        apply auto
   7.140 +        apply (rule_tac x=i in bexI)
   7.141 +        using as(2)[THEN bspec[where x=i]] and as2 i
   7.142 +        apply auto
   7.143 +        done
   7.144 +      ultimately have False using as by auto
   7.145 +    }
   7.146 +    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
   7.147 +    moreover
   7.148 +    {
   7.149 +      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   7.150 +      assume as2: "b\<bullet>i < d\<bullet>i"
   7.151 +      {
   7.152 +        fix j :: 'a
   7.153 +        assume "j\<in>Basis"
   7.154 +        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
   7.155 +          apply (cases "j = i")
   7.156 +          using as(2)[THEN bspec[where x=j]]
   7.157 +          apply (auto simp add: as2)
   7.158 +          done
   7.159 +      }
   7.160 +      then have "?x\<in>box c d"
   7.161 +        unfolding mem_box by auto
   7.162 +      moreover
   7.163 +      have "?x\<notin>cbox a b"
   7.164 +        unfolding mem_box
   7.165 +        apply auto
   7.166 +        apply (rule_tac x=i in bexI)
   7.167 +        using as(2)[THEN bspec[where x=i]] and as2 using i
   7.168 +        apply auto
   7.169 +        done
   7.170 +      ultimately have False using as by auto
   7.171 +    }
   7.172 +    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
   7.173 +    ultimately
   7.174 +    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
   7.175 +  } note part1 = this
   7.176 +  show ?th3
   7.177 +    unfolding subset_eq and Ball_def and mem_box
   7.178 +    apply (rule, rule, rule, rule)
   7.179 +    apply (rule part1)
   7.180 +    unfolding subset_eq and Ball_def and mem_box
   7.181 +    prefer 4
   7.182 +    apply auto
   7.183 +    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
   7.184 +    done
   7.185 +  {
   7.186 +    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   7.187 +    fix i :: 'a
   7.188 +    assume i:"i\<in>Basis"
   7.189 +    from as(1) have "box c d \<subseteq> cbox a b"
   7.190 +      using box_subset_cbox[of a b] by auto
   7.191 +    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   7.192 +      using part1 and as(2) using i by auto
   7.193 +  } note * = this
   7.194 +  show ?th4
   7.195 +    unfolding subset_eq and Ball_def and mem_box
   7.196 +    apply (rule, rule, rule, rule)
   7.197 +    apply (rule *)
   7.198 +    unfolding subset_eq and Ball_def and mem_box
   7.199 +    prefer 4
   7.200 +    apply auto
   7.201 +    apply (erule_tac x=xa in allE, simp)+
   7.202 +    done
   7.203 +qed
   7.204 +
   7.205 +lemma inter_interval:
   7.206 +  fixes a :: "'a::euclidean_space"
   7.207 +  shows "cbox a b \<inter> cbox c d =
   7.208 +    cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
   7.209 +  unfolding set_eq_iff and Int_iff and mem_box
   7.210 +  by auto
   7.211 +
   7.212 +lemma disjoint_interval:
   7.213 +  fixes a::"'a::euclidean_space"
   7.214 +  shows "cbox a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
   7.215 +    and "cbox a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
   7.216 +    and "box a b \<inter> cbox c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
   7.217 +    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
   7.218 +proof -
   7.219 +  let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
   7.220 +  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
   7.221 +      (\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)"
   7.222 +    by blast
   7.223 +  note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10)
   7.224 +  show ?th1 unfolding * by (intro **) auto
   7.225 +  show ?th2 unfolding * by (intro **) auto
   7.226 +  show ?th3 unfolding * by (intro **) auto
   7.227 +  show ?th4 unfolding * by (intro **) auto
   7.228 +qed
   7.229 +
   7.230 +text {* Intervals in general, including infinite and mixtures of open and closed. *}
   7.231 +
   7.232 +definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   7.233 +  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   7.234 +
   7.235 +lemma is_interval_cbox: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   7.236 +  and is_interval_box: "is_interval (box a b)" (is ?th2)
   7.237 +  unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
   7.238 +  by (meson order_trans le_less_trans less_le_trans less_trans)+
   7.239 +
   7.240 +lemma is_interval_empty:
   7.241 + "is_interval {}"
   7.242 +  unfolding is_interval_def
   7.243 +  by simp
   7.244 +
   7.245 +lemma is_interval_univ:
   7.246 + "is_interval UNIV"
   7.247 +  unfolding is_interval_def
   7.248 +  by simp
   7.249 +
   7.250 +lemma mem_is_intervalI:
   7.251 +  assumes "is_interval s"
   7.252 +  assumes "a \<in> s" "b \<in> s"
   7.253 +  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i"
   7.254 +  shows "x \<in> s"
   7.255 +  by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)])
   7.256 +
   7.257 +lemma interval_subst:
   7.258 +  fixes S::"'a::euclidean_space set"
   7.259 +  assumes "is_interval S"
   7.260 +  assumes "x \<in> S" "y j \<in> S"
   7.261 +  assumes "j \<in> Basis"
   7.262 +  shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S"
   7.263 +  by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms)
   7.264 +
   7.265 +lemma mem_box_componentwiseI:
   7.266 +  fixes S::"'a::euclidean_space set"
   7.267 +  assumes "is_interval S"
   7.268 +  assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)"
   7.269 +  shows "x \<in> S"
   7.270 +proof -
   7.271 +  from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i"
   7.272 +    by auto
   7.273 +  with finite_Basis obtain s and bs::"'a list" where
   7.274 +    s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S" and
   7.275 +    bs: "set bs = Basis" "distinct bs"
   7.276 +    by (metis finite_distinct_list)
   7.277 +  from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast
   7.278 +  def y \<equiv> "rec_list
   7.279 +    (s j)
   7.280 +    (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
   7.281 +  have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
   7.282 +    using bs by (auto simp add: s(1)[symmetric] euclidean_representation)
   7.283 +  also have [symmetric]: "y bs = \<dots>"
   7.284 +    using bs(2) bs(1)[THEN equalityD1]
   7.285 +    by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
   7.286 +  also have "y bs \<in> S"
   7.287 +    using bs(1)[THEN equalityD1]
   7.288 +    apply (induct bs)
   7.289 +    apply (auto simp: y_def j)
   7.290 +    apply (rule interval_subst[OF assms(1)])
   7.291 +    apply (auto simp: s)
   7.292 +    done
   7.293 +  finally show ?thesis .
   7.294 +qed
   7.295 +
   7.296  
   7.297  subsection{* Connectedness *}
   7.298  
   7.299 @@ -5937,51 +6219,6 @@
   7.300      done
   7.301  qed
   7.302  
   7.303 -subsection {* Intervals *}
   7.304 -
   7.305 -lemma open_box: "open (box a b)"
   7.306 -proof -
   7.307 -  have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
   7.308 -    by (auto intro!: continuous_open_vimage continuous_inner continuous_at_id continuous_const)
   7.309 -  also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
   7.310 -    by (auto simp add: box_def inner_commute)
   7.311 -  finally show ?thesis .
   7.312 -qed
   7.313 -
   7.314 -instance euclidean_space \<subseteq> second_countable_topology
   7.315 -proof
   7.316 -  def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
   7.317 -  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
   7.318 -    by simp
   7.319 -  def b \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. snd (f i) *\<^sub>R i"
   7.320 -  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
   7.321 -    by simp
   7.322 -  def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
   7.323 -
   7.324 -  have "Ball B open" by (simp add: B_def open_box)
   7.325 -  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
   7.326 -  proof safe
   7.327 -    fix A::"'a set"
   7.328 -    assume "open A"
   7.329 -    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
   7.330 -      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
   7.331 -      apply (subst (3) open_UNION_box[OF `open A`])
   7.332 -      apply (auto simp add: a b B_def)
   7.333 -      done
   7.334 -  qed
   7.335 -  ultimately
   7.336 -  have "topological_basis B"
   7.337 -    unfolding topological_basis_def by blast
   7.338 -  moreover
   7.339 -  have "countable B"
   7.340 -    unfolding B_def
   7.341 -    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
   7.342 -  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
   7.343 -    by (blast intro: topological_basis_imp_subbasis)
   7.344 -qed
   7.345 -
   7.346 -instance euclidean_space \<subseteq> polish_space ..
   7.347 -
   7.348  
   7.349  subsection {* Closure of halfspaces and hyperplanes *}
   7.350  
   7.351 @@ -6175,6 +6412,441 @@
   7.352    by (auto simp: inner_commute)
   7.353  
   7.354  
   7.355 +subsection {* Intervals *}
   7.356 +
   7.357 +lemma open_box[intro]: "open (box a b)"
   7.358 +proof -
   7.359 +  have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
   7.360 +    by (auto intro!: continuous_open_vimage continuous_inner continuous_at_id continuous_const)
   7.361 +  also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
   7.362 +    by (auto simp add: box_def inner_commute)
   7.363 +  finally show ?thesis .
   7.364 +qed
   7.365 +
   7.366 +instance euclidean_space \<subseteq> second_countable_topology
   7.367 +proof
   7.368 +  def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
   7.369 +  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f"
   7.370 +    by simp
   7.371 +  def b \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. snd (f i) *\<^sub>R i"
   7.372 +  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f"
   7.373 +    by simp
   7.374 +  def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^sub>E (\<rat> \<times> \<rat>))"
   7.375 +
   7.376 +  have "Ball B open" by (simp add: B_def open_box)
   7.377 +  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
   7.378 +  proof safe
   7.379 +    fix A::"'a set"
   7.380 +    assume "open A"
   7.381 +    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
   7.382 +      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
   7.383 +      apply (subst (3) open_UNION_box[OF `open A`])
   7.384 +      apply (auto simp add: a b B_def)
   7.385 +      done
   7.386 +  qed
   7.387 +  ultimately
   7.388 +  have "topological_basis B"
   7.389 +    unfolding topological_basis_def by blast
   7.390 +  moreover
   7.391 +  have "countable B"
   7.392 +    unfolding B_def
   7.393 +    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
   7.394 +  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
   7.395 +    by (blast intro: topological_basis_imp_subbasis)
   7.396 +qed
   7.397 +
   7.398 +instance euclidean_space \<subseteq> polish_space ..
   7.399 +
   7.400 +lemma closed_cbox[intro]:
   7.401 +  fixes a b :: "'a::euclidean_space"
   7.402 +  shows "closed (cbox a b)"
   7.403 +proof -
   7.404 +  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
   7.405 +    by (intro closed_INT ballI continuous_closed_vimage allI
   7.406 +      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
   7.407 +  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
   7.408 +    by (auto simp add: cbox_def)
   7.409 +  finally show "closed (cbox a b)" .
   7.410 +qed
   7.411 +
   7.412 +lemma interior_cbox [intro]:
   7.413 +  fixes a b :: "'a::euclidean_space"
   7.414 +  shows "interior (cbox a b) = box a b" (is "?L = ?R")
   7.415 +proof(rule subset_antisym)
   7.416 +  show "?R \<subseteq> ?L"
   7.417 +    using box_subset_cbox open_box
   7.418 +    by (rule interior_maximal)
   7.419 +  {
   7.420 +    fix x
   7.421 +    assume "x \<in> interior (cbox a b)"
   7.422 +    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> cbox a b" ..
   7.423 +    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> cbox a b"
   7.424 +      unfolding open_dist and subset_eq by auto
   7.425 +    {
   7.426 +      fix i :: 'a
   7.427 +      assume i: "i \<in> Basis"
   7.428 +      have "dist (x - (e / 2) *\<^sub>R i) x < e"
   7.429 +        and "dist (x + (e / 2) *\<^sub>R i) x < e"
   7.430 +        unfolding dist_norm
   7.431 +        apply auto
   7.432 +        unfolding norm_minus_cancel
   7.433 +        using norm_Basis[OF i] `e>0`
   7.434 +        apply auto
   7.435 +        done
   7.436 +      then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i"
   7.437 +        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
   7.438 +          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
   7.439 +        unfolding mem_box
   7.440 +        using i
   7.441 +        by blast+
   7.442 +      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
   7.443 +        using `e>0` i
   7.444 +        by (auto simp: inner_diff_left inner_Basis inner_add_left)
   7.445 +    }
   7.446 +    then have "x \<in> box a b"
   7.447 +      unfolding mem_box by auto
   7.448 +  }
   7.449 +  then show "?L \<subseteq> ?R" ..
   7.450 +qed
   7.451 +
   7.452 +lemma bounded_cbox:
   7.453 +  fixes a :: "'a::euclidean_space"
   7.454 +  shows "bounded (cbox a b)"
   7.455 +proof -
   7.456 +  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   7.457 +  {
   7.458 +    fix x :: "'a"
   7.459 +    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   7.460 +    {
   7.461 +      fix i :: 'a
   7.462 +      assume "i \<in> Basis"
   7.463 +      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   7.464 +        using x[THEN bspec[where x=i]] by auto
   7.465 +    }
   7.466 +    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
   7.467 +      apply -
   7.468 +      apply (rule setsum_mono)
   7.469 +      apply auto
   7.470 +      done
   7.471 +    then have "norm x \<le> ?b"
   7.472 +      using norm_le_l1[of x] by auto
   7.473 +  }
   7.474 +  then show ?thesis
   7.475 +    unfolding cbox_def bounded_iff by auto
   7.476 +qed
   7.477 +
   7.478 +lemma bounded_box:
   7.479 +  fixes a :: "'a::euclidean_space"
   7.480 +  shows "bounded (box a b)"
   7.481 +  using bounded_cbox[of a b]
   7.482 +  using box_subset_cbox[of a b]
   7.483 +  using bounded_subset[of "cbox a b" "box a b"]
   7.484 +  by simp
   7.485 +
   7.486 +lemma not_interval_univ:
   7.487 +  fixes a :: "'a::euclidean_space"
   7.488 +  shows "cbox a b \<noteq> UNIV" "box a b \<noteq> UNIV"
   7.489 +  using bounded_box[of a b] bounded_cbox[of a b] by auto
   7.490 +
   7.491 +lemma compact_cbox:
   7.492 +  fixes a :: "'a::euclidean_space"
   7.493 +  shows "compact (cbox a b)"
   7.494 +  using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b]
   7.495 +  by (auto simp: compact_eq_seq_compact_metric)
   7.496 +
   7.497 +lemma box_midpoint:
   7.498 +  fixes a :: "'a::euclidean_space"
   7.499 +  assumes "box a b \<noteq> {}"
   7.500 +  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
   7.501 +proof -
   7.502 +  {
   7.503 +    fix i :: 'a
   7.504 +    assume "i \<in> Basis"
   7.505 +    then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
   7.506 +      using assms[unfolded box_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
   7.507 +  }
   7.508 +  then show ?thesis unfolding mem_box by auto
   7.509 +qed
   7.510 +
   7.511 +lemma open_cbox_convex:
   7.512 +  fixes x :: "'a::euclidean_space"
   7.513 +  assumes x: "x \<in> box a b"
   7.514 +    and y: "y \<in> cbox a b"
   7.515 +    and e: "0 < e" "e \<le> 1"
   7.516 +  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
   7.517 +proof -
   7.518 +  {
   7.519 +    fix i :: 'a
   7.520 +    assume i: "i \<in> Basis"
   7.521 +    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
   7.522 +      unfolding left_diff_distrib by simp
   7.523 +    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   7.524 +      apply (rule add_less_le_mono)
   7.525 +      using e unfolding mult_less_cancel_left and mult_le_cancel_left
   7.526 +      apply simp_all
   7.527 +      using x unfolding mem_box using i
   7.528 +      apply simp
   7.529 +      using y unfolding mem_box using i
   7.530 +      apply simp
   7.531 +      done
   7.532 +    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
   7.533 +      unfolding inner_simps by auto
   7.534 +    moreover
   7.535 +    {
   7.536 +      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
   7.537 +        unfolding left_diff_distrib by simp
   7.538 +      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   7.539 +        apply (rule add_less_le_mono)
   7.540 +        using e unfolding mult_less_cancel_left and mult_le_cancel_left
   7.541 +        apply simp_all
   7.542 +        using x
   7.543 +        unfolding mem_box
   7.544 +        using i
   7.545 +        apply simp
   7.546 +        using y
   7.547 +        unfolding mem_box
   7.548 +        using i
   7.549 +        apply simp
   7.550 +        done
   7.551 +      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   7.552 +        unfolding inner_simps by auto
   7.553 +    }
   7.554 +    ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   7.555 +      by auto
   7.556 +  }
   7.557 +  then show ?thesis
   7.558 +    unfolding mem_box by auto
   7.559 +qed
   7.560 +
   7.561 +lemma closure_box:
   7.562 +  fixes a :: "'a::euclidean_space"
   7.563 +   assumes "box a b \<noteq> {}"
   7.564 +  shows "closure (box a b) = cbox a b"
   7.565 +proof -
   7.566 +  have ab: "a <e b"
   7.567 +    using assms by (simp add: eucl_less_def box_ne_empty)
   7.568 +  let ?c = "(1 / 2) *\<^sub>R (a + b)"
   7.569 +  {
   7.570 +    fix x
   7.571 +    assume as:"x \<in> cbox a b"
   7.572 +    def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
   7.573 +    {
   7.574 +      fix n
   7.575 +      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
   7.576 +      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
   7.577 +        unfolding inverse_le_1_iff by auto
   7.578 +      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
   7.579 +        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
   7.580 +        by (auto simp add: algebra_simps)
   7.581 +      then have "f n <e b" and "a <e f n"
   7.582 +        using open_cbox_convex[OF box_midpoint[OF assms] as *]
   7.583 +        unfolding f_def by (auto simp: box_def eucl_less_def)
   7.584 +      then have False
   7.585 +        using fn unfolding f_def using xc by auto
   7.586 +    }
   7.587 +    moreover
   7.588 +    {
   7.589 +      assume "\<not> (f ---> x) sequentially"
   7.590 +      {
   7.591 +        fix e :: real
   7.592 +        assume "e > 0"
   7.593 +        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
   7.594 +          using real_arch_inv[of e]
   7.595 +          apply (auto simp add: Suc_pred')
   7.596 +          apply (rule_tac x="n - 1" in exI)
   7.597 +          apply auto
   7.598 +          done
   7.599 +        then obtain N :: nat where "inverse (real (N + 1)) < e"
   7.600 +          by auto
   7.601 +        then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
   7.602 +          apply auto
   7.603 +          apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
   7.604 +            real_of_nat_Suc real_of_nat_Suc_gt_zero)
   7.605 +          done
   7.606 +        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
   7.607 +      }
   7.608 +      then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
   7.609 +        unfolding LIMSEQ_def by(auto simp add: dist_norm)
   7.610 +      then have "(f ---> x) sequentially"
   7.611 +        unfolding f_def
   7.612 +        using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   7.613 +        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
   7.614 +        by auto
   7.615 +    }
   7.616 +    ultimately have "x \<in> closure (box a b)"
   7.617 +      using as and box_midpoint[OF assms]
   7.618 +      unfolding closure_def
   7.619 +      unfolding islimpt_sequential
   7.620 +      by (cases "x=?c") (auto simp: in_box_eucl_less)
   7.621 +  }
   7.622 +  then show ?thesis
   7.623 +    using closure_minimal[OF box_subset_cbox, of a b] by blast
   7.624 +qed
   7.625 +
   7.626 +lemma bounded_subset_box_symmetric:
   7.627 +  fixes s::"('a::euclidean_space) set"
   7.628 +  assumes "bounded s"
   7.629 +  shows "\<exists>a. s \<subseteq> box (-a) a"
   7.630 +proof -
   7.631 +  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
   7.632 +    using assms[unfolded bounded_pos] by auto
   7.633 +  def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
   7.634 +  {
   7.635 +    fix x
   7.636 +    assume "x \<in> s"
   7.637 +    fix i :: 'a
   7.638 +    assume i: "i \<in> Basis"
   7.639 +    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
   7.640 +      using b[THEN bspec[where x=x], OF `x\<in>s`]
   7.641 +      using Basis_le_norm[OF i, of x]
   7.642 +      unfolding inner_simps and a_def
   7.643 +      by auto
   7.644 +  }
   7.645 +  then show ?thesis
   7.646 +    by (auto intro: exI[where x=a] simp add: box_def)
   7.647 +qed
   7.648 +
   7.649 +lemma bounded_subset_open_interval:
   7.650 +  fixes s :: "('a::euclidean_space) set"
   7.651 +  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   7.652 +  by (auto dest!: bounded_subset_box_symmetric)
   7.653 +
   7.654 +lemma bounded_subset_cbox_symmetric:
   7.655 +  fixes s :: "('a::euclidean_space) set"
   7.656 +   assumes "bounded s"
   7.657 +  shows "\<exists>a. s \<subseteq> cbox (-a) a"
   7.658 +proof -
   7.659 +  obtain a where "s \<subseteq> box (-a) a"
   7.660 +    using bounded_subset_box_symmetric[OF assms] by auto
   7.661 +  then show ?thesis
   7.662 +    using box_subset_cbox[of "-a" a] by auto
   7.663 +qed
   7.664 +
   7.665 +lemma bounded_subset_cbox:
   7.666 +  fixes s :: "('a::euclidean_space) set"
   7.667 +  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b"
   7.668 +  using bounded_subset_cbox_symmetric[of s] by auto
   7.669 +
   7.670 +lemma frontier_cbox:
   7.671 +  fixes a b :: "'a::euclidean_space"
   7.672 +  shows "frontier (cbox a b) = cbox a b - box a b"
   7.673 +  unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] ..
   7.674 +
   7.675 +lemma frontier_box:
   7.676 +  fixes a b :: "'a::euclidean_space"
   7.677 +  shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)"
   7.678 +proof (cases "box a b = {}")
   7.679 +  case True
   7.680 +  then show ?thesis
   7.681 +    using frontier_empty by auto
   7.682 +next
   7.683 +  case False
   7.684 +  then show ?thesis
   7.685 +    unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box]
   7.686 +    by auto
   7.687 +qed
   7.688 +
   7.689 +lemma inter_interval_mixed_eq_empty:
   7.690 +  fixes a :: "'a::euclidean_space"
   7.691 +   assumes "box c d \<noteq> {}"
   7.692 +  shows "box a b \<inter> cbox c d = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   7.693 +  unfolding closure_box[OF assms, symmetric]
   7.694 +  unfolding open_inter_closure_eq_empty[OF open_box] ..
   7.695 +
   7.696 +lemma diameter_cbox:
   7.697 +  fixes a b::"'a::euclidean_space"
   7.698 +  shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
   7.699 +  by (force simp add: diameter_def SUP_def simp del: Sup_image_eq intro!: cSup_eq_maximum setL2_mono
   7.700 +     simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
   7.701 +
   7.702 +lemma eucl_less_eq_halfspaces:
   7.703 +  fixes a :: "'a\<Colon>euclidean_space"
   7.704 +  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   7.705 +    "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   7.706 +  by (auto simp: eucl_less_def)
   7.707 +
   7.708 +lemma eucl_le_eq_halfspaces:
   7.709 +  fixes a :: "'a\<Colon>euclidean_space"
   7.710 +  shows "{x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
   7.711 +    "{x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
   7.712 +  by auto
   7.713 +
   7.714 +lemma open_Collect_eucl_less[simp, intro]:
   7.715 +  fixes a :: "'a\<Colon>euclidean_space"
   7.716 +  shows "open {x. x <e a}"
   7.717 +    "open {x. a <e x}"
   7.718 +  by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
   7.719 +
   7.720 +lemma closed_Collect_eucl_le[simp, intro]:
   7.721 +  fixes a :: "'a\<Colon>euclidean_space"
   7.722 +  shows "closed {x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i}"
   7.723 +    "closed {x. \<forall>i\<in>Basis. x \<bullet> i \<le> a \<bullet> i}"
   7.724 +  unfolding eucl_le_eq_halfspaces
   7.725 +  by (simp_all add: closed_INT closed_Collect_le)
   7.726 +
   7.727 +lemma image_affinity_cbox: fixes m::real
   7.728 +  fixes a b c :: "'a::euclidean_space"
   7.729 +  shows "(\<lambda>x. m *\<^sub>R x + c) ` cbox a b =
   7.730 +    (if cbox a b = {} then {}
   7.731 +     else (if 0 \<le> m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)
   7.732 +     else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))"
   7.733 +proof (cases "m = 0")
   7.734 +  case True
   7.735 +  {
   7.736 +    fix x
   7.737 +    assume "\<forall>i\<in>Basis. x \<bullet> i \<le> c \<bullet> i" "\<forall>i\<in>Basis. c \<bullet> i \<le> x \<bullet> i"
   7.738 +    then have "x = c"
   7.739 +      apply -
   7.740 +      apply (subst euclidean_eq_iff)
   7.741 +      apply (auto intro: order_antisym)
   7.742 +      done
   7.743 +  }
   7.744 +  moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
   7.745 +    unfolding True by (auto simp add: cbox_sing)
   7.746 +  ultimately show ?thesis using True by (auto simp: cbox_def)
   7.747 +next
   7.748 +  case False
   7.749 +  {
   7.750 +    fix y
   7.751 +    assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m > 0"
   7.752 +    then have "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
   7.753 +      by (auto simp: inner_distrib)
   7.754 +  }
   7.755 +  moreover
   7.756 +  {
   7.757 +    fix y
   7.758 +    assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m < 0"
   7.759 +    then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
   7.760 +      by (auto simp add: mult_left_mono_neg inner_distrib)
   7.761 +  }
   7.762 +  moreover
   7.763 +  {
   7.764 +    fix y
   7.765 +    assume "m > 0" and "\<forall>i\<in>Basis. (m *\<^sub>R a + c) \<bullet> i \<le> y \<bullet> i" and "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R b + c) \<bullet> i"
   7.766 +    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   7.767 +      unfolding image_iff Bex_def mem_box
   7.768 +      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   7.769 +      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   7.770 +      done
   7.771 +  }
   7.772 +  moreover
   7.773 +  {
   7.774 +    fix y
   7.775 +    assume "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i" "m < 0"
   7.776 +    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   7.777 +      unfolding image_iff Bex_def mem_box
   7.778 +      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   7.779 +      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   7.780 +      done
   7.781 +  }
   7.782 +  ultimately show ?thesis using False by (auto simp: cbox_def)
   7.783 +qed
   7.784 +
   7.785 +lemma image_smult_cbox:"(\<lambda>x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b =
   7.786 +  (if cbox a b = {} then {} else if 0 \<le> m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>R a))"
   7.787 +  using image_affinity_cbox[of m 0 a b] by auto
   7.788 +
   7.789 +
   7.790  subsection {* Homeomorphisms *}
   7.791  
   7.792  definition "homeomorphism s t f g \<longleftrightarrow>