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"