# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1504126001 -3600
# Node ID 116f658195af7ab7f8aedd1f21b7d8bee66c53af
# Parent  19bf4d5966dce39d88ff958d000a1ae2cfafc625
unscrambled has_integral_Union

diff -r 19bf4d5966dc -r 116f658195af src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Aug 29 20:34:43 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 30 21:46:41 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