make Multivariate_Analysis work with separate set type
authorhuffman
Fri Aug 12 09:17:24 2011 -0700 (2011-08-12)
changeset 44170510ac30f44c0
parent 44169 bdcc11b2fdc8
child 44171 75ea0e390a92
make Multivariate_Analysis work with separate set type
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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 -
    7.10 -lemma mem_path_component_set:"x \<in> path_component s y \<longleftrightarrow> path_component s y x" unfolding mem_def by auto
    7.11 +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.12 +  apply(rule set_eqI) unfolding mem_Collect_eq unfolding path_component_def by auto
    7.13  
    7.14 -lemma path_component_subset: "(path_component s x) \<subseteq> s"
    7.15 -  apply(rule, rule path_component_mem(2)) by(auto simp add:mem_def)
    7.16 +lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
    7.17 +  apply(rule, rule path_component_mem(2)) by auto
    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)