# HG changeset patch
# User huffman
# Date 1323094215 -3600
# Node ID 714100f5fda4949be68dcd0411771977cfae4bcc
# Parent  6c340de26a0db13d1aa941bf4d8af0f0a48e1dea
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead

diff -r 6c340de26a0d -r 714100f5fda4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 07 10:50:30 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 05 15:10:15 2011 +0100
@@ -303,20 +303,28 @@
   cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
   "cball x e = {y. dist x y \<le> e}"
 
-lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
-lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
-
-lemma mem_ball_0 [simp]:
+lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
+  by (simp add: ball_def)
+
+lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
+  by (simp add: cball_def)
+
+lemma mem_ball_0:
   fixes x :: "'a::real_normed_vector"
   shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
   by (simp add: dist_norm)
 
-lemma mem_cball_0 [simp]:
+lemma mem_cball_0:
   fixes x :: "'a::real_normed_vector"
   shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
   by (simp add: dist_norm)
 
-lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e"  by simp
+lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e"
+  by simp
+
+lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
+  by simp
+
 lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
 lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
 lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
@@ -344,7 +352,6 @@
   apply (erule_tac x="xa" in allE)
   by arith
 
-lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self)
 lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
   unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..