src/HOL/Library/Code_Real_Approx_By_Float.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 52435 6646bb548c6b
child 54489 03ff4d1e6784
permissions -rw-r--r--
more simplification rules on unary and binary minus
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
hoelzl@45483
     7
text{* \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
hoelzl@45483
    15
purposes. *}
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
hoelzl@45483
    88
definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
hoelzl@45483
    89
hoelzl@45483
    90
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
hoelzl@45483
    91
  unfolding real_exp_def ..
hoelzl@45483
    92
haftmann@52435
    93
code_printing
haftmann@52435
    94
  constant real_exp \<rightharpoonup>
haftmann@52435
    95
    (SML) "Math.exp"
haftmann@52435
    96
    and (OCaml) "Pervasives.exp"
hoelzl@45483
    97
declare real_exp_def[code del]
hoelzl@45483
    98
declare exp_def[code del]
hoelzl@45483
    99
hoelzl@45483
   100
hide_const (open) real_exp
hoelzl@45483
   101
haftmann@52435
   102
code_printing
haftmann@52435
   103
  constant ln \<rightharpoonup>
haftmann@52435
   104
    (SML) "Math.ln"
haftmann@52435
   105
    and (OCaml) "Pervasives.ln"
hoelzl@45483
   106
declare ln_def[code del]
hoelzl@45483
   107
haftmann@52435
   108
code_printing
haftmann@52435
   109
  constant cos \<rightharpoonup>
haftmann@52435
   110
    (SML) "Math.cos"
haftmann@52435
   111
    and (OCaml) "Pervasives.cos"
hoelzl@45483
   112
declare cos_def[code del]
hoelzl@45483
   113
haftmann@52435
   114
code_printing
haftmann@52435
   115
  constant sin \<rightharpoonup>
haftmann@52435
   116
    (SML) "Math.sin"
haftmann@52435
   117
    and (OCaml) "Pervasives.sin"
hoelzl@45483
   118
declare sin_def[code del]
hoelzl@45483
   119
haftmann@52435
   120
code_printing
haftmann@52435
   121
  constant pi \<rightharpoonup>
haftmann@52435
   122
    (SML) "Math.pi"
haftmann@52435
   123
    and (OCaml) "Pervasives.pi"
hoelzl@45483
   124
declare pi_def[code del]
hoelzl@45483
   125
haftmann@52435
   126
code_printing
haftmann@52435
   127
  constant arctan \<rightharpoonup>
haftmann@52435
   128
    (SML) "Math.atan"
haftmann@52435
   129
    and (OCaml) "Pervasives.atan"
hoelzl@45483
   130
declare arctan_def[code del]
hoelzl@45483
   131
haftmann@52435
   132
code_printing
haftmann@52435
   133
  constant arccos \<rightharpoonup>
haftmann@52435
   134
    (SML) "Math.scos"
haftmann@52435
   135
    and (OCaml) "Pervasives.acos"
hoelzl@45483
   136
declare arccos_def[code del]
hoelzl@45483
   137
haftmann@52435
   138
code_printing
haftmann@52435
   139
  constant arcsin \<rightharpoonup>
haftmann@52435
   140
    (SML) "Math.asin"
haftmann@52435
   141
    and (OCaml) "Pervasives.asin"
hoelzl@45483
   142
declare arcsin_def[code del]
hoelzl@45483
   143
haftmann@51143
   144
definition real_of_integer :: "integer \<Rightarrow> real" where
haftmann@51143
   145
  "real_of_integer = of_int \<circ> int_of_integer"
hoelzl@45483
   146
haftmann@52435
   147
code_printing
haftmann@52435
   148
  constant real_of_integer \<rightharpoonup>
haftmann@52435
   149
    (SML) "Real.fromInt"
haftmann@52435
   150
    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
hoelzl@45483
   151
haftmann@51143
   152
definition real_of_int :: "int \<Rightarrow> real" where
haftmann@51143
   153
  [code_abbrev]: "real_of_int = of_int"
haftmann@51143
   154
haftmann@51143
   155
lemma [code]:
haftmann@51143
   156
  "real_of_int = real_of_integer \<circ> integer_of_int"
haftmann@51143
   157
  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
hoelzl@45483
   158
huffman@47108
   159
lemma [code_unfold del]:
huffman@47108
   160
  "0 \<equiv> (of_rat 0 :: real)"
huffman@47108
   161
  by simp
huffman@47108
   162
huffman@47108
   163
lemma [code_unfold del]:
huffman@47108
   164
  "1 \<equiv> (of_rat 1 :: real)"
huffman@47108
   165
  by simp
hoelzl@45483
   166
huffman@47108
   167
lemma [code_unfold del]:
huffman@47108
   168
  "numeral k \<equiv> (of_rat (numeral k) :: real)"
huffman@47108
   169
  by simp
huffman@47108
   170
huffman@47108
   171
lemma [code_unfold del]:
huffman@47108
   172
  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
huffman@47108
   173
  by simp
huffman@47108
   174
huffman@47108
   175
hide_const (open) real_of_int
hoelzl@45483
   176
haftmann@52435
   177
code_printing
haftmann@52435
   178
  constant Ratreal \<rightharpoonup> (SML)
hoelzl@52403
   179
hoelzl@52403
   180
definition Realfract :: "int => int => real"
hoelzl@52403
   181
where
hoelzl@52403
   182
  "Realfract p q = of_int p / of_int q"
hoelzl@52403
   183
hoelzl@52403
   184
code_datatype Realfract
hoelzl@52403
   185
haftmann@52435
   186
code_printing
haftmann@52435
   187
  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
hoelzl@52403
   188
hoelzl@52403
   189
lemma [code]:
hoelzl@52403
   190
  "Ratreal r = split Realfract (quotient_of r)"
hoelzl@52403
   191
  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
hoelzl@52403
   192
hoelzl@52403
   193
lemma [code, code del]:
hoelzl@52403
   194
  "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
hoelzl@52403
   195
  ..
hoelzl@52403
   196
hoelzl@52403
   197
lemma [code, code del]:
hoelzl@52403
   198
  "(plus :: real => real => real) = plus"
hoelzl@52403
   199
  ..
hoelzl@52403
   200
hoelzl@52403
   201
lemma [code, code del]:
hoelzl@52403
   202
  "(uminus :: real => real) = uminus"
hoelzl@52403
   203
  ..
hoelzl@52403
   204
hoelzl@52403
   205
lemma [code, code del]:
hoelzl@52403
   206
  "(minus :: real => real => real) = minus"
hoelzl@52403
   207
  ..
hoelzl@52403
   208
hoelzl@52403
   209
lemma [code, code del]:
hoelzl@52403
   210
  "(times :: real => real => real) = times"
hoelzl@52403
   211
  ..
hoelzl@52403
   212
hoelzl@52403
   213
lemma [code, code del]:
hoelzl@52403
   214
  "(divide :: real => real => real) = divide"
hoelzl@52403
   215
  ..
hoelzl@52403
   216
hoelzl@52403
   217
lemma [code]:
hoelzl@52403
   218
  fixes r :: real
hoelzl@52403
   219
  shows "inverse r = 1 / r"
hoelzl@52403
   220
  by (fact inverse_eq_divide)
hoelzl@52403
   221
haftmann@46530
   222
notepad
haftmann@46530
   223
begin
haftmann@46530
   224
  have "cos (pi/2) = 0" by (rule cos_pi_half)
haftmann@46530
   225
  moreover have "cos (pi/2) \<noteq> 0" by eval
haftmann@46530
   226
  ultimately have "False" by blast
haftmann@46530
   227
end
hoelzl@45483
   228
hoelzl@45483
   229
end
haftmann@51143
   230