author paulson Tue, 16 Jun 2015 20:50:00 +0100 changeset 60492 db0f4f4c17c7 parent 60491 2803bc16742c child 60493 866f41a869e6 child 60495 d7ff0a1df90a child 60499 54a3db2ed201
another messy proof fixed
```--- 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"
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: 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 @@
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"```