author paulson Sat, 28 Apr 2018 14:38:53 +0100 changeset 68053 56ff7c3e5550 parent 68052 e98988801fa9 child 68054 ebd179b82e20
getting rid of "defer"
```--- 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)"
@@ -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
-        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:```