author paulson Fri, 25 Aug 2017 13:01:01 +0100 changeset 66508 29d684ce2325 parent 66507 678774070c9b child 66509 65b6d48fc9a9
unscrambling of integrable_alt
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 25 11:10:03 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 25 13:01:01 2017 +0100
@@ -5061,80 +5061,67 @@
next
let ?F = "\<lambda>x. if x \<in> s then f x else 0"
assume rhs: ?r
-  note as = conjunctD2[OF this,rule_format]
let ?cube = "\<lambda>n. cbox (\<Sum>i\<in>Basis. - real n *\<^sub>R i::'n) (\<Sum>i\<in>Basis. real n *\<^sub>R i)"
-  have "Cauchy (\<lambda>n. integral (?cube n) (\<lambda>x. if x \<in> s then f x else 0))"
-  proof (unfold Cauchy_def, safe, goal_cases)
-    case (1 e)
+  have "Cauchy (\<lambda>n. integral (?cube n) ?F)"
+    unfolding Cauchy_def
+  proof (intro allI impI)
+    fix e::real
+    assume "e > 0"
with rhs obtain B where "0 < B"
and B: "\<And>a b c d. ball 0 B \<subseteq> cbox a b \<and> ball 0 B \<subseteq> cbox c d
\<Longrightarrow> norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e"
by blast
obtain N where N: "B \<le> real N"
using real_arch_simple by blast
-    {
-      fix n
-      assume n: "n \<ge> N"
+    have "ball 0 B \<subseteq> ?cube n" if n: "n \<ge> N" for n
+    proof -
have "sum (op *\<^sub>R (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
x \<bullet> i \<le> sum (op *\<^sub>R (real n)) Basis \<bullet> i"
if "norm x < B" "i \<in> Basis" for x i::'n
using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
-      then have "ball 0 B \<subseteq> ?cube n"
+      then show ?thesis
by (auto simp: mem_box dist_norm)
-    }
-    then show ?case
+    qed
+    then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (integral (?cube m) ?F) (integral (?cube n) ?F) < e"
by (fastforce simp add: dist_norm intro!: B)
qed
-  from this[unfolded convergent_eq_Cauchy[symmetric]] guess i ..
-  note i = this[THEN LIMSEQ_D]
-
-  show ?l unfolding integrable_on_def has_integral_alt'[of f]
-    apply (rule_tac x=i in exI)
-    apply safe
-    apply (rule as(1)[unfolded integrable_on_def])
-  proof goal_cases
-    case (1 e)
-    then have *: "e/2 > 0" by auto
-    from i[OF this] guess N..note N =this[rule_format]
-    from as(2)[OF *] guess B..note B=conjunctD2[OF this,rule_format]
+  then obtain i where i: "(\<lambda>n. integral (?cube n) ?F) \<longlonglongrightarrow> i"
+    using convergent_eq_Cauchy by blast
+  have "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow> norm (integral (cbox a b) ?F - i) < e"
+    if "e > 0" for e
+  proof -
+    have *: "e/2 > 0" using that by auto
+    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e / 2"
+      using i[THEN LIMSEQ_D, simplified norm_minus_commute] by meson
+    obtain B where "0 < B"
+      and B: "\<And>a b c d. \<lbrakk>ball 0 B \<subseteq> cbox a b; ball 0 B \<subseteq> cbox c d\<rbrakk> \<Longrightarrow>
+                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e / 2"
+      using rhs * by meson
let ?B = "max (real N) B"
-    show ?case
-      apply (rule_tac x="?B" in exI)
-    proof safe
+    show ?thesis
+    proof (intro exI conjI allI impI)
show "0 < ?B"
-        using B(1) by auto
+        using \<open>B > 0\<close> by auto
fix a b :: 'n
-      assume ab: "ball 0 ?B \<subseteq> cbox a b"
-      from real_arch_simple[of ?B] guess n..note n=this
-      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
-        apply (rule norm_triangle_half_l)
-        apply (rule B(2))
-        defer
-        apply (subst norm_minus_commute)
-        apply (rule N[of n])
-      proof safe
-        show "N \<le> n"
-          using n by auto
+      assume "ball 0 ?B \<subseteq> cbox a b"
+      moreover obtain n where n: "max (real N) B \<le> real n"
+        using real_arch_simple by blast
+      moreover have "ball 0 B \<subseteq> ?cube n"
+      proof
fix x :: 'n
assume x: "x \<in> ball 0 B"
-        then have "x \<in> ball 0 ?B"
-          by auto
-        then show "x \<in> cbox a b"
-          using ab by blast
-        show "x \<in> ?cube n"
-          using x
-          unfolding mem_box mem_ball dist_norm
-          apply -
-        proof (rule, goal_cases)
-          case (1 i)
-          then show ?case
-            using Basis_le_norm[of i x] \<open>i \<in> Basis\<close>
-            using n
-            by (auto simp add: field_simps sum_negf)
-        qed
-      qed
+        have "\<lbrakk>norm (0 - x) < B; i \<in> Basis\<rbrakk>
+              \<Longrightarrow> sum (op *\<^sub>R (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum (op *\<^sub>R n) Basis \<bullet> i" for i
+          using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf)
+        then show "x \<in> ?cube n"
+          using x by (auto simp: mem_box dist_norm)
+      qed
+      ultimately show "norm (integral (cbox a b) ?F - i) < e"
+        using norm_triangle_half_l [OF B N] by force
qed
qed
+  then show ?l unfolding integrable_on_def has_integral_alt'[of f]
+    using rhs by blast
qed

lemma integrable_altD:```