# HG changeset patch # User huffman # Date 1313165850 25200 # Node ID 75ea0e390a92799a31dfb4073e0dc41930301de2 # Parent 510ac30f44c088598e5a9e799de0002c5e0162a3# Parent 238c5ea1e2ceba8660b2e5e96202ef2ab13d611c merged diff -r 238c5ea1e2ce -r 75ea0e390a92 src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Aug 12 09:17:30 2011 -0700 @@ -109,7 +109,7 @@ |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) (*set*) - val set = @{term "defl_set :: udom defl => udom => bool"} $ defl + val set = @{term "defl_set :: udom defl => udom set"} $ defl (*pcpodef*) val tac1 = rtac @{thm defl_set_bottom} 1 diff -r 238c5ea1e2ce -r 75ea0e390a92 src/HOL/HOLCF/Tools/holcf_library.ML --- a/src/HOL/HOLCF/Tools/holcf_library.ML Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML Fri Aug 12 09:17:30 2011 -0700 @@ -15,6 +15,7 @@ val boolT = HOLogic.boolT val natT = HOLogic.natT +val mk_setT = HOLogic.mk_setT val mk_equals = Logic.mk_equals val mk_eq = HOLogic.mk_eq @@ -56,9 +57,9 @@ fun mk_lub t = let val T = Term.range_type (Term.fastype_of t) - val lub_const = Const (@{const_name lub}, (T --> boolT) --> T) + val lub_const = Const (@{const_name lub}, mk_setT T --> T) val UNIV_const = @{term "UNIV :: nat set"} - val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT + val image_type = (natT --> T) --> mk_setT natT --> mk_setT T val image_const = Const (@{const_name image}, image_type) in lub_const $ (image_const $ t $ UNIV_const) diff -r 238c5ea1e2ce -r 75ea0e390a92 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 09:17:30 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 238c5ea1e2ce -r 75ea0e390a92 src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/Library/Infinite_Set.thy Fri Aug 12 09:17:30 2011 -0700 @@ -546,7 +546,7 @@ apply (induct n arbitrary: S) apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty) apply simp -apply (metis Collect_def Collect_mem_eq DiffE infinite_remove) +apply (metis Collect_mem_eq DiffE infinite_remove) done declare enumerate_0 [simp del] enumerate_Suc [simp del] diff -r 238c5ea1e2ce -r 75ea0e390a92 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 09:17:30 2011 -0700 @@ -467,7 +467,7 @@ text {* some lemmas to map between Eucl and Cart *} lemma basis_real_n[simp]:"(basis (\' i)::real^'a) = cart_basis i" unfolding basis_vec_def using pi'_range[where 'n='a] - by (auto simp: vec_eq_iff) + by (auto simp: vec_eq_iff axis_def) subsection {* Orthogonality on cartesian products *} @@ -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 @@ -866,7 +866,7 @@ obtain g where g: "linear g" "g o op *v A = id" by blast have "matrix g ** A = mat 1" unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] - using g(2) by (simp add: o_def id_def stupid_ext) + using g(2) by (simp add: fun_eq_iff) then have "\B. (B::real ^'m^'n) ** A = mat 1" by blast} ultimately show ?thesis by blast qed @@ -894,7 +894,7 @@ have "A ** (matrix g) = mat 1" unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] - using g(2) unfolding o_def stupid_ext[symmetric] id_def + using g(2) unfolding o_def fun_eq_iff id_def . hence "\B. A ** (B::real^'m^'n) = mat 1" by blast } @@ -1635,11 +1635,8 @@ abbreviation dest_vec1:: "'a ^1 \ 'a" where "dest_vec1 x \ (x$1)" -lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y" - by (simp_all add: vec_eq_iff) - -lemma vec1_component[simp]: "(vec1 x)$1 = x" - by (simp_all add: vec_eq_iff) +lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" + by (simp add: vec_eq_iff) lemma forall_vec1: "(\x. P x) \ (\x. P (vec1 x))" by (metis vec1_dest_vec1(1)) @@ -1647,9 +1644,6 @@ lemma exists_vec1: "(\x. P x) \ (\x. P(vec1 x))" by (metis vec1_dest_vec1(1)) -lemma vec1_eq[simp]: "vec1 x = vec1 y \ x = y" - by (metis vec1_dest_vec1(2)) - lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \ x = y" by (metis vec1_dest_vec1(1)) @@ -1741,12 +1735,12 @@ by (simp add: vec_def norm_real) lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)" - by (simp only: dist_real vec1_component) + by (simp only: dist_real vec_component) lemma abs_dest_vec1: "norm x = \dest_vec1 x\" by (metis vec1_dest_vec1(1) norm_vec1) lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component - vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def + vec_inj[where 'b=1] vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def lemma bounded_linear_vec1:"bounded_linear (vec1::real\real^1)" unfolding bounded_linear_def additive_def bounded_linear_axioms_def diff -r 238c5ea1e2ce -r 75ea0e390a92 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 09:17:30 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 238c5ea1e2ce -r 75ea0e390a92 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Aug 12 09:17:30 2011 -0700 @@ -15,22 +15,75 @@ subsection {* Type class of Euclidean spaces *} class euclidean_space = real_inner + + fixes Basis :: "'a set" + assumes nonempty_Basis [simp]: "Basis \ {}" + assumes finite_Basis [simp]: "finite Basis" + assumes inner_Basis: + "\u \ Basis; v \ Basis\ \ inner u v = (if u = v then 1 else 0)" + assumes euclidean_all_zero_iff: + "(\u\Basis. inner x u = 0) \ (x = 0)" + + -- "FIXME: make this a separate definition" fixes dimension :: "'a itself \ nat" + assumes dimension_def: "dimension TYPE('a) = card Basis" + + -- "FIXME: eventually basis function can be removed" fixes basis :: "nat \ 'a" - assumes DIM_positive [intro]: - "0 < dimension TYPE('a)" - assumes basis_zero [simp]: - "dimension TYPE('a) \ i \ basis i = 0" - assumes basis_orthonormal: - "\iji (x = 0)" + assumes image_basis: "basis ` {.. nat" ("(1DIM/(1'(_')))") translations "DIM('t)" == "CONST dimension (TYPE('t))" +lemma (in euclidean_space) norm_Basis: "u \ Basis \ norm u = 1" + unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) + +lemma (in euclidean_space) sgn_Basis: "u \ Basis \ sgn u = u" + unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one) + +lemma (in euclidean_space) Basis_zero [simp]: "0 \ Basis" +proof + assume "0 \ Basis" thus "False" + using inner_Basis [of 0 0] by simp +qed + +lemma (in euclidean_space) nonzero_Basis: "u \ Basis \ u \ 0" + by clarsimp + +text {* Lemmas related to @{text basis} function. *} + +lemma (in euclidean_space) euclidean_all_zero: + "(\i (x = 0)" + using euclidean_all_zero_iff [of x, folded image_basis] + unfolding ball_simps by (simp add: Ball_def inner_commute) + +lemma (in euclidean_space) basis_zero [simp]: + "DIM('a) \ i \ basis i = 0" + using basis_finite by auto + +lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)" + unfolding dimension_def by (simp add: card_gt_0_iff) + +lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {.. Basis \ i < DIM('a)" + by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp) + +lemma (in euclidean_space) Basis_elim: + assumes "u \ Basis" obtains i where "i < DIM('a)" and "u = basis i" + using assms unfolding image_basis [symmetric] by fast + +lemma (in euclidean_space) basis_orthonormal: + "\ij i < DIM('a) then 1 else 0)" proof (cases "(i < DIM('a) \ j < DIM('a))") @@ -161,6 +214,9 @@ begin definition + "Basis = {1::real}" + +definition "dimension (t::real itself) = 1" definition [simp]: @@ -170,42 +226,44 @@ by (rule dimension_real_def) instance - by default simp+ + by default (auto simp add: Basis_real_def) end subsubsection {* Type @{typ complex} *} + (* TODO: move these to Complex.thy/Inner_Product.thy *) + +lemma norm_ii [simp]: "norm ii = 1" + unfolding i_def by simp + +lemma complex_inner_1 [simp]: "inner 1 x = Re x" + unfolding inner_complex_def by simp + +lemma complex_inner_1_right [simp]: "inner x 1 = Re x" + unfolding inner_complex_def by simp + +lemma complex_inner_ii_left [simp]: "inner ii x = Im x" + unfolding inner_complex_def by simp + +lemma complex_inner_ii_right [simp]: "inner x ii = Im x" + unfolding inner_complex_def by simp + instantiation complex :: euclidean_space begin +definition Basis_complex_def: + "Basis = {1, ii}" + definition "dimension (t::complex itself) = 2" definition "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)" -lemma all_less_Suc: "(\i (\i P n" - by (auto simp add: less_Suc_eq) - -instance proof - show "0 < DIM(complex)" - unfolding dimension_complex_def by simp -next - fix i :: nat - assume "DIM(complex) \ i" thus "basis i = (0::complex)" - unfolding dimension_complex_def basis_complex_def by simp -next - show "\iji x = 0" - unfolding dimension_complex_def basis_complex_def inner_complex_def - by (simp add: numeral_2_eq_2 all_less_Suc complex_eq_iff) -qed +instance + by default (auto simp add: Basis_complex_def dimension_complex_def + basis_complex_def intro: complex_eqI split: split_if_asm) end @@ -214,40 +272,50 @@ subsubsection {* Type @{typ "'a \ 'b"} *} +lemma disjoint_iff: "A \ B = {} \ (\x\A. \y\B. x \ y)" + by auto (* TODO: move elsewhere *) + instantiation prod :: (euclidean_space, euclidean_space) euclidean_space begin definition + "Basis = (\u. (u, 0)) ` Basis \ (\v. (0, v)) ` Basis" + +definition "dimension (t::('a \ 'b) itself) = DIM('a) + DIM('b)" definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))" -lemma all_less_sum: - fixes m n :: nat - shows "(\i<(m + n). P i) \ (\i (\i 'b)" - unfolding dimension_prod_def by (intro add_pos_pos DIM_positive) + show "(Basis :: ('a \ 'b) set) \ {}" + unfolding Basis_prod_def by simp next - fix i :: nat - assume "DIM('a \ 'b) \ i" thus "basis i = (0::'a \ 'b)" - unfolding dimension_prod_def basis_prod_def zero_prod_def - by simp + show "finite (Basis :: ('a \ 'b) set)" + unfolding Basis_prod_def by simp next - show "\i 'b). \j 'b). - inner (basis i::'a \ 'b) (basis j) = (if i = j then 1 else 0)" - unfolding dimension_prod_def basis_prod_def inner_prod_def - unfolding all_less_sum prod_eq_iff - by (simp add: basis_orthonormal) + fix u v :: "'a \ 'b" + assume "u \ Basis" and "v \ Basis" + thus "inner u v = (if u = v then 1 else 0)" + unfolding Basis_prod_def inner_prod_def + by (auto simp add: inner_Basis split: split_if_asm) next fix x :: "'a \ 'b" - show "(\i 'b). inner (basis i) x = 0) \ x = 0" - unfolding dimension_prod_def basis_prod_def inner_prod_def - unfolding all_less_sum prod_eq_iff - by (simp add: euclidean_all_zero) + show "(\u\Basis. inner x u = 0) \ x = 0" + unfolding Basis_prod_def ball_Un ball_simps + by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff) +next + show "DIM('a \ 'b) = card (Basis :: ('a \ 'b) set)" + unfolding dimension_prod_def Basis_prod_def + by (simp add: card_Un_disjoint disjoint_iff + card_image inj_on_def dimension_def) +next + show "basis ` {.. 'b)} = (Basis :: ('a \ 'b) set)" + by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def + image_def elim!: Basis_elim) +next + show "basis ` {DIM('a \ 'b)..} = {0::('a \ 'b)}" + by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def) qed end diff -r 238c5ea1e2ce -r 75ea0e390a92 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 17:01:30 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 09:17:30 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 \