1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Dec 16 14:49:18 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Dec 16 17:08:22 2013 +0100
1.3 @@ -4241,7 +4241,7 @@
1.4 have "{a..b} \<noteq> {}"
1.5 using assms by auto
1.6 with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
1.7 - using assms(2) by (auto simp add: interval_eq_empty not_less)
1.8 + using assms(2) by (auto simp add: interval_eq_empty interval)
1.9 have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
1.10 using assms(1)[unfolded mem_interval] using i by auto
1.11 have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Dec 16 14:49:18 2013 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
2.3 @@ -903,23 +903,23 @@
2.4 qed
2.5
2.6 lemma interval_cart:
2.7 - fixes a :: "'a::ord^'n"
2.8 - shows "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
2.9 - and "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
2.10 - by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
2.11 + fixes a :: "real^'n"
2.12 + shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}"
2.13 + and "{a .. b} = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
2.14 + by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_interval Basis_vec_def inner_axis)
2.15
2.16 lemma mem_interval_cart:
2.17 - fixes a :: "'a::ord^'n"
2.18 - shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
2.19 + fixes a :: "real^'n"
2.20 + shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
2.21 and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
2.22 using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def)
2.23
2.24 lemma interval_eq_empty_cart:
2.25 fixes a :: "real^'n"
2.26 - shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
2.27 + shows "(box a b = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1)
2.28 and "({a .. b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
2.29 proof -
2.30 - { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>{a <..< b}"
2.31 + { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b"
2.32 hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
2.33 hence "a$i < b$i" by auto
2.34 hence False using as by auto }
2.35 @@ -931,7 +931,7 @@
2.36 hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
2.37 unfolding vector_smult_component and vector_add_component
2.38 by auto }
2.39 - hence "{a <..< b} \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
2.40 + hence "box a b \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
2.41 ultimately show ?th1 by blast
2.42
2.43 { fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}"
2.44 @@ -953,16 +953,16 @@
2.45 lemma interval_ne_empty_cart:
2.46 fixes a :: "real^'n"
2.47 shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)"
2.48 - and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
2.49 + and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
2.50 unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le)
2.51 (* BH: Why doesn't just "auto" work here? *)
2.52
2.53 lemma subset_interval_imp_cart:
2.54 fixes a :: "real^'n"
2.55 shows "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
2.56 - and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
2.57 - and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}"
2.58 - and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
2.59 + and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
2.60 + and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
2.61 + and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b"
2.62 unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
2.63 by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
2.64
2.65 @@ -975,21 +975,21 @@
2.66 done
2.67
2.68 lemma interval_open_subset_closed_cart:
2.69 - fixes a :: "'a::preorder^'n"
2.70 - shows "{a<..<b} \<subseteq> {a .. b}"
2.71 + fixes a :: "real^'n"
2.72 + shows "box a b \<subseteq> {a .. b}"
2.73 proof (simp add: subset_eq, rule)
2.74 fix x
2.75 - assume x: "x \<in>{a<..<b}"
2.76 + assume x: "x \<in>box a b"
2.77 { fix i
2.78 have "a $ i \<le> x $ i"
2.79 using x order_less_imp_le[of "a$i" "x$i"]
2.80 - by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
2.81 + by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis)
2.82 }
2.83 moreover
2.84 { fix i
2.85 have "x $ i \<le> b $ i"
2.86 using x order_less_imp_le[of "x$i" "b$i"]
2.87 - by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
2.88 + by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis)
2.89 }
2.90 ultimately
2.91 show "a \<le> x \<and> x \<le> b"
2.92 @@ -999,21 +999,21 @@
2.93 lemma subset_interval_cart:
2.94 fixes a :: "real^'n"
2.95 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)
2.96 - 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)
2.97 - 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)
2.98 - 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)
2.99 + 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)
2.100 + 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)
2.101 + 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)
2.102 using subset_interval[of c d a b] by (simp_all add: Basis_vec_def inner_axis)
2.103
2.104 lemma disjoint_interval_cart:
2.105 fixes a::"real^'n"
2.106 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)
2.107 - 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)
2.108 - 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)
2.109 - 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)
2.110 + 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)
2.111 + 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)
2.112 + 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)
2.113 using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis)
2.114
2.115 lemma inter_interval_cart:
2.116 - fixes a :: "'a::linorder^'n"
2.117 + fixes a :: "real^'n"
2.118 shows "{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
2.119 unfolding set_eq_iff and Int_iff and mem_interval_cart
2.120 by auto
3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 14:49:18 2013 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
3.3 @@ -3366,18 +3366,21 @@
3.4 ultimately show ?thesis by auto
3.5 qed
3.6
3.7 +lemma box_real: "box a b = {a<..<b::real}"
3.8 + by (force simp add: box_def)
3.9 +
3.10 lemma rel_interior_real_interval:
3.11 fixes a b :: real
3.12 assumes "a < b"
3.13 shows "rel_interior {a..b} = {a<..<b}"
3.14 proof -
3.15 - have "{a<..<b} \<noteq> {}"
3.16 + have "box a b \<noteq> {}"
3.17 using assms
3.18 unfolding set_eq_iff
3.19 - by (auto intro!: exI[of _ "(a + b) / 2"])
3.20 + by (auto intro!: exI[of _ "(a + b) / 2"] simp: box_def)
3.21 then show ?thesis
3.22 using interior_rel_interior_gen[of "{a..b}", symmetric]
3.23 - by (simp split: split_if_asm add: interior_closed_interval)
3.24 + by (simp split: split_if_asm add: interior_closed_interval box_real)
3.25 qed
3.26
3.27 lemma rel_interior_real_semiline:
3.28 @@ -5666,7 +5669,7 @@
3.29 shows "is_interval s \<Longrightarrow> connected s"
3.30 using is_interval_convex convex_connected by auto
3.31
3.32 -lemma convex_interval: "convex {a .. b}" "convex {a<..<b::'a::ordered_euclidean_space}"
3.33 +lemma convex_interval: "convex {a .. b}" "convex (box a (b::'a::ordered_euclidean_space))"
3.34 apply (rule_tac[!] is_interval_convex)
3.35 using is_interval_interval
3.36 apply auto
4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 16 14:49:18 2013 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Dec 16 17:08:22 2013 +0100
4.3 @@ -586,12 +586,12 @@
4.4
4.5 lemma frechet_derivative_unique_within_open_interval:
4.6 fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::real_normed_vector"
4.7 - assumes "x \<in> {a<..<b}"
4.8 - and "(f has_derivative f' ) (at x within {a<..<b})"
4.9 - and "(f has_derivative f'') (at x within {a<..<b})"
4.10 + assumes "x \<in> box a b"
4.11 + and "(f has_derivative f' ) (at x within box a b)"
4.12 + and "(f has_derivative f'') (at x within box a b)"
4.13 shows "f' = f''"
4.14 proof -
4.15 - from assms(1) have *: "at x within {a<..<b} = at x"
4.16 + from assms(1) have *: "at x within box a b = at x"
4.17 by (metis at_within_interior interior_open open_interval)
4.18 from assms(2,3) [unfolded *] show "f' = f''"
4.19 by (rule frechet_derivative_unique_at)
4.20 @@ -741,10 +741,10 @@
4.21 assumes "a < b"
4.22 and "f a = f b"
4.23 and "continuous_on {a..b} f"
4.24 - and "\<forall>x\<in>{a<..<b}. (f has_derivative f' x) (at x)"
4.25 - shows "\<exists>x\<in>{a<..<b}. f' x = (\<lambda>v. 0)"
4.26 + and "\<forall>x\<in>box a b. (f has_derivative f' x) (at x)"
4.27 + shows "\<exists>x\<in>box a b. f' x = (\<lambda>v. 0)"
4.28 proof -
4.29 - 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)"
4.30 + 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)"
4.31 proof -
4.32 have "(a + b) / 2 \<in> {a .. b}"
4.33 using assms(1) by auto
4.34 @@ -753,20 +753,20 @@
4.35 guess d using continuous_attains_sup[OF compact_interval * assms(3)] .. note d=this
4.36 guess c using continuous_attains_inf[OF compact_interval * assms(3)] .. note c=this
4.37 show ?thesis
4.38 - proof (cases "d \<in> {a<..<b} \<or> c \<in> {a<..<b}")
4.39 + proof (cases "d \<in> box a b \<or> c \<in> box a b")
4.40 case True
4.41 then show ?thesis
4.42 apply (erule_tac disjE)
4.43 apply (rule_tac x=d in bexI)
4.44 apply (rule_tac[3] x=c in bexI)
4.45 using d c
4.46 - apply auto
4.47 + apply (auto simp: box_real)
4.48 done
4.49 next
4.50 def e \<equiv> "(a + b) /2"
4.51 case False
4.52 then have "f d = f c"
4.53 - using d c assms(2) by auto
4.54 + using d c assms(2) by (auto simp: box_real)
4.55 then have "\<And>x. x \<in> {a..b} \<Longrightarrow> f x = f d"
4.56 using c d
4.57 apply -
4.58 @@ -777,13 +777,13 @@
4.59 apply (rule_tac x=e in bexI)
4.60 unfolding e_def
4.61 using assms(1)
4.62 - apply auto
4.63 + apply (auto simp: box_real)
4.64 done
4.65 qed
4.66 qed
4.67 then guess x .. note x=this
4.68 then have "f' x = (\<lambda>v. 0)"
4.69 - apply (rule_tac differential_zero_maxmin[of x "{a<..<b}" f "f' x"])
4.70 + apply (rule_tac differential_zero_maxmin[of x "box a b" f "f' x"])
4.71 defer
4.72 apply (rule open_interval)
4.73 apply (rule assms(4)[unfolded has_derivative_at[symmetric],THEN bspec[where x=x]])
4.74 @@ -813,10 +813,10 @@
4.75 assumes "\<forall>x\<in>{a<..<b}. (f has_derivative (f' x)) (at x)"
4.76 shows "\<exists>x\<in>{a<..<b}. f b - f a = (f' x) (b - a)"
4.77 proof -
4.78 - have "\<exists>x\<in>{a<..<b}. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
4.79 + have "\<exists>x\<in>box a b. (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)"
4.80 proof (intro rolle[OF assms(1), of "\<lambda>x. f x - (f b - f a) / (b - a) * x"] ballI)
4.81 fix x
4.82 - assume x: "x \<in> {a<..<b}"
4.83 + assume "x \<in> box a b" hence x: "x \<in> {a<..<b}" by (simp add: box_real)
4.84 show "((\<lambda>x. f x - (f b - f a) / (b - a) * x) has_derivative
4.85 (\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa)) (at x)"
4.86 by (intro FDERIV_intros assms(3)[rule_format,OF x] mult_right_has_derivative)
4.87 @@ -825,7 +825,7 @@
4.88 then show ?thesis
4.89 apply (rule_tac x=x in bexI)
4.90 apply (drule fun_cong[of _ _ "b - a"])
4.91 - apply auto
4.92 + apply (auto simp: box_real)
4.93 done
4.94 qed
4.95
4.96 @@ -841,13 +841,13 @@
4.97 defer
4.98 proof
4.99 fix x
4.100 - assume x: "x \<in> {a<..<b}"
4.101 + assume x: "x \<in> {a<..<b}" hence x: "x \<in> box a b" by (simp add: box_real)
4.102 show "(f has_derivative f' x) (at x)"
4.103 unfolding has_derivative_within_open[OF x open_interval,symmetric]
4.104 apply (rule has_derivative_within_subset)
4.105 apply (rule assms(2)[rule_format])
4.106 using x
4.107 - apply auto
4.108 + apply (auto simp: box_real)
4.109 done
4.110 qed (insert assms(2), auto)
4.111
4.112 @@ -963,8 +963,7 @@
4.113 apply auto
4.114 done
4.115 then show ?case
4.116 - unfolding has_derivative_within_open[OF goal1 open_interval]
4.117 - by auto
4.118 + unfolding has_derivative_within_open[OF goal1 open_greaterThanLessThan] .
4.119 qed
4.120 guess u using mvt_general[OF zero_less_one 1 2] .. note u = this
4.121 have **: "\<And>x y. x \<in> s \<Longrightarrow> norm (f' x y) \<le> B * norm y"
5.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Dec 16 14:49:18 2013 +0100
5.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Dec 16 17:08:22 2013 +0100
5.3 @@ -80,7 +80,7 @@
5.4 } note x0 = this
5.5 have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
5.6 using UNIV_2 by auto
5.7 - have 1: "{- 1<..<1::real^2} \<noteq> {}"
5.8 + have 1: "box (- 1) (1::real^2) \<noteq> {}"
5.9 unfolding interval_eq_empty_cart by auto
5.10 have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
5.11 apply (intro continuous_on_intros continuous_on_component)
5.12 @@ -344,7 +344,7 @@
5.13 by auto
5.14 next
5.15 have "{a..b} \<noteq> {}"
5.16 - using assms(3) using path_image_nonempty by auto
5.17 + using assms(3) using path_image_nonempty[of f] by auto
5.18 then have "a \<le> b"
5.19 unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
5.20 then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
5.21 @@ -646,7 +646,7 @@
5.22 obtains z where "z \<in> path_image f" and "z \<in> path_image g"
5.23 proof -
5.24 have "{a..b} \<noteq> {}"
5.25 - using path_image_nonempty using assms(3) by auto
5.26 + using path_image_nonempty[of f] using assms(3) by auto
5.27 note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
5.28 have "pathstart f \<in> {a..b}"
5.29 and "pathfinish f \<in> {a..b}"
5.30 @@ -692,7 +692,7 @@
5.31 using ab startfin abab assms(3)
5.32 using assms(9-)
5.33 unfolding assms
5.34 - apply (auto simp add: field_simps)
5.35 + apply (auto simp add: field_simps interval)
5.36 done
5.37 then show "path_image ?P1 \<subseteq> {?a .. ?b}" .
5.38 have "path_image ?P2 \<subseteq> {?a .. ?b}"
5.39 @@ -704,7 +704,7 @@
5.40 using ab startfin abab assms(4)
5.41 using assms(9-)
5.42 unfolding assms
5.43 - apply (auto simp add: field_simps)
5.44 + apply (auto simp add: field_simps interval)
5.45 done
5.46 then show "path_image ?P2 \<subseteq> {?a .. ?b}" .
5.47 show "a $ 1 - 2 = a $ 1 - 2"
6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 16 14:49:18 2013 +0100
6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Dec 16 17:08:22 2013 +0100
6.3 @@ -220,7 +220,8 @@
6.4 where "One \<equiv> \<Sum>Basis"
6.5
6.6 lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}"
6.7 - by (auto simp: set_eq_iff eucl_le[where 'a='a] intro!: bexI[OF _ SOME_Basis])
6.8 + apply (auto simp: eucl_le[where 'a='a])
6.9 + by (metis (mono_tags) eucl_less eucl_less_not_refl order.strict_trans2 zero_less_one)
6.10
6.11 lemma interior_subset_union_intervals:
6.12 assumes "i = {a..b::'a::ordered_euclidean_space}"
6.13 @@ -230,11 +231,11 @@
6.14 and "interior i \<inter> interior j = {}"
6.15 shows "interior i \<subseteq> interior s"
6.16 proof -
6.17 - have "{a<..<b} \<inter> {c..d} = {}"
6.18 + have "box a b \<inter> {c..d} = {}"
6.19 using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
6.20 unfolding assms(1,2) interior_closed_interval by auto
6.21 moreover
6.22 - have "{a<..<b} \<subseteq> {c..d} \<union> s"
6.23 + have "box a b \<subseteq> {c..d} \<union> s"
6.24 apply (rule order_trans,rule interval_open_subset_closed)
6.25 using assms(4) unfolding assms(1,2)
6.26 apply auto
6.27 @@ -310,9 +311,9 @@
6.28 then show ?thesis by auto
6.29 next
6.30 case True show ?thesis
6.31 - proof (cases "x\<in>{a<..<b}")
6.32 + proof (cases "x\<in>box a b")
6.33 case True
6.34 - then obtain d where "0 < d \<and> ball x d \<subseteq> {a<..<b}"
6.35 + then obtain d where "0 < d \<and> ball x d \<subseteq> box a b"
6.36 unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
6.37 then show ?thesis
6.38 apply (rule_tac x=i in bexI, rule_tac x=x in exI, rule_tac x="min d e" in exI)
6.39 @@ -1114,7 +1115,8 @@
6.40 obtain c d where k: "k = {c..d}"
6.41 using p(4)[OF goal1] by blast
6.42 have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
6.43 - using p(2,3)[OF goal1, unfolded k] using assms(2) by auto
6.44 + using p(2,3)[OF goal1, unfolded k] using assms(2)
6.45 + by auto
6.46 obtain q where "q division_of {a..b}" "{c..d} \<in> q"
6.47 by (rule partial_division_extend_1[OF *])
6.48 then show ?case
6.49 @@ -1324,7 +1326,7 @@
6.50 apply (rule assm(1)) unfolding Union_insert
6.51 using assm(2-4) as
6.52 apply -
6.53 - apply (fastforce dest: assm(5))+
6.54 + apply (fast dest: assm(5))+
6.55 done
6.56 next
6.57 assume as: "p \<noteq> {}" "interior {a..b} \<noteq> {}" "{a..b} \<noteq> {}"
6.58 @@ -2149,7 +2151,7 @@
6.59 unfolding s t interior_closed_interval
6.60 proof (rule *)
6.61 fix x
6.62 - assume "x \<in> {c<..<d}" "x \<in> {e<..<f}"
6.63 + assume "x \<in> box c d" "x \<in> box e f"
6.64 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"
6.65 unfolding mem_interval using i'
6.66 apply -
6.67 @@ -3274,7 +3276,7 @@
6.68 then have "{a .. b} = {}"
6.69 unfolding interval_eq_empty by (auto simp: eucl_le[where 'a='a] not_le)
6.70 then show ?thesis
6.71 - by auto
6.72 + by (auto simp: not_le)
6.73 qed
6.74
6.75 lemma division_split_left_inj:
6.76 @@ -3405,7 +3407,7 @@
6.77 apply -
6.78 prefer 3
6.79 apply (subst interval_split[OF k])
6.80 - apply auto
6.81 + apply (auto intro: order.trans)
6.82 done
6.83 fix k'
6.84 assume "k' \<in> ?p1"
6.85 @@ -3426,7 +3428,7 @@
6.86 apply -
6.87 prefer 3
6.88 apply (subst interval_split[OF k])
6.89 - apply auto
6.90 + apply (auto intro: order.trans)
6.91 done
6.92 fix k'
6.93 assume "k' \<in> ?p2"
6.94 @@ -3721,7 +3723,7 @@
6.95 apply (rule tagged_division_union[OF assms(1-2)])
6.96 unfolding interval_split[OF k] interior_closed_interval
6.97 using k
6.98 - apply (auto simp add: eucl_less[where 'a='a] elim!: ballE[where x=k])
6.99 + apply (auto simp add: eucl_less[where 'a='a] interval elim!: ballE[where x=k])
6.100 done
6.101 qed
6.102
6.103 @@ -6248,10 +6250,10 @@
6.104
6.105 subsection {* In particular, the boundary of an interval is negligible. *}
6.106
6.107 -lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - {a<..<b})"
6.108 +lemma negligible_frontier_interval: "negligible({a::'a::ordered_euclidean_space..b} - box a b)"
6.109 proof -
6.110 let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
6.111 - have "{a..b} - {a<..<b} \<subseteq> ?A"
6.112 + have "{a..b} - box a b \<subseteq> ?A"
6.113 apply rule unfolding Diff_iff mem_interval
6.114 apply simp
6.115 apply(erule conjE bexE)+
6.116 @@ -6267,7 +6269,7 @@
6.117 qed
6.118
6.119 lemma has_integral_spike_interior:
6.120 - assumes "\<forall>x\<in>{a<..<b}. g x = f x"
6.121 + assumes "\<forall>x\<in>box a b. g x = f x"
6.122 and "(f has_integral y) ({a..b})"
6.123 shows "(g has_integral y) {a..b}"
6.124 apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
6.125 @@ -6276,7 +6278,7 @@
6.126 done
6.127
6.128 lemma has_integral_spike_interior_eq:
6.129 - assumes "\<forall>x\<in>{a<..<b}. g x = f x"
6.130 + assumes "\<forall>x\<in>box a b. g x = f x"
6.131 shows "(f has_integral y) {a..b} \<longleftrightarrow> (g has_integral y) {a..b}"
6.132 apply rule
6.133 apply (rule_tac[!] has_integral_spike_interior)
6.134 @@ -6285,7 +6287,7 @@
6.135 done
6.136
6.137 lemma integrable_spike_interior:
6.138 - assumes "\<forall>x\<in>{a<..<b}. g x = f x"
6.139 + assumes "\<forall>x\<in>box a b. g x = f x"
6.140 and "f integrable_on {a..b}"
6.141 shows "g integrable_on {a..b}"
6.142 using assms
6.143 @@ -7029,7 +7031,7 @@
6.144 then show "f integrable_on k"
6.145 apply safe
6.146 apply (rule d[THEN conjunct2,rule_format,of x])
6.147 - apply auto
6.148 + apply (auto intro: order.trans)
6.149 done
6.150 qed
6.151 qed
6.152 @@ -7650,7 +7652,7 @@
6.153 fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
6.154 assumes "a \<le> b"
6.155 and "continuous_on {a..b} f"
6.156 - and "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
6.157 + and "\<forall>x\<in>box a b. (f has_vector_derivative f'(x)) (at x)"
6.158 shows "(f' has_integral (f b - f a)) {a..b}"
6.159 proof -
6.160 {
6.161 @@ -7682,7 +7684,7 @@
6.162 note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
6.163 note conjunctD2[OF this]
6.164 note bounded=this(1) and this(2)
6.165 - from this(2) have "\<forall>x\<in>{a<..<b}. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
6.166 + from this(2) have "\<forall>x\<in>box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
6.167 norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
6.168 apply -
6.169 apply safe
6.170 @@ -7885,8 +7887,8 @@
6.171 note result = as(2)[unfolded k interval_bounds_real[OF this(1)] content_real[OF this(1)]]
6.172
6.173 assume as': "x \<noteq> a" "x \<noteq> b"
6.174 - then have "x \<in> {a<..<b}"
6.175 - using p(2-3)[OF as(1)] by auto
6.176 + then have "x \<in> box a b"
6.177 + using p(2-3)[OF as(1)] by (auto simp: interval)
6.178 note * = d(2)[OF this]
6.179 have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
6.180 norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
6.181 @@ -8047,13 +8049,13 @@
6.182 assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
6.183 guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
6.184 guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
6.185 - have "{a <..< ?v} \<subseteq> k \<inter> k'"
6.186 - unfolding v v' by (auto simp add:)
6.187 + have "box a ?v \<subseteq> k \<inter> k'"
6.188 + unfolding v v' by (auto simp add: interval)
6.189 note interior_mono[OF this,unfolded interior_inter]
6.190 - moreover have "(a + ?v)/2 \<in> { a <..< ?v}"
6.191 + moreover have "(a + ?v)/2 \<in> box a ?v"
6.192 using k(3-)
6.193 unfolding v v' content_eq_0 not_le
6.194 - by (auto simp add: not_le)
6.195 + by (auto simp add: interval)
6.196 ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
6.197 unfolding interior_open[OF open_interval] by auto
6.198 then have *: "k = k'"
6.199 @@ -8078,11 +8080,11 @@
6.200 guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
6.201 guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this]
6.202 let ?v = "max v v'"
6.203 - have "{?v <..< b} \<subseteq> k \<inter> k'"
6.204 - unfolding v v' by auto
6.205 + have "box ?v b \<subseteq> k \<inter> k'"
6.206 + unfolding v v' by (auto simp: interval)
6.207 note interior_mono[OF this,unfolded interior_inter]
6.208 - moreover have " ((b + ?v)/2) \<in> {?v <..< b}"
6.209 - using k(3-) unfolding v v' content_eq_0 not_le by auto
6.210 + moreover have " ((b + ?v)/2) \<in> box ?v b"
6.211 + using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: interval)
6.212 ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
6.213 unfolding interior_open[OF open_interval] by auto
6.214 then have *: "k = k'"
6.215 @@ -8175,7 +8177,7 @@
6.216 assumes "finite s"
6.217 and "a \<le> b"
6.218 and "continuous_on {a..b} f"
6.219 - and "\<forall>x\<in>{a<..<b} - s. (f has_vector_derivative f'(x)) (at x)"
6.220 + and "\<forall>x\<in>box a b - s. (f has_vector_derivative f'(x)) (at x)"
6.221 shows "(f' has_integral (f b - f a)) {a..b}"
6.222 using assms
6.223 proof (induct "card s" arbitrary: s a b)
6.224 @@ -8196,7 +8198,7 @@
6.225 done
6.226 note cs = this[rule_format]
6.227 show ?case
6.228 - proof (cases "c \<in> {a<..<b}")
6.229 + proof (cases "c \<in> box a b")
6.230 case False
6.231 then show ?thesis
6.232 apply -
6.233 @@ -8213,7 +8215,7 @@
6.234 by auto
6.235 case True
6.236 then have "a \<le> c" "c \<le> b"
6.237 - by auto
6.238 + by (auto simp: interval)
6.239 then show ?thesis
6.240 apply (subst *)
6.241 apply (rule has_integral_combine)
6.242 @@ -8225,15 +8227,15 @@
6.243 show "continuous_on {a..c} f" "continuous_on {c..b} f"
6.244 apply (rule_tac[!] continuous_on_subset[OF Suc(5)])
6.245 using True
6.246 - apply auto
6.247 - done
6.248 - let ?P = "\<lambda>i j. \<forall>x\<in>{i<..<j} - s'. (f has_vector_derivative f' x) (at x)"
6.249 + apply (auto simp: interval)
6.250 + done
6.251 + let ?P = "\<lambda>i j. \<forall>x\<in>box i j - s'. (f has_vector_derivative f' x) (at x)"
6.252 show "?P a c" "?P c b"
6.253 apply safe
6.254 apply (rule_tac[!] Suc(6)[rule_format])
6.255 using True
6.256 unfolding cs
6.257 - apply auto
6.258 + apply (auto simp: interval)
6.259 done
6.260 qed auto
6.261 qed
6.262 @@ -8248,7 +8250,7 @@
6.263 shows "(f' has_integral (f(b) - f(a))) {a..b}"
6.264 apply (rule fundamental_theorem_of_calculus_interior_strong[OF assms(1-3), of f'])
6.265 using assms(4)
6.266 - apply auto
6.267 + apply (auto simp: interval)
6.268 done
6.269
6.270 lemma indefinite_integral_continuous_left:
6.271 @@ -8609,7 +8611,7 @@
6.272 apply (rule open_interval)
6.273 apply (rule has_derivative_within_subset[where s="{a..b}"])
6.274 using assms(4) assms(5)
6.275 - apply auto
6.276 + apply (auto simp: interval)
6.277 done
6.278 note this[unfolded *]
6.279 note has_integral_unique[OF has_integral_0 this]
6.280 @@ -8773,9 +8775,9 @@
6.281 fixes f :: "'a::ordered_euclidean_space \<Rightarrow> 'b::banach"
6.282 assumes "(f has_integral i) {c..d}"
6.283 and "{c..d} \<subseteq> {a..b}"
6.284 - shows "((\<lambda>x. if x \<in> {c<..<d} then f x else 0) has_integral i) {a..b}"
6.285 -proof -
6.286 - def g \<equiv> "\<lambda>x. if x \<in>{c<..<d} then f x else 0"
6.287 + shows "((\<lambda>x. if x \<in> box c d then f x else 0) has_integral i) {a..b}"
6.288 +proof -
6.289 + def g \<equiv> "\<lambda>x. if x \<in>box c d then f x else 0"
6.290 {
6.291 presume *: "{c..d} \<noteq> {} \<Longrightarrow> ?thesis"
6.292 show ?thesis
6.293 @@ -8784,7 +8786,7 @@
6.294 apply assumption
6.295 proof -
6.296 case goal1
6.297 - then have *: "{c<..<d} = {}"
6.298 + then have *: "box c d = {}"
6.299 using interval_open_subset_closed
6.300 by auto
6.301 show ?thesis
6.302 @@ -9812,7 +9814,7 @@
6.303 from d(5)[OF goal1] show ?case
6.304 unfolding obt interior_closed_interval
6.305 apply -
6.306 - apply (rule negligible_subset[of "({a..b}-{a<..<b}) \<union> ({c..d}-{c<..<d})"])
6.307 + apply (rule negligible_subset[of "({a..b}-box a b) \<union> ({c..d}-box c d)"])
6.308 apply (rule negligible_union negligible_frontier_interval)+
6.309 apply auto
6.310 done
6.311 @@ -9944,7 +9946,7 @@
6.312 case goal1
6.313 note tagged_division_ofD(3-4)[OF assms(2) this]
6.314 then show ?case
6.315 - using integrable_subinterval[OF assms(1)] by auto
6.316 + using integrable_subinterval[OF assms(1)] by blast
6.317 qed
6.318
6.319 lemma integral_combine_tagged_division_topdown:
7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 16 14:49:18 2013 +0100
7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 16 17:08:22 2013 +0100
7.3 @@ -826,7 +826,14 @@
7.4 unfolding dist_norm norm_eq_sqrt_inner setL2_def
7.5 by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
7.6
7.7 -definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
7.8 +definition (in euclidean_space) eucl_less (infix "<e" 50)
7.9 + where "eucl_less a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i)"
7.10 +
7.11 +definition box_eucl_less: "box a b = {x. a <e x \<and> x <e b}"
7.12 +
7.13 +lemma box_def: "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
7.14 + and in_box_eucl_less: "x \<in> box a b \<longleftrightarrow> a <e x \<and> x <e b"
7.15 + by (auto simp: box_eucl_less eucl_less_def)
7.16
7.17 lemma rational_boxes:
7.18 fixes x :: "'a\<Colon>euclidean_space"
7.19 @@ -2042,8 +2049,7 @@
7.20 by auto
7.21 then have "ball x (infdist x A) \<inter> closure A = {}"
7.22 apply auto
7.23 - apply (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
7.24 - eucl_less_not_refl euclidean_trans(2) infdist_le)
7.25 + apply (metis `x \<in> closure A` closure_approachable dist_commute infdist_le not_less)
7.26 done
7.27 then have "x \<notin> closure A"
7.28 by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
7.29 @@ -5992,25 +5998,25 @@
7.30
7.31 lemma interval:
7.32 fixes a :: "'a::ordered_euclidean_space"
7.33 - shows "{a <..< b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
7.34 + shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
7.35 and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
7.36 - by (auto simp add:set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
7.37 + by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
7.38
7.39 lemma mem_interval:
7.40 fixes a :: "'a::ordered_euclidean_space"
7.41 - shows "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
7.42 + shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
7.43 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)"
7.44 using interval[of a b]
7.45 - by (auto simp add: set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
7.46 + by auto
7.47
7.48 lemma interval_eq_empty:
7.49 fixes a :: "'a::ordered_euclidean_space"
7.50 - shows "({a <..< b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
7.51 + shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
7.52 and "({a .. b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
7.53 proof -
7.54 {
7.55 fix i x
7.56 - assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>{a <..< b}"
7.57 + assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
7.58 then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
7.59 unfolding mem_interval by auto
7.60 then have "a\<bullet>i < b\<bullet>i" by auto
7.61 @@ -6028,7 +6034,7 @@
7.62 then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
7.63 by (auto simp: inner_add_left)
7.64 }
7.65 - then have "{a <..< b} \<noteq> {}"
7.66 + then have "box a b \<noteq> {}"
7.67 using mem_interval(1)[of "?x" a b] by auto
7.68 }
7.69 ultimately show ?th1 by blast
7.70 @@ -6062,37 +6068,37 @@
7.71 lemma interval_ne_empty:
7.72 fixes a :: "'a::ordered_euclidean_space"
7.73 shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
7.74 - and "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
7.75 + and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
7.76 unfolding interval_eq_empty[of a b] by fastforce+
7.77
7.78 lemma interval_sing:
7.79 fixes a :: "'a::ordered_euclidean_space"
7.80 shows "{a .. a} = {a}"
7.81 - and "{a<..<a} = {}"
7.82 + and "box a a = {}"
7.83 unfolding set_eq_iff mem_interval eq_iff [symmetric]
7.84 by (auto intro: euclidean_eqI simp: ex_in_conv)
7.85
7.86 lemma subset_interval_imp:
7.87 fixes a :: "'a::ordered_euclidean_space"
7.88 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}"
7.89 - and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}"
7.90 - 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}"
7.91 - 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}"
7.92 + 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"
7.93 + 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}"
7.94 + 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"
7.95 unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
7.96 by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
7.97
7.98 lemma interval_open_subset_closed:
7.99 fixes a :: "'a::ordered_euclidean_space"
7.100 - shows "{a<..<b} \<subseteq> {a .. b}"
7.101 + shows "box a b \<subseteq> {a .. b}"
7.102 unfolding subset_eq [unfolded Ball_def] mem_interval
7.103 by (fast intro: less_imp_le)
7.104
7.105 lemma subset_interval:
7.106 fixes a :: "'a::ordered_euclidean_space"
7.107 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)
7.108 - 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)
7.109 - 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)
7.110 - 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)
7.111 + 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)
7.112 + 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)
7.113 + 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)
7.114 proof -
7.115 show ?th1
7.116 unfolding subset_eq and Ball_def and mem_interval
7.117 @@ -6101,8 +6107,8 @@
7.118 unfolding subset_eq and Ball_def and mem_interval
7.119 by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
7.120 {
7.121 - assume as: "{c<..<d} \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
7.122 - then have "{c<..<d} \<noteq> {}"
7.123 + assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
7.124 + then have "box c d \<noteq> {}"
7.125 unfolding interval_eq_empty by auto
7.126 fix i :: 'a
7.127 assume i: "i \<in> Basis"
7.128 @@ -6119,7 +6125,7 @@
7.129 apply (auto simp add: as2)
7.130 done
7.131 }
7.132 - then have "?x\<in>{c<..<d}"
7.133 + then have "?x\<in>box c d"
7.134 using i unfolding mem_interval by auto
7.135 moreover
7.136 have "?x \<notin> {a .. b}"
7.137 @@ -6145,7 +6151,7 @@
7.138 apply (auto simp add: as2)
7.139 done
7.140 }
7.141 - then have "?x\<in>{c<..<d}"
7.142 + then have "?x\<in>box c d"
7.143 unfolding mem_interval by auto
7.144 moreover
7.145 have "?x\<notin>{a .. b}"
7.146 @@ -6171,10 +6177,10 @@
7.147 apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
7.148 done
7.149 {
7.150 - assume as: "{c<..<d} \<subseteq> {a<..<b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
7.151 + assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
7.152 fix i :: 'a
7.153 assume i:"i\<in>Basis"
7.154 - from as(1) have "{c<..<d} \<subseteq> {a..b}"
7.155 + from as(1) have "box c d \<subseteq> {a..b}"
7.156 using interval_open_subset_closed[of a b] by auto
7.157 then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
7.158 using part1 and as(2) using i by auto
7.159 @@ -6200,9 +6206,9 @@
7.160 lemma disjoint_interval:
7.161 fixes a::"'a::ordered_euclidean_space"
7.162 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)
7.163 - 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)
7.164 - 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)
7.165 - 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)
7.166 + 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)
7.167 + 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)
7.168 + 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)
7.169 proof -
7.170 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"
7.171 have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
7.172 @@ -6219,14 +6225,14 @@
7.173
7.174 lemma open_interval[intro]:
7.175 fixes a b :: "'a::ordered_euclidean_space"
7.176 - shows "open {a<..<b}"
7.177 + shows "open (box a b)"
7.178 proof -
7.179 have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
7.180 by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
7.181 linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
7.182 - also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = {a<..<b}"
7.183 - by (auto simp add: eucl_less [where 'a='a])
7.184 - finally show "open {a<..<b}" .
7.185 + also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
7.186 + by (auto simp add: interval)
7.187 + finally show "open (box a b)" .
7.188 qed
7.189
7.190 lemma closed_interval[intro]:
7.191 @@ -6243,7 +6249,7 @@
7.192
7.193 lemma interior_closed_interval [intro]:
7.194 fixes a b :: "'a::ordered_euclidean_space"
7.195 - shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
7.196 + shows "interior {a..b} = box a b" (is "?L = ?R")
7.197 proof(rule subset_antisym)
7.198 show "?R \<subseteq> ?L"
7.199 using interval_open_subset_closed open_interval
7.200 @@ -6275,7 +6281,7 @@
7.201 using `e>0` i
7.202 by (auto simp: inner_diff_left inner_Basis inner_add_left)
7.203 }
7.204 - then have "x \<in> {a<..<b}"
7.205 + then have "x \<in> box a b"
7.206 unfolding mem_interval by auto
7.207 }
7.208 then show "?L \<subseteq> ?R" ..
7.209 @@ -6309,15 +6315,15 @@
7.210
7.211 lemma bounded_interval:
7.212 fixes a :: "'a::ordered_euclidean_space"
7.213 - shows "bounded {a .. b} \<and> bounded {a<..<b}"
7.214 + shows "bounded {a .. b} \<and> bounded (box a b)"
7.215 using bounded_closed_interval[of a b]
7.216 using interval_open_subset_closed[of a b]
7.217 - using bounded_subset[of "{a..b}" "{a<..<b}"]
7.218 + using bounded_subset[of "{a..b}" "box a b"]
7.219 by simp
7.220
7.221 lemma not_interval_univ:
7.222 fixes a :: "'a::ordered_euclidean_space"
7.223 - shows "{a .. b} \<noteq> UNIV \<and> {a<..<b} \<noteq> UNIV"
7.224 + shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
7.225 using bounded_interval[of a b] by auto
7.226
7.227 lemma compact_interval:
7.228 @@ -6328,8 +6334,8 @@
7.229
7.230 lemma open_interval_midpoint:
7.231 fixes a :: "'a::ordered_euclidean_space"
7.232 - assumes "{a<..<b} \<noteq> {}"
7.233 - shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
7.234 + assumes "box a b \<noteq> {}"
7.235 + shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
7.236 proof -
7.237 {
7.238 fix i :: 'a
7.239 @@ -6342,10 +6348,10 @@
7.240
7.241 lemma open_closed_interval_convex:
7.242 fixes x :: "'a::ordered_euclidean_space"
7.243 - assumes x: "x \<in> {a<..<b}"
7.244 + assumes x: "x \<in> box a b"
7.245 and y: "y \<in> {a .. b}"
7.246 and e: "0 < e" "e \<le> 1"
7.247 - shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> {a<..<b}"
7.248 + shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
7.249 proof -
7.250 {
7.251 fix i :: 'a
7.252 @@ -6392,14 +6398,11 @@
7.253
7.254 lemma closure_open_interval:
7.255 fixes a :: "'a::ordered_euclidean_space"
7.256 - assumes "{a<..<b} \<noteq> {}"
7.257 - shows "closure {a<..<b} = {a .. b}"
7.258 + assumes "box a b \<noteq> {}"
7.259 + shows "closure (box a b) = {a .. b}"
7.260 proof -
7.261 - have ab: "a < b"
7.262 - using assms[unfolded interval_ne_empty]
7.263 - apply (subst eucl_less)
7.264 - apply auto
7.265 - done
7.266 + have ab: "a <e b"
7.267 + using assms by (simp add: eucl_less_def interval_ne_empty)
7.268 let ?c = "(1 / 2) *\<^sub>R (a + b)"
7.269 {
7.270 fix x
7.271 @@ -6407,15 +6410,15 @@
7.272 def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
7.273 {
7.274 fix n
7.275 - assume fn: "f n < b \<longrightarrow> a < f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
7.276 + assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
7.277 have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
7.278 unfolding inverse_le_1_iff by auto
7.279 have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
7.280 x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
7.281 by (auto simp add: algebra_simps)
7.282 - then have "f n < b" and "a < f n"
7.283 + then have "f n <e b" and "a <e f n"
7.284 using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
7.285 - unfolding f_def by auto
7.286 + unfolding f_def by (auto simp: interval eucl_less_def)
7.287 then have False
7.288 using fn unfolding f_def using xc by auto
7.289 }
7.290 @@ -6448,11 +6451,11 @@
7.291 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
7.292 by auto
7.293 }
7.294 - ultimately have "x \<in> closure {a<..<b}"
7.295 + ultimately have "x \<in> closure (box a b)"
7.296 using as and open_interval_midpoint[OF assms]
7.297 unfolding closure_def
7.298 unfolding islimpt_sequential
7.299 - by (cases "x=?c") auto
7.300 + by (cases "x=?c") (auto simp: in_box_eucl_less)
7.301 }
7.302 then show ?thesis
7.303 using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
7.304 @@ -6461,7 +6464,7 @@
7.305 lemma bounded_subset_open_interval_symmetric:
7.306 fixes s::"('a::ordered_euclidean_space) set"
7.307 assumes "bounded s"
7.308 - shows "\<exists>a. s \<subseteq> {-a<..<a}"
7.309 + shows "\<exists>a. s \<subseteq> box (-a) a"
7.310 proof -
7.311 obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
7.312 using assms[unfolded bounded_pos] by auto
7.313 @@ -6478,12 +6481,12 @@
7.314 by auto
7.315 }
7.316 then show ?thesis
7.317 - by (auto intro: exI[where x=a] simp add: eucl_less[where 'a='a])
7.318 + by (auto intro: exI[where x=a] simp add: interval)
7.319 qed
7.320
7.321 lemma bounded_subset_open_interval:
7.322 fixes s :: "('a::ordered_euclidean_space) set"
7.323 - shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> {a<..<b})"
7.324 + shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
7.325 by (auto dest!: bounded_subset_open_interval_symmetric)
7.326
7.327 lemma bounded_subset_closed_interval_symmetric:
7.328 @@ -6491,7 +6494,7 @@
7.329 assumes "bounded s"
7.330 shows "\<exists>a. s \<subseteq> {-a .. a}"
7.331 proof -
7.332 - obtain a where "s \<subseteq> {- a<..<a}"
7.333 + obtain a where "s \<subseteq> box (-a) a"
7.334 using bounded_subset_open_interval_symmetric[OF assms] by auto
7.335 then show ?thesis
7.336 using interval_open_subset_closed[of "-a" a] by auto
7.337 @@ -6504,13 +6507,13 @@
7.338
7.339 lemma frontier_closed_interval:
7.340 fixes a b :: "'a::ordered_euclidean_space"
7.341 - shows "frontier {a .. b} = {a .. b} - {a<..<b}"
7.342 + shows "frontier {a .. b} = {a .. b} - box a b"
7.343 unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
7.344
7.345 lemma frontier_open_interval:
7.346 fixes a b :: "'a::ordered_euclidean_space"
7.347 - shows "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
7.348 -proof (cases "{a<..<b} = {}")
7.349 + shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
7.350 +proof (cases "box a b = {}")
7.351 case True
7.352 then show ?thesis
7.353 using frontier_empty by auto
7.354 @@ -6523,8 +6526,8 @@
7.355
7.356 lemma inter_interval_mixed_eq_empty:
7.357 fixes a :: "'a::ordered_euclidean_space"
7.358 - assumes "{c<..<d} \<noteq> {}"
7.359 - shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
7.360 + assumes "box c d \<noteq> {}"
7.361 + shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
7.362 unfolding closure_open_interval[OF assms, symmetric]
7.363 unfolding open_inter_closure_eq_empty[OF open_interval] ..
7.364
7.365 @@ -6577,7 +6580,7 @@
7.366 (\<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)"
7.367
7.368 lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
7.369 - "is_interval {a<..<b}" (is ?th2) proof -
7.370 + "is_interval (box a b)" (is ?th2) proof -
7.371 show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
7.372 by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
7.373
7.374 @@ -6705,13 +6708,13 @@
7.375
7.376 lemma eucl_lessThan_eq_halfspaces:
7.377 fixes a :: "'a\<Colon>ordered_euclidean_space"
7.378 - shows "{..<a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
7.379 - by (auto simp: eucl_less[where 'a='a])
7.380 + shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
7.381 + by (auto simp: eucl_less_def)
7.382
7.383 lemma eucl_greaterThan_eq_halfspaces:
7.384 fixes a :: "'a\<Colon>ordered_euclidean_space"
7.385 - shows "{a<..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
7.386 - by (auto simp: eucl_less[where 'a='a])
7.387 + shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
7.388 + by (auto simp: eucl_less_def)
7.389
7.390 lemma eucl_atMost_eq_halfspaces:
7.391 fixes a :: "'a\<Colon>ordered_euclidean_space"
7.392 @@ -6725,12 +6728,12 @@
7.393
7.394 lemma open_eucl_lessThan[simp, intro]:
7.395 fixes a :: "'a\<Colon>ordered_euclidean_space"
7.396 - shows "open {..< a}"
7.397 + shows "open {x. x <e a}"
7.398 by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
7.399
7.400 lemma open_eucl_greaterThan[simp, intro]:
7.401 fixes a :: "'a\<Colon>ordered_euclidean_space"
7.402 - shows "open {a <..}"
7.403 + shows "open {x. a <e x}"
7.404 by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
7.405
7.406 lemma closed_eucl_atMost[simp, intro]:
7.407 @@ -7101,7 +7104,7 @@
7.408 by auto
7.409 then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
7.410 using cs[unfolded complete_def, THEN spec[where x="x"]]
7.411 - using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1)
7.412 + using cauchy_isometric[OF `0 < e` s f normf] and cfg and x(1)
7.413 by auto
7.414 then have "\<exists>l\<in>f ` s. (g ---> l) sequentially"
7.415 using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l]
7.416 @@ -7628,4 +7631,7 @@
7.417
7.418 declare tendsto_const [intro] (* FIXME: move *)
7.419
7.420 +no_notation
7.421 + eucl_less (infix "<e" 50)
7.422 +
7.423 end
8.1 --- a/src/HOL/Probability/Borel_Space.thy Mon Dec 16 14:49:18 2013 +0100
8.2 +++ b/src/HOL/Probability/Borel_Space.thy Mon Dec 16 17:08:22 2013 +0100
8.3 @@ -237,18 +237,25 @@
8.4 by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
8.5 closed_atMost closed_atLeast closed_atLeastAtMost)+
8.6
8.7 +notation
8.8 + eucl_less (infix "<e" 50)
8.9 +
8.10 +lemma box_oc: "{x. a <e x \<and> x \<le> b} = {x. a <e x} \<inter> {..b}"
8.11 + and box_co: "{x. a \<le> x \<and> x <e b} = {a..} \<inter> {x. x <e b}"
8.12 + by auto
8.13 +
8.14 lemma eucl_ivals[measurable]:
8.15 fixes a b :: "'a\<Colon>ordered_euclidean_space"
8.16 - shows "{..< a} \<in> sets borel"
8.17 - and "{a <..} \<in> sets borel"
8.18 - and "{a<..<b} \<in> sets borel"
8.19 + shows "{x. x <e a} \<in> sets borel"
8.20 + and "{x. a <e x} \<in> sets borel"
8.21 + and "box a b \<in> sets borel"
8.22 and "{..a} \<in> sets borel"
8.23 and "{a..} \<in> sets borel"
8.24 and "{a..b} \<in> sets borel"
8.25 - and "{a<..b} \<in> sets borel"
8.26 - and "{a..<b} \<in> sets borel"
8.27 - unfolding greaterThanAtMost_def atLeastLessThan_def
8.28 - by (blast intro: borel_open borel_closed)+
8.29 + and "{x. a <e x \<and> x \<le> b} \<in> sets borel"
8.30 + and "{x. a \<le> x \<and> x <e b} \<in> sets borel"
8.31 + unfolding box_oc box_co
8.32 + by (auto intro: borel_open borel_closed)
8.33
8.34 lemma open_Collect_less:
8.35 fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
8.36 @@ -375,11 +382,6 @@
8.37 done
8.38 qed (auto simp: box_def)
8.39
8.40 -lemma borel_eq_greaterThanLessThan:
8.41 - "borel = sigma UNIV (range (\<lambda> (a, b). {a <..< b} :: 'a \<Colon> ordered_euclidean_space set))"
8.42 - unfolding borel_eq_box apply (rule arg_cong2[where f=sigma])
8.43 - by (auto simp: box_def image_iff mem_interval set_eq_iff simp del: greaterThanLessThan_iff)
8.44 -
8.45 lemma halfspace_gt_in_halfspace:
8.46 assumes i: "i \<in> A"
8.47 shows "{x\<Colon>'a. a < x \<bullet> i} \<in>
8.48 @@ -484,15 +486,15 @@
8.49 qed auto
8.50
8.51 lemma borel_eq_greaterThan:
8.52 - "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {a<..}))"
8.53 + "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. a <e x}))"
8.54 (is "_ = ?SIGMA")
8.55 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_le])
8.56 fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
8.57 then have i: "i \<in> Basis" by auto
8.58 have "{x::'a. x\<bullet>i \<le> a} = UNIV - {x::'a. a < x\<bullet>i}" by auto
8.59 also have *: "{x::'a. a < x\<bullet>i} =
8.60 - (\<Union>k::nat. {\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n <..})" using i
8.61 - proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
8.62 + (\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
8.63 + proof (safe, simp_all add: eucl_less_def split: split_if_asm)
8.64 fix x :: 'a
8.65 from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
8.66 guess k::nat .. note k = this
8.67 @@ -511,14 +513,14 @@
8.68 qed auto
8.69
8.70 lemma borel_eq_lessThan:
8.71 - "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {..<a}))"
8.72 + "borel = sigma UNIV (range (\<lambda>a\<Colon>'a\<Colon>ordered_euclidean_space. {x. x <e a}))"
8.73 (is "_ = ?SIGMA")
8.74 proof (rule borel_eq_sigmaI4[OF borel_eq_halfspace_ge])
8.75 fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
8.76 then have i: "i \<in> Basis" by auto
8.77 have "{x::'a. a \<le> x\<bullet>i} = UNIV - {x::'a. x\<bullet>i < a}" by auto
8.78 - 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`
8.79 - proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm)
8.80 + 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`
8.81 + proof (safe, simp_all add: eucl_less_def split: split_if_asm)
8.82 fix x :: 'a
8.83 from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
8.84 guess k::nat .. note k = this
8.85 @@ -532,7 +534,7 @@
8.86 finally show "{x. a \<le> x\<bullet>i} \<in> ?SIGMA"
8.87 apply (simp only:)
8.88 apply (safe intro!: sets.countable_UN sets.Diff)
8.89 - apply (auto intro: sigma_sets_top)
8.90 + apply (auto intro: sigma_sets_top )
8.91 done
8.92 qed auto
8.93
8.94 @@ -558,6 +560,9 @@
8.95 (auto intro!: sigma_sets_top)
8.96 qed auto
8.97
8.98 +lemma eucl_lessThan: "{x::real. x <e a} = lessThan a"
8.99 + by (simp add: eucl_less_def lessThan_def)
8.100 +
8.101 lemma borel_eq_atLeastLessThan:
8.102 "borel = sigma UNIV (range (\<lambda>(a, b). {a ..< b :: real}))" (is "_ = ?SIGMA")
8.103 proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan])
8.104 @@ -565,8 +570,8 @@
8.105 fix x :: real
8.106 have "{..<x} = (\<Union>i::nat. {-real i ..< x})"
8.107 by (auto simp: move_uminus real_arch_simple)
8.108 - then show "{..< x} \<in> ?SIGMA"
8.109 - by (auto intro: sigma_sets.intros)
8.110 + then show "{y. y <e x} \<in> ?SIGMA"
8.111 + by (auto intro: sigma_sets.intros simp: eucl_lessThan)
8.112 qed auto
8.113
8.114 lemma borel_eq_closed: "borel = sigma UNIV (Collect closed)"
8.115 @@ -1195,4 +1200,7 @@
8.116 shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
8.117 unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
8.118
8.119 +no_notation
8.120 + eucl_less (infix "<e" 50)
8.121 +
8.122 end
9.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 16 14:49:18 2013 +0100
9.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Dec 16 17:08:22 2013 +0100
9.3 @@ -916,16 +916,15 @@
9.4 proof (subst sigma_prod_algebra_sigma_eq[where S="\<lambda>_ i::nat. {..<real i}" and E="\<lambda>_. range lessThan", OF I])
9.5 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"
9.6 by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
9.7 -qed (auto simp: borel_eq_lessThan reals_Archimedean2)
9.8 +qed (auto simp: borel_eq_lessThan eucl_lessThan reals_Archimedean2)
9.9
9.10 lemma measurable_e2p[measurable]:
9.11 "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^sub>M (i::'a)\<in>Basis. (lborel :: real measure))"
9.12 proof (rule measurable_sigma_sets[OF sets_product_borel])
9.13 fix A :: "('a \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i} |x. True} "
9.14 then obtain x where "A = (\<Pi>\<^sub>E (i::'a)\<in>Basis. {..<x i})" by auto
9.15 - then have "e2p -` A = {..< (\<Sum>i\<in>Basis. x i *\<^sub>R i) :: 'a}"
9.16 - using DIM_positive by (auto simp add: set_eq_iff e2p_def
9.17 - euclidean_eq_iff[where 'a='a] eucl_less[where 'a='a])
9.18 + then have "e2p -` A = {y :: 'a. eucl_less y (\<Sum>i\<in>Basis. x i *\<^sub>R i)}"
9.19 + using DIM_positive by (auto simp add: set_eq_iff e2p_def eucl_less_def)
9.20 then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
9.21 qed (auto simp: e2p_def)
9.22