src/HOL/Library/Code_Real_Approx_By_Float.thy
author wenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151 a7394aa4d21c
parent 63355 7b23053be254
child 66147 9225370db5f0
permissions -rw-r--r--
tuned proofs;
     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 declare zero_real_code[code_unfold del]
    37 
    38 code_printing
    39   constant "1 :: real" \<rightharpoonup>
    40     (SML) "1.0"
    41     and (OCaml) "1.0"
    42 declare one_real_code[code_unfold del]
    43 
    44 code_printing
    45   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    46     (SML) "Real.== ((_), (_))"
    47     and (OCaml) "Pervasives.(=)"
    48 
    49 code_printing
    50   constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    51     (SML) "Real.<= ((_), (_))"
    52     and (OCaml) "Pervasives.(<=)"
    53 
    54 code_printing
    55   constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    56     (SML) "Real.< ((_), (_))"
    57     and (OCaml) "Pervasives.(<)"
    58 
    59 code_printing
    60   constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    61     (SML) "Real.+ ((_), (_))"
    62     and (OCaml) "Pervasives.( +. )"
    63 
    64 code_printing
    65   constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    66     (SML) "Real.* ((_), (_))"
    67     and (OCaml) "Pervasives.( *. )"
    68 
    69 code_printing
    70   constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    71     (SML) "Real.- ((_), (_))"
    72     and (OCaml) "Pervasives.( -. )"
    73 
    74 code_printing
    75   constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
    76     (SML) "Real.~"
    77     and (OCaml) "Pervasives.( ~-. )"
    78 
    79 code_printing
    80   constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    81     (SML) "Real.'/ ((_), (_))"
    82     and (OCaml) "Pervasives.( '/. )"
    83 
    84 code_printing
    85   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    86     (SML) "Real.== ((_:real), (_))"
    87 
    88 code_printing
    89   constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
    90     (SML) "Math.sqrt"
    91     and (OCaml) "Pervasives.sqrt"
    92 declare sqrt_def[code del]
    93 
    94 context
    95 begin
    96 
    97 qualified definition real_exp :: "real \<Rightarrow> real"
    98   where "real_exp = exp"
    99 
   100 lemma exp_eq_real_exp [code_unfold]: "exp = real_exp"
   101   unfolding real_exp_def ..
   102 
   103 end
   104 
   105 code_printing
   106   constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
   107     (SML) "Math.exp"
   108     and (OCaml) "Pervasives.exp"
   109 declare Code_Real_Approx_By_Float.real_exp_def[code del]
   110 declare exp_def[code del]
   111 
   112 code_printing
   113   constant ln \<rightharpoonup>
   114     (SML) "Math.ln"
   115     and (OCaml) "Pervasives.ln"
   116 declare ln_real_def[code del]
   117 
   118 code_printing
   119   constant cos \<rightharpoonup>
   120     (SML) "Math.cos"
   121     and (OCaml) "Pervasives.cos"
   122 declare cos_def[code del]
   123 
   124 code_printing
   125   constant sin \<rightharpoonup>
   126     (SML) "Math.sin"
   127     and (OCaml) "Pervasives.sin"
   128 declare sin_def[code del]
   129 
   130 code_printing
   131   constant pi \<rightharpoonup>
   132     (SML) "Math.pi"
   133     and (OCaml) "Pervasives.pi"
   134 declare pi_def[code del]
   135 
   136 code_printing
   137   constant arctan \<rightharpoonup>
   138     (SML) "Math.atan"
   139     and (OCaml) "Pervasives.atan"
   140 declare arctan_def[code del]
   141 
   142 code_printing
   143   constant arccos \<rightharpoonup>
   144     (SML) "Math.scos"
   145     and (OCaml) "Pervasives.acos"
   146 declare arccos_def[code del]
   147 
   148 code_printing
   149   constant arcsin \<rightharpoonup>
   150     (SML) "Math.asin"
   151     and (OCaml) "Pervasives.asin"
   152 declare arcsin_def[code del]
   153 
   154 definition real_of_integer :: "integer \<Rightarrow> real"
   155   where "real_of_integer = of_int \<circ> int_of_integer"
   156 
   157 code_printing
   158   constant real_of_integer \<rightharpoonup>
   159     (SML) "Real.fromInt"
   160     and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
   161 
   162 context
   163 begin
   164 
   165 qualified definition real_of_int :: "int \<Rightarrow> real"
   166   where [code_abbrev]: "real_of_int = of_int"
   167 
   168 lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int"
   169   by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
   170 
   171 lemma [code_unfold del]: "0 \<equiv> (of_rat 0 :: real)"
   172   by simp
   173 
   174 lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)"
   175   by simp
   176 
   177 lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)"
   178   by simp
   179 
   180 lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
   181   by simp
   182 
   183 end
   184 
   185 code_printing
   186   constant Ratreal \<rightharpoonup> (SML)
   187 
   188 definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
   189   where "Realfract p q = of_int p / of_int q"
   190 
   191 code_datatype Realfract
   192 
   193 code_printing
   194   constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
   195 
   196 lemma [code]: "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]: "(HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool) = (HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool)"
   200   ..
   201 
   202 lemma [code, code del]: "(plus :: real \<Rightarrow> real \<Rightarrow> real) = plus"
   203   ..
   204 
   205 lemma [code, code del]: "(uminus :: real \<Rightarrow> real) = uminus"
   206   ..
   207 
   208 lemma [code, code del]: "(minus :: real \<Rightarrow> real \<Rightarrow> real) = minus"
   209   ..
   210 
   211 lemma [code, code del]: "(times :: real \<Rightarrow> real \<Rightarrow> real) = times"
   212   ..
   213 
   214 lemma [code, code del]: "(divide :: real \<Rightarrow> real \<Rightarrow> real) = divide"
   215   ..
   216 
   217 lemma [code]: "inverse r = 1 / r" for r :: real
   218   by (fact inverse_eq_divide)
   219 
   220 notepad
   221 begin
   222   have "cos (pi/2) = 0" by (rule cos_pi_half)
   223   moreover have "cos (pi/2) \<noteq> 0" by eval
   224   ultimately have False by blast
   225 end
   226 
   227 end