# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503847044 -3600
# Node ID 0d8dab1f6903b4c59c4ef71577e880796885fab4
# Parent  5a1a2ac950c285125204fb38d354e87e4eedb6aa
some tidying of division_of_nontrivial

diff -r 5a1a2ac950c2 -r 0d8dab1f6903 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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