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