author | wenzelm |
Tue, 19 Jul 2016 09:55:03 +0200 | |
changeset 63520 | 2803d2b8f85d |
parent 63355 | 7b23053be254 |
child 66147 | 9225370db5f0 |
permissions | -rw-r--r-- |
63355 | 1 |
(* Title: HOL/Library/Code_Real_Approx_By_Float.thy |
2 |
Author: Florian Haftmann |
|
3 |
Author: Johannes Hölzl |
|
4 |
Author: Tobias Nipkow |
|
5 |
*) |
|
45483 | 6 |
|
7 |
theory Code_Real_Approx_By_Float |
|
51542 | 8 |
imports Complex_Main Code_Target_Int |
45483 | 9 |
begin |
10 |
||
63355 | 11 |
text\<open> |
12 |
\<^bold>\<open>WARNING!\<close> This theory implements mathematical reals by machine reals |
|
13 |
(floats). This is inconsistent. See the proof of False at the end of the |
|
14 |
theory, where an equality on mathematical reals is (incorrectly) disproved |
|
15 |
by mapping it to machine reals. |
|
45483 | 16 |
|
63355 | 17 |
The \<^theory_text>\<open>value\<close> command cannot display real results yet. |
45483 | 18 |
|
63355 | 19 |
The only legitimate use of this theory is as a tool for code generation |
20 |
purposes. |
|
21 |
\<close> |
|
45483 | 22 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
23 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
24 |
type_constructor real \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
25 |
(SML) "real" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
26 |
and (OCaml) "float" |
45483 | 27 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
28 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
29 |
constant Ratreal \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
30 |
(SML) "error/ \"Bad constant: Ratreal\"" |
45483 | 31 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
32 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
33 |
constant "0 :: real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
34 |
(SML) "0.0" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
35 |
and (OCaml) "0.0" |
45483 | 36 |
declare zero_real_code[code_unfold del] |
37 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
38 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
39 |
constant "1 :: real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
40 |
(SML) "1.0" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
41 |
and (OCaml) "1.0" |
45483 | 42 |
declare one_real_code[code_unfold del] |
43 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
44 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
45 |
constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
46 |
(SML) "Real.== ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
47 |
and (OCaml) "Pervasives.(=)" |
45483 | 48 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
49 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
50 |
constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
51 |
(SML) "Real.<= ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
52 |
and (OCaml) "Pervasives.(<=)" |
45483 | 53 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
54 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
55 |
constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
56 |
(SML) "Real.< ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
57 |
and (OCaml) "Pervasives.(<)" |
45483 | 58 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
59 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
60 |
constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
61 |
(SML) "Real.+ ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
62 |
and (OCaml) "Pervasives.( +. )" |
45483 | 63 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
64 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
65 |
constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
66 |
(SML) "Real.* ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
67 |
and (OCaml) "Pervasives.( *. )" |
45483 | 68 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
69 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
70 |
constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
71 |
(SML) "Real.- ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
72 |
and (OCaml) "Pervasives.( -. )" |
45483 | 73 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
74 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
75 |
constant "uminus :: real \<Rightarrow> real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
76 |
(SML) "Real.~" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
77 |
and (OCaml) "Pervasives.( ~-. )" |
45483 | 78 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
79 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
80 |
constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
81 |
(SML) "Real.'/ ((_), (_))" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
82 |
and (OCaml) "Pervasives.( '/. )" |
45483 | 83 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
84 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
85 |
constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
86 |
(SML) "Real.== ((_:real), (_))" |
45483 | 87 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
88 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
89 |
constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
90 |
(SML) "Math.sqrt" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
91 |
and (OCaml) "Pervasives.sqrt" |
45483 | 92 |
declare sqrt_def[code del] |
93 |
||
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
94 |
context |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
95 |
begin |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
96 |
|
63355 | 97 |
qualified definition real_exp :: "real \<Rightarrow> real" |
98 |
where "real_exp = exp" |
|
45483 | 99 |
|
63355 | 100 |
lemma exp_eq_real_exp [code_unfold]: "exp = real_exp" |
45483 | 101 |
unfolding real_exp_def .. |
102 |
||
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
103 |
end |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
104 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
105 |
code_printing |
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
106 |
constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup> |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
107 |
(SML) "Math.exp" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
108 |
and (OCaml) "Pervasives.exp" |
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
109 |
declare Code_Real_Approx_By_Float.real_exp_def[code del] |
45483 | 110 |
declare exp_def[code del] |
111 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
112 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
113 |
constant ln \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
114 |
(SML) "Math.ln" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
115 |
and (OCaml) "Pervasives.ln" |
60017
b785d6d06430
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents:
54489
diff
changeset
|
116 |
declare ln_real_def[code del] |
45483 | 117 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
118 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
119 |
constant cos \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
120 |
(SML) "Math.cos" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
121 |
and (OCaml) "Pervasives.cos" |
45483 | 122 |
declare cos_def[code del] |
123 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
124 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
125 |
constant sin \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
126 |
(SML) "Math.sin" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
127 |
and (OCaml) "Pervasives.sin" |
45483 | 128 |
declare sin_def[code del] |
129 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
130 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
131 |
constant pi \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
132 |
(SML) "Math.pi" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
133 |
and (OCaml) "Pervasives.pi" |
45483 | 134 |
declare pi_def[code del] |
135 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
136 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
137 |
constant arctan \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
138 |
(SML) "Math.atan" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
139 |
and (OCaml) "Pervasives.atan" |
45483 | 140 |
declare arctan_def[code del] |
141 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
142 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
143 |
constant arccos \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
144 |
(SML) "Math.scos" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
145 |
and (OCaml) "Pervasives.acos" |
45483 | 146 |
declare arccos_def[code del] |
147 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
148 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
149 |
constant arcsin \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
150 |
(SML) "Math.asin" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
151 |
and (OCaml) "Pervasives.asin" |
45483 | 152 |
declare arcsin_def[code del] |
153 |
||
63355 | 154 |
definition real_of_integer :: "integer \<Rightarrow> real" |
155 |
where "real_of_integer = of_int \<circ> int_of_integer" |
|
45483 | 156 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
157 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
158 |
constant real_of_integer \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
159 |
(SML) "Real.fromInt" |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
160 |
and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))" |
45483 | 161 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
162 |
context |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
163 |
begin |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
164 |
|
63355 | 165 |
qualified definition real_of_int :: "int \<Rightarrow> real" |
166 |
where [code_abbrev]: "real_of_int = of_int" |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
167 |
|
63355 | 168 |
lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int" |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
169 |
by (simp add: fun_eq_iff real_of_integer_def real_of_int_def) |
45483 | 170 |
|
63355 | 171 |
lemma [code_unfold del]: "0 \<equiv> (of_rat 0 :: real)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
172 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
173 |
|
63355 | 174 |
lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
175 |
by simp |
45483 | 176 |
|
63355 | 177 |
lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
178 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
179 |
|
63355 | 180 |
lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
181 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
182 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
183 |
end |
45483 | 184 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
185 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
186 |
constant Ratreal \<rightharpoonup> (SML) |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
187 |
|
63355 | 188 |
definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real" |
189 |
where "Realfract p q = of_int p / of_int q" |
|
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
190 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
191 |
code_datatype Realfract |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
192 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
193 |
code_printing |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
194 |
constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
195 |
|
63355 | 196 |
lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
197 |
by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat) |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
198 |
|
63355 | 199 |
lemma [code, code del]: "(HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool) = (HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool)" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
200 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
201 |
|
63355 | 202 |
lemma [code, code del]: "(plus :: real \<Rightarrow> real \<Rightarrow> real) = plus" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
203 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
204 |
|
63355 | 205 |
lemma [code, code del]: "(uminus :: real \<Rightarrow> real) = uminus" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
206 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
207 |
|
63355 | 208 |
lemma [code, code del]: "(minus :: real \<Rightarrow> real \<Rightarrow> real) = minus" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
209 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
210 |
|
63355 | 211 |
lemma [code, code del]: "(times :: real \<Rightarrow> real \<Rightarrow> real) = times" |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
212 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
213 |
|
63355 | 214 |
lemma [code, code del]: "(divide :: real \<Rightarrow> real \<Rightarrow> real) = divide" |
215 |
.. |
|
216 |
||
217 |
lemma [code]: "inverse r = 1 / r" for r :: real |
|
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
218 |
by (fact inverse_eq_divide) |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
219 |
|
46530 | 220 |
notepad |
221 |
begin |
|
222 |
have "cos (pi/2) = 0" by (rule cos_pi_half) |
|
223 |
moreover have "cos (pi/2) \<noteq> 0" by eval |
|
63355 | 224 |
ultimately have False by blast |
46530 | 225 |
end |
45483 | 226 |
|
227 |
end |