--- a/src/HOL/Lim.thy Wed May 05 00:59:59 2010 +0200
+++ b/src/HOL/Lim.thy Tue May 04 21:04:04 2010 -0700
@@ -381,7 +381,7 @@
lemmas LIM_of_real = of_real.LIM
lemma LIM_power:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
assumes f: "f -- a --> l"
shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
by (induct n, simp, simp add: LIM_mult f)
@@ -399,7 +399,7 @@
by (rule LIM_inverse [OF LIM_ident a])
lemma LIM_sgn:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
unfolding sgn_div_norm
by (simp add: LIM_scaleR LIM_inverse LIM_norm)
@@ -408,12 +408,12 @@
subsection {* Continuity *}
lemma LIM_isCont_iff:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
lemma isCont_iff:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
by (simp add: isCont_def LIM_isCont_iff)
@@ -424,7 +424,7 @@
unfolding isCont_def by (rule LIM_const)
lemma isCont_norm:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
unfolding isCont_def by (rule LIM_norm)
@@ -432,27 +432,27 @@
unfolding isCont_def by (rule LIM_rabs)
lemma isCont_add:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
unfolding isCont_def by (rule LIM_add)
lemma isCont_minus:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
unfolding isCont_def by (rule LIM_minus)
lemma isCont_diff:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
unfolding isCont_def by (rule LIM_diff)
lemma isCont_mult:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra"
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
unfolding isCont_def by (rule LIM_mult)
lemma isCont_inverse:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
unfolding isCont_def by (rule LIM_inverse)
@@ -495,12 +495,12 @@
unfolding isCont_def by (rule LIM_of_real)
lemma isCont_power:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
lemma isCont_sgn:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
unfolding isCont_def by (rule LIM_sgn)
@@ -508,7 +508,7 @@
by (rule isCont_rabs [OF isCont_ident])
lemma isCont_setsum:
- fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
+ fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
fixes A :: "'a set" assumes "finite A"
shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
using `finite A`
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed May 05 00:59:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue May 04 21:04:04 2010 -0700
@@ -1632,9 +1632,7 @@
then show ?thesis by blast
qed
-(* ------------------------------------------------------------------------- *)
-(* Geometric progression. *)
-(* ------------------------------------------------------------------------- *)
+subsection {* Geometric progression *}
lemma sum_gp_basic: "((1::'a::{field}) - x) * setsum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
(is "?lhs = ?rhs")
@@ -1703,7 +1701,7 @@
definition "dependent S \<longleftrightarrow> (\<exists>a \<in> S. a \<in> span(S - {a}))"
abbreviation "independent s == ~(dependent s)"
-(* Closure properties of subspaces. *)
+text {* Closure properties of subspaces. *}
lemma subspace_UNIV[simp]: "subspace(UNIV)" by (simp add: subspace_def)
@@ -1876,7 +1874,7 @@
shows "h x"
using span_induct_alt'[of h S] h0 hS x by blast
-(* Individual closure properties. *)
+text {* Individual closure properties. *}
lemma span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
@@ -1902,7 +1900,7 @@
apply (subgoal_tac "(x + y) - x \<in> span S", simp)
by (simp only: span_add span_sub)
-(* Mapping under linear image. *)
+text {* Mapping under linear image. *}
lemma span_linear_image: assumes lf: "linear f"
shows "span (f ` S) = f ` (span S)"
@@ -1934,7 +1932,7 @@
ultimately show ?thesis by blast
qed
-(* The key breakdown property. *)
+text {* The key breakdown property. *}
lemma span_breakdown:
assumes bS: "b \<in> S" and aS: "a \<in> span S"
@@ -2007,7 +2005,7 @@
ultimately show ?thesis by blast
qed
-(* Hence some "reversal" results.*)
+text {* Hence some "reversal" results. *}
lemma in_span_insert:
assumes a: "a \<in> span (insert b S)" and na: "a \<notin> span S"
@@ -2060,7 +2058,7 @@
apply (rule na)
done
-(* Transitivity property. *)
+text {* Transitivity property. *}
lemma span_trans:
assumes x: "x \<in> span S" and y: "y \<in> span (insert x S)"
@@ -2080,9 +2078,7 @@
by (rule x)
qed
-(* ------------------------------------------------------------------------- *)
-(* An explicit expansion is sometimes needed. *)
-(* ------------------------------------------------------------------------- *)
+text {* An explicit expansion is sometimes needed. *}
lemma span_explicit:
"span P = {y. \<exists>S u. finite S \<and> S \<subseteq> P \<and> setsum (\<lambda>v. u v *\<^sub>R v) S = y}"
@@ -2215,7 +2211,7 @@
qed
-(* Standard bases are a spanning set, and obviously finite. *)
+text {* Standard bases are a spanning set, and obviously finite. *}
lemma span_stdbasis:"span {basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
apply (rule set_ext)
@@ -2280,7 +2276,7 @@
then show ?thesis unfolding eq dependent_def ..
qed
-(* This is useful for building a basis step-by-step. *)
+text {* This is useful for building a basis step-by-step. *}
lemma independent_insert:
"independent(insert a S) \<longleftrightarrow>
@@ -2320,7 +2316,7 @@
ultimately show ?thesis by blast
qed
-(* The degenerate case of the Exchange Lemma. *)
+text {* The degenerate case of the Exchange Lemma. *}
lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
by blast
@@ -2356,7 +2352,7 @@
then show "A \<subseteq> B" by blast
qed
-(* The general case of the Exchange Lemma, the key to what follows. *)
+text {* The general case of the Exchange Lemma, the key to what follows. *}
lemma exchange_lemma:
assumes f:"finite t" and i: "independent s"
@@ -2432,7 +2428,7 @@
show ?ths by blast
qed
-(* This implies corresponding size bounds. *)
+text {* This implies corresponding size bounds. *}
lemma independent_span_bound:
assumes f: "finite t" and i: "independent s" and sp:"s \<subseteq> span t"
@@ -2464,7 +2460,7 @@
lemma dependent_biggerset: "(finite (S::(real ^'n) set) ==> card S > CARD('n)) ==> dependent S"
by (metis independent_bound not_less)
-(* Hence we can create a maximal independent subset. *)
+text {* Hence we can create a maximal independent subset. *}
lemma maximal_independent_subset_extend:
assumes sv: "(S::(real^'n) set) \<subseteq> V" and iS: "independent S"
@@ -2501,7 +2497,7 @@
"\<exists>(B:: (real ^'n) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty)
-(* Notion of dimension. *)
+text {* Notion of dimension. *}
definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n))"
@@ -2510,7 +2506,7 @@
using maximal_independent_subset[of V] independent_bound
by auto
-(* Consequences of independence or spanning for cardinality. *)
+text {* Consequences of independence or spanning for cardinality. *}
lemma independent_card_le_dim:
assumes "(B::(real ^'n) set) \<subseteq> V" and "independent B" shows "card B \<le> dim V"
@@ -2531,7 +2527,7 @@
lemma dim_unique: "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
by (metis basis_card_eq_dim)
-(* More lemmas about dimension. *)
+text {* More lemmas about dimension. *}
lemma dim_univ: "dim (UNIV :: (real^'n) set) = CARD('n)"
apply (rule dim_unique[of "{basis i |i. i\<in> (UNIV :: 'n set)}"])
@@ -2545,7 +2541,7 @@
lemma dim_subset_univ: "dim (S:: (real^'n) set) \<le> CARD('n)"
by (metis dim_subset subset_UNIV dim_univ)
-(* Converses to those. *)
+text {* Converses to those. *}
lemma card_ge_dim_independent:
assumes BV:"(B::(real ^'n) set) \<subseteq> V" and iB:"independent B" and dVB:"dim V \<le> card B"
@@ -2587,9 +2583,7 @@
by (metis order_eq_iff card_le_dim_spanning
card_ge_dim_independent)
-(* ------------------------------------------------------------------------- *)
-(* More general size bound lemmas. *)
-(* ------------------------------------------------------------------------- *)
+text {* More general size bound lemmas. *}
lemma independent_bound_general:
"independent (S:: (real^'n) set) \<Longrightarrow> finite S \<and> card S \<le> dim S"
@@ -2637,7 +2631,7 @@
finally show ?thesis .
qed
-(* Relation between bases and injectivity/surjectivity of map. *)
+text {* Relation between bases and injectivity/surjectivity of map. *}
lemma spanning_surjective_image:
assumes us: "UNIV \<subseteq> span S"
@@ -2663,9 +2657,8 @@
then show ?thesis unfolding dependent_def by blast
qed
-(* ------------------------------------------------------------------------- *)
-(* Picking an orthogonal replacement for a spanning set. *)
-(* ------------------------------------------------------------------------- *)
+text {* Picking an orthogonal replacement for a spanning set. *}
+
(* FIXME : Move to some general theory ?*)
definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
@@ -2771,9 +2764,7 @@
using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
by(auto simp add: span_span)
-(* ------------------------------------------------------------------------- *)
-(* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *)
-(* ------------------------------------------------------------------------- *)
+text {* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *}
lemma span_not_univ_orthogonal:
assumes sU: "span S \<noteq> UNIV"
@@ -2832,7 +2823,7 @@
from span_not_univ_subset_hyperplane[OF th] show ?thesis .
qed
-(* We can extend a linear basis-basis injection to the whole set. *)
+text {* We can extend a linear basis-basis injection to the whole set. *}
lemma linear_indep_image_lemma:
assumes lf: "linear f" and fB: "finite B"
@@ -2885,7 +2876,7 @@
show "x = 0" .
qed
-(* We can extend a linear mapping from basis. *)
+text {* We can extend a linear mapping from basis. *}
lemma linear_independent_extend_lemma:
fixes f :: "'a::real_vector \<Rightarrow> 'b::real_vector"
@@ -2988,7 +2979,7 @@
apply clarsimp by blast
qed
-(* Can construct an isomorphism between spaces of same dimension. *)
+text {* Can construct an isomorphism between spaces of same dimension. *}
lemma card_le_inj: assumes fA: "finite A" and fB: "finite B"
and c: "card A \<le> card B" shows "(\<exists>f. f ` A \<subseteq> B \<and> inj_on f A)"
@@ -3066,7 +3057,7 @@
from g(1) gS giS show ?thesis by blast
qed
-(* linear functions are equal on a subspace if they are on a spanning set. *)
+text {* Linear functions are equal on a subspace if they are on a spanning set. *}
lemma subspace_kernel:
assumes lf: "linear f"
@@ -3115,7 +3106,7 @@
then show ?thesis by (auto intro: ext)
qed
-(* Similar results for bilinear functions. *)
+text {* Similar results for bilinear functions. *}
lemma bilinear_eq:
assumes bf: "bilinear f"
@@ -3155,7 +3146,7 @@
from bilinear_eq[OF bf bg equalityD2[OF span_stdbasis] equalityD2[OF span_stdbasis] th] show ?thesis by (blast intro: ext)
qed
-(* Detailed theorems about left and right invertibility in general case. *)
+text {* Detailed theorems about left and right invertibility in general case. *}
lemma left_invertible_transpose:
"(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
@@ -3351,7 +3342,7 @@
unfolding matrix_right_invertible_span_columns
..
-(* An injective map real^'n->real^'n is also surjective. *)
+text {* An injective map @{typ "real^'n \<Rightarrow> real^'n"} is also surjective. *}
lemma linear_injective_imp_surjective:
assumes lf: "linear (f:: real ^'n \<Rightarrow> real ^'n)" and fi: "inj f"
@@ -3377,7 +3368,7 @@
using B(3) by blast
qed
-(* And vice versa. *)
+text {* And vice versa. *}
lemma surjective_iff_injective_gen:
assumes fS: "finite S" and fT: "finite T" and c: "card S = card T"
@@ -3459,7 +3450,7 @@
using B(3) by blast
qed
-(* Hence either is enough for isomorphism. *)
+text {* Hence either is enough for isomorphism. *}
lemma left_right_inverse_eq:
assumes fg: "f o g = id" and gh: "g o h = id"
@@ -3488,7 +3479,7 @@
using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]
by (metis left_right_inverse_eq)
-(* Left and right inverses are the same for R^N->R^N. *)
+text {* Left and right inverses are the same for @{typ "real^'n \<Rightarrow> real^'n"}. *}
lemma linear_inverse_left:
assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and lf': "linear f'"
@@ -3506,7 +3497,7 @@
then show ?thesis using lf lf' by metis
qed
-(* Moreover, a one-sided inverse is automatically linear. *)
+text {* Moreover, a one-sided inverse is automatically linear. *}
lemma left_inverse_linear:
assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and gf: "g o f = id"
@@ -3538,7 +3529,7 @@
with h(1) show ?thesis by blast
qed
-(* The same result in terms of square matrices. *)
+text {* The same result in terms of square matrices. *}
lemma matrix_left_right_inverse:
fixes A A' :: "real ^'n^'n"
@@ -3562,7 +3553,7 @@
then show ?thesis by blast
qed
-(* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *)
+text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *}
definition "rowvector v = (\<chi> i j. (v$j))"
@@ -3589,7 +3580,7 @@
unfolding dot_matrix_product transpose_columnvector[symmetric]
dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
-(* Infinity norm. *)
+subsection {* Infinity norm *}
definition "infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
@@ -3721,7 +3712,7 @@
lemma infnorm_pos_lt: "infnorm x > 0 \<longleftrightarrow> x \<noteq> 0"
using infnorm_pos_le[of x] infnorm_eq_0[of x] by arith
-(* Prove that it differs only up to a bound from Euclidean norm. *)
+text {* Prove that it differs only up to a bound from Euclidean norm. *}
lemma infnorm_le_norm: "infnorm x \<le> norm x"
unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
@@ -3750,7 +3741,7 @@
show ?thesis unfolding norm_eq_sqrt_inner id_def .
qed
-(* Equality in Cauchy-Schwarz and triangle inequalities. *)
+text {* Equality in Cauchy-Schwarz and triangle inequalities. *}
lemma norm_cauchy_schwarz_eq: "x \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -3817,7 +3808,7 @@
ultimately show ?thesis by blast
qed
-(* Collinearity.*)
+subsection {* Collinearity *}
definition
collinear :: "'a::real_vector set \<Rightarrow> bool" where
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed May 05 00:59:59 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue May 04 21:04:04 2010 -0700
@@ -416,30 +416,52 @@
subsection{* Hausdorff and other separation properties *}
-class t0_space =
+class t0_space = topological_space +
assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
-class t1_space =
- assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V"
-begin
-
-subclass t0_space
-proof
-qed (fast dest: t1_space)
-
-end
+class t1_space = topological_space +
+ assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
+
+instance t1_space \<subseteq> t0_space
+proof qed (fast dest: t1_space)
+
+lemma separation_t1:
+ fixes x y :: "'a::t1_space"
+ shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
+ using t1_space[of x y] by blast
+
+lemma closed_sing:
+ fixes a :: "'a::t1_space"
+ shows "closed {a}"
+proof -
+ let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
+ have "open ?T" by (simp add: open_Union)
+ also have "?T = - {a}"
+ by (simp add: expand_set_eq separation_t1, auto)
+ finally show "closed {a}" unfolding closed_def .
+qed
+
+lemma closed_insert [simp]:
+ fixes a :: "'a::t1_space"
+ assumes "closed S" shows "closed (insert a S)"
+proof -
+ from closed_sing assms
+ have "closed ({a} \<union> S)" by (rule closed_Un)
+ thus "closed (insert a S)" by simp
+qed
+
+lemma finite_imp_closed:
+ fixes S :: "'a::t1_space set"
+ shows "finite S \<Longrightarrow> closed S"
+by (induct set: finite, simp_all)
text {* T2 spaces are also known as Hausdorff spaces. *}
-class t2_space =
+class t2_space = topological_space +
assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
-begin
-
-subclass t1_space
-proof
-qed (fast dest: hausdorff)
-
-end
+
+instance t2_space \<subseteq> t1_space
+proof qed (fast dest: hausdorff)
instance metric_space \<subseteq> t2_space
proof
@@ -461,11 +483,6 @@
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
using hausdorff[of x y] by blast
-lemma separation_t1:
- fixes x y :: "'a::t1_space"
- shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)"
- using t1_space[of x y] by blast
-
lemma separation_t0:
fixes x y :: "'a::t0_space"
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
@@ -1200,7 +1217,7 @@
text{* Another limit point characterization. *}
lemma islimpt_sequential:
- fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
+ fixes x :: "'a::metric_space"
shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
(is "?lhs = ?rhs")
proof
@@ -1537,51 +1554,50 @@
qed
lemma Lim_transform_eventually:
- "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+ "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
apply (rule topological_tendstoI)
apply (drule (2) topological_tendstoD)
apply (erule (1) eventually_elim2, simp)
done
lemma Lim_transform_within:
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
- "(f ---> l) (at x within S)"
- shows "(g ---> l) (at x within S)"
- using assms(1,3) unfolding Lim_within
- apply -
- apply (clarify, rename_tac e)
- apply (drule_tac x=e in spec, clarsimp, rename_tac r)
- apply (rule_tac x="min d r" in exI, clarsimp, rename_tac y)
- apply (drule_tac x=y in bspec, assumption, clarsimp)
- apply (simp add: assms(2))
- done
+ assumes "0 < d" and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+ and "(f ---> l) (at x within S)"
+ shows "(g ---> l) (at x within S)"
+proof (rule Lim_transform_eventually)
+ show "eventually (\<lambda>x. f x = g x) (at x within S)"
+ unfolding eventually_within
+ using assms(1,2) by auto
+ show "(f ---> l) (at x within S)" by fact
+qed
lemma Lim_transform_at:
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
- (f ---> l) (at x) ==> (g ---> l) (at x)"
- apply (subst within_UNIV[symmetric])
- using Lim_transform_within[of d UNIV x f g l]
- by (auto simp add: within_UNIV)
+ assumes "0 < d" and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+ and "(f ---> l) (at x)"
+ shows "(g ---> l) (at x)"
+proof (rule Lim_transform_eventually)
+ show "eventually (\<lambda>x. f x = g x) (at x)"
+ unfolding eventually_at
+ using assms(1,2) by auto
+ show "(f ---> l) (at x)" by fact
+qed
text{* Common case assuming being away from some crucial point like 0. *}
lemma Lim_transform_away_within:
- fixes a b :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
+ fixes a b :: "'a::t1_space"
+ assumes "a \<noteq> b" and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and "(f ---> l) (at a within S)"
shows "(g ---> l) (at a within S)"
-proof-
- have "\<forall>x'\<in>S. 0 < dist x' a \<and> dist x' a < dist a b \<longrightarrow> f x' = g x'" using assms(2)
- apply auto apply(erule_tac x=x' in ballE) by (auto simp add: dist_commute)
- thus ?thesis using Lim_transform_within[of "dist a b" S a f g l] using assms(1,3) unfolding dist_nz by auto
+proof (rule Lim_transform_eventually)
+ show "(f ---> l) (at a within S)" by fact
+ show "eventually (\<lambda>x. f x = g x) (at a within S)"
+ unfolding Limits.eventually_within eventually_at_topological
+ by (rule exI [where x="- {b}"], simp add: open_Compl assms)
qed
lemma Lim_transform_away_at:
- fixes a b :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
+ fixes a b :: "'a::t1_space"
assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
and fl: "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
@@ -1591,15 +1607,14 @@
text{* Alternatively, within an open set. *}
lemma Lim_transform_within_open:
- fixes a :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- assumes "open S" "a \<in> S" "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x" "(f ---> l) (at a)"
+ assumes "open S" and "a \<in> S" and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
+ and "(f ---> l) (at a)"
shows "(g ---> l) (at a)"
-proof-
- from assms(1,2) obtain e::real where "e>0" and e:"ball a e \<subseteq> S" unfolding open_contains_ball by auto
- hence "\<forall>x'. 0 < dist x' a \<and> dist x' a < e \<longrightarrow> f x' = g x'" using assms(3)
- unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_commute)
- thus ?thesis using Lim_transform_at[of e a f g l] `e>0` assms(4) by auto
+proof (rule Lim_transform_eventually)
+ show "eventually (\<lambda>x. f x = g x) (at a)"
+ unfolding eventually_at_topological
+ using assms(1,2,3) by auto
+ show "(f ---> l) (at a)" by fact
qed
text{* A congruence rule allowing us to transform limits assuming not at point. *}
@@ -1607,21 +1622,21 @@
(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
lemma Lim_cong_within(*[cong add]*):
- fixes a :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
- by (simp add: Lim_within dist_nz[symmetric])
-
-lemma Lim_cong_at[cong add]:
- fixes a :: "'a::metric_space"
- fixes l :: "'b::metric_space" (* TODO: generalize *)
- shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
- by (simp add: Lim_at dist_nz[symmetric])
+ assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+ shows "((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
+ unfolding tendsto_def Limits.eventually_within eventually_at_topological
+ using assms by simp
+
+lemma Lim_cong_at(*[cong add]*):
+ assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
+ shows "((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a))"
+ unfolding tendsto_def eventually_at_topological
+ using assms by simp
text{* Useful lemmas on closure and set of possible sequential limits.*}
lemma closure_sequential:
- fixes l :: "'a::metric_space" (* TODO: generalize *)
+ fixes l :: "'a::metric_space"
shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
proof
assume "?lhs" moreover
@@ -2910,26 +2925,6 @@
by auto
qed
-lemma closed_sing [simp]:
- fixes a :: "'a::metric_space"
- shows "closed {a}"
- apply (clarsimp simp add: closed_def open_dist)
- apply (rule ccontr)
- apply (drule_tac x="dist x a" in spec)
- apply (simp add: dist_nz dist_commute)
- done
-
-lemma finite_imp_closed:
- fixes s :: "'a::metric_space set"
- shows "finite s ==> closed s"
-proof (induct set: finite)
- case empty show "closed {}" by simp
-next
- case (insert x F)
- hence "closed ({x} \<union> F)" by (simp only: closed_Un closed_sing)
- thus "closed (insert x F)" by simp
-qed
-
lemma finite_imp_compact:
fixes s :: "'a::heine_borel set"
shows "finite s ==> compact s"
@@ -2967,10 +2962,9 @@
by blast
lemma open_delete:
- fixes s :: "'a::metric_space set"
- shows "open s ==> open(s - {x})"
- using open_Diff[of s "{x}"] closed_sing
- by blast
+ fixes s :: "'a::t1_space set"
+ shows "open s \<Longrightarrow> open (s - {x})"
+ by (simp add: open_Diff)
text{* Finite intersection property. I could make it an equivalence in fact. *}
@@ -3252,7 +3246,7 @@
by (rule Lim_trivial_limit)
next
case False
- hence "netlimit (at x) = x"
+ hence 1: "netlimit (at x) = x"
using netlimit_within [of x UNIV]
by (simp add: within_UNIV)
with * show ?thesis by simp
@@ -3411,38 +3405,28 @@
text{* The usual transformation theorems. *}
lemma continuous_transform_within:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
"continuous (at x within s) f"
shows "continuous (at x within s) g"
-proof-
- { fix e::real assume "e>0"
- then obtain d' where d':"d'>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(4) unfolding continuous_within Lim_within by auto
- { fix x' assume "x'\<in>s" "0 < dist x' x" "dist x' x < (min d d')"
- hence "dist (f x') (g x) < e" using assms(2,3) apply(erule_tac x=x in ballE) using d' by auto }
- hence "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
- hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto }
- hence "(f ---> g x) (at x within s)" unfolding Lim_within using assms(1) by auto
- thus ?thesis unfolding continuous_within using Lim_transform_within[of d s x f g "g x"] using assms by blast
+unfolding continuous_within
+proof (rule Lim_transform_within)
+ show "0 < d" by fact
+ show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
+ using assms(3) by auto
+ have "f x = g x"
+ using assms(1,2,3) by auto
+ thus "(f ---> g x) (at x within s)"
+ using assms(4) unfolding continuous_within by simp
qed
lemma continuous_transform_at:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
"continuous (at x) f"
shows "continuous (at x) g"
-proof-
- { fix e::real assume "e>0"
- then obtain d' where d':"d'>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(3) unfolding continuous_at Lim_at by auto
- { fix x' assume "0 < dist x' x" "dist x' x < (min d d')"
- hence "dist (f x') (g x) < e" using assms(2) apply(erule_tac x=x in allE) using d' by auto
- }
- hence "\<forall>xa. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
- hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto
- }
- hence "(f ---> g x) (at x)" unfolding Lim_at using assms(1) by auto
- thus ?thesis unfolding continuous_at using Lim_transform_at[of d x f g "g x"] using assms by blast
-qed
+ using continuous_transform_within [of d x UNIV f g] assms
+ by (simp add: within_UNIV)
text{* Combination results for pointwise continuity. *}
@@ -3752,17 +3736,17 @@
text{* Equality of continuous functions on closure and related results. *}
lemma continuous_closed_in_preimage_constant:
- fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
- using continuous_closed_in_preimage[of s f "{a}"] closed_sing by auto
+ using continuous_closed_in_preimage[of s f "{a}"] by auto
lemma continuous_closed_preimage_constant:
- fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
- using continuous_closed_preimage[of s f "{a}"] closed_sing by auto
+ using continuous_closed_preimage[of s f "{a}"] by auto
lemma continuous_constant_on_closure:
- fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
assumes "continuous_on (closure s) f"
"\<forall>x \<in> s. f x = a"
shows "\<forall>x \<in> (closure s). f x = a"
@@ -3828,14 +3812,14 @@
text{* Proving a function is constant by proving open-ness of level set. *}
lemma continuous_levelset_open_in_cases:
- fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a}
==> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
unfolding connected_clopen using continuous_closed_in_preimage_constant by auto
lemma continuous_levelset_open_in:
- fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
(\<exists>x \<in> s. f x = a) ==> (\<forall>x \<in> s. f x = a)"
@@ -3843,7 +3827,7 @@
by meson
lemma continuous_levelset_open:
- fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
+ fixes f :: "_ \<Rightarrow> 'b::t1_space"
assumes "connected s" "continuous_on s f" "open {x \<in> s. f x = a}" "\<exists>x \<in> s. f x = a"
shows "\<forall>x \<in> s. f x = a"
using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
@@ -4454,7 +4438,7 @@
show ?thesis
proof(cases "c=0")
have *:"(\<lambda>x. 0) ` s = {0}" using `s\<noteq>{}` by auto
- case True thus ?thesis apply auto unfolding * using closed_sing by auto
+ case True thus ?thesis apply auto unfolding * by auto
next
case False
{ fix x l assume as:"\<forall>n::nat. x n \<in> scaleR c ` s" "(x ---> l) sequentially"
--- a/src/HOL/Probability/Measure.thy Wed May 05 00:59:59 2010 +0200
+++ b/src/HOL/Probability/Measure.thy Tue May 04 21:04:04 2010 -0700
@@ -463,7 +463,7 @@
have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)"
by (rule measure_countable_increasing)
(auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits)
- also have "... = measure M (\<Union>i. A i)"
+ also have "measure M (\<Union>i. nat_case {} A i) = measure M (\<Union>i. A i)"
by (simp add: ueq)
finally have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. A i)" .
thus ?thesis using meq
@@ -652,7 +652,7 @@
show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
using ASuc by auto
qed
- also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+ also have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
by (simp add: vimage_UN)
finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
moreover