--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 27 13:50:23 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Aug 27 16:17:24 2017 +0100
@@ -2867,57 +2867,52 @@
subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
-lemma division_of_nontrivial:
- fixes s :: "'a::euclidean_space set set"
- assumes s: "s division_of (cbox a b)"
- and "content (cbox a b) \<noteq> 0"
- shows "{k. k \<in> s \<and> content k \<noteq> 0} division_of (cbox a b)"
- using s
-proof (induction "card s" arbitrary: s rule: less_induct)
+proposition division_of_nontrivial:
+ fixes \<D> :: "'a::euclidean_space set set"
+ assumes sdiv: "\<D> division_of (cbox a b)"
+ and cont0: "content (cbox a b) \<noteq> 0"
+ shows "{k. k \<in> \<D> \<and> content k \<noteq> 0} division_of (cbox a b)"
+ using sdiv
+proof (induction "card \<D>" arbitrary: \<D> rule: less_induct)
case less
- note s = division_ofD[OF less.prems]
+ note \<D> = division_ofD[OF less.prems]
{
- presume *: "{k \<in> s. content k \<noteq> 0} \<noteq> s \<Longrightarrow> ?case"
+ presume *: "{k \<in> \<D>. content k \<noteq> 0} \<noteq> \<D> \<Longrightarrow> ?case"
then show ?case
using less.prems by fastforce
}
- assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s"
- then obtain k c d where "k \<in> s" and contk: "content k = 0" and keq: "k = cbox c d"
- using s(4) by blast
- then have "card s > 0"
+ assume noteq: "{k \<in> \<D>. content k \<noteq> 0} \<noteq> \<D>"
+ then obtain K c d where "K \<in> \<D>" and contk: "content K = 0" and keq: "K = cbox c d"
+ using \<D>(4) by blast
+ then have "card \<D> > 0"
unfolding card_gt_0_iff using less by auto
- then have card: "card (s - {k}) < card s"
- using less \<open>k \<in> s\<close> by (simp add: s(1))
- have closed: "closed (\<Union>(s - {k}))"
+ then have card: "card (\<D> - {K}) < card \<D>"
+ using less \<open>K \<in> \<D>\<close> by (simp add: \<D>(1))
+ have closed: "closed (\<Union>(\<D> - {K}))"
using less.prems by auto
- have "k \<subseteq> \<Union>(s - {k})"
- apply safe
- apply (rule closed[unfolded closed_limpt,rule_format])
+ have "x islimpt \<Union>(\<D> - {K})" if "x \<in> K" for x
unfolding islimpt_approachable
- proof safe
- fix x and e :: real
- assume "x \<in> k" "e > 0"
+ proof (intro allI impI)
+ fix e::real
+ assume "e > 0"
obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>Basis"
- using contk s(3) [OF \<open>k \<in> s\<close>] unfolding box_ne_empty keq
+ using contk \<D>(3) [OF \<open>K \<in> \<D>\<close>] unfolding box_ne_empty keq
by (meson content_eq_0 dual_order.antisym)
then have xi: "x\<bullet>i = d\<bullet>i"
- using \<open>x \<in> k\<close> unfolding keq mem_box by (metis antisym)
+ using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)"
- show "\<exists>x'\<in>\<Union>(s - {k}). x' \<noteq> x \<and> dist x' x < e"
- apply (rule_tac x=y in bexI)
- proof
+ show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
+ proof (intro bexI conjI)
have "d \<in> cbox c d"
- using s(3)[OF \<open>k \<in> s\<close>] by (simp add: box_ne_empty(1) keq mem_box(2))
+ using \<D>(3)[OF \<open>K \<in> \<D>\<close>] by (simp add: box_ne_empty(1) keq mem_box(2))
then have "d \<in> cbox a b"
- using s(2)[OF \<open>k \<in> s\<close>]
- unfolding keq
- by auto
- note di = this[unfolded mem_box,THEN bspec[where x=i]]
+ using \<D>(2)[OF \<open>K \<in> \<D>\<close>] by (auto simp: keq)
+ then have di: "a \<bullet> i \<le> d \<bullet> i \<and> d \<bullet> i \<le> b \<bullet> i"
+ using \<open>i \<in> Basis\<close> mem_box(2) by blast
then have xyi: "y\<bullet>i \<noteq> x\<bullet>i"
- unfolding y_def i xi
- using \<open>e > 0\<close> assms(2)[unfolded content_eq_0] i(2)
- by (auto elim!: ballE[of _ _ i])
+ unfolding y_def i xi using \<open>e > 0\<close> cont0 \<open>i \<in> Basis\<close>
+ by (auto simp: content_eq_0 elim!: ballE[of _ _ i])
then show "y \<noteq> x"
unfolding euclidean_eq_iff[where 'a='a] using i by auto
have "norm (y-x) \<le> (\<Sum>b\<in>Basis. \<bar>(y - x) \<bullet> b\<bar>)"
@@ -2934,25 +2929,23 @@
finally have "norm (y-x) < e + sum (\<lambda>i. 0) Basis" .
then show "dist y x < e"
unfolding dist_norm by auto
- have "y \<notin> k"
+ have "y \<notin> K"
unfolding keq mem_box using i(1) i(2) xi xyi by fastforce
- moreover
- have "y \<in> \<Union>s"
- using subsetD[OF s(2)[OF \<open>k \<in> s\<close>] \<open>x \<in> k\<close>] \<open>e > 0\<close> di i
- unfolding s mem_box y_def
- by (auto simp: field_simps elim!: ballE[of _ _ i])
- ultimately
- show "y \<in> \<Union>(s - {k})" by auto
+ moreover have "y \<in> \<Union>\<D>"
+ using subsetD[OF \<D>(2)[OF \<open>K \<in> \<D>\<close>] \<open>x \<in> K\<close>] \<open>e > 0\<close> di i
+ by (auto simp: \<D> mem_box y_def field_simps elim!: ballE[of _ _ i])
+ ultimately show "y \<in> \<Union>(\<D> - {K})" by auto
qed
qed
- then have "\<Union>(s - {k}) = cbox a b"
- unfolding s(6)[symmetric] by auto
- then have "s - {k} division_of cbox a b"
- by (metis Diff_subset less.prems division_of_subset s(6))
- then have "{ka \<in> s - {k}. content ka \<noteq> 0} division_of (cbox a b)"
+ then have "K \<subseteq> \<Union>(\<D> - {K})"
+ using closed closed_limpt by blast
+ then have "\<Union>(\<D> - {K}) = cbox a b"
+ unfolding \<D>(6)[symmetric] by auto
+ then have "\<D> - {K} division_of cbox a b"
+ by (metis Diff_subset less.prems division_of_subset \<D>(6))
+ then have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} division_of (cbox a b)"
using card less.hyps by blast
- moreover
- have "{ka \<in> s - {k}. content ka \<noteq> 0} = {k \<in> s. content k \<noteq> 0}"
+ moreover have "{ka \<in> \<D> - {K}. content ka \<noteq> 0} = {K \<in> \<D>. content K \<noteq> 0}"
using contk by auto
ultimately show ?case by auto
qed
@@ -3003,7 +2996,7 @@
assumes "f integrable_on {a..b}"
and "{c..d} \<subseteq> {a..b}"
shows "f integrable_on {c..d}"
- by (metis assms(1) assms(2) box_real(2) integrable_subinterval)
+ by (metis assms box_real(2) integrable_subinterval)
subsection \<open>Combining adjacent intervals in 1 dimension.\<close>
@@ -4159,11 +4152,9 @@
unfolding *(1)
apply (subst *(2))
apply (rule norm_triangle_lt add_strict_mono)+
- unfolding norm_minus_cancel
- apply (rule d1_fin[unfolded **])
- apply (rule d2_fin)
+ apply (metis "**" d1_fin norm_minus_cancel)
+ using d2_fin apply blast
using w ***
- unfolding norm_scaleR
apply (auto simp add: field_simps)
done
qed