# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1502664345 -3600
# Node ID f749d39c016ba9bc48e54b7e5537441fb97a7244
# Parent  46cfd348c373bd868fa666bb2ed182eaf2d29246
further tidying

diff -r 46cfd348c373 -r f749d39c016b src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 13 19:24:33 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 13 23:45:45 2017 +0100
@@ -6027,17 +6027,14 @@
 
 lemma monotone_convergence_interval:
   fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
-  assumes "\<forall>k. (f k) integrable_on cbox a b"
-    and "\<forall>k. \<forall>x\<in>cbox a b.(f k x) \<le> f (Suc k) x"
-    and "\<forall>x\<in>cbox a b. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+  assumes "\<And>k. (f k) integrable_on cbox a b"
+    and "\<And>k x. x \<in> cbox a b \<Longrightarrow> (f k x) \<le> f (Suc k) x"
+    and "\<And>x. x \<in> cbox a b \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
     and bounded: "bounded (range (\<lambda>k. integral (cbox a b) (f k)))"
   shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> integral (cbox a b) g) sequentially"
 proof (cases "content (cbox a b) = 0")
   case True
-  show ?thesis
-    using integrable_on_null[OF True]
-    unfolding integral_null[OF True]
-    using tendsto_const
+  then show ?thesis
     by auto
 next
   case False
@@ -6111,14 +6108,9 @@
     qed
     from bchoice[OF this] guess m..note m=conjunctD2[OF this[rule_format],rule_format]
     define d where "d x = c (m x) x" for x
-    show "\<exists>d. gauge d \<and>
+    show "\<exists>\<gamma>. gauge \<gamma> \<and>
              (\<forall>p. p tagged_division_of cbox a b \<and>
-                  d fine p \<longrightarrow>
-                  norm
-                   ((\<Sum>(x, k)\<in>p.
-                       content k *\<^sub>R g x) -
-                    i)
-                  < e)"
+                  \<gamma> fine p \<longrightarrow> norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R g x) - i) < e)"
       apply (rule_tac x=d in exI)
     proof safe
       show "gauge d"
@@ -6288,107 +6280,61 @@
   shows "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
 proof -
   have lem: "g integrable_on S \<and> ((\<lambda>k. integral S (f k)) \<longlongrightarrow> integral S g) sequentially"
-    if "\<forall>k. \<forall>x\<in>S. 0 \<le> f k x"
-    and "\<forall>k. (f k) integrable_on S"
-    and "\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x"
-    and "\<forall>x\<in>S. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
+    if f0: "\<And>k x. x \<in> S \<Longrightarrow> 0 \<le> f k x"
+    and int_f: "\<And>k. (f k) integrable_on S"
+    and le: "\<And>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x"
+    and lim: "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
     and bou: "bounded (range(\<lambda>k. integral S (f k)))"
     for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
   proof -
-    note assms=that[rule_format]
-    have "\<forall>x\<in>S. \<forall>k. (f k x)\<bullet>1 \<le> (g x)\<bullet>1"
-      apply safe
-      apply (rule Lim_component_ge)
-      apply (rule that(4)[rule_format])
-      apply assumption
-      apply (rule trivial_limit_sequentially)
+    have fg: "(f k x)\<bullet>1 \<le> (g x)\<bullet>1" if "x \<in> S" for x k
+      apply (rule Lim_component_ge [OF lim [OF that] trivial_limit_sequentially])
       unfolding eventually_sequentially
       apply (rule_tac x=k in exI)
-      using assms(3) by (force intro: transitive_stepwise_le)
-    note fg=this[rule_format]
+      using le  by (force intro: transitive_stepwise_le that) 
 
     obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
       using bounded_increasing_convergent [OF bou]
-      using \<open>\<forall>k. \<forall>x\<in>S. f k x \<le> f (Suc k) x\<close> assms(2) integral_le by blast
-    have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
-      using assms(3) by (force intro: transitive_stepwise_le)
-    then have i': "\<forall>k. (integral S (f k))\<bullet>1 \<le> i\<bullet>1"
-      apply -
-      apply rule
-      apply (rule Lim_component_ge)
-      apply (rule i)
-      apply (rule trivial_limit_sequentially)
-      unfolding eventually_sequentially
-      apply (rule_tac x=k in exI)
-      apply safe
-      apply (rule integral_component_le)
-      apply simp
-      apply (rule that(2)[rule_format])+
-      apply auto
-      done
-
-    note int = assms(2)[unfolded integrable_alt[of _ S],THEN conjunct1,rule_format]
-    have ifif: "\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> S then f k x else 0 else 0) =
-      (\<lambda>x. if x \<in> t \<inter> S then f k x else 0)"
-      by (rule ext) auto
+      using le int_f integral_le by blast
+    have i': "(integral S (f k))\<bullet>1 \<le> i\<bullet>1" for k
+    proof -
+      have *: "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
+        using le  by (force intro: transitive_stepwise_le)
+      show ?thesis
+        apply (rule Lim_component_ge [OF i trivial_limit_sequentially])
+        unfolding eventually_sequentially
+        apply (rule_tac x=k in exI)
+        using * by (simp add: int_f integral_le)
+    qed
+
+    have int: "(\<lambda>x. if x \<in> S then f k x else 0) integrable_on cbox a b" for a b k
+      by (simp add: int_f integrable_altD(1))
     have int': "\<And>k a b. f k integrable_on cbox a b \<inter> S"
-      apply (subst integrable_restrict_UNIV[symmetric])
-      apply (subst ifif[symmetric])
-      apply (subst integrable_restrict_UNIV)
-      apply (rule int)
-      done
-    have "\<And>a b. (\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b \<and>
-      ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<longlongrightarrow>
-      integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0)) sequentially"
-    proof (rule monotone_convergence_interval, safe, goal_cases)
+      using int by (simp add: Int_commute integrable_restrict_Int) 
+    have "(\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b \<and>
+          (\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0))
+          \<longlonglongrightarrow> integral (cbox a b) (\<lambda>x. if x \<in> S then g x else 0)" for a b
+    proof (rule monotone_convergence_interval, goal_cases)
       case 1
       show ?case by (rule int)
     next
-      case (2 _ _ _ x)
-      then show ?case
-        apply (cases "x \<in> S")
-        using assms(3)
-        apply auto
-        done
-    next
-      case (3 _ _ x)
-      then show ?case
-        apply (cases "x \<in> S")
-        using assms(4)
-        apply auto
-        done
-    next
-      case (4 a b)
-      note * = integral_nonneg
-      have "\<And>k. norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<le> norm (integral S (f k))"
-        unfolding real_norm_def
-        apply (subst abs_of_nonneg)
-        apply (rule *[OF int])
-        apply safe
-        apply (case_tac "x \<in> S")
-        apply (drule assms(1))
-        prefer 3
-        apply (subst abs_of_nonneg)
-        apply (rule *[OF assms(2) that(1)[THEN spec]])
-        apply (subst integral_restrict_UNIV[symmetric,OF int])
-        unfolding ifif
-        unfolding integral_restrict_UNIV[OF int']
-        apply (rule integral_subset_le[OF _ int' assms(2)])
-        using assms(1)
-        apply auto
-        done
-      then show ?case
-        using assms(5)
-        unfolding bounded_iff
-        apply safe
-        apply (rule_tac x=aa in exI)
-        apply safe
-        apply (erule_tac x="integral S (f k)" in ballE)
-        apply (rule order_trans)
-        apply assumption
-        apply auto
-        done
-    qed
+      case 4
+      have "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)) \<le> norm (integral S (f k))" for k
+      proof -
+        have "0 \<le> integral (cbox a b) (\<lambda>x. if x \<in> S then f k x else 0)"
+          by (metis (no_types) integral_nonneg Int_iff f0 inf_commute integral_restrict_Int int')
+        moreover have "0 \<le> integral S (f k)"
+          by (simp add: integral_nonneg f0 int_f)
+        moreover have "integral (S \<inter> cbox a b) (f k) \<le> integral S (f k)"
+          by (metis f0 inf_commute int' int_f integral_subset_le le_inf_iff order_refl)
+        ultimately show ?thesis
+          by (simp add: integral_restrict_Int)
+      qed
+      moreover obtain B where "\<And>x. x \<in> range (\<lambda>k. integral S (f k)) \<Longrightarrow> norm x \<le> B"
+        using bou unfolding bounded_iff by blast
+      ultimately show ?case
+        unfolding bounded_iff by (blast intro: order_trans)
+    qed (use le lim in auto)
     note g = conjunctD2[OF this]
 
     have "(g has_integral i) S"
@@ -6400,7 +6346,7 @@
       then have "e/4>0"
         by auto
       from LIMSEQ_D [OF i this] guess N..note N=this
-      note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]]
+      note that(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]]
       from this[THEN conjunct2,rule_format,OF \<open>e/4>0\<close>] guess B..note B=conjunctD2[OF this]
       show ?case
         apply rule
@@ -6414,13 +6360,13 @@
           by auto
         from LIMSEQ_D [OF g(2)[of a b] this] guess M..note M=this
         have **: "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - i) < e/2"
-          apply (rule norm_triangle_half_l)
-          using B(2)[rule_format,OF ab] N[rule_format,of N]
-          apply -
-          defer
-          apply (subst norm_minus_commute)
-          apply auto
-          done
+        proof (rule norm_triangle_half_l)
+          show "norm (integral (cbox a b) (\<lambda>x. if x \<in> S then f N x else 0) - integral S (f N))
+                < e / 2 / 2"
+            using B(2)[rule_format,OF ab] by simp
+          show "norm (i - integral S (f N)) < e / 2 / 2"
+            using N by (simp add: abs_minus_commute)
+        qed
         have *: "\<And>f1 f2 g. \<bar>f1 - i\<bar> < e/2 \<longrightarrow> \<bar>f2 - g\<bar> < e/2 \<longrightarrow>
           f1 \<le> f2 \<longrightarrow> f2 \<le> i \<longrightarrow> \<bar>g - i\<bar> < e"
           unfolding real_inner_1_right by arith
@@ -6432,42 +6378,32 @@
           apply (rule le_add1)
           apply (rule integral_le[OF int int])
           defer
-          apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
+           apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
         proof (safe, goal_cases)
           case (2 x)
-          have "\<And>m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
-            using assms(3) by (force intro: transitive_stepwise_le)
+          have "(f m x)\<bullet>1 \<le> (f n x)\<bullet>1" if "x \<in> S" "n \<ge> m" for m n
+            apply (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
+            using dual_order.trans apply blast
+            by (simp add: le \<open>x \<in> S\<close>)
           then show ?case
             by auto
         next
           case 1
-          show ?case
-            apply (subst integral_restrict_UNIV[symmetric,OF int])
-            unfolding ifif integral_restrict_UNIV[OF int']
-            apply (rule integral_subset_le[OF _ int'])
-            using assms
-            apply auto
-            done
+          have "integral (cbox a b \<inter> S) (f (M + N)) \<le> integral S (f (M + N))"
+            by (metis Int_lower1 f0 inf_commute int' int_f integral_subset_le)
+          then show ?case
+            by (simp add: inf_commute integral_restrict_Int)
         qed
       qed
     qed
     then show ?thesis
-      apply safe
-      defer
-      apply (drule integral_unique)
-      using i
-      apply auto
-      done
+      using has_integral_integrable_integral i integral_unique by metis
   qed
 
   have sub: "\<And>k. integral S (\<lambda>x. f k x - f 0 x) = integral S (f k) - integral S (f 0)"
-    apply (subst integral_diff)
-    apply (rule assms(1)[rule_format])+
-    apply rule
-    done
-  have "\<And>x m. x \<in> S \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x"
+    by (simp add: integral_diff assms(1))
+  have *: "\<And>x m n. x \<in> S \<Longrightarrow> n\<ge>m \<Longrightarrow> f m x \<le> f n x"
     using assms(2) by (force intro: transitive_stepwise_le)
-  note * = this[rule_format]
   have "(\<lambda>x. g x - f 0 x) integrable_on S \<and> ((\<lambda>k. integral S (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
     integral S (\<lambda>x. g x - f 0 x)) sequentially"
     apply (rule lem)
@@ -6479,10 +6415,7 @@
   next
     case (2 k)
     then show ?case
-      apply (rule integrable_diff)
-      using assms(1)
-      apply auto
-      done
+      by (simp add: integrable_diff assms(1))
   next
     case (3 k x)
     then show ?case
@@ -6513,16 +6446,7 @@
   note tendsto_add[OF this(2) tendsto_const[of "integral S (f 0)"]]
     integrable_add[OF this(1) assms(1)[rule_format,of 0]]
   then show ?thesis
-    unfolding sub
-    apply -
-    apply rule
-     apply simp
-    apply (subst(asm) integral_diff)
-    using assms(1)
-      apply auto
-    apply (rule LIMSEQ_imp_Suc)
-    apply assumption
-    done
+    by (simp add: integral_diff assms(1) LIMSEQ_imp_Suc sub)
 qed
 
 lemma has_integral_monotone_convergence_increasing:
@@ -7762,21 +7686,17 @@
   fixes a :: "'a::ordered_euclidean_space"
   assumes "a \<le> b"
   shows "content {a..b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-  using content_cbox[of a b] assms
-  by (simp add: cbox_interval eucl_le[where 'a='a])
+  using content_cbox[of a b] assms by (simp add: cbox_interval eucl_le[where 'a='a])
 
 lemma integrable_const_ivl[intro]:
   fixes a::"'a::ordered_euclidean_space"
   shows "(\<lambda>x. c) integrable_on {a..b}"
-  unfolding cbox_interval[symmetric]
-  by (rule integrable_const)
+  unfolding cbox_interval[symmetric] by (rule integrable_const)
 
 lemma integrable_on_subinterval:
   fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s"
-    and "{a..b} \<subseteq> s"
+  assumes "f integrable_on s" "{a..b} \<subseteq> s"
   shows "f integrable_on {a..b}"
-  using integrable_on_subcbox[of f s a b] assms
-  by (simp add: cbox_interval)
+  using integrable_on_subcbox[of f s a b] assms by (simp add: cbox_interval)
 
 end