src/HOL/Real_Vector_Spaces.thy
changeset 62379 340738057c8c
parent 62368 106569399cd6
child 62397 5ae24f33d343
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Feb 19 13:40:50 2016 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 22 14:37:56 2016 +0000
     1.3 @@ -862,6 +862,14 @@
     1.4    "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
     1.5  by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
     1.6  
     1.7 +lemma norm_of_real_add1 [simp]:
     1.8 +     "norm (of_real x + 1 :: 'a :: real_normed_div_algebra) = abs (x + 1)"
     1.9 +  by (metis norm_of_real of_real_1 of_real_add)
    1.10 +
    1.11 +lemma norm_of_real_addn [simp]:
    1.12 +     "norm (of_real x + numeral b :: 'a :: real_normed_div_algebra) = abs (x + numeral b)"
    1.13 +  by (metis norm_of_real of_real_add of_real_numeral)
    1.14 +
    1.15  lemma norm_of_int [simp]:
    1.16    "norm (of_int z::'a::real_normed_algebra_1) = \<bar>of_int z\<bar>"
    1.17  by (subst of_real_of_int_eq [symmetric], rule norm_of_real)
    1.18 @@ -1298,6 +1306,8 @@
    1.19  lemma norm_conv_dist: "norm x = dist x 0"
    1.20    unfolding dist_norm by simp
    1.21  
    1.22 +declare norm_conv_dist [symmetric, simp]
    1.23 +
    1.24  lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
    1.25    by (simp_all add: dist_norm)
    1.26  
    1.27 @@ -1868,7 +1878,7 @@
    1.28    have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
    1.29    also note n
    1.30    finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
    1.31 -    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
    1.32 +    by (simp add: divide_simps mult.commute norm_divide)
    1.33  qed
    1.34  
    1.35  lemma (in metric_space) complete_def: