author | paulson <lp15@cam.ac.uk> |
Sat, 11 Apr 2015 11:56:40 +0100 | |
changeset 60017 | b785d6d06430 |
parent 54489 | 03ff4d1e6784 |
child 60500 | 903bb1495239 |
permissions | -rw-r--r-- |
45483 | 1 |
(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *) |
2 |
||
3 |
theory Code_Real_Approx_By_Float |
|
51542 | 4 |
imports Complex_Main Code_Target_Int |
45483 | 5 |
begin |
6 |
||
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. |
|
11 |
||
12 |
The value command cannot display real results yet. |
|
13 |
||
14 |
The only legitimate use of this theory is as a tool for code generation |
|
15 |
purposes. *} |
|
16 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
17 |
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
|
18 |
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
|
19 |
(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
|
20 |
and (OCaml) "float" |
45483 | 21 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
(SML) "error/ \"Bad constant: Ratreal\"" |
45483 | 25 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
26 |
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
|
27 |
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
|
28 |
(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
|
29 |
and (OCaml) "0.0" |
45483 | 30 |
declare zero_real_code[code_unfold del] |
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 "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
|
34 |
(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
|
35 |
and (OCaml) "1.0" |
45483 | 36 |
declare one_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 "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
|
40 |
(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
|
41 |
and (OCaml) "Pervasives.(=)" |
45483 | 42 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
(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
|
46 |
and (OCaml) "Pervasives.(<=)" |
45483 | 47 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
48 |
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
|
49 |
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
|
50 |
(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
|
51 |
and (OCaml) "Pervasives.(<)" |
45483 | 52 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
53 |
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
|
54 |
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
|
55 |
(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
|
56 |
and (OCaml) "Pervasives.( +. )" |
45483 | 57 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
(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
|
61 |
and (OCaml) "Pervasives.( *. )" |
45483 | 62 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
63 |
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
|
64 |
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
|
65 |
(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
|
66 |
and (OCaml) "Pervasives.( -. )" |
45483 | 67 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
(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
|
71 |
and (OCaml) "Pervasives.( ~-. )" |
45483 | 72 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
(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
|
76 |
and (OCaml) "Pervasives.( '/. )" |
45483 | 77 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
(SML) "Real.== ((_:real), (_))" |
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 "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
|
84 |
(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
|
85 |
and (OCaml) "Pervasives.sqrt" |
45483 | 86 |
declare sqrt_def[code del] |
87 |
||
88 |
definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp" |
|
89 |
||
90 |
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp" |
|
91 |
unfolding real_exp_def .. |
|
92 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
93 |
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
|
94 |
constant real_exp \<rightharpoonup> |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
95 |
(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
|
96 |
and (OCaml) "Pervasives.exp" |
45483 | 97 |
declare real_exp_def[code del] |
98 |
declare exp_def[code del] |
|
99 |
||
100 |
hide_const (open) real_exp |
|
101 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
102 |
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
|
103 |
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
|
104 |
(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
|
105 |
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
|
106 |
declare ln_real_def[code del] |
45483 | 107 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
108 |
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
|
109 |
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
|
110 |
(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
|
111 |
and (OCaml) "Pervasives.cos" |
45483 | 112 |
declare cos_def[code del] |
113 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
114 |
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
|
115 |
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
|
116 |
(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
|
117 |
and (OCaml) "Pervasives.sin" |
45483 | 118 |
declare sin_def[code del] |
119 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
120 |
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
|
121 |
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
|
122 |
(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
|
123 |
and (OCaml) "Pervasives.pi" |
45483 | 124 |
declare pi_def[code del] |
125 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
126 |
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
|
127 |
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
|
128 |
(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
|
129 |
and (OCaml) "Pervasives.atan" |
45483 | 130 |
declare arctan_def[code del] |
131 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
132 |
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
|
133 |
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
|
134 |
(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
|
135 |
and (OCaml) "Pervasives.acos" |
45483 | 136 |
declare arccos_def[code del] |
137 |
||
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
138 |
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
|
139 |
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
|
140 |
(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
|
141 |
and (OCaml) "Pervasives.asin" |
45483 | 142 |
declare arcsin_def[code del] |
143 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
144 |
definition real_of_integer :: "integer \<Rightarrow> real" where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
145 |
"real_of_integer = of_int \<circ> int_of_integer" |
45483 | 146 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
(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
|
150 |
and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))" |
45483 | 151 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
152 |
definition real_of_int :: "int \<Rightarrow> real" where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
153 |
[code_abbrev]: "real_of_int = of_int" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
154 |
|
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
155 |
lemma [code]: |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
156 |
"real_of_int = real_of_integer \<circ> integer_of_int" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
157 |
by (simp add: fun_eq_iff real_of_integer_def real_of_int_def) |
45483 | 158 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
159 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
160 |
"0 \<equiv> (of_rat 0 :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
161 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
162 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
163 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
164 |
"1 \<equiv> (of_rat 1 :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
165 |
by simp |
45483 | 166 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
167 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
168 |
"numeral k \<equiv> (of_rat (numeral k) :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
169 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
170 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
171 |
lemma [code_unfold del]: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52435
diff
changeset
|
172 |
"- numeral k \<equiv> (of_rat (- numeral k) :: real)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
173 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
174 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
175 |
hide_const (open) real_of_int |
45483 | 176 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
177 |
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
|
178 |
constant Ratreal \<rightharpoonup> (SML) |
52403
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
179 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
180 |
definition Realfract :: "int => int => real" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
181 |
where |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
182 |
"Realfract p q = of_int p / of_int q" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
183 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
184 |
code_datatype Realfract |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
185 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
186 |
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
|
187 |
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
|
188 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
189 |
lemma [code]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
190 |
"Ratreal r = split Realfract (quotient_of r)" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
191 |
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
|
192 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
193 |
lemma [code, code del]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
194 |
"(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) " |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
195 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
196 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
197 |
lemma [code, code del]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
198 |
"(plus :: real => real => real) = plus" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
199 |
.. |
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 |
lemma [code, code del]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
202 |
"(uminus :: real => real) = uminus" |
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 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
205 |
lemma [code, code del]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
206 |
"(minus :: real => real => real) = minus" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
207 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
208 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
209 |
lemma [code, code del]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
210 |
"(times :: real => real => real) = times" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
211 |
.. |
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 |
lemma [code, code del]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
214 |
"(divide :: real => real => real) = divide" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
215 |
.. |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
216 |
|
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
217 |
lemma [code]: |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
218 |
fixes r :: real |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
219 |
shows "inverse r = 1 / r" |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
220 |
by (fact inverse_eq_divide) |
140ae824ea4a
Code_Real_Approx_By_Float: remove code equations using Ratreal
hoelzl
parents:
51542
diff
changeset
|
221 |
|
46530 | 222 |
notepad |
223 |
begin |
|
224 |
have "cos (pi/2) = 0" by (rule cos_pi_half) |
|
225 |
moreover have "cos (pi/2) \<noteq> 0" by eval |
|
226 |
ultimately have "False" by blast |
|
227 |
end |
|
45483 | 228 |
|
229 |
end |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
47108
diff
changeset
|
230 |