remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
authorhuffman
Mon Dec 05 15:10:15 2011 +0100 (2011-12-05)
changeset 45776714100f5fda4
parent 45775 6c340de26a0d
child 45777 c36637603821
child 45782 f82020ca3248
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 07 10:50:30 2011 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 05 15:10:15 2011 +0100
     1.3 @@ -303,20 +303,28 @@
     1.4    cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
     1.5    "cball x e = {y. dist x y \<le> e}"
     1.6  
     1.7 -lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
     1.8 -lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
     1.9 -
    1.10 -lemma mem_ball_0 [simp]:
    1.11 +lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
    1.12 +  by (simp add: ball_def)
    1.13 +
    1.14 +lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
    1.15 +  by (simp add: cball_def)
    1.16 +
    1.17 +lemma mem_ball_0:
    1.18    fixes x :: "'a::real_normed_vector"
    1.19    shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
    1.20    by (simp add: dist_norm)
    1.21  
    1.22 -lemma mem_cball_0 [simp]:
    1.23 +lemma mem_cball_0:
    1.24    fixes x :: "'a::real_normed_vector"
    1.25    shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
    1.26    by (simp add: dist_norm)
    1.27  
    1.28 -lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e"  by simp
    1.29 +lemma centre_in_ball: "x \<in> ball x e \<longleftrightarrow> 0 < e"
    1.30 +  by simp
    1.31 +
    1.32 +lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
    1.33 +  by simp
    1.34 +
    1.35  lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
    1.36  lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
    1.37  lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
    1.38 @@ -344,7 +352,6 @@
    1.39    apply (erule_tac x="xa" in allE)
    1.40    by arith
    1.41  
    1.42 -lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self)
    1.43  lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
    1.44    unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
    1.45