src/HOL/Library/Code_Real_Approx_By_Float.thy
 author haftmann Tue Oct 13 09:21:15 2015 +0200 (2015-10-13) changeset 61424 c3658c18b7bc parent 61115 3a4400985780 child 63355 7b23053be254 permissions -rw-r--r--
prod_case as canonical name for product type eliminator
1 (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
3 theory Code_Real_Approx_By_Float
4 imports Complex_Main Code_Target_Int
5 begin
7 text\<open>\textbf{WARNING} This theory implements mathematical reals by machine
8 reals (floats). This is inconsistent. See the proof of False at the end of
9 the theory, where an equality on mathematical reals is (incorrectly)
10 disproved by mapping it to machine reals.
12 The value command cannot display real results yet.
14 The only legitimate use of this theory is as a tool for code generation
15 purposes.\<close>
17 code_printing
18   type_constructor real \<rightharpoonup>
19     (SML) "real"
20     and (OCaml) "float"
22 code_printing
23   constant Ratreal \<rightharpoonup>
24     (SML) "error/ \"Bad constant: Ratreal\""
26 code_printing
27   constant "0 :: real" \<rightharpoonup>
28     (SML) "0.0"
29     and (OCaml) "0.0"
30 declare zero_real_code[code_unfold del]
32 code_printing
33   constant "1 :: real" \<rightharpoonup>
34     (SML) "1.0"
35     and (OCaml) "1.0"
36 declare one_real_code[code_unfold del]
38 code_printing
39   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
40     (SML) "Real.== ((_), (_))"
41     and (OCaml) "Pervasives.(=)"
43 code_printing
44   constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
45     (SML) "Real.<= ((_), (_))"
46     and (OCaml) "Pervasives.(<=)"
48 code_printing
49   constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
50     (SML) "Real.< ((_), (_))"
51     and (OCaml) "Pervasives.(<)"
53 code_printing
54   constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
55     (SML) "Real.+ ((_), (_))"
56     and (OCaml) "Pervasives.( +. )"
58 code_printing
59   constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
60     (SML) "Real.* ((_), (_))"
61     and (OCaml) "Pervasives.( *. )"
63 code_printing
64   constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
65     (SML) "Real.- ((_), (_))"
66     and (OCaml) "Pervasives.( -. )"
68 code_printing
69   constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
70     (SML) "Real.~"
71     and (OCaml) "Pervasives.( ~-. )"
73 code_printing
74   constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
75     (SML) "Real.'/ ((_), (_))"
76     and (OCaml) "Pervasives.( '/. )"
78 code_printing
79   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
80     (SML) "Real.== ((_:real), (_))"
82 code_printing
83   constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
84     (SML) "Math.sqrt"
85     and (OCaml) "Pervasives.sqrt"
86 declare sqrt_def[code del]
88 context
89 begin
91 qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
93 lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
94   unfolding real_exp_def ..
96 end
98 code_printing
99   constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
100     (SML) "Math.exp"
101     and (OCaml) "Pervasives.exp"
102 declare Code_Real_Approx_By_Float.real_exp_def[code del]
103 declare exp_def[code del]
105 code_printing
106   constant ln \<rightharpoonup>
107     (SML) "Math.ln"
108     and (OCaml) "Pervasives.ln"
109 declare ln_real_def[code del]
111 code_printing
112   constant cos \<rightharpoonup>
113     (SML) "Math.cos"
114     and (OCaml) "Pervasives.cos"
115 declare cos_def[code del]
117 code_printing
118   constant sin \<rightharpoonup>
119     (SML) "Math.sin"
120     and (OCaml) "Pervasives.sin"
121 declare sin_def[code del]
123 code_printing
124   constant pi \<rightharpoonup>
125     (SML) "Math.pi"
126     and (OCaml) "Pervasives.pi"
127 declare pi_def[code del]
129 code_printing
130   constant arctan \<rightharpoonup>
131     (SML) "Math.atan"
132     and (OCaml) "Pervasives.atan"
133 declare arctan_def[code del]
135 code_printing
136   constant arccos \<rightharpoonup>
137     (SML) "Math.scos"
138     and (OCaml) "Pervasives.acos"
139 declare arccos_def[code del]
141 code_printing
142   constant arcsin \<rightharpoonup>
143     (SML) "Math.asin"
144     and (OCaml) "Pervasives.asin"
145 declare arcsin_def[code del]
147 definition real_of_integer :: "integer \<Rightarrow> real" where
148   "real_of_integer = of_int \<circ> int_of_integer"
150 code_printing
151   constant real_of_integer \<rightharpoonup>
152     (SML) "Real.fromInt"
153     and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
155 context
156 begin
158 qualified definition real_of_int :: "int \<Rightarrow> real" where
159   [code_abbrev]: "real_of_int = of_int"
161 lemma [code]:
162   "real_of_int = real_of_integer \<circ> integer_of_int"
163   by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
165 lemma [code_unfold del]:
166   "0 \<equiv> (of_rat 0 :: real)"
167   by simp
169 lemma [code_unfold del]:
170   "1 \<equiv> (of_rat 1 :: real)"
171   by simp
173 lemma [code_unfold del]:
174   "numeral k \<equiv> (of_rat (numeral k) :: real)"
175   by simp
177 lemma [code_unfold del]:
178   "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
179   by simp
181 end
183 code_printing
184   constant Ratreal \<rightharpoonup> (SML)
186 definition Realfract :: "int => int => real"
187 where
188   "Realfract p q = of_int p / of_int q"
190 code_datatype Realfract
192 code_printing
193   constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
195 lemma [code]:
196   "Ratreal r = case_prod Realfract (quotient_of r)"
197   by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
199 lemma [code, code del]:
200   "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
201   ..
203 lemma [code, code del]:
204   "(plus :: real => real => real) = plus"
205   ..
207 lemma [code, code del]:
208   "(uminus :: real => real) = uminus"
209   ..
211 lemma [code, code del]:
212   "(minus :: real => real => real) = minus"
213   ..
215 lemma [code, code del]:
216   "(times :: real => real => real) = times"
217   ..
219 lemma [code, code del]:
220   "(divide :: real => real => real) = divide"
221   ..
223 lemma [code]:
224   fixes r :: real
225   shows "inverse r = 1 / r"
226   by (fact inverse_eq_divide)