# HG changeset patch
# User wenzelm
# Date 1378484090 -7200
# Node ID 2f6c0289dcde4eb927e447d5c2c1c313178ad3ac
# Parent  f41ab5a7df97cea92c044528f39bc569ff796c1e
tuned proofs;

diff -r f41ab5a7df97 -r 2f6c0289dcde src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 06 17:55:01 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 06 18:14:50 2013 +0200
@@ -3330,34 +3330,79 @@
     done
 qed
 
-lemma division_split_right_inj: fixes type::"'a::ordered_euclidean_space"
-  assumes "d division_of i" "k1 \<in> d" "k2 \<in> d"  "k1 \<noteq> k2"
-  "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}" and k:"k\<in>Basis"
-  shows "content(k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
-proof- note d=division_ofD[OF assms(1)]
-  have *:"\<And>a b::'a. \<And> c. (content({a..b} \<inter> {x. x\<bullet>k >= c}) = 0 \<longleftrightarrow> interior({a..b} \<inter> {x. x\<bullet>k >= c}) = {})"
+lemma division_split_right_inj:
+  fixes type :: "'a::ordered_euclidean_space"
+  assumes "d division_of i"
+    and "k1 \<in> d"
+    and "k2 \<in> d"
+    and "k1 \<noteq> k2"
+    and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+    and k: "k \<in> Basis"
+  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
+proof -
+  note d=division_ofD[OF assms(1)]
+  have *: "\<And>a b::'a. \<And>c. content({a..b} \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
+    interior({a..b} \<inter> {x. x\<bullet>k \<ge> c}) = {}"
     unfolding interval_split[OF k] content_eq_0_interior by auto
   guess u1 v1 using d(4)[OF assms(2)] apply-by(erule exE)+ note uv1=this
   guess u2 v2 using d(4)[OF assms(3)] apply-by(erule exE)+ note uv2=this
-  have **:"\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}" by auto
-  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 by auto qed
-
-lemma tagged_division_split_left_inj: fixes x1::"'a::ordered_euclidean_space"
-  assumes "d tagged_division_of i" "(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}"
-  and k:"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) by auto
-  show ?thesis apply(rule division_split_left_inj[OF division_of_tagged_division[OF assms(1)]])
-    apply(rule_tac[1-2] *) using assms(2-) by auto qed
-
-lemma tagged_division_split_right_inj: fixes x1::"'a::ordered_euclidean_space"
-  assumes "d tagged_division_of i" "(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}"
-  and k:"k\<in>Basis"
+  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
+    by auto
+  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
+qed
+
+lemma tagged_division_split_left_inj:
+  fixes x1 :: "'a::ordered_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"
+  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
+  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
+qed
+
+lemma tagged_division_split_right_inj:
+  fixes x1 :: "'a::ordered_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"
   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) by auto
-  show ?thesis apply(rule division_split_right_inj[OF division_of_tagged_division[OF assms(1)]])
-    apply(rule_tac[1-2] *) using assms(2-) by auto qed
+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
+  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
+qed
 
 lemma division_split: fixes a::"'a::ordered_euclidean_space"
   assumes "p division_of {a..b}" and k:"k\<in>Basis"