# HG changeset patch # User immler # Date 1387210102 -3600 # Node ID 2d3df8633dad6fb6cf065c153b25fe9f8496144c # Parent 81290fe85890e562e6488ccf1bc1909d54d159fc prefer box over greaterThanLessThan on euclidean_space diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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} \ {}" using assms by auto with i have *: "a\i \ b\i" "u\i \ v\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\i\x\i" "x\i\b\i" using assms(1)[unfolded mem_interval] using i by auto have "0 \ (x \ i - a \ i) / (b \ i - a \ i) * (v \ i - u \ i)" diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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. \i. a$i < x$i \ x$i < b$i}" - and "{a .. b} = {x::'a^'n. \i. a$i \ x$i \ x$i \ 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. \i. a$i < x$i \ x$i < b$i}" + and "{a .. b} = {x::real^'n. \i. a$i \ x$i \ x$i \ 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 \ {a<.. (\i. a$i < x$i \ x$i < b$i)" + fixes a :: "real^'n" + shows "x \ box a b \ (\i. a$i < x$i \ x$i < b$i)" and "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ 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} = {} \ (\i. b$i \ a$i))" (is ?th1) + shows "(box a b = {} \ (\i. b$i \ a$i))" (is ?th1) and "({a .. b} = {} \ (\i. b$i < a$i))" (is ?th2) proof - - { fix i x assume as:"b$i \ a$i" and x:"x\{a <..< b}" + { fix i x assume as:"b$i \ a$i" and x:"x\box a b" hence "a $ i < x $ i \ 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} \ {}" using mem_interval_cart(1)[of "?x" a b] by auto } + hence "box a b \ {}" 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\{a .. b}" @@ -953,16 +953,16 @@ lemma interval_ne_empty_cart: fixes a :: "real^'n" shows "{a .. b} \ {} \ (\i. a$i \ b$i)" - and "{a <..< b} \ {} \ (\i. a$i < b$i)" + and "box a b \ {} \ (\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 "(\i. a$i \ c$i \ d$i \ b$i) \ {c .. d} \ {a .. b}" - and "(\i. a$i < c$i \ d$i < b$i) \ {c .. d} \ {a<..i. a$i \ c$i \ d$i \ b$i) \ {c<.. {a .. b}" - and "(\i. a$i \ c$i \ d$i \ b$i) \ {c<.. {a<..i. a$i < c$i \ d$i < b$i) \ {c .. d} \ box a b" + and "(\i. a$i \ c$i \ d$i \ b$i) \ box c d \ {a .. b}" + and "(\i. a$i \ c$i \ d$i \ b$i) \ box c d \ 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<.. {a .. b}" + fixes a :: "real^'n" + shows "box a b \ {a .. b}" proof (simp add: subset_eq, rule) fix x - assume x: "x \{a<..box a b" { fix i have "a $ i \ 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 \ 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 \ x \ x \ b" @@ -999,21 +999,21 @@ lemma subset_interval_cart: fixes a :: "real^'n" shows "{c .. d} \ {a .. b} \ (\i. c$i \ d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th1) - and "{c .. d} \ {a<.. (\i. c$i \ d$i) --> (\i. a$i < c$i \ d$i < b$i)" (is ?th2) - and "{c<.. {a .. b} \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th3) - and "{c<.. {a<.. (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th4) + and "{c .. d} \ box a b \ (\i. c$i \ d$i) --> (\i. a$i < c$i \ d$i < b$i)" (is ?th2) + and "box c d \ {a .. b} \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th3) + and "box c d \ box a b \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ 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} \ {c .. d} = {} \ (\i. (b$i < a$i \ d$i < c$i \ b$i < c$i \ d$i < a$i))" (is ?th1) - and "{a .. b} \ {c<.. (\i. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) - and "{a<.. {c .. d} = {} \ (\i. (b$i \ a$i \ d$i < c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th3) - and "{a<.. {c<.. (\i. (b$i \ a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th4) + and "{a .. b} \ box c d = {} \ (\i. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) + and "box a b \ {c .. d} = {} \ (\i. (b$i \ a$i \ d$i < c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th3) + and "box a b \ box c d = {} \ (\i. (b$i \ a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ 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} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" unfolding set_eq_iff and Int_iff and mem_interval_cart by auto diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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<.. {}" + have "box a b \ {}" 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 \ connected s" using is_interval_convex convex_connected by auto -lemma convex_interval: "convex {a .. b}" "convex {a<.. 'b::real_normed_vector" - assumes "x \ {a<.. 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<..x\{a<..x\{a<..v. 0)" + and "\x\box a b. (f has_derivative f' x) (at x)" + shows "\x\box a b. f' x = (\v. 0)" proof - - have "\x\{a<..y\{a<.. f y) \ (\y\{a<.. f x)" + have "\x\box a b. (\y\box a b. f x \ f y) \ (\y\box a b. f y \ f x)" proof - have "(a + b) / 2 \ {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 \ {a<.. c \ {a<.. box a b \ c \ 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 \ "(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 "\x. x \ {a..b} \ 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 = (\v. 0)" - apply (rule_tac differential_zero_maxmin[of x "{a<..x\{a<..x\{a<..x\{a<..xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" + have "\x\box a b. (\xa. f' x xa - (f b - f a) / (b - a) * xa) = (\v. 0)" proof (intro rolle[OF assms(1), of "\x. f x - (f b - f a) / (b - a) * x"] ballI) fix x - assume x: "x \ {a<.. box a b" hence x: "x \ {a<..x. f x - (f b - f a) / (b - a) * x) has_derivative (\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 \ {a<.. {a<.. 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 **: "\x y. x \ s \ norm (f' x y) \ B * norm y" diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Fashoda.thy --- 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: "\i::2. i \ 1 \ i = 2" using UNIV_2 by auto - have 1: "{- 1<..<1::real^2} \ {}" + have 1: "box (- 1) (1::real^2) \ {}" unfolding interval_eq_empty_cart by auto have 2: "continuous_on {- 1..1} (negatex \ sqprojection \ ?F)" apply (intro continuous_on_intros continuous_on_component) @@ -344,7 +344,7 @@ by auto next have "{a..b} \ {}" - using assms(3) using path_image_nonempty by auto + using assms(3) using path_image_nonempty[of f] by auto then have "a \ b" unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less) then show "a$1 = b$1 \ a$2 = b$2 \ (a$1 < b$1 \ a$2 < b$2)" @@ -646,7 +646,7 @@ obtains z where "z \ path_image f" and "z \ path_image g" proof - have "{a..b} \ {}" - 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 \ {a..b}" and "pathfinish f \ {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 \ {?a .. ?b}" . have "path_image ?P2 \ {?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 \ {?a .. ?b}" . show "a $ 1 - 2 = a $ 1 - 2" diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ \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 \ interior j = {}" shows "interior i \ interior s" proof - - have "{a<.. {c..d} = {}" + have "box a b \ {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<.. {c..d} \ s" + have "box a b \ {c..d} \ 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\{a<..box a b") case True - then obtain d where "0 < d \ ball x d \ {a<.. ball x d \ 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} \ {a..b}" "{c..d} \ {}" - 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} \ 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 \ {}" "interior {a..b} \ {}" "{a..b} \ {}" @@ -2149,7 +2151,7 @@ unfolding s t interior_closed_interval proof (rule *) fix x - assume "x \ {c<.. {e<.. box c d" "x \ box e f" then have x: "c\i < d\i" "e\i < f\i" "c\i < f\i" "e\i < d\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' \ ?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' \ ?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<.. ?A" + have "{a..b} - box a b \ ?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 "\x\{a<..x\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 "\x\{a<..x\box a b. g x = f x" shows "(f has_integral y) {a..b} \ (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 "\x\{a<..x\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 \ 'a::real_normed_vector" assumes "a \ b" and "continuous_on {a..b} f" - and "\x\{a<..x\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 "\x\{a<..d>0. \y. norm (y - x) < d \ + from this(2) have "\x\box a b. \d>0. \y. norm (y - x) < d \ norm (f y - f x - (y - x) *\<^sub>R f' x) \ 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 \ a" "x \ b" - then have "x \ {a<.. 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) \ p" "(a, k') \ p" "content k \ 0" "content k' \ 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} \ k \ k'" - unfolding v v' by (auto simp add:) + have "box a ?v \ k \ k'" + unfolding v v' by (auto simp add: interval) note interior_mono[OF this,unfolded interior_inter] - moreover have "(a + ?v)/2 \ { a <..< ?v}" + moreover have "(a + ?v)/2 \ 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 \ interior k \ 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} \ k \ k'" - unfolding v v' by auto + have "box ?v b \ k \ k'" + unfolding v v' by (auto simp: interval) note interior_mono[OF this,unfolded interior_inter] - moreover have " ((b + ?v)/2) \ {?v <..< b}" - using k(3-) unfolding v v' content_eq_0 not_le by auto + moreover have " ((b + ?v)/2) \ box ?v b" + using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: interval) ultimately have " ((b + ?v)/2) \ interior k \ interior k'" unfolding interior_open[OF open_interval] by auto then have *: "k = k'" @@ -8175,7 +8177,7 @@ assumes "finite s" and "a \ b" and "continuous_on {a..b} f" - and "\x\{a<..x\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 \ {a<.. box a b") case False then show ?thesis apply - @@ -8213,7 +8215,7 @@ by auto case True then have "a \ c" "c \ 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 = "\i j. \x\{i<.. 'b::banach" assumes "(f has_integral i) {c..d}" and "{c..d} \ {a..b}" - shows "((\x. if x \ {c<.. "\x. if x \{c<..x. if x \ box c d then f x else 0) has_integral i) {a..b}" +proof - + def g \ "\x. if x \box c d then f x else 0" { presume *: "{c..d} \ {} \ ?thesis" show ?thesis @@ -8784,7 +8786,7 @@ apply assumption proof - case goal1 - then have *: "{c<.. ({c..d}-{c<.. ({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: diff -r 81290fe85890 -r 2d3df8633dad src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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. \i\Basis. a \ i < x \ i \ x \ i < b \ i}" +definition (in euclidean_space) eucl_less (infix " (\i\Basis. a \ i < b \ i)" + +definition box_eucl_less: "box a b = {x. a x i\Basis. a \ i < x \ i \ x \ i < b \ i}" + and in_box_eucl_less: "x \ box a b \ a x euclidean_space" @@ -2042,8 +2049,7 @@ by auto then have "ball x (infdist x A) \ closure A = {}" apply auto - apply (metis `0 < infdist x A` `x \ closure A` closure_approachable dist_commute - eucl_less_not_refl euclidean_trans(2) infdist_le) + apply (metis `x \ closure A` closure_approachable dist_commute infdist_le not_less) done then have "x \ 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. \i\Basis. a\i < x\i \ x\i < b\i}" + shows "box a b = {x::'a. \i\Basis. a\i < x\i \ x\i < b\i}" and "{a .. b} = {x::'a. \i\Basis. a\i \ x\i \ x\i \ b\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 \ {a<.. (\i\Basis. a\i < x\i \ x\i < b\i)" + shows "x \ box a b \ (\i\Basis. a\i < x\i \ x\i < b\i)" and "x \ {a .. b} \ (\i\Basis. a\i \ x\i \ x\i \ b\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} = {} \ (\i\Basis. b\i \ a\i))" (is ?th1) + shows "(box a b = {} \ (\i\Basis. b\i \ a\i))" (is ?th1) and "({a .. b} = {} \ (\i\Basis. b\i < a\i))" (is ?th2) proof - { fix i x - assume i: "i\Basis" and as:"b\i \ a\i" and x:"x\{a <..< b}" + assume i: "i\Basis" and as:"b\i \ a\i" and x:"x\box a b" then have "a \ i < x \ i \ x \ i < b \ i" unfolding mem_interval by auto then have "a\i < b\i" by auto @@ -6028,7 +6034,7 @@ then have "a\i < ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i < b\i" by (auto simp: inner_add_left) } - then have "{a <..< b} \ {}" + then have "box a b \ {}" 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} \ {} \ (\i\Basis. a\i \ b\i)" - and "{a <..< b} \ {} \ (\i\Basis. a\i < b\i)" + and "box a b \ {} \ (\i\Basis. a\i < b\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<..i\Basis. a\i \ c\i \ d\i \ b\i) \ {c .. d} \ {a .. b}" - and "(\i\Basis. a\i < c\i \ d\i < b\i) \ {c .. d} \ {a<..i\Basis. a\i \ c\i \ d\i \ b\i) \ {c<.. {a .. b}" - and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ {c<.. {a<..i\Basis. a\i < c\i \ d\i < b\i) \ {c .. d} \ box a b" + and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ {a .. b}" + and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ 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<.. {a .. b}" + shows "box a b \ {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} \ {a .. b} \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th1) - and "{c .. d} \ {a<.. (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) - and "{c<.. {a .. b} \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) - and "{c<.. {a<.. (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th4) + and "{c .. d} \ box a b \ (\i\Basis. c\i \ d\i) --> (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) + and "box c d \ {a .. b} \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) + and "box c d \ box a b \ (\i\Basis. c\i < d\i) --> (\i\Basis. a\i \ c\i \ d\i \ b\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<.. {a .. b}" "\i\Basis. c\i < d\i" - then have "{c<.. {}" + assume as: "box c d \ {a .. b}" "\i\Basis. c\i < d\i" + then have "box c d \ {}" unfolding interval_eq_empty by auto fix i :: 'a assume i: "i \ Basis" @@ -6119,7 +6125,7 @@ apply (auto simp add: as2) done } - then have "?x\{c<..box c d" using i unfolding mem_interval by auto moreover have "?x \ {a .. b}" @@ -6145,7 +6151,7 @@ apply (auto simp add: as2) done } - then have "?x\{c<..box c d" unfolding mem_interval by auto moreover have "?x\{a .. b}" @@ -6171,10 +6177,10 @@ apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+ done { - assume as: "{c<.. {a<..i\Basis. c\i < d\i" + assume as: "box c d \ box a b" "\i\Basis. c\i < d\i" fix i :: 'a assume i:"i\Basis" - from as(1) have "{c<.. {a..b}" + from as(1) have "box c d \ {a..b}" using interval_open_subset_closed[of a b] by auto then have "a\i \ c\i \ d\i \ b\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} \ {c .. d} = {} \ (\i\Basis. (b\i < a\i \ d\i < c\i \ b\i < c\i \ d\i < a\i))" (is ?th1) - and "{a .. b} \ {c<.. (\i\Basis. (b\i < a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th2) - and "{a<.. {c .. d} = {} \ (\i\Basis. (b\i \ a\i \ d\i < c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th3) - and "{a<.. {c<.. (\i\Basis. (b\i \ a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th4) + and "{a .. b} \ box c d = {} \ (\i\Basis. (b\i < a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th2) + and "box a b \ {c .. d} = {} \ (\i\Basis. (b\i \ a\i \ d\i < c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th3) + and "box a b \ box c d = {} \ (\i\Basis. (b\i \ a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th4) proof - let ?z = "(\i\Basis. (((max (a\i) (c\i)) + (min (b\i) (d\i))) / 2) *\<^sub>R i)::'a" have **: "\P Q. (\i :: 'a. i \ Basis \ Q ?z i \ P i) \ @@ -6219,14 +6225,14 @@ lemma open_interval[intro]: fixes a b :: "'a::ordered_euclidean_space" - shows "open {a<..i\Basis. (\x. x\i) -` {a\i<..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 "(\i\Basis. (\x. x\i) -` {a\i<..i}) = {a<.. ?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 \ {a<.. box a b" unfolding mem_interval by auto } then show "?L \ ?R" .. @@ -6309,15 +6315,15 @@ lemma bounded_interval: fixes a :: "'a::ordered_euclidean_space" - shows "bounded {a .. b} \ bounded {a<.. 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<.. UNIV \ {a<.. UNIV" + shows "{a .. b} \ UNIV \ box a b \ 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<.. {}" - shows "((1/2) *\<^sub>R (a + b)) \ {a<.. {}" + shows "((1/2) *\<^sub>R (a + b)) \ 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 \ {a<.. box a b" and y: "y \ {a .. b}" and e: "0 < e" "e \ 1" - shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ {a<..R x + (1 - e) *\<^sub>R y) \ box a b" proof - { fix i :: 'a @@ -6392,14 +6398,11 @@ lemma closure_open_interval: fixes a :: "'a::ordered_euclidean_space" - assumes "{a<.. {}" - shows "closure {a<.. {}" + 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 "\n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)" { fix n - assume fn: "f n < b \ a < f n \ f n = x" and xc: "x \ ?c" + assume fn: "f n a f n = x" and xc: "x \ ?c" have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \ 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 n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } - ultimately have "x \ closure {a<.. 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 "\a. s \ {-a<..a. s \ box (-a) a" proof - obtain b where "b>0" and b: "\x\s. norm x \ 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 \ (\a b. s \ {a<.. (\a b. s \ 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 "\a. s \ {-a .. a}" proof - - obtain a where "s \ {- a<.. 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<.. {}" - shows "{a<.. {c .. d} = {} \ {a<.. {c<.. {}" + shows "box a b \ {c .. d} = {} \ box a b \ box c d = {}" unfolding closure_open_interval[OF assms, symmetric] unfolding open_inter_closure_eq_empty[OF open_interval] .. @@ -6577,7 +6580,7 @@ (\a\s. \b\s. \x. (\i\Basis. ((a\i \ x\i \ x\i \ b\i) \ (b\i \ x\i \ x\i \ a\i))) \ x \ s)" lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1) - "is_interval {a<..ordered_euclidean_space" - shows "{..i\Basis. {x. x \ i < a \ i})" - by (auto simp: eucl_less[where 'a='a]) + shows "{x. x i\Basis. {x. x \ i < a \ i})" + by (auto simp: eucl_less_def) lemma eucl_greaterThan_eq_halfspaces: fixes a :: "'a\ordered_euclidean_space" - shows "{a<..} = (\i\Basis. {x. a \ i < x \ i})" - by (auto simp: eucl_less[where 'a='a]) + shows "{x. a i\Basis. {x. a \ i < x \ i})" + by (auto simp: eucl_less_def) lemma eucl_atMost_eq_halfspaces: fixes a :: "'a\ordered_euclidean_space" @@ -6725,12 +6728,12 @@ lemma open_eucl_lessThan[simp, intro]: fixes a :: "'a\ordered_euclidean_space" - shows "open {..< a}" + shows "open {x. x ordered_euclidean_space" - shows "open {a <..}" + shows "open {x. a s" and l:"(x ---> l) sequentially" using cs[unfolded complete_def, THEN spec[where x="x"]] - using cauchy_isometric[OF `0l\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 " x \ b} = {x. a {..b}" + and box_co: "{x. a \ x \ x {x. x ordered_euclidean_space" - shows "{..< a} \ sets borel" - and "{a <..} \ sets borel" - and "{a<.. sets borel" + shows "{x. x sets borel" + and "{x. a sets borel" + and "box a b \ sets borel" and "{..a} \ sets borel" and "{a..} \ sets borel" and "{a..b} \ sets borel" - and "{a<..b} \ sets borel" - and "{a.. sets borel" - unfolding greaterThanAtMost_def atLeastLessThan_def - by (blast intro: borel_open borel_closed)+ + and "{x. a x \ b} \ sets borel" + and "{x. a \ x \ x sets borel" + unfolding box_oc box_co + by (auto intro: borel_open borel_closed) lemma open_Collect_less: fixes f g :: "'i::topological_space \ 'a :: {dense_linorder, linorder_topology}" @@ -375,11 +382,6 @@ done qed (auto simp: box_def) -lemma borel_eq_greaterThanLessThan: - "borel = sigma UNIV (range (\ (a, b). {a <..< b} :: 'a \ 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 \ A" shows "{x\'a. a < x \ i} \ @@ -484,15 +486,15 @@ qed auto lemma borel_eq_greaterThan: - "borel = sigma UNIV (range (\a\'a\ordered_euclidean_space. {a<..}))" + "borel = sigma UNIV (range (\a\'a\ordered_euclidean_space. {x. a UNIV \ Basis" then have i: "i \ Basis" by auto have "{x::'a. x\i \ a} = UNIV - {x::'a. a < x\i}" by auto also have *: "{x::'a. a < x\i} = - (\k::nat. {\n\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) + (\k::nat. {x. (\n\Basis. (if n = i then a else -real k) *\<^sub>R n) i. -x\i)`Basis)"] guess k::nat .. note k = this @@ -511,14 +513,14 @@ qed auto lemma borel_eq_lessThan: - "borel = sigma UNIV (range (\a\'a\ordered_euclidean_space. {..a\'a\ordered_euclidean_space. {x. x UNIV \ Basis" then have i: "i \ Basis" by auto have "{x::'a. a \ x\i} = UNIV - {x::'a. x\i < a}" by auto - also have *: "{x::'a. x\i < a} = (\k::nat. {..< \n\Basis. (if n = i then a else real k) *\<^sub>R n})" using `i\ Basis` - proof (safe, simp_all add: eucl_less[where 'a='a] split: split_if_asm) + also have *: "{x::'a. x\i < a} = (\k::nat. {x. x n\Basis. (if n = i then a else real k) *\<^sub>R n)})" using `i\ Basis` + proof (safe, simp_all add: eucl_less_def split: split_if_asm) fix x :: 'a from reals_Archimedean2[of "Max ((\i. x\i)`Basis)"] guess k::nat .. note k = this @@ -532,7 +534,7 @@ finally show "{x. a \ x\i} \ ?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 (a, b). {a ..< b :: real}))" (is "_ = ?SIGMA") proof (rule borel_eq_sigmaI5[OF borel_eq_lessThan]) @@ -565,8 +570,8 @@ fix x :: real have "{..i::nat. {-real i ..< x})" by (auto simp: move_uminus real_arch_simple) - then show "{..< x} \ ?SIGMA" - by (auto intro: sigma_sets.intros) + then show "{y. y ?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 "(\x. suminf (\i. f i x)) \ borel_measurable M" unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp +no_notation + eucl_less (infix "M I (\i. lborel))) {Pi\<^sub>E I F |F. \i\I. F i \ 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 \ measurable (borel::'a::ordered_euclidean_space measure) (\\<^sub>M (i::'a)\Basis. (lborel :: real measure))" proof (rule measurable_sigma_sets[OF sets_product_borel]) fix A :: "('a \ real) set" assume "A \ {\\<^sub>E (i::'a)\Basis. {..\<^sub>E (i::'a)\Basis. {..i\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 (\i\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 \ space (borel::'a measure) \ sets borel" by simp qed (auto simp: e2p_def)