# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524922733 -3600
# Node ID 56ff7c3e5550500d6ddf6810f95e7e2b2af011cb
# Parent  e98988801fa9d06eb734e6066dd51a3a037323e6
getting rid of "defer"

diff -r e98988801fa9 -r 56ff7c3e5550 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 27 20:59:34 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 28 14:38:53 2018 +0100
@@ -128,20 +128,13 @@
   assumes "k \<in> Basis"
   shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
   \<comment> \<open>Prove using measure theory\<close>
-proof cases
+proof (cases "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i")
+  case True
+  have 1: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
+    by (simp add: if_distrib prod.delta_remove assms)
   note simps = interval_split[OF assms] content_cbox_cases
-  have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
-    using assms by auto
-  have *: "\<And>X Y Z. (\<Prod>i\<in>Basis. Z i (if i = k then X else Y i)) = Z k X * (\<Prod>i\<in>Basis-{k}. Z i (Y i))"
-    "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
-    apply (subst *(1))
-    defer
-    apply (subst *(1))
-    unfolding prod.insert[OF *(2-)]
-    apply auto
-    done
-  assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-  moreover
+  have 2: "(\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i) = (\<Prod>i\<in>Basis-{k}. b\<bullet>i - a\<bullet>i) * (b\<bullet>k - a\<bullet>k)"
+    by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove)
   have "\<And>x. min (b \<bullet> k) c = max (a \<bullet> k) c \<Longrightarrow>
     x * (b\<bullet>k - a\<bullet>k) = x * (max (a \<bullet> k) c - a \<bullet> k) + x * (b \<bullet> k - max (a \<bullet> k) c)"
     by  (auto simp add: field_simps)
@@ -152,17 +145,12 @@
       (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
     by (auto intro!: prod.cong)
   have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
-    unfolding not_le
-    using as[unfolded ,rule_format,of k] assms
-    by auto
+    unfolding not_le using True assms by auto
   ultimately show ?thesis
-    using assms
-    unfolding simps **
-    unfolding *(1)[of "\<lambda>i x. b\<bullet>i - x"] *(1)[of "\<lambda>i x. x - a\<bullet>i"]
-    unfolding *(2)
+    using assms unfolding simps ** 1[of "\<lambda>i x. b\<bullet>i - x"] 1[of "\<lambda>i x. x - a\<bullet>i"] 2
     by auto
 next
-  assume "\<not> (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
+  case False
   then have "cbox a b = {}"
     unfolding box_eq_empty by (auto simp: not_le)
   then show ?thesis
@@ -2585,24 +2573,22 @@
       norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - i) \<le> e * content (cbox a b)))"
 proof (cases "content (cbox a b) = 0")
   case True
-  show ?thesis
+  have "\<And>e p. p tagged_division_of cbox a b \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) \<le> e * content (cbox a b)"
+    unfolding sum_content_null[OF True] True by force
+  moreover have "i = 0" 
+    if "\<And>e. e > 0 \<Longrightarrow> \<exists>d. gauge d \<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 f x) - i) \<le> e * content (cbox a b))"
+    using that [of 1]
+    by (force simp add: True sum_content_null[OF True] intro: fine_division_exists[of _ a b])
+  ultimately show ?thesis
     unfolding has_integral_null_eq[OF True]
-    apply safe
-    apply (rule, rule, rule gauge_trivial, safe)
-    unfolding sum_content_null[OF True] True
-    defer
-    apply (erule_tac x=1 in allE)
-    apply safe
-    defer
-    apply (rule fine_division_exists[of _ a b])
-    apply assumption
-    apply (erule_tac x=p in allE)
-    unfolding sum_content_null[OF True]
-    apply auto
-    done
+    by (force simp add: )
 next
   case False
-  note F = this[unfolded content_lt_nz[symmetric]]
+  then have F: "0 < content (cbox a b)"
+    using zero_less_measure_iff by blast
   let ?P = "\<lambda>e opp. \<exists>d. gauge d \<and>
     (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> opp (norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i)) e)"
   show ?thesis
@@ -2610,28 +2596,18 @@
   proof safe
     fix e :: real
     assume e: "e > 0"
-    {
-      assume "\<forall>e>0. ?P e (<)"
+    { assume "\<forall>e>0. ?P e (<)"
       then show "?P (e * content (cbox a b)) (\<le>)"
-        apply (erule_tac x="e * content (cbox a b)" in allE)
-        apply (erule impE)
-        defer
-        apply (erule exE,rule_tac x=d in exI)
-        using F e
-        apply (auto simp add:field_simps)
-        done
-    }
-    {
-      assume "\<forall>e>0. ?P (e * content (cbox a b)) (\<le>)"
+        apply (rule allE [where x="e * content (cbox a b)"])
+        apply (elim impE ex_forward conj_forward)
+        using F e apply (auto simp add: algebra_simps)
+        done }
+    { assume "\<forall>e>0. ?P (e * content (cbox a b)) (\<le>)"
       then show "?P e (<)"
-        apply (erule_tac x="e/2 / content (cbox a b)" in allE)
-        apply (erule impE)
-        defer
-        apply (erule exE,rule_tac x=d in exI)
-        using F e
-        apply (auto simp add: field_simps)
-        done
-    }
+        apply (rule allE [where x="e/2 / content (cbox a b)"])
+        apply (elim impE ex_forward conj_forward)
+        using F e apply (auto simp add: algebra_simps)
+        done }
   qed
 qed
 
@@ -2995,19 +2971,22 @@
 
 lemma integrable_subinterval:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on cbox a b"
-    and "cbox c d \<subseteq> cbox a b"
+  assumes f: "f integrable_on cbox a b"
+    and cd: "cbox c d \<subseteq> cbox a b"
   shows "f integrable_on cbox c d"
 proof -
   interpret operative conj True "\<lambda>i. f integrable_on i"
     using order_refl by (rule operative_integrableI)
   show ?thesis
-    apply (cases "cbox c d = {}")
-     defer
-     apply (rule partial_division_extend_1[OF assms(2)],assumption)
-    using division [symmetric] assms(1)
-     apply (auto simp: comm_monoid_set_F_and)
-    done
+  proof (cases "cbox c d = {}")
+    case True
+    then show ?thesis
+      using division [symmetric] f by (auto simp: comm_monoid_set_F_and)
+  next
+    case False
+    then show ?thesis
+      by (metis cd comm_monoid_set_F_and division division_of_finite f partial_division_extend_1)
+  qed
 qed
 
 lemma integrable_subinterval_real:
@@ -4261,31 +4240,29 @@
 lemma has_derivative_zero_unique_strong_interval:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "finite k"
-    and "continuous_on {a..b} f"
+    and contf: "continuous_on {a..b} f"
     and "f a = y"
-    and "\<forall>x\<in>({a..b} - k). (f has_derivative (\<lambda>h. 0)) (at x within {a..b})" "x \<in> {a..b}"
+    and fder: "\<And>x. x \<in> {a..b} - k \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within {a..b})"
+    and x: "x \<in> {a..b}"
   shows "f x = y"
 proof -
-  have ab: "a \<le> b"
+  have "a \<le> b" "a \<le> x"
     using assms by auto
-  have *: "a \<le> x"
-    using assms(5) by auto
   have "((\<lambda>x. 0::'a) has_integral f x - f a) {a..x}"
-    apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1) *])
-    apply (rule continuous_on_subset[OF assms(2)])
-    defer
-    apply safe
-    unfolding has_vector_derivative_def
-    apply (subst has_derivative_within_open[symmetric])
-    apply assumption
-    apply (rule open_greaterThanLessThan)
-    apply (rule has_derivative_within_subset[where s="{a..b}"])
-    using assms(4) assms(5)
-    apply (auto simp: mem_box)
-    done
-  note this[unfolded *]
-  note has_integral_unique[OF has_integral_0 this]
-  then show ?thesis
+  proof (rule fundamental_theorem_of_calculus_interior_strong[OF \<open>finite k\<close> \<open>a \<le> x\<close>]; clarify?)
+    have "{a..x} \<subseteq> {a..b}"
+      using x by auto
+    then show "continuous_on {a..x} f"
+      by (rule continuous_on_subset[OF contf])
+    show "(f has_vector_derivative 0) (at z)" if z: "z \<in> {a<..<x}" and notin: "z \<notin> k" for z
+      unfolding has_vector_derivative_def
+    proof (simp add: has_derivative_within_open[OF z, symmetric])
+      show "(f has_derivative (\<lambda>x. 0)) (at z within {a<..<x})"
+        by (rule has_derivative_within_subset [OF fder]) (use x z notin in auto)
+    qed
+  qed
+  from has_integral_unique[OF has_integral_0 this]
+  show ?thesis
     unfolding assms by auto
 qed
 
@@ -4297,7 +4274,7 @@
   assumes "convex S" "finite K"
     and contf: "continuous_on S f"
     and "c \<in> S" "f c = y"
-    and derf: "\<And>x. x \<in> (S - K) \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within S)"
+    and derf: "\<And>x. x \<in> S - K \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within S)"
     and "x \<in> S"
   shows "f x = y"
 proof (cases "x = c")
@@ -4307,8 +4284,10 @@
   case False
   let ?\<phi> = "\<lambda>u. (1 - u) *\<^sub>R c + u *\<^sub>R x"
   have contf': "continuous_on {0 ..1} (f \<circ> ?\<phi>)"
-    apply (rule continuous_intros continuous_on_subset[OF contf])+
-    using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> by (auto simp add: convex_alt algebra_simps)
+  proof (rule continuous_intros continuous_on_subset[OF contf])+
+    show "(\<lambda>u. (1 - u) *\<^sub>R c + u *\<^sub>R x) ` {0..1} \<subseteq> S"
+      using \<open>convex S\<close> \<open>x \<in> S\<close> \<open>c \<in> S\<close> by (auto simp add: convex_alt algebra_simps)
+  qed
   have "t = u" if "?\<phi> t = ?\<phi> u" for t u
   proof -
     from that have "(t - u) *\<^sub>R x = (t - u) *\<^sub>R c"
@@ -4353,7 +4332,7 @@
     and contf: "continuous_on S f"
     and "c \<in> S"
     and "f c = y"
-    and derf: "\<And>x. x \<in> (S - K) \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within S)"
+    and derf: "\<And>x. x \<in> S - K \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within S)"
     and "x \<in> S"
   shows "f x = y"
 proof -
@@ -4486,10 +4465,7 @@
   note has_integral_restrict_open_subinterval[OF assms]
   note * = has_integral_spike[OF negligible_frontier_interval _ this]
   show ?thesis
-    apply (rule *[of c d])
-    using box_subset_cbox[of c d]
-    apply auto
-    done
+    by (rule *[of c d]) (use box_subset_cbox[of c d] in auto)
 qed
 
 lemma has_integral_restrict_closed_subintervals_eq: