author paulson Fri, 04 Aug 2017 21:30:38 +0200 changeset 66339 1c5e521a98f1 parent 66331 f773691617c0 child 66340 91257fbcabee
more horrible proofs disentangled
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 03 12:50:03 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Aug 04 21:30:38 2017 +0200
@@ -574,11 +574,14 @@
shows "integral\<^sup>N lborel f = I"
proof -
from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
-  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
+  from borel_measurable_implies_simple_function_sequence'[OF this]
+  obtain F where F: "\<And>i. simple_function lborel (F i)" "incseq F"
+                 "\<And>i x. F i x < top" "\<And>x. (SUP i. F i x) = ennreal (f x)"
+    by blast
+  then have [measurable]: "\<And>i. F i \<in> borel_measurable lborel"
+    by (metis borel_measurable_simple_function)
let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"

-  note F(1)[THEN borel_measurable_simple_function, measurable]
-
have "0 \<le> I"
using I by (rule has_integral_nonneg) (simp add: nonneg)

@@ -1643,22 +1646,22 @@
fix x
have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
apply (rule separate_point_closed)
-        apply (rule closed_Union)
-        apply (rule finite_subset[OF _ d'(1)])
+         apply (rule closed_Union)
+          apply (rule finite_subset[OF _ d'(1)])
using d'(4)
-        apply auto
+          apply auto
done
then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
by force
qed
then obtain k where k: "\<And>x. 0 < k x"
-                       "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
+      "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
by metis
have "e/2 > 0"
using e by auto
from henstock_lemma[OF assms(1) this]
obtain g where g: "gauge g"
-          "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; g fine p\<rbrakk>
+      "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; g fine p\<rbrakk>
\<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
by (metis (no_types, lifting))
let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
@@ -1686,12 +1689,12 @@
apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
{(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
unfolding p'_def
-          defer
-          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
+           defer
+           apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
apply safe
unfolding image_iff
apply (rule_tac x="(i,x,l)" in bexI)
-          apply auto
+           apply auto
done
fix x k
assume "(x, k) \<in> p'"
@@ -1729,11 +1732,11 @@
unfolding p'_def using d' by auto
show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
apply rule
-          apply (rule Union_least)
+           apply (rule Union_least)
unfolding mem_Collect_eq
-          apply (erule exE)
-          apply (drule *[rule_format])
-          apply safe
+           apply (erule exE)
+           apply (drule *[rule_format])
+           apply safe
proof -
fix y
assume y: "y \<in> cbox a b"
@@ -1749,7 +1752,7 @@
unfolding p'_def Union_iff
apply (rule_tac x="i \<inter> l" in bexI)
using i xl
-            apply auto
+             apply auto
done
qed
qed
@@ -1801,7 +1804,7 @@
unfolding real_norm_def
apply (rule *[rule_format,OF **])
apply safe
-        apply(rule d(2))
+           apply(rule d(2))
proof goal_cases
case 1
show ?case
@@ -1814,161 +1817,145 @@
have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
proof (rule sum_mono, goal_cases)
case k: (1 k)
-          from d'(4)[OF this] guess u v by (elim exE) note uv=this
+          from d'(4)[OF this] obtain u v where uv: "k = cbox u v" by metis
define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
note uvab = d'(2)[OF k[unfolded uv]]
have "d' division_of cbox u v"
apply (subst d'_def)
apply (rule division_inter_1)
-            apply (rule division_of_tagged_division[OF p(1)])
+             apply (rule division_of_tagged_division[OF p(1)])
apply (rule uvab)
done
then have "norm (integral k f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
unfolding uv
apply (subst integral_combine_division_topdown[of _ _ d'])
-            apply (rule integrable_on_subcbox[OF assms(1) uvab])
-            apply assumption
+              apply (rule integrable_on_subcbox[OF assms(1) uvab])
+             apply assumption
apply (rule sum_norm_le)
apply auto
done
also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
-            apply (rule sum.mono_neutral_left)
-            apply (subst Setcompr_eq_image)
-            apply (rule finite_imageI)+
-            apply fact
-            unfolding d'_def uv
-            apply blast
-          proof (rule, goal_cases)
-            case prems: (1 i)
-            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
-              by auto
-            from this[unfolded mem_Collect_eq] guess l .. note l=this
-            then have "cbox u v \<inter> l = {}"
-              using prems by auto
-            then show ?case
-              using l by auto
+          proof -
+            have *: "norm (integral i f) = 0"
+              if "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
+                "i \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for i
+              using that by auto
+            show ?thesis
+              apply (rule sum.mono_neutral_left)
+              unfolding d'_def uv using * by auto
qed
also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
-            unfolding Setcompr_eq_image
-            apply (rule sum.reindex_nontrivial [unfolded o_def])
-            apply (rule finite_imageI)
-            apply (rule p')
-          proof goal_cases
-            case prems: (1 l y)
-            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
-              apply (subst(2) interior_Int)
-              by (metis Int_lower2 Int_subset_iff interior_mono prems(4))
-            then have *: "interior (k \<inter> l) = {}"
-              using snd_p(5)[OF prems(1-3)] by auto
-            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
-            show ?case
-              using *
-              unfolding uv Int_interval content_eq_0_interior[symmetric]
-              by auto
+          proof -
+            have *: "norm (integral (k \<inter> l) f) = 0"
+              if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "k \<inter> l = k \<inter> y" for l y
+            proof -
+              have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
+                by (metis Int_lower2 interior_mono le_inf_iff that(4))
+              then have "interior (k \<inter> l) = {}"
+                by (simp add: snd_p(5) that)
+              moreover from d'(4)[OF k] snd_p(4)[OF that(1)]
+              obtain u1 v1 u2 v2
+                where uv: "k = cbox u1 u2" "l = cbox v1 v2" by metis
+              ultimately show ?thesis
+                using that integral_null
+                unfolding uv Int_interval content_eq_0_interior
+                by (metis (mono_tags, lifting) norm_eq_zero)
+            qed
+            show ?thesis
+              unfolding Setcompr_eq_image
+              apply (rule sum.reindex_nontrivial [unfolded o_def])
+               apply (rule finite_imageI)
+               apply (rule p')
+              using * by auto
qed
finally show ?case .
qed
also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> (snd ` p). norm (integral (i\<inter>l) f))"
-          apply (subst sum_Sigma_product[symmetric])
-          apply fact
-          using p'(1)
-          apply auto
-          done
also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
by (force simp: split_def Sigma_def intro!: sum.cong)
also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
-          unfolding *
-          apply (rule sum.reindex_nontrivial [symmetric, unfolded o_def])
-          apply (rule finite_product_dependent)
-          apply fact
-          apply (rule finite_imageI)
-          apply (rule p')
-          unfolding split_paired_all mem_Collect_eq split_conv o_def
proof -
-          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
-          fix l1 l2 k1 k2
-          assume as:
-            "(l1, k1) \<noteq> (l2, k2)"
-            "l1 \<inter> k1 = l2 \<inter> k2"
-            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
-            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
-          then have "l1 \<in> d" and "k1 \<in> snd ` p"
-            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
-          guess u1 v1 u2 v2 by (elim exE) note uv=this
-          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
-            using as by auto
-          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-            by (metis Pair_inject \<open>k1 \<in> snd ` p\<close> \<open>l1 \<in> d\<close> as(4) d'(5) snd_p(5))
-          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
-            using as(2) by auto
-          ultimately have "interior(l1 \<inter> k1) = {}"
-            by auto
-          then show "norm (integral (l1 \<inter> k1) f) = 0"
-            unfolding uv Int_interval
-            unfolding content_eq_0_interior[symmetric]
-            by auto
+          have eq0: " (integral (l1 \<inter> k1) f) = 0"
+            if "l1 \<inter> k1 = l2 \<inter> k2" "(l1, k1) \<noteq> (l2, k2)"
+              "l1 \<in> d" "(j1,k1) \<in> p" "l2 \<in> d" "(j2,k2) \<in> p"
+            for l1 l2 k1 k2 j1 j2
+          proof -
+            obtain u1 v1 u2 v2 where uv: "l1 = cbox u1 u2" "k1 = cbox v1 v2"
+              using \<open>(j1, k1) \<in> p\<close> \<open>l1 \<in> d\<close> d'(4) p'(4) by blast
+            have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+              using that by auto
+            then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+              by (meson d'(5) old.prod.inject p'(5) that(3) that(4) that(5) that(6))
+            moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
+            ultimately have "interior(l1 \<inter> k1) = {}"
+              by auto
+            then show ?thesis
+              unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
+          qed
+          show ?thesis
+            unfolding *
+            apply (rule sum.reindex_nontrivial [symmetric, unfolded o_def])
+             apply (rule finite_product_dependent [OF \<open>finite d\<close>])
+             apply (rule finite_imageI [OF \<open>finite p\<close>])
+            apply clarsimp
+            by (metis eq0 fst_conv snd_conv)
qed
also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
-          unfolding sum_p'
-          apply (rule sum.mono_neutral_right)
-          apply (subst *)
-          apply (rule finite_imageI[OF finite_product_dependent])
-          apply fact
-          apply (rule finite_imageI[OF p'(1)])
-          apply safe
-        proof goal_cases
-          case (2 i ia l a b)
-          then have "ia \<inter> b = {}"
-            unfolding p'alt image_iff Bex_def not_ex
-            apply (erule_tac x="(a, ia \<inter> b)" in allE)
-            apply auto
-            done
-          then show ?case
-            by auto
-        next
-          case (1 x a b)
-          then show ?case
-            unfolding p'_def
+        proof -
+          have 0: "integral (ia \<inter> snd (a, b)) f = 0"
+            if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for  ia a b
proof -
-            assume "(a, b) \<in> {(x, k) |x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l}"
-            then have "\<exists>n N. (a, b) = (n, N) \<and> (\<exists>Na Nb. n \<in> Na \<and> Na \<in> d \<and> (n, Nb) \<in> p \<and> N = Na \<inter> Nb)"
-              by force
+            have "ia \<inter> b = {}"
+              using that
+              unfolding p'alt image_iff Bex_def not_ex
+              apply (erule_tac x="(a, ia \<inter> b)" in allE)
+              apply auto
+              done
then show ?thesis
-              by (metis (no_types) image_iff snd_conv)
+              by auto
+          qed
+          have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
+          proof -
+            have "\<exists>n N Na. (a, b) = (n, N \<inter> Na) \<and> (n, Na) \<in> p \<and> N \<in> d \<and> N \<inter> Na \<noteq> {}"
+              using that p'alt by blast
+            then show "\<exists>N Na. snd (a, b) = N \<inter> Na \<and> N \<in> d \<and> Na \<in> snd ` p"
+              by (metis (no_types) imageI prod.sel(2))
qed
+          show ?thesis
+            unfolding sum_p'
+            apply (rule sum.mono_neutral_right)
+              apply (subst *)
+              apply (rule finite_imageI[OF finite_product_dependent])
+               apply fact
+              apply (rule finite_imageI[OF p'(1)])
+            using 0 1 by auto
qed
finally show ?case .
next
case 3
let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
-          apply safe
-          unfolding image_iff
-          apply (rule_tac x="((x,l),i)" in bexI)
-          apply auto
-          done
-        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
+          by force
+        have pdfin: "finite (p \<times> d)"
+          using finite_cartesian_product[OF p'(1) d'(1)] by metis
have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
unfolding norm_scaleR
apply (rule sum.mono_neutral_left)
-          apply (subst *)
-          apply (rule finite_imageI)
-          apply fact
-          unfolding p'alt
-          apply blast
-          apply safe
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x=i in exI)
-          apply (rule_tac x=l in exI)
-          apply auto
-          done
+            apply (subst *)
+            apply (rule finite_imageI)
+            apply fact
+          unfolding p'alt apply blast
+          by fastforce
also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
unfolding *
apply (subst sum.reindex_nontrivial)
-          apply fact
+            apply fact
unfolding split_paired_all
unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
-          apply (elim conjE)
+           apply (elim conjE)
proof -
fix x1 l1 k1 x2 l2 k2
assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
@@ -1979,11 +1966,11 @@
then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
apply -
apply (erule disjE)
-            apply (rule disjI2)
-            defer
-            apply (rule disjI1)
-            apply (rule d'(5)[OF as(3-4)])
-            apply assumption
+             apply (rule disjI2)
+             defer
+             apply (rule disjI1)
+             apply (rule d'(5)[OF as(3-4)])
+             apply assumption
apply (rule p'(5)[OF as(1-2)])
apply auto
done
@@ -1998,10 +1985,10 @@
qed safe
also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
apply (subst sum_Sigma_product[symmetric])
-          apply (rule p')
-          apply (rule d')
+            apply (rule p')
+           apply (rule d')
apply (rule sum.cong)
-          apply (rule refl)
+           apply (rule refl)
unfolding split_paired_all split_conv
proof -
fix x l
@@ -2013,7 +2000,7 @@
also have "\<dots> = sum content {k \<inter> cbox u v| k. k \<in> d}"
unfolding Setcompr_eq_image
apply (rule sum.reindex_nontrivial [unfolded o_def, symmetric])
-            apply (rule d')
+             apply (rule d')
proof goal_cases
case prems: (1 k y)
from d'(4)[OF this(1)] d'(4)[OF this(2)]
@@ -2033,29 +2020,16 @@
also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
apply (rule sum.mono_neutral_right)
unfolding Setcompr_eq_image
-            apply (rule finite_imageI)
-            apply (rule d')
-            apply blast
-            apply safe
-            apply (rule_tac x=k in exI)
-          proof goal_cases
-            case prems: (1 i k)
-            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
-            have "interior (k \<inter> cbox u v) \<noteq> {}"
-              using prems(2)
-              unfolding ab Int_interval content_eq_0_interior
-              by auto
-            then show ?case
-              using prems(1)
-              using interior_subset[of "k \<inter> cbox u v"]
-              by auto
-          qed
+              apply (rule finite_imageI)
+              apply (rule d')
+             apply (fastforce simp: inf.commute)+
+            done
finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
unfolding sum_distrib_right[symmetric] real_scaleR_def