src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 52435 6646bb548c6b
parent 52403 140ae824ea4a
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -14,61 +14,75 @@
     1.4  The only legitimate use of this theory is as a tool for code generation
     1.5  purposes. *}
     1.6  
     1.7 -code_type real
     1.8 -  (SML   "real")
     1.9 -  (OCaml "float")
    1.10 +code_printing
    1.11 +  type_constructor real \<rightharpoonup>
    1.12 +    (SML) "real"
    1.13 +    and (OCaml) "float"
    1.14  
    1.15 -code_const Ratreal
    1.16 -  (SML "error/ \"Bad constant: Ratreal\"")
    1.17 +code_printing
    1.18 +  constant Ratreal \<rightharpoonup>
    1.19 +    (SML) "error/ \"Bad constant: Ratreal\""
    1.20  
    1.21 -code_const "0 :: real"
    1.22 -  (SML   "0.0")
    1.23 -  (OCaml "0.0")
    1.24 +code_printing
    1.25 +  constant "0 :: real" \<rightharpoonup>
    1.26 +    (SML) "0.0"
    1.27 +    and (OCaml) "0.0"
    1.28  declare zero_real_code[code_unfold del]
    1.29  
    1.30 -code_const "1 :: real"
    1.31 -  (SML   "1.0")
    1.32 -  (OCaml "1.0")
    1.33 +code_printing
    1.34 +  constant "1 :: real" \<rightharpoonup>
    1.35 +    (SML) "1.0"
    1.36 +    and (OCaml) "1.0"
    1.37  declare one_real_code[code_unfold del]
    1.38  
    1.39 -code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    1.40 -  (SML   "Real.== ((_), (_))")
    1.41 -  (OCaml "Pervasives.(=)")
    1.42 +code_printing
    1.43 +  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    1.44 +    (SML) "Real.== ((_), (_))"
    1.45 +    and (OCaml) "Pervasives.(=)"
    1.46  
    1.47 -code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
    1.48 -  (SML   "Real.<= ((_), (_))")
    1.49 -  (OCaml "Pervasives.(<=)")
    1.50 +code_printing
    1.51 +  constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    1.52 +    (SML) "Real.<= ((_), (_))"
    1.53 +    and (OCaml) "Pervasives.(<=)"
    1.54  
    1.55 -code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
    1.56 -  (SML   "Real.< ((_), (_))")
    1.57 -  (OCaml "Pervasives.(<)")
    1.58 +code_printing
    1.59 +  constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    1.60 +    (SML) "Real.< ((_), (_))"
    1.61 +    and (OCaml) "Pervasives.(<)"
    1.62  
    1.63 -code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
    1.64 -  (SML   "Real.+ ((_), (_))")
    1.65 -  (OCaml "Pervasives.( +. )")
    1.66 +code_printing
    1.67 +  constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    1.68 +    (SML) "Real.+ ((_), (_))"
    1.69 +    and (OCaml) "Pervasives.( +. )"
    1.70  
    1.71 -code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
    1.72 -  (SML   "Real.* ((_), (_))")
    1.73 -  (OCaml "Pervasives.( *. )")
    1.74 +code_printing
    1.75 +  constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    1.76 +    (SML) "Real.* ((_), (_))"
    1.77 +    and (OCaml) "Pervasives.( *. )"
    1.78  
    1.79 -code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
    1.80 -  (SML   "Real.- ((_), (_))")
    1.81 -  (OCaml "Pervasives.( -. )")
    1.82 +code_printing
    1.83 +  constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    1.84 +    (SML) "Real.- ((_), (_))"
    1.85 +    and (OCaml) "Pervasives.( -. )"
    1.86  
    1.87 -code_const "uminus :: real \<Rightarrow> real"
    1.88 -  (SML   "Real.~")
    1.89 -  (OCaml "Pervasives.( ~-. )")
    1.90 +code_printing
    1.91 +  constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
    1.92 +    (SML) "Real.~"
    1.93 +    and (OCaml) "Pervasives.( ~-. )"
    1.94  
    1.95 -code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
    1.96 -  (SML   "Real.'/ ((_), (_))")
    1.97 -  (OCaml "Pervasives.( '/. )")
    1.98 +code_printing
    1.99 +  constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
   1.100 +    (SML) "Real.'/ ((_), (_))"
   1.101 +    and (OCaml) "Pervasives.( '/. )"
   1.102  
   1.103 -code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
   1.104 -  (SML   "Real.== ((_:real), (_))")
   1.105 +code_printing
   1.106 +  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
   1.107 +    (SML) "Real.== ((_:real), (_))"
   1.108  
   1.109 -code_const "sqrt :: real \<Rightarrow> real"
   1.110 -  (SML   "Math.sqrt")
   1.111 -  (OCaml "Pervasives.sqrt")
   1.112 +code_printing
   1.113 +  constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
   1.114 +    (SML) "Math.sqrt"
   1.115 +    and (OCaml) "Pervasives.sqrt"
   1.116  declare sqrt_def[code del]
   1.117  
   1.118  definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
   1.119 @@ -76,55 +90,64 @@
   1.120  lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
   1.121    unfolding real_exp_def ..
   1.122  
   1.123 -code_const real_exp
   1.124 -  (SML   "Math.exp")
   1.125 -  (OCaml "Pervasives.exp")
   1.126 +code_printing
   1.127 +  constant real_exp \<rightharpoonup>
   1.128 +    (SML) "Math.exp"
   1.129 +    and (OCaml) "Pervasives.exp"
   1.130  declare real_exp_def[code del]
   1.131  declare exp_def[code del]
   1.132  
   1.133  hide_const (open) real_exp
   1.134  
   1.135 -code_const ln
   1.136 -  (SML   "Math.ln")
   1.137 -  (OCaml "Pervasives.ln")
   1.138 +code_printing
   1.139 +  constant ln \<rightharpoonup>
   1.140 +    (SML) "Math.ln"
   1.141 +    and (OCaml) "Pervasives.ln"
   1.142  declare ln_def[code del]
   1.143  
   1.144 -code_const cos
   1.145 -  (SML   "Math.cos")
   1.146 -  (OCaml "Pervasives.cos")
   1.147 +code_printing
   1.148 +  constant cos \<rightharpoonup>
   1.149 +    (SML) "Math.cos"
   1.150 +    and (OCaml) "Pervasives.cos"
   1.151  declare cos_def[code del]
   1.152  
   1.153 -code_const sin
   1.154 -  (SML   "Math.sin")
   1.155 -  (OCaml "Pervasives.sin")
   1.156 +code_printing
   1.157 +  constant sin \<rightharpoonup>
   1.158 +    (SML) "Math.sin"
   1.159 +    and (OCaml) "Pervasives.sin"
   1.160  declare sin_def[code del]
   1.161  
   1.162 -code_const pi
   1.163 -  (SML   "Math.pi")
   1.164 -  (OCaml "Pervasives.pi")
   1.165 +code_printing
   1.166 +  constant pi \<rightharpoonup>
   1.167 +    (SML) "Math.pi"
   1.168 +    and (OCaml) "Pervasives.pi"
   1.169  declare pi_def[code del]
   1.170  
   1.171 -code_const arctan
   1.172 -  (SML   "Math.atan")
   1.173 -  (OCaml "Pervasives.atan")
   1.174 +code_printing
   1.175 +  constant arctan \<rightharpoonup>
   1.176 +    (SML) "Math.atan"
   1.177 +    and (OCaml) "Pervasives.atan"
   1.178  declare arctan_def[code del]
   1.179  
   1.180 -code_const arccos
   1.181 -  (SML   "Math.scos")
   1.182 -  (OCaml "Pervasives.acos")
   1.183 +code_printing
   1.184 +  constant arccos \<rightharpoonup>
   1.185 +    (SML) "Math.scos"
   1.186 +    and (OCaml) "Pervasives.acos"
   1.187  declare arccos_def[code del]
   1.188  
   1.189 -code_const arcsin
   1.190 -  (SML   "Math.asin")
   1.191 -  (OCaml "Pervasives.asin")
   1.192 +code_printing
   1.193 +  constant arcsin \<rightharpoonup>
   1.194 +    (SML) "Math.asin"
   1.195 +    and (OCaml) "Pervasives.asin"
   1.196  declare arcsin_def[code del]
   1.197  
   1.198  definition real_of_integer :: "integer \<Rightarrow> real" where
   1.199    "real_of_integer = of_int \<circ> int_of_integer"
   1.200  
   1.201 -code_const real_of_integer
   1.202 -  (SML "Real.fromInt")
   1.203 -  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
   1.204 +code_printing
   1.205 +  constant real_of_integer \<rightharpoonup>
   1.206 +    (SML) "Real.fromInt"
   1.207 +    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
   1.208  
   1.209  definition real_of_int :: "int \<Rightarrow> real" where
   1.210    [code_abbrev]: "real_of_int = of_int"
   1.211 @@ -151,7 +174,8 @@
   1.212  
   1.213  hide_const (open) real_of_int
   1.214  
   1.215 -code_const Ratreal (SML)
   1.216 +code_printing
   1.217 +  constant Ratreal \<rightharpoonup> (SML)
   1.218  
   1.219  definition Realfract :: "int => int => real"
   1.220  where
   1.221 @@ -159,8 +183,8 @@
   1.222  
   1.223  code_datatype Realfract
   1.224  
   1.225 -code_const Realfract
   1.226 -  (SML "Real.fromInt _/ '// Real.fromInt _")
   1.227 +code_printing
   1.228 +  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
   1.229  
   1.230  lemma [code]:
   1.231    "Ratreal r = split Realfract (quotient_of r)"