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