# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1433977947 -3600
# Node ID a5c68d06cbf0fafa881f9aece991e356af9a09a7
# Parent  5035a2af185b613a9bd5e6084fce2627efa79f5f
tidied more proofs

diff -r 5035a2af185b -r a5c68d06cbf0 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Jun 10 22:28:56 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jun 11 00:12:27 2015 +0100
@@ -2794,7 +2794,7 @@
   assume ?l
   then guess y unfolding integrable_on_def has_integral .. note y=this
   show "\<forall>e>0. \<exists>d. ?P e d"
-  proof (rule, rule)
+  proof clarify
     case goal1
     then have "e/2 > 0" by auto
     then guess d
@@ -2824,15 +2824,7 @@
     apply auto
     done
   then have "\<forall>n. \<exists>p. p tagged_division_of (cbox a b) \<and> (\<lambda>x. \<Inter>{d i x |i. i \<in> {0..n}}) fine p"
-    apply -
-  proof
-    case goal1
-    from this[of n]
-    show ?case
-      apply (drule_tac fine_division_exists)
-      apply auto
-      done
-  qed
+    by (meson fine_division_exists)
   from choice[OF this] guess p .. note p = conjunctD2[OF this[rule_format]]
   have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
     using p(2) unfolding fine_inters by auto
@@ -2842,7 +2834,7 @@
     then guess N unfolding real_arch_inv[of e] .. note N=this
     show ?case
       apply (rule_tac x=N in exI)
-    proof (rule, rule, rule, rule)
+    proof clarify
       fix m n
       assume mn: "N \<le> m" "N \<le> n"
       have *: "N = (N - 1) + 1" using N by auto
@@ -2850,8 +2842,7 @@
         apply (rule less_trans[OF _ N[THEN conjunct2,THEN conjunct2]])
         apply(subst *)
         apply(rule d(2))
-        using dp p(1)
-        using mn
+        using dp p(1) mn
         apply auto
         done
     qed
@@ -2859,24 +2850,18 @@
   then guess y unfolding convergent_eq_cauchy[symmetric] .. note y=this[THEN LIMSEQ_D]
   show ?l
     unfolding integrable_on_def has_integral
-    apply (rule_tac x=y in exI)
-  proof (rule, rule)
+  proof (rule_tac x=y in exI, clarify)
     fix e :: real
     assume "e>0"
-    then have *:"e/2 > 0" by auto
+    then have *:"e/2 > 0" by auto 
     then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this
     then have N1': "N1 = N1 - 1 + 1"
       by auto
     guess N2 using y[OF *] .. note N2=this
-    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) - y) < e)"
-      apply (rule_tac x="d (N1 + N2)" in exI)
-      apply rule
-      defer
-    proof (rule, rule, erule conjE)
-      show "gauge (d (N1 + N2))"
-        using d by auto
+    have "gauge (d (N1 + N2))"
+      using d by auto
+    moreover
+    {
       fix q
       assume as: "q tagged_division_of (cbox a b)" "d (N1 + N2) fine q"
       have *: "inverse (real (N1 + N2 + 1)) < e / 2"
@@ -2884,18 +2869,18 @@
         using N1
         apply auto
         done
-      show "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e"
+      have "norm ((\<Sum>(x, k)\<in>q. content k *\<^sub>R f x) - y) < e"
         apply (rule norm_triangle_half_r)
         apply (rule less_trans[OF _ *])
         apply (subst N1', rule d(2)[of "p (N1+N2)"])
-        defer
-        using N2[rule_format,of "N1+N2"]
-        using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"]
-        using p(1)[of "N1 + N2"]
-        using N1
-        apply auto
-        done
-    qed
+        using N1' as(1) as(2) dp 
+        apply (simp add: `\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x`)
+        using N2 le_add2 by blast
+    }
+    ultimately 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) - y) < e)"
+      by (rule_tac x="d (N1 + N2)" in exI) auto
   qed
 qed
 
@@ -2980,11 +2965,8 @@
   show ?thesis
     unfolding uv1 uv2 *
     apply (rule **[OF d(5)[OF assms(2-4)]])
-    defer
-    apply (subst assms(5)[unfolded uv1 uv2])
-    unfolding uv1 uv2
-    apply auto
-    done
+    apply (simp add: uv1)
+    using assms(5) uv1 by auto
 qed
 
 lemma division_split_right_inj:
@@ -3008,57 +2990,42 @@
   show ?thesis
     unfolding uv1 uv2 *
     apply (rule **[OF d(5)[OF assms(2-4)]])
-    defer
-    apply (subst assms(5)[unfolded uv1 uv2])
-    unfolding uv1 uv2
-    apply auto
-    done
+    apply (simp add: uv1)
+    using assms(5) uv1 by auto
 qed
 
 lemma tagged_division_split_left_inj:
   fixes x1 :: "'a::euclidean_space"
-  assumes "d tagged_division_of i"
-    and "(x1, k1) \<in> d"
-    and "(x2, k2) \<in> d"
-    and "k1 \<noteq> k2"
-    and "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
-    and k: "k \<in> Basis"
+  assumes d: "d tagged_division_of i"
+    and k12: "(x1, k1) \<in> d"
+             "(x2, k2) \<in> d"
+             "k1 \<noteq> k2"
+             "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
+             "k \<in> Basis"
   shows "content (k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
 proof -
   have *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c"
-    unfolding image_iff
-    apply (rule_tac x="(a,b)" in bexI)
-    apply auto
-    done
+    by force
   show ?thesis
-    apply (rule division_split_left_inj[OF division_of_tagged_division[OF assms(1)]])
-    apply (rule_tac[1-2] *)
-    using assms(2-)
-    apply auto
-    done
+    using k12
+    by (fastforce intro!:  division_split_left_inj[OF division_of_tagged_division[OF d]] *)
 qed
 
 lemma tagged_division_split_right_inj:
   fixes x1 :: "'a::euclidean_space"
-  assumes "d tagged_division_of i"
-    and "(x1, k1) \<in> d"
-    and "(x2, k2) \<in> d"
-    and "k1 \<noteq> k2"
-    and "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
-  and k: "k \<in> Basis"
+  assumes d: "d tagged_division_of i"
+    and k12: "(x1, k1) \<in> d"
+             "(x2, k2) \<in> d"
+             "k1 \<noteq> k2"
+             "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+             "k \<in> Basis"
   shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
 proof -
   have *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c"
-    unfolding image_iff
-    apply (rule_tac x="(a,b)" in bexI)
-    apply auto
-    done
+    by force
   show ?thesis
-    apply (rule division_split_right_inj[OF division_of_tagged_division[OF assms(1)]])
-    apply (rule_tac[1-2] *)
-    using assms(2-)
-    apply auto
-    done
+    using k12
+    by (fastforce intro!:  division_split_right_inj[OF division_of_tagged_division[OF d]] *)
 qed
 
 lemma division_split:
@@ -3080,12 +3047,12 @@
     assume "k \<in> ?p1"
     then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
     guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
-    show "k \<subseteq> ?I1" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
-      unfolding l
-      using p(2-3)[OF l(2)] l(3)
-      unfolding uv
-      apply -
-      prefer 3
+    show "k \<subseteq> ?I1" 
+      using l p(2) uv by force
+    show  "k \<noteq> {}" 
+      by (simp add: l)
+    show  "\<exists>a b. k = cbox a b"
+      apply (simp add: l uv p(2-3)[OF l(2)])
       apply (subst interval_split[OF k])
       apply (auto intro: order.trans)
       done
@@ -3101,12 +3068,12 @@
     assume "k \<in> ?p2"
     then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
     guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
-    show "k \<subseteq> ?I2" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
-      unfolding l
-      using p(2-3)[OF l(2)] l(3)
-      unfolding uv
-      apply -
-      prefer 3
+    show "k \<subseteq> ?I2" 
+      using l p(2) uv by force
+    show  "k \<noteq> {}" 
+      by (simp add: l)
+    show  "\<exists>a b. k = cbox a b"
+      apply (simp add: l uv p(2-3)[OF l(2)])
       apply (subst interval_split[OF k])
       apply (auto intro: order.trans)
       done
@@ -3200,11 +3167,10 @@
     have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
     proof -
       case goal1
+      then have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
+        by auto
       then show ?case
-        apply -
-        apply (rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"])
-        apply auto
-        done
+        by (rule rev_finite_subset) auto
     qed
     have lem3: "\<And>g :: 'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
       setsum (\<lambda>(x, k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> g k \<noteq> {}} =
@@ -3321,10 +3287,7 @@
     qed
     ultimately
     have "norm (((\<Sum>(x, k)\<in>?M1. content k *\<^sub>R f x) - i) + ((\<Sum>(x, k)\<in>?M2. content k *\<^sub>R f x) - j)) < e/2 + e/2"
-      apply -
-      apply (rule norm_triangle_lt)
-      apply auto
-      done
+      using norm_add_less by blast
     also {
       have *: "\<And>x y. x = (0::real) \<Longrightarrow> x *\<^sub>R (y::'b) = 0"
         using scaleR_zero_left by auto
@@ -3468,12 +3431,8 @@
         have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (e / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then e/2 else 0)"
           using e k by (auto simp: inner_simps inner_not_same_Basis)
         have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (e / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
-          (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
-          apply (rule setsum.cong)
-          apply (rule refl)
-          apply (subst *)
-          apply auto
-          done
+              (\<Sum>i\<in>Basis. (if i = k then e / 2 else 0))"
+          using "*" by (blast intro: setsum.cong)
         also have "\<dots> < e"
           apply (subst setsum.delta)
           using e