author hoelzl Thu Jan 31 11:31:22 2013 +0100 (2013-01-31) changeset 50998 501200635659 parent 50997 31f9ba85dc2e child 50999 3de230ed0547
simplify heine_borel type class
```     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 .
```