src/HOL/Library/Code_Real_Approx_By_Float.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69906 55534affe445
child 70377 04f492d004fa
permissions -rw-r--r--
improved code equations taken over from AFP
wenzelm@63355
     1
(*  Title:      HOL/Library/Code_Real_Approx_By_Float.thy
wenzelm@63355
     2
    Author:     Florian Haftmann
wenzelm@63355
     3
    Author:     Johannes Hölzl
wenzelm@63355
     4
    Author:     Tobias Nipkow
wenzelm@63355
     5
*)
hoelzl@45483
     6
hoelzl@45483
     7
theory Code_Real_Approx_By_Float
wenzelm@51542
     8
imports Complex_Main Code_Target_Int
hoelzl@45483
     9
begin
hoelzl@45483
    10
wenzelm@63355
    11
text\<open>
wenzelm@63355
    12
  \<^bold>\<open>WARNING!\<close> This theory implements mathematical reals by machine reals
wenzelm@63355
    13
  (floats). This is inconsistent. See the proof of False at the end of the
wenzelm@63355
    14
  theory, where an equality on mathematical reals is (incorrectly) disproved
wenzelm@63355
    15
  by mapping it to machine reals.
hoelzl@45483
    16
wenzelm@63355
    17
  The \<^theory_text>\<open>value\<close> command cannot display real results yet.
hoelzl@45483
    18
wenzelm@63355
    19
  The only legitimate use of this theory is as a tool for code generation
wenzelm@63355
    20
  purposes.
wenzelm@63355
    21
\<close>
hoelzl@45483
    22
haftmann@52435
    23
code_printing
haftmann@52435
    24
  type_constructor real \<rightharpoonup>
haftmann@52435
    25
    (SML) "real"
haftmann@52435
    26
    and (OCaml) "float"
hoelzl@45483
    27
haftmann@52435
    28
code_printing
haftmann@52435
    29
  constant Ratreal \<rightharpoonup>
haftmann@52435
    30
    (SML) "error/ \"Bad constant: Ratreal\""
hoelzl@45483
    31
haftmann@52435
    32
code_printing
haftmann@52435
    33
  constant "0 :: real" \<rightharpoonup>
haftmann@52435
    34
    (SML) "0.0"
haftmann@52435
    35
    and (OCaml) "0.0"
hoelzl@45483
    36
haftmann@52435
    37
code_printing
haftmann@52435
    38
  constant "1 :: real" \<rightharpoonup>
haftmann@52435
    39
    (SML) "1.0"
haftmann@52435
    40
    and (OCaml) "1.0"
hoelzl@45483
    41
haftmann@52435
    42
code_printing
haftmann@52435
    43
  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    44
    (SML) "Real.== ((_), (_))"
haftmann@52435
    45
    and (OCaml) "Pervasives.(=)"
hoelzl@45483
    46
haftmann@52435
    47
code_printing
haftmann@52435
    48
  constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    49
    (SML) "Real.<= ((_), (_))"
haftmann@52435
    50
    and (OCaml) "Pervasives.(<=)"
hoelzl@45483
    51
haftmann@52435
    52
code_printing
haftmann@52435
    53
  constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    54
    (SML) "Real.< ((_), (_))"
haftmann@52435
    55
    and (OCaml) "Pervasives.(<)"
hoelzl@45483
    56
haftmann@52435
    57
code_printing
nipkow@67399
    58
  constant "(+) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    59
    (SML) "Real.+ ((_), (_))"
haftmann@52435
    60
    and (OCaml) "Pervasives.( +. )"
hoelzl@45483
    61
haftmann@52435
    62
code_printing
nipkow@69064
    63
  constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    64
    (SML) "Real.* ((_), (_))"
haftmann@52435
    65
    and (OCaml) "Pervasives.( *. )"
hoelzl@45483
    66
haftmann@52435
    67
code_printing
nipkow@67399
    68
  constant "(-) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    69
    (SML) "Real.- ((_), (_))"
haftmann@52435
    70
    and (OCaml) "Pervasives.( -. )"
hoelzl@45483
    71
haftmann@52435
    72
code_printing
haftmann@52435
    73
  constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    74
    (SML) "Real.~"
haftmann@52435
    75
    and (OCaml) "Pervasives.( ~-. )"
hoelzl@45483
    76
haftmann@52435
    77
code_printing
nipkow@67399
    78
  constant "(/) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    79
    (SML) "Real.'/ ((_), (_))"
haftmann@52435
    80
    and (OCaml) "Pervasives.( '/. )"
hoelzl@45483
    81
haftmann@52435
    82
code_printing
haftmann@52435
    83
  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    84
    (SML) "Real.== ((_:real), (_))"
hoelzl@45483
    85
haftmann@52435
    86
code_printing
haftmann@52435
    87
  constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    88
    (SML) "Math.sqrt"
haftmann@52435
    89
    and (OCaml) "Pervasives.sqrt"
hoelzl@45483
    90
declare sqrt_def[code del]
hoelzl@45483
    91
wenzelm@61115
    92
context
wenzelm@61115
    93
begin
wenzelm@61115
    94
wenzelm@63355
    95
qualified definition real_exp :: "real \<Rightarrow> real"
wenzelm@63355
    96
  where "real_exp = exp"
hoelzl@45483
    97
wenzelm@63355
    98
lemma exp_eq_real_exp [code_unfold]: "exp = real_exp"
hoelzl@45483
    99
  unfolding real_exp_def ..
hoelzl@45483
   100
wenzelm@61115
   101
end
wenzelm@61115
   102
haftmann@52435
   103
code_printing
wenzelm@61115
   104
  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
haftmann@52435
   105
    (SML) "Math.exp"
haftmann@52435
   106
    and (OCaml) "Pervasives.exp"
wenzelm@61115
   107
declare Code_Real_Approx_By_Float.real_exp_def[code del]
hoelzl@45483
   108
declare exp_def[code del]
hoelzl@45483
   109
haftmann@52435
   110
code_printing
haftmann@52435
   111
  constant ln \<rightharpoonup>
haftmann@52435
   112
    (SML) "Math.ln"
haftmann@52435
   113
    and (OCaml) "Pervasives.ln"
lp15@60017
   114
declare ln_real_def[code del]
hoelzl@45483
   115
haftmann@52435
   116
code_printing
haftmann@52435
   117
  constant cos \<rightharpoonup>
haftmann@52435
   118
    (SML) "Math.cos"
haftmann@52435
   119
    and (OCaml) "Pervasives.cos"
hoelzl@45483
   120
declare cos_def[code del]
hoelzl@45483
   121
haftmann@52435
   122
code_printing
haftmann@52435
   123
  constant sin \<rightharpoonup>
haftmann@52435
   124
    (SML) "Math.sin"
haftmann@52435
   125
    and (OCaml) "Pervasives.sin"
hoelzl@45483
   126
declare sin_def[code del]
hoelzl@45483
   127
haftmann@52435
   128
code_printing
haftmann@52435
   129
  constant pi \<rightharpoonup>
haftmann@52435
   130
    (SML) "Math.pi"
haftmann@52435
   131
    and (OCaml) "Pervasives.pi"
hoelzl@45483
   132
declare pi_def[code del]
hoelzl@45483
   133
haftmann@52435
   134
code_printing
haftmann@52435
   135
  constant arctan \<rightharpoonup>
haftmann@52435
   136
    (SML) "Math.atan"
haftmann@52435
   137
    and (OCaml) "Pervasives.atan"
hoelzl@45483
   138
declare arctan_def[code del]
hoelzl@45483
   139
haftmann@52435
   140
code_printing
haftmann@52435
   141
  constant arccos \<rightharpoonup>
haftmann@52435
   142
    (SML) "Math.scos"
haftmann@52435
   143
    and (OCaml) "Pervasives.acos"
hoelzl@45483
   144
declare arccos_def[code del]
hoelzl@45483
   145
haftmann@52435
   146
code_printing
haftmann@52435
   147
  constant arcsin \<rightharpoonup>
haftmann@52435
   148
    (SML) "Math.asin"
haftmann@52435
   149
    and (OCaml) "Pervasives.asin"
hoelzl@45483
   150
declare arcsin_def[code del]
hoelzl@45483
   151
wenzelm@63355
   152
definition real_of_integer :: "integer \<Rightarrow> real"
wenzelm@63355
   153
  where "real_of_integer = of_int \<circ> int_of_integer"
hoelzl@45483
   154
haftmann@52435
   155
code_printing
haftmann@52435
   156
  constant real_of_integer \<rightharpoonup>
haftmann@52435
   157
    (SML) "Real.fromInt"
haftmann@69906
   158
    and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
hoelzl@45483
   159
wenzelm@61115
   160
context
wenzelm@61115
   161
begin
wenzelm@61115
   162
wenzelm@63355
   163
qualified definition real_of_int :: "int \<Rightarrow> real"
wenzelm@63355
   164
  where [code_abbrev]: "real_of_int = of_int"
haftmann@51143
   165
wenzelm@63355
   166
lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int"
haftmann@51143
   167
  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
hoelzl@45483
   168
wenzelm@63355
   169
lemma [code_unfold del]: "0 \<equiv> (of_rat 0 :: real)"
huffman@47108
   170
  by simp
huffman@47108
   171
wenzelm@63355
   172
lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)"
huffman@47108
   173
  by simp
hoelzl@45483
   174
wenzelm@63355
   175
lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)"
huffman@47108
   176
  by simp
huffman@47108
   177
wenzelm@63355
   178
lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
huffman@47108
   179
  by simp
huffman@47108
   180
wenzelm@61115
   181
end
hoelzl@45483
   182
haftmann@52435
   183
code_printing
haftmann@52435
   184
  constant Ratreal \<rightharpoonup> (SML)
hoelzl@52403
   185
wenzelm@63355
   186
definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
wenzelm@63355
   187
  where "Realfract p q = of_int p / of_int q"
hoelzl@52403
   188
hoelzl@52403
   189
code_datatype Realfract
hoelzl@52403
   190
haftmann@52435
   191
code_printing
haftmann@52435
   192
  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
hoelzl@52403
   193
wenzelm@63355
   194
lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
hoelzl@52403
   195
  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
hoelzl@52403
   196
haftmann@66148
   197
declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
haftmann@66148
   198
  "plus :: real \<Rightarrow> real \<Rightarrow> real"
haftmann@66148
   199
  "uminus :: real \<Rightarrow> real"
haftmann@66148
   200
  "minus :: real \<Rightarrow> real \<Rightarrow> real"
haftmann@66148
   201
  "times :: real \<Rightarrow> real \<Rightarrow> real"
haftmann@66148
   202
  "divide :: real \<Rightarrow> real \<Rightarrow> real"]]
wenzelm@63355
   203
wenzelm@63355
   204
lemma [code]: "inverse r = 1 / r" for r :: real
hoelzl@52403
   205
  by (fact inverse_eq_divide)
hoelzl@52403
   206
haftmann@46530
   207
notepad
haftmann@46530
   208
begin
haftmann@46530
   209
  have "cos (pi/2) = 0" by (rule cos_pi_half)
haftmann@46530
   210
  moreover have "cos (pi/2) \<noteq> 0" by eval
wenzelm@63355
   211
  ultimately have False by blast
haftmann@46530
   212
end
hoelzl@45483
   213
hoelzl@45483
   214
end