# HG changeset patch
# User hoelzl
# Date 1470329128 -7200
# Node ID bbcb05504fdc90533386fc0d4d59fe4b5f5a742f
# Parent  64db21931bcbfadc84b0343d2b08dae5ac26db8e
HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.

diff -r 64db21931bcb -r bbcb05504fdc src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 03 11:45:09 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 04 18:45:28 2016 +0200
@@ -18,14 +18,13 @@
     shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
 proof -
   have fin: "finite {i \<in> I. u i \<noteq> 0}"
-    using 1 setsum.infinite by (force simp: supp_setsum_def support_def)
-  then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I =
-            setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
-    by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def)
+    using 1 setsum.infinite by (force simp: supp_setsum_def support_on_def)
+  then have eq: "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I = setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+    by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_on_def)
   show ?thesis
     apply (simp add: eq)
     apply (rule convex_setsum [OF fin \<open>convex S\<close>])
-    using 1 assms apply (auto simp: supp_setsum_def support_def)
+    using 1 assms apply (auto simp: supp_setsum_def support_on_def)
     done
 qed
 
@@ -7906,7 +7905,7 @@
   apply (simp add: rel_frontier_def)
   apply (simp add: rel_interior_eq_closure [symmetric])
   using rel_interior_subset_closure by blast
-  
+
 lemma rel_frontier_sing [simp]:
     fixes a :: "'n::euclidean_space"
     shows "rel_frontier {a} = {}"
diff -r 64db21931bcb -r bbcb05504fdc src/HOL/Multivariate_Analysis/Extension.thy
--- a/src/HOL/Multivariate_Analysis/Extension.thy	Wed Aug 03 11:45:09 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Extension.thy	Thu Aug 04 18:45:28 2016 +0200
@@ -27,7 +27,7 @@
     then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
     then show ?thesis
       apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
-      apply (auto simp: continuous_on_const supp_setsum_def support_def)
+      apply (auto simp: continuous_on_const supp_setsum_def support_on_def)
       done
 next
   case False
@@ -52,7 +52,7 @@
       have "x \<notin> closure (S - U)"
         by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
       then show ?thesis
-        apply (simp add: setdist_eq_0_sing_1 supp_setsum_def support_def)
+        apply (simp add: setdist_eq_0_sing_1 supp_setsum_def support_on_def)
         apply (rule ordered_comm_monoid_add_class.setsum_pos2 [OF *, of U])
         using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
         apply (auto simp: setdist_pos_le sd_pos that)
@@ -76,7 +76,7 @@
                      = supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>"
             apply (simp add: supp_setsum_def)
             apply (rule setsum.mono_neutral_right [OF finX])
-            apply (auto simp: setdist_eq_0_sing_1 support_def subset_iff)
+            apply (auto simp: setdist_eq_0_sing_1 support_on_def subset_iff)
             apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE)
             done
           show "continuous (at x within S) (\<lambda>x. supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>)"
@@ -461,7 +461,7 @@
             show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow>
                          (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))
                          = supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>"
-              by (auto simp: supp_setsum_def support_def
+              by (auto simp: supp_setsum_def support_on_def
                        intro: setsum.mono_neutral_right [OF finN])
           qed
         next
diff -r 64db21931bcb -r bbcb05504fdc src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Aug 03 11:45:09 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 04 18:45:28 2016 +0200
@@ -603,6 +603,63 @@
   by (simp add: content_0_subset_gen bounded_cbox)
 
 
+lemma interval_split:
+  fixes a :: "'a::euclidean_space"
+  assumes "k \<in> Basis"
+  shows
+    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
+    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
+  apply (rule_tac[!] set_eqI)
+  unfolding Int_iff mem_box mem_Collect_eq
+  using assms
+  apply auto
+  done
+
+lemma content_split:
+  fixes a :: "'a::euclidean_space"
+  assumes "k \<in> Basis"
+  shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+proof cases
+  note simps = interval_split[OF assms] content_cbox_cases
+  have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
+    using assms by auto
+  have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
+    "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
+    apply (subst *(1))
+    defer
+    apply (subst *(1))
+    unfolding setprod.insert[OF *(2-)]
+    apply auto
+    done
+  assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
+  moreover
+  have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
+    x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
+    by  (auto simp add: field_simps)
+  moreover
+  have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
+      (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
+    "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
+      (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
+    by (auto intro!: setprod.cong)
+  have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
+    unfolding not_le
+    using as[unfolded ,rule_format,of k] assms
+    by auto
+  ultimately show ?thesis
+    using assms
+    unfolding simps **
+    unfolding *(1)[of "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
+    unfolding *(2)
+    by auto
+next
+  assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+  then have "cbox a b = {}"
+    unfolding box_eq_empty by (auto simp: not_le)
+  then show ?thesis
+    by (auto simp: not_le)
+qed
+
 subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
 
 definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
@@ -1391,6 +1448,114 @@
   qed auto
 qed
 
+lemma division_split_left_inj:
+  fixes type :: "'a::euclidean_space"
+  assumes "d division_of i"
+    and "k1 \<in> d"
+    and "k2 \<in> d"
+    and "k1 \<noteq> k2"
+    and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
+    and k: "k\<in>Basis"
+  shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
+proof -
+  note d=division_ofD[OF assms(1)]
+  have *: "\<And>(a::'a) b c. content (cbox a b \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow>
+    interior(cbox a b \<inter> {x. x\<bullet>k \<le> c}) = {}"
+    unfolding  interval_split[OF k] content_eq_0_interior by auto
+  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
+  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
+  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
+    by auto
+  show ?thesis
+    unfolding uv1 uv2 *
+    apply (rule **[OF d(5)[OF assms(2-4)]])
+    apply (simp add: uv1)
+    using assms(5) uv1 by auto
+qed
+
+lemma division_split_right_inj:
+  fixes type :: "'a::euclidean_space"
+  assumes "d division_of i"
+    and "k1 \<in> d"
+    and "k2 \<in> d"
+    and "k1 \<noteq> k2"
+    and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+    and k: "k \<in> Basis"
+  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
+proof -
+  note d=division_ofD[OF assms(1)]
+  have *: "\<And>a b::'a. \<And>c. content(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
+    interior(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+    unfolding interval_split[OF k] content_eq_0_interior by auto
+  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
+  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
+  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
+    by auto
+  show ?thesis
+    unfolding uv1 uv2 *
+    apply (rule **[OF d(5)[OF assms(2-4)]])
+    apply (simp add: uv1)
+    using assms(5) uv1 by auto
+qed
+
+
+lemma division_split:
+  fixes a :: "'a::euclidean_space"
+  assumes "p division_of (cbox a b)"
+    and k: "k\<in>Basis"
+  shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} division_of(cbox a b \<inter> {x. x\<bullet>k \<le> c})"
+      (is "?p1 division_of ?I1")
+    and "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+      (is "?p2 division_of ?I2")
+proof (rule_tac[!] division_ofI)
+  note p = division_ofD[OF assms(1)]
+  show "finite ?p1" "finite ?p2"
+    using p(1) by auto
+  show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
+    unfolding p(6)[symmetric] by auto
+  {
+    fix k
+    assume "k \<in> ?p1"
+    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
+    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
+    show "k \<subseteq> ?I1"
+      using l p(2) uv by force
+    show  "k \<noteq> {}"
+      by (simp add: l)
+    show  "\<exists>a b. k = cbox a b"
+      apply (simp add: l uv p(2-3)[OF l(2)])
+      apply (subst interval_split[OF k])
+      apply (auto intro: order.trans)
+      done
+    fix k'
+    assume "k' \<in> ?p1"
+    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
+    assume "k \<noteq> k'"
+    then show "interior k \<inter> interior k' = {}"
+      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
+  }
+  {
+    fix k
+    assume "k \<in> ?p2"
+    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
+    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
+    show "k \<subseteq> ?I2"
+      using l p(2) uv by force
+    show  "k \<noteq> {}"
+      by (simp add: l)
+    show  "\<exists>a b. k = cbox a b"
+      apply (simp add: l uv p(2-3)[OF l(2)])
+      apply (subst interval_split[OF k])
+      apply (auto intro: order.trans)
+      done
+    fix k'
+    assume "k' \<in> ?p2"
+    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
+    assume "k \<noteq> k'"
+    then show "interior k \<inter> interior k' = {}"
+      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
+  }
+qed
 
 subsection \<open>Tagged (partial) divisions.\<close>
 
@@ -1503,17 +1668,17 @@
   using finite_subset[OF assms(2)]
   by blast
 
-lemma setsum_over_tagged_division_lemma:
+lemma (in comm_monoid_set) over_tagged_division_lemma:
   assumes "p tagged_division_of i"
-    and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = 0"
-  shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)"
+    and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = \<^bold>1"
+  shows "F (\<lambda>(x,k). d k) p = F d (snd ` p)"
 proof -
   have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
     unfolding o_def by (rule ext) auto
   note assm = tagged_division_ofD[OF assms(1)]
   show ?thesis
     unfolding *
-  proof (rule setsum.reindex_nontrivial[symmetric])
+  proof (rule reindex_nontrivial[symmetric])
     show "finite p"
       using assm by auto
     fix x y
@@ -1526,9 +1691,9 @@
       by (intro assm(5)[of "fst x" _ "fst y"]) auto
     then have "content (cbox a b) = 0"
       unfolding \<open>snd x = snd y\<close>[symmetric] ab content_eq_0_interior by auto
-    then have "d (cbox a b) = 0"
+    then have "d (cbox a b) = \<^bold>1"
       using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
-    then show "d (snd x) = 0"
+    then show "d (snd x) = \<^bold>1"
       unfolding ab by auto
   qed
 qed
@@ -1633,6 +1798,468 @@
   apply auto
   done
 
+subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
+
+text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
+  @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
+  @{typ bool}.\<close>
+
+lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
+  using content_empty unfolding empty_as_interval by auto
+
+paragraph \<open>Using additivity of lifted function to encode definedness.\<close>
+
+definition lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
+where
+  "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
+
+lemma lift_option_simps[simp]:
+  "lift_option f (Some a) (Some b) = Some (f a b)"
+  "lift_option f None b' = None"
+  "lift_option f a' None = None"
+  by (auto simp: lift_option_def)
+
+lemma (in comm_monoid) comm_monoid_lift_option: "comm_monoid (lift_option op \<^bold>*) (Some \<^bold>1)"
+  proof qed (auto simp: lift_option_def ac_simps split: bind_split)
+
+lemma (in comm_monoid) comm_monoid_set_lift_option: "comm_monoid_set (lift_option op \<^bold>*) (Some \<^bold>1)"
+  proof qed (auto simp: lift_option_def ac_simps split: bind_split)
+
+lemma comm_monoid_and: "comm_monoid op \<and> True"
+  proof qed auto
+
+lemma comm_monoid_set_and: "comm_monoid_set op \<and> True"
+  proof qed auto
+
+paragraph \<open>Operative\<close>
+
+definition (in comm_monoid) operative :: "('b::euclidean_space set \<Rightarrow> 'a) \<Rightarrow> bool"
+  where "operative g \<longleftrightarrow>
+    (\<forall>a b. content (cbox a b) = 0 \<longrightarrow> g (cbox a b) = \<^bold>1) \<and>
+    (\<forall>a b c. \<forall>k\<in>Basis. g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c}))"
+
+lemma (in comm_monoid) operativeD[dest]:
+  assumes "operative g"
+  shows "\<And>a b. content (cbox a b) = 0 \<Longrightarrow> g (cbox a b) = \<^bold>1"
+    and "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+  using assms unfolding operative_def by auto
+
+lemma (in comm_monoid) operative_empty: "operative g \<Longrightarrow> g {} = \<^bold>1"
+  unfolding operative_def by (rule property_empty_interval) auto
+
+lemma operative_content[intro]: "add.operative content"
+  by (force simp add: add.operative_def content_split[symmetric])
+
+definition "division_points (k::('a::euclidean_space) set) d =
+   {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
+     (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
+
+lemma division_points_finite:
+  fixes i :: "'a::euclidean_space set"
+  assumes "d division_of i"
+  shows "finite (division_points i d)"
+proof -
+  note assm = division_ofD[OF assms]
+  let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
+    (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
+  have *: "division_points i d = \<Union>(?M ` Basis)"
+    unfolding division_points_def by auto
+  show ?thesis
+    unfolding * using assm by auto
+qed
+
+lemma division_points_subset:
+  fixes a :: "'a::euclidean_space"
+  assumes "d division_of (cbox a b)"
+    and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
+    and k: "k \<in> Basis"
+  shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l . l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subseteq>
+      division_points (cbox a b) d" (is ?t1)
+    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
+      division_points (cbox a b) d" (is ?t2)
+proof -
+  note assm = division_ofD[OF assms(1)]
+  have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+    "\<forall>i\<in>Basis. a\<bullet>i \<le> (\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else  b \<bullet> i) *\<^sub>R i) \<bullet> i"
+    "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i \<le> b\<bullet>i"
+    "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
+    using assms using less_imp_le by auto
+  show ?t1 (*FIXME a horrible mess*)
+    unfolding division_points_def interval_split[OF k, of a b]
+    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
+    unfolding *
+    apply (rule subsetI)
+    unfolding mem_Collect_eq split_beta
+    apply (erule bexE conjE)+
+    apply (simp add: )
+    apply (erule exE conjE)+
+  proof
+    fix i l x
+    assume as:
+      "a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
+      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
+      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
+      and fstx: "fst x \<in> Basis"
+    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
+    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
+      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
+    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+      using l using as(6) unfolding box_ne_empty[symmetric] by auto
+    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
+      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
+      using as(1-3,5) fstx
+      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
+      apply (auto split: if_split_asm)
+      done
+    show "snd x < b \<bullet> fst x"
+      using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
+  qed
+  show ?t2
+    unfolding division_points_def interval_split[OF k, of a b]
+    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
+    unfolding *
+    unfolding subset_eq
+    apply rule
+    unfolding mem_Collect_eq split_beta
+    apply (erule bexE conjE)+
+    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
+    apply (erule exE conjE)+
+  proof
+    fix i l x
+    assume as:
+      "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
+      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
+      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
+      and fstx: "fst x \<in> Basis"
+    from assm(4)[OF this(5)] guess u v by (elim exE) note l=this
+    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
+      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
+    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
+      using l using as(6) unfolding box_ne_empty[symmetric] by auto
+    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
+      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
+      using as(1-3,5) fstx
+      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
+      apply (auto split: if_split_asm)
+      done
+    show "a \<bullet> fst x < snd x"
+      using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
+   qed
+qed
+
+lemma division_points_psubset:
+  fixes a :: "'a::euclidean_space"
+  assumes "d division_of (cbox a b)"
+      and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
+      and "l \<in> d"
+      and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
+      and k: "k \<in> Basis"
+  shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subset>
+         division_points (cbox a b) d" (is "?D1 \<subset> ?D")
+    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
+         division_points (cbox a b) d" (is "?D2 \<subset> ?D")
+proof -
+  have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+    using assms(2) by (auto intro!:less_imp_le)
+  guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
+  have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
+    using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty
+    using subset_box(1)
+    apply auto
+    apply blast+
+    done
+  have *: "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
+          "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
+    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
+    using uv[rule_format, of k] ab k
+    by auto
+  have "\<exists>x. x \<in> ?D - ?D1"
+    using assms(3-)
+    unfolding division_points_def interval_bounds[OF ab]
+    apply -
+    apply (erule disjE)
+    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
+    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
+    done
+  moreover have "?D1 \<subseteq> ?D"
+    by (auto simp add: assms division_points_subset)
+  ultimately show "?D1 \<subset> ?D"
+    by blast
+  have *: "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
+    "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
+    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
+    using uv[rule_format, of k] ab k
+    by auto
+  have "\<exists>x. x \<in> ?D - ?D2"
+    using assms(3-)
+    unfolding division_points_def interval_bounds[OF ab]
+    apply -
+    apply (erule disjE)
+    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
+    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
+    done
+  moreover have "?D2 \<subseteq> ?D"
+    by (auto simp add: assms division_points_subset)
+  ultimately show "?D2 \<subset> ?D"
+    by blast
+qed
+
+lemma (in comm_monoid_set) operative_division:
+  fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
+  assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)"
+proof -
+  define C where [abs_def]: "C = card (division_points (cbox a b) d)"
+  then show ?thesis
+    using d
+  proof (induction C arbitrary: a b d rule: less_induct)
+    case (less a b d)
+    show ?case
+    proof cases
+      show "content (cbox a b) = 0 \<Longrightarrow> F g d = g (cbox a b)"
+        using division_of_content_0[OF _ less.prems] operativeD(1)[OF  g] division_ofD(4)[OF less.prems]
+        by (fastforce intro!: neutral)
+    next
+      assume "content (cbox a b) \<noteq> 0"
+      note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
+      then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+        by (auto intro!: less_imp_le)
+      show "F g d = g (cbox a b)"
+      proof (cases "division_points (cbox a b) d = {}")
+        case True
+        { fix u v and j :: 'b
+          assume j: "j \<in> Basis" and as: "cbox u v \<in> d"
+          then have "cbox u v \<noteq> {}"
+            using less.prems by blast
+          then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
+            using j unfolding box_ne_empty by auto
+          have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q (cbox u v)"
+            using as j by auto
+          have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
+               "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
+          note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
+          note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
+          moreover
+          have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
+            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
+            apply (metis j subset_box(1) uv(1))
+            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
+          ultimately have "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
+            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
+        then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
+          (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
+          unfolding forall_in_division[OF less.prems] by blast
+        have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
+          unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
+        note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
+        then guess i .. note i=this
+        guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
+        have "cbox a b \<in> d"
+        proof -
+          have "u = a" "v = b"
+            unfolding euclidean_eq_iff[where 'a='b]
+          proof safe
+            fix j :: 'b
+            assume j: "j \<in> Basis"
+            note i(2)[unfolded uv mem_box,rule_format,of j]
+            then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
+              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
+          qed
+          then have "i = cbox a b" using uv by auto
+          then show ?thesis using i by auto
+        qed
+        then have deq: "d = insert (cbox a b) (d - {cbox a b})"
+          by auto
+        have "F g (d - {cbox a b}) = \<^bold>1"
+        proof (intro neutral ballI)
+          fix x
+          assume x: "x \<in> d - {cbox a b}"
+          then have "x\<in>d"
+            by auto note d'[rule_format,OF this]
+          then guess u v by (elim exE conjE) note uv=this
+          have "u \<noteq> a \<or> v \<noteq> b"
+            using x[unfolded uv] by auto
+          then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
+            unfolding euclidean_eq_iff[where 'a='b] by auto
+          then have "u\<bullet>j = v\<bullet>j"
+            using uv(2)[rule_format,OF j] by auto
+          then have "content (cbox u v) = 0"
+            unfolding content_eq_0 using j
+            by force
+          then show "g x = \<^bold>1"
+            unfolding uv(1) by (rule operativeD(1)[OF g])
+        qed
+        then show "F g d = g (cbox a b)"
+          using division_ofD[OF less.prems]
+          apply (subst deq)
+          apply (subst insert)
+          apply auto
+          done
+      next
+        case False
+        then have "\<exists>x. x \<in> division_points (cbox a b) d"
+          by auto
+        then guess k c
+          unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv
+          apply (elim exE conjE)
+          done
+        note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
+        from this(3) guess j .. note j=this
+        define d1 where "d1 = {l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+        define d2 where "d2 = {l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+        define cb where "cb = (\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)"
+        define ca where "ca = (\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)"
+        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
+        note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
+        then have *: "F g d1 = g (cbox a b \<inter> {x. x\<bullet>k \<le> c})" "F g d2 = g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+          unfolding interval_split[OF kc(4)]
+          apply (rule_tac[!] "less.hyps"[rule_format])
+          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
+          apply (simp_all add: interval_split kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
+          done
+        { fix l y
+          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
+          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
+          have "g (l \<inter> {x. x \<bullet> k \<le> c}) = \<^bold>1"
+            unfolding leq interval_split[OF kc(4)]
+            apply (rule operativeD[OF g])
+            unfolding interval_split[symmetric, OF kc(4)]
+            using division_split_left_inj less as kc leq by blast
+        } note fxk_le = this
+        { fix l y
+          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
+          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
+          have "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
+            unfolding leq interval_split[OF kc(4)]
+            apply (rule operativeD(1)[OF g])
+            unfolding interval_split[symmetric,OF kc(4)]
+            using division_split_right_inj less leq as kc by blast
+        } note fxk_ge = this
+        have d1_alt: "d1 = (\<lambda>l. l \<inter> {x. x\<bullet>k \<le> c}) ` {l \<in> d. l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+          using d1_def by auto
+        have d2_alt: "d2 = (\<lambda>l. l \<inter> {x. x\<bullet>k \<ge> c}) ` {l \<in> d. l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+          using d2_def by auto
+        have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
+          unfolding * using g kc(4) by blast
+        also have "F g d1 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d"
+          unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
+          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
+        also have "F g d2 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d"
+          unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
+          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
+        also have *: "\<forall>x\<in>d. g x = g (x \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (x \<inter> {x. c \<le> x \<bullet> k})"
+          unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
+          using g kc(4) by blast
+        have "F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d \<^bold>* F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d = F g d"
+          using * by (simp add: distrib)
+        finally show ?thesis by auto
+      qed
+    qed
+  qed
+qed
+
+lemma (in comm_monoid_set) operative_tagged_division:
+  assumes f: "operative g" and d: "d tagged_division_of (cbox a b)"
+  shows "F (\<lambda>(x, l). g l) d = g (cbox a b)"
+  unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric]
+  by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d])
+
+lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)"
+  by (metis operative_content setsum.operative_division)
+
+lemma additive_content_tagged_division:
+  "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
+  unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
+
+lemma
+  shows real_inner_1_left: "inner 1 x = x"
+  and real_inner_1_right: "inner x 1 = x"
+  by simp_all
+
+lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
+  by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
+
+lemma interval_real_split:
+  "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
+  "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
+  apply (metis Int_atLeastAtMostL1 atMost_def)
+  apply (metis Int_atLeastAtMostL2 atLeast_def)
+  done
+
+lemma (in comm_monoid) operative_1_lt:
+  "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
+    ((\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1) \<and> (\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
+  apply (simp add: operative_def content_real_eq_0 atMost_def[symmetric] atLeast_def[symmetric]
+              del: content_real_if)
+proof safe
+  fix a b c :: real
+  assume *: "\<forall>a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
+  assume "a < c" "c < b"
+  with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
+    by (simp add: less_imp_le min.absorb2 max.absorb2)
+next
+  fix a b c :: real
+  assume as: "\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1"
+    "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+  from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2)
+  have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
+    "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+    by auto
+  show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
+    by (auto simp: min_def max_def le_less)
+qed
+
+lemma (in comm_monoid) operative_1_le:
+  "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
+    ((\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1) \<and> (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
+  unfolding operative_1_lt
+proof safe
+  fix a b c :: real
+  assume as: "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}" "a < c" "c < b"
+  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
+    apply (rule as(1)[rule_format])
+    using as(2-)
+    apply auto
+    done
+next
+  fix a b c :: real
+  assume "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
+    and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+    and "a \<le> c"
+    and "c \<le> b"
+  note as = this[rule_format]
+  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
+  proof (cases "c = a \<or> c = b")
+    case False
+    then show ?thesis
+      apply -
+      apply (subst as(2))
+      using as(3-)
+      apply auto
+      done
+  next
+    case True
+    then show ?thesis
+    proof
+      assume *: "c = a"
+      then have "g {a .. c} = \<^bold>1"
+        apply -
+        apply (rule as(1)[rule_format])
+        apply auto
+        done
+      then show ?thesis
+        unfolding * by auto
+    next
+      assume *: "c = b"
+      then have "g {c .. b} = \<^bold>1"
+        apply -
+        apply (rule as(1)[rule_format])
+        apply auto
+        done
+      then show ?thesis
+        unfolding * by auto
+    qed
+  qed
+qed
 
 subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
 
@@ -2993,113 +3620,6 @@
 
 subsection \<open>Additivity of integral on abutting intervals.\<close>
 
-lemma interval_split:
-  fixes a :: "'a::euclidean_space"
-  assumes "k \<in> Basis"
-  shows
-    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
-    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
-  apply (rule_tac[!] set_eqI)
-  unfolding Int_iff mem_box mem_Collect_eq
-  using assms
-  apply auto
-  done
-
-lemma content_split:
-  fixes a :: "'a::euclidean_space"
-  assumes "k \<in> Basis"
-  shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-proof cases
-  note simps = interval_split[OF assms] content_cbox_cases
-  have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
-    using assms by auto
-  have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
-    "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
-    apply (subst *(1))
-    defer
-    apply (subst *(1))
-    unfolding setprod.insert[OF *(2-)]
-    apply auto
-    done
-  assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-  moreover
-  have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
-    x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
-    by  (auto simp add: field_simps)
-  moreover
-  have **: "(\<Prod>i\<in>Basis. ((\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) *\<^sub>R i) \<bullet> i - a \<bullet> i)) =
-      (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
-    "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
-      (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
-    by (auto intro!: setprod.cong)
-  have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
-    unfolding not_le
-    using as[unfolded ,rule_format,of k] assms
-    by auto
-  ultimately show ?thesis
-    using assms
-    unfolding simps **
-    unfolding *(1)[of "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
-    unfolding *(2)
-    by auto
-next
-  assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
-  then have "cbox a b = {}"
-    unfolding box_eq_empty by (auto simp: not_le)
-  then show ?thesis
-    by (auto simp: not_le)
-qed
-
-lemma division_split_left_inj:
-  fixes type :: "'a::euclidean_space"
-  assumes "d division_of i"
-    and "k1 \<in> d"
-    and "k2 \<in> d"
-    and "k1 \<noteq> k2"
-    and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
-    and k: "k\<in>Basis"
-  shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
-proof -
-  note d=division_ofD[OF assms(1)]
-  have *: "\<And>(a::'a) b c. content (cbox a b \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow>
-    interior(cbox a b \<inter> {x. x\<bullet>k \<le> c}) = {}"
-    unfolding  interval_split[OF k] content_eq_0_interior by auto
-  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
-  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
-  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
-    by auto
-  show ?thesis
-    unfolding uv1 uv2 *
-    apply (rule **[OF d(5)[OF assms(2-4)]])
-    apply (simp add: uv1)
-    using assms(5) uv1 by auto
-qed
-
-lemma division_split_right_inj:
-  fixes type :: "'a::euclidean_space"
-  assumes "d division_of i"
-    and "k1 \<in> d"
-    and "k2 \<in> d"
-    and "k1 \<noteq> k2"
-    and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
-    and k: "k \<in> Basis"
-  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
-proof -
-  note d=division_ofD[OF assms(1)]
-  have *: "\<And>a b::'a. \<And>c. content(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
-    interior(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-    unfolding interval_split[OF k] content_eq_0_interior by auto
-  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
-  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
-  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
-    by auto
-  show ?thesis
-    unfolding uv1 uv2 *
-    apply (rule **[OF d(5)[OF assms(2-4)]])
-    apply (simp add: uv1)
-    using assms(5) uv1 by auto
-qed
-
 lemma tagged_division_split_left_inj:
   fixes x1 :: "'a::euclidean_space"
   assumes d: "d tagged_division_of i"
@@ -3134,64 +3654,6 @@
     by (fastforce intro!:  division_split_right_inj[OF division_of_tagged_division[OF d]] *)
 qed
 
-lemma division_split:
-  fixes a :: "'a::euclidean_space"
-  assumes "p division_of (cbox a b)"
-    and k: "k\<in>Basis"
-  shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} division_of(cbox a b \<inter> {x. x\<bullet>k \<le> c})"
-      (is "?p1 division_of ?I1")
-    and "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-      (is "?p2 division_of ?I2")
-proof (rule_tac[!] division_ofI)
-  note p = division_ofD[OF assms(1)]
-  show "finite ?p1" "finite ?p2"
-    using p(1) by auto
-  show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
-    unfolding p(6)[symmetric] by auto
-  {
-    fix k
-    assume "k \<in> ?p1"
-    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
-    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
-    show "k \<subseteq> ?I1"
-      using l p(2) uv by force
-    show  "k \<noteq> {}"
-      by (simp add: l)
-    show  "\<exists>a b. k = cbox a b"
-      apply (simp add: l uv p(2-3)[OF l(2)])
-      apply (subst interval_split[OF k])
-      apply (auto intro: order.trans)
-      done
-    fix k'
-    assume "k' \<in> ?p1"
-    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
-    assume "k \<noteq> k'"
-    then show "interior k \<inter> interior k' = {}"
-      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
-  }
-  {
-    fix k
-    assume "k \<in> ?p2"
-    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
-    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
-    show "k \<subseteq> ?I2"
-      using l p(2) uv by force
-    show  "k \<noteq> {}"
-      by (simp add: l)
-    show  "\<exists>a b. k = cbox a b"
-      apply (simp add: l uv p(2-3)[OF l(2)])
-      apply (subst interval_split[OF k])
-      apply (auto intro: order.trans)
-      done
-    fix k'
-    assume "k' \<in> ?p2"
-    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
-    assume "k \<noteq> k'"
-    then show "interior k \<inter> interior k' = {}"
-      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
-  }
-qed
-
 lemma has_integral_split:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes fi: "(f has_integral i) (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
@@ -3562,48 +4024,16 @@
   qed
 qed
 
-
-subsection \<open>Generalized notion of additivity.\<close>
-
-definition operative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (('b::euclidean_space) set \<Rightarrow> 'a) \<Rightarrow> bool"
-  where "operative opp f \<longleftrightarrow>
-    (\<forall>a b. content (cbox a b) = 0 \<longrightarrow> f (cbox a b) = neutral opp) \<and>
-    (\<forall>a b c. \<forall>k\<in>Basis. f (cbox a b) = opp (f(cbox a b \<inter> {x. x\<bullet>k \<le> c})) (f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})))"
-
-lemma operativeD[dest]:
-  fixes type :: "'a::euclidean_space"
-  assumes "operative opp f"
-  shows "\<And>a b::'a. content (cbox a b) = 0 \<Longrightarrow> f (cbox a b) = neutral opp"
-    and "\<And>a b c k. k \<in> Basis \<Longrightarrow> f (cbox a b) =
-      opp (f (cbox a b \<inter> {x. x\<bullet>k \<le> c})) (f (cbox a b \<inter> {x. x\<bullet>k \<ge> c}))"
-  using assms unfolding operative_def by auto
-
-lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
-  using content_empty unfolding empty_as_interval by auto
-
-lemma operative_empty: "operative opp f \<Longrightarrow> f {} = neutral opp"
-  unfolding operative_def by (rule property_empty_interval) auto
-
-
-subsection \<open>Two key instances of additivity.\<close>
-
-lemma operative_content[intro]: "operative (op +) content"
-  by (force simp add: operative_def content_split[symmetric])
-
-lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
-  unfolding monoidal_def neutral_add
-  by (auto simp add: algebra_simps)
-
 lemma operative_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
-  shows "operative (lifted(op +)) (\<lambda>i. if f integrable_on i then Some(integral i f) else None)"
-  unfolding operative_def neutral_lifted[OF monoidal_monoid] neutral_add
+  shows "comm_monoid.operative (lift_option op +) (Some 0) (\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
+  unfolding comm_monoid.operative_def[OF add.comm_monoid_lift_option]
 proof safe
   fix a b c
   fix k :: 'a
   assume k: "k \<in> Basis"
   show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) =
-        lifted op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
+        lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
         (if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
   proof (cases "f integrable_on cbox a b")
     case True
@@ -3637,498 +4067,6 @@
     by (auto simp: integrable_on_null)
 qed
 
-
-subsection \<open>Points of division of a partition.\<close>
-
-definition "division_points (k::('a::euclidean_space) set) d =
-   {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
-     (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
-
-lemma division_points_finite:
-  fixes i :: "'a::euclidean_space set"
-  assumes "d division_of i"
-  shows "finite (division_points i d)"
-proof -
-  note assm = division_ofD[OF assms]
-  let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
-    (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
-  have *: "division_points i d = \<Union>(?M ` Basis)"
-    unfolding division_points_def by auto
-  show ?thesis
-    unfolding * using assm by auto
-qed
-
-lemma division_points_subset:
-  fixes a :: "'a::euclidean_space"
-  assumes "d division_of (cbox a b)"
-    and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
-    and k: "k \<in> Basis"
-  shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l . l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subseteq>
-      division_points (cbox a b) d" (is ?t1)
-    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
-      division_points (cbox a b) d" (is ?t2)
-proof -
-  note assm = division_ofD[OF assms(1)]
-  have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-    "\<forall>i\<in>Basis. a\<bullet>i \<le> (\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else  b \<bullet> i) *\<^sub>R i) \<bullet> i"
-    "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i \<le> b\<bullet>i"
-    "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
-    using assms using less_imp_le by auto
-  show ?t1 (*FIXME a horrible mess*)
-    unfolding division_points_def interval_split[OF k, of a b]
-    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
-    unfolding *
-    apply (rule subsetI)
-    unfolding mem_Collect_eq split_beta
-    apply (erule bexE conjE)+
-    apply (simp add: )
-    apply (erule exE conjE)+
-  proof
-    fix i l x
-    assume as:
-      "a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
-      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
-      and fstx: "fst x \<in> Basis"
-    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
-    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
-      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
-    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
-      using l using as(6) unfolding box_ne_empty[symmetric] by auto
-    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
-      using as(1-3,5) fstx
-      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
-      apply (auto split: if_split_asm)
-      done
-    show "snd x < b \<bullet> fst x"
-      using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
-  qed
-  show ?t2
-    unfolding division_points_def interval_split[OF k, of a b]
-    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
-    unfolding *
-    unfolding subset_eq
-    apply rule
-    unfolding mem_Collect_eq split_beta
-    apply (erule bexE conjE)+
-    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
-    apply (erule exE conjE)+
-  proof
-    fix i l x
-    assume as:
-      "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
-      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
-      and fstx: "fst x \<in> Basis"
-    from assm(4)[OF this(5)] guess u v by (elim exE) note l=this
-    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
-      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
-    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
-      using l using as(6) unfolding box_ne_empty[symmetric] by auto
-    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
-      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
-      using as(1-3,5) fstx
-      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
-      apply (auto split: if_split_asm)
-      done
-    show "a \<bullet> fst x < snd x"
-      using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
-   qed
-qed
-
-lemma division_points_psubset:
-  fixes a :: "'a::euclidean_space"
-  assumes "d division_of (cbox a b)"
-      and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
-      and "l \<in> d"
-      and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
-      and k: "k \<in> Basis"
-  shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subset>
-         division_points (cbox a b) d" (is "?D1 \<subset> ?D")
-    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
-         division_points (cbox a b) d" (is "?D2 \<subset> ?D")
-proof -
-  have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-    using assms(2) by (auto intro!:less_imp_le)
-  guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
-  have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
-    using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty
-    using subset_box(1)
-    apply auto
-    apply blast+
-    done
-  have *: "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
-          "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
-    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
-    using uv[rule_format, of k] ab k
-    by auto
-  have "\<exists>x. x \<in> ?D - ?D1"
-    using assms(3-)
-    unfolding division_points_def interval_bounds[OF ab]
-    apply -
-    apply (erule disjE)
-    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
-    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
-    done
-  moreover have "?D1 \<subseteq> ?D"
-    by (auto simp add: assms division_points_subset)
-  ultimately show "?D1 \<subset> ?D"
-    by blast
-  have *: "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
-    "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
-    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
-    using uv[rule_format, of k] ab k
-    by auto
-  have "\<exists>x. x \<in> ?D - ?D2"
-    using assms(3-)
-    unfolding division_points_def interval_bounds[OF ab]
-    apply -
-    apply (erule disjE)
-    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
-    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
-    done
-  moreover have "?D2 \<subseteq> ?D"
-    by (auto simp add: assms division_points_subset)
-  ultimately show "?D2 \<subset> ?D"
-    by blast
-qed
-
-
-subsection \<open>Preservation by divisions and tagged divisions.\<close>
-
-lemma support_support[simp]:"support opp f (support opp f s) = support opp f s"
-  unfolding support_def by auto
-
-lemma iterate_support[simp]: "iterate opp (support opp f s) f = iterate opp s f"
-  unfolding iterate_def support_support by auto
-
-lemma iterate_expand_cases:
-  "iterate opp s f = (if finite(support opp f s) then iterate opp (support opp f s) f else neutral opp)"
-    by (simp add: iterate_def fold'_def)
-
-lemma iterate_image:
-  assumes "monoidal opp"
-    and "inj_on f s"
-  shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-proof -
-  have *: "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-    if "finite s" "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<longrightarrow> x = y" for s
-    using that
-  proof (induct s)
-    case empty
-    then show ?case by simp
-  next
-    case insert
-    with assms(1) show ?case by auto
-  qed
-  show ?thesis
-    apply (cases "finite (support opp g (f ` s))")
-    prefer 2
-      apply (metis finite_imageI iterate_expand_cases support_clauses(7))
-    apply (subst (1) iterate_support[symmetric], subst (2) iterate_support[symmetric])
-    unfolding support_clauses
-    apply (rule *)
-    apply (meson assms(2) finite_imageD subset_inj_on support_subset)
-    apply (meson assms(2) inj_on_contraD rev_subsetD support_subset)
-    done
-qed
-
-
-(* This lemma about iterations comes up in a few places. *)
-lemma iterate_nonzero_image_lemma:
-  assumes "monoidal opp"
-    and "finite s" "g(a) = neutral opp"
-    and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g(f x) = neutral opp"
-  shows "iterate opp {f x | x. x \<in> s \<and> f x \<noteq> a} g = iterate opp s (g \<circ> f)"
-proof -
-  have *: "{f x |x. x \<in> s \<and> f x \<noteq> a} = f ` {x. x \<in> s \<and> f x \<noteq> a}"
-    by auto
-  have **: "support opp (g \<circ> f) {x \<in> s. f x \<noteq> a} = support opp (g \<circ> f) s"
-    unfolding support_def using assms(3) by auto
-  have inj: "inj_on f (support opp (g \<circ> f) {x \<in> s. f x \<noteq> a})"
-    apply (simp add: inj_on_def)
-    apply (metis (mono_tags, lifting) assms(4) comp_def mem_Collect_eq support_def)
-    done
-  show ?thesis
-    apply (subst iterate_support[symmetric])
-    apply (simp add: * support_clauses iterate_image[OF assms(1) inj])
-    apply (simp add: iterate_def **)
-    done
-qed
-
-lemma iterate_eq_neutral:
-  assumes "monoidal opp"
-      and "\<And>x. x \<in> s \<Longrightarrow> f x = neutral opp"
-    shows "iterate opp s f = neutral opp"
-proof -
-  have [simp]: "support opp f s = {}"
-    unfolding support_def using assms(2) by auto
-  show ?thesis
-    by (subst iterate_support[symmetric]) simp
-qed
-
-lemma iterate_op:
-   "\<lbrakk>monoidal opp; finite s\<rbrakk>
-    \<Longrightarrow> iterate opp s (\<lambda>x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)"
-by (erule finite_induct) (auto simp: monoidal_ac(4) monoidal_ac(5))
-
-lemma iterate_eq:
-  assumes "monoidal opp"
-    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
-  shows "iterate opp s f = iterate opp s g"
-proof -
-  have *: "support opp g s = support opp f s"
-    unfolding support_def using assms(2) by auto
-  show ?thesis
-  proof (cases "finite (support opp f s)")
-    case False
-    then show ?thesis
-      by (simp add: "*" iterate_expand_cases)
-  next
-    case True
-    define su where "su = support opp f s"
-    have fsu: "finite su"
-      using True by (simp add: su_def)
-    moreover
-    { assume "finite su" "su \<subseteq> s"
-      then have "iterate opp su f = iterate opp su g"
-        by (induct su) (auto simp: assms)
-    }
-    ultimately have "iterate opp (support opp f s) f = iterate opp (support opp g s) g"
-      by (simp add: "*" su_def support_subset)
-    then show ?thesis
-      by simp
-  qed
-qed
-
-lemma operative_division:
-  fixes f :: "'a::euclidean_space set \<Rightarrow> 'b"
-  assumes "monoidal opp"
-      and "operative opp f"
-      and "d division_of (cbox a b)"
-    shows "iterate opp d f = f (cbox a b)"
-proof -
-  define C where [abs_def]: "C = card (division_points (cbox a b) d)"
-  then show ?thesis
-    using assms
-  proof (induct C arbitrary: a b d rule: full_nat_induct)
-    case (1 a b d)
-    show ?case
-    proof (cases "content (cbox a b) = 0")
-      case True
-      show "iterate opp d f = f (cbox a b)"
-        unfolding operativeD(1)[OF assms(2) True]
-      proof (rule iterate_eq_neutral[OF \<open>monoidal opp\<close>])
-        fix x
-        assume x: "x \<in> d"
-        then show "f x = neutral opp"
-          by (metis division_ofD(4) 1(4) division_of_content_0[OF True] operativeD(1)[OF assms(2)] x)
-      qed
-    next
-      case False
-      note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
-      then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-        by (auto intro!: less_imp_le)
-        show "iterate opp d f = f (cbox a b)"
-      proof (cases "division_points (cbox a b) d = {}")
-        case True
-        { fix u v and j :: 'a
-          assume j: "j \<in> Basis" and as: "cbox u v \<in> d"
-          then have "cbox u v \<noteq> {}"
-            using "1.prems"(3) by blast
-          then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
-            using j unfolding box_ne_empty by auto
-          have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q (cbox u v)"
-            using as j by auto
-          have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
-               "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
-          note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
-          note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
-          moreover
-          have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
-            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
-            apply (metis j subset_box(1) uv(1))
-            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
-          ultimately have "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
-            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
-        then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
-          (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
-          unfolding forall_in_division[OF 1(4)]
-          by blast
-        have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
-          unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
-        note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
-        then guess i .. note i=this
-        guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
-        have "cbox a b \<in> d"
-        proof -
-          have "u = a" "v = b"
-            unfolding euclidean_eq_iff[where 'a='a]
-          proof safe
-            fix j :: 'a
-            assume j: "j \<in> Basis"
-            note i(2)[unfolded uv mem_box,rule_format,of j]
-            then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
-              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
-          qed
-          then have "i = cbox a b" using uv by auto
-          then show ?thesis using i by auto
-        qed
-        then have deq: "d = insert (cbox a b) (d - {cbox a b})"
-          by auto
-        have "iterate opp (d - {cbox a b}) f = neutral opp"
-        proof (rule iterate_eq_neutral[OF 1(2)])
-          fix x
-          assume x: "x \<in> d - {cbox a b}"
-          then have "x\<in>d"
-            by auto note d'[rule_format,OF this]
-          then guess u v by (elim exE conjE) note uv=this
-          have "u \<noteq> a \<or> v \<noteq> b"
-            using x[unfolded uv] by auto
-          then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
-            unfolding euclidean_eq_iff[where 'a='a] by auto
-          then have "u\<bullet>j = v\<bullet>j"
-            using uv(2)[rule_format,OF j] by auto
-          then have "content (cbox u v) = 0"
-            unfolding content_eq_0 using j
-            by force
-          then show "f x = neutral opp"
-            unfolding uv(1) by (rule operativeD(1)[OF 1(3)])
-        qed
-        then show "iterate opp d f = f (cbox a b)"
-          apply (subst deq)
-          apply (subst iterate_insert[OF 1(2)])
-          using 1
-          apply auto
-          done
-      next
-        case False
-        then have "\<exists>x. x \<in> division_points (cbox a b) d"
-          by auto
-        then guess k c
-          unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv
-          apply (elim exE conjE)
-          done
-        note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
-        from this(3) guess j .. note j=this
-        define d1 where "d1 = {l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
-        define d2 where "d2 = {l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
-        define cb where "cb = (\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)"
-        define ca where "ca = (\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)"
-        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
-        note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
-        then have *: "(iterate opp d1 f) = f (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
-          "(iterate opp d2 f) = f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-          unfolding interval_split[OF kc(4)]
-          apply (rule_tac[!] "1.hyps"[rule_format])
-          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
-          apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
-          done
-        { fix l y
-          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
-          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
-          have "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
-            unfolding leq interval_split[OF kc(4)]
-            apply (rule operativeD(1) 1)+
-            unfolding interval_split[symmetric,OF kc(4)]
-            using division_split_left_inj 1 as kc leq by blast
-        } note fxk_le = this
-        { fix l y
-          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
-          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
-          have "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
-            unfolding leq interval_split[OF kc(4)]
-            apply (rule operativeD(1) 1)+
-            unfolding interval_split[symmetric,OF kc(4)]
-            using division_split_right_inj 1 leq as kc by blast
-        } note fxk_ge = this
-        have "f (cbox a b) = opp (iterate opp d1 f) (iterate opp d2 f)" (is "_ = ?prev")
-          unfolding *
-          using assms(2) kc(4) by blast
-        also have "iterate opp d1 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<le> c}))"
-          unfolding d1_def empty_as_interval
-          apply (rule iterate_nonzero_image_lemma[unfolded o_def])
-          apply (rule 1 division_of_finite operativeD[OF 1(3)])+
-          apply (force simp add: empty_as_interval[symmetric] fxk_le)+
-          done
-        also have "iterate opp d2 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<ge> c}))"
-          unfolding d2_def empty_as_interval
-          apply (rule iterate_nonzero_image_lemma[unfolded o_def])
-          apply (rule 1 division_of_finite operativeD[OF 1(3)])+
-          apply (force simp add: empty_as_interval[symmetric] fxk_ge)+
-          done
-        also have *: "\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
-          unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
-          using assms(2) kc(4) by blast
-        have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k}))) =
-          iterate opp d f"
-          apply (subst(3) iterate_eq[OF _ *[rule_format]])
-          using 1
-          apply (auto simp: iterate_op[symmetric])
-          done
-        finally show ?thesis by auto
-      qed
-    qed
-  qed
-qed
-
-lemma iterate_image_nonzero:
-  assumes "monoidal opp"
-      and "finite s"
-      and "\<And>x y. \<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<and> f x = f y \<longrightarrow> g (f x) = neutral opp"
-    shows "iterate opp (f ` s) g = iterate opp s (g \<circ> f)"
-using assms
-by (induct rule: finite_subset_induct[OF assms(2) subset_refl]) auto
-
-lemma operative_tagged_division:
-  assumes "monoidal opp"
-      and "operative opp f"
-      and "d tagged_division_of (cbox a b)"
-    shows "iterate opp d (\<lambda>(x,l). f l) = f (cbox a b)"
-proof -
-  have *: "(\<lambda>(x,l). f l) = f \<circ> snd"
-    unfolding o_def by rule auto note tagged = tagged_division_ofD[OF assms(3)]
-  { fix a b a'
-    assume as: "(a, b) \<in> d" "(a', b) \<in> d" "(a, b) \<noteq> (a', b)"
-    have "f b = neutral opp"
-      using tagged(4)[OF as(1)]
-      apply clarify
-      apply (rule operativeD(1)[OF assms(2)])
-      by (metis content_eq_0_interior inf.idem tagged_division_ofD(5)[OF assms(3) as(1-3)])
-  }
-  then have "iterate opp d (\<lambda>(x,l). f l) = iterate opp (snd ` d) f"
-    unfolding *
-    by (force intro!: assms iterate_image_nonzero[symmetric, OF _ tagged_division_of_finite])
-  also have "\<dots> = f (cbox a b)"
-    using operative_division[OF assms(1-2) division_of_tagged_division[OF assms(3)]] .
-  finally show ?thesis .
-qed
-
-
-subsection \<open>Additivity of content.\<close>
-
-lemma setsum_iterate:
-  assumes "finite s"
-  shows "setsum f s = iterate op + s f"
-proof -
-  have "setsum f s = setsum f (support op + f s)"
-    using assms
-    by (auto simp: support_def intro: setsum.mono_neutral_right)
-  then show ?thesis unfolding iterate_def fold'_def setsum.eq_fold
-    by (simp add: comp_def)
-qed
-
-lemma additive_content_division:
-    "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)"
-  by (metis division_ofD(1) monoidal_monoid operative_content operative_division setsum_iterate)
-
-lemma additive_content_tagged_division:
-    "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
-  unfolding operative_tagged_division[OF monoidal_monoid operative_content,symmetric]
-  using setsum_iterate by blast
-
-
 subsection \<open>Finally, the integral of a constant\<close>
 
 lemma has_integral_const [intro]:
@@ -4598,17 +4536,6 @@
 
 subsection \<open>Negligibility of hyperplane.\<close>
 
-lemma setsum_nonzero_image_lemma:
-  assumes "finite s"
-    and "g a = 0"
-    and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g (f x) = 0"
-  shows "setsum g {f x |x. x \<in> s \<and> f x \<noteq> a} = setsum (g \<circ> f) s"
-  apply (subst setsum_iterate)
-  using assms monoidal_monoid
-  unfolding setsum_iterate[OF assms(1)]
-  apply (auto intro!: iterate_nonzero_image_lemma)
-  done
-
 lemma interval_doublesplit:
   fixes a :: "'a::euclidean_space"
   assumes "k \<in> Basis"
@@ -4628,7 +4555,7 @@
   fixes a :: "'a::euclidean_space"
   assumes "p division_of (cbox a b)"
     and k: "k \<in> Basis"
-  shows "{l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} |l. l \<in> p \<and> l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
+  shows "(\<lambda>l. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e}) ` {l\<in>p. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
          division_of  (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
 proof -
   have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
@@ -4639,14 +4566,15 @@
   note division_split(2)[OF this, where c="c-e" and k=k,OF k]
   then show ?thesis
     apply (rule **)
-    unfolding interval_doublesplit [OF k]
-    using k
-    apply (simp_all add: * interval_split)
-    apply (rule equalityI, blast)
-    apply clarsimp
-    apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
-    apply auto
-    done
+    subgoal
+      apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image[symmetric])
+      apply (rule equalityI)
+      apply blast
+      apply clarsimp
+      apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
+      apply auto
+      done
+    by (simp add: interval_split k interval_doublesplit)
 qed
 
 lemma content_doublesplit:
@@ -4794,7 +4722,7 @@
         apply (auto simp add:interval_doublesplit[OF k])
         done
       also have "\<dots> < e"
-      proof (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
+      proof (subst setsum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
         case prems: (1 u v)
         have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
           unfolding interval_doublesplit[OF k]
@@ -4806,45 +4734,30 @@
           unfolding prems interval_doublesplit[OF k]
           by (blast intro: antisym)
       next
-        have *: "setsum content {l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} |l. l \<in> snd ` p \<and> l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}} \<ge> 0"
-          apply (rule setsum_nonneg)
-          apply rule
-          unfolding mem_Collect_eq image_iff
-          apply (erule exE bexE conjE)+
-          unfolding split_paired_all
-        proof -
-          fix x l a b
-          assume as: "x = l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}" "(a, b) \<in> p" "l = snd (a, b)"
-          guess u v using p'(4)[OF as(2)] by (elim exE) note * = this
-          show "content x \<ge> 0"
-            unfolding as snd_conv * interval_doublesplit[OF k]
-            by (rule content_pos_le)
-        qed
-        have **: "norm (1::real) \<le> 1"
-          by auto
-        note division_doublesplit[OF p'' k,unfolded interval_doublesplit[OF k]]
-        note dsum_bound[OF this **,unfolded interval_doublesplit[symmetric,OF k]]
-        note this[unfolded real_scaleR_def real_norm_def mult_1_right mult_1, of c d]
-        note le_less_trans[OF this d(2)]
-        from this[unfolded abs_of_nonneg[OF *]]
-        show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e"
-          apply (subst setsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,symmetric])
-          apply (rule finite_imageI p' content_empty)+
-          unfolding forall_in_division[OF p'']
-        proof (rule,rule,rule,rule,rule,rule,rule,erule conjE)
-          fix m n u v
-          assume as:
-            "cbox m n \<in> snd ` p" "cbox u v \<in> snd ` p"
-            "cbox m n \<noteq> cbox u v"
-            "cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
-          have "(cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> cbox m n \<inter> cbox u v"
-            by blast
-          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_Int[of "cbox m n"]]
-          then have "interior (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
-            unfolding as Int_absorb by auto
-          then show "content (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
-            unfolding interval_doublesplit[OF k] content_eq_0_interior[symmetric] .
-        qed
+        have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
+          setsum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
+        proof (subst (2) setsum.reindex_nontrivial)
+          fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
+            "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
+          then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
+            by (auto)
+          from p'(5)[OF \<open>(x', x) \<in> p\<close> \<open>(y', y) \<in> p\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}"
+            by auto
+          moreover have "interior ((x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<subseteq> interior (x \<inter> y)"
+            by (auto intro: interior_mono)
+          ultimately have "interior (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
+            by (auto simp: eq)
+          then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
+            using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
+        qed (insert p'(1), auto intro!: setsum.mono_neutral_right)
+        also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
+          by simp
+        also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
+          using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]]
+          unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto
+        also have "\<dots> < e"
+          using d(2) by simp
+        finally show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
       qed
       finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
     qed
@@ -5491,33 +5404,11 @@
 
 subsection \<open>Integrability of continuous functions.\<close>
 
-lemma neutral_and[simp]: "neutral op \<and> = True"
-  unfolding neutral_def by (rule some_equality) auto
-
-lemma monoidal_and[intro]: "monoidal op \<and>"
-  unfolding monoidal_def by auto
-
-lemma iterate_and[simp]:
-  assumes "finite s"
-  shows "(iterate op \<and>) s p \<longleftrightarrow> (\<forall>x\<in>s. p x)"
-  using assms
-  apply induct
-  unfolding iterate_insert[OF monoidal_and]
-  apply auto
-  done
-
-lemma operative_division_and:
-  assumes "operative op \<and> P"
-    and "d division_of (cbox a b)"
-  shows "(\<forall>i\<in>d. P i) \<longleftrightarrow> P (cbox a b)"
-  using operative_division[OF monoidal_and assms] division_of_finite[OF assms(2)]
-  by auto
-
 lemma operative_approximable:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "0 \<le> e"
-  shows "operative op \<and> (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
-  unfolding operative_def neutral_and
+  shows "comm_monoid.operative op \<and> True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
+  unfolding comm_monoid.operative_def[OF comm_monoid_and]
 proof safe
   fix a b :: 'b
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
@@ -5571,6 +5462,14 @@
   qed
 qed
 
+lemma comm_monoid_set_F_and: "comm_monoid_set.F op \<and> True f s \<longleftrightarrow> (finite s \<longrightarrow> (\<forall>x\<in>s. f x))"
+proof -
+  interpret bool: comm_monoid_set "op \<and>" True
+    proof qed auto
+  show ?thesis
+    by (induction s rule: infinite_finite_induct) auto
+qed
+
 lemma approximable_on_division:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "0 \<le> e"
@@ -5578,9 +5477,9 @@
     and "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
   obtains g where "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
 proof -
-  note * = operative_division[OF monoidal_and operative_approximable[OF assms(1)] assms(2)]
-  note this[unfolded iterate_and[OF division_of_finite[OF assms(2)]]]
-  from assms(3)[unfolded this[of f]] guess g ..
+  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_approximable[OF assms(1)] assms(2)]
+  from assms(3) this[unfolded comm_monoid_set_F_and, of f] division_of_finite[OF assms(2)]
+  guess g by auto
   then show thesis
     apply -
     apply (rule that[of g])
@@ -5633,172 +5532,9 @@
   shows "f integrable_on {a .. b}"
   by (metis assms box_real(2) integrable_continuous)
 
-
 subsection \<open>Specialization of additivity to one dimension.\<close>
 
-lemma
-  shows real_inner_1_left: "inner 1 x = x"
-  and real_inner_1_right: "inner x 1 = x"
-  by simp_all
-
-lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
-  by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
-
-lemma interval_real_split:
-  "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
-  "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
-  apply (metis Int_atLeastAtMostL1 atMost_def)
-  apply (metis Int_atLeastAtMostL2 atLeast_def)
-  done
-
-lemma operative_1_lt:
-  assumes "monoidal opp"
-  shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a .. b::real} = neutral opp) \<and>
-    (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a .. c}) (f {c .. b}) = f {a .. b}))"
-  apply (simp add: operative_def content_real_eq_0 del: content_real_if)
-proof safe
-  fix a b c :: real
-  assume as:
-    "\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> Collect (op \<le> c)))"
-    "a < c"
-    "c < b"
-    from this(2-) have "cbox a b \<inter> {x. x \<le> c} = cbox a c" "cbox a b \<inter> {x. x \<ge> c} = cbox c b"
-      by (auto simp: mem_box)
-    then show "opp (f {a..c}) (f {c..b}) = f {a..b}"
-      unfolding as(1)[rule_format,of a b "c"] by auto
-next
-  fix a b c :: real
-  assume as: "\<forall>a b. b \<le> a \<longrightarrow> f {a..b} = neutral opp"
-    "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
-  show " f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c})) (f ({a..b} \<inter> Collect (op \<le> c)))"
-  proof (cases "c \<in> {a..b}")
-    case False
-    then have "c < a \<or> c > b" by auto
-    then show ?thesis
-    proof
-      assume "c < a"
-      then have *: "{a..b} \<inter> {x. x \<le> c} = {1..0}" "{a..b} \<inter> {x. c \<le> x} = {a..b}"
-        by auto
-      show ?thesis
-        unfolding *
-        apply (subst as(1)[rule_format,of 0 1])
-        using assms
-        apply auto
-        done
-    next
-      assume "b < c"
-      then have *: "{a..b} \<inter> {x. x \<le> c} = {a..b}" "{a..b} \<inter> {x. c \<le> x} = {1 .. 0}"
-        by auto
-      show ?thesis
-        unfolding *
-        apply (subst as(1)[rule_format,of 0 1])
-        using assms
-        apply auto
-        done
-    qed
-  next
-    case True
-    then have *: "min (b) c = c" "max a c = c"
-      by auto
-    have **: "(1::real) \<in> Basis"
-      by simp
-    have ***: "\<And>P Q. (\<Sum>i\<in>Basis. (if i = 1 then P i else Q i) *\<^sub>R i) = (P 1::real)"
-      by simp
-    show ?thesis
-      unfolding interval_real_split unfolding *
-    proof (cases "c = a \<or> c = b")
-      case False
-      then show "f {a..b} = opp (f {a..c}) (f {c..b})"
-        apply -
-        apply (subst as(2)[rule_format])
-        using True
-        apply auto
-        done
-    next
-      case True
-      then show "f {a..b} = opp (f {a..c}) (f {c..b})"
-      proof
-        assume *: "c = a"
-        then have "f {a .. c} = neutral opp"
-          apply -
-          apply (rule as(1)[rule_format])
-          apply auto
-          done
-        then show ?thesis
-          using assms unfolding * by auto
-      next
-        assume *: "c = b"
-        then have "f {c .. b} = neutral opp"
-          apply -
-          apply (rule as(1)[rule_format])
-          apply auto
-          done
-        then show ?thesis
-          using assms unfolding * by auto
-      qed
-    qed
-  qed
-qed
-
-lemma operative_1_le:
-  assumes "monoidal opp"
-  shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a .. b::real} = neutral opp) \<and>
-    (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a .. c}) (f {c .. b}) = f {a .. b}))"
-  unfolding operative_1_lt[OF assms]
-proof safe
-  fix a b c :: real
-  assume as:
-    "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
-    "a < c"
-    "c < b"
-  show "opp (f {a..c}) (f {c..b}) = f {a..b}"
-    apply (rule as(1)[rule_format])
-    using as(2-)
-    apply auto
-    done
-next
-  fix a b c :: real
-  assume "\<forall>a b. b \<le> a \<longrightarrow> f {a .. b} = neutral opp"
-    and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f {a..c}) (f {c..b}) = f {a..b}"
-    and "a \<le> c"
-    and "c \<le> b"
-  note as = this[rule_format]
-  show "opp (f {a..c}) (f {c..b}) = f {a..b}"
-  proof (cases "c = a \<or> c = b")
-    case False
-    then show ?thesis
-      apply -
-      apply (subst as(2))
-      using as(3-)
-      apply auto
-      done
-  next
-    case True
-    then show ?thesis
-    proof
-      assume *: "c = a"
-      then have "f {a .. c} = neutral opp"
-        apply -
-        apply (rule as(1)[rule_format])
-        apply auto
-        done
-      then show ?thesis
-        using assms unfolding * by auto
-    next
-      assume *: "c = b"
-      then have "f {c .. b} = neutral opp"
-        apply -
-        apply (rule as(1)[rule_format])
-        apply auto
-        done
-      then show ?thesis
-        using assms unfolding * by auto
-    qed
-  qed
-qed
-
-
-subsection \<open>Special case of additivity we need for the FCT.\<close>
+subsection \<open>Special case of additivity we need for the FTC.\<close>
 
 lemma additive_tagged_division_1:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
@@ -5809,17 +5545,15 @@
   let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
   have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
     using assms by auto
-  have *: "operative op + ?f"
-    unfolding operative_1_lt[OF monoidal_monoid] box_eq_empty
+  have *: "add.operative ?f"
+    unfolding add.operative_1_lt box_eq_empty
     by auto
   have **: "cbox a b \<noteq> {}"
     using assms(1) by auto
-  note operative_tagged_division[OF monoidal_monoid * assms(2)[simplified box_real[symmetric]]]
+  note setsum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]]
   note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric]
   show ?thesis
     unfolding *
-    apply (subst setsum_iterate[symmetric])
-    defer
     apply (rule setsum.cong)
     unfolding split_paired_all split_conv
     using assms(2)
@@ -6261,8 +5995,8 @@
 
 lemma operative_integrable:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
-  shows "operative op \<and> (\<lambda>i. f integrable_on i)"
-  unfolding operative_def neutral_and
+  shows "comm_monoid.operative op \<and> True (\<lambda>i. f integrable_on i)"
+  unfolding comm_monoid.operative_def[OF comm_monoid_and]
   apply safe
   apply (subst integrable_on_def)
   unfolding has_integral_null_eq
@@ -6279,8 +6013,8 @@
   apply (cases "cbox c d = {}")
   defer
   apply (rule partial_division_extend_1[OF assms(2)],assumption)
-  using operative_division_and[OF operative_integrable,symmetric,of _ _ _ f] assms(1)
-  apply auto
+  using comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable,symmetric,of _ _ _ f] assms(1)
+  apply (auto simp: comm_monoid_set_F_and)
   done
 
 lemma integrable_subinterval_real:
@@ -6301,7 +6035,7 @@
     and "(f has_integral (j::'a::banach)) {c .. b}"
   shows "(f has_integral (i + j)) {a .. b}"
 proof -
-  note operative_integral[of f, unfolded operative_1_le[OF monoidal_lifted[OF monoidal_monoid]]]
+  note operative_integral[of f, unfolded comm_monoid.operative_1_le[OF add.comm_monoid_lift_option]]
   note conjunctD2[OF this,rule_format]
   note * = this(2)[OF conjI[OF assms(1-2)],unfolded if_P[OF assms(3)]]
   then have "f integrable_on cbox a b"
@@ -6321,7 +6055,6 @@
     apply (subst(asm) if_P)
     defer
     apply (subst(asm) if_P)
-    unfolding lifted.simps
     using assms(3-)
     apply (auto simp add: integrable_on_def integral_unique)
     done
@@ -6369,9 +6102,9 @@
     by auto
   note p=this(1-2)
   note division_of_tagged_division[OF this(1)]
-  note * = operative_division_and[OF operative_integrable,OF this,symmetric,of f]
+  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable, OF this, symmetric, of f]
   show ?thesis
-    unfolding *
+    unfolding * comm_monoid_set_F_and
     apply safe
     unfolding snd_conv
   proof -
@@ -6387,7 +6120,7 @@
 qed
 
 
-subsection \<open>Second FCT or existence of antiderivative.\<close>
+subsection \<open>Second FTC or existence of antiderivative.\<close>
 
 lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on cbox a b"
   unfolding integrable_on_def
@@ -8026,8 +7759,7 @@
   }
   assume "cbox c d \<noteq> {}"
   from partial_division_extend_1[OF assms(2) this] guess p . note p=this
-  note mon = monoidal_lifted[OF monoidal_monoid]
-  note operat = operative_division[OF this operative_integral p(1), symmetric]
+  note operat = comm_monoid_set.operative_division[OF add.comm_monoid_set_lift_option operative_integral p(1), symmetric]
   let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
   {
     presume "?P"
@@ -8043,12 +7775,9 @@
       unfolding g_def
       by auto
   }
-
-  note iterate_eq_neutral[OF mon,unfolded neutral_lifted[OF monoidal_monoid]]
-  note * = this[unfolded neutral_add]
-  have iterate:"iterate (lifted op +) (p - {cbox c d})
-    (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
-  proof (rule *)
+  let ?F = "comm_monoid_set.F (lift_option op +) (Some 0)"
+  have iterate:"?F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
+  proof (intro comm_monoid_set.neutral[OF add.comm_monoid_set_lift_option] ballI)
     fix x
     assume x: "x \<in> p - {cbox c d}"
     then have "x \<in> p"
@@ -8086,15 +7815,10 @@
     done
   ultimately show ?P
     unfolding operat
+    using p
     apply (subst *)
-    apply (subst iterate_insert)
-    apply rule+
-    unfolding iterate
-    defer
-    apply (subst if_not_P)
-    defer
-    using p
-    apply auto
+    apply (subst comm_monoid_set.insert[OF add.comm_monoid_set_lift_option])
+    apply (simp_all add: division_of_finite iterate)
     done
 qed
 
@@ -9193,7 +8917,7 @@
     apply assumption
     apply (rule trans[of _ "setsum (\<lambda>(x,k). integral k f) p"])
     apply (subst eq_commute)
-    apply (rule setsum_over_tagged_division_lemma[OF assms(1)])
+    apply (rule setsum.over_tagged_division_lemma[OF assms(1)])
     apply (rule integral_null)
     apply assumption
     apply (rule setsum.cong)
@@ -10652,7 +10376,7 @@
           done
       qed
       have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
-        apply (subst setsum_over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
+        apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
         unfolding norm_eq_zero
         apply (rule integral_null)
         apply assumption
@@ -10823,7 +10547,7 @@
         let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
         have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
           by auto
-        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)" (*{(xl,i)|xl i. xl\<in>p \<and> i\<in>d}"**)
+        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
           apply safe
           unfolding image_iff
           apply (rule_tac x="((x,l),i)" in bexI)
@@ -11101,7 +10825,7 @@
             done
           show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
             using partial_division_of_tagged_division[of p "cbox a b"] p(1)
-            apply (subst setsum_over_tagged_division_lemma[OF p(1)])
+            apply (subst setsum.over_tagged_division_lemma[OF p(1)])
             apply (simp add: integral_null)
             apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
             apply (auto simp: tagged_partial_division_of_def)
@@ -11569,7 +11293,7 @@
   then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
     by (force intro!: choice)
   with * CC show ?thesis
-    by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"])
+    by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
 qed
 
 lemma continuous_on_prod_compactE:
@@ -12484,13 +12208,13 @@
 lemma integral_swap_operative:
   fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
   assumes f: "continuous_on s f" and e: "0 < e"
-    shows "operative(op \<and>)
+    shows "comm_monoid.operative (op \<and>) True
            (\<lambda>k. \<forall>a b c d.
                 cbox (a,c) (b,d) \<subseteq> k \<and> cbox (a,c) (b,d) \<subseteq> s
                 \<longrightarrow> norm(integral (cbox (a,c) (b,d)) f -
                          integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f((x,y)))))
                     \<le> e * content (cbox (a,c) (b,d)))"
-proof (auto simp: operative_def)
+proof (auto simp: comm_monoid.operative_def[OF comm_monoid_and])
   fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b
   assume c0: "content (cbox (a, c) (b, d)) = 0"
      and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)"
@@ -12604,7 +12328,7 @@
       by (rule integrable_continuous [OF assms])
     { fix p
       assume p: "p division_of cbox (a,c) (b,d)"
-      note opd1 = operative_division_and [OF integral_swap_operative [OF assms e'], THEN iffD1,
+      note opd1 = comm_monoid_set.operative_division [OF comm_monoid_set_and integral_swap_operative [OF assms e'], THEN iffD1,
                        THEN spec, THEN spec, THEN spec, THEN spec, of p "(a,c)" "(b,d)" a c b d]
       have "(\<And>t u v w z.
               \<lbrakk>t \<in> p; cbox (u,w) (v,z) \<subseteq> t;  cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)\<rbrakk> \<Longrightarrow>
@@ -12612,7 +12336,7 @@
               \<le> e * content (cbox (u,w) (v,z)) / content?CBOX)
             \<Longrightarrow>
             norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
-        using opd1 [OF p] False  by simp
+        using opd1 [OF p] False  by (simp add: comm_monoid_set_F_and)
     } note op_acbd = this
     { fix k::real and p and u::'a and v w and z::'b and t1 t2 l
       assume k: "0 < k"
diff -r 64db21931bcb -r bbcb05504fdc src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 03 11:45:09 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 04 18:45:28 2016 +0200
@@ -16,156 +16,56 @@
 begin
 
 
-(*FIXME: move elsewhere and use the existing locales*)
-
-subsection \<open>Using additivity of lifted function to encode definedness.\<close>
-
-definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
-
-fun lifted where
-  "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
-| "lifted opp None _ = (None::'b option)"
-| "lifted opp _ None = None"
-
-lemma lifted_simp_1[simp]: "lifted opp v None = None"
-  by (induct v) auto
-
-definition "monoidal opp \<longleftrightarrow>
-  (\<forall>x y. opp x y = opp y x) \<and>
-  (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
-  (\<forall>x. opp (neutral opp) x = x)"
-
-lemma monoidalI:
-  assumes "\<And>x y. opp x y = opp y x"
-    and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
-    and "\<And>x. opp (neutral opp) x = x"
-  shows "monoidal opp"
-  unfolding monoidal_def using assms by fastforce
-
-lemma monoidal_ac:
-  assumes "monoidal opp"
-  shows [simp]: "opp (neutral opp) a = a"
-    and [simp]: "opp a (neutral opp) = a"
-    and "opp a b = opp b a"
-    and "opp (opp a b) c = opp a (opp b c)"
-    and "opp a (opp b c) = opp b (opp a c)"
-  using assms unfolding monoidal_def by metis+
-
-lemma neutral_lifted [cong]:
-  assumes "monoidal opp"
-  shows "neutral (lifted opp) = Some (neutral opp)"
-proof -
-  { fix x
-    assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
-    then have "Some (neutral opp) = x"
-      apply (induct x)
-      apply force
-      by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
-  note [simp] = this
-  show ?thesis
-    apply (subst neutral_def)
-    apply (intro some_equality allI)
-    apply (induct_tac y)
-    apply (auto simp add:monoidal_ac[OF assms])
-    done
-qed
-
-lemma monoidal_lifted[intro]:
-  assumes "monoidal opp"
-  shows "monoidal (lifted opp)"
-  unfolding monoidal_def split_option_all neutral_lifted[OF assms]
-  using monoidal_ac[OF assms]
-  by auto
-
-definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
-definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
-definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
-
-lemma support_subset[intro]: "support opp f s \<subseteq> s"
-  unfolding support_def by auto
-
-lemma support_empty[simp]: "support opp f {} = {}"
-  using support_subset[of opp f "{}"] by auto
-
-lemma comp_fun_commute_monoidal[intro]:
-  assumes "monoidal opp"
-  shows "comp_fun_commute opp"
-  unfolding comp_fun_commute_def
-  using monoidal_ac[OF assms]
-  by auto
-
-lemma support_clauses:
-  "\<And>f g s. support opp f {} = {}"
-  "\<And>f g s. support opp f (insert x s) =
-    (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
-  "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
-  "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
-  "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
-  "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
-  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
-  unfolding support_def by auto
-
-lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
-  unfolding support_def by auto
-
-lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
-  unfolding iterate_def fold'_def by auto
-
-lemma iterate_insert[simp]:
-  assumes "monoidal opp"
-    and "finite s"
-  shows "iterate opp (insert x s) f =
-         (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
-proof (cases "x \<in> s")
-  case True
-  then show ?thesis by (auto simp: insert_absorb iterate_def)
-next
-  case False
-  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
-  show ?thesis
-  proof (cases "f x = neutral opp")
-    case True
-    then show ?thesis
-      using assms \<open>x \<notin> s\<close>
-      by (auto simp: iterate_def support_clauses)
-  next
-    case False
-    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
-      apply (simp add: iterate_def fold'_def support_clauses)
-      apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
-      apply (force simp add: )+
-      done
-  qed
-qed
-
-lemma iterate_some:
-    "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
-  by (erule finite_induct) (auto simp: monoidal_lifted)
-
-lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
-  unfolding neutral_def
-  by (force elim: allE [where x=0])
-
-lemma support_if: "a \<noteq> neutral opp \<Longrightarrow> support opp (\<lambda>x. if P x then a else neutral opp) A = {x \<in> A. P x}"
-unfolding support_def
-by (force intro: Collect_cong)
-
-lemma support_if_subset: "support opp (\<lambda>x. if P x then a else neutral opp) A \<subseteq> {x \<in> A. P x}"
-by (simp add: subset_iff support_def)
-
-definition supp_setsum where "supp_setsum f A \<equiv> setsum f (support op+ f A)"
-
-lemma supp_setsum_divide_distrib:
-    "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A"
-apply (cases "r = 0")
-apply (simp add: supp_setsum_def)
-apply (simp add: supp_setsum_def setsum_divide_distrib support_def)
-done
+(* FIXME: move elsewhere *)
+definition (in monoid_add) support_on :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'b set"
+where
+  "support_on s f = {x\<in>s. f x \<noteq> 0}"
+
+lemma in_support_on: "x \<in> support_on s f \<longleftrightarrow> x \<in> s \<and> f x \<noteq> 0"
+  by (simp add: support_on_def)
+
+lemma support_on_simps[simp]:
+  "support_on {} f = {}"
+  "support_on (insert x s) f =
+    (if f x = 0 then support_on s f else insert x (support_on s f))"
+  "support_on (s \<union> t) f = support_on s f \<union> support_on t f"
+  "support_on (s \<inter> t) f = support_on s f \<inter> support_on t f"
+  "support_on (s - t) f = support_on s f - support_on t f"
+  "support_on (f ` s) g = f ` (support_on s (g \<circ> f))"
+  unfolding support_on_def by auto
+
+lemma support_on_cong:
+  "(\<And>x. x \<in> s \<Longrightarrow> f x = 0 \<longleftrightarrow> g x = 0) \<Longrightarrow> support_on s f = support_on s g"
+  by (auto simp: support_on_def)
+
+lemma support_on_if: "a \<noteq> 0 \<Longrightarrow> support_on A (\<lambda>x. if P x then a else 0) = {x\<in>A. P x}"
+  by (auto simp: support_on_def)
+
+lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}"
+  by (auto simp: support_on_def)
+
+lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support_on s f)"
+  unfolding support_on_def by auto
+
+(* TODO: is supp_setsum really needed? TODO: Generalize to Finite_Set.fold *)
+definition (in comm_monoid_add) supp_setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
+where
+  "supp_setsum f s = (\<Sum>x\<in>support_on s f. f x)"
+
+lemma supp_setsum_empty[simp]: "supp_setsum f {} = 0"
+  unfolding supp_setsum_def by auto
+
+lemma supp_setsum_insert[simp]:
+  "finite (support_on s f) \<Longrightarrow>
+    supp_setsum f (insert x s) = (if x \<in> s then supp_setsum f s else f x + supp_setsum f s)"
+  by (simp add: supp_setsum_def in_support_on insert_absorb)
+
+lemma supp_setsum_divide_distrib: "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A"
+  by (cases "r = 0")
+     (auto simp: supp_setsum_def setsum_divide_distrib intro!: setsum.cong support_on_cong)
 
 (*END OF SUPPORT, ETC.*)
 
-
-
 lemma image_affinity_interval:
   fixes c :: "'a::ordered_real_vector"
   shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}