# HG changeset patch # User immler # Date 1360769707 -3600 # Node ID 3f9dbd2cc4751ae75ccc0d5ed2a8fa0f8b523e72 # Parent 5746e671ea70b30a52428edfeda5b974fe132e24 complete metric for formal power series diff -r 5746e671ea70 -r 3f9dbd2cc475 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Feb 13 16:35:07 2013 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Feb 13 16:35:07 2013 +0100 @@ -3368,4 +3368,80 @@ foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)" by (induct cs arbitrary: c0) (auto simp add: algebra_simps f) +lemma dist_less_imp_nth_equal: + assumes "dist f g < inverse (2 ^ i)" + assumes "j \ i" + shows "f $ j = g $ j" +proof cases + assume "f \ g" + hence "\n. f $ n \ g $ n" by (simp add: fps_eq_iff) + with assms have "i < The (leastP (\n. f $ n \ g $ n))" + by (simp add: split_if_asm dist_fps_def) + moreover + from fps_eq_least_unique[OF `f \ g`] + obtain n where "leastP (\n. f$n \ g$n) n" "The (leastP (\n. f $ n \ g $ n)) = n" by blast + moreover hence "\m. m < n \ f$m = g$m" "f$n \ g$n" + by (auto simp add: leastP_def setge_def) + ultimately show ?thesis using `j \ i` by simp +qed simp + +lemma nth_equal_imp_dist_less: + assumes "\j. j \ i \ f $ j = g $ j" + shows "dist f g < inverse (2 ^ i)" +proof cases + assume "f \ g" + hence "\n. f $ n \ g $ n" by (simp add: fps_eq_iff) + with assms have "dist f g = inverse (2 ^ (The (leastP (\n. f $ n \ g $ n))))" + by (simp add: split_if_asm dist_fps_def) + moreover + from fps_eq_least_unique[OF `f \ g`] + obtain n where "leastP (\n. f$n \ g$n) n" "The (leastP (\n. f $ n \ g $ n)) = n" by blast + with assms have "i < The (leastP (\n. f $ n \ g $ n))" + by (metis (full_types) leastPD1 not_le) + ultimately show ?thesis by simp +qed simp + +lemma dist_less_eq_nth_equal: + shows "dist f g < inverse (2 ^ i) \ (\j \ i. f $ j = g $ j)" + using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast + +instance fps :: (comm_ring_1) complete_space +proof + fix X::"nat \ 'a fps" + assume "Cauchy X" + { + fix i + have "0 < inverse ((2::real)^i)" by simp + from metric_CauchyD[OF `Cauchy X` this] dist_less_imp_nth_equal + have "\M. \m \ M. \j\i. X M $ j = X m $ j" by blast + } + then obtain M where M: "\i. \m \ M i. \j \ i. X (M i) $ j = X m $ j" by metis + hence "\i. \m \ M i. \j \ i. X (M i) $ j = X m $ j" by metis + show "convergent X" + proof (rule convergentI) + show "X ----> Abs_fps (\i. X (M i) $ i)" + unfolding tendsto_iff + proof safe + fix e::real assume "0 < e" + with LIMSEQ_inverse_realpow_zero[of 2, simplified, simplified filterlim_iff, + THEN spec, of "\x. x < e"] + have "eventually (\i. inverse (2 ^ i) < e) sequentially" + by safe (auto simp: eventually_nhds) + then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially) + have "eventually (\x. M i \ x) sequentially" by (auto simp: eventually_sequentially) + thus "eventually (\x. dist (X x) (Abs_fps (\i. X (M i) $ i)) < e) sequentially" + proof eventually_elim + fix x assume "M i \ x" + moreover + have "\j. j \ i \ X (M i) $ j = X (M j) $ j" + using M by (metis nat_le_linear) + ultimately have "dist (X x) (Abs_fps (\j. X (M j) $ j)) < inverse (2 ^ i)" + using M by (force simp: dist_less_eq_nth_equal) + also note `inverse (2 ^ i) < e` + finally show "dist (X x) (Abs_fps (\j. X (M j) $ j)) < e" . + qed + qed + qed +qed + end