src/HOL/Library/Code_Real_Approx_By_Float.thy
author hoelzl
Fri Jun 21 12:41:08 2013 +0200 (2013-06-21)
changeset 52403 140ae824ea4a
parent 51542 738598beeb26
child 52435 6646bb548c6b
permissions -rw-r--r--
Code_Real_Approx_By_Float: remove code equations using Ratreal
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
hoelzl@45483
    17
code_type real
hoelzl@45483
    18
  (SML   "real")
hoelzl@45483
    19
  (OCaml "float")
hoelzl@45483
    20
hoelzl@45483
    21
code_const Ratreal
hoelzl@45483
    22
  (SML "error/ \"Bad constant: Ratreal\"")
hoelzl@45483
    23
hoelzl@45483
    24
code_const "0 :: real"
hoelzl@45483
    25
  (SML   "0.0")
hoelzl@45483
    26
  (OCaml "0.0")
hoelzl@45483
    27
declare zero_real_code[code_unfold del]
hoelzl@45483
    28
hoelzl@45483
    29
code_const "1 :: real"
hoelzl@45483
    30
  (SML   "1.0")
hoelzl@45483
    31
  (OCaml "1.0")
hoelzl@45483
    32
declare one_real_code[code_unfold del]
hoelzl@45483
    33
hoelzl@45483
    34
code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
hoelzl@45483
    35
  (SML   "Real.== ((_), (_))")
hoelzl@45483
    36
  (OCaml "Pervasives.(=)")
hoelzl@45483
    37
hoelzl@45483
    38
code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
hoelzl@45483
    39
  (SML   "Real.<= ((_), (_))")
hoelzl@45483
    40
  (OCaml "Pervasives.(<=)")
hoelzl@45483
    41
hoelzl@45483
    42
code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
hoelzl@45483
    43
  (SML   "Real.< ((_), (_))")
hoelzl@45483
    44
  (OCaml "Pervasives.(<)")
hoelzl@45483
    45
hoelzl@45483
    46
code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
hoelzl@45483
    47
  (SML   "Real.+ ((_), (_))")
hoelzl@45483
    48
  (OCaml "Pervasives.( +. )")
hoelzl@45483
    49
hoelzl@45483
    50
code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
hoelzl@45483
    51
  (SML   "Real.* ((_), (_))")
hoelzl@45483
    52
  (OCaml "Pervasives.( *. )")
hoelzl@45483
    53
hoelzl@45483
    54
code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
hoelzl@45483
    55
  (SML   "Real.- ((_), (_))")
hoelzl@45483
    56
  (OCaml "Pervasives.( -. )")
hoelzl@45483
    57
hoelzl@45483
    58
code_const "uminus :: real \<Rightarrow> real"
hoelzl@45483
    59
  (SML   "Real.~")
hoelzl@45483
    60
  (OCaml "Pervasives.( ~-. )")
hoelzl@45483
    61
hoelzl@45483
    62
code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
hoelzl@45483
    63
  (SML   "Real.'/ ((_), (_))")
hoelzl@45483
    64
  (OCaml "Pervasives.( '/. )")
hoelzl@45483
    65
hoelzl@45483
    66
code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
hoelzl@45483
    67
  (SML   "Real.== ((_:real), (_))")
hoelzl@45483
    68
hoelzl@45483
    69
code_const "sqrt :: real \<Rightarrow> real"
hoelzl@45483
    70
  (SML   "Math.sqrt")
hoelzl@45483
    71
  (OCaml "Pervasives.sqrt")
hoelzl@45483
    72
declare sqrt_def[code del]
hoelzl@45483
    73
hoelzl@45483
    74
definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
hoelzl@45483
    75
hoelzl@45483
    76
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
hoelzl@45483
    77
  unfolding real_exp_def ..
hoelzl@45483
    78
hoelzl@45483
    79
code_const real_exp
hoelzl@45483
    80
  (SML   "Math.exp")
hoelzl@45483
    81
  (OCaml "Pervasives.exp")
hoelzl@45483
    82
declare real_exp_def[code del]
hoelzl@45483
    83
declare exp_def[code del]
hoelzl@45483
    84
hoelzl@45483
    85
hide_const (open) real_exp
hoelzl@45483
    86
hoelzl@45483
    87
code_const ln
hoelzl@45483
    88
  (SML   "Math.ln")
hoelzl@45483
    89
  (OCaml "Pervasives.ln")
hoelzl@45483
    90
declare ln_def[code del]
hoelzl@45483
    91
hoelzl@45483
    92
code_const cos
hoelzl@45483
    93
  (SML   "Math.cos")
hoelzl@45483
    94
  (OCaml "Pervasives.cos")
hoelzl@45483
    95
declare cos_def[code del]
hoelzl@45483
    96
hoelzl@45483
    97
code_const sin
hoelzl@45483
    98
  (SML   "Math.sin")
hoelzl@45483
    99
  (OCaml "Pervasives.sin")
hoelzl@45483
   100
declare sin_def[code del]
hoelzl@45483
   101
hoelzl@45483
   102
code_const pi
hoelzl@45483
   103
  (SML   "Math.pi")
hoelzl@45483
   104
  (OCaml "Pervasives.pi")
hoelzl@45483
   105
declare pi_def[code del]
hoelzl@45483
   106
hoelzl@45483
   107
code_const arctan
hoelzl@45483
   108
  (SML   "Math.atan")
hoelzl@45483
   109
  (OCaml "Pervasives.atan")
hoelzl@45483
   110
declare arctan_def[code del]
hoelzl@45483
   111
hoelzl@45483
   112
code_const arccos
hoelzl@45483
   113
  (SML   "Math.scos")
hoelzl@45483
   114
  (OCaml "Pervasives.acos")
hoelzl@45483
   115
declare arccos_def[code del]
hoelzl@45483
   116
hoelzl@45483
   117
code_const arcsin
hoelzl@45483
   118
  (SML   "Math.asin")
hoelzl@45483
   119
  (OCaml "Pervasives.asin")
hoelzl@45483
   120
declare arcsin_def[code del]
hoelzl@45483
   121
haftmann@51143
   122
definition real_of_integer :: "integer \<Rightarrow> real" where
haftmann@51143
   123
  "real_of_integer = of_int \<circ> int_of_integer"
hoelzl@45483
   124
haftmann@51143
   125
code_const real_of_integer
hoelzl@45483
   126
  (SML "Real.fromInt")
hoelzl@45483
   127
  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
hoelzl@45483
   128
haftmann@51143
   129
definition real_of_int :: "int \<Rightarrow> real" where
haftmann@51143
   130
  [code_abbrev]: "real_of_int = of_int"
haftmann@51143
   131
haftmann@51143
   132
lemma [code]:
haftmann@51143
   133
  "real_of_int = real_of_integer \<circ> integer_of_int"
haftmann@51143
   134
  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
hoelzl@45483
   135
huffman@47108
   136
lemma [code_unfold del]:
huffman@47108
   137
  "0 \<equiv> (of_rat 0 :: real)"
huffman@47108
   138
  by simp
huffman@47108
   139
huffman@47108
   140
lemma [code_unfold del]:
huffman@47108
   141
  "1 \<equiv> (of_rat 1 :: real)"
huffman@47108
   142
  by simp
hoelzl@45483
   143
huffman@47108
   144
lemma [code_unfold del]:
huffman@47108
   145
  "numeral k \<equiv> (of_rat (numeral k) :: real)"
huffman@47108
   146
  by simp
huffman@47108
   147
huffman@47108
   148
lemma [code_unfold del]:
huffman@47108
   149
  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
huffman@47108
   150
  by simp
huffman@47108
   151
huffman@47108
   152
hide_const (open) real_of_int
hoelzl@45483
   153
hoelzl@52403
   154
code_const Ratreal (SML)
hoelzl@52403
   155
hoelzl@52403
   156
definition Realfract :: "int => int => real"
hoelzl@52403
   157
where
hoelzl@52403
   158
  "Realfract p q = of_int p / of_int q"
hoelzl@52403
   159
hoelzl@52403
   160
code_datatype Realfract
hoelzl@52403
   161
hoelzl@52403
   162
code_const Realfract
hoelzl@52403
   163
  (SML "Real.fromInt _/ '// Real.fromInt _")
hoelzl@52403
   164
hoelzl@52403
   165
lemma [code]:
hoelzl@52403
   166
  "Ratreal r = split Realfract (quotient_of r)"
hoelzl@52403
   167
  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
hoelzl@52403
   168
hoelzl@52403
   169
lemma [code, code del]:
hoelzl@52403
   170
  "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
hoelzl@52403
   171
  ..
hoelzl@52403
   172
hoelzl@52403
   173
lemma [code, code del]:
hoelzl@52403
   174
  "(plus :: real => real => real) = plus"
hoelzl@52403
   175
  ..
hoelzl@52403
   176
hoelzl@52403
   177
lemma [code, code del]:
hoelzl@52403
   178
  "(uminus :: real => real) = uminus"
hoelzl@52403
   179
  ..
hoelzl@52403
   180
hoelzl@52403
   181
lemma [code, code del]:
hoelzl@52403
   182
  "(minus :: real => real => real) = minus"
hoelzl@52403
   183
  ..
hoelzl@52403
   184
hoelzl@52403
   185
lemma [code, code del]:
hoelzl@52403
   186
  "(times :: real => real => real) = times"
hoelzl@52403
   187
  ..
hoelzl@52403
   188
hoelzl@52403
   189
lemma [code, code del]:
hoelzl@52403
   190
  "(divide :: real => real => real) = divide"
hoelzl@52403
   191
  ..
hoelzl@52403
   192
hoelzl@52403
   193
lemma [code]:
hoelzl@52403
   194
  fixes r :: real
hoelzl@52403
   195
  shows "inverse r = 1 / r"
hoelzl@52403
   196
  by (fact inverse_eq_divide)
hoelzl@52403
   197
haftmann@46530
   198
notepad
haftmann@46530
   199
begin
haftmann@46530
   200
  have "cos (pi/2) = 0" by (rule cos_pi_half)
haftmann@46530
   201
  moreover have "cos (pi/2) \<noteq> 0" by eval
haftmann@46530
   202
  ultimately have "False" by blast
haftmann@46530
   203
end
hoelzl@45483
   204
hoelzl@45483
   205
end
haftmann@51143
   206