# HG changeset patch
# User paulson
# Date 1504129904 -3600
# Node ID ad0cefe1e9a9cdfec1dab066a351c74a69cc6018
# Parent  beb48215cda765ef8cd92e596c230c0f1563433b# Parent  8f12f7e0d99702bb7e65a773206aaeb9c528df13
merged

diff -r beb48215cda7 -r ad0cefe1e9a9 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 30 23:36:21 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 30 22:51:44 2017 +0100
@@ -685,10 +685,10 @@
   unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..
 
 lemma has_integral_sum:
-  assumes "finite t"
-    and "\<forall>a\<in>t. ((f a) has_integral (i a)) S"
-  shows "((\<lambda>x. sum (\<lambda>a. f a x) t) has_integral (sum i t)) S"
-  using assms(1) subset_refl[of t]
+  assumes "finite T"
+    and "\<And>a. a \<in> T \<Longrightarrow> ((f a) has_integral (i a)) S"
+  shows "((\<lambda>x. sum (\<lambda>a. f a x) T) has_integral (sum i T)) S"
+  using assms(1) subset_refl[of T]
 proof (induct rule: finite_subset_induct)
   case empty
   then show ?case by auto
@@ -2328,9 +2328,9 @@
   using assms by (induct s) auto
 
 lemma negligible_Union[intro]:
-  assumes "finite s"
-    and "\<forall>t\<in>s. negligible t"
-  shows "negligible(\<Union>s)"
+  assumes "finite \<T>"
+    and "\<And>t. t \<in> \<T> \<Longrightarrow> negligible t"
+  shows "negligible(\<Union>\<T>)"
   using assms by induct auto
 
 lemma negligible:
@@ -5123,43 +5123,42 @@
 
 lemma has_integral_Union:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "finite t"
-    and "\<forall>s\<in>t. (f has_integral (i s)) s"
-    and "\<forall>s\<in>t. \<forall>s'\<in>t. s \<noteq> s' \<longrightarrow> negligible (s \<inter> s')"
-  shows "(f has_integral (sum i t)) (\<Union>t)"
+  assumes \<T>: "finite \<T>"
+    and int: "\<And>S. S \<in> \<T> \<Longrightarrow> (f has_integral (i S)) S"
+    and neg: "\<And>S S'. \<lbrakk>S \<in> \<T>; S' \<in> \<T>; S \<noteq> S'\<rbrakk> \<Longrightarrow> negligible (S \<inter> S')"
+  shows "(f has_integral (sum i \<T>)) (\<Union>\<T>)"
 proof -
-  note * = has_integral_restrict_UNIV[symmetric, of f]
-  have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))"
-    apply (rule negligible_Union)
-    apply (rule finite_imageI)
-    apply (rule finite_subset[of _ "t \<times> t"])
-    defer
-    apply (rule finite_cartesian_product[OF assms(1,1)])
-    using assms(3)
-    apply auto
-    done
-  note assms(2)[unfolded *]
-  note has_integral_sum[OF assms(1) this]
+  let ?\<U> = "((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> \<T> \<and> b \<in> {y. y \<in> \<T> \<and> a \<noteq> y}})"
+  have "((\<lambda>x. if x \<in> \<Union>\<T> then f x else 0) has_integral sum i \<T>) UNIV"
+  proof (rule has_integral_spike)
+    show "negligible (\<Union>?\<U>)"
+    proof (rule negligible_Union)
+      have "finite (\<T> \<times> \<T>)"
+        by (simp add: \<T>)
+      moreover have "{(a, b). a \<in> \<T> \<and> b \<in> {y \<in> \<T>. a \<noteq> y}} \<subseteq> \<T> \<times> \<T>"
+        by auto
+      ultimately show "finite ?\<U>"
+        by (blast intro: finite_subset[of _ "\<T> \<times> \<T>"])
+      show "\<And>t. t \<in> ?\<U> \<Longrightarrow> negligible t"
+        using neg by auto
+    qed
+  next
+    show "(if x \<in> \<Union>\<T> then f x else 0) = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
+      if "x \<in> UNIV - (\<Union>?\<U>)" for x
+    proof clarsimp
+      fix S assume "S \<in> \<T>" "x \<in> S"
+      moreover then have "\<forall>b\<in>\<T>. x \<in> b \<longleftrightarrow> b = S"
+        using that by blast
+      ultimately show "f x = (\<Sum>A\<in>\<T>. if x \<in> A then f x else 0)"
+        by (simp add: sum.delta[OF \<T>])
+    qed 
+  next
+    show "((\<lambda>x. \<Sum>A\<in>\<T>. if x \<in> A then f x else 0) has_integral (\<Sum>A\<in>\<T>. i A)) UNIV"
+      apply (rule has_integral_sum [OF \<T>])
+      using int by (simp add: has_integral_restrict_UNIV)
+  qed
   then show ?thesis
-    unfolding *
-    apply -
-    apply (rule has_integral_spike[OF **])
-    defer
-    apply assumption
-    apply safe
-  proof goal_cases
-    case prems: (1 x)
-    then show ?case
-    proof (cases "x \<in> \<Union>t")
-      case True
-      then obtain s where "s \<in> t" "x \<in> s"
-        by blast
-      moreover then have "\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s"
-        using prems(3) by blast
-      ultimately show ?thesis
-        by (simp add: sum.delta[OF assms(1)])
-    qed auto
-  qed
+    using has_integral_restrict_UNIV by blast
 qed
 
 
@@ -5167,61 +5166,54 @@
 
 lemma has_integral_combine_division:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of S"
-    and "\<And>k. k \<in> d \<Longrightarrow> (f has_integral (i k)) k"
-  shows "(f has_integral (sum i d)) S"
+  assumes "\<D> division_of S"
+    and "\<And>k. k \<in> \<D> \<Longrightarrow> (f has_integral (i k)) k"
+  shows "(f has_integral (sum i \<D>)) S"
 proof -
-  note d = division_ofD[OF assms(1)]
-  have neg: "negligible (S \<inter> s')" if "S \<in> d" "s' \<in> d" "S \<noteq> s'" for S s'
+  note \<D> = division_ofD[OF assms(1)]
+  have neg: "negligible (S \<inter> s')" if "S \<in> \<D>" "s' \<in> \<D>" "S \<noteq> s'" for S s'
   proof -
-    obtain a c b d where obt: "S = cbox a b" "s' = cbox c d"
-      by (meson \<open>S \<in> d\<close> \<open>s' \<in> d\<close> d(4))
-    from d(5)[OF that] show ?thesis
+    obtain a c b \<D> where obt: "S = cbox a b" "s' = cbox c \<D>"
+      by (meson \<open>S \<in> \<D>\<close> \<open>s' \<in> \<D>\<close> \<D>(4))
+    from \<D>(5)[OF that] show ?thesis
       unfolding obt interior_cbox
       by (metis (no_types, lifting) Diff_empty Int_interval box_Int_box negligible_frontier_interval)
   qed
   show ?thesis
-    unfolding d(6)[symmetric]
-    by (auto intro: d neg assms has_integral_Union)
+    unfolding \<D>(6)[symmetric]
+    by (auto intro: \<D> neg assms has_integral_Union)
 qed
 
 lemma integral_combine_division_bottomup:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of S"
-    and "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k"
-  shows "integral S f = sum (\<lambda>i. integral i f) d"
+  assumes "\<D> division_of S" "\<And>k. k \<in> \<D> \<Longrightarrow> f integrable_on k"
+  shows "integral S f = sum (\<lambda>i. integral i f) \<D>"
   apply (rule integral_unique)
-  apply (rule has_integral_combine_division[OF assms(1)])
-  using assms(2)
-  unfolding has_integral_integral
-  apply assumption
-  done
+  by (meson assms has_integral_combine_division has_integral_integrable_integral)
 
 lemma has_integral_combine_division_topdown:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on S"
-    and "d division_of k"
-    and "k \<subseteq> S"
-  shows "(f has_integral (sum (\<lambda>i. integral i f) d)) k"
-  apply (rule has_integral_combine_division[OF assms(2)])
-  unfolding has_integral_integral[symmetric]
-proof goal_cases
-  case (1 k)
-  from division_ofD(2,4)[OF assms(2) this]
-  show ?case
-    apply safe
-    apply (rule integrable_on_subcbox)
-    apply (rule assms)
-    using assms(3)
-    apply auto
-    done
+  assumes f: "f integrable_on S"
+    and \<D>: "\<D> division_of K"
+    and "K \<subseteq> S"
+  shows "(f has_integral (sum (\<lambda>i. integral i f) \<D>)) K"
+proof -
+  have "f integrable_on L" if "L \<in> \<D>" for L
+  proof -
+    have "L \<subseteq> S"
+      using \<open>K \<subseteq> S\<close> \<D> that by blast
+    then show "f integrable_on L"
+      using that by (metis (no_types) f \<D> division_ofD(4) integrable_on_subcbox)
+  qed
+  then show ?thesis
+    by (meson \<D> has_integral_combine_division has_integral_integrable_integral)
 qed
 
 lemma integral_combine_division_topdown:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on S"
-    and "d division_of S"
-  shows "integral S f = sum (\<lambda>i. integral i f) d"
+    and "\<D> division_of S"
+  shows "integral S f = sum (\<lambda>i. integral i f) \<D>"
   apply (rule integral_unique)
   apply (rule has_integral_combine_division_topdown)
   using assms
@@ -5230,30 +5222,27 @@
 
 lemma integrable_combine_division:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of S"
-    and "\<forall>i\<in>d. f integrable_on i"
+  assumes \<D>: "\<D> division_of S"
+    and f: "\<And>i. i \<in> \<D> \<Longrightarrow> f integrable_on i"
   shows "f integrable_on S"
-  using assms(2)
-  unfolding integrable_on_def
-  by (metis has_integral_combine_division[OF assms(1)])
+  using f unfolding integrable_on_def by (metis has_integral_combine_division[OF \<D>])
 
 lemma integrable_on_subdivision:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of i"
-    and "f integrable_on S"
+  assumes \<D>: "\<D> division_of i"
+    and f: "f integrable_on S"
     and "i \<subseteq> S"
   shows "f integrable_on i"
-  apply (rule integrable_combine_division assms)+
-  apply safe
-proof goal_cases
-  case 1
-  note division_ofD(2,4)[OF assms(1) this]
-  then show ?case
-    apply safe
-    apply (rule integrable_on_subcbox[OF assms(2)])
-    using assms(3)
-    apply auto
-    done
+proof -
+  have "f integrable_on i" if "i \<in> \<D>" for i
+proof -
+  have "i \<subseteq> S"
+    using assms that by auto
+  then show "f integrable_on i"
+    using that by (metis (no_types) \<D> f division_ofD(4) integrable_on_subcbox)
+qed
+  then show ?thesis
+    using \<D> integrable_combine_division by blast
 qed
 
 
@@ -5294,16 +5283,14 @@
 
 lemma has_integral_combine_tagged_division_topdown:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on cbox a b"
-    and "p tagged_division_of (cbox a b)"
-  shows "(f has_integral (sum (\<lambda>(x,k). integral k f) p)) (cbox a b)"
-  apply (rule has_integral_combine_tagged_division[OF assms(2)])
-  apply safe
-proof goal_cases
-  case 1
-  note tagged_division_ofD(3-4)[OF assms(2) this]
-  then show ?case
-    using integrable_subinterval[OF assms(1)] by blast
+  assumes f: "f integrable_on cbox a b"
+    and p: "p tagged_division_of (cbox a b)"
+  shows "(f has_integral (sum (\<lambda>(x,K). integral K f) p)) (cbox a b)"
+proof -
+  have "(f has_integral integral K f) K" if "(x,K) \<in> p" for x K
+    by (metis assms integrable_integral integrable_on_subcbox tagged_division_ofD(3,4) that)
+  then show ?thesis
+    by (metis assms case_prodI2 has_integral_integrable_integral integral_combine_tagged_division_bottomup)
 qed
 
 lemma integral_combine_tagged_division_topdown:
@@ -5311,10 +5298,8 @@
   assumes "f integrable_on cbox a b"
     and "p tagged_division_of (cbox a b)"
   shows "integral (cbox a b) f = sum (\<lambda>(x,k). integral k f) p"
-  apply (rule integral_unique)
-  apply (rule has_integral_combine_tagged_division_topdown)
-  using assms
-  apply auto
+  apply (rule integral_unique [OF has_integral_combine_tagged_division_topdown])
+  using assms apply auto
   done