# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503955907 -3600
# Node ID 0ad3fc48c9ec07ac2d18ee75e0f8c88bfa4d9c6e
# Parent  6e50b550adf5a72d86c3dbbf1d181c79774eba2f
final cleanup of negligible_standard_hyperplane and other things

diff -r 6e50b550adf5 -r 0ad3fc48c9ec src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 20:33:20 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 22:31:47 2017 +0100
@@ -3617,22 +3617,24 @@
       and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> 0 \<le> Im (vector_derivative \<gamma> (at x) * cnj(\<gamma> x - z))"
     shows "0 \<le> Re(winding_number \<gamma> z)"
 proof -
-  have *: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
+  have ge0: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
     using ge by (simp add: Complex.Im_divide algebra_simps x)
-  show ?thesis
-    apply (simp add: Re_winding_number [OF \<gamma>] field_simps)
+  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
+            (cbox 0 1)"
+    unfolding box_real
+    apply (subst has_contour_integral [symmetric])
+    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
+  have "0 \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
     apply (rule has_integral_component_nonneg
              [of \<i> "\<lambda>x. if x \<in> {0<..<1}
                          then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else 0", simplified])
-      prefer 3 apply (force simp: *)
+      prefer 3 apply (force simp: ge0)
      apply (simp add: Basis_complex_def)
-    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)"])
+    apply (rule has_integral_spike_interior [OF hi])
     apply simp
-    apply (simp only: box_real)
-    apply (subst has_contour_integral [symmetric])
-    using \<gamma>
-    apply (simp add: contour_integrable_inversediff has_contour_integral_integral)
     done
+  then show ?thesis
+    by (simp add: Re_winding_number [OF \<gamma>] field_simps)
 qed
 
 lemma winding_number_pos_lt_lemma:
@@ -3641,19 +3643,20 @@
       and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
     shows "0 < Re(winding_number \<gamma> z)"
 proof -
+  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
+            (cbox 0 1)"
+    unfolding box_real
+    apply (subst has_contour_integral [symmetric])
+    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
   have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
     apply (rule has_integral_component_le
              [of \<i> "\<lambda>x. \<i>*e" "\<i>*e" "{0..1}"
                     "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else \<i>*e"
                     "contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
-    using e
-    apply (simp_all add: Basis_complex_def)
+    using e apply (simp_all add: Basis_complex_def)
     using has_integral_const_real [of _ 0 1] apply force
-    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)", simplified box_real])
-    apply simp
-    apply (subst has_contour_integral [symmetric])
-    using \<gamma>
-    apply (simp_all add: contour_integrable_inversediff has_contour_integral_integral ge)
+     apply (rule has_integral_spike_interior [OF hi, simplified box_real])
+    apply (simp_all add: ge)
     done
   with e show ?thesis
     by (simp add: Re_winding_number [OF \<gamma>] field_simps)
diff -r 6e50b550adf5 -r 0ad3fc48c9ec src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 20:33:20 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 22:31:47 2017 +0100
@@ -2000,50 +2000,45 @@
   next
     fix \<D>
     assume p: "\<D> tagged_division_of (cbox a b)" "(\<lambda>x. ball x d) fine \<D>"
-    have "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})" 
-      if "(x, l) \<in> \<D>" "?i x \<noteq> 0" for x l
+    have "content L = content (L \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})" 
+      if "(x, L) \<in> \<D>" "?i x \<noteq> 0" for x L
     proof -
       have xk: "x\<bullet>k = c"
         using that by (simp add: indicator_def split: if_split_asm)
-      show "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
-        apply (rule arg_cong[where f=content])
-        apply (rule set_eqI)
-        apply rule
-         apply rule
-        unfolding mem_Collect_eq
-      proof -
+      have "L \<subseteq> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
+      proof 
         fix y
-        assume y: "y \<in> l"
-        note p(2)[unfolded fine_def,rule_format,OF that(1),unfolded split_conv]
-        note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y]
-        note le_less_trans[OF Basis_le_norm[OF k] this]
-        then show "\<bar>y \<bullet> k - c\<bar> \<le> d"
+        assume y: "y \<in> L"
+        have "L \<subseteq> ball x d"
+          using p(2) that(1) by auto
+        then have "norm (x - y) < d"
+          by (simp add: dist_norm subset_iff y)
+        then have "\<bar>(x - y) \<bullet> k\<bar> < d"
+          using k norm_bound_Basis_lt by blast
+        then show "y \<in> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
           unfolding inner_simps xk by auto
-      qed auto
+      qed 
+      then show "content L = content (L \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
+        by (metis inf.orderE)
     qed
     then have *: "(\<Sum>(x,K)\<in>\<D>. content K * ?i x) = (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
       by (force simp add: split_paired_all intro!: sum.cong [OF refl])
     note p'= tagged_division_ofD[OF p(1)] and p''=division_of_tagged_division[OF p(1)]
     have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
     proof -
-      have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
-        (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
-        apply (rule sum_mono)
-        unfolding split_paired_all split_conv
-        apply (rule mult_right_le_one_le)
-          apply (drule p'(4))
-          apply (auto simp add:interval_doublesplit[OF k])
-        done
+      have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
+        by (force simp add: indicator_def intro!: sum_mono)
       also have "\<dots> < e"
-      proof (subst sum.over_tagged_division_lemma[OF p(1)], goal_cases)
-        case prems: (1 u v)
+      proof (subst sum.over_tagged_division_lemma[OF p(1)])
+        fix u v::'a
+        assume "box u v = {}"
         then have *: "content (cbox u v) = 0"
           unfolding content_eq_0_interior by simp
         have "cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<subseteq> cbox u v"
           by auto
         then have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
           unfolding interval_doublesplit[OF k] by (rule content_subset)
-        then show ?case
+        then show "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
           unfolding * interval_doublesplit[OF k]
           by (blast intro: antisym)
       next
@@ -2395,47 +2390,30 @@
 lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
 proof -
   let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
-  have "cbox a b - box a b \<subseteq> ?A"
-    apply rule unfolding Diff_iff mem_box
-    apply simp
-    apply(erule conjE bexE)+
-    apply(rule_tac x=i in bexI)
-    apply auto
-    done
-  then show ?thesis
-    apply -
-    apply (rule negligible_subset[of ?A])
-    apply (rule negligible_Union[OF finite_imageI])
-    apply auto
-    done
+  have "negligible ?A"
+    by (force simp add: negligible_Union[OF finite_imageI])
+  moreover have "cbox a b - box a b \<subseteq> ?A"
+    by (force simp add: mem_box)
+  ultimately show ?thesis
+    by (rule negligible_subset)
 qed
 
 lemma has_integral_spike_interior:
-  assumes "\<forall>x\<in>box a b. g x = f x"
-    and "(f has_integral y) (cbox a b)"
+  assumes f: "(f has_integral y) (cbox a b)" and gf: "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
   shows "(g has_integral y) (cbox a b)"
-  apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
-  using assms(1)
-  apply auto
-  done
+  apply (rule has_integral_spike[OF negligible_frontier_interval _ f])
+  using gf by auto
 
 lemma has_integral_spike_interior_eq:
-  assumes "\<forall>x\<in>box a b. g x = f x"
+  assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
   shows "(f has_integral y) (cbox a b) \<longleftrightarrow> (g has_integral y) (cbox a b)"
-  apply rule
-  apply (rule_tac[!] has_integral_spike_interior)
-  using assms
-  apply auto
-  done
+  by (metis assms has_integral_spike_interior)
 
 lemma integrable_spike_interior:
-  assumes "\<forall>x\<in>box a b. g x = f x"
+  assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
     and "f integrable_on cbox a b"
   shows "g integrable_on cbox a b"
-  using assms
-  unfolding integrable_on_def
-  using has_integral_spike_interior[OF assms(1)]
-  by auto
+  using assms has_integral_spike_interior_eq by blast
 
 
 subsection \<open>Integrability of continuous functions.\<close>
@@ -4385,7 +4363,7 @@
       by (meson g_def has_integral_integrable intf)
     moreover have "integral (cbox c d) g = i"
     proof (rule has_integral_unique[OF has_integral_spike_interior intf])
-      show "\<forall>x\<in>box c d. f x = g x"
+      show "\<And>x. x \<in> box c d \<Longrightarrow> f x = g x"
         by (auto simp: g_def)
       show "(g has_integral integral (cbox c d) g) (cbox c d)"
         by (rule integrable_integral[OF intg])