# 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 \<le> x"
-  shows "sqrt x / x = inverse (sqrt x)"
-proof cases
-  assume "x=0" thus ?thesis by simp
-next
-  assume nz: "x\<noteq>0" 
-  hence pos: "0<x" using nneg by arith
-  show ?thesis
-  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
-    show "sqrt x / x \<noteq> 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 \<le> x"
+  shows "sqrt x / x = inverse (sqrt x)"
+proof cases
+  assume "x=0" thus ?thesis by simp
+next
+  assume nz: "x\<noteq>0" 
+  hence pos: "0<x" using nneg by arith
+  show ?thesis
+  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
+    show "sqrt x / x \<noteq> 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