diff -r 78a009ac91d2 -r d7206afe2d28 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 23 20:41:15 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 23 22:05:53 2017 +0200
@@ -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"
@@ -1405,16 +1413,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"
@@ -2458,45 +2466,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
@@ -2517,11 +2529,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
 
@@ -3000,31 +3010,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"
@@ -3044,10 +3066,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) =
@@ -3098,6 +3120,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)
@@ -3112,8 +3136,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
 
@@ -4486,13 +4509,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"
@@ -7012,16 +7033,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)"
@@ -7115,8 +7136,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
@@ -7127,22 +7148,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 p and u::'a and v w and z::'b and t1 t2 l
       assume k: "0 < k"
@@ -7177,7 +7217,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"
@@ -7188,14 +7228,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"