# HG changeset patch
# User huffman
# Date 1244186969 25200
# Node ID d0ffa8fad5bbbffd6bac43b50ffaadce83dc829d
# Parent  27e00c983b7bce34bf2df0d9691d016ebc699b10# Parent  4fa98c1df7ba7cbd4c47b74ca9276579a026fe34
merged

diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -39,7 +39,9 @@
 
 lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
 
-lemma vector_unminus_smult[simp]: "(-1::real) *s x = -x" unfolding pth_3[symmetric] by simp
+lemma vector_unminus_smult[simp]: "(-1::real) *s x = -x"
+  unfolding vector_sneg_minus1 by simp
+  (* TODO: move to Euclidean_Space.thy *)
 
 lemma setsum_delta_notmem: assumes "x\<notin>s"
   shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
@@ -302,7 +304,7 @@
 	apply(rule_tac x="\<lambda>x. (if x=a then v else 0) + u x" in exI)
 	unfolding setsum_clauses(2)[OF `?as`]  apply simp
 	unfolding vector_sadd_rdistrib and setsum_addf 
-	unfolding vu and * and pth_4(1)
+	unfolding vu and * and vector_smult_lzero
 	by (auto simp add: setsum_delta[OF `?as`])
     next
       case False 
@@ -1178,7 +1180,8 @@
       unfolding setsum_addf wv(1) setsum_right_distrib[THEN sym] obt(5) by auto
     moreover have "(\<Sum>v\<in>s. u v *s v + (t * w v) *s v) - (u a *s a + (t * w a) *s a) = y" 
       unfolding setsum_addf obt(6) vector_smult_assoc[THEN sym] setsum_cmul wv(4)
-      by (metis diff_0_right a(2) pth_5 pth_8 pth_d vector_mul_eq_0)
+      using a(2) [THEN eq_neg_iff_add_eq_0 [THEN iffD2]]
+      by (simp add: vector_smult_lneg)
     ultimately have "?P (n - 1)" apply(rule_tac x="(s - {a})" in exI)
       apply(rule_tac x="\<lambda>v. u v + t * w v" in exI) using obt(1-3) and t and a by (auto simp add: *)
     thus False using smallest[THEN spec[where x="n - 1"]] by auto qed
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -1060,54 +1060,103 @@
 
 subsection{* General linear decision procedure for normed spaces. *}
 
-lemma norm_cmul_rule_thm: "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(c *s x)"
-  apply (clarsimp simp add: norm_mul)
-  apply (rule mult_mono1)
-  apply simp_all
+lemma norm_cmul_rule_thm:
+  fixes x :: "'a::real_normed_vector"
+  shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
+  unfolding norm_scaleR
+  apply (erule mult_mono1)
+  apply simp
   done
 
   (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
-lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n::finite) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"
-  apply (rule norm_triangle_le) by simp
+lemma norm_add_rule_thm:
+  fixes x1 x2 :: "'a::real_normed_vector"
+  shows "norm x1 \<le> b1 \<Longrightarrow> norm x2 \<le> b2 \<Longrightarrow> norm (x1 + x2) \<le> b1 + b2"
+  by (rule order_trans [OF norm_triangle_ineq add_mono])
 
 lemma ge_iff_diff_ge_0: "(a::'a::ordered_ring) \<ge> b == a - b \<ge> 0"
   by (simp add: ring_simps)
 
-lemma pth_1: "(x::real^'n) == 1 *s x" by (simp only: vector_smult_lid)
-lemma pth_2: "x - (y::real^'n) == x + -y" by (atomize (full)) simp
-lemma pth_3: "(-x::real^'n) == -1 *s x" by vector
-lemma pth_4: "0 *s (x::real^'n) == 0" "c *s 0 = (0::real ^ 'n)" by vector+
-lemma pth_5: "c *s (d *s x) == (c * d) *s (x::real ^ 'n)" by (atomize (full)) vector
-lemma pth_6: "(c::real) *s (x + y) == c *s x + c *s y" by (atomize (full)) (vector ring_simps)
-lemma pth_7: "0 + x == (x::real^'n)" "x + 0 == x" by simp_all
-lemma pth_8: "(c::real) *s x + d *s x == (c + d) *s x" by (atomize (full)) (vector ring_simps)
-lemma pth_9: "((c::real) *s x + z) + d *s x == (c + d) *s x + z"
-  "c *s x + (d *s x + z) == (c + d) *s x + z"
-  "(c *s x + w) + (d *s x + z) == (c + d) *s x + (w + z)" by ((atomize (full)), vector ring_simps)+
-lemma pth_a: "(0::real) *s x + y == y" by (atomize (full)) vector
-lemma pth_b: "(c::real) *s x + d *s y == c *s x + d *s y"
-  "(c *s x + z) + d *s y == c *s x + (z + d *s y)"
-  "c *s x + (d *s y + z) == c *s x + (d *s y + z)"
-  "(c *s x + w) + (d *s y + z) == c *s x + (w + (d *s y + z))"
-  by ((atomize (full)), vector)+
-lemma pth_c: "(c::real) *s x + d *s y == d *s y + c *s x"
-  "(c *s x + z) + d *s y == d *s y + (c *s x + z)"
-  "c *s x + (d *s y + z) == d *s y + (c *s x + z)"
-  "(c *s x + w) + (d *s y + z) == d *s y + ((c *s x + w) + z)" by ((atomize (full)), vector)+
-lemma pth_d: "x + (0::real ^'n) == x" by (atomize (full)) vector
-
-lemma norm_imp_pos_and_ge: "norm (x::real ^ _) == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
-  by (atomize) (auto simp add: norm_ge_zero)
+lemma pth_1:
+  fixes x :: "'a::real_normed_vector"
+  shows "x == scaleR 1 x" by simp
+
+lemma pth_2:
+  fixes x :: "'a::real_normed_vector"
+  shows "x - y == x + -y" by (atomize (full)) simp
+
+lemma pth_3:
+  fixes x :: "'a::real_normed_vector"
+  shows "- x == scaleR (-1) x" by simp
+
+lemma pth_4:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR 0 x == 0" and "scaleR c 0 = (0::'a)" by simp_all
+
+lemma pth_5:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c (scaleR d x) == scaleR (c * d) x" by simp
+
+lemma pth_6:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c (x + y) == scaleR c x + scaleR c y"
+  by (simp add: scaleR_right_distrib)
+
+lemma pth_7:
+  fixes x :: "'a::real_normed_vector"
+  shows "0 + x == x" and "x + 0 == x" by simp_all
+
+lemma pth_8:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR c x + scaleR d x == scaleR (c + d) x"
+  by (simp add: scaleR_left_distrib)
+
+lemma pth_9:
+  fixes x :: "'a::real_normed_vector" shows
+  "(scaleR c x + z) + scaleR d x == scaleR (c + d) x + z"
+  "scaleR c x + (scaleR d x + z) == scaleR (c + d) x + z"
+  "(scaleR c x + w) + (scaleR d x + z) == scaleR (c + d) x + (w + z)"
+  by (simp_all add: algebra_simps)
+
+lemma pth_a:
+  fixes x :: "'a::real_normed_vector"
+  shows "scaleR 0 x + y == y" by simp
+
+lemma pth_b:
+  fixes x :: "'a::real_normed_vector" shows
+  "scaleR c x + scaleR d y == scaleR c x + scaleR d y"
+  "(scaleR c x + z) + scaleR d y == scaleR c x + (z + scaleR d y)"
+  "scaleR c x + (scaleR d y + z) == scaleR c x + (scaleR d y + z)"
+  "(scaleR c x + w) + (scaleR d y + z) == scaleR c x + (w + (scaleR d y + z))"
+  by (simp_all add: algebra_simps)
+
+lemma pth_c:
+  fixes x :: "'a::real_normed_vector" shows
+  "scaleR c x + scaleR d y == scaleR d y + scaleR c x"
+  "(scaleR c x + z) + scaleR d y == scaleR d y + (scaleR c x + z)"
+  "scaleR c x + (scaleR d y + z) == scaleR d y + (scaleR c x + z)"
+  "(scaleR c x + w) + (scaleR d y + z) == scaleR d y + ((scaleR c x + w) + z)"
+  by (simp_all add: algebra_simps)
+
+lemma pth_d:
+  fixes x :: "'a::real_normed_vector"
+  shows "x + 0 == x" by simp
+
+lemma norm_imp_pos_and_ge:
+  fixes x :: "'a::real_normed_vector"
+  shows "norm x == n \<Longrightarrow> norm x \<ge> 0 \<and> n \<ge> norm x"
+  by atomize auto
 
 lemma real_eq_0_iff_le_ge_0: "(x::real) = 0 == x \<ge> 0 \<and> -x \<ge> 0" by arith
 
 lemma norm_pths:
-  "(x::real ^'n::finite) = y \<longleftrightarrow> norm (x - y) \<le> 0"
+  fixes x :: "'a::real_normed_vector" shows
+  "x = y \<longleftrightarrow> norm (x - y) \<le> 0"
   "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   using norm_ge_zero[of "x - y"] by auto
 
 lemma vector_dist_norm:
-  fixes x y :: "real ^ _"
+  fixes x :: "'a::real_normed_vector"
   shows "dist x y = norm (x - y)"
   by (rule dist_norm)
 
@@ -1117,7 +1166,6 @@
 *} "Proves simple linear statements about vector norms"
 
 
-
 text{* Hence more metric properties. *}
 
 lemma dist_triangle_alt:
@@ -1158,7 +1206,7 @@
 lemma dist_triangle_add:
   fixes x y x' y' :: "'a::real_normed_vector"
   shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
-unfolding dist_norm by (rule norm_diff_triangle_ineq)
+  by norm
 
 lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
   unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
@@ -1166,7 +1214,7 @@
 lemma dist_triangle_add_half:
   fixes x x' y y' :: "'a::real_normed_vector"
   shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
-by (rule le_less_trans [OF dist_triangle_add], simp)
+  by norm
 
 lemma setsum_component [simp]:
   fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -10,6 +10,14 @@
 
 subsection {* Real inner product spaces *}
 
+text {* Temporarily relax constraints for @{term dist} and @{term norm}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"}) *}
+
 class real_inner = real_vector + sgn_div_norm + dist_norm + topo_dist +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
@@ -116,6 +124,14 @@
 
 end
 
+text {* Re-enable constraints for @{term dist} and @{term norm}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
+
 interpretation inner:
   bounded_bilinear "inner::'a::real_inner \<Rightarrow> 'a \<Rightarrow> real"
 proof
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -1058,26 +1058,25 @@
   "trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net"
 
 lemma trivial_limit_within:
-  fixes a :: "'a::metric_space"
   shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
 proof
   assume "trivial_limit (at a within S)"
   thus "\<not> a islimpt S"
     unfolding trivial_limit_def
     unfolding Rep_net_within Rep_net_at
-    unfolding islimpt_approachable_le dist_nz
-    apply (clarsimp simp add: not_le expand_set_eq)
-    apply (rule_tac x="r/2" in exI, clarsimp)
-    apply (drule_tac x=x' in spec, simp)
+    unfolding islimpt_def open_def [symmetric]
+    apply (clarsimp simp add: expand_set_eq)
+    apply (rename_tac T, rule_tac x=T in exI)
+    apply (clarsimp, drule_tac x=y in spec, simp)
     done
 next
   assume "\<not> a islimpt S"
   thus "trivial_limit (at a within S)"
     unfolding trivial_limit_def
     unfolding Rep_net_within Rep_net_at
-    unfolding islimpt_approachable_le dist_nz
-    apply (clarsimp simp add: image_image not_le)
-    apply (rule_tac x=e in image_eqI)
+    unfolding islimpt_def open_def [symmetric]
+    apply (clarsimp simp add: image_image)
+    apply (rule_tac x=T in image_eqI)
     apply (auto simp add: expand_set_eq)
     done
 qed
@@ -1105,9 +1104,9 @@
 
 subsection{* Some property holds "sufficiently close" to the limit point. *}
 
-lemma eventually_at:
+lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
   "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_def Rep_net_at dist_nz by auto
+unfolding eventually_at dist_nz by auto
 
 lemma eventually_at_infinity:
   "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
@@ -1212,35 +1211,31 @@
 
 text{* The expected monotonicity property. *}
 
-lemma Lim_within_empty: "(f ---> l) (at x within {})"
-  by (simp add: Lim_within_le)
-
-lemma Lim_within_subset: "(f ---> l) (at a within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at a within T)"
-  apply (auto simp add: Lim_within_le)
-  by (metis subset_eq)
-
-lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
-  shows "(f ---> l) (at x within (S \<union> T))"
-proof-
-  { fix e::real assume "e>0"
-    obtain d1 where d1:"d1>0" "\<forall>xa\<in>T. 0 < dist xa x \<and> dist xa x < d1 \<longrightarrow> dist (f xa) l < e" using assms unfolding Lim_within using `e>0` by auto
-    obtain d2 where d2:"d2>0" "\<forall>xa\<in>S. 0 < dist xa x \<and> dist xa x < d2 \<longrightarrow> dist (f xa) l < e" using assms unfolding Lim_within using `e>0` by auto
-    have "\<exists>d>0. \<forall>xa\<in>S \<union> T. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) l < e" using d1 d2
-      by (rule_tac x="min d1 d2" in exI)auto
-  }
-  thus ?thesis unfolding Lim_within by auto
-qed
+lemma Lim_within_empty: "(f ---> l) (net within {})"
+  unfolding tendsto_def Limits.eventually_within by simp
+
+lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+  unfolding tendsto_def Limits.eventually_within
+  by (auto elim!: eventually_elim1)
+
+lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
+  shows "(f ---> l) (net within (S \<union> T))"
+  using assms unfolding tendsto_def Limits.eventually_within
+  apply clarify
+  apply (drule spec, drule (1) mp)+
+  apply (auto elim: eventually_elim2)
+  done
 
 lemma Lim_Un_univ:
- "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
-        ==> (f ---> l) (at x)"
+ "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow>  S \<union> T = UNIV
+        ==> (f ---> l) net"
   by (metis Lim_Un within_UNIV)
 
 text{* Interrelations between restricted and unrestricted limits. *}
 
-lemma Lim_at_within: "(f ---> l)(at a) ==> (f ---> l)(at a within S)"
-  apply (simp add: Lim_at Lim_within)
-  by metis
+lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
+  unfolding tendsto_def Limits.eventually_within
+  by (auto elim!: eventually_elim1)
 
 lemma Lim_within_open:
   assumes"a \<in> S" "open S"
@@ -1248,18 +1243,23 @@
 proof
   assume ?lhs
   { fix e::real assume "e>0"
-    obtain d  where d:  "d >0" "\<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?lhs` `e>0` unfolding Lim_within by auto
-    obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms  unfolding open_dist by auto
-    from d d' have "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" by (rule_tac x= "min d d'" in exI)auto
+    have "eventually (\<lambda>x. dist (f x) l < e) (at a within S)"
+      using `?lhs` `e>0` by (rule tendstoD)
+    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
+      unfolding Limits.eventually_within .
+    then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> dist (f x) l < e"
+      unfolding eventually_at_topological open_def by fast
+    hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> dist (f x) l < e"
+      using assms by auto
+    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
+      by fast
+    hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
+      unfolding eventually_at_topological open_def Bex_def .
   }
-  thus ?rhs unfolding Lim_at by auto
+  thus ?rhs by (rule tendstoI)
 next
   assume ?rhs
-  { fix e::real assume "e>0"
-    then obtain d where "d>0" and d:"\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?rhs` unfolding Lim_at by auto
-    hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `d>0` by auto
-  }
-  thus ?lhs using Lim_at_within[of f l a S] by (auto simp add: Lim_at)
+  thus ?lhs by (rule Lim_at_within)
 qed
 
 text{* Another limit point characterization. *}
@@ -1619,7 +1619,7 @@
 
 definition
   netlimit :: "'a::metric_space net \<Rightarrow> 'a" where
-  "netlimit net = (SOME a. \<forall>r>0. \<exists>A\<in>Rep_net net. \<forall>x\<in>A. dist x a < r)"
+  "netlimit net = (SOME a. \<forall>r>0. eventually (\<lambda>x. dist x a < r) net)"
 
 lemma dist_triangle3:
   fixes x y :: "'a::metric_space"
@@ -1632,7 +1632,7 @@
   shows "netlimit (at a within S) = a"
 using assms
 apply (simp add: trivial_limit_within)
-apply (simp add: netlimit_def Rep_net_within Rep_net_at)
+apply (simp add: netlimit_def eventually_within zero_less_dist_iff)
 apply (rule some_equality, fast)
 apply (rename_tac b)
 apply (rule ccontr)
@@ -1641,7 +1641,8 @@
 apply (simp only: islimpt_approachable)
 apply (drule_tac x="min r (dist b a / 2)" in spec, drule mp, simp add: dist_nz)
 apply (clarify)
-apply (drule_tac x=x' in bspec, simp add: dist_nz)
+apply (drule_tac x=x' in bspec, simp)
+apply (drule mp, simp)
 apply (subgoal_tac "dist b a < dist b a / 2 + dist b a / 2", simp)
 apply (rule le_less_trans [OF dist_triangle3])
 apply (erule add_strict_mono)
@@ -1696,6 +1697,7 @@
 text{* Common case assuming being away from some crucial point like 0. *}
 
 lemma Lim_transform_away_within:
+  fixes a b :: "'a::metric_space"
   assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and "(f ---> l) (at a within S)"
   shows "(g ---> l) (at a within S)"
@@ -1706,6 +1708,7 @@
 qed
 
 lemma Lim_transform_away_at:
+  fixes a b :: "'a::metric_space"
   assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and fl: "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
@@ -1715,6 +1718,7 @@
 text{* Alternatively, within an open set. *}
 
 lemma Lim_transform_within_open:
+  fixes a :: "'a::metric_space"
   assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
 proof-
@@ -1729,10 +1733,12 @@
 (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
 
 lemma Lim_cong_within[cong add]:
+  fixes a :: "'a::metric_space" shows
  "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
   by (simp add: Lim_within dist_nz[symmetric])
 
 lemma Lim_cong_at[cong add]:
+  fixes a :: "'a::metric_space" shows
  "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
   by (simp add: Lim_at dist_nz[symmetric])
 
@@ -1992,7 +1998,9 @@
 
 text{* For points in the interior, localization of limits makes no difference.   *}
 
-lemma eventually_within_interior: assumes "x \<in> interior S"
+lemma eventually_within_interior:
+  fixes x :: "'a::metric_space"
+  assumes "x \<in> interior S"
   shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
 proof-
   from assms obtain e where e:"e>0" "\<forall>y. dist x y < e \<longrightarrow> y \<in> S" unfolding mem_interior ball_def subset_eq by auto
@@ -2004,7 +2012,9 @@
   show "?thesis" by auto
 qed
 
-lemma lim_within_interior: "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
+lemma lim_within_interior:
+  fixes x :: "'a::metric_space"
+  shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
   by (simp add: tendsto_def eventually_within_interior)
 
 lemma netlimit_within_interior:
@@ -3057,7 +3067,7 @@
   (* FIXME: generalize *)
 proof(cases "x islimpt s")
   case True show ?thesis using assms unfolding continuous_def and netlimit_at
-    using Lim_at_within[of f "f x" x s]
+    using Lim_at_within[of f "f x" "at x" s]
     unfolding netlimit_within[unfolded trivial_limit_within not_not, OF True] by blast
 next
   case False thus ?thesis unfolding continuous_def and netlimit_at
@@ -3401,11 +3411,16 @@
   thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
 qed
 
+lemma dist_minus:
+  fixes x y :: "'a::real_normed_vector"
+  shows "dist (- x) (- y) = dist x y"
+  unfolding dist_norm minus_diff_minus norm_minus_cancel ..
+
 lemma uniformly_continuous_on_neg:
   fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
   shows "uniformly_continuous_on s f
          ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
-  using uniformly_continuous_on_cmul[of s f "-1"] unfolding pth_3 by auto
+  unfolding uniformly_continuous_on_def dist_minus .
 
 lemma uniformly_continuous_on_add:
   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
@@ -3735,9 +3750,15 @@
   thus ?thesis unfolding open_dist by auto
 qed
 
+lemma minus_image_eq_vimage:
+  fixes A :: "'a::ab_group_add set"
+  shows "(\<lambda>x. - x) ` A = (\<lambda>x. - x) -` A"
+  by (auto intro!: image_eqI [where f="\<lambda>x. - x"])
+
 lemma open_negations:
   fixes s :: "(real ^ _) set" (* FIXME: generalize *)
-  shows "open s ==> open ((\<lambda> x. -x) ` s)" unfolding pth_3 by auto
+  shows "open s ==> open ((\<lambda> x. -x) ` s)"
+  unfolding vector_sneg_minus1 by auto
 
 lemma open_translation:
   fixes s :: "(real ^ _) set" (* FIXME: generalize *)
@@ -4261,7 +4282,8 @@
   fixes s :: "(real ^ _) set"
   assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
 proof-
-  have "uminus ` s = (\<lambda>x. -1 *s x) ` s" apply auto unfolding image_iff pth_3 by auto
+  have "(\<lambda>x. - x) ` s = (\<lambda>x. (- 1) *s x) ` s"
+    unfolding vector_sneg_minus1 ..
   thus ?thesis using compact_scaling[OF assms, of "-1"] by auto
 qed
 
@@ -4401,7 +4423,8 @@
 lemma closed_negations:
   fixes s :: "(real ^ _) set" (* FIXME: generalize *)
   assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaling[OF assms, of "-1"] unfolding  pth_3 by auto
+  using closed_scaling[OF assms, of "- 1"]
+  unfolding vector_sneg_minus1 by auto
 
 lemma compact_closed_sums:
   fixes s :: "(real ^ _) set"
@@ -5141,11 +5164,10 @@
 text{* Limits relative to a union.                                               *}
 
 lemma Lim_within_union:
- "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
-  (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
-  unfolding Lim_within apply auto apply blast apply blast
-    apply(erule_tac x=e in allE)+ apply auto
-    apply(rule_tac x="min d da" in exI) by auto
+ "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
+  (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
+  unfolding tendsto_def Limits.eventually_within
+  by (auto elim!: eventually_elim1 intro: eventually_conjI)
 
 lemma continuous_on_union:
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Library/normarith.ML	Fri Jun 05 00:29:29 2009 -0700
@@ -49,21 +49,23 @@
  fun int_lincomb_eq l r = Intfunc.is_undefined (int_lincomb_sub l r)
 
 fun vector_lincomb t = case term_of t of 
-   Const(@{const_name plus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) $ _ $ _ =>
+   Const(@{const_name plus}, _) $ _ $ _ =>
     cterm_lincomb_add (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t))
- | Const(@{const_name minus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) $ _ $ _ =>
+ | Const(@{const_name minus}, _) $ _ $ _ =>
     cterm_lincomb_sub (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t))
- | Const(@{const_name vector_scalar_mult},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$_$_ =>
+ | Const(@{const_name scaleR}, _)$_$_ =>
     cterm_lincomb_cmul (dest_ratconst (dest_arg1 t)) (vector_lincomb (dest_arg t))
- | Const(@{const_name uminus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$_ =>
+ | Const(@{const_name uminus}, _)$_ =>
      cterm_lincomb_neg (vector_lincomb (dest_arg t))
- | Const(@{const_name vec},_)$_ => 
+(* FIXME: how should we handle numerals?
+ | Const(@ {const_name vec},_)$_ => 
    let 
      val b = ((snd o HOLogic.dest_number o term_of o dest_arg) t = 0 
                handle TERM _=> false)
    in if b then Ctermfunc.onefunc (t,Rat.one)
       else Ctermfunc.undefined
    end
+*)
  | _ => Ctermfunc.onefunc (t,Rat.one)
 
  fun vector_lincombs ts =
@@ -188,7 +190,7 @@
  val apply_pth5 = rewr_conv @{thm pth_5};
  val apply_pth6 = rewr_conv @{thm pth_6};
  val apply_pth7 = rewrs_conv @{thms pth_7};
- val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm vector_smult_lzero})));
+ val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
  val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv);
  val apply_ptha = rewr_conv @{thm pth_a};
  val apply_pthb = rewrs_conv @{thms pth_b};
@@ -196,9 +198,9 @@
  val apply_pthd = try_conv (rewr_conv @{thm pth_d});
 
 fun headvector t = case t of 
-  Const(@{const_name plus}, Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$
-   (Const(@{const_name vector_scalar_mult}, _)$l$v)$r => v
- | Const(@{const_name vector_scalar_mult}, _)$l$v => v
+  Const(@{const_name plus}, _)$
+   (Const(@{const_name scaleR}, _)$l$v)$r => v
+ | Const(@{const_name scaleR}, _)$l$v => v
  | _ => error "headvector: non-canonical term"
 
 fun vector_cmul_conv ct =
@@ -234,7 +236,7 @@
    val th = Drule.binop_cong_rule p lth rth 
   in fconv_rule (arg_conv vector_add_conv) th end
 
-| Const(@{const_name vector_scalar_mult}, _)$_$_ =>
+| Const(@{const_name scaleR}, _)$_$_ =>
   let 
    val (p,r) = Thm.dest_comb ct
    val rth = Drule.arg_cong_rule p (vector_canon_conv r) 
@@ -245,12 +247,13 @@
 
 | Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct
 
+(* FIXME
 | Const(@{const_name vec},_)$n => 
   let val n = Thm.dest_arg ct
   in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) 
      then reflexive ct else apply_pth1 ct
   end
-
+*)
 | _ => apply_pth1 ct
 
 fun norm_canon_conv ct = case term_of ct of
@@ -266,8 +269,8 @@
   then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq;
 
 local
- val pth_zero = @{thm "norm_0"}
- val tv_n = (hd o tl o dest_ctyp o ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of)
+ val pth_zero = @{thm norm_zero}
+ val tv_n = (ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of)
              pth_zero
  val concl = dest_arg o cprop_of 
  fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 
@@ -327,7 +330,7 @@
         (fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
 
   in RealArith.real_linear_prover translator
-        (map (fn t => instantiate ([(tv_n,(hd o tl o dest_ctyp o ctyp_of_term) t)],[]) pth_zero)
+        (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
             zerodests,
         map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
@@ -350,7 +353,7 @@
   val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
   val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
-  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t
+  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
   val replace_conv = try_conv (rewrs_conv asl)
@@ -391,7 +394,7 @@
 
   fun init_conv ctxt = 
    Simplifier.rewrite (Simplifier.context ctxt 
-     (HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
+     (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths})))
    then_conv field_comp_conv 
    then_conv nnf_conv
 
@@ -409,4 +412,4 @@
    ObjectLogic.full_atomize_tac THEN'
    CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
 
-end;
\ No newline at end of file
+end;
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/Limits.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -109,12 +109,12 @@
   [code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))"
 
 definition
-  at :: "'a::metric_space \<Rightarrow> 'a net" where
-  [code del]: "at a = Abs_net ((\<lambda>r. {x. x \<noteq> a \<and> dist x a < r}) ` {r. 0 < r})"
+  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
+  [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
 
 definition
-  within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
-  [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
+  at :: "'a::topological_space \<Rightarrow> 'a net" where
+  [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
 
 lemma Rep_net_sequentially:
   "Rep_net sequentially = range (\<lambda>n. {n..})"
@@ -125,15 +125,6 @@
 apply (rule_tac x="max m n" in exI, auto)
 done
 
-lemma Rep_net_at:
-  "Rep_net (at a) = ((\<lambda>r. {x. x \<noteq> a \<and> dist x a < r}) ` {r. 0 < r})"
-unfolding at_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, rule_tac x=1 in exI, simp)
-apply (clarsimp, rename_tac r s)
-apply (rule_tac x="min r s" in exI, auto)
-done
-
 lemma Rep_net_within:
   "Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net"
 unfolding within_def
@@ -144,18 +135,41 @@
 apply (clarify, rule_tac x=C in bexI, auto)
 done
 
+lemma Rep_net_at:
+  "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S\<in>topo. a \<in> S})"
+unfolding at_def
+apply (rule Abs_net_inverse')
+apply (rule image_nonempty)
+apply (rule_tac x="UNIV" in exI, simp add: topo_UNIV)
+apply (clarsimp, rename_tac S T)
+apply (rule_tac x="S \<inter> T" in exI, auto simp add: topo_Int)
+done
+
 lemma eventually_sequentially:
   "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
 unfolding eventually_def Rep_net_sequentially by auto
 
-lemma eventually_at:
-  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_def Rep_net_at by auto
-
 lemma eventually_within:
   "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
 unfolding eventually_def Rep_net_within by auto
 
+lemma eventually_at_topological:
+  "eventually P (at a) \<longleftrightarrow> (\<exists>S\<in>topo. a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
+unfolding eventually_def Rep_net_at by auto
+
+lemma eventually_at:
+  fixes a :: "'a::metric_space"
+  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
+unfolding eventually_at_topological topo_dist
+apply safe
+apply fast
+apply (rule_tac x="{x. dist x a < d}" in bexI, simp)
+apply clarsimp
+apply (rule_tac x="d - dist x a" in exI, clarsimp)
+apply (simp only: less_diff_eq)
+apply (erule le_less_trans [OF dist_triangle])
+done
+
 
 subsection {* Boundedness *}
 
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/NSA/NSA.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -12,7 +12,7 @@
 begin
 
 definition
-  hnorm :: "'a::norm star \<Rightarrow> real star" where
+  hnorm :: "'a::real_normed_vector star \<Rightarrow> real star" where
   [transfer_unfold]: "hnorm = *f* norm"
 
 definition
diff -r 4fa98c1df7ba -r d0ffa8fad5bb src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu Jun 04 23:42:11 2009 +0200
+++ b/src/HOL/RealVector.thy	Fri Jun 05 00:29:29 2009 -0700
@@ -733,6 +733,18 @@
     using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
 qed
 
+subsection {* Extra type constraints *}
+
+text {* Only allow @{term dist} in class @{text metric_space}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"}) *}
+
+text {* Only allow @{term norm} in class @{text real_normed_vector}. *}
+
+setup {* Sign.add_const_constraint
+  (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
+
 
 subsection {* Sign function *}