# HG changeset patch # User paulson # 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 \ Basis" shows "content (cbox a b) = content(cbox a b \ {x. x\k \ c}) + content(cbox a b \ {x. x\k \ c})" \ \Prove using measure theory\ -proof cases +proof (cases "\i\Basis. a \ i \ b \ i") + case True + have 1: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\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})" "\x. finite (Basis-{x})" "\x. x\Basis-{x}" - using assms by auto - have *: "\X Y Z. (\i\Basis. Z i (if i = k then X else Y i)) = Z k X * (\i\Basis-{k}. Z i (Y i))" - "(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)" - apply (subst *(1)) - defer - apply (subst *(1)) - unfolding prod.insert[OF *(2-)] - apply auto - done - assume as: "\i\Basis. a \ i \ b \ i" - moreover + have 2: "(\i\Basis. b\i - a\i) = (\i\Basis-{k}. b\i - a\i) * (b\k - a\k)" + by (metis (no_types, lifting) assms finite_Basis mult.commute prod.remove) have "\x. min (b \ k) c = max (a \ k) c \ x * (b\k - a\k) = x * (max (a \ k) c - a \ k) + x * (b \ k - max (a \ k) c)" by (auto simp add: field_simps) @@ -152,17 +145,12 @@ (\i\Basis. b \ i - (if i = k then max (a \ k) c else a \ i))" by (auto intro!: prod.cong) have "\ a \ k \ c \ \ c \ b \ k \ 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 "\i x. b\i - x"] *(1)[of "\i x. x - a\i"] - unfolding *(2) + using assms unfolding simps ** 1[of "\i x. b\i - x"] 1[of "\i x. x - a\i"] 2 by auto next - assume "\ (\i\Basis. a \ i \ b \ 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 (\(x,k). content k *\<^sub>R f x) p - i) \ e * content (cbox a b)))" proof (cases "content (cbox a b) = 0") case True - show ?thesis + have "\e p. p tagged_division_of cbox a b \ norm ((\(x, k)\p. content k *\<^sub>R f x)) \ e * content (cbox a b)" + unfolding sum_content_null[OF True] True by force + moreover have "i = 0" + if "\e. e > 0 \ \d. gauge d \ + (\p. p tagged_division_of cbox a b \ + d fine p \ + norm ((\(x, k)\p. content k *\<^sub>R f x) - i) \ 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 = "\e opp. \d. gauge d \ (\p. p tagged_division_of (cbox a b) \ d fine p \ opp (norm ((\(x, k)\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 "\e>0. ?P e (<)" + { assume "\e>0. ?P e (<)" then show "?P (e * content (cbox a b)) (\)" - 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 "\e>0. ?P (e * content (cbox a b)) (\)" + 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 "\e>0. ?P (e * content (cbox a b)) (\)" 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 \ 'a::banach" - assumes "f integrable_on cbox a b" - and "cbox c d \ cbox a b" + assumes f: "f integrable_on cbox a b" + and cd: "cbox c d \ cbox a b" shows "f integrable_on cbox c d" proof - interpret operative conj True "\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 \ 'a::banach" assumes "finite k" - and "continuous_on {a..b} f" + and contf: "continuous_on {a..b} f" and "f a = y" - and "\x\({a..b} - k). (f has_derivative (\h. 0)) (at x within {a..b})" "x \ {a..b}" + and fder: "\x. x \ {a..b} - k \ (f has_derivative (\h. 0)) (at x within {a..b})" + and x: "x \ {a..b}" shows "f x = y" proof - - have ab: "a \ b" + have "a \ b" "a \ x" using assms by auto - have *: "a \ x" - using assms(5) by auto have "((\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 \finite k\ \a \ x\]; clarify?) + have "{a..x} \ {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 \ {a<.. k" for z + unfolding has_vector_derivative_def + proof (simp add: has_derivative_within_open[OF z, symmetric]) + show "(f has_derivative (\x. 0)) (at z within {a<.. S" "f c = y" - and derf: "\x. x \ (S - K) \ (f has_derivative (\h. 0)) (at x within S)" + and derf: "\x. x \ S - K \ (f has_derivative (\h. 0)) (at x within S)" and "x \ S" shows "f x = y" proof (cases "x = c") @@ -4307,8 +4284,10 @@ case False let ?\ = "\u. (1 - u) *\<^sub>R c + u *\<^sub>R x" have contf': "continuous_on {0 ..1} (f \ ?\)" - apply (rule continuous_intros continuous_on_subset[OF contf])+ - using \convex S\ \x \ S\ \c \ S\ by (auto simp add: convex_alt algebra_simps) + proof (rule continuous_intros continuous_on_subset[OF contf])+ + show "(\u. (1 - u) *\<^sub>R c + u *\<^sub>R x) ` {0..1} \ S" + using \convex S\ \x \ S\ \c \ S\ by (auto simp add: convex_alt algebra_simps) + qed have "t = u" if "?\ t = ?\ 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 \ S" and "f c = y" - and derf: "\x. x \ (S - K) \ (f has_derivative (\h. 0)) (at x within S)" + and derf: "\x. x \ S - K \ (f has_derivative (\h. 0)) (at x within S)" and "x \ 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: