# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1434484200 -3600
# Node ID db0f4f4c17c732cbf43bbc7fcd09b997a0a60ea2
# Parent  2803bc16742c43cf34592ca380ecd7293e3963f8
another messy proof fixed

diff -r 2803bc16742c -r db0f4f4c17c7 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 15 23:56:40 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 16 20:50:00 2015 +0100
@@ -4578,7 +4578,8 @@
   fixes a :: "'a::euclidean_space"
   assumes "p division_of (cbox a b)"
     and k: "k \<in> Basis"
-  shows "{l \<inter> {x. abs(x\<bullet>k - c) \<le> e} |l. l \<in> p \<and> l \<inter> {x. abs(x\<bullet>k - c) \<le> e} \<noteq> {}} division_of (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> e})"
+  shows "{l \<inter> {x. abs(x\<bullet>k - c) \<le> e} |l. l \<in> p \<and> l \<inter> {x. abs(x\<bullet>k - c) \<le> e} \<noteq> {}}
+         division_of  (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> e})"
 proof -
   have *: "\<And>x c. abs (x - c) \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
     by auto
@@ -4588,18 +4589,11 @@
   note division_split(2)[OF this, where c="c-e" and k=k,OF k]
   then show ?thesis
     apply (rule **)
+    unfolding interval_doublesplit [OF k]
     using k
-    apply -
-    unfolding interval_doublesplit
-    unfolding *
-    unfolding interval_split interval_doublesplit
-    apply (rule set_eqI)
-    unfolding mem_Collect_eq
-    apply rule
-    apply (erule conjE exE)+
-    apply (rule_tac x=la in exI)
-    defer
-    apply (erule conjE exE)+
+    apply (simp_all add: * interval_split)
+    apply (rule equalityI, blast)
+    apply clarsimp
     apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
     apply auto
     done
@@ -4612,16 +4606,14 @@
   obtains d where "0 < d" and "content (cbox a b \<inter> {x. abs(x\<bullet>k - c) \<le> d}) < e"
 proof (cases "content (cbox a b) = 0")
   case True
+  then have ce: "content (cbox a b) < e"
+    by (metis `0 < e`)
   show ?thesis
     apply (rule that[of 1])
-    defer
+    apply simp
     unfolding interval_doublesplit[OF k]
-    apply (rule le_less_trans[OF content_subset])
-    defer
-    apply (subst True)
-    unfolding interval_doublesplit[symmetric,OF k]
-    using assms
-    apply auto
+    apply (rule le_less_trans[OF content_subset ce])
+    apply (auto simp: interval_doublesplit[symmetric] k)
     done
 next
   case False
@@ -4630,47 +4622,15 @@
   then have "\<And>x. x \<in> Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x"
     by (auto simp add:not_le)
   then have prod0: "0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
-    apply -
-    apply (rule setprod_pos)
-    apply (auto simp add: field_simps)
-    done
+    by (force simp add: setprod_pos field_simps)
   then have "d > 0"
-    unfolding d_def
     using assms
-    by (auto simp add:field_simps)
+    by (auto simp add: d_def field_simps)
   then show ?thesis
   proof (rule that[of d])
     have *: "Basis = insert k (Basis - {k})"
       using k by auto
-    have **: "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {} \<Longrightarrow>
-      (\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
-        interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i) =
-      (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
-      apply (rule setprod.cong)
-      apply (rule refl)
-      unfolding interval_doublesplit[OF k]
-      apply (subst interval_bounds)
-      defer
-      apply (subst interval_bounds)
-      unfolding box_eq_empty not_ex not_less
-      apply auto
-      done
-    show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
-      apply cases
-      unfolding content_def
-      apply (subst if_P)
-      apply assumption
-      apply (rule assms)
-      unfolding if_not_P
-      apply (subst *)
-      apply (subst setprod.insert)
-      unfolding **
-      unfolding interval_doublesplit[OF k] box_eq_empty not_ex not_less
-      prefer 3
-      apply (subst interval_bounds)
-      defer
-      apply (subst interval_bounds)
-      apply (simp_all only: k inner_setsum_left_Basis simp_thms if_P cong: bex_cong ball_cong)
+    have less_e: "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
     proof -
       have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d"
         by auto
@@ -4680,7 +4640,27 @@
         by (auto simp add: field_simps)
       finally show "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
         unfolding pos_less_divide_eq[OF prod0] .
-    qed auto
+    qed
+    show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
+    proof (cases "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {}")
+      case True
+      then show ?thesis
+        using assms by simp
+    next
+      case False
+      then have 
+          "(\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
+                interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i) 
+           = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
+        by (simp add: box_eq_empty interval_doublesplit[OF k])
+      then show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
+        unfolding content_def
+        using assms False 
+        apply (subst *)
+        apply (subst setprod.insert)
+        apply (simp_all add: interval_doublesplit[OF k] box_eq_empty not_less less_e)
+        done
+    qed
   qed
 qed
 
@@ -4689,8 +4669,7 @@
   assumes k: "k \<in> Basis"
   shows "negligible {x. x\<bullet>k = c}"
   unfolding negligible_def has_integral
-  apply (rule, rule, rule, rule)
-proof -
+proof clarify
   case goal1
   from content_doublesplit[OF this k,of a b c] guess d . note d=this
   let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"