--- 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