author huffman Mon Aug 15 14:29:17 2011 -0700 (2011-08-15) changeset 44214 1e0414bda9af parent 44213 6fb54701a11b child 44215 786876687ef8
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
```     1.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Aug 15 14:09:39 2011 -0700
1.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Aug 15 14:29:17 2011 -0700
1.3 @@ -154,13 +154,62 @@
1.4    then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
1.5  qed
1.6
1.7 +text {* Product preserves separation axioms. *}
1.8 +
1.9 +lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
1.10 +  by (induct x) simp (* TODO: move elsewhere *)
1.11 +
1.12 +instance prod :: (t0_space, t0_space) t0_space
1.13 +proof
1.14 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
1.15 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
1.16 +    by (simp add: prod_eq_iff)
1.17 +  thus "\<exists>U. open U \<and> (x \<in> U) \<noteq> (y \<in> U)"
1.18 +    apply (rule disjE)
1.19 +    apply (drule t0_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
1.20 +    apply (simp add: open_Times mem_Times_iff)
1.21 +    apply (drule t0_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
1.22 +    apply (simp add: open_Times mem_Times_iff)
1.23 +    done
1.24 +qed
1.25 +
1.26 +instance prod :: (t1_space, t1_space) t1_space
1.27 +proof
1.28 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
1.29 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
1.30 +    by (simp add: prod_eq_iff)
1.31 +  thus "\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
1.32 +    apply (rule disjE)
1.33 +    apply (drule t1_space, erule exE, rule_tac x="U \<times> UNIV" in exI)
1.34 +    apply (simp add: open_Times mem_Times_iff)
1.35 +    apply (drule t1_space, erule exE, rule_tac x="UNIV \<times> U" in exI)
1.36 +    apply (simp add: open_Times mem_Times_iff)
1.37 +    done
1.38 +qed
1.39 +
1.40 +instance prod :: (t2_space, t2_space) t2_space
1.41 +proof
1.42 +  fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
1.43 +  hence "fst x \<noteq> fst y \<or> snd x \<noteq> snd y"
1.44 +    by (simp add: prod_eq_iff)
1.45 +  thus "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
1.46 +    apply (rule disjE)
1.47 +    apply (drule hausdorff, clarify)
1.48 +    apply (rule_tac x="U \<times> UNIV" in exI, rule_tac x="V \<times> UNIV" in exI)
1.49 +    apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
1.50 +    apply (drule hausdorff, clarify)
1.51 +    apply (rule_tac x="UNIV \<times> U" in exI, rule_tac x="UNIV \<times> V" in exI)
1.52 +    apply (simp add: open_Times mem_Times_iff disjoint_iff_not_equal)
1.53 +    done
1.54 +qed
1.55 +
1.56  subsection {* Product is a metric space *}
1.57
1.58  instantiation prod :: (metric_space, metric_space) metric_space
1.59  begin
1.60
1.61  definition dist_prod_def:
1.62 -  "dist (x::'a \<times> 'b) y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)"
1.63 +  "dist x y = sqrt ((dist (fst x) (fst y))\<twosuperior> + (dist (snd x) (snd y))\<twosuperior>)"
1.64
1.65  lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<twosuperior> + (dist b d)\<twosuperior>)"
1.66    unfolding dist_prod_def by simp
```