src/HOL/Library/Code_Real_Approx_By_Float.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 61424 c3658c18b7bc
child 63355 7b23053be254
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
hoelzl@45483
     1
(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
hoelzl@45483
     2
hoelzl@45483
     3
theory Code_Real_Approx_By_Float
wenzelm@51542
     4
imports Complex_Main Code_Target_Int
hoelzl@45483
     5
begin
hoelzl@45483
     6
wenzelm@60500
     7
text\<open>\textbf{WARNING} This theory implements mathematical reals by machine
hoelzl@45483
     8
reals (floats). This is inconsistent. See the proof of False at the end of
hoelzl@45483
     9
the theory, where an equality on mathematical reals is (incorrectly)
hoelzl@45483
    10
disproved by mapping it to machine reals.
hoelzl@45483
    11
hoelzl@45483
    12
The value command cannot display real results yet.
hoelzl@45483
    13
hoelzl@45483
    14
The only legitimate use of this theory is as a tool for code generation
wenzelm@60500
    15
purposes.\<close>
hoelzl@45483
    16
haftmann@52435
    17
code_printing
haftmann@52435
    18
  type_constructor real \<rightharpoonup>
haftmann@52435
    19
    (SML) "real"
haftmann@52435
    20
    and (OCaml) "float"
hoelzl@45483
    21
haftmann@52435
    22
code_printing
haftmann@52435
    23
  constant Ratreal \<rightharpoonup>
haftmann@52435
    24
    (SML) "error/ \"Bad constant: Ratreal\""
hoelzl@45483
    25
haftmann@52435
    26
code_printing
haftmann@52435
    27
  constant "0 :: real" \<rightharpoonup>
haftmann@52435
    28
    (SML) "0.0"
haftmann@52435
    29
    and (OCaml) "0.0"
hoelzl@45483
    30
declare zero_real_code[code_unfold del]
hoelzl@45483
    31
haftmann@52435
    32
code_printing
haftmann@52435
    33
  constant "1 :: real" \<rightharpoonup>
haftmann@52435
    34
    (SML) "1.0"
haftmann@52435
    35
    and (OCaml) "1.0"
hoelzl@45483
    36
declare one_real_code[code_unfold del]
hoelzl@45483
    37
haftmann@52435
    38
code_printing
haftmann@52435
    39
  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    40
    (SML) "Real.== ((_), (_))"
haftmann@52435
    41
    and (OCaml) "Pervasives.(=)"
hoelzl@45483
    42
haftmann@52435
    43
code_printing
haftmann@52435
    44
  constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    45
    (SML) "Real.<= ((_), (_))"
haftmann@52435
    46
    and (OCaml) "Pervasives.(<=)"
hoelzl@45483
    47
haftmann@52435
    48
code_printing
haftmann@52435
    49
  constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    50
    (SML) "Real.< ((_), (_))"
haftmann@52435
    51
    and (OCaml) "Pervasives.(<)"
hoelzl@45483
    52
haftmann@52435
    53
code_printing
haftmann@52435
    54
  constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    55
    (SML) "Real.+ ((_), (_))"
haftmann@52435
    56
    and (OCaml) "Pervasives.( +. )"
hoelzl@45483
    57
haftmann@52435
    58
code_printing
haftmann@52435
    59
  constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    60
    (SML) "Real.* ((_), (_))"
haftmann@52435
    61
    and (OCaml) "Pervasives.( *. )"
hoelzl@45483
    62
haftmann@52435
    63
code_printing
haftmann@52435
    64
  constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    65
    (SML) "Real.- ((_), (_))"
haftmann@52435
    66
    and (OCaml) "Pervasives.( -. )"
hoelzl@45483
    67
haftmann@52435
    68
code_printing
haftmann@52435
    69
  constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    70
    (SML) "Real.~"
haftmann@52435
    71
    and (OCaml) "Pervasives.( ~-. )"
hoelzl@45483
    72
haftmann@52435
    73
code_printing
haftmann@52435
    74
  constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    75
    (SML) "Real.'/ ((_), (_))"
haftmann@52435
    76
    and (OCaml) "Pervasives.( '/. )"
hoelzl@45483
    77
haftmann@52435
    78
code_printing
haftmann@52435
    79
  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
    80
    (SML) "Real.== ((_:real), (_))"
hoelzl@45483
    81
haftmann@52435
    82
code_printing
haftmann@52435
    83
  constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
haftmann@52435
    84
    (SML) "Math.sqrt"
haftmann@52435
    85
    and (OCaml) "Pervasives.sqrt"
hoelzl@45483
    86
declare sqrt_def[code del]
hoelzl@45483
    87
wenzelm@61115
    88
context
wenzelm@61115
    89
begin
wenzelm@61115
    90
wenzelm@61115
    91
qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
hoelzl@45483
    92
hoelzl@45483
    93
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
hoelzl@45483
    94
  unfolding real_exp_def ..
hoelzl@45483
    95
wenzelm@61115
    96
end
wenzelm@61115
    97
haftmann@52435
    98
code_printing
wenzelm@61115
    99
  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
haftmann@52435
   100
    (SML) "Math.exp"
haftmann@52435
   101
    and (OCaml) "Pervasives.exp"
wenzelm@61115
   102
declare Code_Real_Approx_By_Float.real_exp_def[code del]
hoelzl@45483
   103
declare exp_def[code del]
hoelzl@45483
   104
haftmann@52435
   105
code_printing
haftmann@52435
   106
  constant ln \<rightharpoonup>
haftmann@52435
   107
    (SML) "Math.ln"
haftmann@52435
   108
    and (OCaml) "Pervasives.ln"
lp15@60017
   109
declare ln_real_def[code del]
hoelzl@45483
   110
haftmann@52435
   111
code_printing
haftmann@52435
   112
  constant cos \<rightharpoonup>
haftmann@52435
   113
    (SML) "Math.cos"
haftmann@52435
   114
    and (OCaml) "Pervasives.cos"
hoelzl@45483
   115
declare cos_def[code del]
hoelzl@45483
   116
haftmann@52435
   117
code_printing
haftmann@52435
   118
  constant sin \<rightharpoonup>
haftmann@52435
   119
    (SML) "Math.sin"
haftmann@52435
   120
    and (OCaml) "Pervasives.sin"
hoelzl@45483
   121
declare sin_def[code del]
hoelzl@45483
   122
haftmann@52435
   123
code_printing
haftmann@52435
   124
  constant pi \<rightharpoonup>
haftmann@52435
   125
    (SML) "Math.pi"
haftmann@52435
   126
    and (OCaml) "Pervasives.pi"
hoelzl@45483
   127
declare pi_def[code del]
hoelzl@45483
   128
haftmann@52435
   129
code_printing
haftmann@52435
   130
  constant arctan \<rightharpoonup>
haftmann@52435
   131
    (SML) "Math.atan"
haftmann@52435
   132
    and (OCaml) "Pervasives.atan"
hoelzl@45483
   133
declare arctan_def[code del]
hoelzl@45483
   134
haftmann@52435
   135
code_printing
haftmann@52435
   136
  constant arccos \<rightharpoonup>
haftmann@52435
   137
    (SML) "Math.scos"
haftmann@52435
   138
    and (OCaml) "Pervasives.acos"
hoelzl@45483
   139
declare arccos_def[code del]
hoelzl@45483
   140
haftmann@52435
   141
code_printing
haftmann@52435
   142
  constant arcsin \<rightharpoonup>
haftmann@52435
   143
    (SML) "Math.asin"
haftmann@52435
   144
    and (OCaml) "Pervasives.asin"
hoelzl@45483
   145
declare arcsin_def[code del]
hoelzl@45483
   146
haftmann@51143
   147
definition real_of_integer :: "integer \<Rightarrow> real" where
haftmann@51143
   148
  "real_of_integer = of_int \<circ> int_of_integer"
hoelzl@45483
   149
haftmann@52435
   150
code_printing
haftmann@52435
   151
  constant real_of_integer \<rightharpoonup>
haftmann@52435
   152
    (SML) "Real.fromInt"
haftmann@52435
   153
    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
hoelzl@45483
   154
wenzelm@61115
   155
context
wenzelm@61115
   156
begin
wenzelm@61115
   157
wenzelm@61115
   158
qualified definition real_of_int :: "int \<Rightarrow> real" where
haftmann@51143
   159
  [code_abbrev]: "real_of_int = of_int"
haftmann@51143
   160
haftmann@51143
   161
lemma [code]:
haftmann@51143
   162
  "real_of_int = real_of_integer \<circ> integer_of_int"
haftmann@51143
   163
  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
hoelzl@45483
   164
huffman@47108
   165
lemma [code_unfold del]:
huffman@47108
   166
  "0 \<equiv> (of_rat 0 :: real)"
huffman@47108
   167
  by simp
huffman@47108
   168
huffman@47108
   169
lemma [code_unfold del]:
huffman@47108
   170
  "1 \<equiv> (of_rat 1 :: real)"
huffman@47108
   171
  by simp
hoelzl@45483
   172
huffman@47108
   173
lemma [code_unfold del]:
huffman@47108
   174
  "numeral k \<equiv> (of_rat (numeral k) :: real)"
huffman@47108
   175
  by simp
huffman@47108
   176
huffman@47108
   177
lemma [code_unfold del]:
haftmann@54489
   178
  "- 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
hoelzl@52403
   186
definition Realfract :: "int => int => real"
hoelzl@52403
   187
where
hoelzl@52403
   188
  "Realfract p q = of_int p / of_int q"
hoelzl@52403
   189
hoelzl@52403
   190
code_datatype Realfract
hoelzl@52403
   191
haftmann@52435
   192
code_printing
haftmann@52435
   193
  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
hoelzl@52403
   194
hoelzl@52403
   195
lemma [code]:
haftmann@61424
   196
  "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
hoelzl@52403
   199
lemma [code, code del]:
hoelzl@52403
   200
  "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
hoelzl@52403
   201
  ..
hoelzl@52403
   202
hoelzl@52403
   203
lemma [code, code del]:
hoelzl@52403
   204
  "(plus :: real => real => real) = plus"
hoelzl@52403
   205
  ..
hoelzl@52403
   206
hoelzl@52403
   207
lemma [code, code del]:
hoelzl@52403
   208
  "(uminus :: real => real) = uminus"
hoelzl@52403
   209
  ..
hoelzl@52403
   210
hoelzl@52403
   211
lemma [code, code del]:
hoelzl@52403
   212
  "(minus :: real => real => real) = minus"
hoelzl@52403
   213
  ..
hoelzl@52403
   214
hoelzl@52403
   215
lemma [code, code del]:
hoelzl@52403
   216
  "(times :: real => real => real) = times"
hoelzl@52403
   217
  ..
hoelzl@52403
   218
hoelzl@52403
   219
lemma [code, code del]:
hoelzl@52403
   220
  "(divide :: real => real => real) = divide"
hoelzl@52403
   221
  ..
hoelzl@52403
   222
hoelzl@52403
   223
lemma [code]:
hoelzl@52403
   224
  fixes r :: real
hoelzl@52403
   225
  shows "inverse r = 1 / r"
hoelzl@52403
   226
  by (fact inverse_eq_divide)
hoelzl@52403
   227
haftmann@46530
   228
notepad
haftmann@46530
   229
begin
haftmann@46530
   230
  have "cos (pi/2) = 0" by (rule cos_pi_half)
haftmann@46530
   231
  moreover have "cos (pi/2) \<noteq> 0" by eval
haftmann@46530
   232
  ultimately have "False" by blast
haftmann@46530
   233
end
hoelzl@45483
   234
hoelzl@45483
   235
end
haftmann@51143
   236