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 +