# HG changeset patch
# User huffman
# Date 1244043809 25200
# Node ID 80686a815b59667b16f85e52c727214582cbff22
# Parent  8514775606e09fb193e6a1dce28a111e8d966b4c
instance * :: topological_space

diff -r 8514775606e0 -r 80686a815b59 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Wed Jun 03 08:43:01 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Wed Jun 03 08:43:29 2009 -0700
@@ -39,6 +39,38 @@
 
 end
 
+subsection {* Product is a topological space *}
+
+instantiation
+  "*" :: (topological_space, topological_space) topological_space
+begin
+
+definition open_prod_def:
+  "open S = (\<forall>x\<in>S. \<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S)"
+
+instance proof
+  show "open (UNIV :: ('a \<times> 'b) set)"
+    unfolding open_prod_def by (fast intro: open_UNIV)
+next
+  fix S T :: "('a \<times> 'b) set"
+  assume "open S" "open T" thus "open (S \<inter> T)"
+    unfolding open_prod_def
+    apply clarify
+    apply (drule (1) bspec)+
+    apply (clarify, rename_tac Sa Ta Sb Tb)
+    apply (rule_tac x="Sa \<inter> Ta" in exI)
+    apply (rule_tac x="Sb \<inter> Tb" in exI)
+    apply (simp add: open_Int)
+    apply fast
+    done
+next
+  fix T :: "('a \<times> 'b) set set"
+  assume "\<forall>A\<in>T. open A" thus "open (\<Union>T)"
+    unfolding open_prod_def by fast
+qed
+
+end
+
 subsection {* Product is a metric space *}
 
 instantiation
@@ -67,6 +99,55 @@
     apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
     apply (simp only: real_sum_squared_expand)
     done
+next
+  (* FIXME: long proof! *)
+  (* Maybe it would be easier to define topological spaces *)
+  (* in terms of neighborhoods instead of open sets? *)
+  fix S :: "('a \<times> 'b) set"
+  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+    unfolding open_prod_def open_dist
+    apply safe
+    apply (drule (1) bspec)
+    apply clarify
+    apply (drule (1) bspec)+
+    apply (clarify, rename_tac r s)
+    apply (rule_tac x="min r s" in exI, simp)
+    apply (clarify, rename_tac c d)
+    apply (erule subsetD)
+    apply (simp add: dist_Pair_Pair)
+    apply (rule conjI)
+    apply (drule spec, erule mp)
+    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
+    apply (drule spec, erule mp)
+    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
+
+    apply (drule (1) bspec)
+    apply clarify
+    apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
+    apply clarify
+    apply (rule_tac x="{y. dist y a < r}" in exI)
+    apply (rule_tac x="{y. dist y b < s}" in exI)
+    apply (rule conjI)
+    apply clarify
+    apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
+    apply clarify
+    apply (rule le_less_trans [OF dist_triangle])
+    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (rule conjI)
+    apply clarify
+    apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
+    apply clarify
+    apply (rule le_less_trans [OF dist_triangle])
+    apply (erule less_le_trans [OF add_strict_right_mono], simp)
+    apply (rule conjI)
+    apply simp
+    apply (clarify, rename_tac c d)
+    apply (drule spec, erule mp)
+    apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono)
+    apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
+    apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
+    apply (simp add: power_divide)
+    done
 qed
 
 end