src/HOL/Library/Product_Vector.thy
changeset 44214 1e0414bda9af
parent 44127 7b57b9295d98
child 44233 aa74ce315bae
     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