# HG changeset patch
# User haftmann
# Date 1470848240 -7200
# Node ID abe0c3872d8a3cc95de3a75d7e2888aa16056e28
# Parent  7faa9bf9860bd42525964a90e2aef4677e84113f
keeping lifting rules local

diff -r 7faa9bf9860b -r abe0c3872d8a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 10 18:57:20 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 10 18:57:20 2016 +0200
@@ -1686,17 +1686,20 @@
   "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
+lemma comm_monoid_lift_option:
+  assumes "comm_monoid f z"
+  shows "comm_monoid (lift_option f) (Some z)"
+proof -
+  from assms interpret comm_monoid f z .
+  show ?thesis
+    by standard (auto simp: lift_option_def ac_simps split: bind_split)
+qed
+
+lemma comm_monoid_and: "comm_monoid HOL.conj True"
+  by standard auto
+
+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>
 
@@ -3893,45 +3896,51 @@
 
 lemma operative_integral:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
-  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) =
-        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
-    with k show ?thesis
-      apply (simp add: integrable_split)
-      apply (rule integral_unique [OF has_integral_split[OF _ _ k]])
-      apply (auto intro: integrable_integral)
-      done
-  next
-    case False
-    have "\<not> (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
-    proof (rule ccontr)
-      assume "\<not> ?thesis"
-      then have "f integrable_on cbox a b"
-        unfolding integrable_on_def
-        apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
-        apply (rule has_integral_split[OF _ _ k])
+  shows "comm_monoid.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)
+    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) =
+          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
+      with k show ?thesis
+        apply (simp add: integrable_split)
+        apply (rule integral_unique [OF has_integral_split[OF _ _ k]])
         apply (auto intro: integrable_integral)
         done
-      then show False
+    next
+    case False
+      have "\<not> (f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<or> \<not> ( f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k})"
+      proof (rule ccontr)
+        assume "\<not> ?thesis"
+        then have "f integrable_on cbox a b"
+          unfolding integrable_on_def
+          apply (rule_tac x="integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f + integral (cbox a b \<inter> {x. x \<bullet> k \<ge> c}) f" in exI)
+          apply (rule has_integral_split[OF _ _ k])
+          apply (auto intro: integrable_integral)
+          done
+        then show False
+          using False by auto
+      qed
+      then show ?thesis
         using False by auto
     qed
-    then show ?thesis
-      using False by auto
-  qed
-next
-  fix a b :: 'a
-  assume "content (cbox a b) = 0"
-  then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
-    using has_integral_null_eq
-    by (auto simp: integrable_on_null)
+  next
+    fix a b :: 'a
+    assume "content (cbox a b) = 0"
+    then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
+      using has_integral_null_eq
+      by (auto simp: integrable_on_null)
+  qed
 qed
 
 subsection \<open>Finally, the integral of a constant\<close>
@@ -5902,9 +5911,13 @@
     and "(f has_integral (j::'a::banach)) {c .. b}"
   shows "(f has_integral (i + j)) {a .. b}"
 proof -
-  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)]]
+  interpret comm_monoid "lift_option plus" "Some (0::'a)"
+    by (rule comm_monoid_lift_option)
+      (rule add.comm_monoid_axioms)
+  note operative_integral [of f, unfolded operative_1_le]
+  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"
     apply -
     apply (rule ccontr)
@@ -7625,8 +7638,14 @@
     qed
   }
   assume "cbox c d \<noteq> {}"
-  from partial_division_extend_1[OF assms(2) this] guess p . note p=this
-  note operat = comm_monoid_set.operative_division[OF add.comm_monoid_set_lift_option operative_integral p(1), symmetric]
+  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]
   let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
   {
     presume "?P"
@@ -7642,9 +7661,9 @@
       unfolding g_def
       by auto
   }
-  let ?F = "comm_monoid_set.F (lift_option op +) (Some 0)"
+  let ?F = F
   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)
+  proof (intro neutral ballI)
     fix x
     assume x: "x \<in> p - {cbox c d}"
     then have "x \<in> p"
@@ -7666,6 +7685,11 @@
 
   have *: "p = insert (cbox c d) (p - {cbox c d})"
     using p by auto
+  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
   have **: "g integrable_on cbox c d"
     apply (rule integrable_spike_interior[where f=f])
     unfolding g_def  using assms(1)
@@ -7684,7 +7708,7 @@
     unfolding operat
     using p
     apply (subst *)
-    apply (subst comm_monoid_set.insert[OF add.comm_monoid_set_lift_option])
+    apply (subst insert)
     apply (simp_all add: division_of_finite iterate)
     done
 qed