replace 'topo' with 'open'; add extra type constraint for 'open'
authorhuffman
Sun Jun 07 17:59:54 2009 -0700 (2009-06-07)
changeset 314925400beeddb55
parent 31491 f7310185481d
child 31493 d92cfed6c6b2
replace 'topo' with 'open'; add extra type constraint for 'open'
src/HOL/Complex.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/Limits.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Complex.thy	Sun Jun 07 15:18:52 2009 -0700
     1.2 +++ b/src/HOL/Complex.thy	Sun Jun 07 17:59:54 2009 -0700
     1.3 @@ -281,8 +281,8 @@
     1.4  definition dist_complex_def:
     1.5    "dist x y = cmod (x - y)"
     1.6  
     1.7 -definition topo_complex_def [code del]:
     1.8 -  "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
     1.9 +definition open_complex_def [code del]:
    1.10 +  "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.11  
    1.12  lemmas cmod_def = complex_norm_def
    1.13  
    1.14 @@ -290,7 +290,7 @@
    1.15    by (simp add: complex_norm_def)
    1.16  
    1.17  instance proof
    1.18 -  fix r :: real and x y :: complex
    1.19 +  fix r :: real and x y :: complex and S :: "complex set"
    1.20    show "0 \<le> norm x"
    1.21      by (induct x) simp
    1.22    show "(norm x = 0) = (x = 0)"
    1.23 @@ -308,8 +308,8 @@
    1.24      by (rule complex_sgn_def)
    1.25    show "dist x y = cmod (x - y)"
    1.26      by (rule dist_complex_def)
    1.27 -  show "topo = {S::complex set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    1.28 -    by (rule topo_complex_def)
    1.29 +  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.30 +    by (rule open_complex_def)
    1.31  qed
    1.32  
    1.33  end
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 15:18:52 2009 -0700
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sun Jun 07 17:59:54 2009 -0700
     2.3 @@ -506,8 +506,9 @@
     2.4  definition dist_vector_def:
     2.5    "dist (x::'a^'b) (y::'a^'b) = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
     2.6  
     2.7 -definition topo_vector_def:
     2.8 -  "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
     2.9 +definition open_vector_def:
    2.10 +  "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
    2.11 +    (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    2.12  
    2.13  instance proof
    2.14    fix x y :: "'a ^ 'b"
    2.15 @@ -522,8 +523,9 @@
    2.16      apply (simp add: setL2_mono dist_triangle2)
    2.17      done
    2.18  next
    2.19 -  show "topo = {S::('a ^ 'b) set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    2.20 -    by (rule topo_vector_def)
    2.21 +  fix S :: "('a ^ 'b) set"
    2.22 +  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    2.23 +    by (rule open_vector_def)
    2.24  qed
    2.25  
    2.26  end
     3.1 --- a/src/HOL/Library/Inner_Product.thy	Sun Jun 07 15:18:52 2009 -0700
     3.2 +++ b/src/HOL/Library/Inner_Product.thy	Sun Jun 07 17:59:54 2009 -0700
     3.3 @@ -10,7 +10,13 @@
     3.4  
     3.5  subsection {* Real inner product spaces *}
     3.6  
     3.7 -text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
     3.8 +text {*
     3.9 +  Temporarily relax type constraints for @{term "open"},
    3.10 +  @{term dist}, and @{term norm}.
    3.11 +*}
    3.12 +
    3.13 +setup {* Sign.add_const_constraint
    3.14 +  (@{const_name "open"}, SOME @{typ "'a::open set \<Rightarrow> bool"}) *}
    3.15  
    3.16  setup {* Sign.add_const_constraint
    3.17    (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
    3.18 @@ -18,7 +24,7 @@
    3.19  setup {* Sign.add_const_constraint
    3.20    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
    3.21  
    3.22 -class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
    3.23 +class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
    3.24    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    3.25    assumes inner_commute: "inner x y = inner y x"
    3.26    and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
    3.27 @@ -124,7 +130,13 @@
    3.28  
    3.29  end
    3.30  
    3.31 -text {* Re-enable constraints for @{term dist} and @{term norm}. *}
    3.32 +text {*
    3.33 +  Re-enable constraints for @{term "open"},
    3.34 +  @{term dist}, and @{term norm}.
    3.35 +*}
    3.36 +
    3.37 +setup {* Sign.add_const_constraint
    3.38 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
    3.39  
    3.40  setup {* Sign.add_const_constraint
    3.41    (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
     4.1 --- a/src/HOL/Library/Product_Vector.thy	Sun Jun 07 15:18:52 2009 -0700
     4.2 +++ b/src/HOL/Library/Product_Vector.thy	Sun Jun 07 17:59:54 2009 -0700
     4.3 @@ -45,29 +45,29 @@
     4.4    "*" :: (topological_space, topological_space) topological_space
     4.5  begin
     4.6  
     4.7 -definition topo_prod_def:
     4.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}"
     4.9 +definition open_prod_def:
    4.10 +  "open (S :: ('a \<times> 'b) set) \<longleftrightarrow>
    4.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)"
    4.12  
    4.13  instance proof
    4.14 -  show "(UNIV :: ('a \<times> 'b) set) \<in> topo"
    4.15 -    unfolding topo_prod_def by (auto intro: topo_UNIV)
    4.16 +  show "open (UNIV :: ('a \<times> 'b) set)"
    4.17 +    unfolding open_prod_def by auto
    4.18  next
    4.19    fix S T :: "('a \<times> 'b) set"
    4.20 -  assume "S \<in> topo" "T \<in> topo" thus "S \<inter> T \<in> topo"
    4.21 -    unfolding topo_prod_def
    4.22 +  assume "open S" "open T" thus "open (S \<inter> T)"
    4.23 +    unfolding open_prod_def
    4.24      apply clarify
    4.25      apply (drule (1) bspec)+
    4.26      apply (clarify, rename_tac Sa Ta Sb Tb)
    4.27 -    apply (rule_tac x="Sa \<inter> Ta" in rev_bexI)
    4.28 -    apply (simp add: topo_Int)
    4.29 -    apply (rule_tac x="Sb \<inter> Tb" in rev_bexI)
    4.30 -    apply (simp add: topo_Int)
    4.31 +    apply (rule_tac x="Sa \<inter> Ta" in exI)
    4.32 +    apply (rule_tac x="Sb \<inter> Tb" in exI)
    4.33 +    apply (simp add: open_Int)
    4.34      apply fast
    4.35      done
    4.36  next
    4.37 -  fix T :: "('a \<times> 'b) set set"
    4.38 -  assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
    4.39 -    unfolding topo_prod_def Bex_def by fast
    4.40 +  fix K :: "('a \<times> 'b) set set"
    4.41 +  assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    4.42 +    unfolding open_prod_def by fast
    4.43  qed
    4.44  
    4.45  end
    4.46 @@ -104,9 +104,10 @@
    4.47    (* FIXME: long proof! *)
    4.48    (* Maybe it would be easier to define topological spaces *)
    4.49    (* in terms of neighborhoods instead of open sets? *)
    4.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}"
    4.51 -    unfolding topo_prod_def topo_dist
    4.52 -    apply (safe, rename_tac S a b)
    4.53 +  fix S :: "('a \<times> 'b) set"
    4.54 +  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    4.55 +    unfolding open_prod_def open_dist
    4.56 +    apply safe
    4.57      apply (drule (1) bspec)
    4.58      apply clarify
    4.59      apply (drule (1) bspec)+
    4.60 @@ -121,18 +122,19 @@
    4.61      apply (drule spec, erule mp)
    4.62      apply (erule le_less_trans [OF real_sqrt_sum_squares_ge2])
    4.63  
    4.64 -    apply (rename_tac S a b)
    4.65      apply (drule (1) bspec)
    4.66      apply clarify
    4.67      apply (subgoal_tac "\<exists>r>0. \<exists>s>0. e = sqrt (r\<twosuperior> + s\<twosuperior>)")
    4.68      apply clarify
    4.69 -    apply (rule_tac x="{y. dist y a < r}" in rev_bexI)
    4.70 +    apply (rule_tac x="{y. dist y a < r}" in exI)
    4.71 +    apply (rule_tac x="{y. dist y b < s}" in exI)
    4.72 +    apply (rule conjI)
    4.73      apply clarify
    4.74      apply (rule_tac x="r - dist x a" in exI, rule conjI, simp)
    4.75      apply clarify
    4.76      apply (rule le_less_trans [OF dist_triangle])
    4.77      apply (erule less_le_trans [OF add_strict_right_mono], simp)
    4.78 -    apply (rule_tac x="{y. dist y b < s}" in rev_bexI)
    4.79 +    apply (rule conjI)
    4.80      apply clarify
    4.81      apply (rule_tac x="s - dist x b" in exI, rule conjI, simp)
    4.82      apply clarify
    4.83 @@ -163,13 +165,13 @@
    4.84    assumes "(f ---> a) net"
    4.85    shows "((\<lambda>x. fst (f x)) ---> fst a) net"
    4.86  proof (rule topological_tendstoI)
    4.87 -  fix S assume "S \<in> topo" "fst a \<in> S"
    4.88 -  then have "fst -` S \<in> topo" "a \<in> fst -` S"
    4.89 -    unfolding topo_prod_def
    4.90 +  fix S assume "open S" "fst a \<in> S"
    4.91 +  then have "open (fst -` S)" "a \<in> fst -` S"
    4.92 +    unfolding open_prod_def
    4.93      apply simp_all
    4.94      apply clarify
    4.95 -    apply (erule rev_bexI, simp)
    4.96 -    apply (rule rev_bexI [OF topo_UNIV])
    4.97 +    apply (rule exI, erule conjI)
    4.98 +    apply (rule exI, rule conjI [OF open_UNIV])
    4.99      apply auto
   4.100      done
   4.101    with assms have "eventually (\<lambda>x. f x \<in> fst -` S) net"
   4.102 @@ -182,13 +184,13 @@
   4.103    assumes "(f ---> a) net"
   4.104    shows "((\<lambda>x. snd (f x)) ---> snd a) net"
   4.105  proof (rule topological_tendstoI)
   4.106 -  fix S assume "S \<in> topo" "snd a \<in> S"
   4.107 -  then have "snd -` S \<in> topo" "a \<in> snd -` S"
   4.108 -    unfolding topo_prod_def
   4.109 +  fix S assume "open S" "snd a \<in> S"
   4.110 +  then have "open (snd -` S)" "a \<in> snd -` S"
   4.111 +    unfolding open_prod_def
   4.112      apply simp_all
   4.113      apply clarify
   4.114 -    apply (rule rev_bexI [OF topo_UNIV])
   4.115 -    apply (erule rev_bexI)
   4.116 +    apply (rule exI, rule conjI [OF open_UNIV])
   4.117 +    apply (rule exI, erule conjI)
   4.118      apply auto
   4.119      done
   4.120    with assms have "eventually (\<lambda>x. f x \<in> snd -` S) net"
   4.121 @@ -201,15 +203,15 @@
   4.122    assumes "(f ---> a) net" and "(g ---> b) net"
   4.123    shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
   4.124  proof (rule topological_tendstoI)
   4.125 -  fix S assume "S \<in> topo" "(a, b) \<in> S"
   4.126 -  then obtain A B where "A \<in> topo" "B \<in> topo" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   4.127 -    unfolding topo_prod_def by auto
   4.128 +  fix S assume "open S" "(a, b) \<in> S"
   4.129 +  then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
   4.130 +    unfolding open_prod_def by auto
   4.131    have "eventually (\<lambda>x. f x \<in> A) net"
   4.132 -    using `(f ---> a) net` `A \<in> topo` `a \<in> A`
   4.133 +    using `(f ---> a) net` `open A` `a \<in> A`
   4.134      by (rule topological_tendstoD)
   4.135    moreover
   4.136    have "eventually (\<lambda>x. g x \<in> B) net"
   4.137 -    using `(g ---> b) net` `B \<in> topo` `b \<in> B`
   4.138 +    using `(g ---> b) net` `open B` `b \<in> B`
   4.139      by (rule topological_tendstoD)
   4.140    ultimately
   4.141    show "eventually (\<lambda>x. (f x, g x) \<in> S) net"
     5.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Jun 07 15:18:52 2009 -0700
     5.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Sun Jun 07 17:59:54 2009 -0700
     5.3 @@ -255,11 +255,6 @@
     5.4  
     5.5  subsection{* Topological properties of open balls *}
     5.6  
     5.7 -lemma open_dist:
     5.8 -  fixes S :: "'a::metric_space set"
     5.9 -  shows "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
    5.10 -  unfolding open_def topo_dist by simp
    5.11 -
    5.12  lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
    5.13    "(a::real) - b < 0 \<longleftrightarrow> a < b"
    5.14    "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
    5.15 @@ -274,7 +269,7 @@
    5.16    using dist_triangle_alt[where z=x]
    5.17    apply (clarsimp simp add: diff_less_iff)
    5.18    apply atomize
    5.19 -  apply (erule_tac x="x'" in allE)
    5.20 +  apply (erule_tac x="y" in allE)
    5.21    apply (erule_tac x="xa" in allE)
    5.22    by arith
    5.23  
    5.24 @@ -1004,7 +999,7 @@
    5.25    thus "\<not> a islimpt S"
    5.26      unfolding trivial_limit_def
    5.27      unfolding Rep_net_within Rep_net_at
    5.28 -    unfolding islimpt_def open_def [symmetric]
    5.29 +    unfolding islimpt_def
    5.30      apply (clarsimp simp add: expand_set_eq)
    5.31      apply (rename_tac T, rule_tac x=T in exI)
    5.32      apply (clarsimp, drule_tac x=y in spec, simp)
    5.33 @@ -1014,7 +1009,7 @@
    5.34    thus "trivial_limit (at a within S)"
    5.35      unfolding trivial_limit_def
    5.36      unfolding Rep_net_within Rep_net_at
    5.37 -    unfolding islimpt_def open_def [symmetric]
    5.38 +    unfolding islimpt_def
    5.39      apply (clarsimp simp add: image_image)
    5.40      apply (rule_tac x=T in image_eqI)
    5.41      apply (auto simp add: expand_set_eq)
    5.42 @@ -1164,7 +1159,8 @@
    5.43    shows "(f ---> l) (net within (S \<union> T))"
    5.44    using assms unfolding tendsto_def Limits.eventually_within
    5.45    apply clarify
    5.46 -  apply (drule (1) bspec)+
    5.47 +  apply (drule spec, drule (1) mp, drule (1) mp)
    5.48 +  apply (drule spec, drule (1) mp, drule (1) mp)
    5.49    apply (auto elim: eventually_elim2)
    5.50    done
    5.51  
    5.52 @@ -1177,7 +1173,7 @@
    5.53  
    5.54  lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
    5.55    unfolding tendsto_def Limits.eventually_within
    5.56 -  apply (clarify, drule (1) bspec)
    5.57 +  apply (clarify, drule spec, drule (1) mp, drule (1) mp)
    5.58    by (auto elim!: eventually_elim1)
    5.59  
    5.60  lemma Lim_within_open:
    5.61 @@ -1192,13 +1188,13 @@
    5.62      hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
    5.63        unfolding Limits.eventually_within .
    5.64      then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> dist (f x) l < e"
    5.65 -      unfolding eventually_at_topological open_def by fast
    5.66 +      unfolding eventually_at_topological by fast
    5.67      hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> dist (f x) l < e"
    5.68        using assms by auto
    5.69      hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
    5.70        by fast
    5.71      hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
    5.72 -      unfolding eventually_at_topological open_def Bex_def .
    5.73 +      unfolding eventually_at_topological .
    5.74    }
    5.75    thus ?rhs by (rule tendstoI)
    5.76  next
    5.77 @@ -1778,6 +1774,7 @@
    5.78  unfolding Collect_neg_eq [symmetric] not_le
    5.79  apply (clarsimp simp add: open_dist, rename_tac y)
    5.80  apply (rule_tac x="dist x y - e" in exI, clarsimp)
    5.81 +apply (rename_tac x')
    5.82  apply (cut_tac x=x and y=x' and z=y in dist_triangle)
    5.83  apply simp
    5.84  done
     6.1 --- a/src/HOL/Limits.thy	Sun Jun 07 15:18:52 2009 -0700
     6.2 +++ b/src/HOL/Limits.thy	Sun Jun 07 17:59:54 2009 -0700
     6.3 @@ -114,7 +114,7 @@
     6.4  
     6.5  definition
     6.6    at :: "'a::topological_space \<Rightarrow> 'a net" where
     6.7 -  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
     6.8 +  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
     6.9  
    6.10  lemma Rep_net_sequentially:
    6.11    "Rep_net sequentially = range (\<lambda>n. {n..})"
    6.12 @@ -136,13 +136,13 @@
    6.13  done
    6.14  
    6.15  lemma Rep_net_at:
    6.16 -  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
    6.17 +  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
    6.18  unfolding at_def
    6.19  apply (rule Abs_net_inverse')
    6.20  apply (rule image_nonempty)
    6.21 -apply (rule_tac x="UNIV" in exI, simp add: topo_UNIV)
    6.22 +apply (rule_tac x="UNIV" in exI, simp)
    6.23  apply (clarsimp, rename_tac S T)
    6.24 -apply (rule_tac x="S \<inter> T" in exI, auto simp add: topo_Int)
    6.25 +apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int)
    6.26  done
    6.27  
    6.28  lemma eventually_sequentially:
    6.29 @@ -154,16 +154,16 @@
    6.30  unfolding eventually_def Rep_net_within by auto
    6.31  
    6.32  lemma eventually_at_topological:
    6.33 -  "eventually P (at a) \<longleftrightarrow> (\<exists>S\<in>topo. a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
    6.34 +  "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
    6.35  unfolding eventually_def Rep_net_at by auto
    6.36  
    6.37  lemma eventually_at:
    6.38    fixes a :: "'a::metric_space"
    6.39    shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    6.40 -unfolding eventually_at_topological topo_dist
    6.41 +unfolding eventually_at_topological open_dist
    6.42  apply safe
    6.43  apply fast
    6.44 -apply (rule_tac x="{x. dist x a < d}" in bexI, simp)
    6.45 +apply (rule_tac x="{x. dist x a < d}" in exI, simp)
    6.46  apply clarsimp
    6.47  apply (rule_tac x="d - dist x a" in exI, clarsimp)
    6.48  apply (simp only: less_diff_eq)
    6.49 @@ -356,22 +356,22 @@
    6.50    tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
    6.51      (infixr "--->" 55)
    6.52  where [code del]:
    6.53 -  "(f ---> l) net \<longleftrightarrow> (\<forall>S\<in>topo. l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
    6.54 +  "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
    6.55  
    6.56  lemma topological_tendstoI:
    6.57 -  "(\<And>S. S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
    6.58 +  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
    6.59      \<Longrightarrow> (f ---> l) net"
    6.60    unfolding tendsto_def by auto
    6.61  
    6.62  lemma topological_tendstoD:
    6.63 -  "(f ---> l) net \<Longrightarrow> S \<in> topo \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
    6.64 +  "(f ---> l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
    6.65    unfolding tendsto_def by auto
    6.66  
    6.67  lemma tendstoI:
    6.68    assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
    6.69    shows "(f ---> l) net"
    6.70  apply (rule topological_tendstoI)
    6.71 -apply (simp add: topo_dist)
    6.72 +apply (simp add: open_dist)
    6.73  apply (drule (1) bspec, clarify)
    6.74  apply (drule assms)
    6.75  apply (erule eventually_elim1, simp)
    6.76 @@ -380,7 +380,7 @@
    6.77  lemma tendstoD:
    6.78    "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
    6.79  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
    6.80 -apply (clarsimp simp add: topo_dist)
    6.81 +apply (clarsimp simp add: open_dist)
    6.82  apply (rule_tac x="e - dist x l" in exI, clarsimp)
    6.83  apply (simp only: less_diff_eq)
    6.84  apply (erule le_less_trans [OF dist_triangle])
     7.1 --- a/src/HOL/RealVector.thy	Sun Jun 07 15:18:52 2009 -0700
     7.2 +++ b/src/HOL/RealVector.thy	Sun Jun 07 17:59:54 2009 -0700
     7.3 @@ -418,39 +418,19 @@
     7.4  
     7.5  subsection {* Topological spaces *}
     7.6  
     7.7 -class topo =
     7.8 -  fixes topo :: "'a set set"
     7.9 -
    7.10 -text {*
    7.11 -  The syntactic class uses @{term topo} instead of @{text "open"}
    7.12 -  so that @{text "open"} and @{text closed} will have the same type.
    7.13 -  Maybe we could use extra type constraints instead, like with
    7.14 -  @{text dist} and @{text norm}?
    7.15 -*}
    7.16 +class "open" =
    7.17 +  fixes "open" :: "'a set set"
    7.18  
    7.19 -class topological_space = topo +
    7.20 -  assumes topo_UNIV: "UNIV \<in> topo"
    7.21 -  assumes topo_Int: "A \<in> topo \<Longrightarrow> B \<in> topo \<Longrightarrow> A \<inter> B \<in> topo"
    7.22 -  assumes topo_Union: "T \<subseteq> topo \<Longrightarrow> \<Union>T \<in> topo"
    7.23 +class topological_space = "open" +
    7.24 +  assumes open_UNIV [simp, intro]: "open UNIV"
    7.25 +  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
    7.26 +  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
    7.27  begin
    7.28  
    7.29  definition
    7.30 -  "open" :: "'a set \<Rightarrow> bool" where
    7.31 -  "open S \<longleftrightarrow> S \<in> topo"
    7.32 -
    7.33 -definition
    7.34    closed :: "'a set \<Rightarrow> bool" where
    7.35    "closed S \<longleftrightarrow> open (- S)"
    7.36  
    7.37 -lemma open_UNIV [intro, simp]:  "open UNIV"
    7.38 -  unfolding open_def by (rule topo_UNIV)
    7.39 -
    7.40 -lemma open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
    7.41 -  unfolding open_def by (rule topo_Int)
    7.42 -
    7.43 -lemma open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
    7.44 -  unfolding open_def subset_eq [symmetric] by (rule topo_Union)
    7.45 -
    7.46  lemma open_empty [intro, simp]: "open {}"
    7.47    using open_Union [of "{}"] by simp
    7.48  
    7.49 @@ -516,10 +496,10 @@
    7.50  class dist =
    7.51    fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    7.52  
    7.53 -class topo_dist = topo + dist +
    7.54 -  assumes topo_dist: "topo = {S. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
    7.55 +class open_dist = "open" + dist +
    7.56 +  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    7.57  
    7.58 -class metric_space = topo_dist +
    7.59 +class metric_space = open_dist +
    7.60    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    7.61    assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    7.62  begin
    7.63 @@ -554,20 +534,20 @@
    7.64  proof
    7.65    have "\<exists>e::real. 0 < e"
    7.66      by (fast intro: zero_less_one)
    7.67 -  then show "UNIV \<in> topo"
    7.68 -    unfolding topo_dist by simp
    7.69 +  then show "open UNIV"
    7.70 +    unfolding open_dist by simp
    7.71  next
    7.72 -  fix A B assume "A \<in> topo" "B \<in> topo"
    7.73 -  then show "A \<inter> B \<in> topo"
    7.74 -    unfolding topo_dist
    7.75 +  fix S T assume "open S" "open T"
    7.76 +  then show "open (S \<inter> T)"
    7.77 +    unfolding open_dist
    7.78      apply clarify
    7.79      apply (drule (1) bspec)+
    7.80      apply (clarify, rename_tac r s)
    7.81      apply (rule_tac x="min r s" in exI, simp)
    7.82      done
    7.83  next
    7.84 -  fix T assume "T \<subseteq> topo" thus "\<Union>T \<in> topo"
    7.85 -    unfolding topo_dist by fast
    7.86 +  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
    7.87 +    unfolding open_dist by fast
    7.88  qed
    7.89  
    7.90  end
    7.91 @@ -584,7 +564,7 @@
    7.92  class dist_norm = dist + norm + minus +
    7.93    assumes dist_norm: "dist x y = norm (x - y)"
    7.94  
    7.95 -class real_normed_vector = real_vector + sgn_div_norm + dist_norm + topo_dist +
    7.96 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
    7.97    assumes norm_ge_zero [simp]: "0 \<le> norm x"
    7.98    and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    7.99    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
   7.100 @@ -621,14 +601,14 @@
   7.101  definition dist_real_def:
   7.102    "dist x y = \<bar>x - y\<bar>"
   7.103  
   7.104 -definition topo_real_def [code del]:
   7.105 -  "topo = {S::real set. \<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S}"
   7.106 +definition open_real_def [code del]:
   7.107 +  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   7.108  
   7.109  instance
   7.110  apply (intro_classes, unfold real_norm_def real_scaleR_def)
   7.111  apply (rule dist_real_def)
   7.112 +apply (rule open_real_def)
   7.113  apply (simp add: real_sgn_def)
   7.114 -apply (rule topo_real_def)
   7.115  apply (rule abs_ge_zero)
   7.116  apply (rule abs_eq_0)
   7.117  apply (rule abs_triangle_ineq)
   7.118 @@ -819,6 +799,11 @@
   7.119  
   7.120  subsection {* Extra type constraints *}
   7.121  
   7.122 +text {* Only allow @{term "open"} in class @{text topological_space}. *}
   7.123 +
   7.124 +setup {* Sign.add_const_constraint
   7.125 +  (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"}) *}
   7.126 +
   7.127  text {* Only allow @{term dist} in class @{text metric_space}. *}
   7.128  
   7.129  setup {* Sign.add_const_constraint