# HG changeset patch
# User wenzelm
# Date 1349343956 -7200
# Node ID f68e237e8c104953eaa16e3cb1da138217c93662
# Parent  ad2bd4e5a029ba9705db7339478babd228018707
tuned proofs;

diff -r ad2bd4e5a029 -r f68e237e8c10 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Oct 04 11:39:24 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Oct 04 11:45:56 2012 +0200
@@ -338,48 +338,72 @@
 
 lemma content_empty[simp]: "content {} = 0" unfolding content_def by auto
 
-lemma content_subset: assumes "{a..b} \<subseteq> {c..d}" shows "content {a..b::'a::ordered_euclidean_space} \<le> content {c..d}" proof(cases "{a..b}={}")
-  case True thus ?thesis using content_pos_le[of c d] by auto next
-  case False hence ab_ne:"\<forall>i<DIM('a). a $$ i \<le> b $$ i" unfolding interval_ne_empty by auto
+lemma content_subset:
+  assumes "{a..b} \<subseteq> {c..d}"
+  shows "content {a..b::'a::ordered_euclidean_space} \<le> content {c..d}"
+proof (cases "{a..b} = {}")
+  case True
+  thus ?thesis using content_pos_le[of c d] by auto
+next
+  case False
+  hence ab_ne:"\<forall>i<DIM('a). a $$ i \<le> b $$ i" unfolding interval_ne_empty by auto
   hence ab_ab:"a\<in>{a..b}" "b\<in>{a..b}" unfolding mem_interval by auto
   have "{c..d} \<noteq> {}" using assms False by auto
   hence cd_ne:"\<forall>i<DIM('a). c $$ i \<le> d $$ i" using assms unfolding interval_ne_empty by auto
-  show ?thesis unfolding content_def unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
-    unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`] apply(rule setprod_mono,rule) proof
-    fix i assume i:"i\<in>{..<DIM('a)}"
+  show ?thesis
+    unfolding content_def
+    unfolding interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
+    unfolding if_not_P[OF False] if_not_P[OF `{c..d} \<noteq> {}`]
+    apply(rule setprod_mono,rule)
+  proof
+    fix i
+    assume i:"i\<in>{..<DIM('a)}"
     show "0 \<le> b $$ i - a $$ i" using ab_ne[THEN spec[where x=i]] i by auto
     show "b $$ i - a $$ i \<le> d $$ i - c $$ i"
       using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(2),of i]
-      using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i] using i by auto qed qed
+      using assms[unfolded subset_eq mem_interval,rule_format,OF ab_ab(1),of i]
+      using i by auto
+  qed
+qed
 
 lemma content_lt_nz: "0 < content {a..b} \<longleftrightarrow> content {a..b} \<noteq> 0"
   unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
 
+
 subsection {* The notion of a gauge --- simply an open set containing the point. *}
 
 definition gauge where "gauge d \<longleftrightarrow> (\<forall>x. x\<in>(d x) \<and> open(d x))"
 
-lemma gaugeI:assumes "\<And>x. x\<in>g x" "\<And>x. open (g x)" shows "gauge g"
+lemma gaugeI: assumes "\<And>x. x\<in>g x" "\<And>x. open (g x)" shows "gauge g"
   using assms unfolding gauge_def by auto
 
-lemma gaugeD[dest]: assumes "gauge d" shows "x\<in>d x" "open (d x)" using assms unfolding gauge_def by auto
+lemma gaugeD[dest]: assumes "gauge d" shows "x\<in>d x" "open (d x)"
+  using assms unfolding gauge_def by auto
 
 lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
   unfolding gauge_def by auto 
 
 lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)" unfolding gauge_def by auto 
 
-lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)" apply(rule gauge_ball) by auto
+lemma gauge_trivial[intro]: "gauge (\<lambda>x. ball x 1)"
+  by (rule gauge_ball) auto
 
 lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. (d1 x) \<inter> (d2 x))"
   unfolding gauge_def by auto 
 
-lemma gauge_inters: assumes "finite s" "\<forall>d\<in>s. gauge (f d)" shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})" proof-
-  have *:"\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s" by auto show ?thesis
-  unfolding gauge_def unfolding * 
-  using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto qed
-
-lemma gauge_existence_lemma: "(\<forall>x. \<exists>d::real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)" by(meson zero_less_one)
+lemma gauge_inters:
+  assumes "finite s" "\<forall>d\<in>s. gauge (f d)"
+  shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})"
+proof -
+  have *:"\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s" by auto
+  show ?thesis
+    unfolding gauge_def unfolding * 
+    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
+qed
+
+lemma gauge_existence_lemma: "(\<forall>x. \<exists>d::real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
+  by(meson zero_less_one)
+
 
 subsection {* Divisions. *}
 
@@ -390,13 +414,15 @@
         (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
         (\<Union>s = i)"
 
-lemma division_ofD[dest]: assumes  "s division_of i"
-  shows"finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
-  "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i" using assms unfolding division_of_def by auto
+lemma division_ofD[dest]:
+  assumes "s division_of i"
+  shows "finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
+    "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i"
+  using assms unfolding division_of_def by auto
 
 lemma division_ofI:
   assumes "finite s" "\<And>k. k\<in>s \<Longrightarrow> k \<subseteq> i" "\<And>k. k\<in>s \<Longrightarrow>  k \<noteq> {}" "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
-  "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i"
+    "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}" "\<Union>s = i"
   shows "s division_of i" using assms unfolding division_of_def by auto
 
 lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
@@ -407,19 +433,30 @@
 
 lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}" unfolding division_of_def by auto 
 
-lemma division_of_sing[simp]: "s division_of {a..a::'a::ordered_euclidean_space} \<longleftrightarrow> s = {{a..a}}" (is "?l = ?r") proof
-  assume ?r moreover { assume "s = {{a}}" moreover fix k assume "k\<in>s" 
-    ultimately have"\<exists>x y. k = {x..y}" apply(rule_tac x=a in exI)+ unfolding interval_sing by auto }
-  ultimately show ?l unfolding division_of_def interval_sing by auto next
-  assume ?l note as=conjunctD4[OF this[unfolded division_of_def interval_sing]]
+lemma division_of_sing[simp]:
+  "s division_of {a..a::'a::ordered_euclidean_space} \<longleftrightarrow> s = {{a..a}}" (is "?l = ?r")
+proof
+  assume ?r
+  moreover {
+    assume "s = {{a}}"
+    moreover fix k assume "k\<in>s" 
+    ultimately have"\<exists>x y. k = {x..y}"
+      apply (rule_tac x=a in exI)+ unfolding interval_sing by auto
+  }
+  ultimately show ?l unfolding division_of_def interval_sing by auto
+next
+  assume ?l
+  note as=conjunctD4[OF this[unfolded division_of_def interval_sing]]
   { fix x assume x:"x\<in>s" have "x={a}" using as(2)[rule_format,OF x] by auto }
-  moreover have "s \<noteq> {}" using as(4) by auto ultimately show ?r unfolding interval_sing by auto qed
+  moreover have "s \<noteq> {}" using as(4) by auto
+  ultimately show ?r unfolding interval_sing by auto
+qed
 
 lemma elementary_empty: obtains p where "p division_of {}"
   unfolding division_of_trivial by auto
 
-lemma elementary_interval: obtains p where  "p division_of {a..b}"
-  by(metis division_of_trivial division_of_self)
+lemma elementary_interval: obtains p where "p division_of {a..b}"
+  by (metis division_of_trivial division_of_self)
 
 lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
   unfolding division_of_def by auto
@@ -429,14 +466,27 @@
   unfolding division_of_def by fastforce
 
 lemma division_of_subset: assumes "p division_of (\<Union>p)" "q \<subseteq> p" shows "q division_of (\<Union>q)"
-  apply(rule division_ofI) proof- note as=division_ofD[OF assms(1)]
-  show "finite q" apply(rule finite_subset) using as(1) assms(2) by auto
-  { fix k assume "k \<in> q" hence kp:"k\<in>p" using assms(2) by auto show "k\<subseteq>\<Union>q" using `k \<in> q` by auto
-  show "\<exists>a b. k = {a..b}" using as(4)[OF kp] by auto show "k \<noteq> {}" using as(3)[OF kp] by auto }
-  fix k1 k2 assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2" hence *:"k1\<in>p" "k2\<in>p" "k1\<noteq>k2" using assms(2) by auto
-  show "interior k1 \<inter> interior k2 = {}" using as(5)[OF *] by auto qed auto
-
-lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)" unfolding division_of_def by auto
+  apply (rule division_ofI)
+proof -
+  note as=division_ofD[OF assms(1)]
+  show "finite q"
+    apply (rule finite_subset)
+    using as(1) assms(2) apply auto
+    done
+  { fix k
+    assume "k \<in> q"
+    hence kp:"k\<in>p" using assms(2) by auto
+    show "k\<subseteq>\<Union>q" using `k \<in> q` by auto
+    show "\<exists>a b. k = {a..b}" using as(4)[OF kp]
+      by auto show "k \<noteq> {}" using as(3)[OF kp] by auto }
+  fix k1 k2
+  assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
+  hence *: "k1\<in>p" "k2\<in>p" "k1\<noteq>k2" using assms(2) by auto
+  show "interior k1 \<inter> interior k2 = {}" using as(5)[OF *] by auto
+qed auto
+
+lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
+  unfolding division_of_def by auto
 
 lemma division_of_content_0: assumes "content {a..b} = 0" "d division_of {a..b}" shows "\<forall>k\<in>d. content k = 0"
   unfolding forall_in_division[OF assms(2)] apply(rule,rule,rule) apply(drule division_ofD(2)[OF assms(2)])