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