add code equation for real_of_float
authorhoelzl
Thu Apr 26 14:42:50 2012 +0200 (2012-04-26)
changeset 477803357688660ff
parent 47779 5a10e24fe7ab
child 47781 49381b55b2c1
add code equation for real_of_float
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Thu Apr 26 14:11:13 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Apr 26 14:42:50 2012 +0200
     1.3 @@ -130,6 +130,10 @@
     1.4  lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
     1.5  declare Float.rep_eq[simp]
     1.6  
     1.7 +lemma compute_real_of_float[code]:
     1.8 +  "real_of_float (Float m e) = (if e \<ge> 0 then m * 2 ^ nat e else m / 2 ^ (nat (-e)))"
     1.9 +by (simp add: real_of_float_def[symmetric] powr_int)
    1.10 +
    1.11  code_datatype Float
    1.12  
    1.13  subsection {* Arithmetic operations on floating point numbers *}