1.1 --- a/src/HOL/NthRoot.thy	Tue May 06 23:35:24 2014 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Wed May 07 12:25:35 2014 +0200
     1.3 @@ -374,12 +374,18 @@
     1.4  lemma real_sqrt_one [simp]: "sqrt 1 = 1"
     1.5  unfolding sqrt_def by (rule real_root_one [OF pos2])
     1.6  
     1.7 +lemma real_sqrt_four [simp]: "sqrt 4 = 2"
     1.8 +  using real_sqrt_abs[of 2] by simp
     1.9 +
    1.10  lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
    1.11  unfolding sqrt_def by (rule real_root_minus)
    1.12  
    1.13  lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
    1.14  unfolding sqrt_def by (rule real_root_mult)
    1.15  
    1.16 +lemma real_sqrt_mult_self[simp]: "sqrt a * sqrt a = \<bar>a\<bar>"
    1.17 +  using real_sqrt_abs[of a] unfolding power2_eq_square real_sqrt_mult .
    1.18 +
    1.19  lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
    1.20  unfolding sqrt_def by (rule real_root_inverse)
    1.21