src/HOL/NthRoot.thy
changeset 56889 48a745e1bde7
parent 56536 aefb4a8da31f
child 57155 5c59114ff0cb
--- a/src/HOL/NthRoot.thy	Tue May 06 23:35:24 2014 +0200
+++ b/src/HOL/NthRoot.thy	Wed May 07 12:25:35 2014 +0200
@@ -374,12 +374,18 @@
 lemma real_sqrt_one [simp]: "sqrt 1 = 1"
 unfolding sqrt_def by (rule real_root_one [OF pos2])
 
+lemma real_sqrt_four [simp]: "sqrt 4 = 2"
+  using real_sqrt_abs[of 2] by simp
+
 lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
 unfolding sqrt_def by (rule real_root_minus)
 
 lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
 unfolding sqrt_def by (rule real_root_mult)
 
+lemma real_sqrt_mult_self[simp]: "sqrt a * sqrt a = \<bar>a\<bar>"
+  using real_sqrt_abs[of a] unfolding power2_eq_square real_sqrt_mult .
+
 lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
 unfolding sqrt_def by (rule real_root_inverse)