# HG changeset patch
# User nipkow
# Date 1179574873 -7200
# Node ID 9da9585c816e13b9282e8e9b779e5aa0c9248b29
# Parent  c7ff1537c4bf86073319e127803bda78dafc9f0d
added code generation based on Isabelle's rat type.

diff -r c7ff1537c4bf -r 9da9585c816e src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sat May 19 13:40:33 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Sat May 19 13:41:13 2007 +0200
@@ -971,4 +971,43 @@
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 by simp
 
+subsection{*Code generation using Isabelle's rats*}
+
+types_code
+  real ("Rat.rat")
+attach (term_of) {*
+fun term_of_real x =
+ let 
+  val rT = HOLogic.realT
+  val (p, q) = Rat.quotient_of_rat x
+ in if q = 1 then HOLogic.mk_number rT p
+    else Const("HOL.divide",[rT,rT] ---> rT) $
+           (HOLogic.mk_number rT p) $ (HOLogic.mk_number rT q)
+end;
+*}
+attach (test) {*
+fun gen_real i =
+let val p = random_range 0 i; val q = random_range 0 i;
+    val r = if q=0 then Rat.rat_of_int i else Rat.rat_of_quotient(p,q)
+in if one_of [true,false] then r else Rat.neg r end;
+*}
+
+consts_code
+  "0 :: real" ("Rat.zero")
+  "1 :: real" ("Rat.one")
+  "uminus :: real \<Rightarrow> real" ("Rat.neg")
+  "op + :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.add")
+  "op * :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.mult")
+  "inverse :: real \<Rightarrow> real" ("Rat.inv")
+  "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.le")
+  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("(Rat.ord (_, _) = LESS)")
+  "op = :: real \<Rightarrow> real \<Rightarrow> bool" ("curry Rat.eq")
+  "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
+  "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
+
+
+lemma [code, code unfold]:
+  "number_of k = real (number_of k :: int)"
+  by simp
+
 end