# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503607273 -3600
# Node ID 04b3a4548323595d857b8249e70b1a734f4ffeba
# Parent  7685861f337d7298c35048288bd497ebd147792a
tidying up has_integral'

diff -r 7685861f337d -r 04b3a4548323 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 17:15:53 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 21:41:13 2017 +0100
@@ -11,8 +11,8 @@
 
 (*FIXME DELETE*)
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
-
 (* try instead structured proofs below *)
+
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
   \<Longrightarrow> norm(y-x) \<le> e"
   using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
@@ -4627,142 +4627,88 @@
 
 lemma has_integral':
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  shows "(f has_integral i) s \<longleftrightarrow>
+  shows "(f has_integral i) S \<longleftrightarrow>
     (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
-      (\<exists>z. ((\<lambda>x. if x \<in> s then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - i) < e))"
+      (\<exists>z. ((\<lambda>x. if x \<in> S then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - i) < e))"
   (is "?l \<longleftrightarrow> (\<forall>e>0. ?r e)")
-proof -
-  {
-    presume *: "\<exists>a b. s = cbox a b \<Longrightarrow> ?thesis"
-    show ?thesis
-      apply cases
-      apply (rule *)
-      apply assumption
-      apply (subst has_integral_alt)
-      apply auto
-      done
-  }
-  assume "\<exists>a b. s = cbox a b"
-  then obtain a b where s: "s = cbox a b"
-    by blast
-  from bounded_cbox[of a b, unfolded bounded_pos] 
+proof (cases "\<exists>a b. S = cbox a b")
+  case False then show ?thesis 
+    by (simp add: has_integral_alt)
+next
+  case True
+  then obtain a b where S: "S = cbox a b"
+    by blast 
   obtain B where " 0 < B" and B: "\<And>x. x \<in> cbox a b \<Longrightarrow> norm x \<le> B"
-    by blast
+    using bounded_cbox[unfolded bounded_pos] by blast
   show ?thesis
   proof safe
     fix e :: real
     assume ?l and "e > 0"
-    show "?r e"
+    have "((\<lambda>x. if x \<in> S then f x else 0) has_integral i) (cbox c d)"
+      if "ball 0 (B+1) \<subseteq> cbox c d" for c d
+        unfolding S using B that
+        by (force intro: \<open>?l\<close>[unfolded S] has_integral_restrict_closed_subinterval)
+    then show "?r e"
       apply (rule_tac x="B+1" in exI)
-      apply safe
-      defer
-      apply (rule_tac x=i in exI)
-    proof
-      fix c d :: 'n
-      assume as: "ball 0 (B+1) \<subseteq> cbox c d"
-      then show "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) (cbox c d)"
-        unfolding s
-        apply -
-        apply (rule has_integral_restrict_closed_subinterval)
-        apply (rule \<open>?l\<close>[unfolded s])
-        apply safe
-        apply (drule B[rule_format])
-        unfolding subset_eq
-        apply (erule_tac x=x in ballE)
-        apply (auto simp add: dist_norm)
-        done
-    qed (insert \<open>B>0\<close> \<open>e>0\<close>, auto)
+      using \<open>B>0\<close> \<open>e>0\<close> by force
   next
     assume as: "\<forall>e>0. ?r e"
-    from this[rule_format,OF zero_less_one] guess C..note C=conjunctD2[OF this,rule_format]
+    then obtain C 
+      where C: "\<And>a b. ball 0 C \<subseteq> cbox a b \<Longrightarrow>
+                \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b)"
+      by (meson zero_less_one)
     define c :: 'n where "c = (\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)"
     define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
-    have c_d: "cbox a b \<subseteq> cbox c d"
-      apply safe
-      apply (drule B)
-      unfolding mem_box
-    proof
-      fix x i
-      show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" and "i \<in> Basis"
-        using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
-        unfolding c_def d_def
-        by (auto simp add: field_simps sum_negf)
-    qed
-    have "ball 0 C \<subseteq> cbox c d"
-      apply (rule subsetI)
-      unfolding mem_box mem_ball dist_norm
-    proof
-      fix x i :: 'n
-      assume x: "norm (0 - x) < C" and i: "i \<in> Basis"
-      show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
-        using Basis_le_norm[OF i, of x] and x i
-        unfolding c_def d_def
-        by (auto simp: sum_negf)
-    qed
-    from C(2)[OF this] have "\<exists>y. (f has_integral y) (cbox a b)"
-      unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,symmetric]
-      unfolding s
-      by auto
-    then guess y..note y=this
-
+    have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm x \<le> B" "i \<in> Basis" for x i
+      using that and Basis_le_norm[OF \<open>i\<in>Basis\<close>, of x]
+      by (auto simp add: field_simps sum_negf c_def d_def)
+    then have c_d: "cbox a b \<subseteq> cbox c d"
+      by (meson B mem_box(2) subsetI)
+    have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
+      if x: "norm (0 - x) < C" and i: "i \<in> Basis" for x i
+        using Basis_le_norm[OF i, of x] x i by (auto simp: sum_negf c_def d_def)
+      then have "ball 0 C \<subseteq> cbox c d"
+        by (auto simp: mem_box dist_norm)
+    with C obtain y where y: "(f has_integral y) (cbox a b)"
+      using c_d has_integral_restrict_closed_subintervals_eq S by blast
     have "y = i"
     proof (rule ccontr)
-      assume "\<not> ?thesis"
+      assume "y \<noteq> i"
       then have "0 < norm (y - i)"
         by auto
-      from as[rule_format,OF this] guess C ..  note C=conjunctD2[OF this,rule_format]
+      from as[rule_format,OF this]
+      obtain C where C: "\<And>a b. ball 0 C \<subseteq> cbox a b \<Longrightarrow> 
+           \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and> norm (z-i) < norm (y-i)"
+        by auto
       define c :: 'n where "c = (\<Sum>i\<in>Basis. (- max B C) *\<^sub>R i)"
       define d :: 'n where "d = (\<Sum>i\<in>Basis. max B C *\<^sub>R i)"
-      have c_d: "cbox a b \<subseteq> cbox c d"
-        apply safe
-        apply (drule B)
-        unfolding mem_box
-      proof
-        fix x i :: 'n
-        assume "norm x \<le> B" and "i \<in> Basis"
-        then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
-          using Basis_le_norm[of i x]
-          unfolding c_def d_def
-          by (auto simp add: field_simps sum_negf)
-      qed
-      have "ball 0 C \<subseteq> cbox c d"
-        apply (rule subsetI)
-        unfolding mem_box mem_ball dist_norm
-      proof
-        fix x i :: 'n
-        assume "norm (0 - x) < C" and "i \<in> Basis"
-        then show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
-          using Basis_le_norm[of i x]
-          unfolding c_def d_def
-          by (auto simp: sum_negf)
-      qed
-      note C(2)[OF this] then guess z..note z = conjunctD2[OF this, unfolded s]
-      note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]]
-      then have "z = y" and "norm (z - i) < norm (y - i)"
-        apply -
-        apply (rule has_integral_unique[OF _ y(1)])
-        apply assumption
-        apply assumption
-        done
-      then show False
+      have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
+        if "norm x \<le> B" and "i \<in> Basis" for x i
+          using that Basis_le_norm[of i x] by (auto simp add: field_simps sum_negf c_def d_def)
+        then have c_d: "cbox a b \<subseteq> cbox c d"
+        by (simp add: B mem_box(2) subset_eq)
+      have "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i" if "norm (0 - x) < C" and "i \<in> Basis" for x i
+        using Basis_le_norm[of i x] that by (auto simp: sum_negf c_def d_def)
+      then have "ball 0 C \<subseteq> cbox c d"
+        by (auto simp: mem_box dist_norm)
+      with C obtain z where z: "(f has_integral z) (cbox a b)" "norm (z-i) < norm (y-i)"
+        using has_integral_restrict_closed_subintervals_eq[OF c_d] S by blast
+      moreover then have "z = y" 
+        by (blast intro: has_integral_unique[OF _ y])
+      ultimately show False
         by auto
     qed
     then show ?l
-      using y
-      unfolding s
-      by auto
+      using y by (auto simp: S)
   qed
 qed
 
 lemma has_integral_le:
   fixes f :: "'n::euclidean_space \<Rightarrow> real"
-  assumes "(f has_integral i) S"
-    and "(g has_integral j) S"
-    and "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
+  assumes fg: "(f has_integral i) S" "(g has_integral j) S"
+    and le: "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
   shows "i \<le> j"
-  using has_integral_component_le[OF _ assms(1-2), of 1]
-  using assms(3)
-  by auto
+  using has_integral_component_le[OF _ fg, of 1] le  by auto
 
 lemma integral_le:
   fixes f :: "'n::euclidean_space \<Rightarrow> real"