src/HOL/Real_Vector_Spaces.thy

 by (subst of_real_numeral [symmetric], subst norm_of_real, simp)
 
 lemma norm_neg_numeral [simp]:
   "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
 by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
+
+lemma norm_of_real_add1 [simp]:
+     "norm (of_real x + 1 :: 'a :: real_normed_div_algebra) = abs (x + 1)"
+  by (metis norm_of_real of_real_1 of_real_add)
+
+lemma norm_of_real_addn [simp]:
+     "norm (of_real x + numeral b :: 'a :: real_normed_div_algebra) = abs (x + numeral b)"
+  by (metis norm_of_real of_real_add of_real_numeral)
 
 lemma norm_of_int [simp]:
   "norm (of_int z::'a::real_normed_algebra_1) = \<bar>of_int z\<bar>"
 by (subst of_real_of_int_eq [symmetric], rule norm_of_real)
 

   by (cases "0::real" x rule: linorder_cases) simp_all
 
 lemma norm_conv_dist: "norm x = dist x 0"
   unfolding dist_norm by simp
 
+declare norm_conv_dist [symmetric, 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 -

   fix e :: real assume e: "e > 0"
   fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
   have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
   also note n
   finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
-    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
+    by (simp add: divide_simps mult.commute norm_divide)
 qed
 
 lemma (in metric_space) complete_def:
   shows "complete S = (\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l))"
   unfolding complete_uniform