# HG changeset patch
# User huffman
# Date 1244010952 25200
# Node ID 1f72869f1a2e4a77624001fe81c39a3cc757f027
# Parent  05d2eddc5d4173b6140d8429b0053ace85f24d11
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair

diff -r 05d2eddc5d41 -r 1f72869f1a2e src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Jun 02 23:31:03 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Tue Jun 02 23:35:52 2009 -0700
@@ -71,6 +71,123 @@
 
 end
 
+subsection {* Continuity of operations *}
+
+lemma dist_fst_le: "dist (fst x) (fst y) \<le> dist x y"
+unfolding dist_prod_def by simp
+
+lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
+unfolding dist_prod_def by simp
+
+lemma tendsto_fst:
+  assumes "tendsto f a net"
+  shows "tendsto (\<lambda>x. fst (f x)) (fst a) net"
+proof (rule tendstoI)
+  fix r :: real assume "0 < r"
+  have "eventually (\<lambda>x. dist (f x) a < r) net"
+    using `tendsto f a net` `0 < r` by (rule tendstoD)
+  thus "eventually (\<lambda>x. dist (fst (f x)) (fst a) < r) net"
+    by (rule eventually_elim1)
+       (rule le_less_trans [OF dist_fst_le])
+qed
+
+lemma tendsto_snd:
+  assumes "tendsto f a net"
+  shows "tendsto (\<lambda>x. snd (f x)) (snd a) net"
+proof (rule tendstoI)
+  fix r :: real assume "0 < r"
+  have "eventually (\<lambda>x. dist (f x) a < r) net"
+    using `tendsto f a net` `0 < r` by (rule tendstoD)
+  thus "eventually (\<lambda>x. dist (snd (f x)) (snd a) < r) net"
+    by (rule eventually_elim1)
+       (rule le_less_trans [OF dist_snd_le])
+qed
+
+lemma tendsto_Pair:
+  assumes "tendsto X a net" and "tendsto Y b net"
+  shows "tendsto (\<lambda>i. (X i, Y i)) (a, b) net"
+proof (rule tendstoI)
+  fix r :: real assume "0 < r"
+  then have "0 < r / sqrt 2" (is "0 < ?s")
+    by (simp add: divide_pos_pos)
+  have "eventually (\<lambda>i. dist (X i) a < ?s) net"
+    using `tendsto X a net` `0 < ?s` by (rule tendstoD)
+  moreover
+  have "eventually (\<lambda>i. dist (Y i) b < ?s) net"
+    using `tendsto Y b net` `0 < ?s` by (rule tendstoD)
+  ultimately
+  show "eventually (\<lambda>i. dist (X i, Y i) (a, b) < r) net"
+    by (rule eventually_elim2)
+       (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
+qed
+
+lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_fst)
+
+lemma LIMSEQ_snd: "(X ----> a) \<Longrightarrow> (\<lambda>n. snd (X n)) ----> snd a"
+unfolding LIMSEQ_conv_tendsto by (rule tendsto_snd)
+
+lemma LIMSEQ_Pair:
+  assumes "X ----> a" and "Y ----> b"
+  shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
+using assms unfolding LIMSEQ_conv_tendsto
+by (rule tendsto_Pair)
+
+lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
+unfolding LIM_conv_tendsto by (rule tendsto_fst)
+
+lemma LIM_snd: "f -- x --> a \<Longrightarrow> (\<lambda>x. snd (f x)) -- x --> snd a"
+unfolding LIM_conv_tendsto by (rule tendsto_snd)
+
+lemma LIM_Pair:
+  assumes "f -- x --> a" and "g -- x --> b"
+  shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
+using assms unfolding LIM_conv_tendsto
+by (rule tendsto_Pair)
+
+lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
+unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
+
+lemma Cauchy_snd: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. snd (X n))"
+unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le])
+
+lemma Cauchy_Pair:
+  assumes "Cauchy X" and "Cauchy Y"
+  shows "Cauchy (\<lambda>n. (X n, Y n))"
+proof (rule metric_CauchyI)
+  fix r :: real assume "0 < r"
+  then have "0 < r / sqrt 2" (is "0 < ?s")
+    by (simp add: divide_pos_pos)
+  obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
+    using metric_CauchyD [OF `Cauchy X` `0 < ?s`] ..
+  obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
+    using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] ..
+  have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r"
+    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
+  then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
+qed
+
+lemma isCont_Pair [simp]:
+  "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
+  unfolding isCont_def by (rule LIM_Pair)
+
+subsection {* Product is a complete metric space *}
+
+instance "*" :: (complete_space, complete_space) complete_space
+proof
+  fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
+  have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
+    using Cauchy_fst [OF `Cauchy X`]
+    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
+  have 2: "(\<lambda>n. snd (X n)) ----> lim (\<lambda>n. snd (X n))"
+    using Cauchy_snd [OF `Cauchy X`]
+    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
+  have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
+    using LIMSEQ_Pair [OF 1 2] by simp
+  then show "convergent X"
+    by (rule convergentI)
+qed
+
 subsection {* Product is a normed vector space *}
 
 instantiation
@@ -113,6 +230,8 @@
 
 end
 
+instance "*" :: (banach, banach) banach ..
+
 subsection {* Product is an inner product space *}
 
 instantiation "*" :: (real_inner, real_inner) real_inner
@@ -149,7 +268,7 @@
 
 end
 
-subsection {* Pair operations are linear and continuous *}
+subsection {* Pair operations are linear *}
 
 interpretation fst: bounded_linear fst
   apply (unfold_locales)
@@ -201,80 +320,6 @@
   then show "\<exists>K. \<forall>x. norm (f x, g x) \<le> norm x * K" ..
 qed
 
-text {*
-  TODO: The "tendsto" notion generalizes LIM and LIMSEQ.
-  But the Cauchy proof still requires a lot of duplication.
-  Is there a good way to factor out the common parts?
-*}
-
-lemma tendsto_Pair:
-  assumes "tendsto X a net" and "tendsto Y b net"
-  shows "tendsto (\<lambda>i. (X i, Y i)) (a, b) net"
-proof (rule tendstoI)
-  fix r :: real assume "0 < r"
-  then have "0 < r / sqrt 2" (is "0 < ?s")
-    by (simp add: divide_pos_pos)
-  have "eventually (\<lambda>i. dist (X i) a < ?s) net"
-    using `tendsto X a net` `0 < ?s` by (rule tendstoD)
-  moreover
-  have "eventually (\<lambda>i. dist (Y i) b < ?s) net"
-    using `tendsto Y b net` `0 < ?s` by (rule tendstoD)
-  ultimately
-  show "eventually (\<lambda>i. dist (X i, Y i) (a, b) < r) net"
-    by (rule eventually_elim2)
-       (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
-qed
-
-lemma LIMSEQ_Pair:
-  assumes "X ----> a" and "Y ----> b"
-  shows "(\<lambda>n. (X n, Y n)) ----> (a, b)"
-using assms unfolding LIMSEQ_conv_tendsto
-by (rule tendsto_Pair)
-
-lemma LIM_Pair:
-  assumes "f -- x --> a" and "g -- x --> b"
-  shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
-using assms unfolding LIM_conv_tendsto
-by (rule tendsto_Pair)
-
-lemma Cauchy_Pair:
-  assumes "Cauchy X" and "Cauchy Y"
-  shows "Cauchy (\<lambda>n. (X n, Y n))"
-proof (rule metric_CauchyI)
-  fix r :: real assume "0 < r"
-  then have "0 < r / sqrt 2" (is "0 < ?s")
-    by (simp add: divide_pos_pos)
-  obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
-    using metric_CauchyD [OF `Cauchy X` `0 < ?s`] ..
-  obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
-    using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] ..
-  have "\<forall>m\<ge>max M N. \<forall>n\<ge>max M N. dist (X m, Y m) (X n, Y n) < r"
-    using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
-  then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
-qed
-
-lemma isCont_Pair [simp]:
-  "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
-  unfolding isCont_def by (rule LIM_Pair)
-
-
-subsection {* Product is a complete vector space *}
-
-instance "*" :: (banach, banach) banach
-proof
-  fix X :: "nat \<Rightarrow> 'a \<times> 'b" assume "Cauchy X"
-  have 1: "(\<lambda>n. fst (X n)) ----> lim (\<lambda>n. fst (X n))"
-    using fst.Cauchy [OF `Cauchy X`]
-    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
-  have 2: "(\<lambda>n. snd (X n)) ----> lim (\<lambda>n. snd (X n))"
-    using snd.Cauchy [OF `Cauchy X`]
-    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
-  have "X ----> (lim (\<lambda>n. fst (X n)), lim (\<lambda>n. snd (X n)))"
-    using LIMSEQ_Pair [OF 1 2] by simp
-  then show "convergent X"
-    by (rule convergentI)
-qed
-
 subsection {* Frechet derivatives involving pairs *}
 
 lemma FDERIV_Pair: