instance * :: topological_space
authorhuffman
Wed Jun 03 08:43:29 2009 -0700 (2009-06-03)
changeset 3141580686a815b59
parent 31414 8514775606e0
child 31416 f4c079225845
instance * :: topological_space
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Wed Jun 03 08:43:01 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Wed Jun 03 08:43:29 2009 -0700
     1.3 @@ -39,6 +39,38 @@
     1.4  
     1.5  end
     1.6  
     1.7 +subsection {* Product is a topological space *}
     1.8 +
     1.9 +instantiation
    1.10 +  "*" :: (topological_space, topological_space) topological_space
    1.11 +begin
    1.12 +
    1.13 +definition open_prod_def:
    1.14 +  "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)"
    1.15 +
    1.16 +instance proof
    1.17 +  show "open (UNIV :: ('a \<times> 'b) set)"
    1.18 +    unfolding open_prod_def by (fast intro: open_UNIV)
    1.19 +next
    1.20 +  fix S T :: "('a \<times> 'b) set"
    1.21 +  assume "open S" "open T" thus "open (S \<inter> T)"
    1.22 +    unfolding open_prod_def
    1.23 +    apply clarify
    1.24 +    apply (drule (1) bspec)+
    1.25 +    apply (clarify, rename_tac Sa Ta Sb Tb)
    1.26 +    apply (rule_tac x="Sa \<inter> Ta" in exI)
    1.27 +    apply (rule_tac x="Sb \<inter> Tb" in exI)
    1.28 +    apply (simp add: open_Int)
    1.29 +    apply fast
    1.30 +    done
    1.31 +next
    1.32 +  fix T :: "('a \<times> 'b) set set"
    1.33 +  assume "\<forall>A\<in>T. open A" thus "open (\<Union>T)"
    1.34 +    unfolding open_prod_def by fast
    1.35 +qed
    1.36 +
    1.37 +end
    1.38 +
    1.39  subsection {* Product is a metric space *}
    1.40  
    1.41  instantiation
    1.42 @@ -67,6 +99,55 @@
    1.43      apply (rule power_mono [OF dist_triangle2 [of _ _ "snd z"] zero_le_dist])
    1.44      apply (simp only: real_sum_squared_expand)
    1.45      done
    1.46 +next
    1.47 +  (* FIXME: long proof! *)
    1.48 +  (* Maybe it would be easier to define topological spaces *)
    1.49 +  (* in terms of neighborhoods instead of open sets? *)
    1.50 +  fix S :: "('a \<times> 'b) set"
    1.51 +  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.52 +    unfolding open_prod_def open_dist
    1.53 +    apply safe
    1.54 +    apply (drule (1) bspec)
    1.55 +    apply clarify
    1.56 +    apply (drule (1) bspec)+
    1.57 +    apply (clarify, rename_tac r s)
    1.58 +    apply (rule_tac x="min r s" in exI, simp)
    1.59 +    apply (clarify, rename_tac c d)
    1.60 +    apply (erule subsetD)
    1.61 +    apply (simp add: dist_Pair_Pair)
    1.62 +    apply (rule conjI)
    1.63 +    apply (drule spec, erule mp)
    1.64 +    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge1])
    1.65 +    apply (drule spec, erule mp)
    1.66 +    apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
    1.67 +
    1.68 +    apply (drule (1) bspec)
    1.69 +    apply clarify
    1.70 +    apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
    1.71 +    apply clarify
    1.72 +    apply (rule_tac x="{y. dist y a < r}" in exI)
    1.73 +    apply (rule_tac x="{y. dist y b < s}" in exI)
    1.74 +    apply (rule conjI)
    1.75 +    apply clarify
    1.76 +    apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
    1.77 +    apply clarify
    1.78 +    apply (rule le_less_trans [OF dist_triangle])
    1.79 +    apply (erule less_le_trans [OF add_strict_right_mono], simp)
    1.80 +    apply (rule conjI)
    1.81 +    apply clarify
    1.82 +    apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
    1.83 +    apply clarify
    1.84 +    apply (rule le_less_trans [OF dist_triangle])
    1.85 +    apply (erule less_le_trans [OF add_strict_right_mono], simp)
    1.86 +    apply (rule conjI)
    1.87 +    apply simp
    1.88 +    apply (clarify, rename_tac c d)
    1.89 +    apply (drule spec, erule mp)
    1.90 +    apply (simp add: dist_Pair_Pair add_strict_mono power_strict_mono)
    1.91 +    apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
    1.92 +    apply (rule_tac x="e / sqrt 2" in exI, simp add: divide_pos_pos)
    1.93 +    apply (simp add: power_divide)
    1.94 +    done
    1.95  qed
    1.96  
    1.97  end