# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1434400406 -3600
# Node ID 2abfcf85c62728dccde5a80ce5ac3822d4100976
# Parent  17a2dae7d2462a4a734dde3e8be33904226094cd
inverted another messy proof

diff -r 17a2dae7d246 -r 2abfcf85c627 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 15 15:34:29 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 15 21:33:26 2015 +0100
@@ -2763,7 +2763,7 @@
   qed
 next
   assume "\<forall>e>0. \<exists>d. ?P e d"
-  then have "\<forall>n::nat. \<exists>d. ?P (inverse(real (n + 1))) d"
+  then have "\<forall>n::nat. \<exists>d. ?P (inverse(of_nat (n + 1))) d"
     by auto
   from choice[OF this] guess d .. note d=conjunctD2[OF this[rule_format],rule_format]
   have "\<And>n. gauge (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}})"
@@ -2789,10 +2789,7 @@
       show "norm ((\<Sum>(x, k)\<in>p m. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p n. content k *\<^sub>R f x)) < e"
         apply (rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]])
         apply(subst *)
-        apply(rule d(2))
-        using dp p(1) mn
-        apply auto
-        done
+        using dp p(1) mn d(2) real_of_nat_def by auto
     qed
   qed
   then guess y unfolding convergent_eq_cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
@@ -2812,7 +2809,7 @@
     {
       fix q
       assume as: "q tagged_division_of (cbox a b)" "d (N1 + N2) fine q"
-      have *: "inverse (real (N1 + N2 + 1)) < e / 2"
+      have *: "inverse (of_nat (N1 + N2 + 1)) < e / 2"
         apply (rule less_trans)
         using N1
         apply auto
@@ -4417,153 +4414,128 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
   assumes "\<forall>e>0. \<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
   shows "f integrable_on cbox a b"
-proof -
-  {
-    presume *: "content (cbox a b) > 0 \<Longrightarrow> ?thesis"
-    show ?thesis
-      apply cases
-      apply (rule *)
-      apply assumption
-      unfolding content_lt_nz integrable_on_def
+proof (cases "content (cbox a b) > 0")
+  case False then show ?thesis
       using has_integral_null
-      apply auto
-      done
-  }
-  assume as: "content (cbox a b) > 0"
+      by (simp add: content_lt_nz integrable_on_def)
+next
+  case True
   have *: "\<And>P. \<forall>e>(0::real). P e \<Longrightarrow> \<forall>n::nat. P (inverse (real n + 1))"
     by auto
   from choice[OF *[OF assms]] guess g .. note g=conjunctD2[OF this[rule_format],rule_format]
-  from choice[OF allI[OF g(2)[unfolded integrable_on_def], of "\<lambda>x. x"]] guess i .. note i=this[rule_format]
-
+  from choice[OF allI[OF g(2)[unfolded integrable_on_def], of "\<lambda>x. x"]] 
+  obtain i where i: "\<And>x. (g x has_integral i x) (cbox a b)"
+      by auto
   have "Cauchy i"
     unfolding Cauchy_def
-  proof (rule, rule)
+  proof clarify
     fix e :: real
     assume "e>0"
     then have "e / 4 / content (cbox a b) > 0"
-      using as by (auto simp add: field_simps)
-    then guess M
-      apply -
-      apply (subst(asm) real_arch_inv)
-      apply (elim exE conjE)
-      done
-    note M=this
+      using True by (auto simp add: field_simps)
+    then obtain M :: nat
+         where M: "M \<noteq> 0" "0 < inverse (real_of_nat M)" "inverse (of_nat M) < e / 4 / content (cbox a b)"
+      by (subst (asm) real_arch_inv) (auto simp: real_of_nat_def)
     show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (i m) (i n) < e"
-      apply (rule_tac x=M in exI,rule,rule,rule,rule)
-    proof -
-      case goal1
+    proof (rule exI [where x=M], clarify)
+      fix m n
+      assume m: "M \<le> m" and n: "M \<le> n"
       have "e/4>0" using \<open>e>0\<close> by auto
       note * = i[unfolded has_integral,rule_format,OF this]
       from *[of m] guess gm by (elim conjE exE) note gm=this[rule_format]
       from *[of n] guess gn by (elim conjE exE) note gn=this[rule_format]
-      from fine_division_exists[OF gauge_inter[OF gm(1) gn(1)], of a b] guess p . note p=this
-      have lem2: "\<And>s1 s2 i1 i2. norm(s2 - s1) \<le> e/2 \<Longrightarrow> norm (s1 - i1) < e / 4 \<Longrightarrow>
-        norm (s2 - i2) < e / 4 \<Longrightarrow> norm (i1 - i2) < e"
-      proof -
-        case goal1
+      from fine_division_exists[OF gauge_inter[OF gm(1) gn(1)], of a b] 
+      obtain p where p: "p tagged_division_of cbox a b" "(\<lambda>x. gm x \<inter> gn x) fine p"
+        by auto
+      { fix s1 s2 i1 and i2::'b
+        assume no: "norm(s2 - s1) \<le> e/2" "norm (s1 - i1) < e/4" "norm (s2 - i2) < e/4"
         have "norm (i1 - i2) \<le> norm (i1 - s1) + norm (s1 - s2) + norm (s2 - i2)"
           using norm_triangle_ineq[of "i1 - s1" "s1 - i2"]
           using norm_triangle_ineq[of "s1 - s2" "s2 - i2"]
           by (auto simp add: algebra_simps)
         also have "\<dots> < e"
-          using goal1
+          using no
           unfolding norm_minus_commute
           by (auto simp add: algebra_simps)
-        finally show ?case .
-      qed
-      show ?case
-        unfolding dist_norm
-        apply (rule lem2)
-        defer
-        apply (rule gm(2)[OF conjI[OF p(1)]],rule_tac[2] gn(2)[OF conjI[OF p(1)]])
-        using conjunctD2[OF p(2)[unfolded fine_inter]]
-        apply -
-        apply assumption+
-        apply (rule order_trans)
-        apply (rule rsum_diff_bound[OF p(1), where e="2 / real M"])
-      proof
-        show "2 / real M * content (cbox a b) \<le> e / 2"
-          unfolding divide_inverse
-          using M as
-          by (auto simp add: field_simps)
-        fix x
+        finally have "norm (i1 - i2) < e" .
+      } note triangle3 = this
+      have finep: "gm fine p" "gn fine p"
+        using fine_inter p  by auto
+      { fix x
         assume x: "x \<in> cbox a b"
         have "norm (f x - g n x) + norm (f x - g m x) \<le> inverse (real n + 1) + inverse (real m + 1)"
           using g(1)[OF x, of n] g(1)[OF x, of m] by auto
         also have "\<dots> \<le> inverse (real M) + inverse (real M)"
           apply (rule add_mono)
-          apply (rule_tac[!] le_imp_inverse_le)
-          using goal1 M
-          apply auto
-          done
+          using M(2) m n by auto
         also have "\<dots> = 2 / real M"
           unfolding divide_inverse by auto
-        finally show "norm (g n x - g m x) \<le> 2 / real M"
+        finally have "norm (g n x - g m x) \<le> 2 / real M"
           using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
           by (auto simp add: algebra_simps simp add: norm_minus_commute)
-      qed
-    qed
-  qed
-  from this[unfolded convergent_eq_cauchy[symmetric]] guess s .. note s=this
-
+      } note norm_le = this
+      have le_e2: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g n x) - (\<Sum>(x, k)\<in>p. content k *\<^sub>R g m x)) \<le> e / 2"
+        apply (rule order_trans [OF rsum_diff_bound[OF p(1), where e="2 / real M"]])
+        apply (blast intro: norm_le)
+        using M True
+        by (auto simp add: field_simps)
+      then show "dist (i m) (i n) < e"
+        unfolding dist_norm
+        using gm gn p finep
+        by (auto intro!: triangle3)
+    qed
+  qed
+  then obtain s where s: "i ----> s" 
+    using convergent_eq_cauchy[symmetric] by blast
   show ?thesis
-    unfolding integrable_on_def
-    apply (rule_tac x=s in exI)
-    unfolding has_integral
-  proof (rule, rule)
-    case goal1
+    unfolding integrable_on_def has_integral
+  proof (rule_tac x=s in exI, clarify)
+    fix e::real
+    assume e: "0 < e"
     then have *: "e/3 > 0" by auto
-    from LIMSEQ_D [OF s this] guess N1 .. note N1=this
-    from goal1 as have "e / 3 / content (cbox a b) > 0"
+    then obtain N1 where N1: "\<forall>n\<ge>N1. norm (i n - s) < e / 3"
+      using LIMSEQ_D [OF s] by metis
+    from e True have "e / 3 / content (cbox a b) > 0"
       by (auto simp add: field_simps)
     from real_arch_invD[OF this] guess N2 by (elim exE conjE) note N2=this
     from i[of "N1 + N2",unfolded has_integral,rule_format,OF *] guess g' .. note g'=conjunctD2[OF this,rule_format]
-    have lem: "\<And>sf sg i. norm (sf - sg) \<le> e / 3 \<Longrightarrow>
-      norm(i - s) < e / 3 \<Longrightarrow> norm (sg - i) < e / 3 \<Longrightarrow> norm (sf - s) < e"
-    proof -
-      case goal1
+    { fix sf sg i
+      assume no: "norm (sf - sg) \<le> e / 3"
+                 "norm(i - s) < e / 3"
+                 "norm (sg - i) < e / 3"
       have "norm (sf - s) \<le> norm (sf - sg) + norm (sg - i) + norm (i - s)"
         using norm_triangle_ineq[of "sf - sg" "sg - s"]
         using norm_triangle_ineq[of "sg -  i" " i - s"]
         by (auto simp add: algebra_simps)
       also have "\<dots> < e"
-        using goal1
+        using no
         unfolding norm_minus_commute
         by (auto simp add: algebra_simps)
-      finally show ?case .
-    qed
-    show ?case
-      apply (rule_tac x=g' in exI)
-      apply rule
-      apply (rule g')
-    proof (rule, rule)
-      fix p
+      finally have "norm (sf - s) < e" .
+    } note lem = this 
+    { fix p
       assume p: "p tagged_division_of (cbox a b) \<and> g' fine p"
-      note * = g'(2)[OF this]
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - s) < e"
-        apply -
-        apply (rule lem[OF _ _ *])
-        apply (rule order_trans)
+      then have norm_less: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g (N1 + N2) x) - i (N1 + N2)) < e / 3"
+        using g' by blast
+      have "content (cbox a b) < e / 3 * (of_nat N2)"
+        using N2 unfolding inverse_eq_divide using True by (auto simp add: field_simps)
+      moreover have "e / 3 * of_nat N2 \<le> e / 3 * (of_nat (N1 + N2) + 1)"
+        using \<open>e>0\<close> by auto
+      ultimately have "content (cbox a b) < e / 3 * (of_nat (N1 + N2) + 1)"
+        by linarith
+      then have le_e3: "inverse (real (N1 + N2) + 1) * content (cbox a b) \<le> e / 3"
+        unfolding inverse_eq_divide
+        by (auto simp add: field_simps)
+      have ne3: "norm (i (N1 + N2) - s) < e / 3"
+        using N1 by auto
+      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - s) < e"
+        apply (rule lem[OF order_trans [OF _ le_e3] ne3 norm_less])
         apply (rule rsum_diff_bound[OF p[THEN conjunct1]])
-        apply rule
-        apply (rule g)
-        apply assumption
-      proof -
-        have "content (cbox a b) < e / 3 * (real N2)"
-          using N2 unfolding inverse_eq_divide using as by (auto simp add: field_simps)
-        then have "content (cbox a b) < e / 3 * (real (N1 + N2) + 1)"
-          apply -
-          apply (rule less_le_trans,assumption)
-          using \<open>e>0\<close>
-          apply auto
-          done
-        then show "inverse (real (N1 + N2) + 1) * content (cbox a b) \<le> e / 3"
-          unfolding inverse_eq_divide
-          by (auto simp add: field_simps)
-        show "norm (i (N1 + N2) - s) < e / 3"
-          by (rule N1[rule_format]) auto
-      qed
-    qed
+        apply (blast intro: g)
+        done }
+    then show "\<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) - s) < e)"
+      by (blast intro: g')
   qed
 qed
 
@@ -4576,20 +4548,15 @@
 
 subsection \<open>Negligibility of hyperplane.\<close>
 
-lemma vsum_nonzero_image_lemma:
+lemma setsum_nonzero_image_lemma:
   assumes "finite s"
     and "g a = 0"
     and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g (f x) = 0"
   shows "setsum g {f x |x. x \<in> s \<and> f x \<noteq> a} = setsum (g o f) s"
+  apply (subst setsum_iterate)
+  using assms monoidal_monoid 
   unfolding setsum_iterate[OF assms(1)]
-  apply (subst setsum_iterate)
-  defer
-  apply (rule iterate_nonzero_image_lemma)
-  apply (rule assms monoidal_monoid)+
-  unfolding assms
-  unfolding neutral_add
-  using assms
-  apply auto
+  apply (auto intro!: iterate_nonzero_image_lemma)
   done
 
 lemma interval_doublesplit:
@@ -4634,11 +4601,7 @@
     defer
     apply (erule conjE exE)+
     apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
-    apply rule
-    defer
-    apply rule
-    apply (rule_tac x=l in exI)
-    apply blast+
+    apply auto
     done
 qed
 
@@ -4837,7 +4800,7 @@
         note le_less_trans[OF this d(2)]
         from this[unfolded abs_of_nonneg[OF *]]
         show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e"
-          apply (subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,symmetric])
+          apply (subst setsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,symmetric])
           apply (rule finite_imageI p' content_empty)+
           unfolding forall_in_division[OF p'']
         proof (rule,rule,rule,rule,rule,rule,rule,erule conjE)