# HG changeset patch
# User huffman
# Date 1313443757 25200
# Node ID 1e0414bda9af3cb4b6f4a55de4016b8a7245df4d
# Parent  6fb54701a11bc5512304340cf88e7865b59426f5
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space

diff -r 6fb54701a11b -r 1e0414bda9af src/HOL/Library/Product_Vector.thy
--- 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