# HG changeset patch # User huffman # Date 1313165844 25200 # Node ID 510ac30f44c088598e5a9e799de0002c5e0162a3 # Parent bdcc11b2fdc8663b277aa1e1adbeff6e362d9716 make Multivariate_Analysis work with separate set type diff -r bdcc11b2fdc8 -r 510ac30f44c0 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 07:18:28 2011 -0700 +++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 09:17:24 2011 -0700 @@ -1370,7 +1370,7 @@ } moreover { assume "?lhs" hence "?rhs" - by (metis Collect_def Collect_mem_eq SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff + by (metis SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8)) } ultimately show ?thesis by auto qed @@ -1390,7 +1390,7 @@ } moreover { assume "?lhs" hence "?rhs" - by (metis Collect_def Collect_mem_eq le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff + by (metis le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8)) } ultimately show ?thesis by auto qed @@ -2210,21 +2210,20 @@ qed qed auto -lemma (in order) mono_set: - "mono S \ (\x y. x \ y \ x \ S \ y \ S)" - by (auto simp: mono_def mem_def) +definition (in order) mono_set: + "mono_set S \ (\x y. x \ y \ x \ S \ y \ S)" -lemma (in order) mono_greaterThan [intro, simp]: "mono {B<..}" unfolding mono_set by auto -lemma (in order) mono_atLeast [intro, simp]: "mono {B..}" unfolding mono_set by auto -lemma (in order) mono_UNIV [intro, simp]: "mono UNIV" unfolding mono_set by auto -lemma (in order) mono_empty [intro, simp]: "mono {}" unfolding mono_set by auto +lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto +lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto +lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto +lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto lemma (in complete_linorder) mono_set_iff: fixes S :: "'a set" defines "a \ Inf S" - shows "mono S \ (S = {a <..} \ S = {a..})" (is "_ = ?c") + shows "mono_set S \ (S = {a <..} \ S = {a..})" (is "_ = ?c") proof - assume "mono S" + assume "mono_set S" then have mono: "\x y. x \ y \ x \ S \ y \ S" by (auto simp: mono_set) show ?c proof cases diff -r bdcc11b2fdc8 -r 510ac30f44c0 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700 @@ -762,7 +762,7 @@ apply auto apply (rule span_mul) apply (rule span_superset) -apply (auto simp add: Collect_def mem_def) +apply auto done lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\ (UNIV:: 'n set)}" (is "finite ?S") @@ -785,12 +785,12 @@ proof- let ?U = "UNIV :: 'n set" let ?B = "cart_basis ` S" - let ?P = "\(x::real^_). \i\ ?U. i \ S \ x$i =0" + let ?P = "{(x::real^_). \i\ ?U. i \ S \ x$i =0}" {fix x::"real^_" assume xS: "x\ ?B" - from xS have "?P x" by auto} + from xS have "x \ ?P" by auto} moreover have "subspace ?P" - by (auto simp add: subspace_def Collect_def mem_def) + by (auto simp add: subspace_def) ultimately show ?thesis using x span_induct[of ?B ?P x] iS by blast qed @@ -830,7 +830,7 @@ from equalityD2[OF span_stdbasis] have IU: " (UNIV :: (real^'m) set) \ span ?I" by blast from linear_eq[OF lf lg IU] fg x - have "f x = g x" unfolding Collect_def Ball_def mem_def by metis} + have "f x = g x" unfolding Ball_def mem_Collect_eq by metis} then show ?thesis by (auto intro: ext) qed diff -r bdcc11b2fdc8 -r 510ac30f44c0 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700 @@ -101,9 +101,9 @@ lemma span_eq[simp]: "(span s = s) <-> subspace s" proof- - { fix f assume "f <= subspace" - hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto } - thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto + { fix f assume "Ball f subspace" + hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto } + thus ?thesis using hull_eq[of subspace s] span_def by auto qed lemma basis_inj_on: "d \ {.. inj_on (basis :: nat => 'n::euclidean_space) d" @@ -391,11 +391,11 @@ unfolding affine_def by auto lemma affine_affine_hull: "affine(affine hull s)" - unfolding hull_def using affine_Inter[of "{t \ affine. s \ t}"] - unfolding mem_def by auto + unfolding hull_def using affine_Inter[of "{t. affine t \ s \ t}"] + by auto lemma affine_hull_eq[simp]: "(affine hull s = s) \ affine s" -by (metis affine_affine_hull hull_same mem_def) +by (metis affine_affine_hull hull_same) subsection {* Some explicit formulations (from Lars Schewe). *} @@ -459,7 +459,7 @@ lemma affine_hull_explicit: "affine hull p = {y. \s u. finite s \ s \ {} \ s \ p \ setsum u s = 1 \ setsum (\v. (u v) *\<^sub>R v) s = y}" - apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine] + apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof- fix x assume "x\p" thus "\s u. finite s \ s \ {} \ s \ p \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" apply(rule_tac x="{x}" in exI, rule_tac x="\x. 1" in exI) by auto @@ -500,7 +500,7 @@ subsection {* Stepping theorems and hence small special cases. *} lemma affine_hull_empty[simp]: "affine hull {} = {}" - apply(rule hull_unique) unfolding mem_def by auto + apply(rule hull_unique) by auto lemma affine_hull_finite_step: fixes y :: "'a::real_vector" @@ -812,12 +812,11 @@ subsection {* Conic hull. *} lemma cone_cone_hull: "cone (cone hull s)" - unfolding hull_def using cone_Inter[of "{t \ conic. s \ t}"] - by (auto simp add: mem_def) + unfolding hull_def by auto lemma cone_hull_eq: "(cone hull s = s) \ cone s" - apply(rule hull_eq[unfolded mem_def]) - using cone_Inter unfolding subset_eq by (auto simp add: mem_def) + apply(rule hull_eq) + using cone_Inter unfolding subset_eq by auto lemma mem_cone: assumes "cone S" "x : S" "c>=0" @@ -888,7 +887,7 @@ lemma mem_cone_hull: assumes "x : S" "c>=0" shows "c *\<^sub>R x : cone hull S" -by (metis assms cone_cone_hull hull_inc mem_cone mem_def) +by (metis assms cone_cone_hull hull_inc mem_cone) lemma cone_hull_expl: fixes S :: "('m::euclidean_space) set" @@ -901,11 +900,11 @@ moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto } hence "cone ?rhs" unfolding cone_def by auto - hence "?rhs : cone" unfolding mem_def by auto + hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto { fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto hence "x : ?rhs" by auto } hence "S <= ?rhs" by auto -hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto +hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto moreover { fix x assume "x : ?rhs" from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto @@ -1081,18 +1080,18 @@ subsection {* Convex hull. *} lemma convex_convex_hull: "convex(convex hull s)" - unfolding hull_def using convex_Inter[of "{t\convex. s\t}"] - unfolding mem_def by auto + unfolding hull_def using convex_Inter[of "{t. convex t \ s \ t}"] + by auto lemma convex_hull_eq: "convex hull s = s \ convex s" -by (metis convex_convex_hull hull_same mem_def) +by (metis convex_convex_hull hull_same) lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" assumes "bounded s" shows "bounded(convex hull s)" proof- from assms obtain B where B:"\x\s. norm x \ B" unfolding bounded_iff by auto show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B]) - unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball] + unfolding subset_hull[of convex, OF convex_cball] unfolding subset_eq mem_cball dist_norm using B by auto qed lemma finite_imp_bounded_convex_hull: @@ -1125,17 +1124,17 @@ subsection {* Stepping theorems for convex hulls of finite sets. *} lemma convex_hull_empty[simp]: "convex hull {} = {}" - apply(rule hull_unique) unfolding mem_def by auto + apply(rule hull_unique) by auto lemma convex_hull_singleton[simp]: "convex hull {a} = {a}" - apply(rule hull_unique) unfolding mem_def by auto + apply(rule hull_unique) by auto lemma convex_hull_insert: fixes s :: "'a::real_vector set" assumes "s \ {}" shows "convex hull (insert a s) = {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") - apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof- + apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof- fix x assume x:"x = a \ x \ s" thus "x\?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto @@ -1192,7 +1191,7 @@ shows "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ (setsum u {1..k} = 1) \ (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") - apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer + apply(rule hull_unique) apply(rule) defer apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule) proof- fix x assume "x\s" @@ -1232,7 +1231,7 @@ assumes "finite s" shows "convex hull s = {y. \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") -proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set]) +proof(rule hull_unique, auto simp add: convex_def[of ?set]) fix x assume "x\s" thus " \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" apply(rule_tac x="\y. if x=y then 1 else 0" in exI) apply auto unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto @@ -1356,8 +1355,8 @@ apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\x. v" in exI) by simp qed lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u. 0 \ u \ u \ 1}" - unfolding convex_hull_2 unfolding Collect_def -proof(rule ext) have *:"\x y ::real. x + y = 1 \ x = 1 - y" by auto + unfolding convex_hull_2 +proof(rule Collect_cong) have *:"\x y ::real. x + y = 1 \ x = 1 - y" by auto fix x show "(\v u. x = v *\<^sub>R a + u *\<^sub>R b \ 0 \ v \ 0 \ u \ v + u = 1) = (\u. x = a + u *\<^sub>R (b - a) \ 0 \ u \ u \ 1)" unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed @@ -1367,8 +1366,8 @@ have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto have *:"\x y z ::real. x + y + z = 1 \ x = 1 - y - z" "\x y z ::_::euclidean_space. x + y + z = 1 \ x = 1 - y - z" by (auto simp add: field_simps) - show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and * - unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto + show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and * + unfolding convex_hull_finite_step[OF fin(3)] apply(rule Collect_cong) apply simp apply auto apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\x. w" in exI) by simp qed @@ -1392,14 +1391,14 @@ lemma affine_hull_subset_span: fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \ (span s)" -by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span) +by (metis hull_minimal span_inc subspace_imp_affine subspace_span) lemma convex_hull_subset_span: fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \ (span s)" -by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span) +by (metis hull_minimal span_inc subspace_imp_convex subspace_span) lemma convex_hull_subset_affine_hull: "(convex hull s) \ (affine hull s)" -by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def) +by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset) lemma affine_dependent_imp_dependent: @@ -1572,11 +1571,11 @@ proof- have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto -ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def) +ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal) have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto -ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal mem_def) +ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal) hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto from this show ?thesis using h1 by auto qed @@ -3016,7 +3015,7 @@ then obtain a b where ab:"a \ 0" "0 < b" "\x\convex hull c. b < inner a x" using separating_hyperplane_closed_0[OF convex_convex_hull, of c] using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2) - using subset_hull[unfolded mem_def, of convex, OF assms(1), THEN sym, of c] by auto + using subset_hull[of convex, OF assms(1), THEN sym, of c] by auto hence "\x. norm x = 1 \ (\y\c. 0 \ inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI) using hull_subset[of c convex] unfolding subset_eq and inner_scaleR apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg) @@ -3077,7 +3076,7 @@ lemma convex_hull_translation_lemma: "convex hull ((\x. a + x) ` s) \ (\x. a + x) ` (convex hull s)" -by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono mem_def) +by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono) lemma convex_hull_bilemma: fixes neg assumes "(\s a. (convex hull (up a s)) \ up a (convex hull s))" @@ -3091,7 +3090,7 @@ lemma convex_hull_scaling_lemma: "(convex hull ((\x. c *\<^sub>R x) ` s)) \ (\x. c *\<^sub>R x) ` (convex hull s)" -by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff) +by (metis convex_convex_hull convex_scaling hull_subset subset_hull subset_image_iff) lemma convex_hull_scaling: "convex hull ((\x. c *\<^sub>R x) ` s) = (\x. c *\<^sub>R x) ` (convex hull s)" @@ -3269,7 +3268,7 @@ unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto have *:"g \ h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto have "convex hull (X ` h) \ \ g" "convex hull (X ` g) \ \ h" - apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding mem_def unfolding subset_eq + apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding subset_eq apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof- fix x assume "x\X ` g" then guess y unfolding image_iff .. thus "x\\h" using X[THEN bspec[where x=y]] using * f by auto next @@ -3710,7 +3709,7 @@ apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **) apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE) - by(auto simp add: mem_def[of _ convex]) qed + by auto qed subsection {* And this is a finite set of vertices. *} @@ -3883,7 +3882,7 @@ closed_segment :: "'a::real_vector \ 'a \ 'a set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" -definition "between = (\ (a,b). closed_segment a b)" +definition "between = (\ (a,b) x. x \ closed_segment a b)" lemmas segment = open_segment_def closed_segment_def @@ -3968,15 +3967,15 @@ lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps) lemma between_mem_segment: "between (a,b) x \ x \ closed_segment a b" - unfolding between_def mem_def by auto + unfolding between_def by auto lemma between:"between (a,b) (x::'a::euclidean_space) \ dist a b = (dist a x) + (dist x b)" proof(cases "a = b") - case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric] + case True thus ?thesis unfolding between_def split_conv by(auto simp add:segment_refl dist_commute) next case False hence Fal:"norm (a - b) \ 0" and Fal2: "norm (a - b) > 0" by auto have *:"\u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps) - show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq + show ?thesis unfolding between_def split_conv closed_segment_def mem_Collect_eq apply rule apply(erule exE, (erule conjE)+) apply(subst dist_triangle_eq) proof- fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \ u" "u \ 1" hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)" @@ -4743,8 +4742,8 @@ { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto } hence "y : Inter {closure S |S. S : I}" by auto } hence "Inter I <= Inter {closure S |S. S : I}" by auto -moreover have "Inter {closure S |S. S : I} : closed" - unfolding mem_def closed_Inter closed_closure by auto +moreover have "closed (Inter {closure S |S. S : I})" + unfolding closed_Inter closed_closure by auto ultimately show ?thesis using closure_hull[of "Inter I"] hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto qed @@ -5074,8 +5073,8 @@ using I_def u_def by auto } hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto -moreover have "(convex hull S) <*> (convex hull T) : convex" - unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull) +moreover have "convex ((convex hull S) <*> (convex hull T))" + by (simp add: convex_direct_sum convex_convex_hull) ultimately show ?thesis using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"] hull_subset[of S convex] hull_subset[of T convex] by auto @@ -5384,7 +5383,6 @@ finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto } hence "convex ?rhs" unfolding convex_def by auto -hence "?rhs : convex" unfolding mem_def by auto from this show ?thesis using `?lhs >= ?rhs` * hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast qed @@ -5578,7 +5576,7 @@ hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto } hence "K0 >= Union (K ` I)" by auto - moreover have "K0 : convex" unfolding mem_def K0_def + moreover have "convex K0" unfolding K0_def apply (subst convex_cone_hull) apply (subst convex_direct_sum) unfolding C0_def using convex_convex_hull by auto ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast @@ -5587,7 +5585,7 @@ hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono) hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto - moreover have "convex hull(Union (K ` I)) : cone" unfolding mem_def apply (subst cone_convex_hull) + moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull) using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto ultimately have "convex hull (Union (K ` I)) >= K0" unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast diff -r bdcc11b2fdc8 -r 510ac30f44c0 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 07:18:28 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 09:17:24 2011 -0700 @@ -102,7 +102,7 @@ then show False using MInf by auto next case PInf then have "S={\}" by (metis Inf_eq_PInfty assms(2)) - then show False by (metis `Inf S ~: S` insert_code mem_def PInf) + then show False using `Inf S ~: S` by simp next case (real r) then have fin: "\Inf S\ \ \" by simp from ereal_open_cont_interval[OF a this] guess e . note e = this @@ -284,22 +284,22 @@ lemma ereal_open_mono_set: fixes S :: "ereal set" defines "a \ Inf S" - shows "(open S \ mono S) \ (S = UNIV \ S = {a <..})" + shows "(open S \ mono_set S) \ (S = UNIV \ S = {a <..})" by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff ereal_open_atLeast ereal_open_closed mono_set_iff open_ereal_greaterThan) lemma ereal_closed_mono_set: fixes S :: "ereal set" - shows "(closed S \ mono S) \ (S = {} \ S = {Inf S ..})" + shows "(closed S \ mono_set S) \ (S = {} \ S = {Inf S ..})" by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan) lemma ereal_Liminf_Sup_monoset: fixes f :: "'a => ereal" - shows "Liminf net f = Sup {l. \S. open S \ mono S \ l \ S \ eventually (\x. f x \ S) net}" + shows "Liminf net f = Sup {l. \S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net}" unfolding Liminf_Sup proof (intro arg_cong[where f="\P. Sup (Collect P)"] ext iffI allI impI) - fix l S assume ev: "\yx. y < f x) net" and "open S" "mono S" "l \ S" + fix l S assume ev: "\yx. y < f x) net" and "open S" "mono_set S" "l \ S" then have "S = UNIV \ S = {Inf S <..}" using ereal_open_mono_set[of S] by auto then show "eventually (\x. f x \ S) net" @@ -310,7 +310,7 @@ then show "eventually (\x. f x \ S) net" by (subst S) auto qed auto next - fix l y assume S: "\S. open S \ mono S \ l \ S \ eventually (\x. f x \ S) net" "y < l" + fix l y assume S: "\S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net" "y < l" have "eventually (\x. f x \ {y <..}) net" using `y < l` by (intro S[rule_format]) auto then show "eventually (\x. y < f x) net" by auto @@ -318,11 +318,11 @@ lemma ereal_Limsup_Inf_monoset: fixes f :: "'a => ereal" - shows "Limsup net f = Inf {l. \S. open S \ mono (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net}" + shows "Limsup net f = Inf {l. \S. open S \ mono_set (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net}" unfolding Limsup_Inf proof (intro arg_cong[where f="\P. Inf (Collect P)"] ext iffI allI impI) - fix l S assume ev: "\y>l. eventually (\x. f x < y) net" and "open S" "mono (uminus`S)" "l \ S" - then have "open (uminus`S) \ mono (uminus`S)" by (simp add: ereal_open_uminus) + fix l S assume ev: "\y>l. eventually (\x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \ S" + then have "open (uminus`S) \ mono_set (uminus`S)" by (simp add: ereal_open_uminus) then have "S = UNIV \ S = {..< Sup S}" unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp then show "eventually (\x. f x \ S) net" @@ -333,7 +333,7 @@ then show "eventually (\x. f x \ S) net" by (subst S) auto qed auto next - fix l y assume S: "\S. open S \ mono (uminus`S) \ l \ S \ eventually (\x. f x \ S) net" "l < y" + fix l y assume S: "\S. open S \ mono_set (uminus`S) \ l \ S \ eventually (\x. f x \ S) net" "l < y" have "eventually (\x. f x \ {..< y}) net" using `l < y` by (intro S[rule_format]) auto then show "eventually (\x. f x < y) net" by auto @@ -469,7 +469,7 @@ lemma liminf_bounded_open: fixes x :: "nat \ ereal" - shows "x0 \ liminf x \ (\S. open S \ mono S \ x0 \ S \ (\N. \n\N. x n \ S))" + shows "x0 \ liminf x \ (\S. open S \ mono_set S \ x0 \ S \ (\N. \n\N. x n \ S))" (is "_ \ ?P x0") proof assume "?P x0" then show "x0 \ liminf x" @@ -477,7 +477,7 @@ by (intro complete_lattice_class.Sup_upper) auto next assume "x0 \ liminf x" - { fix S :: "ereal set" assume om: "open S & mono S & x0:S" + { fix S :: "ereal set" assume om: "open S & mono_set S & x0:S" { assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto } moreover { assume "~(S=UNIV)" @@ -641,7 +641,7 @@ shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)" proof- let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)" -{ fix T assume T_def: "open T & mono T & ?l:T" +{ fix T assume T_def: "open T & mono_set T & ?l:T" have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T" proof- { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) } @@ -660,7 +660,7 @@ } moreover { fix z - assume a: "ALL T. open T --> mono T --> z : T --> + assume a: "ALL T. open T --> mono_set T --> z : T --> (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)" { fix B assume "B0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)" @@ -683,7 +683,7 @@ shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)" proof- let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)" -{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T" +{ fix T assume T_def: "open T & mono_set (uminus ` T) & ?l:T" have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T" proof- { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) } @@ -707,7 +707,7 @@ } moreover { fix z - assume a: "ALL T. open T --> mono (uminus ` T) --> z : T --> + assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T --> (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)" { fix B assume "z0 & (ALL y:S. 0 < dist y x & dist y x < d --> f yf P Q. (\x k. (x,k) \ {(x,f k) | x k. P x k} \ Q x k) \ (\x k. P x k \ Q x (f k))" by auto have lem2: "\f s P f. finite s \ finite {(x,f k) | x k. (x,k) \ s \ P x k}" proof- case goal1 thus ?case apply-apply(rule finite_subset[of _ "(\(x,k). (x,f k)) ` s"]) by auto qed - have lem3: "\g::('a \ bool) \ 'a \ bool. finite p \ + have lem3: "\g::'a set \ 'a set. finite p \ setsum (\(x,k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \ p \ ~(g k = {})} = setsum (\(x,k). content k *\<^sub>R f x) ((\(x,k). (x,g k)) ` p)" apply(rule setsum_mono_zero_left) prefer 3 - proof fix g::"('a \ bool) \ 'a \ bool" and i::"('a) \ (('a) set)" + proof fix g::"'a set \ 'a set" and i::"('a) \ (('a) set)" assume "i \ (\(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \ p \ g k \ {}}" then obtain x k where xk:"i=(x,g k)" "(x,k)\p" "(x,g k) \ {(x, g k) |x k. (x, k) \ p \ g k \ {}}" by auto have "content (g k) = 0" using xk using content_empty by auto @@ -3004,9 +3004,9 @@ lemma gauge_modify: assumes "(\s. open s \ open {x. f(x) \ s})" "gauge d" - shows "gauge (\x y. d (f x) (f y))" + shows "gauge (\x. {y. f y \ d (f x)})" using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE) - apply(erule_tac x="d (f x)" in allE) unfolding mem_def Collect_def by auto + apply(erule_tac x="d (f x)" in allE) by auto subsection {* Only need trivial subintervals if the interval itself is trivial. *} @@ -3194,7 +3194,7 @@ show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz) proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos) from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format] - def d' \ "\x y. d (g x) (g y)" have d':"\x. d' x = {y. g y \ (d (g x))}" unfolding d'_def by(auto simp add:mem_def) + def d' \ "\x. {y. g y \ d (g x)}" have d':"\x. d' x = {y. g y \ (d (g x))}" unfolding d'_def .. show "\d. gauge d \ (\p. p tagged_division_of h ` {a..b} \ d fine p \ norm ((\(x, k)\p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)" proof(rule_tac x=d' in exI,safe) show "gauge d'" using d(1) unfolding gauge_def d' using continuous_open_preimage_univ[OF assms(4)] by auto fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)] diff -r bdcc11b2fdc8 -r 510ac30f44c0 src/HOL/Multivariate_Analysis/Linear_Algebra.thy --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 12 07:18:28 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 12 09:17:24 2011 -0700 @@ -648,17 +648,17 @@ subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} -definition hull :: "'a set set \ 'a set \ 'a set" (infixl "hull" 75) where - "S hull s = Inter {t. t \ S \ s \ t}" - -lemma hull_same: "s \ S \ S hull s = s" +definition hull :: "('a set \ bool) \ 'a set \ 'a set" (infixl "hull" 75) where + "S hull s = Inter {t. S t \ s \ t}" + +lemma hull_same: "S s \ S hull s = s" unfolding hull_def by auto -lemma hull_in: "(\T. T \ S ==> Inter T \ S) ==> (S hull s) \ S" -unfolding hull_def subset_iff by auto - -lemma hull_eq: "(\T. T \ S ==> Inter T \ S) ==> (S hull s) = s \ s \