src/HOL/Library/Code_Real_Approx_By_Float.thy
author hoelzl
Fri Jun 21 12:41:08 2013 +0200 (2013-06-21)
changeset 52403 140ae824ea4a
parent 51542 738598beeb26
child 52435 6646bb548c6b
permissions -rw-r--r--
Code_Real_Approx_By_Float: remove code equations using Ratreal
     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{* \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. *}
    16 
    17 code_type real
    18   (SML   "real")
    19   (OCaml "float")
    20 
    21 code_const Ratreal
    22   (SML "error/ \"Bad constant: Ratreal\"")
    23 
    24 code_const "0 :: real"
    25   (SML   "0.0")
    26   (OCaml "0.0")
    27 declare zero_real_code[code_unfold del]
    28 
    29 code_const "1 :: real"
    30   (SML   "1.0")
    31   (OCaml "1.0")
    32 declare one_real_code[code_unfold del]
    33 
    34 code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    35   (SML   "Real.== ((_), (_))")
    36   (OCaml "Pervasives.(=)")
    37 
    38 code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
    39   (SML   "Real.<= ((_), (_))")
    40   (OCaml "Pervasives.(<=)")
    41 
    42 code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
    43   (SML   "Real.< ((_), (_))")
    44   (OCaml "Pervasives.(<)")
    45 
    46 code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
    47   (SML   "Real.+ ((_), (_))")
    48   (OCaml "Pervasives.( +. )")
    49 
    50 code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
    51   (SML   "Real.* ((_), (_))")
    52   (OCaml "Pervasives.( *. )")
    53 
    54 code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
    55   (SML   "Real.- ((_), (_))")
    56   (OCaml "Pervasives.( -. )")
    57 
    58 code_const "uminus :: real \<Rightarrow> real"
    59   (SML   "Real.~")
    60   (OCaml "Pervasives.( ~-. )")
    61 
    62 code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
    63   (SML   "Real.'/ ((_), (_))")
    64   (OCaml "Pervasives.( '/. )")
    65 
    66 code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    67   (SML   "Real.== ((_:real), (_))")
    68 
    69 code_const "sqrt :: real \<Rightarrow> real"
    70   (SML   "Math.sqrt")
    71   (OCaml "Pervasives.sqrt")
    72 declare sqrt_def[code del]
    73 
    74 definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
    75 
    76 lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
    77   unfolding real_exp_def ..
    78 
    79 code_const real_exp
    80   (SML   "Math.exp")
    81   (OCaml "Pervasives.exp")
    82 declare real_exp_def[code del]
    83 declare exp_def[code del]
    84 
    85 hide_const (open) real_exp
    86 
    87 code_const ln
    88   (SML   "Math.ln")
    89   (OCaml "Pervasives.ln")
    90 declare ln_def[code del]
    91 
    92 code_const cos
    93   (SML   "Math.cos")
    94   (OCaml "Pervasives.cos")
    95 declare cos_def[code del]
    96 
    97 code_const sin
    98   (SML   "Math.sin")
    99   (OCaml "Pervasives.sin")
   100 declare sin_def[code del]
   101 
   102 code_const pi
   103   (SML   "Math.pi")
   104   (OCaml "Pervasives.pi")
   105 declare pi_def[code del]
   106 
   107 code_const arctan
   108   (SML   "Math.atan")
   109   (OCaml "Pervasives.atan")
   110 declare arctan_def[code del]
   111 
   112 code_const arccos
   113   (SML   "Math.scos")
   114   (OCaml "Pervasives.acos")
   115 declare arccos_def[code del]
   116 
   117 code_const arcsin
   118   (SML   "Math.asin")
   119   (OCaml "Pervasives.asin")
   120 declare arcsin_def[code del]
   121 
   122 definition real_of_integer :: "integer \<Rightarrow> real" where
   123   "real_of_integer = of_int \<circ> int_of_integer"
   124 
   125 code_const real_of_integer
   126   (SML "Real.fromInt")
   127   (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
   128 
   129 definition real_of_int :: "int \<Rightarrow> real" where
   130   [code_abbrev]: "real_of_int = of_int"
   131 
   132 lemma [code]:
   133   "real_of_int = real_of_integer \<circ> integer_of_int"
   134   by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
   135 
   136 lemma [code_unfold del]:
   137   "0 \<equiv> (of_rat 0 :: real)"
   138   by simp
   139 
   140 lemma [code_unfold del]:
   141   "1 \<equiv> (of_rat 1 :: real)"
   142   by simp
   143 
   144 lemma [code_unfold del]:
   145   "numeral k \<equiv> (of_rat (numeral k) :: real)"
   146   by simp
   147 
   148 lemma [code_unfold del]:
   149   "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
   150   by simp
   151 
   152 hide_const (open) real_of_int
   153 
   154 code_const Ratreal (SML)
   155 
   156 definition Realfract :: "int => int => real"
   157 where
   158   "Realfract p q = of_int p / of_int q"
   159 
   160 code_datatype Realfract
   161 
   162 code_const Realfract
   163   (SML "Real.fromInt _/ '// Real.fromInt _")
   164 
   165 lemma [code]:
   166   "Ratreal r = split Realfract (quotient_of r)"
   167   by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
   168 
   169 lemma [code, code del]:
   170   "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
   171   ..
   172 
   173 lemma [code, code del]:
   174   "(plus :: real => real => real) = plus"
   175   ..
   176 
   177 lemma [code, code del]:
   178   "(uminus :: real => real) = uminus"
   179   ..
   180 
   181 lemma [code, code del]:
   182   "(minus :: real => real => real) = minus"
   183   ..
   184 
   185 lemma [code, code del]:
   186   "(times :: real => real => real) = times"
   187   ..
   188 
   189 lemma [code, code del]:
   190   "(divide :: real => real => real) = divide"
   191   ..
   192 
   193 lemma [code]:
   194   fixes r :: real
   195   shows "inverse r = 1 / r"
   196   by (fact inverse_eq_divide)
   197 
   198 notepad
   199 begin
   200   have "cos (pi/2) = 0" by (rule cos_pi_half)
   201   moreover have "cos (pi/2) \<noteq> 0" by eval
   202   ultimately have "False" by blast
   203 end
   204 
   205 end
   206