--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jul 26 13:36:36 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jul 26 16:07:45 2017 +0100
@@ -46,6 +46,19 @@
lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
by (simp add: box_ne_empty inner_diff)
+lemma content_cbox_if: "content (cbox a b) = (if cbox a b = {} then 0 else \<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+ by (simp add: content_cbox')
+
+lemma content_division_of:
+ assumes "K \<in> \<D>" "\<D> division_of S"
+ shows "content K = (\<Prod>i \<in> Basis. interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)"
+proof -
+ obtain a b where "K = cbox a b"
+ using cbox_division_memE assms by metis
+ then show ?thesis
+ using assms by (force simp: division_of_def content_cbox')
+qed
+
lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
by simp