src/HOL/Library/Code_Real_Approx_By_Float.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63355 7b23053be254
child 66147 9225370db5f0
permissions -rw-r--r--
tuned proofs;
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
declare zero_real_code[code_unfold del]
hoelzl@45483
    37
haftmann@52435
    38
code_printing
haftmann@52435
    39
  constant "1 :: real" \<rightharpoonup>
haftmann@52435
    40
    (SML) "1.0"
haftmann@52435
    41
    and (OCaml) "1.0"
hoelzl@45483
    42
declare one_real_code[code_unfold del]
hoelzl@45483
    43
haftmann@52435
    44
code_printing
haftmann@52435
    45
  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    46
    (SML) "Real.== ((_), (_))"
haftmann@52435
    47
    and (OCaml) "Pervasives.(=)"
hoelzl@45483
    48
haftmann@52435
    49
code_printing
haftmann@52435
    50
  constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    51
    (SML) "Real.<= ((_), (_))"
haftmann@52435
    52
    and (OCaml) "Pervasives.(<=)"
hoelzl@45483
    53
haftmann@52435
    54
code_printing
haftmann@52435
    55
  constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    56
    (SML) "Real.< ((_), (_))"
haftmann@52435
    57
    and (OCaml) "Pervasives.(<)"
hoelzl@45483
    58
haftmann@52435
    59
code_printing
haftmann@52435
    60
  constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    61
    (SML) "Real.+ ((_), (_))"
haftmann@52435
    62
    and (OCaml) "Pervasives.( +. )"
hoelzl@45483
    63
haftmann@52435
    64
code_printing
haftmann@52435
    65
  constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    66
    (SML) "Real.* ((_), (_))"
haftmann@52435
    67
    and (OCaml) "Pervasives.( *. )"
hoelzl@45483
    68
haftmann@52435
    69
code_printing
haftmann@52435
    70
  constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    71
    (SML) "Real.- ((_), (_))"
haftmann@52435
    72
    and (OCaml) "Pervasives.( -. )"
hoelzl@45483
    73
haftmann@52435
    74
code_printing
haftmann@52435
    75
  constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    76
    (SML) "Real.~"
haftmann@52435
    77
    and (OCaml) "Pervasives.( ~-. )"
hoelzl@45483
    78
haftmann@52435
    79
code_printing
haftmann@52435
    80
  constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    81
    (SML) "Real.'/ ((_), (_))"
haftmann@52435
    82
    and (OCaml) "Pervasives.( '/. )"
hoelzl@45483
    83
haftmann@52435
    84
code_printing
haftmann@52435
    85
  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    86
    (SML) "Real.== ((_:real), (_))"
hoelzl@45483
    87
haftmann@52435
    88
code_printing
haftmann@52435
    89
  constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    90
    (SML) "Math.sqrt"
haftmann@52435
    91
    and (OCaml) "Pervasives.sqrt"
hoelzl@45483
    92
declare sqrt_def[code del]
hoelzl@45483
    93
wenzelm@61115
    94
context
wenzelm@61115
    95
begin
wenzelm@61115
    96
wenzelm@63355
    97
qualified definition real_exp :: "real \<Rightarrow> real"
wenzelm@63355
    98
  where "real_exp = exp"
hoelzl@45483
    99
wenzelm@63355
   100
lemma exp_eq_real_exp [code_unfold]: "exp = real_exp"
hoelzl@45483
   101
  unfolding real_exp_def ..
hoelzl@45483
   102
wenzelm@61115
   103
end
wenzelm@61115
   104
haftmann@52435
   105
code_printing
wenzelm@61115
   106
  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
haftmann@52435
   107
    (SML) "Math.exp"
haftmann@52435
   108
    and (OCaml) "Pervasives.exp"
wenzelm@61115
   109
declare Code_Real_Approx_By_Float.real_exp_def[code del]
hoelzl@45483
   110
declare exp_def[code del]
hoelzl@45483
   111
haftmann@52435
   112
code_printing
haftmann@52435
   113
  constant ln \<rightharpoonup>
haftmann@52435
   114
    (SML) "Math.ln"
haftmann@52435
   115
    and (OCaml) "Pervasives.ln"
lp15@60017
   116
declare ln_real_def[code del]
hoelzl@45483
   117
haftmann@52435
   118
code_printing
haftmann@52435
   119
  constant cos \<rightharpoonup>
haftmann@52435
   120
    (SML) "Math.cos"
haftmann@52435
   121
    and (OCaml) "Pervasives.cos"
hoelzl@45483
   122
declare cos_def[code del]
hoelzl@45483
   123
haftmann@52435
   124
code_printing
haftmann@52435
   125
  constant sin \<rightharpoonup>
haftmann@52435
   126
    (SML) "Math.sin"
haftmann@52435
   127
    and (OCaml) "Pervasives.sin"
hoelzl@45483
   128
declare sin_def[code del]
hoelzl@45483
   129
haftmann@52435
   130
code_printing
haftmann@52435
   131
  constant pi \<rightharpoonup>
haftmann@52435
   132
    (SML) "Math.pi"
haftmann@52435
   133
    and (OCaml) "Pervasives.pi"
hoelzl@45483
   134
declare pi_def[code del]
hoelzl@45483
   135
haftmann@52435
   136
code_printing
haftmann@52435
   137
  constant arctan \<rightharpoonup>
haftmann@52435
   138
    (SML) "Math.atan"
haftmann@52435
   139
    and (OCaml) "Pervasives.atan"
hoelzl@45483
   140
declare arctan_def[code del]
hoelzl@45483
   141
haftmann@52435
   142
code_printing
haftmann@52435
   143
  constant arccos \<rightharpoonup>
haftmann@52435
   144
    (SML) "Math.scos"
haftmann@52435
   145
    and (OCaml) "Pervasives.acos"
hoelzl@45483
   146
declare arccos_def[code del]
hoelzl@45483
   147
haftmann@52435
   148
code_printing
haftmann@52435
   149
  constant arcsin \<rightharpoonup>
haftmann@52435
   150
    (SML) "Math.asin"
haftmann@52435
   151
    and (OCaml) "Pervasives.asin"
hoelzl@45483
   152
declare arcsin_def[code del]
hoelzl@45483
   153
wenzelm@63355
   154
definition real_of_integer :: "integer \<Rightarrow> real"
wenzelm@63355
   155
  where "real_of_integer = of_int \<circ> int_of_integer"
hoelzl@45483
   156
haftmann@52435
   157
code_printing
haftmann@52435
   158
  constant real_of_integer \<rightharpoonup>
haftmann@52435
   159
    (SML) "Real.fromInt"
haftmann@52435
   160
    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
hoelzl@45483
   161
wenzelm@61115
   162
context
wenzelm@61115
   163
begin
wenzelm@61115
   164
wenzelm@63355
   165
qualified definition real_of_int :: "int \<Rightarrow> real"
wenzelm@63355
   166
  where [code_abbrev]: "real_of_int = of_int"
haftmann@51143
   167
wenzelm@63355
   168
lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int"
haftmann@51143
   169
  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
hoelzl@45483
   170
wenzelm@63355
   171
lemma [code_unfold del]: "0 \<equiv> (of_rat 0 :: real)"
huffman@47108
   172
  by simp
huffman@47108
   173
wenzelm@63355
   174
lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)"
huffman@47108
   175
  by simp
hoelzl@45483
   176
wenzelm@63355
   177
lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)"
huffman@47108
   178
  by simp
huffman@47108
   179
wenzelm@63355
   180
lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
huffman@47108
   181
  by simp
huffman@47108
   182
wenzelm@61115
   183
end
hoelzl@45483
   184
haftmann@52435
   185
code_printing
haftmann@52435
   186
  constant Ratreal \<rightharpoonup> (SML)
hoelzl@52403
   187
wenzelm@63355
   188
definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
wenzelm@63355
   189
  where "Realfract p q = of_int p / of_int q"
hoelzl@52403
   190
hoelzl@52403
   191
code_datatype Realfract
hoelzl@52403
   192
haftmann@52435
   193
code_printing
haftmann@52435
   194
  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
hoelzl@52403
   195
wenzelm@63355
   196
lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
hoelzl@52403
   197
  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
hoelzl@52403
   198
wenzelm@63355
   199
lemma [code, code del]: "(HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool) = (HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool)"
hoelzl@52403
   200
  ..
hoelzl@52403
   201
wenzelm@63355
   202
lemma [code, code del]: "(plus :: real \<Rightarrow> real \<Rightarrow> real) = plus"
hoelzl@52403
   203
  ..
hoelzl@52403
   204
wenzelm@63355
   205
lemma [code, code del]: "(uminus :: real \<Rightarrow> real) = uminus"
hoelzl@52403
   206
  ..
hoelzl@52403
   207
wenzelm@63355
   208
lemma [code, code del]: "(minus :: real \<Rightarrow> real \<Rightarrow> real) = minus"
hoelzl@52403
   209
  ..
hoelzl@52403
   210
wenzelm@63355
   211
lemma [code, code del]: "(times :: real \<Rightarrow> real \<Rightarrow> real) = times"
hoelzl@52403
   212
  ..
hoelzl@52403
   213
wenzelm@63355
   214
lemma [code, code del]: "(divide :: real \<Rightarrow> real \<Rightarrow> real) = divide"
wenzelm@63355
   215
  ..
wenzelm@63355
   216
wenzelm@63355
   217
lemma [code]: "inverse r = 1 / r" for r :: real
hoelzl@52403
   218
  by (fact inverse_eq_divide)
hoelzl@52403
   219
haftmann@46530
   220
notepad
haftmann@46530
   221
begin
haftmann@46530
   222
  have "cos (pi/2) = 0" by (rule cos_pi_half)
haftmann@46530
   223
  moreover have "cos (pi/2) \<noteq> 0" by eval
wenzelm@63355
   224
  ultimately have False by blast
haftmann@46530
   225
end
hoelzl@45483
   226
hoelzl@45483
   227
end