src/HOL/Library/Product_Vector.thy
changeset 31492 5400beeddb55
parent 31491 f7310185481d
child 31562 10d0fb526643
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Sun Jun 07 15:18:52 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Sun Jun 07 17:59:54 2009 -0700
     1.3 @@ -45,29 +45,29 @@
     1.4    "*" :: (topological_space, topological_space) topological_space
     1.5  begin
     1.6  
     1.7 -definition topo_prod_def:
     1.8 -  "topo = {S. \<forall>x\<in>S. \<exists>A\<in>topo. \<exists>B\<in>topo. x \<in> A \<times> B \<and> A \<times> B \<subseteq> S}"
     1.9 +definition open_prod_def:
    1.10 +  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
    1.11 +    (\<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.12  
    1.13  instance proof
    1.14 -  show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
    1.15 -    unfolding topo_prod_def by (auto intro: topo_UNIV)
    1.16 +  show "open (UNIV :: ('a \<times> 'b) set)"
    1.17 +    unfolding open_prod_def by auto
    1.18  next
    1.19    fix S T :: "('a \<times> 'b) set"
    1.20 -  assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
    1.21 -    unfolding topo_prod_def
    1.22 +  assume "open S" "open T" thus "open (S \<inter> T)"
    1.23 +    unfolding open_prod_def
    1.24      apply clarify
    1.25      apply (drule (1) bspec)+
    1.26      apply (clarify, rename_tac Sa Ta Sb Tb)
    1.27 -    apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
    1.28 -    apply (simp add: topo_Int)
    1.29 -    apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
    1.30 -    apply (simp add: topo_Int)
    1.31 +    apply (rule_tac x="Sa \<inter> Ta" in exI)
    1.32 +    apply (rule_tac x="Sb \<inter> Tb" in exI)
    1.33 +    apply (simp add: open_Int)
    1.34      apply fast
    1.35      done
    1.36  next
    1.37 -  fix T :: "('a \<times> 'b) set set"
    1.38 -  assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
    1.39 -    unfolding topo_prod_def Bex_def by fast
    1.40 +  fix K :: "('a \<times> 'b) set set"
    1.41 +  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    1.42 +    unfolding open_prod_def by fast
    1.43  qed
    1.44  
    1.45  end
    1.46 @@ -104,9 +104,10 @@
    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 -  show "topo = {S::('a \<times> 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.51 -    unfolding topo_prod_def topo_dist
    1.52 -    apply (safe, rename_tac S a b)
    1.53 +  fix S :: "('a \<times> 'b) set"
    1.54 +  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.55 +    unfolding open_prod_def open_dist
    1.56 +    apply safe
    1.57      apply (drule (1) bspec)
    1.58      apply clarify
    1.59      apply (drule (1) bspec)+
    1.60 @@ -121,18 +122,19 @@
    1.61      apply (drule spec, erule mp)
    1.62      apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
    1.63  
    1.64 -    apply (rename_tac S a b)
    1.65      apply (drule (1) bspec)
    1.66      apply clarify
    1.67      apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
    1.68      apply clarify
    1.69 -    apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
    1.70 +    apply (rule_tac x="{y. dist y a < r}" in exI)
    1.71 +    apply (rule_tac x="{y. dist y b < s}" in exI)
    1.72 +    apply (rule conjI)
    1.73      apply clarify
    1.74      apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
    1.75      apply clarify
    1.76      apply (rule le_less_trans [OF dist_triangle])
    1.77      apply (erule less_le_trans [OF add_strict_right_mono], simp)
    1.78 -    apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
    1.79 +    apply (rule conjI)
    1.80      apply clarify
    1.81      apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
    1.82      apply clarify
    1.83 @@ -163,13 +165,13 @@
    1.84    assumes "(f ---> a) net"
    1.85    shows "((\<lambda>x. fst (f x)) ---> fst a) net"
    1.86  proof (rule topological_tendstoI)
    1.87 -  fix S assume "S \<in> topo" "fst a \<in> S"
    1.88 -  then have "fst -` S \<in> topo" "a \<in> fst -` S"
    1.89 -    unfolding topo_prod_def
    1.90 +  fix S assume "open S" "fst a \<in> S"
    1.91 +  then have "open (fst -` S)" "a \<in> fst -` S"
    1.92 +    unfolding open_prod_def
    1.93      apply simp_all
    1.94      apply clarify
    1.95 -    apply (erule rev_bexI, simp)
    1.96 -    apply (rule rev_bexI [OF topo_UNIV])
    1.97 +    apply (rule exI, erule conjI)
    1.98 +    apply (rule exI, rule conjI [OF open_UNIV])
    1.99      apply auto
   1.100      done
   1.101    with assms have "eventually (\<lambda>x. f x \<in> fst -` S) net"
   1.102 @@ -182,13 +184,13 @@
   1.103    assumes "(f ---> a) net"
   1.104    shows "((\<lambda>x. snd (f x)) ---> snd a) net"
   1.105  proof (rule topological_tendstoI)
   1.106 -  fix S assume "S \<in> topo" "snd a \<in> S"
   1.107 -  then have "snd -` S \<in> topo" "a \<in> snd -` S"
   1.108 -    unfolding topo_prod_def
   1.109 +  fix S assume "open S" "snd a \<in> S"
   1.110 +  then have "open (snd -` S)" "a \<in> snd -` S"
   1.111 +    unfolding open_prod_def
   1.112      apply simp_all
   1.113      apply clarify
   1.114 -    apply (rule rev_bexI [OF topo_UNIV])
   1.115 -    apply (erule rev_bexI)
   1.116 +    apply (rule exI, rule conjI [OF open_UNIV])
   1.117 +    apply (rule exI, erule conjI)
   1.118      apply auto
   1.119      done
   1.120    with assms have "eventually (\<lambda>x. f x \<in> snd -` S) net"
   1.121 @@ -201,15 +203,15 @@
   1.122    assumes "(f ---> a) net" and "(g ---> b) net"
   1.123    shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
   1.124  proof (rule topological_tendstoI)
   1.125 -  fix S assume "S \<in> topo" "(a, b) \<in> S"
   1.126 -  then obtain A B where "A \<in> topo" "B \<in> topo" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   1.127 -    unfolding topo_prod_def by auto
   1.128 +  fix S assume "open S" "(a, b) \<in> S"
   1.129 +  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   1.130 +    unfolding open_prod_def by auto
   1.131    have "eventually (\<lambda>x. f x \<in> A) net"
   1.132 -    using `(f ---> a) net` `A \<in> topo` `a \<in> A`
   1.133 +    using `(f ---> a) net` `open A` `a \<in> A`
   1.134      by (rule topological_tendstoD)
   1.135    moreover
   1.136    have "eventually (\<lambda>x. g x \<in> B) net"
   1.137 -    using `(g ---> b) net` `B \<in> topo` `b \<in> B`
   1.138 +    using `(g ---> b) net` `open B` `b \<in> B`
   1.139      by (rule topological_tendstoD)
   1.140    ultimately
   1.141    show "eventually (\<lambda>x. (f x, g x) \<in> S) net"