# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503575146 -3600
# Node ID 97fc319d608980bae580bf774b53d4e90f3dbf2a
# Parent  8645dc296dca97e549ac361d82626c703761027e# Parent  18a6478a574ca072d9b918d4e1e73d5f6a59fa40
Merge (non-trivial)

diff -r 18a6478a574c -r 97fc319d6089 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Aug 23 23:46:35 2017 +0100
+++ b/Admin/components/components.sha1	Thu Aug 24 12:45:46 2017 +0100
@@ -10,6 +10,7 @@
 b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9  cvc4-1.5pre-3.tar.gz
 76ff6103b8560f0e2778bbfbdb05f5fa18f850b7  cvc4-1.5pre-4.tar.gz
 03aec2ec5757301c9df149f115d1f4f1d2cafd9e  cvc4-1.5pre.tar.gz
+d70bfbe63590153c07709dea7084fbc39c669841  cvc4-1.5-1.tar.gz
 3682476dc5e915cf260764fa5b86f1ebdab57507  cvc4-1.5.tar.gz
 842d9526f37b928cf9e22f141884365129990d63  cygwin-20130110.tar.gz
 cb3b0706d208f104b800267697204f6d82f7b48a  cygwin-20130114.tar.gz
diff -r 18a6478a574c -r 97fc319d6089 Admin/components/main
--- a/Admin/components/main	Wed Aug 23 23:46:35 2017 +0100
+++ b/Admin/components/main	Thu Aug 24 12:45:46 2017 +0100
@@ -1,7 +1,7 @@
 #main components for everyday use, without big impact on overall build time
 bash_process-1.2.1
 csdp-6.x
-cvc4-1.5
+cvc4-1.5-1
 e-2.0
 isabelle_fonts-20160830
 jdk-8u144
diff -r 18a6478a574c -r 97fc319d6089 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 12:45:46 2017 +0100
@@ -188,15 +188,23 @@
   finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
 qed
 
-lemma operative_content[intro]: "add.operative content"
-  by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior)
+global_interpretation sum_content: operative plus 0 content
+  rewrites "comm_monoid_set.F plus 0 = sum"
+proof -
+  interpret operative plus 0 content
+    by standard (auto simp add: content_split [symmetric] content_eq_0_interior)
+  show "operative plus 0 content"
+    by standard
+  show "comm_monoid_set.F plus 0 = sum"
+    by (simp add: sum_def)
+qed
 
 lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> sum content d = content (cbox a b)"
-  by (metis operative_content sum.operative_division)
+  by (fact sum_content.division)
 
 lemma additive_content_tagged_division:
   "d tagged_division_of (cbox a b) \<Longrightarrow> sum (\<lambda>(x,l). content l) d = content (cbox a b)"
-  unfolding sum.operative_tagged_division[OF operative_content, symmetric] by blast
+  by (fact sum_content.tagged_division)
 
 lemma subadditive_content_division:
   assumes "\<D> division_of S" "S \<subseteq> cbox a b"
@@ -1404,16 +1412,16 @@
     by (simp add: interval_split[OF k] integrable_Cauchy)
 qed
 
-lemma operative_integral:
+lemma operative_integralI:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
-  shows "comm_monoid.operative (lift_option op +) (Some 0)
+  shows "operative (lift_option op +) (Some 0)
     (\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
 proof -
   interpret comm_monoid "lift_option plus" "Some (0::'b)"
     by (rule comm_monoid_lift_option)
       (rule add.comm_monoid_axioms)
   show ?thesis
-  proof (unfold operative_def, safe)
+  proof
     fix a b c
     fix k :: 'a
     assume k: "k \<in> Basis"
@@ -2457,45 +2465,49 @@
 
 subsection \<open>Integrability of continuous functions.\<close>
 
-lemma operative_approximable:
+lemma operative_approximableI:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "0 \<le> e"
-  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"
-    if "box a b = {}" for a b
-    apply (rule_tac x=f in exI)
-    using assms that by (auto simp: content_eq_0_interior)
-  {
-    fix c g and k :: 'b
-    assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
-    assume k: "k \<in> Basis"
-    show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-         "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-       apply (rule_tac[!] x=g in exI)
-      using fg integrable_split[OF g k] by auto
-  }
-  show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" 
-      and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" 
-      and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" 
-      and k: "k \<in> Basis"
-    for c k g1 g2
-  proof -
-    let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+  shows "operative conj True (\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i)"
+proof -
+  interpret comm_monoid conj True
+    by standard auto
+  show ?thesis
+  proof (standard, 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"
-    proof (intro exI conjI ballI)
-      show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
-        by (auto simp: that assms fg1 fg2)
-      show "?g integrable_on cbox a b"
-      proof -
-        have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-          by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
-        with has_integral_split[OF _ _ k] show ?thesis
-          unfolding integrable_on_def by blast
+      if "box a b = {}" for a b
+      apply (rule_tac x=f in exI)
+      using assms that by (auto simp: content_eq_0_interior)
+    {
+      fix c g and k :: 'b
+      assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
+      assume k: "k \<in> Basis"
+      show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+           "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+         apply (rule_tac[!] x=g in exI)
+        using fg integrable_split[OF g k] by auto
+    }
+    show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+      if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" 
+        and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+        and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" 
+        and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" 
+        and k: "k \<in> Basis"
+      for c k g1 g2
+    proof -
+      let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+      show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+      proof (intro exI conjI ballI)
+        show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
+          by (auto simp: that assms fg1 fg2)
+        show "?g integrable_on cbox a b"
+        proof -
+          have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+            by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+          with has_integral_split[OF _ _ k] show ?thesis
+            unfolding integrable_on_def by blast
+        qed
       qed
     qed
   qed
@@ -2516,11 +2528,9 @@
     and f: "\<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 * = comm_monoid_set.operative_division
-             [OF comm_monoid_set_and operative_approximable[OF \<open>0 \<le> e\<close>] d]
-  have "finite d"
-    by (rule division_of_finite[OF d])
-  with f *[unfolded comm_monoid_set_F_and, of f] that show thesis
+  interpret operative conj True "\<lambda>i. \<exists>g. (\<forall>x\<in>i. norm (f x - g (x::'b)) \<le> e) \<and> g integrable_on i"
+    using \<open>0 \<le> e\<close> by (rule operative_approximableI)
+  from f local.division [OF d] that show thesis
     by auto
 qed
 
@@ -2999,31 +3009,43 @@
 
 subsection \<open>Integrability on subintervals.\<close>
 
-lemma operative_integrable:
+lemma operative_integrableI:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
-  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)
-     apply rule
-     apply (rule has_integral_null_eq[where i=0, THEN iffD2])
-      apply (simp add: content_eq_0_interior)
-     apply rule
-    apply (rule, assumption, assumption)+
-  unfolding integrable_on_def
-  by (auto intro!: has_integral_split)
+  assumes "0 \<le> e"
+  shows "operative conj True (\<lambda>i. f integrable_on i)"
+proof -
+  interpret comm_monoid conj True
+    by standard auto
+  show ?thesis
+    apply standard
+    apply safe
+       apply (subst integrable_on_def)
+       apply rule
+       apply (rule has_integral_null_eq[where i=0, THEN iffD2])
+        apply (simp add: content_eq_0_interior)
+       apply rule
+      apply (rule, assumption, assumption)+
+    unfolding integrable_on_def
+    apply (auto intro!: has_integral_split)
+    done
+qed
 
 lemma integrable_subinterval:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on cbox a b"
     and "cbox c d \<subseteq> cbox a b"
   shows "f integrable_on cbox c d"
-  apply (cases "cbox c d = {}")
-  defer
-  apply (rule partial_division_extend_1[OF assms(2)],assumption)
-  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
+proof -
+  interpret operative conj True "\<lambda>i. f integrable_on i"
+    using order_refl by (rule operative_integrableI)
+  show ?thesis
+    apply (cases "cbox c d = {}")
+     defer
+     apply (rule partial_division_extend_1[OF assms(2)],assumption)
+    using division [symmetric] assms(1)
+     apply (auto simp: comm_monoid_set_F_and)
+    done
+qed
 
 lemma integrable_subinterval_real:
   fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3043,10 +3065,10 @@
       and cb: "(f has_integral j) {c..b}"
   shows "(f has_integral (i + j)) {a..b}"
 proof -
-  interpret comm_monoid "lift_option plus" "Some (0::'a)"
-    by (rule comm_monoid_lift_option)
-      (rule add.comm_monoid_axioms)
-  from operative_integral [of f, unfolded operative_1_le] \<open>a \<le> c\<close> \<open>c \<le> b\<close>
+  interpret operative_real "lift_option plus" "Some 0"
+    "\<lambda>i. if f integrable_on i then Some (integral i f) else None"
+    using operative_integralI by (rule operative_realI)
+  from \<open>a \<le> c\<close> \<open>c \<le> b\<close> ac cb coalesce_less_eq
   have *: "lift_option op +
              (if f integrable_on {a..c} then Some (integral {a..c} f) else None)
              (if f integrable_on {c..b} then Some (integral {c..b} f) else None) =
@@ -3097,6 +3119,8 @@
     f integrable_on cbox u v"
   shows "f integrable_on cbox a b"
 proof -
+  interpret operative conj True "\<lambda>i. f integrable_on i"
+    using order_refl by (rule operative_integrableI)
   have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
     f integrable_on cbox u v)"
     using assms by (metis zero_less_one)
@@ -3111,8 +3135,7 @@
   have "f integrable_on k" if "(x, k) \<in> p" for x k
     using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto
   then show ?thesis
-    unfolding comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable sndp,  symmetric]
-              comm_monoid_set_F_and
+    unfolding division [symmetric, OF sndp] comm_monoid_set_F_and
     by auto
 qed
 
@@ -4485,13 +4508,11 @@
   }
   assume "cbox c d \<noteq> {}"
   from partial_division_extend_1 [OF assms(2) this] guess p . note p=this
-  interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
-    apply (rule comm_monoid_set.intro)
-    apply (rule comm_monoid_lift_option)
-    apply (rule add.comm_monoid_axioms)
-    done
-  note operat = operative_division
-    [OF operative_integral p(1), symmetric]
+  interpret operative "lift_option plus" "Some (0 :: 'b)"
+    "\<lambda>i. if g integrable_on i then Some (integral i g) else None"
+    by (fact operative_integralI)
+  note operat = division
+    [OF 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"
@@ -6984,16 +7005,16 @@
   apply (auto simp: has_integral_integral [symmetric])
   done
 
-lemma integral_swap_operative:
+lemma integral_swap_operativeI:
   fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
   assumes f: "continuous_on s f" and e: "0 < e"
-    shows "comm_monoid.operative (op \<and>) True
+    shows "operative conj 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: comm_monoid.operative_def[OF comm_monoid_and])
+proof (standard, auto)
   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 *: "box (a, c) (b, d) = {}"
      and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)"
@@ -7087,8 +7108,8 @@
 
 lemma integral_prod_continuous:
   fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
-  assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f")
-    shows "integral (cbox (a,c) (b,d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f(x,y)))"
+  assumes "continuous_on (cbox (a, c) (b, d)) f" (is "continuous_on ?CBOX f")
+    shows "integral (cbox (a, c) (b, d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y)))"
 proof (cases "content ?CBOX = 0")
   case True
   then show ?thesis
@@ -7099,22 +7120,41 @@
     using content_lt_nz by blast
   have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0"
   proof (rule dense_eq0_I, simp)
-    fix e::real  assume "0 < e"
-    with cbp have e': "0 < e/content ?CBOX"
+    fix e :: real 
+    assume "0 < e"
+    with \<open>content ?CBOX > 0\<close> have "0 < e / content ?CBOX"
       by simp
-    have f_int_acbd: "f integrable_on cbox (a,c) (b,d)"
+    have f_int_acbd: "f integrable_on ?CBOX"
       by (rule integrable_continuous [OF assms])
     { fix p
-      assume p: "p division_of cbox (a,c) (b,d)"
-      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>
-              norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
-              \<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 add: comm_monoid_set_F_and)
+      assume p: "p division_of ?CBOX"
+      then have "finite p"
+        by blast
+      define e' where "e' = e / content ?CBOX"
+      with \<open>0 < e\<close> \<open>0 < e / content ?CBOX\<close>
+      have "0 < e'"
+        by simp
+      interpret operative conj True
+           "\<lambda>k. \<forall>a' b' c' d'.
+                cbox (a', c') (b', d') \<subseteq> k \<and> cbox (a', c') (b', d') \<subseteq> ?CBOX
+                \<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'))"
+        using assms \<open>0 < e'\<close> by (rule integral_swap_operativeI)
+      have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
+          \<le> e' * content ?CBOX"
+        if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
+          \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
+              integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
+              \<le> e' * content (cbox (u, w) (v, z))"
+        using that division [of p "(a, c)" "(b, d)"] p \<open>finite p\<close> by (auto simp add: comm_monoid_set_F_and)
+      with False have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x, y))))
+          \<le> e"
+        if "\<And>t u v w z. t \<in> p \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> t \<Longrightarrow> cbox (u, w) (v, z) \<subseteq> ?CBOX
+          \<Longrightarrow> norm (integral (cbox (u, w) (v, z)) f -
+              integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
+              \<le> e * content (cbox (u, w) (v, z)) / content ?CBOX"
+        using that by (simp add: e'_def)
     } note op_acbd = this
     { fix k::real and \<D> and u::'a and v w and z::'b and t1 t2 l
       assume k: "0 < k"
@@ -7149,7 +7189,7 @@
          \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
         apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
         apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
-        using cbp e' nf'
+        using cbp \<open>0 < e / content ?CBOX\<close> nf'
         apply (auto simp: integrable_diff f_int_uwvz integrable_const)
         done
       have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
@@ -7160,14 +7200,14 @@
                \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
         apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
         apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
-        using cbp e' nf'
+        using cbp \<open>0 < e / content ?CBOX\<close> nf'
         apply (auto simp: integrable_diff f_int_uv integrable_const)
         done
       have "norm (integral (cbox u v)
                (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
             \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
         apply (rule integrable_bound [OF _ _ normint_wz])
-        using cbp e'
+        using cbp \<open>0 < e / content ?CBOX\<close>
         apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
         done
       also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
diff -r 18a6478a574c -r 97fc319d6089 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 24 12:45:46 2017 +0100
@@ -10,6 +10,8 @@
   Topology_Euclidean_Space
 begin
 
+term comm_monoid
+
 lemma sum_Sigma_product:
   assumes "finite S"
     and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
@@ -571,7 +573,7 @@
                   "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
           using f g by (auto simp: PiE_iff)
         with * ord[of i] show "interior l \<inter> interior k = {}"
-          by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
+          by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
       }
       note \<open>k \<subseteq> cbox a b\<close>
     }
@@ -1200,6 +1202,91 @@
   apply auto
   done
 
+lemma tagged_division_Un_interval:
+  fixes a :: "'a::euclidean_space"
+  assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
+    and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+    and k: "k \<in> Basis"
+  shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
+proof -
+  have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+    by auto
+  show ?thesis
+    apply (subst *)
+    apply (rule tagged_division_Un[OF assms(1-2)])
+    unfolding interval_split[OF k] interior_cbox
+    using k
+    apply (auto simp add: box_def elim!: ballE[where x=k])
+    done
+qed
+
+lemma tagged_division_Un_interval_real:
+  fixes a :: real
+  assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
+    and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
+    and k: "k \<in> Basis"
+  shows "(p1 \<union> p2) tagged_division_of {a .. b}"
+  using assms
+  unfolding box_real[symmetric]
+  by (rule tagged_division_Un_interval)
+
+lemma tagged_division_split_left_inj:
+  assumes d: "d tagged_division_of i"
+  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+  and "K1 \<noteq> K2"
+  and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
+    shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+proof -
+  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
+    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+  then show ?thesis
+    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
+
+lemma tagged_division_split_right_inj:
+  assumes d: "d tagged_division_of i"
+  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
+  and "K1 \<noteq> K2"
+  and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+    shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+proof -
+  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
+    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+  then show ?thesis
+    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
+
+lemma (in comm_monoid_set) over_tagged_division_lemma:
+  assumes "p tagged_division_of i"
+    and "\<And>u v. box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
+  shows "F (\<lambda>(_, k). d k) p = F d (snd ` p)"
+proof -
+  have *: "(\<lambda>(_ ,k). d k) = d \<circ> snd"
+    by (simp add: fun_eq_iff)
+  note assm = tagged_division_ofD[OF assms(1)]
+  show ?thesis
+    unfolding *
+  proof (rule reindex_nontrivial[symmetric])
+    show "finite p"
+      using assm by auto
+    fix x y
+    assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
+    obtain a b where ab: "snd x = cbox a b"
+      using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
+    have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
+      using \<open>x \<in> p\<close> \<open>x \<noteq> y\<close> \<open>snd x = snd y\<close> [symmetric] by auto
+    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
+      by (intro assm(5)[of "fst x" _ "fst y"]) auto
+    then have "box a b = {}"
+      unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
+    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) = \<^bold>1"
+      unfolding ab by auto
+  qed
+qed
+
+
 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
@@ -1233,29 +1320,21 @@
 lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
   by (rule comm_monoid_set.intro) (fact comm_monoid_and)
 
-paragraph \<open>Operative\<close>
 
-definition (in comm_monoid) operative :: "('b::euclidean_space set \<Rightarrow> 'a) \<Rightarrow> bool"
-  where "operative g \<longleftrightarrow>
-    (\<forall>a b. box a b = {} \<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}))"
+paragraph \<open>Misc\<close>
 
-lemma (in comm_monoid) operativeD[dest]:
-  assumes "operative g"
-  shows "\<And>a b. box a b = {} \<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 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_empty:
-  assumes g: "operative g" shows "g {} = \<^bold>1"
-proof -
-  have *: "cbox One (-One) = ({}::'b set)"
-    by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
-  moreover have "box One (-One) = ({}::'b set)"
-    using box_subset_cbox[of One "-One"] by (auto simp: *)
-  ultimately show ?thesis
-    using operativeD(1)[OF g, of One "-One"] by simp
-qed
+lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
+  by (meson zero_less_one)
+
+
+paragraph \<open>Division points\<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>
@@ -1463,14 +1542,31 @@
     by (simp add: interval_split k interval_doublesplit)
 qed
               
-lemma (in comm_monoid_set) operative_division:
+paragraph \<open>Operative\<close>
+
+locale operative = comm_monoid_set +
   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)"
+  assumes box_empty_imp: "\<And>a b. box a b = {} \<Longrightarrow> g (cbox a b) = \<^bold>1"
+    and Basis_imp: "\<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})"
+begin
+
+lemma empty [simp]:
+  "g {} = \<^bold>1"
+proof -
+  have *: "cbox One (-One) = ({}::'b set)"
+    by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
+  moreover have "box One (-One) = ({}::'b set)"
+    using box_subset_cbox[of One "-One"] by (auto simp: *)
+  ultimately show ?thesis
+    using box_empty_imp [of One "-One"] by simp
+qed
+       
+lemma division:
+  "F g d = g (cbox a b)" if "d division_of (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)
+  using that proof (induction C arbitrary: a b d rule: less_induct)
     case (less a b d)
     show ?case
     proof cases
@@ -1483,9 +1579,9 @@
         then have "box a' b' \<subseteq> box a b"
           unfolding subset_box by auto
         then have "g k = \<^bold>1"
-          using operativeD(1)[OF g, of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
+          using box_empty_imp [of a' b'] k by (simp add: \<open>box a b = {}\<close>) }
       then show "box a b = {} \<Longrightarrow> F g d = g (cbox a b)"
-        by (auto intro!: neutral simp: operativeD(1)[OF g])
+        by (auto intro!: neutral simp: box_empty_imp)
     next
       assume "box a b \<noteq> {}"
       then have ab: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i" and ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
@@ -1560,7 +1656,7 @@
           then have "box u v = {}"
             using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
           then show "g x = \<^bold>1"
-            unfolding uv(1) by (rule operativeD(1)[OF g])
+            unfolding uv(1) by (rule box_empty_imp)
         qed
         then show "F g d = g (cbox a b)"
           using division_ofD[OF less.prems]
@@ -1613,7 +1709,8 @@
           have "interior (cbox u v \<inter> ?lec) = {}"
             using that division_split_left_inj leq less.prems by blast
           then show ?thesis
-            unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+            unfolding leq interval_split [OF \<open>k \<in> Basis\<close>]
+            by (auto intro: box_empty_imp)
         qed
         have fxk_ge: "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
           if "l \<in> d" "y \<in> d" "l \<inter> ?gec = y \<inter> ?gec" "l \<noteq> y" for l y
@@ -1623,23 +1720,26 @@
           have "interior (cbox u v \<inter> ?gec) = {}"
             using that division_split_right_inj leq less.prems by blast
           then show ?thesis
-            unfolding leq interval_split[OF \<open>k \<in> Basis\<close>] using g by auto
+            unfolding leq interval_split[OF \<open>k \<in> Basis\<close>]
+            by (auto intro: box_empty_imp)
         qed
         have d1_alt: "d1 = (\<lambda>l. l \<inter> ?lec) ` {l \<in> d. l \<inter> ?lec \<noteq> {}}"
           using d1_def by auto
         have d2_alt: "d2 = (\<lambda>l. l \<inter> ?gec) ` {l \<in> d. l \<inter> ?gec \<noteq> {}}"
           using d2_def by auto
         have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
-          unfolding * using g \<open>k \<in> Basis\<close> by blast
+          unfolding * using \<open>k \<in> Basis\<close>
+          by (auto dest: Basis_imp)
         also have "F g d1 = F (\<lambda>l. g (l \<inter> ?lec)) 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])
+          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
         also have "F g d2 = F (\<lambda>l. g (l \<inter> ?gec)) 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])
+          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
         also have *: "\<forall>x\<in>d. g x = g (x \<inter> ?lec) \<^bold>* g (x \<inter> ?gec)"
           unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
-          using g \<open>k \<in> Basis\<close> by blast
+          using \<open>k \<in> Basis\<close>
+          by (auto dest: Basis_imp)
         have "F (\<lambda>l. g (l \<inter> ?lec)) d \<^bold>* F (\<lambda>l. g (l \<inter> ?gec)) d = F g d"
           using * by (simp add: distrib)
         finally show ?thesis by auto
@@ -1648,166 +1748,86 @@
   qed
 qed
 
-lemma (in comm_monoid_set) over_tagged_division_lemma:
-  assumes "p tagged_division_of i"
-    and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> box u v = {} \<Longrightarrow> d (cbox u v) = \<^bold>1"
-  shows "F (\<lambda>(x,k). d k) p = F d (snd ` p)"
+lemma tagged_division:
+  assumes "d tagged_division_of (cbox a b)"
+  shows "F (\<lambda>(_, l). g l) d = g (cbox a b)"
 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 reindex_nontrivial[symmetric])
-    show "finite p"
-      using assm by auto
-    fix x y
-    assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
-    obtain a b where ab: "snd x = cbox a b"
-      using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
-    have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
-      by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
-    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
-      by (intro assm(5)[of "fst x" _ "fst y"]) auto
-    then have "box a b = {}"
-      unfolding \<open>snd x = snd y\<close>[symmetric] ab by auto
-    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) = \<^bold>1"
-      unfolding ab by auto
+  have "F (\<lambda>(_, k). g k) d = F g (snd ` d)"
+    using assms box_empty_imp by (rule over_tagged_division_lemma)
+  then show ?thesis
+    unfolding assms [THEN division_of_tagged_division, THEN division] .
   qed
-qed
+
+end
 
-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 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
+locale operative_real = comm_monoid_set +
+  fixes g :: "real set \<Rightarrow> 'a"
+  assumes neutral: "b \<le> a \<Longrightarrow> g {a..b} = \<^bold>1"
+  assumes coalesce_less: "a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+begin
 
-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 atMost_def[symmetric] atLeast_def[symmetric])
-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)
+sublocale operative where g = g
+  rewrites "box = (greaterThanLessThan :: real \<Rightarrow> _)"
+    and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
+    and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
+proof -
+  show "operative f z g"
+  proof
+    show "g (cbox a b) = \<^bold>1" if "box a b = {}" for a b
+      using that by (simp add: neutral)
+    show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+      if "k \<in> Basis" for a b c k
+    proof -
+      from that have [simp]: "k = 1"
+        by simp
+      from neutral [of 0 1] neutral [of a a for a] coalesce_less
   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}"
+      have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
     by (auto simp: min_def max_def le_less)
+      then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+        by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
 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 eq1: "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
-    and eqg: "\<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"
-  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
-  proof (cases "c = a \<or> c = b")
-    case False
-    then show ?thesis
-      using eqg \<open>a \<le> c\<close> \<open>c \<le> b\<close> by auto
-  next
-    case True
-    then show ?thesis
-    proof
-      assume *: "c = a"
-      then have "g {a .. c} = \<^bold>1"
-        using eq1 by blast
-      then show ?thesis
-        unfolding * by auto
-    next
-      assume *: "c = b"
-      then have "g {c .. b} = \<^bold>1"
-        using eq1 by blast
-      then show ?thesis
-        unfolding * by auto
-    qed
   qed
+  show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
+    and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
+    and "\<And>x::real. x \<in> Basis \<longleftrightarrow> x = 1"
+    by (simp_all add: fun_eq_iff)
 qed
 
-lemma tagged_division_Un_interval:
-  fixes a :: "'a::euclidean_space"
-  assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
-    and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-    and k: "k \<in> Basis"
-  shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
+lemma coalesce_less_eq:
+  "g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
+  proof (cases "c = a \<or> c = b")
+    case False
+  with that have "a < c" "c < b"
+    by auto
+    then show ?thesis
+    by (rule coalesce_less)
+  next
+    case True
+  with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
+    by safe simp_all
+    qed
+
+end
+
+lemma operative_realI:
+  "operative_real f z g" if "operative f z g"
 proof -
-  have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-    by auto
+  interpret operative f z g
+    using that .
   show ?thesis
-    apply (subst *)
-    apply (rule tagged_division_Un[OF assms(1-2)])
-    unfolding interval_split[OF k] interior_cbox
-    using k
-    apply (auto simp add: box_def elim!: ballE[where x=k])
-    done
+  proof
+    show "g {a..b} = z" if "b \<le> a" for a b
+      using that box_empty_imp by simp
+    show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
+      using that
+    using Basis_imp [of 1 a b c]
+      by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
+qed
 qed
 
-lemma tagged_division_Un_interval_real:
-  fixes a :: real
-  assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
-    and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
-    and k: "k \<in> Basis"
-  shows "(p1 \<union> p2) tagged_division_of {a .. b}"
-  using assms
-  unfolding box_real[symmetric]
-  by (rule tagged_division_Un_interval)
-
-lemma tagged_division_split_left_inj:
-  assumes d: "d tagged_division_of i"
-  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
-  and "K1 \<noteq> K2"
-  and eq: "K1 \<inter> {x. x \<bullet> k \<le> c} = K2 \<inter> {x. x \<bullet> k \<le> c}"
-    shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
-proof -
-  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
-    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
-  then show ?thesis
-    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
-
-lemma tagged_division_split_right_inj:
-  assumes d: "d tagged_division_of i"
-  and tags: "(x1, K1) \<in> d" "(x2, K2) \<in> d"
-  and "K1 \<noteq> K2"
-  and eq: "K1 \<inter> {x. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
-    shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
-proof -
-  have "interior (K1 \<inter> K2) = {} \<or> (x2, K2) = (x1, K1)"
-    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
-  then show ?thesis
-    using eq \<open>K1 \<noteq> K2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
-qed
 
 subsection \<open>Special case of additivity we need for the FTC.\<close>
 
@@ -1818,10 +1838,11 @@
   shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
 proof -
   let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
+  interpret operative_real plus 0 ?f
+    rewrites "comm_monoid_set.F op + 0 = sum"
+    by standard[1] (auto simp add: sum_def)
   have p_td: "p tagged_division_of cbox a b"
     using assms(2) box_real(2) by presburger
-  have *: "add.operative ?f"
-    unfolding add.operative_1_lt box_eq_empty by auto
   have **: "cbox a b \<noteq> {}"
     using assms(1) by auto
   then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
@@ -1829,14 +1850,12 @@
       have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
         using assms by auto
       then show ?thesis
-        using p_td assms by (simp add: "*" sum.operative_tagged_division)
+        using p_td assms by (simp add: tagged_division) 
     qed 
   then show ?thesis
     using assms by (auto intro!: sum.cong)
 qed
 
-lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
-  by (meson zero_less_one)
 
 subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
 
diff -r 18a6478a574c -r 97fc319d6089 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Aug 24 12:45:46 2017 +0100
@@ -1521,34 +1521,25 @@
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
 by (cases "B = {#}") (auto dest: multi_member_split)
 
-lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#M. \<not> P x #}"
-apply (subst multiset_eq_iff)
-apply auto
-done
-
-lemma mset_subset_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
+lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
+  by (subst multiset_eq_iff) auto
+
+lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
-  case (empty M)
-  then have "M \<noteq> {#}" by (simp add: subset_mset.zero_less_iff_neq_zero)
-  then obtain M' x where "M = add_mset x M'"
-    by (blast dest: multi_nonempty_split)
-  then show ?case by simp
+  case empty
+  then show ?case
+    using nonempty_has_size by auto
 next
-  case (add x S T)
-  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
-  have SxsubT: "add_mset x S \<subset># T" by fact
-  then have "x \<in># T" and "S \<subset># T"
-    by (auto dest: mset_subset_insertD)
-  then obtain T' where T: "T = add_mset x T'"
-    by (blast dest: multi_member_split)
-  then have "S \<subset># T'" using SxsubT
-    by simp
-  then have "size S < size T'" using IH by simp
-  then show ?case using T by simp
+  case (add x A)
+  have "add_mset x A \<subseteq># B"
+    by (meson add.prems subset_mset_def)
+  then show ?case
+    by (metis (no_types) add.prems add.right_neutral add_diff_cancel_left' leD nat_neq_iff
+      size_Diff_submset size_eq_0_iff_empty size_mset_mono subset_mset.le_iff_add subset_mset_def)
 qed
 
 lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
-by (cases M) auto
+  by (cases M) auto
 
 
 subsubsection \<open>Strong induction and subset induction for multisets\<close>
@@ -1674,18 +1665,13 @@
   "image_mset f = fold_mset (add_mset \<circ> f) {#}"
 
 lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \<circ> f)"
-proof
-qed (simp add: fun_eq_iff)
+  by unfold_locales (simp add: fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   by (simp add: image_mset_def)
 
 lemma image_mset_single: "image_mset f {#x#} = {#f x#}"
-proof -
-  interpret comp_fun_commute "add_mset \<circ> f"
-    by (fact comp_fun_commute_mset_image)
-  show ?thesis by (simp add: image_mset_def)
-qed
+  by (simp add: comp_fun_commute.fold_mset_add_mset comp_fun_commute_mset_image image_mset_def)
 
 lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
 proof -
@@ -1723,8 +1709,7 @@
   finally show ?thesis by simp
 qed
 
-lemma count_image_mset:
-  "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
+lemma count_image_mset: "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
 proof (induction A)
   case empty
   then show ?case by simp
@@ -1733,7 +1718,7 @@
   moreover have *: "(if x = y then Suc n else n) = n + (if x = y then 1 else 0)" for n y
     by simp
   ultimately show ?case
-    by (auto simp: sum.distrib sum.delta' intro!: sum.mono_neutral_left)
+    by (auto simp: sum.distrib intro!: sum.mono_neutral_left)
 qed
 
 lemma image_mset_subseteq_mono: "A \<subseteq># B \<Longrightarrow> image_mset f A \<subseteq># image_mset f B"
@@ -1765,7 +1750,7 @@
 \<close>
 
 lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
-by (metis set_image_mset)
+  by simp
 
 functor image_mset: image_mset
 proof -
@@ -2065,24 +2050,20 @@
 
 end
 
-lemma mset_sorted_list_of_multiset [simp]:
-  "mset (sorted_list_of_multiset M) = M"
-by (induct M) simp_all
-
-lemma sorted_list_of_multiset_mset [simp]:
-  "sorted_list_of_multiset (mset xs) = sort xs"
-by (induct xs) simp_all
-
-lemma finite_set_mset_mset_set[simp]:
-  "finite A \<Longrightarrow> set_mset (mset_set A) = A"
-by (induct A rule: finite_induct) simp_all
+lemma mset_sorted_list_of_multiset[simp]: "mset (sorted_list_of_multiset M) = M"
+  by (induct M) simp_all
+
+lemma sorted_list_of_multiset_mset[simp]: "sorted_list_of_multiset (mset xs) = sort xs"
+  by (induct xs) simp_all
+
+lemma finite_set_mset_mset_set[simp]: "finite A \<Longrightarrow> set_mset (mset_set A) = A"
+  by auto
 
 lemma mset_set_empty_iff: "mset_set A = {#} \<longleftrightarrow> A = {} \<or> infinite A"
   using finite_set_mset_mset_set by fastforce
 
-lemma infinite_set_mset_mset_set:
-  "\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
-by simp
+lemma infinite_set_mset_mset_set: "\<not> finite A \<Longrightarrow> set_mset (mset_set A) = {}"
+  by simp
 
 lemma set_sorted_list_of_multiset [simp]:
   "set (sorted_list_of_multiset M) = set_mset M"
@@ -2108,22 +2089,15 @@
   finally show ?case by simp
 qed simp_all
 
-lemma msubset_mset_set_iff [simp]:
-  assumes "finite A" "finite B"
-  shows   "mset_set A \<subseteq># mset_set B \<longleftrightarrow> A \<subseteq> B"
-  using subset_imp_msubset_mset_set[of A B] 
-        set_mset_mono[of "mset_set A" "mset_set B"] assms by auto
-    
-lemma mset_set_eq_iff [simp]:
+lemma msubset_mset_set_iff[simp]:
   assumes "finite A" "finite B"
-  shows   "mset_set A = mset_set B \<longleftrightarrow> A = B"
-proof -
-  from assms have "mset_set A = mset_set B \<longleftrightarrow> set_mset (mset_set A) = set_mset (mset_set B)"
-    by (intro iffI equalityI set_mset_mono) auto
-  also from assms have "\<dots> \<longleftrightarrow> A = B" by simp
-  finally show ?thesis .
-qed
-
+  shows "mset_set A \<subseteq># mset_set B \<longleftrightarrow> A \<subseteq> B"
+  using assms set_mset_mono subset_imp_msubset_mset_set by fastforce
+
+lemma mset_set_eq_iff[simp]:
+  assumes "finite A" "finite B"
+  shows "mset_set A = mset_set B \<longleftrightarrow> A = B"
+  using assms by (fastforce dest: finite_set_mset_mset_set)
 
 (* Contributed by Lukas Bulwahn *)
 lemma image_mset_mset_set:
@@ -2158,17 +2132,14 @@
 lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
   by (induct D) simp_all
 
-lemma replicate_count_mset_eq_filter_eq:
-  "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
+lemma replicate_count_mset_eq_filter_eq: "replicate (count (mset xs) k) k = filter (HOL.eq k) xs"
   by (induct xs) auto
 
-lemma replicate_mset_eq_empty_iff [simp]:
-  "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
+lemma replicate_mset_eq_empty_iff [simp]: "replicate_mset n a = {#} \<longleftrightarrow> n = 0"
   by (induct n) simp_all
 
 lemma replicate_mset_eq_iff:
-  "replicate_mset m a = replicate_mset n b \<longleftrightarrow>
-    m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
+  "replicate_mset m a = replicate_mset n b \<longleftrightarrow> m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
   by (auto simp add: multiset_eq_iff)
 
 lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \<longleftrightarrow> A = B \<or> a = 0"
diff -r 18a6478a574c -r 97fc319d6089 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Aug 23 23:46:35 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Thu Aug 24 12:45:46 2017 +0100
@@ -278,7 +278,8 @@
         map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
       val overloaded_size_simps = flat overloaded_size_simpss;
       val size_thmss = map2 append size_simpss overloaded_size_simpss;
-      val size_gen_thmss = size_simpss
+      val size_gen_thmss = size_simpss;
+
       fun rhs_is_zero thm =
         let val Const (trueprop, _) $ (Const (eq, _) $ _ $ rhs) = Thm.prop_of thm in
           trueprop = @{const_name Trueprop} andalso eq = @{const_name HOL.eq} andalso