author | nipkow |
Wed, 13 Feb 2019 07:48:42 +0100 | |
changeset 69801 | a99a0f5474c5 |
parent 69064 | 5840724b1d71 |
child 69906 | 55534affe445 |
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 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
37 |
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
|
38 |
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
|
39 |
(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
|
40 |
and (OCaml) "1.0" |
45483 | 41 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
(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
|
45 |
and (OCaml) "Pervasives.(=)" |
45483 | 46 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
(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
|
50 |
and (OCaml) "Pervasives.(<=)" |
45483 | 51 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
(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
|
55 |
and (OCaml) "Pervasives.(<)" |
45483 | 56 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
57 |
code_printing |
67399 | 58 |
constant "(+) :: real \<Rightarrow> real \<Rightarrow> real" \<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
|
59 |
(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
|
60 |
and (OCaml) "Pervasives.( +. )" |
45483 | 61 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
62 |
code_printing |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
67399
diff
changeset
|
63 |
constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<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
|
64 |
(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
|
65 |
and (OCaml) "Pervasives.( *. )" |
45483 | 66 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
67 |
code_printing |
67399 | 68 |
constant "(-) :: real \<Rightarrow> real \<Rightarrow> real" \<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
|
69 |
(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
|
70 |
and (OCaml) "Pervasives.( -. )" |
45483 | 71 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
72 |
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
|
73 |
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
|
74 |
(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
|
75 |
and (OCaml) "Pervasives.( ~-. )" |
45483 | 76 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
77 |
code_printing |
67399 | 78 |
constant "(/) :: real \<Rightarrow> real \<Rightarrow> real" \<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
|
79 |
(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
|
80 |
and (OCaml) "Pervasives.( '/. )" |
45483 | 81 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
(SML) "Real.== ((_:real), (_))" |
45483 | 85 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
(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
|
89 |
and (OCaml) "Pervasives.sqrt" |
45483 | 90 |
declare sqrt_def[code del] |
91 |
||
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
92 |
context |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
93 |
begin |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
94 |
|
63355 | 95 |
qualified definition real_exp :: "real \<Rightarrow> real" |
96 |
where "real_exp = exp" |
|
45483 | 97 |
|
63355 | 98 |
lemma exp_eq_real_exp [code_unfold]: "exp = real_exp" |
45483 | 99 |
unfolding real_exp_def .. |
100 |
||
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
101 |
end |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
102 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
103 |
code_printing |
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
104 |
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
|
105 |
(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
|
106 |
and (OCaml) "Pervasives.exp" |
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
107 |
declare Code_Real_Approx_By_Float.real_exp_def[code del] |
45483 | 108 |
declare exp_def[code del] |
109 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
110 |
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
|
111 |
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
|
112 |
(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
|
113 |
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
|
114 |
declare ln_real_def[code del] |
45483 | 115 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
116 |
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
|
117 |
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
|
118 |
(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
|
119 |
and (OCaml) "Pervasives.cos" |
45483 | 120 |
declare cos_def[code del] |
121 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
(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
|
125 |
and (OCaml) "Pervasives.sin" |
45483 | 126 |
declare sin_def[code del] |
127 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
128 |
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
|
129 |
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
|
130 |
(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
|
131 |
and (OCaml) "Pervasives.pi" |
45483 | 132 |
declare pi_def[code del] |
133 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
134 |
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
|
135 |
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
|
136 |
(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
|
137 |
and (OCaml) "Pervasives.atan" |
45483 | 138 |
declare arctan_def[code del] |
139 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
140 |
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
|
141 |
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
|
142 |
(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
|
143 |
and (OCaml) "Pervasives.acos" |
45483 | 144 |
declare arccos_def[code del] |
145 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
146 |
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
|
147 |
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
|
148 |
(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
|
149 |
and (OCaml) "Pervasives.asin" |
45483 | 150 |
declare arcsin_def[code del] |
151 |
||
63355 | 152 |
definition real_of_integer :: "integer \<Rightarrow> real" |
153 |
where "real_of_integer = of_int \<circ> int_of_integer" |
|
45483 | 154 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
155 |
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
|
156 |
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
|
157 |
(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
|
158 |
and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))" |
45483 | 159 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
160 |
context |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
161 |
begin |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
162 |
|
63355 | 163 |
qualified definition real_of_int :: "int \<Rightarrow> real" |
164 |
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
|
165 |
|
63355 | 166 |
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
|
167 |
by (simp add: fun_eq_iff real_of_integer_def real_of_int_def) |
45483 | 168 |
|
63355 | 169 |
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
|
170 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
171 |
|
63355 | 172 |
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
|
173 |
by simp |
45483 | 174 |
|
63355 | 175 |
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
|
176 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
177 |
|
63355 | 178 |
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
|
179 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
180 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
181 |
end |
45483 | 182 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
183 |
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
|
184 |
constant Ratreal \<rightharpoonup> (SML) |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
185 |
|
63355 | 186 |
definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real" |
187 |
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
|
188 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
189 |
code_datatype Realfract |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
190 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
191 |
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
|
192 |
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
|
193 |
|
63355 | 194 |
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
|
195 |
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
|
196 |
|
66148 | 197 |
declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" |
198 |
"plus :: real \<Rightarrow> real \<Rightarrow> real" |
|
199 |
"uminus :: real \<Rightarrow> real" |
|
200 |
"minus :: real \<Rightarrow> real \<Rightarrow> real" |
|
201 |
"times :: real \<Rightarrow> real \<Rightarrow> real" |
|
202 |
"divide :: real \<Rightarrow> real \<Rightarrow> real"]] |
|
63355 | 203 |
|
204 |
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
|
205 |
by (fact inverse_eq_divide) |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
206 |
|
46530 | 207 |
notepad |
208 |
begin |
|
209 |
have "cos (pi/2) = 0" by (rule cos_pi_half) |
|
210 |
moreover have "cos (pi/2) \<noteq> 0" by eval |
|
63355 | 211 |
ultimately have False by blast |
46530 | 212 |
end |
45483 | 213 |
|
214 |
end |