src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 52403 140ae824ea4a
parent 51542 738598beeb26
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Jun 21 09:00:26 2013 +0200
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Jun 21 12:41:08 2013 +0200
     1.3 @@ -151,6 +151,50 @@
     1.4  
     1.5  hide_const (open) real_of_int
     1.6  
     1.7 +code_const Ratreal (SML)
     1.8 +
     1.9 +definition Realfract :: "int => int => real"
    1.10 +where
    1.11 +  "Realfract p q = of_int p / of_int q"
    1.12 +
    1.13 +code_datatype Realfract
    1.14 +
    1.15 +code_const Realfract
    1.16 +  (SML "Real.fromInt _/ '// Real.fromInt _")
    1.17 +
    1.18 +lemma [code]:
    1.19 +  "Ratreal r = split Realfract (quotient_of r)"
    1.20 +  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
    1.21 +
    1.22 +lemma [code, code del]:
    1.23 +  "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
    1.24 +  ..
    1.25 +
    1.26 +lemma [code, code del]:
    1.27 +  "(plus :: real => real => real) = plus"
    1.28 +  ..
    1.29 +
    1.30 +lemma [code, code del]:
    1.31 +  "(uminus :: real => real) = uminus"
    1.32 +  ..
    1.33 +
    1.34 +lemma [code, code del]:
    1.35 +  "(minus :: real => real => real) = minus"
    1.36 +  ..
    1.37 +
    1.38 +lemma [code, code del]:
    1.39 +  "(times :: real => real => real) = times"
    1.40 +  ..
    1.41 +
    1.42 +lemma [code, code del]:
    1.43 +  "(divide :: real => real => real) = divide"
    1.44 +  ..
    1.45 +
    1.46 +lemma [code]:
    1.47 +  fixes r :: real
    1.48 +  shows "inverse r = 1 / r"
    1.49 +  by (fact inverse_eq_divide)
    1.50 +
    1.51  notepad
    1.52  begin
    1.53    have "cos (pi/2) = 0" by (rule cos_pi_half)