src/HOL/Multivariate_Analysis/Integration.thy

   where "One \<equiv> \<Sum>Basis"
 
 lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
   using nonempty_Basis
   by (fastforce simp add: set_eq_iff mem_box)
-
-lemma One_nonneg: "0 \<le> (One::'a::ordered_euclidean_space)"
-  by (auto intro: setsum_nonneg)
 
 lemma interior_subset_union_intervals:
   assumes "i = cbox a b"
     and "j = cbox c d"
     and "interior j \<noteq> {}"

   done
 
 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
   by (auto simp: interval_upperbound_def interval_lowerbound_def SUP_def INF_def content_def)
 
-lemma content_closed_interval:
-  fixes a :: "'a::ordered_euclidean_space"
-  assumes "a \<le> b"
-  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-  using content_cbox[of a b] assms
-  by (simp add: cbox_interval eucl_le[where 'a='a])
-
 lemma content_singleton[simp]: "content {a} = 0"
 proof -
   have "content (cbox a a) = 0"
     by (subst content_cbox) (auto simp: ex_in_conv)
   then show ?thesis by (simp add: cbox_sing)

 qed
 
 lemma elementary_bounded[dest]:
   fixes s :: "'a::euclidean_space set"
   shows "p division_of s \<Longrightarrow> bounded s"
-  unfolding division_of_def by (metis bounded_Union bounded_interval)
+  unfolding division_of_def by (metis bounded_Union bounded_cbox)
 
 lemma elementary_subset_cbox:
   "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
   by (meson elementary_bounded bounded_subset_cbox)
 

 
 
 subsection {* The set we're concerned with must be closed. *}
 
 lemma division_of_closed:
-  fixes i :: "'n::ordered_euclidean_space set"
+  fixes i :: "'n::euclidean_space set"
   shows "s division_of i \<Longrightarrow> closed i"
   unfolding division_of_def by fastforce
 
 subsection {* General bisection principle for intervals; might be useful elsewhere. *}
 

   show ?thesis
     apply (subst *)
     apply (rule tagged_division_union[OF assms(1-2)])
     unfolding interval_split[OF k] interior_cbox
     using k
-    apply (auto simp add: box elim!: ballE[where x=k])
+    apply (auto simp add: box_def elim!: ballE[where x=k])
     done
 qed
 
 lemma tagged_division_union_interval_real:
   fixes a :: real

   unfolding integrable_on_def
   apply rule
   apply (rule has_integral_const)
   done
 
-lemma integrable_const_ivl[intro]:
-  fixes a::"'a::ordered_euclidean_space"
-  shows "(\<lambda>x. c) integrable_on {a .. b}"
-  unfolding cbox_interval[symmetric]
-  by (rule integrable_const)
-
 lemma integral_has_vector_derivative:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "continuous_on {a .. b} f"
     and "x \<in> {a .. b}"
   shows "((\<lambda>u. integral {a .. u} f) has_vector_derivative f(x)) (at x within {a .. b})"

       apply auto
       done
   }
   assume "\<exists>a b. s = cbox a b"
   then guess a b by (elim exE) note s=this
-  from bounded_interval[of a b, THEN conjunct1, unfolded bounded_pos] guess B ..
+  from bounded_cbox[of a b, unfolded bounded_pos] guess B ..
   note B = conjunctD2[OF this,rule_format] show ?thesis
     apply safe
   proof -
     fix e :: real
     assume ?l and "e > 0"

   defer
   apply (rule integrable_altD(1)[OF assms(1)])
   using assms(2)
   apply auto
   done
-
-lemma integrable_on_subinterval:
-  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s"
-    and "{a .. b} \<subseteq> s"
-  shows "f integrable_on {a .. b}"
-  using integrable_on_subcbox[of f s a b] assms
-  by (simp add: cbox_interval)
 
 
 subsection {* A straddling criterion for integrability *}
 
 lemma integrable_straddle_interval: