src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 45483 34d07cf7d207
child 45494 e828ccc5c110
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 11:50:52 2011 +0100
     1.3 @@ -0,0 +1,148 @@
     1.4 +(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
     1.5 +
     1.6 +theory Code_Real_Approx_By_Float
     1.7 +imports Complex_Main "~~/src/HOL/Library/Code_Integer"
     1.8 +begin
     1.9 +
    1.10 +text{* \textbf{WARNING} This theory implements mathematical reals by machine
    1.11 +reals (floats). This is inconsistent. See the proof of False at the end of
    1.12 +the theory, where an equality on mathematical reals is (incorrectly)
    1.13 +disproved by mapping it to machine reals.
    1.14 +
    1.15 +The value command cannot display real results yet.
    1.16 +
    1.17 +The only legitimate use of this theory is as a tool for code generation
    1.18 +purposes. *}
    1.19 +
    1.20 +code_type real
    1.21 +  (SML   "real")
    1.22 +  (OCaml "float")
    1.23 +
    1.24 +code_const Ratreal
    1.25 +  (SML "error/ \"Bad constant: Ratreal\"")
    1.26 +
    1.27 +code_const "0 :: real"
    1.28 +  (SML   "0.0")
    1.29 +  (OCaml "0.0")
    1.30 +declare zero_real_code[code_unfold del]
    1.31 +
    1.32 +code_const "1 :: real"
    1.33 +  (SML   "1.0")
    1.34 +  (OCaml "1.0")
    1.35 +declare one_real_code[code_unfold del]
    1.36 +
    1.37 +code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    1.38 +  (SML   "Real.== ((_), (_))")
    1.39 +  (OCaml "Pervasives.(=)")
    1.40 +
    1.41 +code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
    1.42 +  (SML   "Real.<= ((_), (_))")
    1.43 +  (OCaml "Pervasives.(<=)")
    1.44 +
    1.45 +code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
    1.46 +  (SML   "Real.< ((_), (_))")
    1.47 +  (OCaml "Pervasives.(<)")
    1.48 +
    1.49 +code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
    1.50 +  (SML   "Real.+ ((_), (_))")
    1.51 +  (OCaml "Pervasives.( +. )")
    1.52 +
    1.53 +code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
    1.54 +  (SML   "Real.* ((_), (_))")
    1.55 +  (OCaml "Pervasives.( *. )")
    1.56 +
    1.57 +code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
    1.58 +  (SML   "Real.- ((_), (_))")
    1.59 +  (OCaml "Pervasives.( -. )")
    1.60 +
    1.61 +code_const "uminus :: real \<Rightarrow> real"
    1.62 +  (SML   "Real.~")
    1.63 +  (OCaml "Pervasives.( ~-. )")
    1.64 +
    1.65 +code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
    1.66 +  (SML   "Real.'/ ((_), (_))")
    1.67 +  (OCaml "Pervasives.( '/. )")
    1.68 +
    1.69 +code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    1.70 +  (SML   "Real.== ((_:real), (_))")
    1.71 +
    1.72 +code_const "sqrt :: real \<Rightarrow> real"
    1.73 +  (SML   "Math.sqrt")
    1.74 +  (OCaml "Pervasives.sqrt")
    1.75 +declare sqrt_def[code del]
    1.76 +
    1.77 +definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
    1.78 +
    1.79 +lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
    1.80 +  unfolding real_exp_def ..
    1.81 +
    1.82 +code_const real_exp
    1.83 +  (SML   "Math.exp")
    1.84 +  (OCaml "Pervasives.exp")
    1.85 +declare real_exp_def[code del]
    1.86 +declare exp_def[code del]
    1.87 +
    1.88 +hide_const (open) real_exp
    1.89 +
    1.90 +code_const ln
    1.91 +  (SML   "Math.ln")
    1.92 +  (OCaml "Pervasives.ln")
    1.93 +declare ln_def[code del]
    1.94 +
    1.95 +code_const cos
    1.96 +  (SML   "Math.cos")
    1.97 +  (OCaml "Pervasives.cos")
    1.98 +declare cos_def[code del]
    1.99 +
   1.100 +code_const sin
   1.101 +  (SML   "Math.sin")
   1.102 +  (OCaml "Pervasives.sin")
   1.103 +declare sin_def[code del]
   1.104 +
   1.105 +code_const pi
   1.106 +  (SML   "Math.pi")
   1.107 +  (OCaml "Pervasives.pi")
   1.108 +declare pi_def[code del]
   1.109 +
   1.110 +code_const arctan
   1.111 +  (SML   "Math.atan")
   1.112 +  (OCaml "Pervasives.atan")
   1.113 +declare arctan_def[code del]
   1.114 +
   1.115 +code_const arccos
   1.116 +  (SML   "Math.scos")
   1.117 +  (OCaml "Pervasives.acos")
   1.118 +declare arccos_def[code del]
   1.119 +
   1.120 +code_const arcsin
   1.121 +  (SML   "Math.asin")
   1.122 +  (OCaml "Pervasives.asin")
   1.123 +declare arcsin_def[code del]
   1.124 +
   1.125 +definition real_of_int :: "int \<Rightarrow> real" where
   1.126 +  "real_of_int \<equiv> of_int"
   1.127 +
   1.128 +code_const real_of_int
   1.129 +  (SML "Real.fromInt")
   1.130 +  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
   1.131 +
   1.132 +lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
   1.133 +  unfolding real_of_int_def ..
   1.134 +
   1.135 +hide_const (open) real_of_int
   1.136 +
   1.137 +declare number_of_real_code [code_unfold del]
   1.138 +
   1.139 +lemma "False"
   1.140 +proof-
   1.141 +  have "cos(pi/2) = 0" by(rule cos_pi_half)
   1.142 +  moreover have "cos(pi/2) \<noteq> 0" by eval
   1.143 +  ultimately show "False" by blast
   1.144 +qed
   1.145 +
   1.146 +definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))"
   1.147 +
   1.148 +export_code test
   1.149 +  in OCaml file -
   1.150 +
   1.151 +end