--- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 09:17:24 2011 -0700
@@ -1370,7 +1370,7 @@
}
moreover
{ assume "?lhs" hence "?rhs"
- by (metis Collect_def Collect_mem_eq SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
+ by (metis SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
} ultimately show ?thesis by auto
qed
@@ -1390,7 +1390,7 @@
}
moreover
{ assume "?lhs" hence "?rhs"
- by (metis Collect_def Collect_mem_eq le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
+ by (metis le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
} ultimately show ?thesis by auto
qed
@@ -2210,21 +2210,20 @@
qed
qed auto
-lemma (in order) mono_set:
- "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
- by (auto simp: mono_def mem_def)
+definition (in order) mono_set:
+ "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
-lemma (in order) mono_greaterThan [intro, simp]: "mono {B<..}" unfolding mono_set by auto
-lemma (in order) mono_atLeast [intro, simp]: "mono {B..}" unfolding mono_set by auto
-lemma (in order) mono_UNIV [intro, simp]: "mono UNIV" unfolding mono_set by auto
-lemma (in order) mono_empty [intro, simp]: "mono {}" unfolding mono_set by auto
+lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
+lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
+lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
+lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
lemma (in complete_linorder) mono_set_iff:
fixes S :: "'a set"
defines "a \<equiv> Inf S"
- shows "mono S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
+ shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
proof
- assume "mono S"
+ assume "mono_set S"
then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
show ?c
proof cases
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700
@@ -762,7 +762,7 @@
apply auto
apply (rule span_mul)
apply (rule span_superset)
-apply (auto simp add: Collect_def mem_def)
+apply auto
done
lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
@@ -785,12 +785,12 @@
proof-
let ?U = "UNIV :: 'n set"
let ?B = "cart_basis ` S"
- let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
+ let ?P = "{(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0}"
{fix x::"real^_" assume xS: "x\<in> ?B"
- from xS have "?P x" by auto}
+ from xS have "x \<in> ?P" by auto}
moreover
have "subspace ?P"
- by (auto simp add: subspace_def Collect_def mem_def)
+ by (auto simp add: subspace_def)
ultimately show ?thesis
using x span_induct[of ?B ?P x] iS by blast
qed
@@ -830,7 +830,7 @@
from equalityD2[OF span_stdbasis]
have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
from linear_eq[OF lf lg IU] fg x
- have "f x = g x" unfolding Collect_def Ball_def mem_def by metis}
+ have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
then show ?thesis by (auto intro: ext)
qed
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700
@@ -101,9 +101,9 @@
lemma span_eq[simp]: "(span s = s) <-> subspace s"
proof-
- { fix f assume "f <= subspace"
- hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto }
- thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto
+ { fix f assume "Ball f subspace"
+ hence "subspace (Inter f)" using subspace_Inter[of f] unfolding Ball_def by auto }
+ thus ?thesis using hull_eq[of subspace s] span_def by auto
qed
lemma basis_inj_on: "d \<subseteq> {..<DIM('n)} \<Longrightarrow> inj_on (basis :: nat => 'n::euclidean_space) d"
@@ -391,11 +391,11 @@
unfolding affine_def by auto
lemma affine_affine_hull: "affine(affine hull s)"
- unfolding hull_def using affine_Inter[of "{t \<in> affine. s \<subseteq> t}"]
- unfolding mem_def by auto
+ unfolding hull_def using affine_Inter[of "{t. affine t \<and> s \<subseteq> t}"]
+ by auto
lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
-by (metis affine_affine_hull hull_same mem_def)
+by (metis affine_affine_hull hull_same)
subsection {* Some explicit formulations (from Lars Schewe). *}
@@ -459,7 +459,7 @@
lemma affine_hull_explicit:
"affine hull p = {y. \<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}"
- apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq and mem_def[of _ affine]
+ apply(rule hull_unique) apply(subst subset_eq) prefer 3 apply rule unfolding mem_Collect_eq
apply (erule exE)+ apply(erule conjE)+ prefer 2 apply rule proof-
fix x assume "x\<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"
apply(rule_tac x="{x}" in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
@@ -500,7 +500,7 @@
subsection {* Stepping theorems and hence small special cases. *}
lemma affine_hull_empty[simp]: "affine hull {} = {}"
- apply(rule hull_unique) unfolding mem_def by auto
+ apply(rule hull_unique) by auto
lemma affine_hull_finite_step:
fixes y :: "'a::real_vector"
@@ -812,12 +812,11 @@
subsection {* Conic hull. *}
lemma cone_cone_hull: "cone (cone hull s)"
- unfolding hull_def using cone_Inter[of "{t \<in> conic. s \<subseteq> t}"]
- by (auto simp add: mem_def)
+ unfolding hull_def by auto
lemma cone_hull_eq: "(cone hull s = s) \<longleftrightarrow> cone s"
- apply(rule hull_eq[unfolded mem_def])
- using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
+ apply(rule hull_eq)
+ using cone_Inter unfolding subset_eq by auto
lemma mem_cone:
assumes "cone S" "x : S" "c>=0"
@@ -888,7 +887,7 @@
lemma mem_cone_hull:
assumes "x : S" "c>=0"
shows "c *\<^sub>R x : cone hull S"
-by (metis assms cone_cone_hull hull_inc mem_cone mem_def)
+by (metis assms cone_cone_hull hull_inc mem_cone)
lemma cone_hull_expl:
fixes S :: "('m::euclidean_space) set"
@@ -901,11 +900,11 @@
moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
} hence "cone ?rhs" unfolding cone_def by auto
- hence "?rhs : cone" unfolding mem_def by auto
+ hence "?rhs : Collect cone" unfolding mem_Collect_eq by auto
{ fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
hence "x : ?rhs" by auto
} hence "S <= ?rhs" by auto
-hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto
+hence "?lhs <= ?rhs" using `?rhs : Collect cone` hull_minimal[of S "?rhs" "cone"] by auto
moreover
{ fix x assume "x : ?rhs"
from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
@@ -1081,18 +1080,18 @@
subsection {* Convex hull. *}
lemma convex_convex_hull: "convex(convex hull s)"
- unfolding hull_def using convex_Inter[of "{t\<in>convex. s\<subseteq>t}"]
- unfolding mem_def by auto
+ unfolding hull_def using convex_Inter[of "{t. convex t \<and> s \<subseteq> t}"]
+ by auto
lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
-by (metis convex_convex_hull hull_same mem_def)
+by (metis convex_convex_hull hull_same)
lemma bounded_convex_hull:
fixes s :: "'a::real_normed_vector set"
assumes "bounded s" shows "bounded(convex hull s)"
proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
- unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
+ unfolding subset_hull[of convex, OF convex_cball]
unfolding subset_eq mem_cball dist_norm using B by auto qed
lemma finite_imp_bounded_convex_hull:
@@ -1125,17 +1124,17 @@
subsection {* Stepping theorems for convex hulls of finite sets. *}
lemma convex_hull_empty[simp]: "convex hull {} = {}"
- apply(rule hull_unique) unfolding mem_def by auto
+ apply(rule hull_unique) by auto
lemma convex_hull_singleton[simp]: "convex hull {a} = {a}"
- apply(rule hull_unique) unfolding mem_def by auto
+ apply(rule hull_unique) by auto
lemma convex_hull_insert:
fixes s :: "'a::real_vector set"
assumes "s \<noteq> {}"
shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
- apply(rule,rule hull_minimal,rule) unfolding mem_def[of _ convex] and insert_iff prefer 3 apply rule proof-
+ apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof-
fix x assume x:"x = a \<or> x \<in> s"
thus "x\<in>?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer
apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto
@@ -1192,7 +1191,7 @@
shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
(setsum u {1..k} = 1) \<and>
(setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
- apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
+ apply(rule hull_unique) apply(rule) defer
apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule)
proof-
fix x assume "x\<in>s"
@@ -1232,7 +1231,7 @@
assumes "finite s"
shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
-proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
+proof(rule hull_unique, auto simp add: convex_def[of ?set])
fix x assume "x\<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"
apply(rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) apply auto
unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto
@@ -1356,8 +1355,8 @@
apply(rule_tac x=u in exI) apply simp apply(rule_tac x="\<lambda>x. v" in exI) by simp qed
lemma convex_hull_2_alt: "convex hull {a,b} = {a + u *\<^sub>R (b - a) | u. 0 \<le> u \<and> u \<le> 1}"
- unfolding convex_hull_2 unfolding Collect_def
-proof(rule ext) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
+ unfolding convex_hull_2
+proof(rule Collect_cong) have *:"\<And>x y ::real. x + y = 1 \<longleftrightarrow> x = 1 - y" by auto
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)"
unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
@@ -1367,8 +1366,8 @@
have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
"\<And>x y z ::_::euclidean_space. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z" by (auto simp add: field_simps)
- show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and *
- unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto
+ show ?thesis unfolding convex_hull_finite[OF fin(1)] and convex_hull_finite_step[OF fin(2)] and *
+ unfolding convex_hull_finite_step[OF fin(3)] apply(rule Collect_cong) apply simp apply auto
apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp
apply(rule_tac x="1 - v - w" in exI) apply simp apply(rule_tac x=v in exI) apply simp apply(rule_tac x="\<lambda>x. w" in exI) by simp qed
@@ -1392,14 +1391,14 @@
lemma affine_hull_subset_span:
fixes s :: "(_::euclidean_space) set" shows "(affine hull s) \<subseteq> (span s)"
-by (metis hull_minimal mem_def span_inc subspace_imp_affine subspace_span)
+by (metis hull_minimal span_inc subspace_imp_affine subspace_span)
lemma convex_hull_subset_span:
fixes s :: "(_::euclidean_space) set" shows "(convex hull s) \<subseteq> (span s)"
-by (metis hull_minimal mem_def span_inc subspace_imp_convex subspace_span)
+by (metis hull_minimal span_inc subspace_imp_convex subspace_span)
lemma convex_hull_subset_affine_hull: "(convex hull s) \<subseteq> (affine hull s)"
-by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset mem_def)
+by (metis affine_affine_hull affine_imp_convex hull_minimal hull_subset)
lemma affine_dependent_imp_dependent:
@@ -1572,11 +1571,11 @@
proof-
have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto
moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
-ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def)
+ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal)
have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto
moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto
moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto
-ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal mem_def)
+ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal)
hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto
from this show ?thesis using h1 by auto
qed
@@ -3016,7 +3015,7 @@
then obtain a b where ab:"a \<noteq> 0" "0 < b" "\<forall>x\<in>convex hull c. b < inner a x"
using separating_hyperplane_closed_0[OF convex_convex_hull, of c]
using finite_imp_compact_convex_hull[OF c(3), THEN compact_imp_closed] and assms(2)
- using subset_hull[unfolded mem_def, of convex, OF assms(1), THEN sym, of c] by auto
+ using subset_hull[of convex, OF assms(1), THEN sym, of c] by auto
hence "\<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)
using hull_subset[of c convex] unfolding subset_eq and inner_scaleR
apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
@@ -3077,7 +3076,7 @@
lemma convex_hull_translation_lemma:
"convex hull ((\<lambda>x. a + x) ` s) \<subseteq> (\<lambda>x. a + x) ` (convex hull s)"
-by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono mem_def)
+by (metis convex_convex_hull convex_translation hull_minimal hull_subset image_mono)
lemma convex_hull_bilemma: fixes neg
assumes "(\<forall>s a. (convex hull (up a s)) \<subseteq> up a (convex hull s))"
@@ -3091,7 +3090,7 @@
lemma convex_hull_scaling_lemma:
"(convex hull ((\<lambda>x. c *\<^sub>R x) ` s)) \<subseteq> (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
-by (metis convex_convex_hull convex_scaling hull_subset mem_def subset_hull subset_image_iff)
+by (metis convex_convex_hull convex_scaling hull_subset subset_hull subset_image_iff)
lemma convex_hull_scaling:
"convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
@@ -3269,7 +3268,7 @@
unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
- apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding mem_def unfolding subset_eq
+ apply(rule_tac [!] hull_minimal) using Suc gh(3-4) unfolding subset_eq
apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof-
fix x assume "x\<in>X ` g" then guess y unfolding image_iff ..
thus "x\<in>\<Inter>h" using X[THEN bspec[where x=y]] using * f by auto next
@@ -3710,7 +3709,7 @@
apply(rule_tac n2="DIM('a)" in *) prefer 3 apply(subst(2) **)
apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
unfolding mem_interval apply rule unfolding mem_Collect_eq apply(erule_tac x=i in allE)
- by(auto simp add: mem_def[of _ convex]) qed
+ by auto qed
subsection {* And this is a finite set of vertices. *}
@@ -3883,7 +3882,7 @@
closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set" where
"closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
-definition "between = (\<lambda> (a,b). closed_segment a b)"
+definition "between = (\<lambda> (a,b) x. x \<in> closed_segment a b)"
lemmas segment = open_segment_def closed_segment_def
@@ -3968,15 +3967,15 @@
lemma segment_refl:"closed_segment a a = {a}" unfolding segment by (auto simp add: algebra_simps)
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
- unfolding between_def mem_def by auto
+ unfolding between_def by auto
lemma between:"between (a,b) (x::'a::euclidean_space) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
proof(cases "a = b")
- case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
+ case True thus ?thesis unfolding between_def split_conv
by(auto simp add:segment_refl dist_commute) next
case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto
have *:"\<And>u. a - ((1 - u) *\<^sub>R a + u *\<^sub>R b) = u *\<^sub>R (a - b)" by (auto simp add: algebra_simps)
- show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq
+ show ?thesis unfolding between_def split_conv closed_segment_def mem_Collect_eq
apply rule apply(erule exE, (erule conjE)+) apply(subst dist_triangle_eq) proof-
fix u assume as:"x = (1 - u) *\<^sub>R a + u *\<^sub>R b" "0 \<le> u" "u \<le> 1"
hence *:"a - x = u *\<^sub>R (a - b)" "x - b = (1 - u) *\<^sub>R (a - b)"
@@ -4743,8 +4742,8 @@
{ fix S assume "S : I" hence "y : closure S" using closure_subset y_def by auto }
hence "y : Inter {closure S |S. S : I}" by auto
} hence "Inter I <= Inter {closure S |S. S : I}" by auto
-moreover have "Inter {closure S |S. S : I} : closed"
- unfolding mem_def closed_Inter closed_closure by auto
+moreover have "closed (Inter {closure S |S. S : I})"
+ unfolding closed_Inter closed_closure by auto
ultimately show ?thesis using closure_hull[of "Inter I"]
hull_minimal[of "Inter I" "Inter {closure S |S. S : I}" "closed"] by auto
qed
@@ -5074,8 +5073,8 @@
using I_def u_def by auto
}
hence "convex hull (S <*> T) >= (convex hull S) <*> (convex hull T)" by auto
-moreover have "(convex hull S) <*> (convex hull T) : convex"
- unfolding mem_def by (simp add: convex_direct_sum convex_convex_hull)
+moreover have "convex ((convex hull S) <*> (convex hull T))"
+ by (simp add: convex_direct_sum convex_convex_hull)
ultimately show ?thesis
using hull_minimal[of "S <*> T" "(convex hull S) <*> (convex hull T)" "convex"]
hull_subset[of S convex] hull_subset[of T convex] by auto
@@ -5384,7 +5383,6 @@
finally have "u *\<^sub>R x + v *\<^sub>R y = setsum (%i. (e i) *\<^sub>R (q i)) I" by auto
hence "u *\<^sub>R x + v *\<^sub>R y : ?rhs" using ge0 sum1 qs by auto
} hence "convex ?rhs" unfolding convex_def by auto
-hence "?rhs : convex" unfolding mem_def by auto
from this show ?thesis using `?lhs >= ?rhs` *
hull_minimal[of "Union (S ` I)" "?rhs" "convex"] by blast
qed
@@ -5578,7 +5576,7 @@
hence "K0 >= K i" unfolding K0_def K_def apply (subst hull_mono) using `!i:I. C0 >= S i` by auto
}
hence "K0 >= Union (K ` I)" by auto
- moreover have "K0 : convex" unfolding mem_def K0_def
+ moreover have "convex K0" unfolding K0_def
apply (subst convex_cone_hull) apply (subst convex_direct_sum)
unfolding C0_def using convex_convex_hull by auto
ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
@@ -5587,7 +5585,7 @@
hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
- moreover have "convex hull(Union (K ` I)) : cone" unfolding mem_def apply (subst cone_convex_hull)
+ moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
ultimately have "convex hull (Union (K ` I)) >= K0"
unfolding K0_def using hull_minimal[of _ "convex hull (Union (K ` I))" "cone"] by blast
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Aug 12 09:17:24 2011 -0700
@@ -102,7 +102,7 @@
then show False using MInf by auto
next
case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
- then show False by (metis `Inf S ~: S` insert_code mem_def PInf)
+ then show False using `Inf S ~: S` by simp
next
case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
from ereal_open_cont_interval[OF a this] guess e . note e = this
@@ -284,22 +284,22 @@
lemma ereal_open_mono_set:
fixes S :: "ereal set"
defines "a \<equiv> Inf S"
- shows "(open S \<and> mono S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
+ shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {a <..})"
by (metis Inf_UNIV a_def atLeast_eq_UNIV_iff ereal_open_atLeast
ereal_open_closed mono_set_iff open_ereal_greaterThan)
lemma ereal_closed_mono_set:
fixes S :: "ereal set"
- shows "(closed S \<and> mono S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
+ shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
lemma ereal_Liminf_Sup_monoset:
fixes f :: "'a => ereal"
- shows "Liminf net f = Sup {l. \<forall>S. open S \<longrightarrow> mono S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
+ 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}"
unfolding Liminf_Sup
proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
- fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono S" "l \<in> S"
+ fix l S assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
then have "S = UNIV \<or> S = {Inf S <..}"
using ereal_open_mono_set[of S] by auto
then show "eventually (\<lambda>x. f x \<in> S) net"
@@ -310,7 +310,7 @@
then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
qed auto
next
- 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"
+ 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"
have "eventually (\<lambda>x. f x \<in> {y <..}) net"
using `y < l` by (intro S[rule_format]) auto
then show "eventually (\<lambda>x. y < f x) net" by auto
@@ -318,11 +318,11 @@
lemma ereal_Limsup_Inf_monoset:
fixes f :: "'a => ereal"
- shows "Limsup net f = Inf {l. \<forall>S. open S \<longrightarrow> mono (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
+ 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}"
unfolding Limsup_Inf
proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
- fix l S assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono (uminus`S)" "l \<in> S"
- then have "open (uminus`S) \<and> mono (uminus`S)" by (simp add: ereal_open_uminus)
+ 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"
+ then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
then have "S = UNIV \<or> S = {..< Sup S}"
unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
then show "eventually (\<lambda>x. f x \<in> S) net"
@@ -333,7 +333,7 @@
then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
qed auto
next
- 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"
+ 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"
have "eventually (\<lambda>x. f x \<in> {..< y}) net"
using `l < y` by (intro S[rule_format]) auto
then show "eventually (\<lambda>x. f x < y) net" by auto
@@ -469,7 +469,7 @@
lemma liminf_bounded_open:
fixes x :: "nat \<Rightarrow> ereal"
- 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))"
+ 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))"
(is "_ \<longleftrightarrow> ?P x0")
proof
assume "?P x0" then show "x0 \<le> liminf x"
@@ -477,7 +477,7 @@
by (intro complete_lattice_class.Sup_upper) auto
next
assume "x0 \<le> liminf x"
- { fix S :: "ereal set" assume om: "open S & mono S & x0:S"
+ { fix S :: "ereal set" assume om: "open S & mono_set S & x0:S"
{ assume "S = UNIV" hence "EX N. (ALL n>=N. x n : S)" by auto }
moreover
{ assume "~(S=UNIV)"
@@ -641,7 +641,7 @@
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
proof-
let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
-{ fix T assume T_def: "open T & mono T & ?l:T"
+{ fix T assume T_def: "open T & mono_set T & ?l:T"
have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
proof-
{ assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
@@ -660,7 +660,7 @@
}
moreover
{ fix z
- assume a: "ALL T. open T --> mono T --> z : T -->
+ assume a: "ALL T. open T --> mono_set T --> z : T -->
(EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
{ fix B assume "B<z"
then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
@@ -683,7 +683,7 @@
shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
proof-
let ?l="(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
-{ fix T assume T_def: "open T & mono (uminus ` T) & ?l:T"
+{ fix T assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
proof-
{ assume "T=UNIV" hence ?thesis by (simp add: gt_ex) }
@@ -707,7 +707,7 @@
}
moreover
{ fix z
- assume a: "ALL T. open T --> mono (uminus ` T) --> z : T -->
+ assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
(EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
{ fix B assume "z<B"
then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Aug 12 09:17:24 2011 -0700
@@ -1584,11 +1584,11 @@
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
have lem2: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
proof- case goal1 thus ?case apply-apply(rule finite_subset[of _ "(\<lambda>(x,k). (x,f k)) ` s"]) by auto qed
- have lem3: "\<And>g::('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool. finite p \<Longrightarrow>
+ have lem3: "\<And>g::'a set \<Rightarrow> 'a set. finite p \<Longrightarrow>
setsum (\<lambda>(x,k). content k *\<^sub>R f x) {(x,g k) |x k. (x,k) \<in> p \<and> ~(g k = {})}
= setsum (\<lambda>(x,k). content k *\<^sub>R f x) ((\<lambda>(x,k). (x,g k)) ` p)"
apply(rule setsum_mono_zero_left) prefer 3
- proof fix g::"('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" and i::"('a) \<times> (('a) set)"
+ proof fix g::"'a set \<Rightarrow> 'a set" and i::"('a) \<times> (('a) set)"
assume "i \<in> (\<lambda>(x, k). (x, g k)) ` p - {(x, g k) |x k. (x, k) \<in> p \<and> g k \<noteq> {}}"
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
have "content (g k) = 0" using xk using content_empty by auto
@@ -3004,9 +3004,9 @@
lemma gauge_modify:
assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d"
- shows "gauge (\<lambda>x y. d (f x) (f y))"
+ shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
using assms unfolding gauge_def apply safe defer apply(erule_tac x="f x" in allE)
- apply(erule_tac x="d (f x)" in allE) unfolding mem_def Collect_def by auto
+ apply(erule_tac x="d (f x)" in allE) by auto
subsection {* Only need trivial subintervals if the interval itself is trivial. *}
@@ -3194,7 +3194,7 @@
show ?thesis unfolding has_integral_def has_integral_compact_interval_def apply(subst if_P) apply(rule,rule,rule wz)
proof safe fix e::real assume e:"e>0" hence "e * r > 0" using assms(1) by(rule mult_pos_pos)
from assms(8)[unfolded has_integral,rule_format,OF this] guess d apply-by(erule exE conjE)+ note d=this[rule_format]
- def d' \<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)
+ 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 ..
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)"
proof(rule_tac x=d' in exI,safe) show "gauge d'" using d(1) unfolding gauge_def d' using continuous_open_preimage_univ[OF assms(4)] by auto
fix p assume as:"p tagged_division_of h ` {a..b}" "d' fine p" note p = tagged_division_ofD[OF as(1)]
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Aug 12 09:17:24 2011 -0700
@@ -648,17 +648,17 @@
subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *}
-definition hull :: "'a set set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
- "S hull s = Inter {t. t \<in> S \<and> s \<subseteq> t}"
-
-lemma hull_same: "s \<in> S \<Longrightarrow> S hull s = s"
+definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75) where
+ "S hull s = Inter {t. S t \<and> s \<subseteq> t}"
+
+lemma hull_same: "S s \<Longrightarrow> S hull s = s"
unfolding hull_def by auto
-lemma hull_in: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) \<in> S"
-unfolding hull_def subset_iff by auto
-
-lemma hull_eq: "(\<And>T. T \<subseteq> S ==> Inter T \<in> S) ==> (S hull s) = s \<longleftrightarrow> s \<in> S"
-using hull_same[of s S] hull_in[of S s] by metis
+lemma hull_in: "(\<And>T. Ball T S ==> S (Inter T)) ==> S (S hull s)"
+unfolding hull_def Ball_def by auto
+
+lemma hull_eq: "(\<And>T. Ball T S ==> S (Inter T)) ==> (S hull s) = s \<longleftrightarrow> S s"
+using hull_same[of S s] hull_in[of S s] by metis
lemma hull_hull: "S hull (S hull s) = S hull s"
@@ -670,29 +670,29 @@
lemma hull_mono: " s \<subseteq> t ==> (S hull s) \<subseteq> (S hull t)"
unfolding hull_def by blast
-lemma hull_antimono: "S \<subseteq> T ==> (T hull s) \<subseteq> (S hull s)"
+lemma hull_antimono: "\<forall>x. S x \<longrightarrow> T x ==> (T hull s) \<subseteq> (S hull s)"
unfolding hull_def by blast
-lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> t \<in> S ==> (S hull s) \<subseteq> t"
+lemma hull_minimal: "s \<subseteq> t \<Longrightarrow> S t ==> (S hull s) \<subseteq> t"
unfolding hull_def by blast
-lemma subset_hull: "t \<in> S ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
+lemma subset_hull: "S t ==> S hull s \<subseteq> t \<longleftrightarrow> s \<subseteq> t"
unfolding hull_def by blast
-lemma hull_unique: "s \<subseteq> t \<Longrightarrow> t \<in> S \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> t' \<in> S ==> t \<subseteq> t')
+lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' ==> t \<subseteq> t')
==> (S hull s = t)"
unfolding hull_def by auto
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"
using hull_minimal[of S "{x. P x}" Q]
- by (auto simp add: subset_eq Collect_def mem_def)
+ by (auto simp add: subset_eq)
lemma hull_inc: "x \<in> S \<Longrightarrow> x \<in> P hull S" by (metis hull_subset subset_eq)
lemma hull_union_subset: "(S hull s) \<union> (S hull t) \<subseteq> (S hull (s \<union> t))"
unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)
-lemma hull_union: assumes T: "\<And>T. T \<subseteq> S ==> Inter T \<in> S"
+lemma hull_union: assumes T: "\<And>T. Ball T S ==> S (Inter T)"
shows "S hull (s \<union> t) = S hull (S hull s \<union> S hull t)"
apply rule
apply (rule hull_mono)
@@ -907,24 +907,9 @@
lemma (in real_vector) subspace_span: "subspace(span S)"
unfolding span_def
- apply (rule hull_in[unfolded mem_def])
+ apply (rule hull_in)
apply (simp only: subspace_def Inter_iff Int_iff subset_eq)
apply auto
- apply (erule_tac x="X" in ballE)
- apply (simp add: mem_def)
- apply blast
- apply (erule_tac x="X" in ballE)
- apply (erule_tac x="X" in ballE)
- apply (erule_tac x="X" in ballE)
- apply (clarsimp simp add: mem_def)
- apply simp
- apply simp
- apply simp
- apply (erule_tac x="X" in ballE)
- apply (erule_tac x="X" in ballE)
- apply (simp add: mem_def)
- apply simp
- apply simp
done
lemma (in real_vector) span_clauses:
@@ -935,21 +920,18 @@
by (metis span_def hull_subset subset_eq)
(metis subspace_span subspace_def)+
-lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"
- and P: "subspace P" and x: "x \<in> span S" shows "P x"
+lemma (in real_vector) span_induct: assumes SP: "\<And>x. x \<in> S ==> x \<in> P"
+ and P: "subspace P" and x: "x \<in> span S" shows "x \<in> P"
proof-
- from SP have SP': "S \<subseteq> P" by (simp add: mem_def subset_eq)
- from P have P': "P \<in> subspace" by (simp add: mem_def)
- from x hull_minimal[OF SP' P', unfolded span_def[symmetric]]
- show "P x" by (metis mem_def subset_eq)
+ from SP have SP': "S \<subseteq> P" by (simp add: subset_eq)
+ from x hull_minimal[where S=subspace, OF SP' P, unfolded span_def[symmetric]]
+ show "x \<in> P" by (metis subset_eq)
qed
lemma span_empty[simp]: "span {} = {0}"
apply (simp add: span_def)
apply (rule hull_unique)
- apply (auto simp add: mem_def subspace_def)
- unfolding mem_def[of "0::'a", symmetric]
- apply simp
+ apply (auto simp add: subspace_def)
done
lemma (in real_vector) independent_empty[intro]: "independent {}"
@@ -968,21 +950,21 @@
done
lemma (in real_vector) span_subspace: "A \<subseteq> B \<Longrightarrow> B \<le> span A \<Longrightarrow> subspace B \<Longrightarrow> span A = B"
- by (metis order_antisym span_def hull_minimal mem_def)
+ by (metis order_antisym span_def hull_minimal)
lemma (in real_vector) span_induct': assumes SP: "\<forall>x \<in> S. P x"
- and P: "subspace P" shows "\<forall>x \<in> span S. P x"
+ and P: "subspace {x. P x}" shows "\<forall>x \<in> span S. P x"
using span_induct SP P by blast
-inductive (in real_vector) span_induct_alt_help for S:: "'a \<Rightarrow> bool"
+inductive_set (in real_vector) span_induct_alt_help for S:: "'a set"
where
- span_induct_alt_help_0: "span_induct_alt_help S 0"
- | 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)"
+ span_induct_alt_help_0: "0 \<in> span_induct_alt_help S"
+ | 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"
lemma span_induct_alt':
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"
proof-
- {fix x:: "'a" assume x: "span_induct_alt_help S x"
+ {fix x:: "'a" assume x: "x \<in> span_induct_alt_help S"
have "h x"
apply (rule span_induct_alt_help.induct[OF x])
apply (rule h0)
@@ -991,19 +973,19 @@
note th0 = this
{fix x assume x: "x \<in> span S"
- have "span_induct_alt_help S x"
+ have "x \<in> span_induct_alt_help S"
proof(rule span_induct[where x=x and S=S])
show "x \<in> span S" using x .
next
fix x assume xS : "x \<in> S"
from span_induct_alt_help_S[OF xS span_induct_alt_help_0, of 1]
- show "span_induct_alt_help S x" by simp
+ show "x \<in> span_induct_alt_help S" by simp
next
- have "span_induct_alt_help S 0" by (rule span_induct_alt_help_0)
+ have "0 \<in> span_induct_alt_help S" by (rule span_induct_alt_help_0)
moreover
- {fix x y assume h: "span_induct_alt_help S x" "span_induct_alt_help S y"
+ {fix x y assume h: "x \<in> span_induct_alt_help S" "y \<in> span_induct_alt_help S"
from h
- have "span_induct_alt_help S (x + y)"
+ have "(x + y) \<in> span_induct_alt_help S"
apply (induct rule: span_induct_alt_help.induct)
apply simp
unfolding add_assoc
@@ -1012,8 +994,8 @@
apply simp
done}
moreover
- {fix c x assume xt: "span_induct_alt_help S x"
- then have "span_induct_alt_help S (c *\<^sub>R x)"
+ {fix c x assume xt: "x \<in> span_induct_alt_help S"
+ then have "(c *\<^sub>R x) \<in> span_induct_alt_help S"
apply (induct rule: span_induct_alt_help.induct)
apply (simp add: span_induct_alt_help_0)
apply (simp add: scaleR_right_distrib)
@@ -1023,7 +1005,7 @@
done
}
ultimately show "subspace (span_induct_alt_help S)"
- unfolding subspace_def mem_def Ball_def by blast
+ unfolding subspace_def Ball_def by blast
qed}
with th0 show ?thesis by blast
qed
@@ -1081,23 +1063,22 @@
apply (clarsimp simp add: image_iff)
apply (frule span_superset)
apply blast
- apply (simp only: mem_def)
apply (rule subspace_linear_image[OF lf])
apply (rule subspace_span)
apply (rule x)
done}
moreover
{fix x assume x: "x \<in> span S"
- have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_eqI)
- unfolding mem_def Collect_def ..
- have "f x \<in> span (f ` S)"
+ have "x \<in> {x. f x \<in> span (f ` S)}"
apply (rule span_induct[where S=S])
+ apply simp
apply (rule span_superset)
apply simp
- apply (subst th0)
apply (rule subspace_linear_preimage[OF lf subspace_span, of "f ` S"])
apply (rule x)
- done}
+ done
+ hence "f x \<in> span (f ` S)" by simp
+ }
ultimately show ?thesis by blast
qed
@@ -1120,29 +1101,27 @@
apply (rule exI[where x=0])
apply (rule span_superset)
by simp}
- ultimately have "?P x" by blast}
- moreover have "subspace ?P"
+ ultimately have "x \<in> Collect ?P" by blast}
+ moreover have "subspace (Collect ?P)"
unfolding subspace_def
apply auto
- apply (simp add: mem_def)
apply (rule exI[where x=0])
using span_0[of "S - {b}"]
- apply (simp add: mem_def)
- apply (clarsimp simp add: mem_def)
+ apply simp
apply (rule_tac x="k + ka" in exI)
apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)")
apply (simp only: )
- apply (rule span_add[unfolded mem_def])
+ apply (rule span_add)
apply assumption+
apply (simp add: algebra_simps)
- apply (clarsimp simp add: mem_def)
apply (rule_tac x= "c*k" in exI)
apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)")
apply (simp only: )
- apply (rule span_mul[unfolded mem_def])
+ apply (rule span_mul)
apply assumption
by (simp add: algebra_simps)
- ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis
+ ultimately have "a \<in> Collect ?P" using aS by (rule span_induct)
+ thus "?P a" by simp
qed
lemma span_breakdown_eq:
@@ -1266,13 +1245,13 @@
by (auto intro: span_superset span_mul)}
moreover
have "\<forall>x \<in> span P. x \<in> ?E"
- unfolding mem_def Collect_def
proof(rule span_induct_alt')
- show "?h 0"
+ show "0 \<in> Collect ?h"
+ unfolding mem_Collect_eq
apply (rule exI[where x="{}"]) by simp
next
fix c x y
- assume x: "x \<in> P" and hy: "?h y"
+ assume x: "x \<in> P" and hy: "y \<in> Collect ?h"
from hy obtain S u where fS: "finite S" and SP: "S\<subseteq>P"
and u: "setsum (\<lambda>v. u v *\<^sub>R v) S = y" by blast
let ?S = "insert x S"
@@ -1303,7 +1282,8 @@
by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)}
ultimately have "?Q ?S ?u (c*\<^sub>R x + y)"
by (cases "x \<in> S", simp, simp)
- then show "?h (c*\<^sub>R x + y)"
+ then show "(c*\<^sub>R x + y) \<in> Collect ?h"
+ unfolding mem_Collect_eq
apply -
apply (rule exI[where x="?S"])
apply (rule exI[where x="?u"]) by metis
@@ -2268,7 +2248,7 @@
with a have a0:"?a \<noteq> 0" by auto
have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
proof(rule span_induct')
- show "subspace (\<lambda>x. ?a \<bullet> x = 0)" by (auto simp add: subspace_def mem_def inner_simps)
+ show "subspace {x. ?a \<bullet> x = 0}" by (auto simp add: subspace_def inner_simps)
next
{fix x assume x: "x \<in> B"
from x have B': "B = insert x (B - {x})" by blast
@@ -2548,12 +2528,8 @@
lemma linear_eq_0_span:
assumes lf: "linear f" and f0: "\<forall>x\<in>B. f x = 0"
shows "\<forall>x \<in> span B. f x = 0"
-proof
- fix x assume x: "x \<in> span B"
- let ?P = "\<lambda>x. f x = 0"
- from subspace_kernel[OF lf] have "subspace ?P" unfolding Collect_def .
- with x f0 span_induct[of B "?P" x] show "f x = 0" by blast
-qed
+ using f0 subspace_kernel[OF lf]
+ by (rule span_induct')
lemma linear_eq_0:
assumes lf: "linear f" and SB: "S \<subseteq> span B" and f0: "\<forall>x\<in>B. f x = 0"
@@ -2594,24 +2570,19 @@
and fg: "\<forall>x\<in> B. \<forall>y\<in> C. f x y = g x y"
shows "\<forall>x\<in>S. \<forall>y\<in>T. f x y = g x y "
proof-
- let ?P = "\<lambda>x. \<forall>y\<in> span C. f x y = g x y"
+ let ?P = "{x. \<forall>y\<in> span C. f x y = g x y}"
from bf bg have sp: "subspace ?P"
unfolding bilinear_def linear_def subspace_def bf bg
- 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])
+ by(auto simp add: span_0 bilinear_lzero[OF bf] bilinear_lzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
have "\<forall>x \<in> span B. \<forall>y\<in> span C. f x y = g x y"
- apply -
+ apply (rule span_induct' [OF _ sp])
apply (rule ballI)
- apply (rule span_induct[of B ?P])
- defer
- apply (rule sp)
- apply assumption
- apply (clarsimp simp add: Ball_def)
- apply (rule_tac P="\<lambda>y. f xa y = g xa y" and S=C in span_induct)
- using fg
+ apply (rule span_induct')
+ apply (simp add: fg)
apply (auto simp add: subspace_def)
using bf bg unfolding bilinear_def linear_def
- 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])
+ by(auto simp add: span_0 bilinear_rzero[OF bf] bilinear_rzero[OF bg] span_add Ball_def intro: bilinear_ladd[OF bf])
then show ?thesis using SB TC by (auto intro: ext)
qed
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Aug 12 09:17:24 2011 -0700
@@ -387,16 +387,14 @@
subsection {* Can also consider it as a set, as the name suggests. *}
-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 )}"
- apply(rule set_eqI) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto
-
-lemma mem_path_component_set:"x \<in> path_component s y \<longleftrightarrow> path_component s y x" unfolding mem_def by auto
+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 )}"
+ apply(rule set_eqI) unfolding mem_Collect_eq unfolding path_component_def by auto
-lemma path_component_subset: "(path_component s x) \<subseteq> s"
- apply(rule, rule path_component_mem(2)) by(auto simp add:mem_def)
+lemma path_component_subset: "{y. path_component s x y} \<subseteq> s"
+ apply(rule, rule path_component_mem(2)) by auto
-lemma path_component_eq_empty: "path_component s x = {} \<longleftrightarrow> x \<notin> s"
- apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_path_component_set
+lemma path_component_eq_empty: "{y. path_component s x y} = {} \<longleftrightarrow> x \<notin> s"
+ apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_Collect_eq
apply(drule path_component_mem(1)) using path_component_refl by auto
subsection {* Path connectedness of a space. *}
@@ -406,9 +404,9 @@
lemma path_connected_component: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. path_component s x y)"
unfolding path_connected_def path_component_def by auto
-lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. path_component s x = s)"
+lemma path_connected_component_set: "path_connected s \<longleftrightarrow> (\<forall>x\<in>s. {y. path_component s x y} = s)"
unfolding path_connected_component apply(rule, rule, rule, rule path_component_subset)
- unfolding subset_eq mem_path_component_set Ball_def mem_def by auto
+ unfolding subset_eq mem_Collect_eq Ball_def by auto
subsection {* Some useful lemmas about path-connectedness. *}
@@ -435,25 +433,25 @@
lemma open_path_component:
fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
- assumes "open s" shows "open(path_component s x)"
+ assumes "open s" shows "open {y. path_component s x y}"
unfolding open_contains_ball proof
- fix y assume as:"y \<in> path_component s x"
- hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto
+ fix y assume as:"y \<in> {y. path_component s x y}"
+ hence "y\<in>s" apply- apply(rule path_component_mem(2)) unfolding mem_Collect_eq by auto
then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
- 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-
+ 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-
fix z assume "dist y z < e" thus "path_component s x z" apply(rule_tac path_component_trans[of _ _ y]) defer
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`
- using as[unfolded mem_def] by auto qed qed
+ using as by auto qed qed
lemma open_non_path_component:
fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
- assumes "open s" shows "open(s - path_component s x)"
+ assumes "open s" shows "open(s - {y. path_component s x y})"
unfolding open_contains_ball proof
- fix y assume as:"y\<in>s - path_component s x"
+ fix y assume as:"y\<in>s - {y. path_component s x y}"
then obtain e where e:"e>0" "ball y e \<subseteq> s" using assms[unfolded open_contains_ball] by auto
- 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)
- fix z assume "z\<in>ball y e" "\<not> z \<notin> path_component s x"
- hence "y \<in> path_component s x" unfolding not_not mem_path_component_set using `e>0`
+ 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)
+ fix z assume "z\<in>ball y e" "\<not> z \<notin> {y. path_component s x y}"
+ hence "y \<in> {y. path_component s x y}" unfolding not_not mem_Collect_eq using `e>0`
apply- apply(rule path_component_trans,assumption) apply(rule path_component_of_subset[OF e(2)])
apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto
thus False using as by auto qed(insert e(2), auto) qed
@@ -462,11 +460,11 @@
fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
assumes "open s" "connected s" shows "path_connected s"
unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule)
- fix x y assume "x \<in> s" "y \<in> s" show "y \<in> path_component s x" proof(rule ccontr)
- assume "y \<notin> path_component s x" moreover
- have "path_component s x \<inter> s \<noteq> {}" using `x\<in>s` path_component_eq_empty path_component_subset[of s x] by auto
+ fix x y assume "x \<in> s" "y \<in> s" show "y \<in> {y. path_component s x y}" proof(rule ccontr)
+ assume "y \<notin> {y. path_component s x y}" moreover
+ 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
ultimately show False using `y\<in>s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)]
- using assms(2)[unfolded connected_def not_ex, rule_format, of"path_component s x" "s - path_component s x"] by auto
+ 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
qed qed
lemma path_connected_continuous_image:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Aug 12 09:17:24 2011 -0700
@@ -22,8 +22,8 @@
subsection{* General notion of a topology *}
-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)"
-typedef (open) 'a topology = "{L::('a set) set. istopology L}"
+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))"
+typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
morphisms "openin" "topology"
unfolding istopology_def by blast
@@ -31,7 +31,7 @@
using openin[of U] by blast
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
- using topology_inverse[unfolded mem_def Collect_def] .
+ using topology_inverse[unfolded mem_Collect_eq] .
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
@@ -41,7 +41,7 @@
{assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
moreover
{assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
- hence "openin T1 = openin T2" by (metis mem_def set_eqI)
+ hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
hence "topology (openin T1) = topology (openin T2)" by simp
hence "T1 = T2" unfolding openin_inverse .}
ultimately show ?thesis by blast
@@ -58,8 +58,8 @@
shows "openin U {}"
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
- using openin[of U] unfolding istopology_def Collect_def mem_def
- unfolding subset_eq Ball_def mem_def by auto
+ using openin[of U] unfolding istopology_def mem_Collect_eq
+ by fast+
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
unfolding topspace_def by blast
@@ -130,33 +130,38 @@
subsection{* Subspace topology. *}
-definition "subtopology U V = topology {S \<inter> V |S. openin U S}"
-
-lemma istopology_subtopology: "istopology {S \<inter> V |S. openin U S}" (is "istopology ?L")
+term "{f x |x. P x}"
+term "{y. \<exists>x. y = f x \<and> P x}"
+
+definition "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
+
+lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
+ (is "istopology ?L")
proof-
- have "{} \<in> ?L" by blast
- {fix A B assume A: "A \<in> ?L" and B: "B \<in> ?L"
+ have "?L {}" by blast
+ {fix A B assume A: "?L A" and B: "?L B"
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
have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+
- then have "A \<inter> B \<in> ?L" by blast}
+ then have "?L (A \<inter> B)" by blast}
moreover
- {fix K assume K: "K \<subseteq> ?L"
- have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U "
+ {fix K assume K: "K \<subseteq> Collect ?L"
+ have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
apply (rule set_eqI)
apply (simp add: Ball_def image_iff)
- by (metis mem_def)
+ by metis
from K[unfolded th0 subset_image_iff]
- obtain Sk where Sk: "Sk \<subseteq> openin U" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
+ obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto
- moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq mem_def)
- ultimately have "\<Union>K \<in> ?L" by blast}
- ultimately show ?thesis unfolding istopology_def by blast
+ moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq)
+ ultimately have "?L (\<Union>K)" by blast}
+ ultimately show ?thesis
+ unfolding subset_eq mem_Collect_eq istopology_def by blast
qed
lemma openin_subtopology:
"openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))"
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
- by (auto simp add: Collect_def)
+ by auto
lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V"
by (auto simp add: topspace_def openin_subtopology)
@@ -210,7 +215,7 @@
apply (rule cong[where x=S and y=S])
apply (rule topology_inverse[symmetric])
apply (auto simp add: istopology_def)
- by (auto simp add: mem_def subset_eq)
+ done
lemma topspace_euclidean: "topspace euclidean = UNIV"
apply (simp add: topspace_def)
@@ -266,7 +271,7 @@
"a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+
lemma open_ball[intro, simp]: "open (ball x e)"
- unfolding open_dist ball_def Collect_def Ball_def mem_def
+ unfolding open_dist ball_def mem_Collect_eq Ball_def
unfolding dist_commute
apply clarify
apply (rule_tac x="e - dist xa x" in exI)
@@ -492,7 +497,7 @@
unfolding closed_def
apply (subst open_subopen)
apply (simp add: islimpt_def subset_eq)
- by (metis ComplE ComplI insertCI insert_absorb mem_def)
+ by (metis ComplE ComplI)
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
unfolding islimpt_def by auto
@@ -691,14 +696,13 @@
}
ultimately show ?thesis
using hull_unique[of S, of "closure S", of closed]
- unfolding mem_def
by simp
qed
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
unfolding closure_hull
- using hull_eq[of closed, unfolded mem_def, OF closed_Inter, of S]
- by (metis mem_def subset_eq)
+ using hull_eq[of closed, OF closed_Inter, of S]
+ by metis
lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
using closure_eq[of S]
@@ -721,12 +725,12 @@
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
using hull_minimal[of S T closed]
- unfolding closure_hull mem_def
+ unfolding closure_hull
by simp
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"
using hull_unique[of S T closed]
- unfolding closure_hull mem_def
+ unfolding closure_hull
by simp
lemma closure_empty[simp]: "closure {} = {}"
@@ -1623,7 +1627,7 @@
qed
lemma open_contains_cball_eq: "open S ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
- by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball mem_def)
+ by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
apply (simp add: interior_def, safe)