--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Sep 04 17:40:07 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Sep 04 21:25:03 2013 +0200
@@ -156,7 +156,7 @@
assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
(is "?l = ?r")
-proof (safe)
+proof safe
assume ?r
fix n m :: nat
assume "m < n"
@@ -176,14 +176,16 @@
done
next
case False
- then have "m = n" using Suc(2) by auto
- then show ?thesis using `?r` by auto
+ then have "m = n"
+ using Suc(2) by auto
+ then show ?thesis
+ using `?r` by auto
qed
qed
qed auto
lemma transitive_stepwise_gt:
- assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
+ assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
shows "\<forall>n>m. R m n"
proof -
have "\<forall>m. \<forall>n>m. R m n"
@@ -204,7 +206,7 @@
assume ?r
fix m n :: nat
assume "m \<le> n"
- thus "R m n"
+ then show "R m n"
proof (induct n arbitrary: m)
case 0
with assms show ?case by auto
@@ -220,21 +222,25 @@
done
next
case False
- hence "m = Suc n" using Suc(2) by auto
- thus ?thesis using assms(1) by auto
+ then have "m = Suc n"
+ using Suc(2) by auto
+ then show ?thesis
+ using assms(1) by auto
qed
qed
qed auto
lemma transitive_stepwise_le:
- assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
+ assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+ and "\<And>n. R n (Suc n)"
shows "\<forall>n\<ge>m. R m n"
proof -
have "\<forall>m. \<forall>n\<ge>m. R m n"
apply (subst transitive_stepwise_le_eq)
apply (rule assms)
apply (rule assms,assumption,assumption)
- using assms(3) apply auto
+ using assms(3)
+ apply auto
done
then show ?thesis by auto
qed
@@ -242,7 +248,8 @@
subsection {* Some useful lemmas about intervals. *}
-abbreviation One where "One \<equiv> (\<Sum>Basis)::'a::euclidean_space"
+abbreviation One :: "'a::euclidean_space"
+ where "One \<equiv> \<Sum>Basis"
lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}"
by (auto simp: set_eq_iff eucl_le[where 'a='a] intro!: bexI[OF _ SOME_Basis])
@@ -293,31 +300,33 @@
apply auto
done
have lem2: "\<And>x s P. \<exists>x\<in>s. P x \<Longrightarrow> \<exists>x\<in>insert x s. P x" by auto
- have "\<And>f. finite f \<Longrightarrow> (\<forall>t\<in>f. \<exists>a b. t = {a..b}) \<Longrightarrow>
- (\<exists>x. x \<in> s \<inter> interior (\<Union>f)) \<Longrightarrow> (\<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t)"
+ have "\<And>f. finite f \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = {a..b} \<Longrightarrow>
+ \<exists>x. x \<in> s \<inter> interior (\<Union>f) \<Longrightarrow> \<exists>t\<in>f. \<exists>x. \<exists>e>0. ball x e \<subseteq> s \<inter> t"
proof -
case goal1
then show ?case
proof (induct rule: finite_induct)
case empty
- from this(2) guess x ..
+ obtain x where "x \<in> s \<inter> interior (\<Union>{})"
+ using empty(2) ..
then have False
unfolding Union_empty interior_empty by auto
then show ?case by auto
next
case (insert i f)
- guess x using insert(5) .. note x = this
- then guess e
- unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior],rule_format] .. note e=this
- guess a
+ obtain x where x: "x \<in> s \<inter> interior (\<Union>insert i f)"
+ using insert(5) ..
+ then obtain e where e: "0 < e \<and> ball x e \<subseteq> s \<inter> interior (\<Union>insert i f)"
+ unfolding open_contains_ball_eq[OF open_Int[OF assms(2) open_interior], rule_format] ..
+ obtain a where "\<exists>b. i = {a..b}"
using insert(4)[rule_format,OF insertI1] ..
- then guess b .. note ab = this
+ then obtain b where ab: "i = {a..b}" ..
show ?case
- proof (cases "x\<in>i")
+ proof (cases "x \<in> i")
case False
then have "x \<in> UNIV - {a..b}"
unfolding ab by auto
- then guess d
+ then obtain d where "0 < d \<and> ball x d \<subseteq> UNIV - {a..b}"
unfolding open_contains_ball_eq[OF open_Diff[OF open_UNIV closed_interval],rule_format] ..
then have "0 < d" "ball x (min d e) \<subseteq> UNIV - i"
unfolding ab ball_min_Int by auto
@@ -335,7 +344,8 @@
case True show ?thesis
proof (cases "x\<in>{a<..<b}")
case True
- then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
+ then obtain d where "0 < d \<and> ball x d \<subseteq> {a<..<b}"
+ unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
then show ?thesis
apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
unfolding ab
@@ -405,10 +415,12 @@
have "ball ?z (e / 2) \<inter> i = {}"
apply (rule ccontr)
unfolding ex_in_conv[symmetric]
- proof (erule exE)
+ apply (erule exE)
+ proof -
fix y
assume "y \<in> ball ?z (e / 2) \<inter> i"
- then have "dist ?z y < e/2" and yi: "y\<in>i" by auto
+ then have "dist ?z y < e/2" and yi: "y \<in> i"
+ by auto
then have "\<bar>(?z - y) \<bullet> k\<bar> < e/2"
using Basis_le_norm[OF k, of "?z - y"]
unfolding dist_norm by auto
@@ -445,9 +457,9 @@
apply auto
done
qed
- then guess x ..
+ then obtain x where "ball x (e / 2) \<subseteq> s \<inter> \<Union>f" ..
then have "x \<in> s \<inter> interior (\<Union>f)"
- unfolding lem1[where U="\<Union>f",symmetric]
+ unfolding lem1[where U="\<Union>f", symmetric]
using centre_in_ball e[THEN conjunct1] by auto
then show ?thesis
apply -
@@ -459,15 +471,12 @@
qed
qed
qed
- note * = this
- guess t using *[OF assms(1,3) goal1] ..
- from this(2) guess x ..
- then guess e ..
- then have "x \<in> s" "x\<in>interior t"
- defer
+ from this[OF assms(1,3) goal1]
+ obtain t x e where "t \<in> f" "0 < e" "ball x e \<subseteq> s \<inter> t"
+ by blast
+ then have "x \<in> s" "x \<in> interior t"
using open_subset_interior[OF open_ball, of x e t]
- apply auto
- done
+ by auto
then show False
using `t \<in> f` assms(4) by auto
qed
@@ -530,14 +539,8 @@
apply assumption
done
-lemma content_real:
- assumes "a \<le> b"
- shows "content {a..b} = b - a"
-proof -
- have *: "{..<Suc 0} = {0}" by auto
- show ?thesis
- unfolding content_def using assms by (auto simp: *)
-qed
+lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
+ unfolding content_def by auto
lemma content_singleton[simp]: "content {a} = 0"
proof -
@@ -548,8 +551,10 @@
lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1"
proof -
- have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i" by auto
- have "0 \<in> {0..One::'a}" unfolding mem_interval by auto
+ have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
+ by auto
+ have "0 \<in> {0..One::'a}"
+ unfolding mem_interval by auto
then show ?thesis
unfolding content_def interval_bounds[OF *] using setprod_1 by auto
qed
@@ -568,10 +573,12 @@
apply (erule_tac x=x in ballE)
apply auto
done
- then show ?thesis unfolding content_def by (auto simp del:interval_bounds')
+ then show ?thesis
+ unfolding content_def by (auto simp del:interval_bounds')
next
case True
- then show ?thesis unfolding content_def by auto
+ then show ?thesis
+ unfolding content_def by auto
qed
lemma content_pos_lt:
@@ -580,10 +587,12 @@
shows "0 < content {a..b}"
proof -
have help_lemma1: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> \<forall>i\<in>Basis. a\<bullet>i \<le> ((b\<bullet>i)::real)"
- apply (rule, erule_tac x=i in ballE)
+ apply rule
+ apply (erule_tac x=i in ballE)
apply auto
done
- show ?thesis unfolding content_closed_interval[OF help_lemma1[OF assms]]
+ show ?thesis
+ unfolding content_closed_interval[OF help_lemma1[OF assms]]
apply (rule setprod_pos)
using assms
apply (erule_tac x=x in ballE)
@@ -591,7 +600,8 @@
done
qed
-lemma content_eq_0: "content{a..b::'a::ordered_euclidean_space} = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
+lemma content_eq_0:
+ "content{a..b::'a::ordered_euclidean_space} = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
proof (cases "{a..b} = {}")
case True
then show ?thesis
@@ -604,15 +614,15 @@
done
next
case False
- from this[unfolded interval_eq_empty not_ex not_less]
- have as: "\<forall>i\<in>Basis. b \<bullet> i \<ge> a \<bullet> i" by fastforce
- show ?thesis
+ then have "\<forall>i\<in>Basis. b \<bullet> i \<ge> a \<bullet> i"
+ unfolding interval_eq_empty not_ex not_less
+ by fastforce
+ then show ?thesis
unfolding content_def if_not_P[OF False] setprod_zero_iff[OF finite_Basis]
- using as
by (auto intro!: bexI)
qed
-lemma cond_cases:"(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
+lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
by auto
lemma content_closed_interval_cases:
@@ -621,7 +631,8 @@
by (auto simp: not_le content_eq_0 intro: less_imp_le content_closed_interval)
lemma content_eq_0_interior: "content {a..b} = 0 \<longleftrightarrow> interior({a..b}) = {}"
- unfolding content_eq_0 interior_closed_interval interval_eq_empty by auto
+ unfolding content_eq_0 interior_closed_interval interval_eq_empty
+ by auto
lemma content_pos_lt_eq:
"0 < content {a..b::'a::ordered_euclidean_space} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
@@ -658,7 +669,8 @@
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)
+ apply (rule setprod_mono)
+ apply rule
proof
fix i :: 'a
assume i: "i \<in> Basis"
@@ -677,7 +689,7 @@
subsection {* The notion of a gauge --- simply an open set containing the point. *}
-definition "gauge d \<longleftrightarrow> (\<forall>x. x\<in>(d x) \<and> open (d x))"
+definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
lemma gaugeI:
assumes "\<And>x. x \<in> g x"
@@ -700,13 +712,13 @@
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))"
+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"
and "\<forall>d\<in>s. gauge (f d)"
- shows "gauge(\<lambda>x. \<Inter> {f d x | d. d \<in> s})"
+ 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
@@ -716,13 +728,14 @@
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)"
+ "(\<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 (metis zero_less_one)
subsection {* Divisions. *}
-definition division_of (infixl "division'_of" 40) where
+definition division_of (infixl "division'_of" 40)
+where
"s division_of i \<longleftrightarrow>
finite s \<and>
(\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = {a..b})) \<and>
@@ -731,15 +744,20 @@
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"
+ shows "finite s"
+ and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
+ and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
+ and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
+ and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
+ and "\<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 "\<And>k. k\<in>s \<Longrightarrow> k \<noteq> {}"
- and "\<And>k. k\<in>s \<Longrightarrow> (\<exists>a b. k = {a..b})"
- and "\<And>k1 k2. \<lbrakk>k1\<in>s; k2\<in>s; k1 \<noteq> k2\<rbrakk> \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
+ assumes "finite s"
+ and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
+ and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
+ and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
+ and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
and "\<Union>s = i"
shows "s division_of i"
using assms unfolding division_of_def by auto
@@ -772,14 +790,16 @@
unfolding division_of_def interval_sing by auto
next
assume ?l
- note as=conjunctD4[OF this[unfolded division_of_def interval_sing]]
+ note * = 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
+ using *(2)[rule_format,OF x] by auto
}
- moreover have "s \<noteq> {}" using as(4) by auto
- ultimately show ?r unfolding interval_sing by auto
+ moreover have "s \<noteq> {}"
+ using *(4) by auto
+ ultimately show ?r
+ unfolding interval_sing by auto
qed
lemma elementary_empty: obtains p where "p division_of {}"
@@ -792,34 +812,38 @@
unfolding division_of_def by auto
lemma forall_in_division:
- "d division_of i \<Longrightarrow> ((\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. {a..b} \<in> d \<longrightarrow> P {a..b}))"
+ "d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. {a..b} \<in> d \<longrightarrow> P {a..b})"
unfolding division_of_def by fastforce
lemma division_of_subset:
assumes "p division_of (\<Union>p)"
and "q \<subseteq> p"
shows "q division_of (\<Union>q)"
- apply (rule division_ofI)
-proof -
- note as=division_ofD[OF assms(1)]
+proof (rule division_ofI)
+ note * = division_ofD[OF assms(1)]
show "finite q"
apply (rule finite_subset)
- using as(1) assms(2) apply auto
+ using *(1) assms(2)
+ apply auto
done
{
fix k
assume "k \<in> q"
- then have 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
+ then have 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 *(4)[OF kp] by auto
+ show "k \<noteq> {}"
+ using *(3)[OF kp] by auto
}
fix k1 k2
assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
- then have *: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
+ then have **: "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
+ using *(5)[OF **] by auto
qed auto
lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
@@ -838,12 +862,14 @@
qed
lemma division_inter:
- assumes "p1 division_of s1" "p2 division_of (s2::('a::ordered_euclidean_space) set)"
+ fixes s1 s2 :: "'a::ordered_euclidean_space set"
+ assumes "p1 division_of s1"
+ and "p2 division_of s2"
shows "{k1 \<inter> k2 | k1 k2 .k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
(is "?A' division_of _")
proof -
let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
- have *:"?A' = ?A" by auto
+ have *: "?A' = ?A" by auto
show ?thesis
unfolding *
proof (rule division_ofI)
@@ -863,30 +889,34 @@
{
fix k
assume "k \<in> ?A"
- then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}"
+ then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
by auto
- then show "k \<noteq> {}" by auto
+ then show "k \<noteq> {}"
+ by auto
show "k \<subseteq> s1 \<inter> s2"
using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
unfolding k by auto
- guess a1 using division_ofD(4)[OF assms(1) k(2)] ..
- then guess b1 .. note ab1=this
- guess a2 using division_ofD(4)[OF assms(2) k(3)] ..
- then guess b2 .. note ab2=this
+ obtain a1 b1 where k1: "k1 = {a1..b1}"
+ using division_ofD(4)[OF assms(1) k(2)] by blast
+ obtain a2 b2 where k2: "k2 = {a2..b2}"
+ using division_ofD(4)[OF assms(2) k(3)] by blast
show "\<exists>a b. k = {a..b}"
- unfolding k ab1 ab2 unfolding inter_interval by auto }
+ unfolding k k1 k2 unfolding inter_interval by auto
+ }
fix k1 k2
- assume "k1\<in>?A"
- then obtain x1 y1 where k1:"k1 = x1 \<inter> y1" "x1\<in>p1" "y1\<in>p2" "k1\<noteq>{}" by auto
- assume "k2\<in>?A"
- then obtain x2 y2 where k2:"k2 = x2 \<inter> y2" "x2\<in>p1" "y2\<in>p2" "k2\<noteq>{}" by auto
+ assume "k1 \<in> ?A"
+ then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
+ by auto
+ assume "k2 \<in> ?A"
+ then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
+ by auto
assume "k1 \<noteq> k2"
then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
unfolding k1 k2 by auto
- have *: "(interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {}) \<Longrightarrow>
- interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
- interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
- \<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
+ have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
+ interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
+ interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
+ interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
show "interior k1 \<inter> interior k2 = {}"
unfolding k1 k2
apply (rule *)
@@ -894,14 +924,16 @@
apply (rule_tac[1-4] interior_mono)
using division_ofD(5)[OF assms(1) k1(2) k2(2)]
using division_ofD(5)[OF assms(2) k1(3) k2(3)]
- using th apply auto
+ using th
+ apply auto
done
qed
qed
lemma division_inter_1:
- assumes "d division_of i" "{a..b::'a::ordered_euclidean_space} \<subseteq> i"
- shows "{ {a..b} \<inter> k |k. k \<in> d \<and> {a..b} \<inter> k \<noteq> {} } division_of {a..b}"
+ assumes "d division_of i"
+ and "{a..b::'a::ordered_euclidean_space} \<subseteq> i"
+ shows "{{a..b} \<inter> k | k. k \<in> d \<and> {a..b} \<inter> k \<noteq> {}} division_of {a..b}"
proof (cases "{a..b} = {}")
case True
show ?thesis
@@ -915,14 +947,18 @@
qed
lemma elementary_inter:
- assumes "p1 division_of s" "p2 division_of (t::('a::ordered_euclidean_space) set)"
+ fixes s t :: "'a::ordered_euclidean_space set"
+ assumes "p1 division_of s"
+ and "p2 division_of t"
shows "\<exists>p. p division_of (s \<inter> t)"
apply rule
apply (rule division_inter[OF assms])
done
lemma elementary_inters:
- assumes "finite f" "f\<noteq>{}" "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)"
+ assumes "finite f"
+ and "f \<noteq> {}"
+ and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::ordered_euclidean_space) set)"
shows "\<exists>p. p division_of (\<Inter> f)"
using assms
proof (induct f rule: finite_induct)
@@ -934,11 +970,14 @@
unfolding True using insert by auto
next
case False
- guess p using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
- moreover guess px using insert(5)[rule_format,OF insertI1] ..
+ obtain p where "p division_of \<Inter>f"
+ using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
+ moreover obtain px where "px division_of x"
+ using insert(5)[rule_format,OF insertI1] ..
ultimately show ?thesis
+ apply -
unfolding Inter_insert
- apply (rule_tac elementary_inter)
+ apply (rule elementary_inter)
apply assumption
apply assumption
done
@@ -946,12 +985,17 @@
qed auto
lemma division_disjoint_union:
- assumes "p1 division_of s1" "p2 division_of s2" "interior s1 \<inter> interior s2 = {}"
+ assumes "p1 division_of s1"
+ and "p2 division_of s2"
+ and "interior s1 \<inter> interior s2 = {}"
shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
proof (rule division_ofI)
- note d1 = division_ofD[OF assms(1)] and d2 = division_ofD[OF assms(2)]
- show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
- show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
+ note d1 = division_ofD[OF assms(1)]
+ note d2 = division_ofD[OF assms(2)]
+ show "finite (p1 \<union> p2)"
+ using d1(1) d2(1) by auto
+ show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
+ using d1(6) d2(6) by auto
{
fix k1 k2
assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
@@ -975,17 +1019,22 @@
}
fix k
assume k: "k \<in> p1 \<union> p2"
- show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
- show "k \<noteq> {}" using k d1(3) d2(3) by auto
- show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto
+ show "k \<subseteq> s1 \<union> s2"
+ using k d1(2) d2(2) by auto
+ show "k \<noteq> {}"
+ using k d1(3) d2(3) by auto
+ show "\<exists>a b. k = {a..b}"
+ using k d1(4) d2(4) by auto
qed
lemma partial_division_extend_1:
- assumes incl: "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}"
+ fixes a b c d :: "'a::ordered_euclidean_space"
+ assumes incl: "{c..d} \<subseteq> {a..b}"
and nonempty: "{c..d} \<noteq> {}"
obtains p where "p division_of {a..b}" "{c..d} \<in> p"
proof
- let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a. {(\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)}"
+ let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
+ {(\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)}"
def p \<equiv> "?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
show "{c .. d} \<in> p"
@@ -1009,7 +1058,8 @@
assume "k \<in> p"
then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
by (auto simp: p_def)
- then show "\<exists>a b. k = {a..b}" by auto
+ then show "\<exists>a b. k = {a..b}"
+ by auto
have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
proof (simp add: k interval_eq_empty subset_interval not_less, safe)
fix i :: 'a
@@ -1020,36 +1070,38 @@
show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
by (auto simp: subset_iff eucl_le[where 'a='a])
qed
- then show "k \<noteq> {}" "k \<subseteq> {a .. b}" by auto
+ then show "k \<noteq> {}" "k \<subseteq> {a .. b}"
+ by auto
{
- fix l assume "l \<in> p"
+ fix l
+ assume "l \<in> p"
then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
by (auto simp: p_def)
assume "l \<noteq> k"
have "\<exists>i\<in>Basis. f i \<noteq> g i"
proof (rule ccontr)
- assume "\<not> (\<exists>i\<in>Basis. f i \<noteq> g i)"
+ assume "\<not> ?thesis"
with f g have "f = g"
by (auto simp: PiE_iff extensional_def intro!: ext)
with `l \<noteq> k` show False
by (simp add: l k)
qed
- then guess i .. note * = this
- moreover from * have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
+ then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
+ then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
"g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
using f g by (auto simp: PiE_iff)
- moreover note ord[of i]
- ultimately show "interior l \<inter> interior k = {}"
+ with * ord[of i] show "interior l \<inter> interior k = {}"
by (auto simp add: l k interior_closed_interval disjoint_interval intro!: bexI[of _ i])
}
- note `k \<subseteq> { a.. b}`
+ note `k \<subseteq> {a.. b}`
}
moreover
{
fix x assume x: "x \<in> {a .. b}"
have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
proof
- fix i :: 'a assume "i \<in> Basis"
+ fix i :: 'a
+ assume "i \<in> Basis"
with x ord[of i]
have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
(d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
@@ -1057,13 +1109,16 @@
then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
by auto
qed
- then guess f unfolding bchoice_iff .. note f = this
+ then obtain f where
+ f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
+ unfolding bchoice_iff ..
moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
by auto
moreover from f have "x \<in> ?B (restrict f Basis)"
by (auto simp: mem_interval eucl_le[where 'a='a])
ultimately have "\<exists>k\<in>p. x \<in> k"
- unfolding p_def by blast }
+ unfolding p_def by blast
+ }
ultimately show "\<Union>p = {a..b}"
by auto
qed
@@ -1074,7 +1129,8 @@
obtains q where "p \<subseteq> q" "q division_of {a..b::'a::ordered_euclidean_space}"
proof (cases "p = {}")
case True
- guess q apply (rule elementary_interval[of a b]) .
+ obtain q where "q division_of {a..b}"
+ by (rule elementary_interval)
then show ?thesis
apply -
apply (rule that[of q])
@@ -1084,29 +1140,34 @@
next
case False
note p = division_ofD[OF assms(1)]
- have *: "\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q"
+ have *: "\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k \<in> q"
proof
case goal1
- guess c using p(4)[OF goal1] ..
- then guess d .. note "cd" = this
+ obtain c d where k: "k = {c..d}"
+ using p(4)[OF goal1] by blast
have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
- using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
- guess q apply(rule partial_division_extend_1[OF *]) .
- then show ?case unfolding "cd" by auto
+ using p(2,3)[OF goal1, unfolded k] using assms(2) by auto
+ obtain q where "q division_of {a..b}" "{c..d} \<in> q"
+ by (rule partial_division_extend_1[OF *])
+ then show ?case
+ unfolding k by auto
qed
- guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
- have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
- apply (rule, rule_tac p="q x" in division_of_subset)
+ obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of {a..b}" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
+ using bchoice[OF *] by blast
+ have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
+ apply rule
+ apply (rule_tac p="q x" in division_of_subset)
proof -
fix x
- assume x: "x\<in>p"
+ assume x: "x \<in> p"
show "q x division_of \<Union>q x"
apply -
apply (rule division_ofI)
using division_ofD[OF q(1)[OF x]]
apply auto
done
- show "q x - {x} \<subseteq> q x" by auto
+ show "q x - {x} \<subseteq> q x"
+ by auto
qed
then have "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
apply -
@@ -1116,16 +1177,16 @@
apply (rule False)
apply auto
done
- then guess d .. note d = this
+ then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
show ?thesis
apply (rule that[of "d \<union> p"])
proof -
- have *: "\<And>s f t. s \<noteq> {} \<Longrightarrow> (\<forall>i\<in>s. f i \<union> i = t) \<Longrightarrow> t = \<Inter> (f ` s) \<union> (\<Union>s)" by auto
- have *: "{a..b} = \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
+ have *: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
+ have *: "{a..b} = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
apply (rule *[OF False])
proof
fix i
- assume i: "i\<in>p"
+ assume i: "i \<in> p"
show "\<Union>(q i - {i}) \<union> i = {a..b}"
using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
qed
@@ -1134,10 +1195,12 @@
apply (rule division_disjoint_union[OF d assms(1)])
apply (rule inter_interior_unions_intervals)
apply (rule p open_interior ballI)+
- proof (assumption, rule)
+ apply assumption
+ proof
fix k
- assume k: "k\<in>p"
- have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
+ assume k: "k \<in> p"
+ have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}"
+ by auto
show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<inter> interior k = {}"
apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
defer
@@ -1145,29 +1208,34 @@
apply (rule inter_interior_unions_intervals)
proof -
note qk=division_ofD[OF q(1)[OF k]]
- show "finite (q k - {k})" "open (interior k)"
- "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
+ show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}"
+ using qk by auto
show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
using qk(5) using q(2)[OF k] by auto
- have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto
+ have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x"
+ by auto
show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<subseteq> interior (\<Union>(q k - {k}))"
apply (rule interior_mono *)+
- using k by auto
+ using k
+ apply auto
+ done
qed
qed
qed auto
qed
lemma elementary_bounded[dest]:
- "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
- unfolding division_of_def by(metis bounded_Union bounded_interval)
+ fixes s :: "'a::ordered_euclidean_space set"
+ shows "p division_of s \<Longrightarrow> bounded s"
+ unfolding division_of_def by (metis bounded_Union bounded_interval)
lemma elementary_subset_interval:
"p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> {a..b::'a::ordered_euclidean_space}"
by (meson elementary_bounded bounded_subset_closed_interval)
lemma division_union_intervals_exists:
- assumes "{a..b::'a::ordered_euclidean_space} \<noteq> {}"
+ fixes a b :: "'a::ordered_euclidean_space"
+ assumes "{a..b} \<noteq> {}"
obtains p where "(insert {a..b} p) division_of ({a..b} \<union> {c..d})"
proof (cases "{c..d} = {}")
case True
@@ -1179,16 +1247,15 @@
done
next
case False
- note false=this
show ?thesis
proof (cases "{a..b} \<inter> {c..d} = {}")
case True
- have *:"\<And>a b. {a,b} = {a} \<union> {b}" by auto
+ have *: "\<And>a b. {a, b} = {a} \<union> {b}" by auto
show ?thesis
apply (rule that[of "{{c..d}}"])
unfolding *
apply (rule division_disjoint_union)
- using false True assms
+ using `{c..d} \<noteq> {}` True assms
using interior_subset
apply auto
done
@@ -1197,8 +1264,9 @@
obtain u v where uv: "{a..b} \<inter> {c..d} = {u..v}"
unfolding inter_interval by auto
have *: "{u..v} \<subseteq> {c..d}" using uv by auto
- guess p apply (rule partial_division_extend_1[OF * False[unfolded uv]]) .
- note p=this division_ofD[OF this(1)]
+ obtain p where "p division_of {c..d}" "{u..v} \<in> p"
+ by (rule partial_division_extend_1[OF * False[unfolded uv]])
+ note p = this division_ofD[OF this(1)]
have *: "{a..b} \<union> {c..d} = {a..b} \<union> \<Union>(p - {{u..v}})" "\<And>x s. insert x s = {x} \<union> s"
using p(8) unfolding uv[symmetric] by auto
show ?thesis
@@ -1232,7 +1300,7 @@
lemma division_of_unions:
assumes "finite f"
- and "\<And>p. p\<in>f \<Longrightarrow> p division_of (\<Union>p)"
+ and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
shows "\<Union>f division_of \<Union>\<Union>f"
apply (rule division_ofI)
@@ -1247,11 +1315,12 @@
done
lemma elementary_union_interval:
+ fixes a b :: "'a::ordered_euclidean_space"
assumes "p division_of \<Union>p"
- obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)"
+ obtains q where "q division_of ({a..b} \<union> \<Union>p)"
proof -
note assm = division_ofD[OF assms]
- have lem1: "\<And>f s. \<Union>\<Union> (f ` s) = \<Union>((\<lambda>x.\<Union>(f x)) ` s)"
+ have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
by auto
have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
by auto
@@ -1263,9 +1332,11 @@
then show thesis by auto
next
assume as: "p = {}"
- guess p by (rule elementary_interval[of a b])
+ obtain p where "p division_of {a..b}"
+ by (rule elementary_interval)
then show thesis
- apply (rule_tac that[of p])
+ apply -
+ apply (rule that[of p])
unfolding as
apply auto
done
@@ -1292,18 +1363,20 @@
have "\<forall>k\<in>p. \<exists>q. (insert {a..b} q) division_of ({a..b} \<union> k)"
proof
case goal1
- from assm(4)[OF this] guess c .. then guess d ..
+ from assm(4)[OF this] obtain c d where "k = {c..d}" by blast
then show ?case
apply -
- apply (rule division_union_intervals_exists[OF as(3),of c d])
+ apply (rule division_union_intervals_exists[OF as(3), of c d])
apply auto
done
qed
- from bchoice[OF this] guess q .. note q=division_ofD[OF this[rule_format]]
+ from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert {a..b} (q x) division_of {a..b} \<union> x" ..
+ note q = division_ofD[OF this[rule_format]]
let ?D = "\<Union>{insert {a..b} (q k) | k. k \<in> p}"
show thesis
apply (rule that[of "?D"])
- proof (rule division_ofI)
+ apply (rule division_ofI)
+ proof -
have *: "{insert {a..b} (q k) |k. k \<in> p} = (\<lambda>k. insert {a..b} (q k)) ` p"
by auto
show "finite ?D"
@@ -1315,18 +1388,21 @@
done
show "\<Union>?D = {a..b} \<union> \<Union>p"
unfolding * lem1
- unfolding lem2[OF as(1), of "{a..b}",symmetric]
+ unfolding lem2[OF as(1), of "{a..b}", symmetric]
using q(6)
by auto
fix k
- assume k: "k\<in>?D"
- then show "k \<subseteq> {a..b} \<union> \<Union>p" using q(2) by auto
+ assume k: "k \<in> ?D"
+ then show "k \<subseteq> {a..b} \<union> \<Union>p"
+ using q(2) by auto
show "k \<noteq> {}"
- using q(3) k by auto show "\<exists>a b. k = {a..b}" using q(4) k by auto
+ using q(3) k by auto
+ show "\<exists>a b. k = {a..b}"
+ using q(4) k by auto
fix k'
- assume k': "k'\<in>?D" "k\<noteq>k'"
- obtain x where x: "k \<in>insert {a..b} (q x)" "x\<in>p"
- using k by auto
+ assume k': "k' \<in> ?D" "k \<noteq> k'"
+ obtain x where x: "k \<in> insert {a..b} (q x)" "x\<in>p"
+ using k by auto
obtain x' where x': "k'\<in>insert {a..b} (q x')" "x'\<in>p"
using k' by auto
show "interior k \<inter> interior k' = {}"
@@ -1348,7 +1424,11 @@
next
assume as': "k = {a..b}"
show ?thesis
- apply (rule q(5)) using x' k'(2) unfolding as' by auto
+ apply (rule q(5))
+ using x' k'(2)
+ unfolding as'
+ apply auto
+ done
next
assume as': "k' = {a..b}"
show ?thesis
@@ -1359,21 +1439,22 @@
done
}
assume as': "k \<noteq> {a..b}" "k' \<noteq> {a..b}"
- guess c using q(4)[OF x(2,1)] ..
- then guess d .. note c_d=this
- have "interior k \<inter> interior {a..b} = {}"
- apply(rule q(5))
- using x k'(2)
+ obtain c d where k: "k = {c..d}"
+ using q(4)[OF x(2,1)] by blast
+ have "interior k \<inter> interior {a..b} = {}"
+ apply (rule q(5))
+ using x k'(2)
using as'
apply auto
done
then have "interior k \<subseteq> interior x"
apply -
- apply (rule interior_subset_union_intervals[OF c_d _ as(2) q(2)[OF x(2,1)]])
+ apply (rule interior_subset_union_intervals[OF k _ as(2) q(2)[OF x(2,1)]])
apply auto
done
moreover
- guess c using q(4)[OF x'(2,1)] .. then guess d .. note c_d=this
+ obtain c d where c_d: "k' = {c..d}"
+ using q(4)[OF x'(2,1)] by blast
have "interior k' \<inter> interior {a..b} = {}"
apply (rule q(5))
using x' k'(2)
@@ -1403,14 +1484,14 @@
next
fix x F
assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
- from this(3) guess p .. note p=this
- from assms(2)[OF as(4)] guess a .. then guess b .. note ab=this
+ from this(3) obtain p where p: "p division_of \<Union>F" ..
+ from assms(2)[OF as(4)] obtain a b where x: "x = {a..b}" by blast
have *: "\<Union>F = \<Union>p"
using division_ofD[OF p] by auto
show "\<exists>p. p division_of \<Union>insert x F"
using elementary_union_interval[OF p[unfolded *], of a b]
- unfolding Union_insert ab * by auto
- qed(insert assms, auto)
+ unfolding Union_insert x * by auto
+ qed (insert assms, auto)
then show ?thesis
apply -
apply (erule exE)
@@ -1420,8 +1501,9 @@
qed
lemma elementary_union:
+ fixes s t :: "'a::ordered_euclidean_space set"
assumes "ps division_of s"
- and "pt division_of (t::('a::ordered_euclidean_space) set)"
+ and "pt division_of t"
obtains p where "p division_of (s \<union> t)"
proof -
have "s \<union> t = \<Union>ps \<union> \<Union>pt"
@@ -1429,7 +1511,7 @@
then have *: "\<Union>(ps \<union> pt) = s \<union> t" by auto
show ?thesis
apply -
- apply (rule elementary_unions_intervals[of "ps\<union>pt"])
+ apply (rule elementary_unions_intervals[of "ps \<union> pt"])
unfolding *
prefer 3
apply (rule_tac p=p in that)
@@ -1448,14 +1530,15 @@
note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
obtain a b where ab: "t \<subseteq> {a..b}"
using elementary_subset_interval[OF assms(2)] by auto
- guess r1
+ obtain r1 where "p \<subseteq> r1" "r1 division_of {a..b}"
apply (rule partial_division_extend_interval)
apply (rule assms(1)[unfolded divp(6)[symmetric]])
apply (rule subset_trans)
apply (rule ab assms[unfolded divp(6)[symmetric]])+
+ apply assumption
done
note r1 = this division_ofD[OF this(2)]
- guess p'
+ obtain p' where "p' division_of \<Union>(r1 - p)"
apply (rule elementary_unions_intervals[of "r1 - p"])
using r1(3,6)
apply auto
@@ -1470,7 +1553,8 @@
assume x: "x \<in> t" "x \<notin> s"
then have "x\<in>\<Union>r1"
unfolding r1 using ab by auto
- then guess r unfolding Union_iff .. note r=this
+ then obtain r where r: "r \<in> r1" "x \<in> r"
+ unfolding Union_iff ..
moreover
have "r \<notin> p"
proof
@@ -1492,7 +1576,7 @@
proof -
have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
proof (rule inter_interior_unions_intervals)
- show "finite (r1 - p)" and "open (interior s)" "\<forall>t\<in>r1-p. \<exists>a b. t = {a..b}"
+ show "finite (r1 - p)" and "open (interior s)" and "\<forall>t\<in>r1-p. \<exists>a b. t = {a..b}"
using r1 by auto
have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
by auto
@@ -1523,157 +1607,302 @@
subsection {* Tagged (partial) divisions. *}
-definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40) where
- "(s tagged_partial_division_of i) \<equiv>
- finite s \<and>
- (\<forall>x k. (x,k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and>
- (\<forall>x1 k1 x2 k2. (x1,k1) \<in> s \<and> (x2,k2) \<in> s \<and> ((x1,k1) \<noteq> (x2,k2))
- \<longrightarrow> (interior(k1) \<inter> interior(k2) = {}))"
-
-lemma tagged_partial_division_ofD[dest]: assumes "s tagged_partial_division_of i"
- shows "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
- "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
- "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> (x1,k1) \<noteq> (x2,k2) \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
- using assms unfolding tagged_partial_division_of_def apply- by blast+
-
-definition tagged_division_of (infixr "tagged'_division'_of" 40) where
- "(s tagged_division_of i) \<equiv>
- (s tagged_partial_division_of i) \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
+ where "s tagged_partial_division_of i \<longleftrightarrow>
+ finite s \<and>
+ (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and>
+ (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
+ interior k1 \<inter> interior k2 = {})"
+
+lemma tagged_partial_division_ofD[dest]:
+ assumes "s tagged_partial_division_of i"
+ shows "finite s"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
+ and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow>
+ (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
+ using assms unfolding tagged_partial_division_of_def by blast+
+
+definition tagged_division_of (infixr "tagged'_division'_of" 40)
+ where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
lemma tagged_division_of:
- "(s tagged_division_of i) \<longleftrightarrow>
- finite s \<and>
- (\<forall>x k. (x,k) \<in> s
- \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and>
- (\<forall>x1 k1 x2 k2. (x1,k1) \<in> s \<and> (x2,k2) \<in> s \<and> ~((x1,k1) = (x2,k2))
- \<longrightarrow> (interior(k1) \<inter> interior(k2) = {})) \<and>
- (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+ "s tagged_division_of i \<longleftrightarrow>
+ finite s \<and>
+ (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = {a..b})) \<and>
+ (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
+ interior k1 \<inter> interior k2 = {}) \<and>
+ (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
unfolding tagged_division_of_def tagged_partial_division_of_def by auto
-lemma tagged_division_ofI: assumes
- "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i" "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
- "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})"
- "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+lemma tagged_division_ofI:
+ assumes "finite s"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
+ and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
+ interior k1 \<inter> interior k2 = {}"
+ and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
shows "s tagged_division_of i"
- unfolding tagged_division_of apply(rule) defer apply rule
- apply(rule allI impI conjI assms)+ apply assumption
- apply(rule, rule assms, assumption) apply(rule assms, assumption)
- using assms(1,5-) apply- by blast+
-
-lemma tagged_division_ofD[dest]: assumes "s tagged_division_of i"
- shows "finite s" "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k" "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i" "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
- "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2,k2) \<in> s \<Longrightarrow> ~((x1,k1) = (x2,k2)) \<Longrightarrow> (interior(k1) \<inter> interior(k2) = {})"
- "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)" using assms unfolding tagged_division_of apply- by blast+
-
-lemma division_of_tagged_division: assumes"s tagged_division_of i" shows "(snd ` s) division_of i"
-proof(rule division_ofI) note assm=tagged_division_ofD[OF assms]
- show "\<Union>(snd ` s) = i" "finite (snd ` s)" using assm by auto
- fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
- thus "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastforce+
- fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
- thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
+ unfolding tagged_division_of
+ apply rule
+ defer
+ apply rule
+ apply (rule allI impI conjI assms)+
+ apply assumption
+ apply rule
+ apply (rule assms)
+ apply assumption
+ apply (rule assms)
+ apply assumption
+ using assms(1,5-)
+ apply blast+
+ done
+
+lemma tagged_division_ofD[dest]:
+ assumes "s tagged_division_of i"
+ shows "finite s"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
+ and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = {a..b}"
+ and "\<And>x1 k1 x2 k2. (x1, k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
+ interior k1 \<inter> interior k2 = {}"
+ and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
+ using assms unfolding tagged_division_of by blast+
+
+lemma division_of_tagged_division:
+ assumes "s tagged_division_of i"
+ shows "(snd ` s) division_of i"
+proof (rule division_ofI)
+ note assm = tagged_division_ofD[OF assms]
+ show "\<Union>(snd ` s) = i" "finite (snd ` s)"
+ using assm by auto
+ fix k
+ assume k: "k \<in> snd ` s"
+ then obtain xk where xk: "(xk, k) \<in> s"
+ by auto
+ then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}"
+ using assm by fastforce+
+ fix k'
+ assume k': "k' \<in> snd ` s" "k \<noteq> k'"
+ from this(1) obtain xk' where xk': "(xk', k') \<in> s"
+ by auto
+ then show "interior k \<inter> interior k' = {}"
+ apply -
+ apply (rule assm(5))
+ apply (rule xk xk')+
+ using k'
+ apply auto
+ done
qed
-lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i"
+lemma partial_division_of_tagged_division:
+ assumes "s tagged_partial_division_of i"
shows "(snd ` s) division_of \<Union>(snd ` s)"
-proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms]
- show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)" using assm by auto
- fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
- thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>(snd ` s)" using assm by auto
- fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
- thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
+proof (rule division_ofI)
+ note assm = tagged_partial_division_ofD[OF assms]
+ show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
+ using assm by auto
+ fix k
+ assume k: "k \<in> snd ` s"
+ then obtain xk where xk: "(xk, k) \<in> s"
+ by auto
+ then show "k \<noteq> {}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>(snd ` s)"
+ using assm by auto
+ fix k'
+ assume k': "k' \<in> snd ` s" "k \<noteq> k'"
+ from this(1) obtain xk' where xk': "(xk', k') \<in> s"
+ by auto
+ then show "interior k \<inter> interior k' = {}"
+ apply -
+ apply (rule assm(5))
+ apply(rule xk xk')+
+ using k'
+ apply auto
+ done
qed
-lemma tagged_partial_division_subset: assumes "s tagged_partial_division_of i" "t \<subseteq> s"
+lemma tagged_partial_division_subset:
+ assumes "s tagged_partial_division_of i"
+ and "t \<subseteq> s"
shows "t tagged_partial_division_of i"
- using assms unfolding tagged_partial_division_of_def using finite_subset[OF assms(2)] by blast
-
-lemma setsum_over_tagged_division_lemma: fixes d::"('m::ordered_euclidean_space) set \<Rightarrow> 'a::real_normed_vector"
- assumes "p tagged_division_of i" "\<And>u v. {u..v} \<noteq> {} \<Longrightarrow> content {u..v} = 0 \<Longrightarrow> d {u..v} = 0"
+ using assms
+ unfolding tagged_partial_division_of_def
+ using finite_subset[OF assms(2)]
+ by blast
+
+lemma setsum_over_tagged_division_lemma:
+ fixes d :: "'m::ordered_euclidean_space set \<Rightarrow> 'a::real_normed_vector"
+ assumes "p tagged_division_of i"
+ and "\<And>u v. {u..v} \<noteq> {} \<Longrightarrow> content {u..v} = 0 \<Longrightarrow> d {u..v} = 0"
shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)"
-proof- note assm=tagged_division_ofD[OF assms(1)]
- have *:"(\<lambda>(x,k). d k) = d \<circ> snd" unfolding o_def apply(rule ext) by auto
- show ?thesis unfolding * apply(subst eq_commute) proof(rule setsum_reindex_nonzero)
- show "finite p" using assm by auto
- fix x y assume as:"x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
- obtain a b where ab:"snd x = {a..b}" using assm(4)[of "fst x" "snd x"] as(1) by auto
- have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y" unfolding as(4)[symmetric] using as(1-3) by auto
- hence "interior (snd x) \<inter> interior (snd y) = {}" apply-apply(rule assm(5)[of "fst x" _ "fst y"]) using as by auto
- hence "content {a..b} = 0" unfolding as(4)[symmetric] ab content_eq_0_interior by auto
- hence "d {a..b} = 0" apply-apply(rule assms(2)) using assm(2)[of "fst x" "snd x"] as(1) unfolding ab[symmetric] by auto
- thus "d (snd x) = 0" unfolding ab by auto qed qed
-
-lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x,k) \<in> p \<Longrightarrow> x \<in> i" by auto
+proof -
+ note assm = tagged_division_ofD[OF assms(1)]
+ have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
+ unfolding o_def by (rule ext) auto
+ show ?thesis
+ unfolding *
+ apply (subst eq_commute)
+ proof (rule setsum_reindex_nonzero)
+ show "finite p"
+ using assm by auto
+ fix x y
+ assume as: "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
+ obtain a b where ab: "snd x = {a..b}"
+ using assm(4)[of "fst x" "snd x"] as(1) by auto
+ have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
+ unfolding as(4)[symmetric] using as(1-3) by auto
+ then have "interior (snd x) \<inter> interior (snd y) = {}"
+ apply -
+ apply (rule assm(5)[of "fst x" _ "fst y"])
+ using as
+ apply auto
+ done
+ then have "content {a..b} = 0"
+ unfolding as(4)[symmetric] ab content_eq_0_interior by auto
+ then have "d {a..b} = 0"
+ apply -
+ apply (rule assms(2))
+ using assm(2)[of "fst x" "snd x"] as(1)
+ unfolding ab[symmetric]
+ apply auto
+ done
+ then show "d (snd x) = 0"
+ unfolding ab by auto
+ qed
+qed
+
+lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
+ by auto
lemma tagged_division_of_empty: "{} tagged_division_of {}"
unfolding tagged_division_of by auto
-lemma tagged_partial_division_of_trivial[simp]:
- "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
+lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
unfolding tagged_partial_division_of_def by auto
-lemma tagged_division_of_trivial[simp]:
- "p tagged_division_of {} \<longleftrightarrow> p = {}"
+lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} \<longleftrightarrow> p = {}"
unfolding tagged_division_of by auto
-lemma tagged_division_of_self:
- "x \<in> {a..b} \<Longrightarrow> {(x,{a..b})} tagged_division_of {a..b}"
- apply(rule tagged_division_ofI) by auto
+lemma tagged_division_of_self: "x \<in> {a..b} \<Longrightarrow> {(x,{a..b})} tagged_division_of {a..b}"
+ by (rule tagged_division_ofI) auto
lemma tagged_division_union:
- assumes "p1 tagged_division_of s1" "p2 tagged_division_of s2" "interior s1 \<inter> interior s2 = {}"
+ assumes "p1 tagged_division_of s1"
+ and "p2 tagged_division_of s2"
+ and "interior s1 \<inter> interior s2 = {}"
shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
-proof(rule tagged_division_ofI) note p1=tagged_division_ofD[OF assms(1)] and p2=tagged_division_ofD[OF assms(2)]
- show "finite (p1 \<union> p2)" using p1(1) p2(1) by auto
- show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2" using p1(6) p2(6) by blast
- fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
- show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
- fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
- have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
- show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
- apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
- using p1(3) p2(3) using xk xk' by auto qed
+proof (rule tagged_division_ofI)
+ note p1 = tagged_division_ofD[OF assms(1)]
+ note p2 = tagged_division_ofD[OF assms(2)]
+ show "finite (p1 \<union> p2)"
+ using p1(1) p2(1) by auto
+ show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
+ using p1(6) p2(6) by blast
+ fix x k
+ assume xk: "(x, k) \<in> p1 \<union> p2"
+ show "x \<in> k" "\<exists>a b. k = {a..b}"
+ using xk p1(2,4) p2(2,4) by auto
+ show "k \<subseteq> s1 \<union> s2"
+ using xk p1(3) p2(3) by blast
+ fix x' k'
+ assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
+ have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
+ using assms(3) interior_mono by blast
+ show "interior k \<inter> interior k' = {}"
+ apply (cases "(x, k) \<in> p1")
+ apply (case_tac[!] "(x',k') \<in> p1")
+ apply (rule p1(5))
+ prefer 4
+ apply (rule *)
+ prefer 6
+ apply (subst Int_commute)
+ apply (rule *)
+ prefer 8
+ apply (rule p2(5))
+ using p1(3) p2(3)
+ using xk xk'
+ apply auto
+ done
+qed
lemma tagged_division_unions:
- assumes "finite iset" "\<forall>i\<in>iset. (pfn(i) tagged_division_of i)"
- "\<forall>i1 \<in> iset. \<forall>i2 \<in> iset. ~(i1 = i2) \<longrightarrow> (interior(i1) \<inter> interior(i2) = {})"
+ assumes "finite iset"
+ and "\<forall>i\<in>iset. pfn i tagged_division_of i"
+ and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
-proof(rule tagged_division_ofI)
+proof (rule tagged_division_ofI)
note assm = tagged_division_ofD[OF assms(2)[rule_format]]
- show "finite (\<Union>(pfn ` iset))" apply(rule finite_Union) using assms by auto
- have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)" by blast
- also have "\<dots> = \<Union>iset" using assm(6) by auto
+ show "finite (\<Union>(pfn ` iset))"
+ apply (rule finite_Union)
+ using assms
+ apply auto
+ done
+ have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
+ by blast
+ also have "\<dots> = \<Union>iset"
+ using assm(6) by auto
finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
- fix x k assume xk:"(x,k)\<in>\<Union>(pfn ` iset)" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto
- show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
- fix x' k' assume xk':"(x',k')\<in>\<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
- have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
- using assms(3)[rule_format] interior_mono by blast
- show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
- using assm(5)[OF i _ xk'(2)] i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
+ fix x k
+ assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
+ then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
+ by auto
+ show "x \<in> k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset"
+ using assm(2-4)[OF i] using i(1) by auto
+ fix x' k'
+ assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
+ then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
+ by auto
+ have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
+ using i(1) i'(1)
+ using assms(3)[rule_format] interior_mono
+ by blast
+ show "interior k \<inter> interior k' = {}"
+ apply (cases "i = i'")
+ using assm(5)[OF i _ xk'(2)] i'(2)
+ using assm(3)[OF i] assm(3)[OF i']
+ defer
+ apply -
+ apply (rule *)
+ apply auto
+ done
qed
lemma tagged_partial_division_of_union_self:
- assumes "p tagged_partial_division_of s" shows "p tagged_division_of (\<Union>(snd ` p))"
- apply(rule tagged_division_ofI) using tagged_partial_division_ofD[OF assms] by auto
-
-lemma tagged_division_of_union_self: assumes "p tagged_division_of s"
+ assumes "p tagged_partial_division_of s"
shows "p tagged_division_of (\<Union>(snd ` p))"
- apply(rule tagged_division_ofI) using tagged_division_ofD[OF assms] by auto
+ apply (rule tagged_division_ofI)
+ using tagged_partial_division_ofD[OF assms]
+ apply auto
+ done
+
+lemma tagged_division_of_union_self:
+ assumes "p tagged_division_of s"
+ shows "p tagged_division_of (\<Union>(snd ` p))"
+ apply (rule tagged_division_ofI)
+ using tagged_division_ofD[OF assms]
+ apply auto
+ done
+
subsection {* Fine-ness of a partition w.r.t. a gauge. *}
-definition fine (infixr "fine" 46) where
- "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d(x))"
-
-lemma fineI: assumes "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
- shows "d fine s" using assms unfolding fine_def by auto
-
-lemma fineD[dest]: assumes "d fine s"
- shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x" using assms unfolding fine_def by auto
+definition fine (infixr "fine" 46)
+ where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
+
+lemma fineI:
+ assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
+ shows "d fine s"
+ using assms unfolding fine_def by auto
+
+lemma fineD[dest]:
+ assumes "d fine s"
+ shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
+ using assms unfolding fine_def by auto
lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
unfolding fine_def by auto
@@ -1682,61 +1911,76 @@
"(\<lambda>x. \<Inter> {f d x | d. d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
unfolding fine_def by blast
-lemma fine_union:
- "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
+lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
unfolding fine_def by blast
-lemma fine_unions:"(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
+lemma fine_unions: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
unfolding fine_def by auto
-lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
+lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
unfolding fine_def by blast
+
subsection {* Gauge integral. Define on compact intervals first, then use a limit. *}
-definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46) where
- "(f has_integral_compact_interval y) i \<equiv>
- (\<forall>e>0. \<exists>d. gauge d \<and>
- (\<forall>p. p tagged_division_of i \<and> d fine p
- \<longrightarrow> norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - y) < e))"
-
-definition has_integral (infixr "has'_integral" 46) where
-"((f::('n::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector)) has_integral y) i \<equiv>
- if (\<exists>a b. i = {a..b}) then (f has_integral_compact_interval y) i
- else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
- \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) {a..b} \<and>
- norm(z - y) < e))"
+definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46)
+ where "(f has_integral_compact_interval y) i \<longleftrightarrow>
+ (\<forall>e>0. \<exists>d. gauge d \<and>
+ (\<forall>p. p tagged_division_of i \<and> d fine p \<longrightarrow>
+ norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - y) < e))"
+
+definition has_integral ::
+ "('n::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> 'n set \<Rightarrow> bool"
+ (infixr "has'_integral" 46)
+ where "(f has_integral y) i \<longleftrightarrow>
+ (if \<exists>a b. i = {a..b}
+ then (f has_integral_compact_interval y) i
+ else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+ (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) {a..b} \<and>
+ norm (z - y) < e)))"
lemma has_integral:
- "(f has_integral y) ({a..b}) \<longleftrightarrow>
- (\<forall>e>0. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p
- \<longrightarrow> norm(setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
- unfolding has_integral_def has_integral_compact_interval_def by auto
-
-lemma has_integralD[dest]: assumes
- "(f has_integral y) ({a..b})" "e>0"
- obtains d where "gauge d" "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> d fine p
- \<Longrightarrow> norm(setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p - y) < e"
+ "(f has_integral y) {a..b} \<longleftrightarrow>
+ (\<forall>e>0. \<exists>d. gauge d \<and>
+ (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
+ norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
+ unfolding has_integral_def has_integral_compact_interval_def
+ by auto
+
+lemma has_integralD[dest]:
+ assumes "(f has_integral y) ({a..b})"
+ and "e > 0"
+ obtains d where "gauge d"
+ and "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> d fine p \<Longrightarrow>
+ norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p - y) < e"
using assms unfolding has_integral by auto
lemma has_integral_alt:
- "(f has_integral y) i \<longleftrightarrow>
- (if (\<exists>a b. i = {a..b}) then (f has_integral y) i
- else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b}
- \<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0)
- has_integral z) ({a..b}) \<and>
- norm(z - y) < e)))"
- unfolding has_integral unfolding has_integral_compact_interval_def has_integral_def by auto
+ "(f has_integral y) i \<longleftrightarrow>
+ (if \<exists>a b. i = {a..b}
+ then (f has_integral y) i
+ else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+ (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) ({a..b}) \<and> norm (z - y) < e)))"
+ unfolding has_integral
+ unfolding has_integral_compact_interval_def has_integral_def
+ by auto
lemma has_integral_altD:
- assumes "(f has_integral y) i" "\<not> (\<exists>a b. i = {a..b})" "e>0"
- obtains B where "B>0" "\<forall>a b. ball 0 B \<subseteq> {a..b}\<longrightarrow> (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) ({a..b}) \<and> norm(z - y) < e)"
- using assms unfolding has_integral unfolding has_integral_compact_interval_def has_integral_def by auto
-
-definition integrable_on (infixr "integrable'_on" 46) where
- "(f integrable_on i) \<equiv> \<exists>y. (f has_integral y) i"
-
-definition "integral i f \<equiv> SOME y. (f has_integral y) i"
+ assumes "(f has_integral y) i"
+ and "\<not> (\<exists>a b. i = {a..b})"
+ and "e>0"
+ obtains B where "B > 0"
+ and "\<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
+ (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) ({a..b}) \<and> norm(z - y) < e)"
+ using assms
+ unfolding has_integral
+ unfolding has_integral_compact_interval_def has_integral_def
+ by auto
+
+definition integrable_on (infixr "integrable'_on" 46)
+ where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
+
+definition "integral i f = (SOME y. (f has_integral y) i)"
lemma integrable_integral[dest]:
"f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"