--- a/src/HOL/Library/Product_Vector.thy Mon Aug 15 14:09:39 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy Mon Aug 15 14:29:17 2011 -0700
@@ -154,13 +154,62 @@
then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
qed
+text {* Product preserves separation axioms. *}
+
+lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
+ by (induct x) simp (* TODO: move elsewhere *)
+
+instance prod :: (t0_space, t0_space) t0_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
+ apply (rule disjE)
+ apply (drule t0_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
+ apply (simp add: open_Times mem_Times_iff)
+ apply (drule t0_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
+ apply (simp add: open_Times mem_Times_iff)
+ done
+qed
+
+instance prod :: (t1_space, t1_space) t1_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
+ apply (rule disjE)
+ apply (drule t1_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
+ apply (simp add: open_Times mem_Times_iff)
+ apply (drule t1_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
+ apply (simp add: open_Times mem_Times_iff)
+ done
+qed
+
+instance prod :: (t2_space, t2_space) t2_space
+proof
+ fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
+ hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
+ by (simp add: prod_eq_iff)
+ thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
+ apply (rule disjE)
+ apply (drule hausdorff, clarify)
+ apply (rule_tac x="U \<times> UNIV" in exI, rule_tac x="V \<times> UNIV" in exI)
+ apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
+ apply (drule hausdorff, clarify)
+ apply (rule_tac x="UNIV \<times> U" in exI, rule_tac x="UNIV \<times> V" in exI)
+ apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
+ done
+qed
+
subsection {* Product is a metric space *}
instantiation prod :: (metric_space, metric_space) metric_space
begin
definition dist_prod_def:
- "dist (x::'a \<times> 'b) y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)"
+ "dist x y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)"
lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<twosuperior> + (dist b d)\<twosuperior>)"
unfolding dist_prod_def by simp