simplify heine_borel type class
authorhoelzl
Thu Jan 31 11:31:22 2013 +0100 (2013-01-31)
changeset 50998501200635659
parent 50997 31f9ba85dc2e
child 50999 3de230ed0547
simplify heine_borel type class
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 31 11:20:12 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 31 11:31:22 2013 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}
     1.6  
     1.7  theory Cartesian_Euclidean_Space
     1.8 @@ -828,7 +827,7 @@
     1.9  
    1.10  lemma compact_lemma_cart:
    1.11    fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
    1.12 -  assumes "bounded s" and "\<forall>n. f n \<in> s"
    1.13 +  assumes f: "bounded (range f)"
    1.14    shows "\<forall>d.
    1.15          \<exists>l r. subseq r \<and>
    1.16          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
    1.17 @@ -842,16 +841,17 @@
    1.18      thus ?case unfolding subseq_def by auto
    1.19    next
    1.20      case (insert k d)
    1.21 -    have s': "bounded ((\<lambda>x. x $ k) ` s)"
    1.22 -      using `bounded s` by (rule bounded_component_cart)
    1.23      obtain l1::"'a^'n" and r1 where r1:"subseq r1"
    1.24        and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
    1.25        using insert(3) by auto
    1.26 -    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` s"
    1.27 -      using `\<forall>n. f n \<in> s` by simp
    1.28 -    obtain l2 r2 where r2: "subseq r2"
    1.29 +    have s': "bounded ((\<lambda>x. x $ k) ` range f)" using `bounded (range f)`
    1.30 +      by (auto intro!: bounded_component_cart)
    1.31 +    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp
    1.32 +    have "bounded (range (\<lambda>i. f (r1 i) $ k))"
    1.33 +      by (metis (lifting) bounded_subset image_subsetI f' s')
    1.34 +    then obtain l2 r2 where r2: "subseq r2"
    1.35        and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
    1.36 -      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
    1.37 +      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def)
    1.38      def r \<equiv> "r1 \<circ> r2"
    1.39      have r: "subseq r"
    1.40        using r1 and r2 unfolding r_def o_def subseq_def by auto
    1.41 @@ -873,11 +873,11 @@
    1.42  
    1.43  instance vec :: (heine_borel, finite) heine_borel
    1.44  proof
    1.45 -  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
    1.46 -  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
    1.47 +  fix f :: "nat \<Rightarrow> 'a ^ 'b"
    1.48 +  assume f: "bounded (range f)"
    1.49    then obtain l r where r: "subseq r"
    1.50        and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
    1.51 -    using compact_lemma_cart [OF s f] by blast
    1.52 +    using compact_lemma_cart [OF f] by blast
    1.53    let ?d = "UNIV::'b set"
    1.54    { fix e::real assume "e>0"
    1.55      hence "0 < e / (real_of_nat (card ?d))"
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 31 11:20:12 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 31 11:31:22 2013 +0100
     2.3 @@ -47,6 +47,17 @@
     2.4  definition "topological_basis B =
     2.5    ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
     2.6  
     2.7 +lemma "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x))"
     2.8 +  unfolding topological_basis_def
     2.9 +  apply safe
    2.10 +     apply fastforce
    2.11 +    apply fastforce
    2.12 +   apply (erule_tac x="x" in allE)
    2.13 +   apply simp
    2.14 +   apply (rule_tac x="{x}" in exI)
    2.15 +  apply auto
    2.16 +  done
    2.17 +
    2.18  lemma topological_basis_iff:
    2.19    assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
    2.20    shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))"
    2.21 @@ -2143,6 +2154,9 @@
    2.22    bounded :: "'a set \<Rightarrow> bool" where
    2.23    "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
    2.24  
    2.25 +lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
    2.26 +  unfolding bounded_def subset_eq by auto
    2.27 +
    2.28  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
    2.29  unfolding bounded_def
    2.30  apply safe
    2.31 @@ -3202,16 +3216,16 @@
    2.32  
    2.33  class heine_borel = metric_space +
    2.34    assumes bounded_imp_convergent_subsequence:
    2.35 -    "bounded s \<Longrightarrow> \<forall>n. f n \<in> s
    2.36 -      \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
    2.37 +    "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
    2.38  
    2.39  lemma bounded_closed_imp_seq_compact:
    2.40    fixes s::"'a::heine_borel set"
    2.41    assumes "bounded s" and "closed s" shows "seq_compact s"
    2.42  proof (unfold seq_compact_def, clarify)
    2.43    fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
    2.44 +  with `bounded s` have "bounded (range f)" by (auto intro: bounded_subset)
    2.45    obtain l r where r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
    2.46 -    using bounded_imp_convergent_subsequence [OF `bounded s` `\<forall>n. f n \<in> s`] by auto
    2.47 +    using bounded_imp_convergent_subsequence [OF `bounded (range f)`] by auto
    2.48    from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp
    2.49    have "l \<in> s" using `closed s` fr l
    2.50      unfolding closed_sequential_limits by blast
    2.51 @@ -3239,20 +3253,20 @@
    2.52  
    2.53  instance real :: heine_borel
    2.54  proof
    2.55 -  fix s :: "real set" and f :: "nat \<Rightarrow> real"
    2.56 -  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
    2.57 +  fix f :: "nat \<Rightarrow> real"
    2.58 +  assume f: "bounded (range f)"
    2.59    obtain r where r: "subseq r" "monoseq (f \<circ> r)"
    2.60      unfolding comp_def by (metis seq_monosub)
    2.61    moreover
    2.62    then have "Bseq (f \<circ> r)"
    2.63 -    unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
    2.64 +    unfolding Bseq_eq_bounded using f by (auto intro: bounded_subset)
    2.65    ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
    2.66      using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
    2.67  qed
    2.68  
    2.69  lemma compact_lemma:
    2.70    fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
    2.71 -  assumes "bounded s" and "\<forall>n. f n \<in> s"
    2.72 +  assumes "bounded (range f)"
    2.73    shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
    2.74          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
    2.75  proof safe
    2.76 @@ -3262,14 +3276,16 @@
    2.77        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
    2.78    proof(induct d) case empty thus ?case unfolding subseq_def by auto
    2.79    next case (insert k d) have k[intro]:"k\<in>Basis" using insert by auto
    2.80 -    have s': "bounded ((\<lambda>x. x \<bullet> k) ` s)" using `bounded s`
    2.81 +    have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)" using `bounded (range f)`
    2.82        by (auto intro!: bounded_linear_image bounded_linear_inner_left)
    2.83      obtain l1::"'a" and r1 where r1:"subseq r1" and
    2.84        lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
    2.85        using insert(3) using insert(4) by auto
    2.86 -    have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` s" using `\<forall>n. f n \<in> s` by simp
    2.87 -    obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
    2.88 -      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
    2.89 +    have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f" by simp
    2.90 +    have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))"
    2.91 +      by (metis (lifting) bounded_subset f' image_subsetI s')
    2.92 +    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
    2.93 +      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"] by (auto simp: o_def)
    2.94      def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
    2.95        using r1 and r2 unfolding r_def o_def subseq_def by auto
    2.96      moreover
    2.97 @@ -3289,11 +3305,11 @@
    2.98  
    2.99  instance euclidean_space \<subseteq> heine_borel
   2.100  proof
   2.101 -  fix s :: "'a set" and f :: "nat \<Rightarrow> 'a"
   2.102 -  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
   2.103 +  fix f :: "nat \<Rightarrow> 'a"
   2.104 +  assume f: "bounded (range f)"
   2.105    then obtain l::'a and r where r: "subseq r"
   2.106      and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
   2.107 -    using compact_lemma [OF s f] by blast
   2.108 +    using compact_lemma [OF f] by blast
   2.109    { fix e::real assume "e>0"
   2.110      hence "0 < e / real_of_nat DIM('a)" by (auto intro!: divide_pos_pos DIM_positive)
   2.111      with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
   2.112 @@ -3338,19 +3354,16 @@
   2.113  
   2.114  instance prod :: (heine_borel, heine_borel) heine_borel
   2.115  proof
   2.116 -  fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b"
   2.117 -  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
   2.118 -  from s have s1: "bounded (fst ` s)" by (rule bounded_fst)
   2.119 -  from f have f1: "\<forall>n. fst (f n) \<in> fst ` s" by simp
   2.120 -  obtain l1 r1 where r1: "subseq r1"
   2.121 -    and l1: "((\<lambda>n. fst (f (r1 n))) ---> l1) sequentially"
   2.122 -    using bounded_imp_convergent_subsequence [OF s1 f1]
   2.123 -    unfolding o_def by fast
   2.124 -  from s have s2: "bounded (snd ` s)" by (rule bounded_snd)
   2.125 -  from f have f2: "\<forall>n. snd (f (r1 n)) \<in> snd ` s" by simp
   2.126 +  fix f :: "nat \<Rightarrow> 'a \<times> 'b"
   2.127 +  assume f: "bounded (range f)"
   2.128 +  from f have s1: "bounded (range (fst \<circ> f))" unfolding image_comp by (rule bounded_fst)
   2.129 +  obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1"
   2.130 +    using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
   2.131 +  from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
   2.132 +    by (auto simp add: image_comp intro: bounded_snd bounded_subset)
   2.133    obtain l2 r2 where r2: "subseq r2"
   2.134      and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially"
   2.135 -    using bounded_imp_convergent_subsequence [OF s2 f2]
   2.136 +    using bounded_imp_convergent_subsequence [OF s2]
   2.137      unfolding o_def by fast
   2.138    have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
   2.139      using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .