# HG changeset patch # User huffman # Date 1312863472 25200 # Node ID 5469da57ab773c235c013201ec42df8de64493a8 # Parent 730f7cced3a6ab5b0270f29f6f2419c3c3fdcd8c instance real_basis_with_inner < perfect_space diff -r 730f7cced3a6 -r 5469da57ab77 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 19:26:53 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 21:17:52 2011 -0700 @@ -473,29 +473,15 @@ using islimpt_UNIV [of x] by (simp add: islimpt_approachable) -instance real :: perfect_space -apply default -apply (rule islimpt_approachable [THEN iffD2]) -apply (clarify, rule_tac x="x + e/2" in bexI) -apply (auto simp add: dist_norm) -done - -instance euclidean_space \ perfect_space -proof fix x::'a +instance real_basis_with_inner \ perfect_space +proof + fix x :: 'a { fix e :: real assume "0 < e" - def a \ "x $$ 0" - have "a islimpt UNIV" by (rule islimpt_UNIV) - with `0 < e` obtain b where "b \ a" and "dist b a < e" - unfolding islimpt_approachable by auto - def y \ "\\ i. if i = 0 then b else x$$i :: 'a" - from `b \ a` have "y \ x" unfolding a_def y_def apply(subst euclidean_eq) apply safe - apply(erule_tac x=0 in allE) using DIM_positive[where 'a='a] by auto - - have *:"(\i) = (\i\{0}. (dist (y $$ i) (x $$ i))\)" - apply(rule setsum_mono_zero_right) unfolding y_def by auto - from `dist b a < e` have "dist y x < e" - apply(subst euclidean_dist_l2) - unfolding setL2_def * unfolding y_def a_def using `0 < e` by auto + def y \ "x + scaleR (e/2) (sgn (basis 0))" + from `0 < e` have "y \ x" + unfolding y_def by (simp add: sgn_zero_iff basis_eq_0_iff DIM_positive) + from `0 < e` have "dist y x < e" + unfolding y_def by (simp add: dist_norm norm_sgn) from `y \ x` and `dist y x < e` have "\y\UNIV. y \ x \ dist y x < e" by auto }