src/HOL/Real_Vector_Spaces.thy

--- a/src/HOL/Real_Vector_Spaces.thy	Tue Feb 23 15:49:17 2016 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 24 15:51:01 2016 +0000
@@ -1308,6 +1308,11 @@
 
 declare norm_conv_dist [symmetric, simp]
 
+lemma dist_0_norm [simp]:
+  fixes x :: "'a::real_normed_vector"
+  shows "dist 0 x = norm x"
+unfolding dist_norm by simp
+
 lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
   by (simp_all add: dist_norm)