# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503788270 -3600
# Node ID b757c1cc8868e1a8cf9596a4d7d51dcae263748a
# Parent  5e65236e95aa42e29009520166383f2de8f3a8d4
Elimination of some "presume"

diff -r 5e65236e95aa -r b757c1cc8868 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 26 18:04:27 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Aug 26 23:57:50 2017 +0100
@@ -314,61 +314,46 @@
 lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
   by (rule forw_subst)
 
+lemma has_integral_unique_cbox:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  shows "(f has_integral k1) (cbox a b) \<Longrightarrow> (f has_integral k2) (cbox a b) \<Longrightarrow> k1 = k2"
+    by (auto simp: has_integral_cbox intro: tendsto_unique[OF division_filter_not_empty])    
+
 lemma has_integral_unique:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "(f has_integral k1) i"
-    and "(f has_integral k2) i"
+  assumes "(f has_integral k1) i" "(f has_integral k2) i"
   shows "k1 = k2"
 proof (rule ccontr)
   let ?e = "norm (k1 - k2) / 2"
-  assume as: "k1 \<noteq> k2"
+  let ?F = "(\<lambda>x. if x \<in> i then f x else 0)"
+  assume "k1 \<noteq> k2"
   then have e: "?e > 0"
     by auto
-  have lem: "(f has_integral k1) (cbox a b) \<Longrightarrow> (f has_integral k2) (cbox a b) \<Longrightarrow> k1 = k2"
-    for f :: "'n \<Rightarrow> 'a" and a b k1 k2
-    by (auto simp: has_integral_cbox intro: tendsto_unique[OF division_filter_not_empty])
-  {
-    presume "\<not> (\<exists>a b. i = cbox a b) \<Longrightarrow> False"
-    then show False
-      using as assms lem by blast
-  }
-  assume as: "\<not> (\<exists>a b. i = cbox a b)"
+  have nonbox: "\<not> (\<exists>a b. i = cbox a b)"
+    using \<open>k1 \<noteq> k2\<close> assms has_integral_unique_cbox by blast
   obtain B1 where B1:
       "0 < B1"
       "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
-        \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and>
-          norm (z - k1) < norm (k1 - k2) / 2"
-    by (rule has_integral_altD[OF assms(1) as,OF e]) blast
+        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2) / 2"
+    by (rule has_integral_altD[OF assms(1) nonbox,OF e]) blast
   obtain B2 where B2:
       "0 < B2"
       "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
-        \<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and>
-          norm (z - k2) < norm (k1 - k2) / 2"
-    by (rule has_integral_altD[OF assms(2) as,OF e]) blast
-  have "\<exists>a b::'n. ball 0 B1 \<union> ball 0 B2 \<subseteq> cbox a b"
-    apply (rule bounded_subset_cbox)
-    using bounded_Un bounded_ball
-    apply auto
-    done
-  then obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
-    by blast
-  obtain w where w:
-    "((\<lambda>x. if x \<in> i then f x else 0) has_integral w) (cbox a b)"
-    "norm (w - k1) < norm (k1 - k2) / 2"
+        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2) / 2"
+    by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
+  obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
+    by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
+  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2) / 2"
     using B1(2)[OF ab(1)] by blast
-  obtain z where z:
-    "((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b)"
-    "norm (z - k2) < norm (k1 - k2) / 2"
+  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2) / 2"
     using B2(2)[OF ab(2)] by blast
   have "z = w"
-    using lem[OF w(1) z(1)] by auto
+    using has_integral_unique_cbox[OF w(1) z(1)] by auto
   then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
     using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
     by (auto simp add: norm_minus_commute)
   also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
-    apply (rule add_strict_mono)
-    apply (rule_tac[!] z(2) w(2))
-    done
+    by (metis add_strict_mono z(2) w(2))
   finally show False by auto
 qed
 
@@ -408,29 +393,28 @@
   shows "integral {a..b} (\<lambda>x. c) = content {a..b} *\<^sub>R c"
   by (metis box_real(2) integral_const)
 
-lemma has_integral_is_0:
+lemma has_integral_is_0_cbox:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "\<forall>x\<in>s. f x = 0"
-  shows "(f has_integral 0) s"
-proof -
-  have lem: "(\<forall>x\<in>cbox a b. f x = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)" for a  b and f :: "'n \<Rightarrow> 'a"
+  assumes "\<And>x. x \<in> cbox a b \<Longrightarrow> f x = 0"
+  shows "(f has_integral 0) (cbox a b)"
     unfolding has_integral_cbox
-    using eventually_division_filter_tagged_division[of "cbox a b"]
+    using eventually_division_filter_tagged_division[of "cbox a b"] assms
     by (subst tendsto_cong[where g="\<lambda>_. 0"])
        (auto elim!: eventually_mono intro!: sum.neutral simp: tag_in_interval)
-  {
-    presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
-    with assms lem show ?thesis
-      by blast
-  }
-  have *: "(\<lambda>x. if x \<in> s then f x else 0) = (\<lambda>x. 0)"
-    apply (rule ext)
-    using assms
-    apply auto
-    done
-  assume "\<not> (\<exists>a b. s = cbox a b)"
-  then show ?thesis
-    using lem
+
+lemma has_integral_is_0:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes "\<And>x. x \<in> S \<Longrightarrow> f x = 0"
+  shows "(f has_integral 0) S"
+proof (cases "(\<exists>a b. S = cbox a b)")
+  case True with assms has_integral_is_0_cbox show ?thesis
+    by blast
+next
+  case False
+  have *: "(\<lambda>x. if x \<in> S then f x else 0) = (\<lambda>x. 0)"
+    by (auto simp add: assms)
+  show ?thesis
+    using has_integral_is_0_cbox False
     by (subst has_integral_alt) (force simp add: *)
 qed
 
@@ -440,47 +424,56 @@
 lemma has_integral_0_eq[simp]: "((\<lambda>x. 0) has_integral i) S \<longleftrightarrow> i = 0"
   using has_integral_unique[OF has_integral_0] by auto
 
+lemma has_integral_linear_cbox:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
+  assumes f: "(f has_integral y) (cbox a b)"
+    and h: "bounded_linear h"
+  shows "((h \<circ> f) has_integral (h y)) (cbox a b)"
+proof -
+  interpret bounded_linear h using h .
+  show ?thesis
+    unfolding has_integral_cbox using tendsto [OF f [unfolded has_integral_cbox]]
+    by (simp add: sum scaleR split_beta')
+qed
+
 lemma has_integral_linear:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  assumes "(f has_integral y) S"
-    and "bounded_linear h"
-  shows "((h \<circ> f) has_integral ((h y))) S"
-proof -
-  interpret bounded_linear h
-    using assms(2) .
+  assumes f: "(f has_integral y) S"
+    and h: "bounded_linear h"
+  shows "((h \<circ> f) has_integral (h y)) S"
+proof (cases "(\<exists>a b. S = cbox a b)")
+  case True with f h has_integral_linear_cbox show ?thesis 
+    by blast
+next
+  case False
+  interpret bounded_linear h using h .
   from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
     by blast
-  have lem: "\<And>a b y f::'n\<Rightarrow>'a. (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> f) has_integral h y) (cbox a b)"
-    unfolding has_integral_cbox by (drule tendsto) (simp add: sum scaleR split_beta')
-  {
-    presume "\<not> (\<exists>a b. S = cbox a b) \<Longrightarrow> ?thesis"
-    then show ?thesis
-      using assms(1) lem by blast
-  }
-  assume as: "\<not> (\<exists>a b. S = cbox a b)"
-  then show ?thesis
-  proof (subst has_integral_alt, clarsimp)
+  let ?S = "\<lambda>f x. if x \<in> S then f x else 0"
+  show ?thesis
+  proof (subst has_integral_alt, clarsimp simp: False)
     fix e :: real
     assume e: "e > 0"
     have *: "0 < e/B" using e B(1) by simp
     obtain M where M:
       "M > 0"
       "\<And>a b. ball 0 M \<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 - y) < e/B"
-      using has_integral_altD[OF assms(1) as *] by blast
+        \<exists>z. (?S f has_integral z) (cbox a b) \<and> norm (z - y) < e/B"
+      using has_integral_altD[OF f False *] by blast
     show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
-      (\<exists>z. ((\<lambda>x. if x \<in> S then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
-    proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases)
-      case prems: (1 a b)
-      obtain z where z:
-        "((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b)"
-        "norm (z - y) < e/B"
-        using M(2)[OF prems(1)] by blast
-      have *: "(\<lambda>x. if x \<in> S then (h \<circ> f) x else 0) = h \<circ> (\<lambda>x. if x \<in> S then f x else 0)"
+      (\<exists>z. (?S(h \<circ> f) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
+    proof (rule exI, intro allI conjI impI)
+      show "M > 0" using M by metis
+    next
+      fix a b::'n
+      assume sb: "ball 0 M \<subseteq> cbox a b"
+      obtain z where z: "(?S f has_integral z) (cbox a b)" "norm (z - y) < e/B"
+        using M(2)[OF sb] by blast
+      have *: "?S(h \<circ> f) = h \<circ> ?S f"
         using zero by auto
-      show ?case
+      show "\<exists>z. (?S(h \<circ> f) has_integral z) (cbox a b) \<and> norm (z - h y) < e"
         apply (rule_tac x="h z" in exI)
-        apply (simp add: * lem[OF z(1)])
+        apply (simp add: * has_integral_linear_cbox[OF z(1) h])
         apply (metis B diff le_less_trans pos_less_divide_eq z(2))
         done
     qed
@@ -571,19 +564,19 @@
     then show ?thesis
       using assms lem by force
   }
-  assume as: "\<not> (\<exists>a b. S = cbox a b)"
+  assume nonbox: "\<not> (\<exists>a b. S = cbox a b)"
   then show ?thesis
   proof (subst has_integral_alt, clarsimp, goal_cases)
     case (1 e)
     then have *: "e/2 > 0"
       by auto
-    from has_integral_altD[OF assms(1) as *]
+    from has_integral_altD[OF assms(1) nonbox *]
     obtain B1 where B1:
         "0 < B1"
         "\<And>a b. ball 0 B1 \<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 - k) < e/2"
       by blast
-    from has_integral_altD[OF assms(2) as *]
+    from has_integral_altD[OF assms(2) nonbox *]
     obtain B2 where B2:
         "0 < B2"
         "\<And>a b. ball 0 B2 \<subseteq> (cbox a b) \<Longrightarrow>
@@ -804,7 +797,7 @@
   by (simp add: has_integral_integrable)
 
 lemma has_integral_empty[intro]: "(f has_integral 0) {}"
-  by (simp add: has_integral_is_0)
+  by (meson ex_in_conv has_integral_is_0)
 
 lemma has_integral_empty_eq[simp]: "(f has_integral i) {} \<longleftrightarrow> i = 0"
   by (auto simp add: has_integral_empty has_integral_unique)
@@ -6022,7 +6015,7 @@
       using bounded_increasing_convergent [OF bou] le int_f integral_le by blast
     have i': "(integral S (f k)) \<le> i" for k
     proof -
-      have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
+      have "\<And>k. \<And>x. x \<in> S \<Longrightarrow> \<forall>n\<ge>k. f k x \<le> f n x"
         using le  by (force intro: transitive_stepwise_le)
       then show ?thesis
         using tendsto_lowerbound [OF i eventually_sequentiallyI trivial_limit_sequentially]
@@ -6199,7 +6192,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes int_f: "f integrable_on S"
     and int_g: "g integrable_on S"
-    and le_g: "\<forall>x\<in>S. norm (f x) \<le> g x"
+    and le_g: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> g x"
   shows "norm (integral S f) \<le> integral S g"
 proof -
   have norm: "norm \<eta> \<le> y + e"
@@ -6306,31 +6299,29 @@
 lemma integral_norm_bound_integral_component:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   fixes g :: "'n \<Rightarrow> 'b::euclidean_space"
-  assumes "f integrable_on s"
-    and "g integrable_on s"
-    and "\<forall>x\<in>s. norm(f x) \<le> (g x)\<bullet>k"
-  shows "norm (integral s f) \<le> (integral s g)\<bullet>k"
+  assumes f: "f integrable_on S" and g: "g integrable_on S"
+    and fg: "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> (g x)\<bullet>k"
+  shows "norm (integral S f) \<le> (integral S g)\<bullet>k"
 proof -
-  have "norm (integral s f) \<le> integral s ((\<lambda>x. x \<bullet> k) \<circ> g)"
-    apply (rule integral_norm_bound_integral[OF assms(1)])
-    apply (rule integrable_linear[OF assms(2)])
-    apply rule
+  have "norm (integral S f) \<le> integral S ((\<lambda>x. x \<bullet> k) \<circ> g)"
+    apply (rule integral_norm_bound_integral[OF f integrable_linear[OF g]])
+    apply (simp add: bounded_linear_inner_left)
     unfolding o_def
-    apply (rule assms)
+    apply (metis fg)
     done
   then show ?thesis
-    unfolding o_def integral_component_eq[OF assms(2)] .
+    unfolding o_def integral_component_eq[OF g] .
 qed
 
 lemma has_integral_norm_bound_integral_component:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   fixes g :: "'n \<Rightarrow> 'b::euclidean_space"
-  assumes "(f has_integral i) s"
-    and "(g has_integral j) s"
-    and "\<forall>x\<in>s. norm (f x) \<le> (g x)\<bullet>k"
+  assumes f: "(f has_integral i) S"
+    and g: "(g has_integral j) S"
+    and "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> (g x)\<bullet>k"
   shows "norm i \<le> j\<bullet>k"
-  using integral_norm_bound_integral_component[of f s g k]
-  unfolding integral_unique[OF assms(1)] integral_unique[OF assms(2)]
+  using integral_norm_bound_integral_component[of f S g k] 
+  unfolding integral_unique[OF f] integral_unique[OF g]
   using assms
   by auto