New code generator setup (taken from Library/Executable_Real.thy,
authorberghofe
Thu Sep 06 11:39:43 2007 +0200 (2007-09-06)
changeset 2453409b9a47904b7
parent 24533 fe1f93f6a15a
child 24535 d458d44639fc
New code generator setup (taken from Library/Executable_Real.thy,
also works for old code generator).
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Real/RealDef.thy	Thu Sep 06 11:38:10 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Thu Sep 06 11:39:43 2007 +0200
     1.3 @@ -549,8 +549,8 @@
     1.4    real :: "'a => real"
     1.5  
     1.6  defs (overloaded)
     1.7 -  real_of_nat_def [code unfold]: "real == real_of_nat"
     1.8 -  real_of_int_def [code unfold]: "real == real_of_int"
     1.9 +  real_of_nat_def [code inline]: "real == real_of_nat"
    1.10 +  real_of_int_def [code inline]: "real == real_of_int"
    1.11  
    1.12  lemma real_eq_of_nat: "real = of_nat"
    1.13    unfolding real_of_nat_def ..
    1.14 @@ -926,38 +926,108 @@
    1.15  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
    1.16  by simp
    1.17  
    1.18 -subsection{*Code generation using Isabelle's rats*}
    1.19 +
    1.20 +subsection {* Implementation of rational real numbers as pairs of integers *}
    1.21 +
    1.22 +definition
    1.23 +  RealC :: "int \<times> int \<Rightarrow> real"
    1.24 +where
    1.25 +  "RealC = INum"
    1.26 +
    1.27 +code_datatype RealC
    1.28 +
    1.29 +lemma RealC_simp:
    1.30 +  "RealC (k, l) = real_of_int k / real_of_int l"
    1.31 +  unfolding RealC_def INum_def by simp
    1.32 +
    1.33 +lemma RealC_zero [simp]: "RealC 0\<^sub>N = 0"
    1.34 +  by (simp add: RealC_simp)
    1.35 +
    1.36 +lemma RealC_lit [simp]: "RealC i\<^sub>N = real_of_int i"
    1.37 +  by (simp add: RealC_simp)
    1.38 +
    1.39 +lemma zero_real_code [code, code unfold]:
    1.40 +  "0 = RealC 0\<^sub>N" by simp
    1.41 +
    1.42 +lemma one_real_code [code, code unfold]:
    1.43 +  "1 = RealC 1\<^sub>N" by simp
    1.44 +
    1.45 +instance real :: eq ..
    1.46 +
    1.47 +lemma real_eq_code [code]: "RealC x = RealC y \<longleftrightarrow> normNum x = normNum y"
    1.48 +  unfolding RealC_def INum_normNum_iff ..
    1.49 +
    1.50 +lemma real_less_eq_code [code]: "RealC x \<le> RealC y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
    1.51 +proof -
    1.52 +  have "normNum x \<le>\<^sub>N normNum y \<longleftrightarrow> RealC (normNum x) \<le> RealC (normNum y)" 
    1.53 +    by (simp add: RealC_def del: normNum)
    1.54 +  also have "\<dots> = (RealC x \<le> RealC y)" by (simp add: RealC_def)
    1.55 +  finally show ?thesis by simp
    1.56 +qed
    1.57 +
    1.58 +lemma real_less_code [code]: "RealC x < RealC y \<longleftrightarrow> normNum x <\<^sub>N normNum y"
    1.59 +proof -
    1.60 +  have "normNum x <\<^sub>N normNum y \<longleftrightarrow> RealC (normNum x) < RealC (normNum y)" 
    1.61 +    by (simp add: RealC_def del: normNum)
    1.62 +  also have "\<dots> = (RealC x < RealC y)" by (simp add: RealC_def)
    1.63 +  finally show ?thesis by simp
    1.64 +qed
    1.65 +
    1.66 +lemma real_add_code [code]: "RealC x + RealC y = RealC (x +\<^sub>N y)"
    1.67 +  unfolding RealC_def by simp
    1.68 +
    1.69 +lemma real_mul_code [code]: "RealC x * RealC y = RealC (x *\<^sub>N y)"
    1.70 +  unfolding RealC_def by simp
    1.71 +
    1.72 +lemma real_neg_code [code]: "- RealC x = RealC (~\<^sub>N x)"
    1.73 +  unfolding RealC_def by simp
    1.74 +
    1.75 +lemma real_sub_code [code]: "RealC x - RealC y = RealC (x -\<^sub>N y)"
    1.76 +  unfolding RealC_def by simp
    1.77 +
    1.78 +lemma real_inv_code [code]: "inverse (RealC x) = RealC (Ninv x)"
    1.79 +  unfolding RealC_def Ninv real_divide_def by simp
    1.80 +
    1.81 +lemma real_div_code [code]: "RealC x / RealC y = RealC (x \<div>\<^sub>N y)"
    1.82 +  unfolding RealC_def by simp
    1.83 +
    1.84 +text {* Setup for old code generator *}
    1.85  
    1.86  types_code
    1.87 -  real ("Rat.rat")
    1.88 +  real ("(int */ int)")
    1.89  attach (term_of) {*
    1.90 -fun term_of_real x =
    1.91 - let 
    1.92 -  val rT = HOLogic.realT
    1.93 -  val (p, q) = Rat.quotient_of_rat x
    1.94 - in if q = 1 then HOLogic.mk_number rT p
    1.95 -    else Const("HOL.divide",[rT,rT] ---> rT) $
    1.96 -           (HOLogic.mk_number rT p) $ (HOLogic.mk_number rT q)
    1.97 -end;
    1.98 +fun term_of_real (p, q) =
    1.99 +  let val rT = HOLogic.realT
   1.100 +  in
   1.101 +    if q = 1 orelse p = 0 then HOLogic.mk_number rT p
   1.102 +    else Const ("HOL.inverse_class.divide", [rT, rT] ---> rT) $
   1.103 +      HOLogic.mk_number rT p $ HOLogic.mk_number rT q
   1.104 +  end;
   1.105  *}
   1.106  attach (test) {*
   1.107  fun gen_real i =
   1.108 -let val p = random_range 0 i; val q = random_range 0 i;
   1.109 -    val r = if q=0 then Rat.rat_of_int i else Rat.rat_of_quotient(p,q)
   1.110 -in if one_of [true,false] then r else Rat.neg r end;
   1.111 +  let
   1.112 +    val p = random_range 0 i;
   1.113 +    val q = random_range 1 (i + 1);
   1.114 +    val g = Integer.gcd p q;
   1.115 +    val p' = Integer.div p g;
   1.116 +    val q' = Integer.div q g;
   1.117 +  in
   1.118 +    (if one_of [true, false] then p' else ~ p',
   1.119 +     if p' = 0 then 0 else q')
   1.120 +  end;
   1.121  *}
   1.122  
   1.123  consts_code
   1.124 -  "0 :: real" ("Rat.zero")
   1.125 -  "1 :: real" ("Rat.one")
   1.126 -  "uminus :: real \<Rightarrow> real" ("Rat.neg")
   1.127 -  "op + :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.add")
   1.128 -  "op * :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.mult")
   1.129 -  "inverse :: real \<Rightarrow> real" ("Rat.inv")
   1.130 -  "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.le")
   1.131 -  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.lt")
   1.132 -  "op = :: real \<Rightarrow> real \<Rightarrow> bool" ("curry Rat.eq")
   1.133 -  "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
   1.134 -  "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
   1.135 +  RealC ("(_)")
   1.136 +
   1.137 +consts_code
   1.138 +  "of_int :: int \<Rightarrow> real" ("\<module>real'_of'_int")
   1.139 +attach {*
   1.140 +fun real_of_int 0 = (0, 0)
   1.141 +  | real_of_int i = (i, 1);
   1.142 +*}
   1.143 +
   1.144 +declare real_of_int_of_nat_eq [symmetric, code]
   1.145  
   1.146  end