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