--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Dec 16 17:08:22 2013 +0100
@@ -4241,7 +4241,7 @@
have "{a..b} \<noteq> {}"
using assms by auto
with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
- using assms(2) by (auto simp add: interval_eq_empty not_less)
+ using assms(2) by (auto simp add: interval_eq_empty interval)
have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
using assms(1)[unfolded mem_interval] using i by auto
have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -903,23 +903,23 @@
qed
lemma interval_cart:
- fixes a :: "'a::ord^'n"
- shows "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
- and "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
- by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
+ fixes a :: "real^'n"
+ shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
+ and "{a .. b} = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
+ by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_interval Basis_vec_def inner_axis)
lemma mem_interval_cart:
- fixes a :: "'a::ord^'n"
- shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
+ fixes a :: "real^'n"
+ shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
lemma interval_eq_empty_cart:
fixes a :: "real^'n"
- shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
+ shows "(box a b = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
and "({a .. b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
proof -
- { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>{a <..< b}"
+ { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b"
hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
hence "a$i < b$i" by auto
hence False using as by auto }
@@ -931,7 +931,7 @@
hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
unfolding vector_smult_component and vector_add_component
by auto }
- hence "{a <..< b} \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
+ hence "box a b \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
ultimately show ?th1 by blast
{ fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}"
@@ -953,16 +953,16 @@
lemma interval_ne_empty_cart:
fixes a :: "real^'n"
shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)"
- and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
+ and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
(* BH: Why doesn't just "auto" work here? *)
lemma subset_interval_imp_cart:
fixes a :: "real^'n"
shows "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
- and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
- and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}"
- and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
+ and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
+ and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
+ and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b"
unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
@@ -975,21 +975,21 @@
done
lemma interval_open_subset_closed_cart:
- fixes a :: "'a::preorder^'n"
- shows "{a<..<b} \<subseteq> {a .. b}"
+ fixes a :: "real^'n"
+ shows "box a b \<subseteq> {a .. b}"
proof (simp add: subset_eq, rule)
fix x
- assume x: "x \<in>{a<..<b}"
+ assume x: "x \<in>box a b"
{ fix i
have "a $ i \<le> x $ i"
using x order_less_imp_le[of "a$i" "x$i"]
- by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
+ by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis)
}
moreover
{ fix i
have "x $ i \<le> b $ i"
using x order_less_imp_le[of "x$i" "b$i"]
- by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
+ by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis)
}
ultimately
show "a \<le> x \<and> x \<le> b"
@@ -999,21 +999,21 @@
lemma subset_interval_cart:
fixes a :: "real^'n"
shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th1)
- and "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2)
- and "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3)
- and "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th4)
+ and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2)
+ and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3)
+ and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th4)
using subset_interval[of c d a b] by (simp_all add: Basis_vec_def inner_axis)
lemma disjoint_interval_cart:
fixes a::"real^'n"
shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i < c$i \<or> b$i < c$i \<or> d$i < a$i))" (is ?th1)
- and "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2)
- and "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3)
- and "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4)
+ and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2)
+ and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3)
+ and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4)
using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis)
lemma inter_interval_cart:
- fixes a :: "'a::linorder^'n"
+ fixes a :: "real^'n"
shows "{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
unfolding set_eq_iff and Int_iff and mem_interval_cart
by auto
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -3366,18 +3366,21 @@
ultimately show ?thesis by auto
qed
+lemma box_real: "box a b = {a<..<b::real}"
+ by (force simp add: box_def)
+
lemma rel_interior_real_interval:
fixes a b :: real
assumes "a < b"
shows "rel_interior {a..b} = {a<..<b}"
proof -
- have "{a<..<b} \<noteq> {}"
+ have "box a b \<noteq> {}"
using assms
unfolding set_eq_iff
- by (auto intro!: exI[of _ "(a + b) / 2"])
+ by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
then show ?thesis
using interior_rel_interior_gen[of "{a..b}", symmetric]
- by (simp split: split_if_asm add: interior_closed_interval)
+ by (simp split: split_if_asm add: interior_closed_interval box_real)
qed
lemma rel_interior_real_semiline:
@@ -5666,7 +5669,7 @@
shows "is_interval s \<Longrightarrow> connected s"
using is_interval_convex convex_connected by auto
-lemma convex_interval: "convex {a .. b}" "convex {a<..<b::'a::ordered_euclidean_space}"
+lemma convex_interval: "convex {a .. b}" "convex (box a (b::'a::ordered_euclidean_space))"
apply (rule_tac[!] is_interval_convex)
using is_interval_interval
apply auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 16 17:08:22 2013 +0100
@@ -586,12 +586,12 @@
lemma frechet_derivative_unique_within_open_interval:
fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
- assumes "x \<in> {a<..<b}"
- and "(f has_derivative f' ) (at x within {a<..<b})"
- and "(f has_derivative f'') (at x within {a<..<b})"
+ assumes "x \<in> box a b"
+ and "(f has_derivative f' ) (at x within box a b)"
+ and "(f has_derivative f'') (at x within box a b)"
shows "f' = f''"
proof -
- from assms(1) have *: "at x within {a<..<b} = at x"
+ from assms(1) have *: "at x within box a b = at x"
by (metis at_within_interior interior_open open_interval)
from assms(2,3) [unfolded *] show "f' = f''"
by (rule frechet_derivative_unique_at)
@@ -741,10 +741,10 @@
assumes "a < b"
and "f a = f b"
and "continuous_on {a..b} f"
- and "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
- shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
+ and "\<forall>x\<in>box a b. (f has_derivative f' x) (at x)"
+ shows "\<exists>x\<in>box a b. f' x = (\<lambda>v. 0)"
proof -
- have "\<exists>x\<in>{a<..<b}. (\<forall>y\<in>{a<..<b}. f x \<le> f y) \<or> (\<forall>y\<in>{a<..<b}. f y \<le> f x)"
+ have "\<exists>x\<in>box a b. (\<forall>y\<in>box a b. f x \<le> f y) \<or> (\<forall>y\<in>box a b. f y \<le> f x)"
proof -
have "(a + b) / 2 \<in> {a .. b}"
using assms(1) by auto
@@ -753,20 +753,20 @@
guess d using continuous_attains_sup[OF compact_interval * assms(3)] .. note d=this
guess c using continuous_attains_inf[OF compact_interval * assms(3)] .. note c=this
show ?thesis
- proof (cases "d \<in> {a<..<b} \<or> c \<in> {a<..<b}")
+ proof (cases "d \<in> box a b \<or> c \<in> box a b")
case True
then show ?thesis
apply (erule_tac disjE)
apply (rule_tac x=d in bexI)
apply (rule_tac[3] x=c in bexI)
using d c
- apply auto
+ apply (auto simp: box_real)
done
next
def e \<equiv> "(a + b) /2"
case False
then have "f d = f c"
- using d c assms(2) by auto
+ using d c assms(2) by (auto simp: box_real)
then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
using c d
apply -
@@ -777,13 +777,13 @@
apply (rule_tac x=e in bexI)
unfolding e_def
using assms(1)
- apply auto
+ apply (auto simp: box_real)
done
qed
qed
then guess x .. note x=this
then have "f' x = (\<lambda>v. 0)"
- apply (rule_tac differential_zero_maxmin[of x "{a<..<b}" f "f' x"])
+ apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
defer
apply (rule open_interval)
apply (rule assms(4)[unfolded has_derivative_at[symmetric],THEN bspec[where x=x]])
@@ -813,10 +813,10 @@
assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
proof -
- have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
+ have "\<exists>x\<in>box a b. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
fix x
- assume x: "x \<in> {a<..<b}"
+ assume "x \<in> box a b" hence x: "x \<in> {a<..<b}" by (simp add: box_real)
show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
@@ -825,7 +825,7 @@
then show ?thesis
apply (rule_tac x=x in bexI)
apply (drule fun_cong[of _ _ "b - a"])
- apply auto
+ apply (auto simp: box_real)
done
qed
@@ -841,13 +841,13 @@
defer
proof
fix x
- assume x: "x \<in> {a<..<b}"
+ assume x: "x \<in> {a<..<b}" hence x: "x \<in> box a b" by (simp add: box_real)
show "(f has_derivative f' x) (at x)"
unfolding has_derivative_within_open[OF x open_interval,symmetric]
apply (rule has_derivative_within_subset)
apply (rule assms(2)[rule_format])
using x
- apply auto
+ apply (auto simp: box_real)
done
qed (insert assms(2), auto)
@@ -963,8 +963,7 @@
apply auto
done
then show ?case
- unfolding has_derivative_within_open[OF goal1 open_interval]
- by auto
+ unfolding has_derivative_within_open[OF goal1 open_greaterThanLessThan] .
qed
guess u using mvt_general[OF zero_less_one 1 2] .. note u = this
have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Dec 16 17:08:22 2013 +0100
@@ -80,7 +80,7 @@
} note x0 = this
have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
using UNIV_2 by auto
- have 1: "{- 1<..<1::real^2} \<noteq> {}"
+ have 1: "box (- 1) (1::real^2) \<noteq> {}"
unfolding interval_eq_empty_cart by auto
have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
apply (intro continuous_on_intros continuous_on_component)
@@ -344,7 +344,7 @@
by auto
next
have "{a..b} \<noteq> {}"
- using assms(3) using path_image_nonempty by auto
+ using assms(3) using path_image_nonempty[of f] by auto
then have "a \<le> b"
unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
@@ -646,7 +646,7 @@
obtains z where "z \<in> path_image f" and "z \<in> path_image g"
proof -
have "{a..b} \<noteq> {}"
- using path_image_nonempty using assms(3) by auto
+ using path_image_nonempty[of f] using assms(3) by auto
note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
have "pathstart f \<in> {a..b}"
and "pathfinish f \<in> {a..b}"
@@ -692,7 +692,7 @@
using ab startfin abab assms(3)
using assms(9-)
unfolding assms
- apply (auto simp add: field_simps)
+ apply (auto simp add: field_simps interval)
done
then show "path_image ?P1 \<subseteq> {?a .. ?b}" .
have "path_image ?P2 \<subseteq> {?a .. ?b}"
@@ -704,7 +704,7 @@
using ab startfin abab assms(4)
using assms(9-)
unfolding assms
- apply (auto simp add: field_simps)
+ apply (auto simp add: field_simps interval)
done
then show "path_image ?P2 \<subseteq> {?a .. ?b}" .
show "a $ 1 - 2 = a $ 1 - 2"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 16 17:08:22 2013 +0100
@@ -220,7 +220,8 @@
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])
+ apply (auto simp: eucl_le[where 'a='a])
+ by (metis (mono_tags) eucl_less eucl_less_not_refl order.strict_trans2 zero_less_one)
lemma interior_subset_union_intervals:
assumes "i = {a..b::'a::ordered_euclidean_space}"
@@ -230,11 +231,11 @@
and "interior i \<inter> interior j = {}"
shows "interior i \<subseteq> interior s"
proof -
- have "{a<..<b} \<inter> {c..d} = {}"
+ have "box a b \<inter> {c..d} = {}"
using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
unfolding assms(1,2) interior_closed_interval by auto
moreover
- have "{a<..<b} \<subseteq> {c..d} \<union> s"
+ have "box a b \<subseteq> {c..d} \<union> s"
apply (rule order_trans,rule interval_open_subset_closed)
using assms(4) unfolding assms(1,2)
apply auto
@@ -310,9 +311,9 @@
then show ?thesis by auto
next
case True show ?thesis
- proof (cases "x\<in>{a<..<b}")
+ proof (cases "x\<in>box a b")
case True
- then obtain d where "0 < d \<and> ball x d \<subseteq> {a<..<b}"
+ then obtain d where "0 < d \<and> ball x d \<subseteq> box 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)
@@ -1114,7 +1115,8 @@
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 k] using assms(2) 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
@@ -1324,7 +1326,7 @@
apply (rule assm(1)) unfolding Union_insert
using assm(2-4) as
apply -
- apply (fastforce dest: assm(5))+
+ apply (fast dest: assm(5))+
done
next
assume as: "p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b} \<noteq> {}"
@@ -2149,7 +2151,7 @@
unfolding s t interior_closed_interval
proof (rule *)
fix x
- assume "x \<in> {c<..<d}" "x \<in> {e<..<f}"
+ assume "x \<in> box c d" "x \<in> box e f"
then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
unfolding mem_interval using i'
apply -
@@ -3274,7 +3276,7 @@
then have "{a .. b} = {}"
unfolding interval_eq_empty by (auto simp: eucl_le[where 'a='a] not_le)
then show ?thesis
- by auto
+ by (auto simp: not_le)
qed
lemma division_split_left_inj:
@@ -3405,7 +3407,7 @@
apply -
prefer 3
apply (subst interval_split[OF k])
- apply auto
+ apply (auto intro: order.trans)
done
fix k'
assume "k' \<in> ?p1"
@@ -3426,7 +3428,7 @@
apply -
prefer 3
apply (subst interval_split[OF k])
- apply auto
+ apply (auto intro: order.trans)
done
fix k'
assume "k' \<in> ?p2"
@@ -3721,7 +3723,7 @@
apply (rule tagged_division_union[OF assms(1-2)])
unfolding interval_split[OF k] interior_closed_interval
using k
- apply (auto simp add: eucl_less[where 'a='a] elim!: ballE[where x=k])
+ apply (auto simp add: eucl_less[where 'a='a] interval elim!: ballE[where x=k])
done
qed
@@ -6248,10 +6250,10 @@
subsection {* In particular, the boundary of an interval is negligible. *}
-lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - {a<..<b})"
+lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - box a b)"
proof -
let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
- have "{a..b} - {a<..<b} \<subseteq> ?A"
+ have "{a..b} - box a b \<subseteq> ?A"
apply rule unfolding Diff_iff mem_interval
apply simp
apply(erule conjE bexE)+
@@ -6267,7 +6269,7 @@
qed
lemma has_integral_spike_interior:
- assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+ assumes "\<forall>x\<in>box a b. g x = f x"
and "(f has_integral y) ({a..b})"
shows "(g has_integral y) {a..b}"
apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
@@ -6276,7 +6278,7 @@
done
lemma has_integral_spike_interior_eq:
- assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+ assumes "\<forall>x\<in>box a b. g x = f x"
shows "(f has_integral y) {a..b} \<longleftrightarrow> (g has_integral y) {a..b}"
apply rule
apply (rule_tac[!] has_integral_spike_interior)
@@ -6285,7 +6287,7 @@
done
lemma integrable_spike_interior:
- assumes "\<forall>x\<in>{a<..<b}. g x = f x"
+ assumes "\<forall>x\<in>box a b. g x = f x"
and "f integrable_on {a..b}"
shows "g integrable_on {a..b}"
using assms
@@ -7029,7 +7031,7 @@
then show "f integrable_on k"
apply safe
apply (rule d[THEN conjunct2,rule_format,of x])
- apply auto
+ apply (auto intro: order.trans)
done
qed
qed
@@ -7650,7 +7652,7 @@
fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
assumes "a \<le> b"
and "continuous_on {a..b} f"
- and "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
+ and "\<forall>x\<in>box a b. (f has_vector_derivative f'(x)) (at x)"
shows "(f' has_integral (f b - f a)) {a..b}"
proof -
{
@@ -7682,7 +7684,7 @@
note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
note conjunctD2[OF this]
note bounded=this(1) and this(2)
- from this(2) have "\<forall>x\<in>{a<..<b}. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
+ from this(2) have "\<forall>x\<in>box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
apply -
apply safe
@@ -7885,8 +7887,8 @@
note result = as(2)[unfolded k interval_bounds_real[OF this(1)] content_real[OF this(1)]]
assume as': "x \<noteq> a" "x \<noteq> b"
- then have "x \<in> {a<..<b}"
- using p(2-3)[OF as(1)] by auto
+ then have "x \<in> box a b"
+ using p(2-3)[OF as(1)] by (auto simp: interval)
note * = d(2)[OF this]
have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
@@ -8047,13 +8049,13 @@
assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
- have "{a <..< ?v} \<subseteq> k \<inter> k'"
- unfolding v v' by (auto simp add:)
+ have "box a ?v \<subseteq> k \<inter> k'"
+ unfolding v v' by (auto simp add: interval)
note interior_mono[OF this,unfolded interior_inter]
- moreover have "(a + ?v)/2 \<in> { a <..< ?v}"
+ moreover have "(a + ?v)/2 \<in> box a ?v"
using k(3-)
unfolding v v' content_eq_0 not_le
- by (auto simp add: not_le)
+ by (auto simp add: interval)
ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
unfolding interior_open[OF open_interval] by auto
then have *: "k = k'"
@@ -8078,11 +8080,11 @@
guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this]
let ?v = "max v v'"
- have "{?v <..< b} \<subseteq> k \<inter> k'"
- unfolding v v' by auto
+ have "box ?v b \<subseteq> k \<inter> k'"
+ unfolding v v' by (auto simp: interval)
note interior_mono[OF this,unfolded interior_inter]
- moreover have " ((b + ?v)/2) \<in> {?v <..< b}"
- using k(3-) unfolding v v' content_eq_0 not_le by auto
+ moreover have " ((b + ?v)/2) \<in> box ?v b"
+ using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: interval)
ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
unfolding interior_open[OF open_interval] by auto
then have *: "k = k'"
@@ -8175,7 +8177,7 @@
assumes "finite s"
and "a \<le> b"
and "continuous_on {a..b} f"
- and "\<forall>x\<in>{a<..<b} - s. (f has_vector_derivative f'(x)) (at x)"
+ and "\<forall>x\<in>box a b - s. (f has_vector_derivative f'(x)) (at x)"
shows "(f' has_integral (f b - f a)) {a..b}"
using assms
proof (induct "card s" arbitrary: s a b)
@@ -8196,7 +8198,7 @@
done
note cs = this[rule_format]
show ?case
- proof (cases "c \<in> {a<..<b}")
+ proof (cases "c \<in> box a b")
case False
then show ?thesis
apply -
@@ -8213,7 +8215,7 @@
by auto
case True
then have "a \<le> c" "c \<le> b"
- by auto
+ by (auto simp: interval)
then show ?thesis
apply (subst *)
apply (rule has_integral_combine)
@@ -8225,15 +8227,15 @@
show "continuous_on {a..c} f" "continuous_on {c..b} f"
apply (rule_tac[!] continuous_on_subset[OF Suc(5)])
using True
- apply auto
- done
- let ?P = "\<lambda>i j. \<forall>x\<in>{i<..<j} - s'. (f has_vector_derivative f' x) (at x)"
+ apply (auto simp: interval)
+ done
+ let ?P = "\<lambda>i j. \<forall>x\<in>box i j - s'. (f has_vector_derivative f' x) (at x)"
show "?P a c" "?P c b"
apply safe
apply (rule_tac[!] Suc(6)[rule_format])
using True
unfolding cs
- apply auto
+ apply (auto simp: interval)
done
qed auto
qed
@@ -8248,7 +8250,7 @@
shows "(f' has_integral (f(b) - f(a))) {a..b}"
apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
using assms(4)
- apply auto
+ apply (auto simp: interval)
done
lemma indefinite_integral_continuous_left:
@@ -8609,7 +8611,7 @@
apply (rule open_interval)
apply (rule has_derivative_within_subset[where s="{a..b}"])
using assms(4) assms(5)
- apply auto
+ apply (auto simp: interval)
done
note this[unfolded *]
note has_integral_unique[OF has_integral_0 this]
@@ -8773,9 +8775,9 @@
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
assumes "(f has_integral i) {c..d}"
and "{c..d} \<subseteq> {a..b}"
- shows "((\<lambda>x. if x \<in> {c<..<d} then f x else 0) has_integral i) {a..b}"
-proof -
- def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
+ shows "((\<lambda>x. if x \<in> box c d then f x else 0) has_integral i) {a..b}"
+proof -
+ def g \<equiv> "\<lambda>x. if x \<in>box c d then f x else 0"
{
presume *: "{c..d} \<noteq> {} \<Longrightarrow> ?thesis"
show ?thesis
@@ -8784,7 +8786,7 @@
apply assumption
proof -
case goal1
- then have *: "{c<..<d} = {}"
+ then have *: "box c d = {}"
using interval_open_subset_closed
by auto
show ?thesis
@@ -9812,7 +9814,7 @@
from d(5)[OF goal1] show ?case
unfolding obt interior_closed_interval
apply -
- apply (rule negligible_subset[of "({a..b}-{a<..<b}) \<union> ({c..d}-{c<..<d})"])
+ apply (rule negligible_subset[of "({a..b}-box a b) \<union> ({c..d}-box c d)"])
apply (rule negligible_union negligible_frontier_interval)+
apply auto
done
@@ -9944,7 +9946,7 @@
case goal1
note tagged_division_ofD(3-4)[OF assms(2) this]
then show ?case
- using integrable_subinterval[OF assms(1)] by auto
+ using integrable_subinterval[OF assms(1)] by blast
qed
lemma integral_combine_tagged_division_topdown:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -826,7 +826,14 @@
unfolding dist_norm norm_eq_sqrt_inner setL2_def
by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
-definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
+definition (in euclidean_space) eucl_less (infix "<e" 50)
+ where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
+
+definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
+
+lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
+ and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
+ by (auto simp: box_eucl_less eucl_less_def)
lemma rational_boxes:
fixes x :: "'a\<Colon>euclidean_space"
@@ -2042,8 +2049,7 @@
by auto
then have "ball x (infdist x A) \<inter> closure A = {}"
apply auto
- apply (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
- eucl_less_not_refl euclidean_trans(2) infdist_le)
+ apply (metis `x \<in> closure A` closure_approachable dist_commute infdist_le not_less)
done
then have "x \<notin> closure A"
by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
@@ -5992,25 +5998,25 @@
lemma interval:
fixes a :: "'a::ordered_euclidean_space"
- shows "{a <..< b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
+ shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
- by (auto simp add:set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
+ by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
lemma mem_interval:
fixes a :: "'a::ordered_euclidean_space"
- shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
+ shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)"
using interval[of a b]
- by (auto simp add: set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
+ by auto
lemma interval_eq_empty:
fixes a :: "'a::ordered_euclidean_space"
- shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
+ shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
and "({a .. b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
proof -
{
fix i x
- assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>{a <..< b}"
+ assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
unfolding mem_interval by auto
then have "a\<bullet>i < b\<bullet>i" by auto
@@ -6028,7 +6034,7 @@
then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
by (auto simp: inner_add_left)
}
- then have "{a <..< b} \<noteq> {}"
+ then have "box a b \<noteq> {}"
using mem_interval(1)[of "?x" a b] by auto
}
ultimately show ?th1 by blast
@@ -6062,37 +6068,37 @@
lemma interval_ne_empty:
fixes a :: "'a::ordered_euclidean_space"
shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
- and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
+ and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
unfolding interval_eq_empty[of a b] by fastforce+
lemma interval_sing:
fixes a :: "'a::ordered_euclidean_space"
shows "{a .. a} = {a}"
- and "{a<..<a} = {}"
+ and "box a a = {}"
unfolding set_eq_iff mem_interval eq_iff [symmetric]
by (auto intro: euclidean_eqI simp: ex_in_conv)
lemma subset_interval_imp:
fixes a :: "'a::ordered_euclidean_space"
shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
- and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
- and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}"
- and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
+ and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
+ and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
+ and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
lemma interval_open_subset_closed:
fixes a :: "'a::ordered_euclidean_space"
- shows "{a<..<b} \<subseteq> {a .. b}"
+ shows "box a b \<subseteq> {a .. b}"
unfolding subset_eq [unfolded Ball_def] mem_interval
by (fast intro: less_imp_le)
lemma subset_interval:
fixes a :: "'a::ordered_euclidean_space"
shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
- and "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
- and "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
- and "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
+ and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
+ and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
+ and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
proof -
show ?th1
unfolding subset_eq and Ball_def and mem_interval
@@ -6101,8 +6107,8 @@
unfolding subset_eq and Ball_def and mem_interval
by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
{
- assume as: "{c<..<d} \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
- then have "{c<..<d} \<noteq> {}"
+ assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+ then have "box c d \<noteq> {}"
unfolding interval_eq_empty by auto
fix i :: 'a
assume i: "i \<in> Basis"
@@ -6119,7 +6125,7 @@
apply (auto simp add: as2)
done
}
- then have "?x\<in>{c<..<d}"
+ then have "?x\<in>box c d"
using i unfolding mem_interval by auto
moreover
have "?x \<notin> {a .. b}"
@@ -6145,7 +6151,7 @@
apply (auto simp add: as2)
done
}
- then have "?x\<in>{c<..<d}"
+ then have "?x\<in>box c d"
unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
@@ -6171,10 +6177,10 @@
apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
done
{
- assume as: "{c<..<d} \<subseteq> {a<..<b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
+ assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
fix i :: 'a
assume i:"i\<in>Basis"
- from as(1) have "{c<..<d} \<subseteq> {a..b}"
+ from as(1) have "box c d \<subseteq> {a..b}"
using interval_open_subset_closed[of a b] by auto
then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
using part1 and as(2) using i by auto
@@ -6200,9 +6206,9 @@
lemma disjoint_interval:
fixes a::"'a::ordered_euclidean_space"
shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
- and "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
- and "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
- and "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
+ and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
+ and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
+ and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
proof -
let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
@@ -6219,14 +6225,14 @@
lemma open_interval[intro]:
fixes a b :: "'a::ordered_euclidean_space"
- shows "open {a<..<b}"
+ shows "open (box a b)"
proof -
have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
- also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = {a<..<b}"
- by (auto simp add: eucl_less [where 'a='a])
- finally show "open {a<..<b}" .
+ also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
+ by (auto simp add: interval)
+ finally show "open (box a b)" .
qed
lemma closed_interval[intro]:
@@ -6243,7 +6249,7 @@
lemma interior_closed_interval [intro]:
fixes a b :: "'a::ordered_euclidean_space"
- shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
+ shows "interior {a..b} = box a b" (is "?L = ?R")
proof(rule subset_antisym)
show "?R \<subseteq> ?L"
using interval_open_subset_closed open_interval
@@ -6275,7 +6281,7 @@
using `e>0` i
by (auto simp: inner_diff_left inner_Basis inner_add_left)
}
- then have "x \<in> {a<..<b}"
+ then have "x \<in> box a b"
unfolding mem_interval by auto
}
then show "?L \<subseteq> ?R" ..
@@ -6309,15 +6315,15 @@
lemma bounded_interval:
fixes a :: "'a::ordered_euclidean_space"
- shows "bounded {a .. b} \<and> bounded {a<..<b}"
+ shows "bounded {a .. b} \<and> bounded (box a b)"
using bounded_closed_interval[of a b]
using interval_open_subset_closed[of a b]
- using bounded_subset[of "{a..b}" "{a<..<b}"]
+ using bounded_subset[of "{a..b}" "box a b"]
by simp
lemma not_interval_univ:
fixes a :: "'a::ordered_euclidean_space"
- shows "{a .. b} \<noteq> UNIV \<and> {a<..<b} \<noteq> UNIV"
+ shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
using bounded_interval[of a b] by auto
lemma compact_interval:
@@ -6328,8 +6334,8 @@
lemma open_interval_midpoint:
fixes a :: "'a::ordered_euclidean_space"
- assumes "{a<..<b} \<noteq> {}"
- shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
+ assumes "box a b \<noteq> {}"
+ shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
proof -
{
fix i :: 'a
@@ -6342,10 +6348,10 @@
lemma open_closed_interval_convex:
fixes x :: "'a::ordered_euclidean_space"
- assumes x: "x \<in> {a<..<b}"
+ assumes x: "x \<in> box a b"
and y: "y \<in> {a .. b}"
and e: "0 < e" "e \<le> 1"
- shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> {a<..<b}"
+ shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
proof -
{
fix i :: 'a
@@ -6392,14 +6398,11 @@
lemma closure_open_interval:
fixes a :: "'a::ordered_euclidean_space"
- assumes "{a<..<b} \<noteq> {}"
- shows "closure {a<..<b} = {a .. b}"
+ assumes "box a b \<noteq> {}"
+ shows "closure (box a b) = {a .. b}"
proof -
- have ab: "a < b"
- using assms[unfolded interval_ne_empty]
- apply (subst eucl_less)
- apply auto
- done
+ have ab: "a <e b"
+ using assms by (simp add: eucl_less_def interval_ne_empty)
let ?c = "(1 / 2) *\<^sub>R (a + b)"
{
fix x
@@ -6407,15 +6410,15 @@
def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
{
fix n
- assume fn: "f n < b \<longrightarrow> a < f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
+ assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
unfolding inverse_le_1_iff by auto
have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
by (auto simp add: algebra_simps)
- then have "f n < b" and "a < f n"
+ then have "f n <e b" and "a <e f n"
using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
- unfolding f_def by auto
+ unfolding f_def by (auto simp: interval eucl_less_def)
then have False
using fn unfolding f_def using xc by auto
}
@@ -6448,11 +6451,11 @@
using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
by auto
}
- ultimately have "x \<in> closure {a<..<b}"
+ ultimately have "x \<in> closure (box a b)"
using as and open_interval_midpoint[OF assms]
unfolding closure_def
unfolding islimpt_sequential
- by (cases "x=?c") auto
+ by (cases "x=?c") (auto simp: in_box_eucl_less)
}
then show ?thesis
using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
@@ -6461,7 +6464,7 @@
lemma bounded_subset_open_interval_symmetric:
fixes s::"('a::ordered_euclidean_space) set"
assumes "bounded s"
- shows "\<exists>a. s \<subseteq> {-a<..<a}"
+ shows "\<exists>a. s \<subseteq> box (-a) a"
proof -
obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
using assms[unfolded bounded_pos] by auto
@@ -6478,12 +6481,12 @@
by auto
}
then show ?thesis
- by (auto intro: exI[where x=a] simp add: eucl_less[where 'a='a])
+ by (auto intro: exI[where x=a] simp add: interval)
qed
lemma bounded_subset_open_interval:
fixes s :: "('a::ordered_euclidean_space) set"
- shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a<..<b})"
+ shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
by (auto dest!: bounded_subset_open_interval_symmetric)
lemma bounded_subset_closed_interval_symmetric:
@@ -6491,7 +6494,7 @@
assumes "bounded s"
shows "\<exists>a. s \<subseteq> {-a .. a}"
proof -
- obtain a where "s \<subseteq> {- a<..<a}"
+ obtain a where "s \<subseteq> box (-a) a"
using bounded_subset_open_interval_symmetric[OF assms] by auto
then show ?thesis
using interval_open_subset_closed[of "-a" a] by auto
@@ -6504,13 +6507,13 @@
lemma frontier_closed_interval:
fixes a b :: "'a::ordered_euclidean_space"
- shows "frontier {a .. b} = {a .. b} - {a<..<b}"
+ shows "frontier {a .. b} = {a .. b} - box a b"
unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
lemma frontier_open_interval:
fixes a b :: "'a::ordered_euclidean_space"
- shows "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
-proof (cases "{a<..<b} = {}")
+ shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
+proof (cases "box a b = {}")
case True
then show ?thesis
using frontier_empty by auto
@@ -6523,8 +6526,8 @@
lemma inter_interval_mixed_eq_empty:
fixes a :: "'a::ordered_euclidean_space"
- assumes "{c<..<d} \<noteq> {}"
- shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
+ assumes "box c d \<noteq> {}"
+ shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
unfolding closure_open_interval[OF assms, symmetric]
unfolding open_inter_closure_eq_empty[OF open_interval] ..
@@ -6577,7 +6580,7 @@
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
- "is_interval {a<..<b}" (is ?th2) proof -
+ "is_interval (box a b)" (is ?th2) proof -
show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
@@ -6705,13 +6708,13 @@
lemma eucl_lessThan_eq_halfspaces:
fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{..<a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
- by (auto simp: eucl_less[where 'a='a])
+ shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
+ by (auto simp: eucl_less_def)
lemma eucl_greaterThan_eq_halfspaces:
fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "{a<..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
- by (auto simp: eucl_less[where 'a='a])
+ shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
+ by (auto simp: eucl_less_def)
lemma eucl_atMost_eq_halfspaces:
fixes a :: "'a\<Colon>ordered_euclidean_space"
@@ -6725,12 +6728,12 @@
lemma open_eucl_lessThan[simp, intro]:
fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "open {..< a}"
+ shows "open {x. x <e a}"
by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
lemma open_eucl_greaterThan[simp, intro]:
fixes a :: "'a\<Colon>ordered_euclidean_space"
- shows "open {a <..}"
+ shows "open {x. a <e x}"
by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
lemma closed_eucl_atMost[simp, intro]:
@@ -7101,7 +7104,7 @@
by auto
then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
using cs[unfolded complete_def, THEN spec[where x="x"]]
- using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1)
+ using cauchy_isometric[OF `0 < e` s f normf] and cfg and x(1)
by auto
then have "\<exists>l\<in>f ` s. (g ---> l) sequentially"
using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
@@ -7628,4 +7631,7 @@
declare tendsto_const [intro] (* FIXME: move *)
+no_notation
+ eucl_less (infix "<e" 50)
+
end
--- a/src/HOL/Probability/Borel_Space.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Mon Dec 16 17:08:22 2013 +0100
@@ -237,18 +237,25 @@
by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
closed_atMost closed_atLeast closed_atLeastAtMost)+
+notation
+ eucl_less (infix "<e" 50)
+
+lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}"
+ and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}"
+ by auto
+
lemma eucl_ivals[measurable]:
fixes a b :: "'a\<Colon>ordered_euclidean_space"
- shows "{..< a} \<in> sets borel"
- and "{a <..} \<in> sets borel"
- and "{a<..<b} \<in> sets borel"
+ shows "{x. x <e a} \<in> sets borel"
+ and "{x. a <e x} \<in> sets borel"
+ and "box a b \<in> sets borel"
and "{..a} \<in> sets borel"
and "{a..} \<in> sets borel"
and "{a..b} \<in> sets borel"
- and "{a<..b} \<in> sets borel"
- and "{a..<b} \<in> sets borel"
- unfolding greaterThanAtMost_def atLeastLessThan_def
- by (blast intro: borel_open borel_closed)+
+ and "{x. a <e x \<and> x \<le> b} \<in> sets borel"
+ and "{x. a \<le> x \<and> x <e b} \<in> sets borel"
+ unfolding box_oc box_co
+ by (auto intro: borel_open borel_closed)
lemma open_Collect_less:
fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
@@ -375,11 +382,6 @@
done
qed (auto simp: box_def)
-lemma borel_eq_greaterThanLessThan:
- "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))"
- unfolding borel_eq_box apply (rule arg_cong2[where f=sigma])
- by (auto simp: box_def image_iff mem_interval set_eq_iff simp del: greaterThanLessThan_iff)
-
lemma halfspace_gt_in_halfspace:
assumes i: "i \<in> A"
shows "{x\<Colon>'a. a < x \<bullet> i} \<in>
@@ -484,15 +486,15 @@
qed auto
lemma borel_eq_greaterThan:
- "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))"
+ "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. a <e x}))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have i: "i \<in> Basis" by auto
have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
also have *: "{x::'a. a < x\<bullet>i} =
- (\<Union>k::nat. {\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n <..})" using i
- proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
+ (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
+ proof (safe, simp_all add: eucl_less_def split: split_if_asm)
fix x :: 'a
from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
guess k::nat .. note k = this
@@ -511,14 +513,14 @@
qed auto
lemma borel_eq_lessThan:
- "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<a}))"
+ "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. x <e a}))"
(is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have i: "i \<in> Basis" by auto
have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
- also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {..< \<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n})" using `i\<in> Basis`
- proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
+ also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using `i\<in> Basis`
+ proof (safe, simp_all add: eucl_less_def split: split_if_asm)
fix x :: 'a
from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
guess k::nat .. note k = this
@@ -532,7 +534,7 @@
finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
apply (simp only:)
apply (safe intro!: sets.countable_UN sets.Diff)
- apply (auto intro: sigma_sets_top)
+ apply (auto intro: sigma_sets_top )
done
qed auto
@@ -558,6 +560,9 @@
(auto intro!: sigma_sets_top)
qed auto
+lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
+ by (simp add: eucl_less_def lessThan_def)
+
lemma borel_eq_atLeastLessThan:
"borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
@@ -565,8 +570,8 @@
fix x :: real
have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
by (auto simp: move_uminus real_arch_simple)
- then show "{..< x} \<in> ?SIGMA"
- by (auto intro: sigma_sets.intros)
+ then show "{y. y <e x} \<in> ?SIGMA"
+ by (auto intro: sigma_sets.intros simp: eucl_lessThan)
qed auto
lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
@@ -1195,4 +1200,7 @@
shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
+no_notation
+ eucl_less (infix "<e" 50)
+
end
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 16 14:49:18 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 16 17:08:22 2013 +0100
@@ -916,16 +916,15 @@
proof (subst sigma_prod_algebra_sigma_eq[where S="\<lambda>_ i::nat. {..<real i}" and E="\<lambda>_. range lessThan", OF I])
show "sigma_sets (space (Pi\<^sub>M I (\<lambda>i. lborel))) {Pi\<^sub>E I F |F. \<forall>i\<in>I. F i \<in> range lessThan} = ?G"
by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
-qed (auto simp: borel_eq_lessThan reals_Archimedean2)
+qed (auto simp: borel_eq_lessThan eucl_lessThan reals_Archimedean2)
lemma measurable_e2p[measurable]:
"e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^sub>M (i::'a)\<in>Basis. (lborel :: real measure))"
proof (rule measurable_sigma_sets[OF sets_product_borel])
fix A :: "('a \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i} |x. True} "
then obtain x where "A = (\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i})" by auto
- then have "e2p -` A = {..< (\<Sum>i\<in>Basis. x i *\<^sub>R i) :: 'a}"
- using DIM_positive by (auto simp add: set_eq_iff e2p_def
- euclidean_eq_iff[where 'a='a] eucl_less[where 'a='a])
+ then have "e2p -` A = {y :: 'a. eucl_less y (\<Sum>i\<in>Basis. x i *\<^sub>R i)}"
+ using DIM_positive by (auto simp add: set_eq_iff e2p_def eucl_less_def)
then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
qed (auto simp: e2p_def)