author | Christian Sternagel |
Thu, 13 Dec 2012 13:11:38 +0100 | |
changeset 50516 | ed6b40d15d1c |
parent 47108 | 2a1953f0d20d |
child 51143 | 0a2371e7ced3 |
permissions | -rw-r--r-- |
45483 | 1 |
(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *) |
2 |
||
3 |
theory Code_Real_Approx_By_Float |
|
4 |
imports Complex_Main "~~/src/HOL/Library/Code_Integer" |
|
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 |
||
17 |
code_type real |
|
18 |
(SML "real") |
|
19 |
(OCaml "float") |
|
20 |
||
21 |
code_const Ratreal |
|
22 |
(SML "error/ \"Bad constant: Ratreal\"") |
|
23 |
||
24 |
code_const "0 :: real" |
|
25 |
(SML "0.0") |
|
26 |
(OCaml "0.0") |
|
27 |
declare zero_real_code[code_unfold del] |
|
28 |
||
29 |
code_const "1 :: real" |
|
30 |
(SML "1.0") |
|
31 |
(OCaml "1.0") |
|
32 |
declare one_real_code[code_unfold del] |
|
33 |
||
34 |
code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" |
|
35 |
(SML "Real.== ((_), (_))") |
|
36 |
(OCaml "Pervasives.(=)") |
|
37 |
||
38 |
code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" |
|
39 |
(SML "Real.<= ((_), (_))") |
|
40 |
(OCaml "Pervasives.(<=)") |
|
41 |
||
42 |
code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" |
|
43 |
(SML "Real.< ((_), (_))") |
|
44 |
(OCaml "Pervasives.(<)") |
|
45 |
||
46 |
code_const "op + :: real \<Rightarrow> real \<Rightarrow> real" |
|
47 |
(SML "Real.+ ((_), (_))") |
|
48 |
(OCaml "Pervasives.( +. )") |
|
49 |
||
50 |
code_const "op * :: real \<Rightarrow> real \<Rightarrow> real" |
|
51 |
(SML "Real.* ((_), (_))") |
|
52 |
(OCaml "Pervasives.( *. )") |
|
53 |
||
54 |
code_const "op - :: real \<Rightarrow> real \<Rightarrow> real" |
|
55 |
(SML "Real.- ((_), (_))") |
|
56 |
(OCaml "Pervasives.( -. )") |
|
57 |
||
58 |
code_const "uminus :: real \<Rightarrow> real" |
|
59 |
(SML "Real.~") |
|
60 |
(OCaml "Pervasives.( ~-. )") |
|
61 |
||
62 |
code_const "op / :: real \<Rightarrow> real \<Rightarrow> real" |
|
63 |
(SML "Real.'/ ((_), (_))") |
|
64 |
(OCaml "Pervasives.( '/. )") |
|
65 |
||
66 |
code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" |
|
67 |
(SML "Real.== ((_:real), (_))") |
|
68 |
||
69 |
code_const "sqrt :: real \<Rightarrow> real" |
|
70 |
(SML "Math.sqrt") |
|
71 |
(OCaml "Pervasives.sqrt") |
|
72 |
declare sqrt_def[code del] |
|
73 |
||
74 |
definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp" |
|
75 |
||
76 |
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp" |
|
77 |
unfolding real_exp_def .. |
|
78 |
||
79 |
code_const real_exp |
|
80 |
(SML "Math.exp") |
|
81 |
(OCaml "Pervasives.exp") |
|
82 |
declare real_exp_def[code del] |
|
83 |
declare exp_def[code del] |
|
84 |
||
85 |
hide_const (open) real_exp |
|
86 |
||
87 |
code_const ln |
|
88 |
(SML "Math.ln") |
|
89 |
(OCaml "Pervasives.ln") |
|
90 |
declare ln_def[code del] |
|
91 |
||
92 |
code_const cos |
|
93 |
(SML "Math.cos") |
|
94 |
(OCaml "Pervasives.cos") |
|
95 |
declare cos_def[code del] |
|
96 |
||
97 |
code_const sin |
|
98 |
(SML "Math.sin") |
|
99 |
(OCaml "Pervasives.sin") |
|
100 |
declare sin_def[code del] |
|
101 |
||
102 |
code_const pi |
|
103 |
(SML "Math.pi") |
|
104 |
(OCaml "Pervasives.pi") |
|
105 |
declare pi_def[code del] |
|
106 |
||
107 |
code_const arctan |
|
108 |
(SML "Math.atan") |
|
109 |
(OCaml "Pervasives.atan") |
|
110 |
declare arctan_def[code del] |
|
111 |
||
112 |
code_const arccos |
|
113 |
(SML "Math.scos") |
|
114 |
(OCaml "Pervasives.acos") |
|
115 |
declare arccos_def[code del] |
|
116 |
||
117 |
code_const arcsin |
|
118 |
(SML "Math.asin") |
|
119 |
(OCaml "Pervasives.asin") |
|
120 |
declare arcsin_def[code del] |
|
121 |
||
122 |
definition real_of_int :: "int \<Rightarrow> real" where |
|
123 |
"real_of_int \<equiv> of_int" |
|
124 |
||
125 |
code_const real_of_int |
|
126 |
(SML "Real.fromInt") |
|
127 |
(OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))") |
|
128 |
||
129 |
lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int" |
|
130 |
unfolding real_of_int_def .. |
|
131 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
132 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
133 |
"0 \<equiv> (of_rat 0 :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
134 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
135 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
136 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
137 |
"1 \<equiv> (of_rat 1 :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
138 |
by simp |
45483 | 139 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
140 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
141 |
"numeral k \<equiv> (of_rat (numeral k) :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
142 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
143 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
144 |
lemma [code_unfold del]: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
145 |
"neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
146 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
147 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46530
diff
changeset
|
148 |
hide_const (open) real_of_int |
45483 | 149 |
|
46530 | 150 |
notepad |
151 |
begin |
|
152 |
have "cos (pi/2) = 0" by (rule cos_pi_half) |
|
153 |
moreover have "cos (pi/2) \<noteq> 0" by eval |
|
154 |
ultimately have "False" by blast |
|
155 |
end |
|
45483 | 156 |
|
157 |
end |