src/HOL/Real_Vector_Spaces.thy

 proof -
   have "norm (- (b - a)) = norm (b - a)"
     by (rule norm_minus_cancel)
   thus ?thesis by simp
 qed
+
+lemma norm_uminus_minus: "norm (-x - y :: 'a :: real_normed_vector) = norm (x + y)"
+  by (subst (2) norm_minus_cancel[symmetric], subst minus_add_distrib) simp
 
 lemma norm_triangle_ineq2:
   fixes a b :: "'a::real_normed_vector"
   shows "norm a - norm b \<le> norm (a - b)"
 proof -

   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)
   
+lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: real_normed_algebra_1) = of_int \<bar>m - n\<bar>"
+proof -
+  have "dist (of_int m) (of_int n :: 'a) = dist (of_int m :: 'a) (of_int m - (of_int (m - n)))"
+    by simp
+  also have "\<dots> = of_int \<bar>m - n\<bar>" by (subst dist_diff, subst norm_of_int) simp
+  finally show ?thesis .
+qed
+
+lemma dist_of_nat: 
+  "dist (of_nat m) (of_nat n :: 'a :: real_normed_algebra_1) = of_int \<bar>int m - int n\<bar>"
+  by (subst (1 2) of_int_of_nat_eq [symmetric]) (rule dist_of_int)
+  
 subsection \<open>Bounded Linear and Bilinear Operators\<close>
 
 locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
   assumes scaleR: "f (scaleR r x) = scaleR r (f x)"