src/HOL/Library/Code_Real_Approx_By_Float.thy
 author haftmann Tue Nov 19 10:05:53 2013 +0100 (2013-11-19) changeset 54489 03ff4d1e6784 parent 52435 6646bb548c6b child 60017 b785d6d06430 permissions -rw-r--r--
eliminiated neg_numeral in favour of - (numeral _)
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{* \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. *}
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 definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
90 lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
91   unfolding real_exp_def ..
93 code_printing
94   constant real_exp \<rightharpoonup>
95     (SML) "Math.exp"
96     and (OCaml) "Pervasives.exp"
97 declare real_exp_def[code del]
98 declare exp_def[code del]
100 hide_const (open) real_exp
102 code_printing
103   constant ln \<rightharpoonup>
104     (SML) "Math.ln"
105     and (OCaml) "Pervasives.ln"
106 declare ln_def[code del]
108 code_printing
109   constant cos \<rightharpoonup>
110     (SML) "Math.cos"
111     and (OCaml) "Pervasives.cos"
112 declare cos_def[code del]
114 code_printing
115   constant sin \<rightharpoonup>
116     (SML) "Math.sin"
117     and (OCaml) "Pervasives.sin"
118 declare sin_def[code del]
120 code_printing
121   constant pi \<rightharpoonup>
122     (SML) "Math.pi"
123     and (OCaml) "Pervasives.pi"
124 declare pi_def[code del]
126 code_printing
127   constant arctan \<rightharpoonup>
128     (SML) "Math.atan"
129     and (OCaml) "Pervasives.atan"
130 declare arctan_def[code del]
132 code_printing
133   constant arccos \<rightharpoonup>
134     (SML) "Math.scos"
135     and (OCaml) "Pervasives.acos"
136 declare arccos_def[code del]
138 code_printing
139   constant arcsin \<rightharpoonup>
140     (SML) "Math.asin"
141     and (OCaml) "Pervasives.asin"
142 declare arcsin_def[code del]
144 definition real_of_integer :: "integer \<Rightarrow> real" where
145   "real_of_integer = of_int \<circ> int_of_integer"
147 code_printing
148   constant real_of_integer \<rightharpoonup>
149     (SML) "Real.fromInt"
150     and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
152 definition real_of_int :: "int \<Rightarrow> real" where
153   [code_abbrev]: "real_of_int = of_int"
155 lemma [code]:
156   "real_of_int = real_of_integer \<circ> integer_of_int"
157   by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
159 lemma [code_unfold del]:
160   "0 \<equiv> (of_rat 0 :: real)"
161   by simp
163 lemma [code_unfold del]:
164   "1 \<equiv> (of_rat 1 :: real)"
165   by simp
167 lemma [code_unfold del]:
168   "numeral k \<equiv> (of_rat (numeral k) :: real)"
169   by simp
171 lemma [code_unfold del]:
172   "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
173   by simp
175 hide_const (open) real_of_int
177 code_printing
178   constant Ratreal \<rightharpoonup> (SML)
180 definition Realfract :: "int => int => real"
181 where
182   "Realfract p q = of_int p / of_int q"
184 code_datatype Realfract
186 code_printing
187   constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
189 lemma [code]:
190   "Ratreal r = split Realfract (quotient_of r)"
191   by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
193 lemma [code, code del]:
194   "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
195   ..
197 lemma [code, code del]:
198   "(plus :: real => real => real) = plus"
199   ..
201 lemma [code, code del]:
202   "(uminus :: real => real) = uminus"
203   ..
205 lemma [code, code del]:
206   "(minus :: real => real => real) = minus"
207   ..
209 lemma [code, code del]:
210   "(times :: real => real => real) = times"
211   ..
213 lemma [code, code del]:
214   "(divide :: real => real => real) = divide"
215   ..
217 lemma [code]:
218   fixes r :: real
219   shows "inverse r = 1 / r"
220   by (fact inverse_eq_divide)