src/HOL/Real/RealDef.thy
changeset 23031 9da9585c816e
parent 22970 b5910e3dec4c
child 23287 063039db59dd
     1.1 --- a/src/HOL/Real/RealDef.thy	Sat May 19 13:40:33 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sat May 19 13:41:13 2007 +0200
     1.3 @@ -971,4 +971,43 @@
     1.4  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
     1.5  by simp
     1.6  
     1.7 +subsection{*Code generation using Isabelle's rats*}
     1.8 +
     1.9 +types_code
    1.10 +  real ("Rat.rat")
    1.11 +attach (term_of) {*
    1.12 +fun term_of_real x =
    1.13 + let 
    1.14 +  val rT = HOLogic.realT
    1.15 +  val (p, q) = Rat.quotient_of_rat x
    1.16 + in if q = 1 then HOLogic.mk_number rT p
    1.17 +    else Const("HOL.divide",[rT,rT] ---> rT) $
    1.18 +           (HOLogic.mk_number rT p) $ (HOLogic.mk_number rT q)
    1.19 +end;
    1.20 +*}
    1.21 +attach (test) {*
    1.22 +fun gen_real i =
    1.23 +let val p = random_range 0 i; val q = random_range 0 i;
    1.24 +    val r = if q=0 then Rat.rat_of_int i else Rat.rat_of_quotient(p,q)
    1.25 +in if one_of [true,false] then r else Rat.neg r end;
    1.26 +*}
    1.27 +
    1.28 +consts_code
    1.29 +  "0 :: real" ("Rat.zero")
    1.30 +  "1 :: real" ("Rat.one")
    1.31 +  "uminus :: real \<Rightarrow> real" ("Rat.neg")
    1.32 +  "op + :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.add")
    1.33 +  "op * :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.mult")
    1.34 +  "inverse :: real \<Rightarrow> real" ("Rat.inv")
    1.35 +  "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.le")
    1.36 +  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("(Rat.ord (_, _) = LESS)")
    1.37 +  "op = :: real \<Rightarrow> real \<Rightarrow> bool" ("curry Rat.eq")
    1.38 +  "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
    1.39 +  "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
    1.40 +
    1.41 +
    1.42 +lemma [code, code unfold]:
    1.43 +  "number_of k = real (number_of k :: int)"
    1.44 +  by simp
    1.45 +
    1.46  end