author paulson Wed, 09 Aug 2017 23:41:47 +0200 changeset 66388 8e614c223000 parent 66387 5db8427fdfd3 child 66389 fa473c07d86c child 66400 abb7f0a71e74
fundamental_theorem_of_calculus_interior: more cleanup
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 09 13:41:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 09 23:41:47 2017 +0200
@@ -3811,7 +3811,7 @@
then show "0 \<le> e * ((Sup k) - (Inf k))"
unfolding uv using e by (auto simp add: field_simps)
qed
-      have **: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
+      have norm_le: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a) / 2"
proof -
have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
by auto
@@ -3831,16 +3831,11 @@
by auto
then obtain u v where uv: "k = cbox u v"
using p(4) by blast
-          have "k \<noteq> {}"
-            using p(2)[OF xk] by auto
-          then have *: "u = v"
-            using xk k0 by (auto simp: uv content_eq_0 box_eq_empty)
+          then have "u = v"
+            using xk k0 p(2) by force
then show "content k *\<^sub>R (f' (x)) - (f ((Sup k)) - f ((Inf k))) = 0"
using xk unfolding uv by auto
next
-          have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} =
-            {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}"
-            by blast
have **: "norm (sum f s) \<le> e"
if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y" "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e" "e > 0"
for s f and e :: real
@@ -3851,135 +3846,102 @@
case False
then obtain x where "x \<in> s"
by auto
-            then have *: "s = {x}"
+            then have "s = {x}"
using that(1) by auto
then show ?thesis
using \<open>x \<in> s\<close> that(2) by auto
qed
case 2
+            let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
+          have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} = ?B a \<union> ?B b"
+            by blast
show ?case
apply (subst *)
apply (subst sum.union_disjoint)
prefer 4
apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
-            apply (rule_tac[1-2] **)
+                 apply (rule_tac[1-2] **)
+
proof -
-            let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
proof -
obtain u v where uv: "k = cbox u v"
using \<open>(a, k) \<in> p\<close> p(4) by blast
-              then have *: "u \<le> v"
-                using p(2)[OF that] by auto
-              have u: "u = a"
-              proof (rule ccontr)
-                have "u \<in> cbox u v"
-                  using p(2-3)[OF that(1)] unfolding uv by auto
-                have "u \<ge> a"
-                  using p(2-3)[OF that(1)] unfolding uv subset_eq by auto
-                moreover assume "\<not> ?thesis"
-                ultimately have "u > a" by auto
-                then show False
-                  using p(2)[OF that(1)] unfolding uv by (auto simp add:)
-              qed
-              then show ?thesis
-                apply (rule_tac x=v in exI)
-                unfolding uv
-                using *
-                apply auto
-                done
+              moreover have "u \<le> v"
+                using uv p(2)[OF that] by auto
+              moreover have "u = a"
+                using p(2) p(3) that uv by force
+              ultimately show ?thesis
+                by blast
qed
have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
proof -
obtain u v where uv: "k = cbox u v"
using \<open>(b, k) \<in> p\<close> p(4) by blast
-              have *: "u \<le> v"
+              moreover have "u \<le> v"
using p(2)[OF that] unfolding uv by auto
-              have u: "v = b"
-              proof (rule ccontr)
-                have "u \<in> cbox u v"
-                  using p(2-3)[OF that(1)] unfolding uv by auto
-                have "v \<le> b"
-                  using p(2-3)[OF that(1)] unfolding uv subset_eq by auto
-                moreover assume "\<not> ?thesis"
-                ultimately have "v < b" by auto
-                then show False
-                  using p(2)[OF that(1)] unfolding uv by (auto simp add:)
-              qed
-              then show ?thesis
-                apply (rule_tac x=u in exI)
-                unfolding uv
-                using *
-                apply auto
-                done
+              moreover have "v = b"
+                using p(2) p(3) that uv by force
+              ultimately show ?thesis
+                by blast
qed
show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
-              apply (rule,rule,rule,unfold split_paired_all)
-              unfolding mem_Collect_eq fst_conv snd_conv
-              apply safe
-            proof -
+            proof (safe; clarsimp)
fix x k k'
assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
-              guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
-              guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
+              obtain v where v: "k = cbox a v" "a \<le> v"
+                using pa[OF k(1)] by blast
+              obtain v' where v': "k' = cbox a v'" "a \<le> v'"
+                using pa[OF k(2)] by blast
+              let ?v = "min v v'"
have "box a ?v \<subseteq> k \<inter> k'"
unfolding v v' by (auto simp add: mem_box)
-              note interior_mono[OF this,unfolded interior_Int]
+              then have "interior (box a (min v v')) \<subseteq> interior k \<inter> interior k'"
+                using interior_Int interior_mono by blast
moreover have "(a + ?v)/2 \<in> box a ?v"
using k(3-)
unfolding v v' content_eq_0 not_le
ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
unfolding interior_open[OF open_box] by auto
-              then have *: "k = k'"
-                apply -
-                apply (rule ccontr)
-                using p(5)[OF k(1-2)]
-                apply auto
-                done
-              { assume "x \<in> k" then show "x \<in> k'" unfolding * . }
-              { assume "x \<in> k'" then show "x \<in> k" unfolding * . }
+              then have eq: "k = k'"
+                using p(5)[OF k(1-2)] by auto
+              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
+              { assume "x \<in> k'" then show "x \<in> k" unfolding eq . }
qed
+
show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
-              apply rule
-              apply rule
-              apply rule
-              apply (unfold split_paired_all)
-              unfolding mem_Collect_eq fst_conv snd_conv
-              apply safe
-            proof -
+            proof (safe; clarsimp)
fix x k k'
assume k: "(b, k) \<in> p" "(b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
-              guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
-              guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this]
+              obtain v where v: "k = cbox v b" "v \<le> b"
+                using pb[OF k(1)] by blast
+              obtain v' where v': "k' = cbox v' b" "v' \<le> b"
+                using pb[OF k(2)] by blast
let ?v = "max v v'"
have "box ?v b \<subseteq> k \<inter> k'"
unfolding v v' by (auto simp: mem_box)
-                note interior_mono[OF this,unfolded interior_Int]
+              then have "interior (box (max v v') b) \<subseteq> interior k \<inter> interior k'"
+                using interior_Int interior_mono by blast
moreover have " ((b + ?v)/2) \<in> box ?v b"
using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
unfolding interior_open[OF open_box] by auto
-              then have *: "k = k'"
-                apply -
-                apply (rule ccontr)
-                using p(5)[OF k(1-2)]
-                apply auto
-                done
-              { assume "x \<in> k" then show "x \<in> k'" unfolding * . }
-              { assume "x \<in> k'" then show "x\<in>k" unfolding * . }
+              then have eq: "k = k'"
+                using p(5)[OF k(1-2)] by auto
+              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
+              { assume "x \<in> k'" then show "x\<in>k" unfolding eq . }
qed

-            let ?a = a and ?b = b (* a is something else while proofing the next theorem. *)
have "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
proof -
obtain v where v: "c = cbox a v" and "a \<le> v"
using pa[OF \<open>(a, c) \<in> p\<close>] by metis
-              then have "?a \<in> {?a..v}" "v \<le> ?b"
+              then have "a \<in> {a..v}" "v \<le> b"
using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
-              moreover have "{?a..v} \<subseteq> ball ?a da"
+              moreover have "{a..v} \<subseteq> ball a da"
using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
ultimately show ?thesis
unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
@@ -3994,9 +3956,9 @@
proof -
obtain v where v: "c = cbox v b" and "v \<le> b"
using \<open>(b, c) \<in> p\<close> pb by blast
-              then have "v \<ge> ?a""?b \<in> {v.. ?b}"
+              then have "v \<ge> a""b \<in> {v.. b}"
using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
-              moreover have "{v..?b} \<subseteq> ball ?b db"
+              moreover have "{v..b} \<subseteq> ball b db"
using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
ultimately show ?thesis
using db v by auto
@@ -4019,7 +3981,7 @@
unfolding sum_distrib_left[symmetric]