# HG changeset patch
# User huffman
# Date 1273032244 25200
# Node ID 1342e3aeceeb8d59c0f83e5f4929a78adc308153
# Parent  16b0a722083afa7490d798f588fab5ff63b0bd7c# Parent  6302f9ad7047d0633aeb88cee5c178987d3c3769
merged

diff -r 6302f9ad7047 -r 1342e3aeceeb src/HOL/Lim.thy
--- 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`
diff -r 6302f9ad7047 -r 1342e3aeceeb src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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
diff -r 6302f9ad7047 -r 1342e3aeceeb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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"
diff -r 6302f9ad7047 -r 1342e3aeceeb src/HOL/Probability/Measure.thy
--- 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