1.1 --- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 07:18:28 2011 -0700
1.2 +++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 09:17:24 2011 -0700
1.3 @@ -1370,7 +1370,7 @@
1.4 }
1.5 moreover
1.6 { assume "?lhs" hence "?rhs"
1.7 - by (metis Collect_def Collect_mem_eq SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
1.8 + by (metis SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
1.9 inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
1.10 } ultimately show ?thesis by auto
1.11 qed
1.12 @@ -1390,7 +1390,7 @@
1.13 }
1.14 moreover
1.15 { assume "?lhs" hence "?rhs"
1.16 - by (metis Collect_def Collect_mem_eq le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
1.17 + by (metis le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
1.18 inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
1.19 } ultimately show ?thesis by auto
1.20 qed
1.21 @@ -2210,21 +2210,20 @@
1.22 qed
1.23 qed auto
1.24
1.25 -lemma (in order) mono_set:
1.26 - "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
1.27 - by (auto simp: mono_def mem_def)
1.28 +definition (in order) mono_set:
1.29 + "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
1.30
1.31 -lemma (in order) mono_greaterThan [intro, simp]: "mono {B<..}" unfolding mono_set by auto
1.32 -lemma (in order) mono_atLeast [intro, simp]: "mono {B..}" unfolding mono_set by auto
1.33 -lemma (in order) mono_UNIV [intro, simp]: "mono UNIV" unfolding mono_set by auto
1.34 -lemma (in order) mono_empty [intro, simp]: "mono {}" unfolding mono_set by auto
1.35 +lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
1.36 +lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
1.37 +lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
1.38 +lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
1.39
1.40 lemma (in complete_linorder) mono_set_iff:
1.41 fixes S :: "'a set"
1.42 defines "a \<equiv> Inf S"
1.43 - shows "mono S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
1.44 + shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
1.45 proof
1.46 - assume "mono S"
1.47 + assume "mono_set S"
1.48 then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
1.49 show ?c
1.50 proof cases
2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700
2.3 @@ -762,7 +762,7 @@
2.4 apply auto
2.5 apply (rule span_mul)
2.6 apply (rule span_superset)
2.7 -apply (auto simp add: Collect_def mem_def)
2.8 +apply auto
2.9 done
2.10
2.11 lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
2.12 @@ -785,12 +785,12 @@
2.13 proof-
2.14 let ?U = "UNIV :: 'n set"
2.15 let ?B = "cart_basis ` S"
2.16 - let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
2.17 + let ?P = "{(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0}"
2.18 {fix x::"real^_" assume xS: "x\<in> ?B"
2.19 - from xS have "?P x" by auto}
2.20 + from xS have "x \<in> ?P" by auto}
2.21 moreover
2.22 have "subspace ?P"
2.23 - by (auto simp add: subspace_def Collect_def mem_def)
2.24 + by (auto simp add: subspace_def)
2.25 ultimately show ?thesis
2.26 using x span_induct[of ?B ?P x] iS by blast
2.27 qed
2.28 @@ -830,7 +830,7 @@
2.29 from equalityD2[OF span_stdbasis]
2.30 have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
2.31 from linear_eq[OF lf lg IU] fg x
2.32 - have "f x = g x" unfolding Collect_def Ball_def mem_def by metis}
2.33 + have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
2.34 then show ?thesis by (auto intro: ext)
2.35 qed
2.36
3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700
3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700
3.3 @@ -101,9 +101,9 @@
3.4
3.5 lemma span_eq[simp]: "(span s = s) <-> subspace s"
3.6 proof-
3.7 - { fix f assume "f <= subspace"
3.8 - hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto }
3.9 - thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto
3.10 + { fix f assume "Ball f subspace"
3.11 + hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto }
3.12 + thus ?thesis using hull_eq[of subspace s] span_def by auto
3.13 qed
3.14
3.15 lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
3.16 @@ -391,11 +391,11 @@
3.17 unfolding affine_def by auto
3.18
3.19 lemma affine_affine_hull: "affine(affine hull s)"
3.20 - unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]
3.21 - unfolding mem_def by auto
3.22 + unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"]
3.23 + by auto
3.24
3.25 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
3.26 -by (metis affine_affine_hull hull_same mem_def)
3.27 +by (metis affine_affine_hull hull_same)
3.28
3.29 subsection {* Some explicit formulations (from Lars Schewe). *}
3.30
3.31 @@ -459,7 +459,7 @@
3.32
3.33 lemma affine_hull_explicit:
3.34 "affine hull p = {y. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> setsum (\<lambda>v. (u v) *\<^sub>R v) s = y}"
3.35 - apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]
3.36 + apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq
3.37 apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
3.38 fix x assume "x\<in>p" thus "\<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
3.39 apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
3.40 @@ -500,7 +500,7 @@
3.41 subsection {* Stepping theorems and hence small special cases. *}
3.42
3.43 lemma affine_hull_empty[simp]: "affine hull {} = {}"
3.44 - apply(rule hull_unique) unfolding mem_def by auto
3.45 + apply(rule hull_unique) by auto
3.46
3.47 lemma affine_hull_finite_step:
3.48 fixes y :: "'a::real_vector"
3.49 @@ -812,12 +812,11 @@
3.50 subsection {* Conic hull. *}
3.51
3.52 lemma cone_cone_hull: "cone (cone hull s)"
3.53 - unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"]
3.54 - by (auto simp add: mem_def)
3.55 + unfolding hull_def by auto
3.56
3.57 lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
3.58 - apply(rule hull_eq[unfolded mem_def])
3.59 - using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
3.60 + apply(rule hull_eq)
3.61 + using cone_Inter unfolding subset_eq by auto
3.62
3.63 lemma mem_cone:
3.64 assumes "cone S" "x : S" "c>=0"
3.65 @@ -888,7 +887,7 @@
3.66 lemma mem_cone_hull:
3.67 assumes "x : S" "c>=0"
3.68 shows "c *\<^sub>R x : cone hull S"
3.69 -by (metis assms cone_cone_hull hull_inc mem_cone mem_def)
3.70 +by (metis assms cone_cone_hull hull_inc mem_cone)
3.71
3.72 lemma cone_hull_expl:
3.73 fixes S :: "('m::euclidean_space) set"
3.74 @@ -901,11 +900,11 @@
3.75 moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
3.76 ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
3.77 } hence "cone ?rhs" unfolding cone_def by auto
3.78 - hence "?rhs : cone" unfolding mem_def by auto
3.79 + hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto
3.80 { fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
3.81 hence "x : ?rhs" by auto
3.82 } hence "S <= ?rhs" by auto
3.83 -hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto
3.84 +hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto
3.85 moreover
3.86 { fix x assume "x : ?rhs"
3.87 from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
3.88 @@ -1081,18 +1080,18 @@
3.89 subsection {* Convex hull. *}
3.90
3.91 lemma convex_convex_hull: "convex(convex hull s)"
3.92 - unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
3.93 - unfolding mem_def by auto
3.94 + unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
3.95 + by auto
3.96
3.97 lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
3.98 -by (metis convex_convex_hull hull_same mem_def)
3.99 +by (metis convex_convex_hull hull_same)
3.100
3.101 lemma bounded_convex_hull:
3.102 fixes s :: "'a::real_normed_vector set"
3.103 assumes "bounded s" shows "bounded(convex hull s)"
3.104 proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
3.105 show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
3.106 - unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
3.107 + unfolding subset_hull[of convex, OF convex_cball]
3.108 unfolding subset_eq mem_cball dist_norm using B by auto qed
3.109
3.110 lemma finite_imp_bounded_convex_hull:
3.111 @@ -1125,17 +1124,17 @@
3.112 subsection {* Stepping theorems for convex hulls of finite sets. *}
3.113
3.114 lemma convex_hull_empty[simp]: "convex hull {} = {}"
3.115 - apply(rule hull_unique) unfolding mem_def by auto
3.116 + apply(rule hull_unique) by auto
3.117
3.118 lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
3.119 - apply(rule hull_unique) unfolding mem_def by auto
3.120 + apply(rule hull_unique) by auto
3.121
3.122 lemma convex_hull_insert:
3.123 fixes s :: "'a::real_vector set"
3.124 assumes "s \<noteq> {}"
3.125 shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
3.126 b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
3.127 - apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-
3.128 + apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
3.129 fix x assume x:"x = a \<or> x \<in> s"
3.130 thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
3.131 apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
3.132 @@ -1192,7 +1191,7 @@
3.133 shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
3.134 (setsum u {1..k} = 1) \<and>
3.135 (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
3.136 - apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
3.137 + apply(rule hull_unique) apply(rule) defer
3.138 apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
3.139 proof-
3.140 fix x assume "x\<in>s"
3.141 @@ -1232,7 +1231,7 @@
3.142 assumes "finite s"
3.143 shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
3.144 setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
3.145 -proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
3.146 +proof(rule hull_unique, auto simp add: convex_def[of ?set])
3.147 fix x assume "x\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
3.148 apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
3.149 unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
3.150 @@ -1356,8 +1355,8 @@
3.151 apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed
3.152
3.153 lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u. 0 \<le> u \<and> u \<le> 1}"
3.154 - unfolding convex_hull_2 unfolding Collect_def
3.155 -proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
3.156 + unfolding convex_hull_2
3.157 +proof(rule Collect_cong) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
3.158 fix x show "(\<exists>v u. x = v *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> v \<and> 0 \<le> u \<and> v + u = 1) = (\<exists>u. x = a + u *\<^sub>R (b - a) \<and> 0 \<le> u \<and> u \<le> 1)"
3.159 unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
3.160
3.161 @@ -1367,8 +1366,8 @@
3.162 have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
3.163 have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
3.164 "\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
3.165 - show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
3.166 - unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
3.167 + show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and *
3.168 + unfolding convex_hull_finite_step[OF fin(3)] apply(rule Collect_cong) apply simp apply auto
3.169 apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
3.170 apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed
3.171
3.172 @@ -1392,14 +1391,14 @@
3.173
3.174 lemma affine_hull_subset_span:
3.175 fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
3.176 -by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span)
3.177 +by (metis hull_minimal span_inc subspace_imp_affine subspace_span)
3.178
3.179 lemma convex_hull_subset_span:
3.180 fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
3.181 -by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span)
3.182 +by (metis hull_minimal span_inc subspace_imp_convex subspace_span)
3.183
3.184 lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
3.185 -by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def)
3.186 +by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
3.187
3.188
3.189 lemma affine_dependent_imp_dependent:
3.190 @@ -1572,11 +1571,11 @@
3.191 proof-
3.192 have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto
3.193 moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
3.194 -ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def)
3.195 +ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal)
3.196 have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto
3.197 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
3.198 moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto
3.199 -ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal mem_def)
3.200 +ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal)
3.201 hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto
3.202 from this show ?thesis using h1 by auto
3.203 qed
3.204 @@ -3016,7 +3015,7 @@
3.205 then obtain a b where ab:"a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < inner a x"
3.206 using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
3.207 using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
3.208 - using subset_hull[unfolded mem_def, of convex, OF assms(1), THEN sym, of c] by auto
3.209 + using subset_hull[of convex, OF assms(1), THEN sym, of c] by auto
3.210 hence "\<exists>x. norm x = 1 \<and> (\<forall>y\<in>c. 0 \<le> inner y x)" apply(rule_tac x="inverse(norm a) *\<^sub>R a" in exI)
3.211 using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
3.212 apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
3.213 @@ -3077,7 +3076,7 @@
3.214
3.215 lemma convex_hull_translation_lemma:
3.216 "convex hull ((\<lambda>x. a + x) ` s) \<subseteq> (\<lambda>x. a + x) ` (convex hull s)"
3.217 -by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono mem_def)
3.218 +by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono)
3.219
3.220 lemma convex_hull_bilemma: fixes neg
3.221 assumes "(\<forall>s a. (convex hull (up a s)) \<subseteq> up a (convex hull s))"
3.222 @@ -3091,7 +3090,7 @@
3.223
3.224 lemma convex_hull_scaling_lemma:
3.225 "(convex hull ((\<lambda>x. c *\<^sub>R x) ` s)) \<subseteq> (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
3.226 -by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff)
3.227 +by (metis convex_convex_hull convex_scaling hull_subset subset_hull subset_image_iff)
3.228
3.229 lemma convex_hull_scaling:
3.230 "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
3.231 @@ -3269,7 +3268,7 @@
3.232 unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
3.233 have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
3.234 have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
3.235 - apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding mem_def unfolding subset_eq
3.236 + apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding subset_eq
3.237 apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof-
3.238 fix x assume "x\<in>X ` g" then guess y unfolding image_iff ..
3.239 thus "x\<in>\<Inter>h" using X[THEN bspec[where x=y]] using * f by auto next
3.240 @@ -3710,7 +3709,7 @@
3.241 apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **)
3.242 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
3.243 unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
3.244 - by(auto simp add: mem_def[of _ convex]) qed
3.245 + by auto qed
3.246
3.247 subsection {* And this is a finite set of vertices. *}
3.248
3.249 @@ -3883,7 +3882,7 @@
3.250 closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
3.251 "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
3.252
3.253 -definition "between = (\<lambda> (a,b). closed_segment a b)"
3.254 +definition "between = (\<lambda> (a,b) x. x \<in> closed_segment a b)"
3.255
3.256 lemmas segment = open_segment_def closed_segment_def
3.257
3.258 @@ -3968,15 +3967,15 @@
3.259 lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps)
3.260
3.261 lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
3.262 - unfolding between_def mem_def by auto
3.263 + unfolding between_def by auto
3.264
3.265 lemma between:"between (a,b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
3.266 proof(cases "a = b")
3.267 - case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
3.268 + case True thus ?thesis unfolding between_def split_conv
3.269 by(auto simp add:segment_refl dist_commute) next
3.270 case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto
3.271 have *:"\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps)
3.272 - show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq
3.273 + show ?thesis unfolding between_def split_conv closed_segment_def mem_Collect_eq
3.274 apply rule apply(erule exE, (erule conjE)+) apply(subst dist_triangle_eq) proof-
3.275 fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
3.276 hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
3.277 @@ -4743,8 +4742,8 @@
3.278 { fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto }
3.279 hence "y : Inter {closure S |S. S : I}" by auto
3.280 } hence "Inter I <= Inter {closure S |S. S : I}" by auto
3.281 -moreover have "Inter {closure S |S. S : I} : closed"
3.282 - unfolding mem_def closed_Inter closed_closure by auto
3.283 +moreover have "closed (Inter {closure S |S. S : I})"
3.284 + unfolding closed_Inter closed_closure by auto
3.285 ultimately show ?thesis using closure_hull[of "Inter I"]
3.286 hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto
3.287 qed
3.288 @@ -5074,8 +5073,8 @@
3.289 using I_def u_def by auto
3.290 }
3.291 hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto
3.292 -moreover have "(convex hull S) <*> (convex hull T) : convex"
3.293 - unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull)
3.294 +moreover have "convex ((convex hull S) <*> (convex hull T))"
3.295 + by (simp add: convex_direct_sum convex_convex_hull)
3.296 ultimately show ?thesis
3.297 using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"]
3.298 hull_subset[of S convex] hull_subset[of T convex] by auto
3.299 @@ -5384,7 +5383,6 @@
3.300 finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
3.301 hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
3.302 } hence "convex ?rhs" unfolding convex_def by auto
3.303 -hence "?rhs : convex" unfolding mem_def by auto
3.304 from this show ?thesis using `?lhs >= ?rhs` *
3.305 hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
3.306 qed
3.307 @@ -5578,7 +5576,7 @@
3.308 hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto
3.309 }
3.310 hence "K0 >= Union (K ` I)" by auto
3.311 - moreover have "K0 : convex" unfolding mem_def K0_def
3.312 + moreover have "convex K0" unfolding K0_def
3.313 apply (subst convex_cone_hull) apply (subst convex_direct_sum)
3.314 unfolding C0_def using convex_convex_hull by auto
3.315 ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
3.316 @@ -5587,7 +5585,7 @@
3.317 hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
3.318 hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
3.319 using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
3.320 - moreover have "convex hull(Union (K ` I)) : cone" unfolding mem_def apply (subst cone_convex_hull)
3.321 + moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
3.322 using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
3.323 ultimately have "convex hull (Union (K ` I)) >= K0"
3.324 unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast
4.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 07:18:28 2011 -0700
4.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 09:17:24 2011 -0700
4.3 @@ -102,7 +102,7 @@
4.4 then show False using MInf by auto
4.5 next
4.6 case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
4.7 - then show False by (metis `Inf S ~: S` insert_code mem_def PInf)
4.8 + then show False using `Inf S ~: S` by simp
4.9 next
4.10 case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
4.11 from ereal_open_cont_interval[OF a this] guess e . note e = this
4.12 @@ -284,22 +284,22 @@
4.13 lemma ereal_open_mono_set:
4.14 fixes S :: "ereal set"
4.15 defines "a \<equiv> Inf S"
4.16 - shows "(open S \<and> mono S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
4.17 + shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
4.18 by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff ereal_open_atLeast
4.19 ereal_open_closed mono_set_iff open_ereal_greaterThan)
4.20
4.21 lemma ereal_closed_mono_set:
4.22 fixes S :: "ereal set"
4.23 - shows "(closed S \<and> mono S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
4.24 + shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
4.25 by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
4.26 ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
4.27
4.28 lemma ereal_Liminf_Sup_monoset:
4.29 fixes f :: "'a => ereal"
4.30 - shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
4.31 + shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
4.32 unfolding Liminf_Sup
4.33 proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
4.34 - fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono S" "l \<in> S"
4.35 + fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
4.36 then have "S = UNIV \<or> S = {Inf S <..}"
4.37 using ereal_open_mono_set[of S] by auto
4.38 then show "eventually (\<lambda>x. f x \<in> S) net"
4.39 @@ -310,7 +310,7 @@
4.40 then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
4.41 qed auto
4.42 next
4.43 - fix l y assume S: "\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "y < l"
4.44 + fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "y < l"
4.45 have "eventually (\<lambda>x. f x \<in> {y <..}) net"
4.46 using `y < l` by (intro S[rule_format]) auto
4.47 then show "eventually (\<lambda>x. y < f x) net" by auto
4.48 @@ -318,11 +318,11 @@
4.49
4.50 lemma ereal_Limsup_Inf_monoset:
4.51 fixes f :: "'a => ereal"
4.52 - shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
4.53 + shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
4.54 unfolding Limsup_Inf
4.55 proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
4.56 - fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono (uminus`S)" "l \<in> S"
4.57 - then have "open (uminus`S) \<and> mono (uminus`S)" by (simp add: ereal_open_uminus)
4.58 + fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
4.59 + then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
4.60 then have "S = UNIV \<or> S = {..< Sup S}"
4.61 unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
4.62 then show "eventually (\<lambda>x. f x \<in> S) net"
4.63 @@ -333,7 +333,7 @@
4.64 then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
4.65 qed auto
4.66 next
4.67 - fix l y assume S: "\<forall>S. open S \<longrightarrow> mono (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "l < y"
4.68 + fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net" "l < y"
4.69 have "eventually (\<lambda>x. f x \<in> {..< y}) net"
4.70 using `l < y` by (intro S[rule_format]) auto
4.71 then show "eventually (\<lambda>x. f x < y) net" by auto
4.72 @@ -469,7 +469,7 @@
4.73
4.74 lemma liminf_bounded_open:
4.75 fixes x :: "nat \<Rightarrow> ereal"
4.76 - shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
4.77 + shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
4.78 (is "_ \<longleftrightarrow> ?P x0")
4.79 proof
4.80 assume "?P x0" then show "x0 \<le> liminf x"
4.81 @@ -477,7 +477,7 @@
4.82 by (intro complete_lattice_class.Sup_upper) auto
4.83 next
4.84 assume "x0 \<le> liminf x"
4.85 - { fix S :: "ereal set" assume om: "open S & mono S & x0:S"
4.86 + { fix S :: "ereal set" assume om: "open S & mono_set S & x0:S"
4.87 { assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto }
4.88 moreover
4.89 { assume "~(S=UNIV)"
4.90 @@ -641,7 +641,7 @@
4.91 shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
4.92 proof-
4.93 let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
4.94 -{ fix T assume T_def: "open T & mono T & ?l:T"
4.95 +{ fix T assume T_def: "open T & mono_set T & ?l:T"
4.96 have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
4.97 proof-
4.98 { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
4.99 @@ -660,7 +660,7 @@
4.100 }
4.101 moreover
4.102 { fix z
4.103 - assume a: "ALL T. open T --> mono T --> z : T -->
4.104 + assume a: "ALL T. open T --> mono_set T --> z : T -->
4.105 (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
4.106 { fix B assume "B<z"
4.107 then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
4.108 @@ -683,7 +683,7 @@
4.109 shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
4.110 proof-
4.111 let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
4.112 -{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T"
4.113 +{ fix T assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
4.114 have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
4.115 proof-
4.116 { assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
4.117 @@ -707,7 +707,7 @@
4.118 }
4.119 moreover
4.120 { fix z
4.121 - assume a: "ALL T. open T --> mono (uminus ` T) --> z : T -->
4.122 + assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
4.123 (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
4.124 { fix B assume "z<B"
4.125 then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 12 07:18:28 2011 -0700
5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 12 09:17:24 2011 -0700
5.3 @@ -1584,11 +1584,11 @@
5.4 have lem1: "\<And>f P Q. (\<forall>x k. (x,k) \<in> {(x,f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow> (\<forall>x k. P x k \<longrightarrow> Q x (f k))" by auto
5.5 have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
5.6 proof- case goal1 thus ?case apply-apply(rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"]) by auto qed
5.7 - have lem3: "\<And>g::('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool. finite p \<Longrightarrow>
5.8 + have lem3: "\<And>g::'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
5.9 setsum (\<lambda>(x,k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> ~(g k = {})}
5.10 = setsum (\<lambda>(x,k). content k *\<^sub>R f x) ((\<lambda>(x,k). (x,g k)) ` p)"
5.11 apply(rule setsum_mono_zero_left) prefer 3
5.12 - proof fix g::"('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" and i::"('a) \<times> (('a) set)"
5.13 + proof fix g::"'a set \<Rightarrow> 'a set" and i::"('a) \<times> (('a) set)"
5.14 assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
5.15 then obtain x k where xk:"i=(x,g k)" "(x,k)\<in>p" "(x,g k) \<notin> {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}" by auto
5.16 have "content (g k) = 0" using xk using content_empty by auto
5.17 @@ -3004,9 +3004,9 @@
5.18
5.19 lemma gauge_modify:
5.20 assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d"
5.21 - shows "gauge (\<lambda>x y. d (f x) (f y))"
5.22 + shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
5.23 using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE)
5.24 - apply(erule_tac x="d (f x)" in allE) unfolding mem_def Collect_def by auto
5.25 + apply(erule_tac x="d (f x)" in allE) by auto
5.26
5.27 subsection {* Only need trivial subintervals if the interval itself is trivial. *}
5.28
5.29 @@ -3194,7 +3194,7 @@
5.30 show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz)
5.31 proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos)
5.32 from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format]
5.33 - def d' \<equiv> "\<lambda>x y. d (g x) (g y)" have d':"\<And>x. d' x = {y. g y \<in> (d (g x))}" unfolding d'_def by(auto simp add:mem_def)
5.34 + def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}" have d':"\<And>x. d' x = {y. g y \<in> (d (g x))}" unfolding d'_def ..
5.35 show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` {a..b} \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
5.36 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
5.37 fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)]
6.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 12 07:18:28 2011 -0700
6.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 12 09:17:24 2011 -0700
6.3 @@ -648,17 +648,17 @@
6.4
6.5 subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
6.6
6.7 -definition hull :: "'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
6.8 - "S hull s = Inter {t. t \<in> S \<and> s \<subseteq> t}"
6.9 -
6.10 -lemma hull_same: "s \<in> S \<Longrightarrow> S hull s = s"
6.11 +definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
6.12 + "S hull s = Inter {t. S t \<and> s \<subseteq> t}"
6.13 +
6.14 +lemma hull_same: "S s \<Longrightarrow> S hull s = s"
6.15 unfolding hull_def by auto
6.16
6.17 -lemma hull_in: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) \<in> S"
6.18 -unfolding hull_def subset_iff by auto
6.19 -
6.20 -lemma hull_eq: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) = s \<longleftrightarrow> s \<in> S"
6.21 -using hull_same[of s S] hull_in[of S s] by metis
6.22 +lemma hull_in: "(\<And>T. Ball T S ==> S (Inter T)) ==> S (S hull s)"
6.23 +unfolding hull_def Ball_def by auto
6.24 +
6.25 +lemma hull_eq: "(\<And>T. Ball T S ==> S (Inter T)) ==> (S hull s) = s \<longleftrightarrow> S s"
6.26 +using hull_same[of S s] hull_in[of S s] by metis
6.27
6.28
6.29 lemma hull_hull: "S hull (S hull s) = S hull s"
6.30 @@ -670,29 +670,29 @@
6.31 lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"
6.32 unfolding hull_def by blast
6.33
6.34 -lemma hull_antimono: "S \<subseteq> T ==> (T hull s) \<subseteq> (S hull s)"
6.35 +lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x ==> (T hull s) \<subseteq> (S hull s)"
6.36 unfolding hull_def by blast
6.37
6.38 -lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> t \<in> S ==> (S hull s) \<subseteq> t"
6.39 +lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t ==> (S hull s) \<subseteq> t"
6.40 unfolding hull_def by blast
6.41
6.42 -lemma subset_hull: "t \<in> S ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
6.43 +lemma subset_hull: "S t ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
6.44 unfolding hull_def by blast
6.45
6.46 -lemma hull_unique: "s \<subseteq> t \<Longrightarrow> t \<in> S \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> t' \<in> S ==> t \<subseteq> t')
6.47 +lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' ==> t \<subseteq> t')
6.48 ==> (S hull s = t)"
6.49 unfolding hull_def by auto
6.50
6.51 lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
6.52 using hull_minimal[of S "{x. P x}" Q]
6.53 - by (auto simp add: subset_eq Collect_def mem_def)
6.54 + by (auto simp add: subset_eq)
6.55
6.56 lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S" by (metis hull_subset subset_eq)
6.57
6.58 lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
6.59 unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
6.60
6.61 -lemma hull_union: assumes T: "\<And>T. T \<subseteq> S ==> Inter T \<in> S"
6.62 +lemma hull_union: assumes T: "\<And>T. Ball T S ==> S (Inter T)"
6.63 shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
6.64 apply rule
6.65 apply (rule hull_mono)
6.66 @@ -907,24 +907,9 @@
6.67
6.68 lemma (in real_vector) subspace_span: "subspace(span S)"
6.69 unfolding span_def
6.70 - apply (rule hull_in[unfolded mem_def])
6.71 + apply (rule hull_in)
6.72 apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
6.73 apply auto
6.74 - apply (erule_tac x="X" in ballE)
6.75 - apply (simp add: mem_def)
6.76 - apply blast
6.77 - apply (erule_tac x="X" in ballE)
6.78 - apply (erule_tac x="X" in ballE)
6.79 - apply (erule_tac x="X" in ballE)
6.80 - apply (clarsimp simp add: mem_def)
6.81 - apply simp
6.82 - apply simp
6.83 - apply simp
6.84 - apply (erule_tac x="X" in ballE)
6.85 - apply (erule_tac x="X" in ballE)
6.86 - apply (simp add: mem_def)
6.87 - apply simp
6.88 - apply simp
6.89 done
6.90
6.91 lemma (in real_vector) span_clauses:
6.92 @@ -935,21 +920,18 @@
6.93 by (metis span_def hull_subset subset_eq)
6.94 (metis subspace_span subspace_def)+
6.95
6.96 -lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"
6.97 - and P: "subspace P" and x: "x \<in> span S" shows "P x"
6.98 +lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> x \<in> P"
6.99 + and P: "subspace P" and x: "x \<in> span S" shows "x \<in> P"
6.100 proof-
6.101 - from SP have SP': "S \<subseteq> P" by (simp add: mem_def subset_eq)
6.102 - from P have P': "P \<in> subspace" by (simp add: mem_def)
6.103 - from x hull_minimal[OF SP' P', unfolded span_def[symmetric]]
6.104 - show "P x" by (metis mem_def subset_eq)
6.105 + from SP have SP': "S \<subseteq> P" by (simp add: subset_eq)
6.106 + from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
6.107 + show "x \<in> P" by (metis subset_eq)
6.108 qed
6.109
6.110 lemma span_empty[simp]: "span {} = {0}"
6.111 apply (simp add: span_def)
6.112 apply (rule hull_unique)
6.113 - apply (auto simp add: mem_def subspace_def)
6.114 - unfolding mem_def[of "0::'a", symmetric]
6.115 - apply simp
6.116 + apply (auto simp add: subspace_def)
6.117 done
6.118
6.119 lemma (in real_vector) independent_empty[intro]: "independent {}"
6.120 @@ -968,21 +950,21 @@
6.121 done
6.122
6.123 lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B"
6.124 - by (metis order_antisym span_def hull_minimal mem_def)
6.125 + by (metis order_antisym span_def hull_minimal)
6.126
6.127 lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"
6.128 - and P: "subspace P" shows "\<forall>x \<in> span S. P x"
6.129 + and P: "subspace {x. P x}" shows "\<forall>x \<in> span S. P x"
6.130 using span_induct SP P by blast
6.131
6.132 -inductive (in real_vector) span_induct_alt_help for S:: "'a \<Rightarrow> bool"
6.133 +inductive_set (in real_vector) span_induct_alt_help for S:: "'a set"
6.134 where
6.135 - span_induct_alt_help_0: "span_induct_alt_help S 0"
6.136 - | span_induct_alt_help_S: "x \<in> S \<Longrightarrow> span_induct_alt_help S z \<Longrightarrow> span_induct_alt_help S (c *\<^sub>R x + z)"
6.137 + span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
6.138 + | span_induct_alt_help_S: "x \<in> S \<Longrightarrow> z \<in> span_induct_alt_help S \<Longrightarrow> (c *\<^sub>R x + z) \<in> span_induct_alt_help S"
6.139
6.140 lemma span_induct_alt':
6.141 assumes h0: "h 0" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c *\<^sub>R x + y)" shows "\<forall>x \<in> span S. h x"
6.142 proof-
6.143 - {fix x:: "'a" assume x: "span_induct_alt_help S x"
6.144 + {fix x:: "'a" assume x: "x \<in> span_induct_alt_help S"
6.145 have "h x"
6.146 apply (rule span_induct_alt_help.induct[OF x])
6.147 apply (rule h0)
6.148 @@ -991,19 +973,19 @@
6.149 note th0 = this
6.150 {fix x assume x: "x \<in> span S"
6.151
6.152 - have "span_induct_alt_help S x"
6.153 + have "x \<in> span_induct_alt_help S"
6.154 proof(rule span_induct[where x=x and S=S])
6.155 show "x \<in> span S" using x .
6.156 next
6.157 fix x assume xS : "x \<in> S"
6.158 from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
6.159 - show "span_induct_alt_help S x" by simp
6.160 + show "x \<in> span_induct_alt_help S" by simp
6.161 next
6.162 - have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0)
6.163 + have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
6.164 moreover
6.165 - {fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y"
6.166 + {fix x y assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
6.167 from h
6.168 - have "span_induct_alt_help S (x + y)"
6.169 + have "(x + y) \<in> span_induct_alt_help S"
6.170 apply (induct rule: span_induct_alt_help.induct)
6.171 apply simp
6.172 unfolding add_assoc
6.173 @@ -1012,8 +994,8 @@
6.174 apply simp
6.175 done}
6.176 moreover
6.177 - {fix c x assume xt: "span_induct_alt_help S x"
6.178 - then have "span_induct_alt_help S (c *\<^sub>R x)"
6.179 + {fix c x assume xt: "x \<in> span_induct_alt_help S"
6.180 + then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
6.181 apply (induct rule: span_induct_alt_help.induct)
6.182 apply (simp add: span_induct_alt_help_0)
6.183 apply (simp add: scaleR_right_distrib)
6.184 @@ -1023,7 +1005,7 @@
6.185 done
6.186 }
6.187 ultimately show "subspace (span_induct_alt_help S)"
6.188 - unfolding subspace_def mem_def Ball_def by blast
6.189 + unfolding subspace_def Ball_def by blast
6.190 qed}
6.191 with th0 show ?thesis by blast
6.192 qed
6.193 @@ -1081,23 +1063,22 @@
6.194 apply (clarsimp simp add: image_iff)
6.195 apply (frule span_superset)
6.196 apply blast
6.197 - apply (simp only: mem_def)
6.198 apply (rule subspace_linear_image[OF lf])
6.199 apply (rule subspace_span)
6.200 apply (rule x)
6.201 done}
6.202 moreover
6.203 {fix x assume x: "x \<in> span S"
6.204 - have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_eqI)
6.205 - unfolding mem_def Collect_def ..
6.206 - have "f x \<in> span (f ` S)"
6.207 + have "x \<in> {x. f x \<in> span (f ` S)}"
6.208 apply (rule span_induct[where S=S])
6.209 + apply simp
6.210 apply (rule span_superset)
6.211 apply simp
6.212 - apply (subst th0)
6.213 apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
6.214 apply (rule x)
6.215 - done}
6.216 + done
6.217 + hence "f x \<in> span (f ` S)" by simp
6.218 + }
6.219 ultimately show ?thesis by blast
6.220 qed
6.221
6.222 @@ -1120,29 +1101,27 @@
6.223 apply (rule exI[where x=0])
6.224 apply (rule span_superset)
6.225 by simp}
6.226 - ultimately have "?P x" by blast}
6.227 - moreover have "subspace ?P"
6.228 + ultimately have "x \<in> Collect ?P" by blast}
6.229 + moreover have "subspace (Collect ?P)"
6.230 unfolding subspace_def
6.231 apply auto
6.232 - apply (simp add: mem_def)
6.233 apply (rule exI[where x=0])
6.234 using span_0[of "S - {b}"]
6.235 - apply (simp add: mem_def)
6.236 - apply (clarsimp simp add: mem_def)
6.237 + apply simp
6.238 apply (rule_tac x="k + ka" in exI)
6.239 apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
6.240 apply (simp only: )
6.241 - apply (rule span_add[unfolded mem_def])
6.242 + apply (rule span_add)
6.243 apply assumption+
6.244 apply (simp add: algebra_simps)
6.245 - apply (clarsimp simp add: mem_def)
6.246 apply (rule_tac x= "c*k" in exI)
6.247 apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
6.248 apply (simp only: )
6.249 - apply (rule span_mul[unfolded mem_def])
6.250 + apply (rule span_mul)
6.251 apply assumption
6.252 by (simp add: algebra_simps)
6.253 - ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis
6.254 + ultimately have "a \<in> Collect ?P" using aS by (rule span_induct)
6.255 + thus "?P a" by simp
6.256 qed
6.257
6.258 lemma span_breakdown_eq:
6.259 @@ -1266,13 +1245,13 @@
6.260 by (auto intro: span_superset span_mul)}
6.261 moreover
6.262 have "\<forall>x \<in> span P. x \<in> ?E"
6.263 - unfolding mem_def Collect_def
6.264 proof(rule span_induct_alt')
6.265 - show "?h 0"
6.266 + show "0 \<in> Collect ?h"
6.267 + unfolding mem_Collect_eq
6.268 apply (rule exI[where x="{}"]) by simp
6.269 next
6.270 fix c x y
6.271 - assume x: "x \<in> P" and hy: "?h y"
6.272 + assume x: "x \<in> P" and hy: "y \<in> Collect ?h"
6.273 from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
6.274 and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
6.275 let ?S = "insert x S"
6.276 @@ -1303,7 +1282,8 @@
6.277 by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)}
6.278 ultimately have "?Q ?S ?u (c*\<^sub>R x + y)"
6.279 by (cases "x \<in> S", simp, simp)
6.280 - then show "?h (c*\<^sub>R x + y)"
6.281 + then show "(c*\<^sub>R x + y) \<in> Collect ?h"
6.282 + unfolding mem_Collect_eq
6.283 apply -
6.284 apply (rule exI[where x="?S"])
6.285 apply (rule exI[where x="?u"]) by metis
6.286 @@ -2268,7 +2248,7 @@
6.287 with a have a0:"?a \<noteq> 0" by auto
6.288 have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
6.289 proof(rule span_induct')
6.290 - show "subspace (\<lambda>x. ?a \<bullet> x = 0)" by (auto simp add: subspace_def mem_def inner_simps)
6.291 + show "subspace {x. ?a \<bullet> x = 0}" by (auto simp add: subspace_def inner_simps)
6.292 next
6.293 {fix x assume x: "x \<in> B"
6.294 from x have B': "B = insert x (B - {x})" by blast
6.295 @@ -2548,12 +2528,8 @@
6.296 lemma linear_eq_0_span:
6.297 assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
6.298 shows "\<forall>x \<in> span B. f x = 0"
6.299 -proof
6.300 - fix x assume x: "x \<in> span B"
6.301 - let ?P = "\<lambda>x. f x = 0"
6.302 - from subspace_kernel[OF lf] have "subspace ?P" unfolding Collect_def .
6.303 - with x f0 span_induct[of B "?P" x] show "f x = 0" by blast
6.304 -qed
6.305 + using f0 subspace_kernel[OF lf]
6.306 + by (rule span_induct')
6.307
6.308 lemma linear_eq_0:
6.309 assumes lf: "linear f" and SB: "S \<subseteq> span B" and f0: "\<forall>x\<in>B. f x = 0"
6.310 @@ -2594,24 +2570,19 @@
6.311 and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
6.312 shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
6.313 proof-
6.314 - let ?P = "\<lambda>x. \<forall>y\<in> span C. f x y = g x y"
6.315 + let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
6.316 from bf bg have sp: "subspace ?P"
6.317 unfolding bilinear_def linear_def subspace_def bf bg
6.318 - by(auto simp add: span_0 mem_def bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
6.319 + by(auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
6.320
6.321 have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
6.322 - apply -
6.323 + apply (rule span_induct' [OF _ sp])
6.324 apply (rule ballI)
6.325 - apply (rule span_induct[of B ?P])
6.326 - defer
6.327 - apply (rule sp)
6.328 - apply assumption
6.329 - apply (clarsimp simp add: Ball_def)
6.330 - apply (rule_tac P="\<lambda>y. f xa y = g xa y" and S=C in span_induct)
6.331 - using fg
6.332 + apply (rule span_induct')
6.333 + apply (simp add: fg)
6.334 apply (auto simp add: subspace_def)
6.335 using bf bg unfolding bilinear_def linear_def
6.336 - by(auto simp add: span_0 mem_def bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
6.337 + by(auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
6.338 then show ?thesis using SB TC by (auto intro: ext)
6.339 qed
6.340
7.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 12 07:18:28 2011 -0700
7.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 12 09:17:24 2011 -0700
7.3 @@ -387,16 +387,14 @@
7.4
7.5 subsection {* Can also consider it as a set, as the name suggests. *}
7.6
7.7 -lemma path_component_set: "path_component s x = { y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y )}"
7.8 - apply(rule set_eqI) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto
7.9 +lemma path_component_set: "{y. path_component s x y} = { y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y )}"
7.10 + apply(rule set_eqI) unfolding mem_Collect_eq unfolding path_component_def by auto
7.11
7.12 -lemma mem_path_component_set:"x \<in> path_component s y \<longleftrightarrow> path_component s y x" unfolding mem_def by auto
7.13 +lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
7.14 + apply(rule, rule path_component_mem(2)) by auto
7.15
7.16 -lemma path_component_subset: "(path_component s x) \<subseteq> s"
7.17 - apply(rule, rule path_component_mem(2)) by(auto simp add:mem_def)
7.18 -
7.19 -lemma path_component_eq_empty: "path_component s x = {} \<longleftrightarrow> x \<notin> s"
7.20 - apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_path_component_set
7.21 +lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s"
7.22 + apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_Collect_eq
7.23 apply(drule path_component_mem(1)) using path_component_refl by auto
7.24
7.25 subsection {* Path connectedness of a space. *}
7.26 @@ -406,9 +404,9 @@
7.27 lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
7.28 unfolding path_connected_def path_component_def by auto
7.29
7.30 -lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. path_component s x = s)"
7.31 +lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)"
7.32 unfolding path_connected_component apply(rule, rule, rule, rule path_component_subset)
7.33 - unfolding subset_eq mem_path_component_set Ball_def mem_def by auto
7.34 + unfolding subset_eq mem_Collect_eq Ball_def by auto
7.35
7.36 subsection {* Some useful lemmas about path-connectedness. *}
7.37
7.38 @@ -435,25 +433,25 @@
7.39
7.40 lemma open_path_component:
7.41 fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
7.42 - assumes "open s" shows "open(path_component s x)"
7.43 + assumes "open s" shows "open {y. path_component s x y}"
7.44 unfolding open_contains_ball proof
7.45 - fix y assume as:"y \<in> path_component s x"
7.46 - hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto
7.47 + fix y assume as:"y \<in> {y. path_component s x y}"
7.48 + hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_Collect_eq by auto
7.49 then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
7.50 - show "\<exists>e>0. ball y e \<subseteq> path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule) unfolding mem_ball mem_path_component_set proof-
7.51 + show "\<exists>e>0. ball y e \<subseteq> {y. path_component s x y}" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule) unfolding mem_ball mem_Collect_eq proof-
7.52 fix z assume "dist y z < e" thus "path_component s x z" apply(rule_tac path_component_trans[of _ _ y]) defer
7.53 apply(rule path_component_of_subset[OF e(2)]) apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) using `e>0`
7.54 - using as[unfolded mem_def] by auto qed qed
7.55 + using as by auto qed qed
7.56
7.57 lemma open_non_path_component:
7.58 fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
7.59 - assumes "open s" shows "open(s - path_component s x)"
7.60 + assumes "open s" shows "open(s - {y. path_component s x y})"
7.61 unfolding open_contains_ball proof
7.62 - fix y assume as:"y\<in>s - path_component s x"
7.63 + fix y assume as:"y\<in>s - {y. path_component s x y}"
7.64 then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
7.65 - show "\<exists>e>0. ball y e \<subseteq> s - path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr)
7.66 - fix z assume "z\<in>ball y e" "\<not> z \<notin> path_component s x"
7.67 - hence "y \<in> path_component s x" unfolding not_not mem_path_component_set using `e>0`
7.68 + show "\<exists>e>0. ball y e \<subseteq> s - {y. path_component s x y}" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr)
7.69 + fix z assume "z\<in>ball y e" "\<not> z \<notin> {y. path_component s x y}"
7.70 + hence "y \<in> {y. path_component s x y}" unfolding not_not mem_Collect_eq using `e>0`
7.71 apply- apply(rule path_component_trans,assumption) apply(rule path_component_of_subset[OF e(2)])
7.72 apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto
7.73 thus False using as by auto qed(insert e(2), auto) qed
7.74 @@ -462,11 +460,11 @@
7.75 fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
7.76 assumes "open s" "connected s" shows "path_connected s"
7.77 unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule)
7.78 - fix x y assume "x \<in> s" "y \<in> s" show "y \<in> path_component s x" proof(rule ccontr)
7.79 - assume "y \<notin> path_component s x" moreover
7.80 - have "path_component s x \<inter> s \<noteq> {}" using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto
7.81 + fix x y assume "x \<in> s" "y \<in> s" show "y \<in> {y. path_component s x y}" proof(rule ccontr)
7.82 + assume "y \<notin> {y. path_component s x y}" moreover
7.83 + have "{y. path_component s x y} \<inter> s \<noteq> {}" using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto
7.84 ultimately show False using `y\<in>s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
7.85 - using assms(2)[unfolded connected_def not_ex, rule_format, of"path_component s x" "s - path_component s x"] by auto
7.86 + using assms(2)[unfolded connected_def not_ex, rule_format, of"{y. path_component s x y}" "s - {y. path_component s x y}"] by auto
7.87 qed qed
7.88
7.89 lemma path_connected_continuous_image:
8.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700
8.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700
8.3 @@ -22,8 +22,8 @@
8.4
8.5 subsection{* General notion of a topology *}
8.6
8.7 -definition "istopology L \<longleftrightarrow> {} \<in> L \<and> (\<forall>S \<in>L. \<forall>T \<in>L. S \<inter> T \<in> L) \<and> (\<forall>K. K \<subseteq>L \<longrightarrow> \<Union> K \<in> L)"
8.8 -typedef (open) 'a topology = "{L::('a set) set. istopology L}"
8.9 +definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
8.10 +typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
8.11 morphisms "openin" "topology"
8.12 unfolding istopology_def by blast
8.13
8.14 @@ -31,7 +31,7 @@
8.15 using openin[of U] by blast
8.16
8.17 lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
8.18 - using topology_inverse[unfolded mem_def Collect_def] .
8.19 + using topology_inverse[unfolded mem_Collect_eq] .
8.20
8.21 lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
8.22 using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
8.23 @@ -41,7 +41,7 @@
8.24 {assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
8.25 moreover
8.26 {assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
8.27 - hence "openin T1 = openin T2" by (metis mem_def set_eqI)
8.28 + hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
8.29 hence "topology (openin T1) = topology (openin T2)" by simp
8.30 hence "T1 = T2" unfolding openin_inverse .}
8.31 ultimately show ?thesis by blast
8.32 @@ -58,8 +58,8 @@
8.33 shows "openin U {}"
8.34 "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
8.35 "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
8.36 - using openin[of U] unfolding istopology_def Collect_def mem_def
8.37 - unfolding subset_eq Ball_def mem_def by auto
8.38 + using openin[of U] unfolding istopology_def mem_Collect_eq
8.39 + by fast+
8.40
8.41 lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
8.42 unfolding topspace_def by blast
8.43 @@ -130,33 +130,38 @@
8.44
8.45 subsection{* Subspace topology. *}
8.46
8.47 -definition "subtopology U V = topology {S \<inter> V |S. openin U S}"
8.48 -
8.49 -lemma istopology_subtopology: "istopology {S \<inter> V |S. openin U S}" (is "istopology ?L")
8.50 +term "{f x |x. P x}"
8.51 +term "{y. \<exists>x. y = f x \<and> P x}"
8.52 +
8.53 +definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
8.54 +
8.55 +lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
8.56 + (is "istopology ?L")
8.57 proof-
8.58 - have "{} \<in> ?L" by blast
8.59 - {fix A B assume A: "A \<in> ?L" and B: "B \<in> ?L"
8.60 + have "?L {}" by blast
8.61 + {fix A B assume A: "?L A" and B: "?L B"
8.62 from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" by blast
8.63 have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+
8.64 - then have "A \<inter> B \<in> ?L" by blast}
8.65 + then have "?L (A \<inter> B)" by blast}
8.66 moreover
8.67 - {fix K assume K: "K \<subseteq> ?L"
8.68 - have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U "
8.69 + {fix K assume K: "K \<subseteq> Collect ?L"
8.70 + have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
8.71 apply (rule set_eqI)
8.72 apply (simp add: Ball_def image_iff)
8.73 - by (metis mem_def)
8.74 + by metis
8.75 from K[unfolded th0 subset_image_iff]
8.76 - obtain Sk where Sk: "Sk \<subseteq> openin U" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
8.77 + obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
8.78 have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto
8.79 - moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq mem_def)
8.80 - ultimately have "\<Union>K \<in> ?L" by blast}
8.81 - ultimately show ?thesis unfolding istopology_def by blast
8.82 + moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq)
8.83 + ultimately have "?L (\<Union>K)" by blast}
8.84 + ultimately show ?thesis
8.85 + unfolding subset_eq mem_Collect_eq istopology_def by blast
8.86 qed
8.87
8.88 lemma openin_subtopology:
8.89 "openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))"
8.90 unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
8.91 - by (auto simp add: Collect_def)
8.92 + by auto
8.93
8.94 lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V"
8.95 by (auto simp add: topspace_def openin_subtopology)
8.96 @@ -210,7 +215,7 @@
8.97 apply (rule cong[where x=S and y=S])
8.98 apply (rule topology_inverse[symmetric])
8.99 apply (auto simp add: istopology_def)
8.100 - by (auto simp add: mem_def subset_eq)
8.101 + done
8.102
8.103 lemma topspace_euclidean: "topspace euclidean = UNIV"
8.104 apply (simp add: topspace_def)
8.105 @@ -266,7 +271,7 @@
8.106 "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+
8.107
8.108 lemma open_ball[intro, simp]: "open (ball x e)"
8.109 - unfolding open_dist ball_def Collect_def Ball_def mem_def
8.110 + unfolding open_dist ball_def mem_Collect_eq Ball_def
8.111 unfolding dist_commute
8.112 apply clarify
8.113 apply (rule_tac x="e - dist xa x" in exI)
8.114 @@ -492,7 +497,7 @@
8.115 unfolding closed_def
8.116 apply (subst open_subopen)
8.117 apply (simp add: islimpt_def subset_eq)
8.118 - by (metis ComplE ComplI insertCI insert_absorb mem_def)
8.119 + by (metis ComplE ComplI)
8.120
8.121 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
8.122 unfolding islimpt_def by auto
8.123 @@ -691,14 +696,13 @@
8.124 }
8.125 ultimately show ?thesis
8.126 using hull_unique[of S, of "closure S", of closed]
8.127 - unfolding mem_def
8.128 by simp
8.129 qed
8.130
8.131 lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
8.132 unfolding closure_hull
8.133 - using hull_eq[of closed, unfolded mem_def, OF closed_Inter, of S]
8.134 - by (metis mem_def subset_eq)
8.135 + using hull_eq[of closed, OF closed_Inter, of S]
8.136 + by metis
8.137
8.138 lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
8.139 using closure_eq[of S]
8.140 @@ -721,12 +725,12 @@
8.141
8.142 lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
8.143 using hull_minimal[of S T closed]
8.144 - unfolding closure_hull mem_def
8.145 + unfolding closure_hull
8.146 by simp
8.147
8.148 lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
8.149 using hull_unique[of S T closed]
8.150 - unfolding closure_hull mem_def
8.151 + unfolding closure_hull
8.152 by simp
8.153
8.154 lemma closure_empty[simp]: "closure {} = {}"
8.155 @@ -1623,7 +1627,7 @@
8.156 qed
8.157
8.158 lemma open_contains_cball_eq: "open S ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
8.159 - by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball mem_def)
8.160 + by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
8.161
8.162 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
8.163 apply (simp add: interior_def, safe)