author | haftmann |
Wed, 10 Aug 2022 18:26:22 +0000 | |
changeset 75800 | a21debbc7074 |
parent 75799 | f1141438b4db |
permissions | -rw-r--r-- |
63355 | 1 |
(* Title: HOL/Library/Code_Real_Approx_By_Float.thy |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
2 |
Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
3 |
Author: Jose Divasón <jose.divasonm at unirioja.es> |
63355 | 4 |
Author: Florian Haftmann |
5 |
Author: Johannes Hölzl |
|
6 |
Author: Tobias Nipkow |
|
7 |
*) |
|
45483 | 8 |
|
9 |
theory Code_Real_Approx_By_Float |
|
51542 | 10 |
imports Complex_Main Code_Target_Int |
45483 | 11 |
begin |
12 |
||
63355 | 13 |
text\<open> |
14 |
\<^bold>\<open>WARNING!\<close> This theory implements mathematical reals by machine reals |
|
15 |
(floats). This is inconsistent. See the proof of False at the end of the |
|
16 |
theory, where an equality on mathematical reals is (incorrectly) disproved |
|
17 |
by mapping it to machine reals. |
|
45483 | 18 |
|
63355 | 19 |
The \<^theory_text>\<open>value\<close> command cannot display real results yet. |
45483 | 20 |
|
63355 | 21 |
The only legitimate use of this theory is as a tool for code generation |
22 |
purposes. |
|
23 |
\<close> |
|
45483 | 24 |
|
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
25 |
context |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
26 |
begin |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
27 |
|
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
28 |
qualified definition real_of_integer :: "integer \<Rightarrow> real" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
29 |
where [code_abbrev]: "real_of_integer = of_int \<circ> int_of_integer" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
30 |
|
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
31 |
end |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
32 |
|
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
33 |
code_datatype Code_Real_Approx_By_Float.real_of_integer \<open>(/) :: real \<Rightarrow> real \<Rightarrow> real\<close> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
34 |
|
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
35 |
lemma [code_unfold del]: "numeral k \<equiv> real_of_rat (numeral k)" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
36 |
by simp |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
37 |
|
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
38 |
lemma [code_unfold del]: "- numeral k \<equiv> real_of_rat (- numeral k)" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
39 |
by simp |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
40 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
41 |
context |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
42 |
begin |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
43 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
44 |
qualified definition real_of_int :: \<open>int \<Rightarrow> real\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
45 |
where [code_abbrev]: \<open>real_of_int = of_int\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
46 |
|
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
47 |
lemma [code]: "real_of_int = Code_Real_Approx_By_Float.real_of_integer \<circ> integer_of_int" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
48 |
by (simp add: fun_eq_iff Code_Real_Approx_By_Float.real_of_integer_def real_of_int_def) |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
49 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
50 |
qualified definition exp_real :: \<open>real \<Rightarrow> real\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
51 |
where [code_abbrev, code del]: \<open>exp_real = exp\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
52 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
53 |
qualified definition sin_real :: \<open>real \<Rightarrow> real\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
54 |
where [code_abbrev, code del]: \<open>sin_real = sin\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
55 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
56 |
qualified definition cos_real :: \<open>real \<Rightarrow> real\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
57 |
where [code_abbrev, code del]: \<open>cos_real = cos\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
58 |
|
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
59 |
qualified definition tan_real :: \<open>real \<Rightarrow> real\<close> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
60 |
where [code_abbrev, code del]: \<open>tan_real = tan\<close> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
61 |
|
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
62 |
end |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
63 |
|
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
64 |
lemma [code]: \<open>Ratreal r = (case quotient_of r of (p, q) \<Rightarrow> real_of_int p / real_of_int q)\<close> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
65 |
by (cases r) (simp add: quotient_of_Fract of_rat_rat) |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
66 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
67 |
lemma [code]: \<open>inverse r = 1 / r\<close> for r :: real |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
68 |
by (fact inverse_eq_divide) |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
69 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
70 |
declare [[code drop: \<open>HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool\<close> |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
71 |
\<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
72 |
\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
73 |
\<open>plus :: real \<Rightarrow> real \<Rightarrow> real\<close> |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
74 |
\<open>times :: real \<Rightarrow> real \<Rightarrow> real\<close> |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
75 |
\<open>uminus :: real \<Rightarrow> real\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
76 |
\<open>minus :: real \<Rightarrow> real \<Rightarrow> real\<close> |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
77 |
\<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close> |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
78 |
sqrt |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
79 |
\<open>ln :: real \<Rightarrow> real\<close> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
80 |
pi |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
81 |
arcsin |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
82 |
arccos |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
83 |
arctan]] |
75799
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
84 |
|
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
85 |
code_reserved SML Real |
f1141438b4db
more correct approximation (contributed by Achim Brucker)
Achim D. Brucker <adbrucker@0x5f.org>
parents:
70377
diff
changeset
|
86 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52403
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
(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
|
90 |
and (OCaml) "float" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
91 |
and (Haskell) "Prelude.Double" (*Double precision*) |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
92 |
| constant "0 :: 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
|
93 |
(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
|
94 |
and (OCaml) "0.0" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
95 |
and (Haskell) "0.0" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
96 |
| constant "1 :: 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
|
97 |
(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
|
98 |
and (OCaml) "1.0" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
99 |
and (Haskell) "1.0" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
100 |
| constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<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
|
101 |
(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
|
102 |
and (OCaml) "Pervasives.(=)" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
103 |
and (Haskell) infix 4 "==" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
104 |
| class_instance real :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*) |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
105 |
| constant "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool" \<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
|
106 |
(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
|
107 |
and (OCaml) "Pervasives.(<=)" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
108 |
and (Haskell) infix 4 "<=" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
109 |
| constant "(<) :: real \<Rightarrow> real \<Rightarrow> bool" \<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
|
110 |
(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
|
111 |
and (OCaml) "Pervasives.(<)" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
112 |
and (Haskell) infix 4 "<" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
113 |
| 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
|
114 |
(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
|
115 |
and (OCaml) "Pervasives.( +. )" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
116 |
and (Haskell) infixl 6 "+" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
117 |
| 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
|
118 |
(SML) "Real.* ((_), (_))" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
119 |
and (Haskell) infixl 7 "*" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
120 |
| constant "uminus :: 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
|
121 |
(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
|
122 |
and (OCaml) "Pervasives.( ~-. )" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
123 |
and (Haskell) "negate" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
124 |
| constant "(-) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
125 |
(SML) "Real.- ((_), (_))" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
126 |
and (OCaml) "Pervasives.( -. )" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
127 |
and (Haskell) infixl 6 "-" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
128 |
| 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
|
129 |
(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
|
130 |
and (OCaml) "Pervasives.( '/. )" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
131 |
and (Haskell) infixl 7 "/" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
132 |
| constant "sqrt :: 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
|
133 |
(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
|
134 |
and (OCaml) "Pervasives.sqrt" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
135 |
and (Haskell) "Prelude.sqrt" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
136 |
| constant Code_Real_Approx_By_Float.exp_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
|
137 |
(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
|
138 |
and (OCaml) "Pervasives.exp" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
139 |
and (Haskell) "Prelude.exp" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
140 |
| constant ln \<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
|
141 |
(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
|
142 |
and (OCaml) "Pervasives.ln" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
143 |
and (Haskell) "Prelude.log" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
144 |
| constant Code_Real_Approx_By_Float.sin_real \<rightharpoonup> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
145 |
(SML) "Math.sin" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
146 |
and (OCaml) "Pervasives.sin" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
147 |
and (Haskell) "Prelude.sin" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
148 |
| constant Code_Real_Approx_By_Float.cos_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
|
149 |
(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
|
150 |
and (OCaml) "Pervasives.cos" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
151 |
and (Haskell) "Prelude.cos" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
152 |
| constant Code_Real_Approx_By_Float.tan_real \<rightharpoonup> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
153 |
(SML) "Math.tan" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
154 |
and (OCaml) "Pervasives.tan" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
155 |
and (Haskell) "Prelude.tan" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
156 |
| constant pi \<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
|
157 |
(SML) "Math.pi" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
158 |
(*missing in OCaml*) |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
159 |
and (Haskell) "Prelude.pi" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
160 |
| constant arcsin \<rightharpoonup> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
161 |
(SML) "Math.asin" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
162 |
and (OCaml) "Pervasives.asin" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
163 |
and (Haskell) "Prelude.asin" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
164 |
| constant arccos \<rightharpoonup> |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
165 |
(SML) "Math.scos" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
166 |
and (OCaml) "Pervasives.acos" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
167 |
and (Haskell) "Prelude.acos" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
168 |
| constant arctan \<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
|
169 |
(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
|
170 |
and (OCaml) "Pervasives.atan" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
171 |
and (Haskell) "Prelude.atan" |
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
172 |
| constant Code_Real_Approx_By_Float.real_of_integer \<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
|
173 |
(SML) "Real.fromInt" |
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69064
diff
changeset
|
174 |
and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))" |
75800
a21debbc7074
Further streamlining of quick-and-dirty evaluation.
haftmann
parents:
75799
diff
changeset
|
175 |
and (Haskell) "Prelude.fromIntegral (_)" |
45483 | 176 |
|
46530 | 177 |
notepad |
178 |
begin |
|
179 |
have "cos (pi/2) = 0" by (rule cos_pi_half) |
|
180 |
moreover have "cos (pi/2) \<noteq> 0" by eval |
|
63355 | 181 |
ultimately have False by blast |
46530 | 182 |
end |
45483 | 183 |
|
184 |
end |