src/HOL/Library/Code_Real_Approx_By_Float.thy
author huffman
Sun Mar 25 20:15:39 2012 +0200 (2012-03-25)
changeset 47108 2a1953f0d20d
parent 46530 d5d14046686f
child 51143 0a2371e7ced3
permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
hoelzl@45483
     1
(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
hoelzl@45483
     2
hoelzl@45483
     3
theory Code_Real_Approx_By_Float
hoelzl@45483
     4
imports Complex_Main "~~/src/HOL/Library/Code_Integer"
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
hoelzl@45483
   122
definition real_of_int :: "int \<Rightarrow> real" where
hoelzl@45483
   123
  "real_of_int \<equiv> of_int"
hoelzl@45483
   124
hoelzl@45483
   125
code_const real_of_int
hoelzl@45483
   126
  (SML "Real.fromInt")
hoelzl@45483
   127
  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
hoelzl@45483
   128
hoelzl@45483
   129
lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
hoelzl@45483
   130
  unfolding real_of_int_def ..
hoelzl@45483
   131
huffman@47108
   132
lemma [code_unfold del]:
huffman@47108
   133
  "0 \<equiv> (of_rat 0 :: real)"
huffman@47108
   134
  by simp
huffman@47108
   135
huffman@47108
   136
lemma [code_unfold del]:
huffman@47108
   137
  "1 \<equiv> (of_rat 1 :: real)"
huffman@47108
   138
  by simp
hoelzl@45483
   139
huffman@47108
   140
lemma [code_unfold del]:
huffman@47108
   141
  "numeral k \<equiv> (of_rat (numeral k) :: real)"
huffman@47108
   142
  by simp
huffman@47108
   143
huffman@47108
   144
lemma [code_unfold del]:
huffman@47108
   145
  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
huffman@47108
   146
  by simp
huffman@47108
   147
huffman@47108
   148
hide_const (open) real_of_int
hoelzl@45483
   149
haftmann@46530
   150
notepad
haftmann@46530
   151
begin
haftmann@46530
   152
  have "cos (pi/2) = 0" by (rule cos_pi_half)
haftmann@46530
   153
  moreover have "cos (pi/2) \<noteq> 0" by eval
haftmann@46530
   154
  ultimately have "False" by blast
haftmann@46530
   155
end
hoelzl@45483
   156
hoelzl@45483
   157
end