author hoelzl Thu, 31 Jan 2013 11:31:22 +0100 changeset 50998 501200635659 parent 50997 31f9ba85dc2e child 50999 3de230ed0547
simplify heine_borel type class
```--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 31 11:20:12 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jan 31 11:31:22 2013 +0100
@@ -1,4 +1,3 @@
-
header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*}

theory Cartesian_Euclidean_Space
@@ -828,7 +827,7 @@

lemma compact_lemma_cart:
fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
-  assumes "bounded s" and "\<forall>n. f n \<in> s"
+  assumes f: "bounded (range f)"
shows "\<forall>d.
\<exists>l r. subseq r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \$ i) (l \$ i) < e) sequentially)"
@@ -842,16 +841,17 @@
thus ?case unfolding subseq_def by auto
next
case (insert k d)
-    have s': "bounded ((\<lambda>x. x \$ k) ` s)"
-      using `bounded s` by (rule bounded_component_cart)
obtain l1::"'a^'n" and r1 where r1:"subseq r1"
and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \$ i) (l1 \$ i) < e) sequentially"
using insert(3) by auto
-    have f': "\<forall>n. f (r1 n) \$ k \<in> (\<lambda>x. x \$ k) ` s"
-      using `\<forall>n. f n \<in> s` by simp
-    obtain l2 r2 where r2: "subseq r2"
+    have s': "bounded ((\<lambda>x. x \$ k) ` range f)" using `bounded (range f)`
+      by (auto intro!: bounded_component_cart)
+    have f': "\<forall>n. f (r1 n) \$ k \<in> (\<lambda>x. x \$ k) ` range f" by simp
+    have "bounded (range (\<lambda>i. f (r1 i) \$ k))"
+      by (metis (lifting) bounded_subset image_subsetI f' s')
+    then obtain l2 r2 where r2: "subseq r2"
and lr2: "((\<lambda>i. f (r1 (r2 i)) \$ k) ---> l2) sequentially"
-      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
+      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \$ k"] by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2"
have r: "subseq r"
using r1 and r2 unfolding r_def o_def subseq_def by auto
@@ -873,11 +873,11 @@

instance vec :: (heine_borel, finite) heine_borel
proof
-  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
-  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+  fix f :: "nat \<Rightarrow> 'a ^ 'b"
+  assume f: "bounded (range f)"
then obtain l r where r: "subseq r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) \$ i) (l \$ i) < e) sequentially"
-    using compact_lemma_cart [OF s f] by blast
+    using compact_lemma_cart [OF f] by blast
let ?d = "UNIV::'b set"
{ fix e::real assume "e>0"
hence "0 < e / (real_of_nat (card ?d))"```
```--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 31 11:20:12 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Jan 31 11:31:22 2013 +0100
@@ -47,6 +47,17 @@
definition "topological_basis B =
((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"

+lemma "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x))"
+  unfolding topological_basis_def
+  apply safe
+     apply fastforce
+    apply fastforce
+   apply (erule_tac x="x" in allE)
+   apply simp
+   apply (rule_tac x="{x}" in exI)
+  apply auto
+  done
+
lemma topological_basis_iff:
assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
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'))"
@@ -2143,6 +2154,9 @@
bounded :: "'a set \<Rightarrow> bool" where
"bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"

+lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
+  unfolding bounded_def subset_eq by auto
+
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
unfolding bounded_def
apply safe
@@ -3202,16 +3216,16 @@

class heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
-    "bounded s \<Longrightarrow> \<forall>n. f n \<in> s
-      \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+    "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"

lemma bounded_closed_imp_seq_compact:
fixes s::"'a::heine_borel set"
assumes "bounded s" and "closed s" shows "seq_compact s"
proof (unfold seq_compact_def, clarify)
fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+  with `bounded s` have "bounded (range f)" by (auto intro: bounded_subset)
obtain l r where r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
-    using bounded_imp_convergent_subsequence [OF `bounded s` `\<forall>n. f n \<in> s`] by auto
+    using bounded_imp_convergent_subsequence [OF `bounded (range f)`] by auto
from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp
have "l \<in> s" using `closed s` fr l
unfolding closed_sequential_limits by blast
@@ -3239,20 +3253,20 @@

instance real :: heine_borel
proof
-  fix s :: "real set" and f :: "nat \<Rightarrow> real"
-  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+  fix f :: "nat \<Rightarrow> real"
+  assume f: "bounded (range f)"
obtain r where r: "subseq r" "monoseq (f \<circ> r)"
unfolding comp_def by (metis seq_monosub)
moreover
then have "Bseq (f \<circ> r)"
-    unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
+    unfolding Bseq_eq_bounded using f by (auto intro: bounded_subset)
ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed

lemma compact_lemma:
fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
-  assumes "bounded s" and "\<forall>n. f n \<in> s"
+  assumes "bounded (range f)"
shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
proof safe
@@ -3262,14 +3276,16 @@
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
proof(induct d) case empty thus ?case unfolding subseq_def by auto
next case (insert k d) have k[intro]:"k\<in>Basis" using insert by auto
-    have s': "bounded ((\<lambda>x. x \<bullet> k) ` s)" using `bounded s`
+    have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)" using `bounded (range f)`
by (auto intro!: bounded_linear_image bounded_linear_inner_left)
obtain l1::"'a" and r1 where r1:"subseq r1" and
lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
using insert(3) using insert(4) by auto
-    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
-    obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
-      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
+    have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f" by simp
+    have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))"
+      by (metis (lifting) bounded_subset f' image_subsetI s')
+    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
+      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"] by (auto simp: o_def)
def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
using r1 and r2 unfolding r_def o_def subseq_def by auto
moreover
@@ -3289,11 +3305,11 @@

instance euclidean_space \<subseteq> heine_borel
proof
-  fix s :: "'a set" and f :: "nat \<Rightarrow> 'a"
-  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+  fix f :: "nat \<Rightarrow> 'a"
+  assume f: "bounded (range f)"
then obtain l::'a and r where r: "subseq r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
-    using compact_lemma [OF s f] by blast
+    using compact_lemma [OF f] by blast
{ fix e::real assume "e>0"
hence "0 < e / real_of_nat DIM('a)" by (auto intro!: divide_pos_pos DIM_positive)
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"
@@ -3338,19 +3354,16 @@

instance prod :: (heine_borel, heine_borel) heine_borel
proof
-  fix s :: "('a * 'b) set" and f :: "nat \<Rightarrow> 'a * 'b"
-  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
-  from s have s1: "bounded (fst ` s)" by (rule bounded_fst)
-  from f have f1: "\<forall>n. fst (f n) \<in> fst ` s" by simp
-  obtain l1 r1 where r1: "subseq r1"
-    and l1: "((\<lambda>n. fst (f (r1 n))) ---> l1) sequentially"
-    using bounded_imp_convergent_subsequence [OF s1 f1]
-    unfolding o_def by fast
-  from s have s2: "bounded (snd ` s)" by (rule bounded_snd)
-  from f have f2: "\<forall>n. snd (f (r1 n)) \<in> snd ` s" by simp
+  fix f :: "nat \<Rightarrow> 'a \<times> 'b"
+  assume f: "bounded (range f)"
+  from f have s1: "bounded (range (fst \<circ> f))" unfolding image_comp by (rule bounded_fst)
+  obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) ----> l1"
+    using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
+  from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
+    by (auto simp add: image_comp intro: bounded_snd bounded_subset)
obtain l2 r2 where r2: "subseq r2"
and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially"
-    using bounded_imp_convergent_subsequence [OF s2 f2]
+    using bounded_imp_convergent_subsequence [OF s2]
unfolding o_def by fast
have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .```