author huffman Wed, 14 Mar 2007 21:52:26 +0100 changeset 22443 346729a55460 parent 22442 15d9ed9b5051 child 22444 fb80fedd192d
move sqrt_divide_self_eq to NthRoot.thy
 src/HOL/Hyperreal/HTranscendental.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/NthRoot.thy file | annotate | diff | comparison | revisions
```--- 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 *}```
```--- 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```