src/HOL/Hyperreal/HTranscendental.thy
 changeset 15013 34264f5e4691 parent 14641 79b7bd936264 child 15077 89840837108e
```     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Jun 30 14:04:58 2004 +0200
1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Jul 01 12:29:53 2004 +0200
1.3 @@ -9,6 +9,25 @@
1.4
1.5  theory HTranscendental = Transcendental + Integration:
1.6
1.7 +text{*really belongs in Transcendental*}
1.8 +lemma sqrt_divide_self_eq:
1.9 +  assumes nneg: "0 \<le> x"
1.10 +  shows "sqrt x / x = inverse (sqrt x)"
1.11 +proof cases
1.12 +  assume "x=0" thus ?thesis by simp
1.13 +next
1.14 +  assume nz: "x\<noteq>0"
1.15 +  hence pos: "0<x" using nneg by arith
1.16 +  show ?thesis
1.17 +  proof (rule right_inverse_eq [THEN iffD1, THEN sym])
1.18 +    show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz)
1.19 +    show "inverse (sqrt x) / (sqrt x / x) = 1"
1.20 +      by (simp add: divide_inverse mult_assoc [symmetric]
1.21 +                  power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz)
1.22 +  qed
1.23 +qed
1.24 +
1.25 +
1.26  constdefs
1.27
1.28    exphr :: "real => hypreal"
```