author paulson Thu, 03 Aug 2017 11:29:08 +0200 changeset 66317 a9bb833ee971 parent 66316 2a1739aad711 child 66318 f2e1047d6cc1
more tidying up
```--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Aug 03 10:52:13 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Aug 03 11:29:08 2017 +0200
@@ -12,6 +12,24 @@
imports Interval_Integral
begin

+
+lemma finite_product_dependent: (*FIXME DELETE*)
+  assumes "finite s"
+    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
+  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
+  using assms
+proof induct
+  case (insert x s)
+  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
+    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
+  show ?case
+    unfolding *
+    apply (rule finite_UnI)
+    using insert
+    apply auto
+    done
+qed auto
+
lemma nn_integral_substitution_aux:
fixes f :: "real \<Rightarrow> ennreal"
assumes Mf: "f \<in> borel_measurable borel"```
```--- a/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 03 10:52:13 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 03 11:29:08 2017 +0200
@@ -10,23 +10,6 @@
Topology_Euclidean_Space
begin

-lemma finite_product_dependent: (*FIXME DELETE*)
-  assumes "finite s"
-    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
-  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
-  using assms
-proof induct
-  case (insert x s)
-  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
-    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
-  show ?case
-    unfolding *
-    apply (rule finite_UnI)
-    using insert
-    apply auto
-    done
-qed auto
-
lemma sum_Sigma_product:
assumes "finite S"
and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
@@ -210,18 +193,18 @@

subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>

-definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
+definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"

lemma gaugeI:
-  assumes "\<And>x. x \<in> g x"
-    and "\<And>x. open (g x)"
-  shows "gauge g"
+  assumes "\<And>x. x \<in> \<gamma> x"
+    and "\<And>x. open (\<gamma> x)"
+  shows "gauge \<gamma>"
using assms unfolding gauge_def by auto

lemma gaugeD[dest]:
-  assumes "gauge d"
-  shows "x \<in> d x"
-    and "open (d x)"
+  assumes "gauge \<gamma>"
+  shows "x \<in> \<gamma> x"
+    and "open (\<gamma> 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))"
@@ -233,7 +216,7 @@
lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
by (rule gauge_ball) auto

-lemma gauge_Int[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
+lemma gauge_Int[intro]: "gauge \<gamma>1 \<Longrightarrow> gauge \<gamma>2 \<Longrightarrow> gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
unfolding gauge_def by auto

lemma gauge_reflect:
@@ -244,10 +227,10 @@

lemma gauge_Inter:
assumes "finite S"
-    and "\<And>d. d\<in>S \<Longrightarrow> gauge (f d)"
-  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> S})"
+    and "\<And>u. u\<in>S \<Longrightarrow> gauge (f u)"
+  shows "gauge (\<lambda>x. \<Inter>{f u x | u. u \<in> S})"
proof -
-  have *: "\<And>x. {f d x |d. d \<in> S} = (\<lambda>d. f d x) ` S"
+  have *: "\<And>x. {f u x |u. u \<in> S} = (\<lambda>u. f u x) ` S"
by auto
show ?thesis
unfolding gauge_def unfolding *
@@ -314,18 +297,15 @@
assume "s = {{a}}" "K\<in>s"
then have "\<exists>x y. K = cbox x y"
apply (rule_tac x=a in exI)+
-      apply (force simp: cbox_sing)
+      apply force
done
}
ultimately show ?l
unfolding division_of_def cbox_sing by auto
next
assume ?l
-  {
-    fix x
-    assume x: "x \<in> s" have "x = {a}"
-      by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD x)
-  }
+  have "x = {a}" if  "x \<in> s" for x
+    by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
moreover have "s \<noteq> {}"
using \<open>s division_of cbox a a\<close> by auto
ultimately show ?r
@@ -401,11 +381,8 @@
have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
by auto
show "\<Union>?A = s1 \<inter> s2"
-      apply (rule set_eqI)
-      unfolding * and UN_iff
-      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
-      apply auto
-      done
+      unfolding *
+      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
{
fix k
assume "k \<in> ?A"
@@ -461,14 +438,14 @@
unfolding * by auto
qed

-lemma elementary_inter:
+lemma elementary_Int:
fixes s t :: "'a::euclidean_space set"
assumes "p1 division_of s"
and "p2 division_of t"
shows "\<exists>p. p division_of (s \<inter> t)"
using assms division_inter by blast

-lemma elementary_inters:
+lemma elementary_Inter:
assumes "finite f"
and "f \<noteq> {}"
and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
@@ -488,7 +465,7 @@
moreover obtain px where "px division_of x"
using insert(5)[rule_format,OF insertI1] ..
ultimately show ?thesis
-      by (simp add: elementary_inter Inter_insert)
+      by (simp add: elementary_Int Inter_insert)
qed
qed auto

@@ -665,8 +642,8 @@
then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
by (meson Diff_subset division_of_subset)
have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
-    apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
-    apply (auto dest: di simp: False elementary_inters [OF finite_imageI[OF p(1)]])
+    apply (rule elementary_Inter [OF finite_imageI[OF p(1)]])
+    apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]])
done
then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
have "d \<union> p division_of cbox a b"
@@ -920,7 +897,7 @@
apply auto
done
then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
-    by (metis assms(2) divq(6) elementary_inter)
+    by (metis assms(2) divq(6) elementary_Int)
{
fix x
assume x: "x \<in> T" "x \<notin> S"```