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