# HG changeset patch # User huffman # Date 1173905546 -3600 # Node ID 346729a55460113102e82a248507364be1091c2d # Parent 15d9ed9b505127356e96c1a3f507f78ec60fdc50 move sqrt_divide_self_eq to NthRoot.thy diff -r 15d9ed9b5051 -r 346729a55460 src/HOL/Hyperreal/HTranscendental.thy --- a/src/HOL/Hyperreal/HTranscendental.thy Wed Mar 14 21:40:28 2007 +0100 +++ b/src/HOL/Hyperreal/HTranscendental.thy Wed Mar 14 21:52:26 2007 +0100 @@ -11,25 +11,6 @@ imports Transcendental Integration HSeries begin -text{*really belongs in Transcendental*} -lemma sqrt_divide_self_eq: - assumes nneg: "0 \ x" - shows "sqrt x / x = inverse (sqrt x)" -proof cases - assume "x=0" thus ?thesis by simp -next - assume nz: "x\0" - hence pos: "0 0" by (simp add: divide_inverse nneg nz) - show "inverse (sqrt x) / (sqrt x / x) = 1" - by (simp add: divide_inverse mult_assoc [symmetric] - power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) - qed -qed - - definition exphr :: "real => hypreal" where --{*define exponential function using standard part *} diff -r 15d9ed9b5051 -r 346729a55460 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Wed Mar 14 21:40:28 2007 +0100 +++ b/src/HOL/Hyperreal/NthRoot.thy Wed Mar 14 21:52:26 2007 +0100 @@ -386,4 +386,21 @@ del: realpow_Suc) done +lemma sqrt_divide_self_eq: + assumes nneg: "0 \ x" + shows "sqrt x / x = inverse (sqrt x)" +proof cases + assume "x=0" thus ?thesis by simp +next + assume nz: "x\0" + hence pos: "0 0" by (simp add: divide_inverse nneg nz) + show "inverse (sqrt x) / (sqrt x / x) = 1" + by (simp add: divide_inverse mult_assoc [symmetric] + power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) + qed +qed + end