Theory HOL-Library.Code_Real_Approx_By_Float

(*  Title:      HOL/Library/Code_Real_Approx_By_Float.thy
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Florian Haftmann
    Author:     Johannes Hölzl
    Author:     Tobias Nipkow
*)

theory Code_Real_Approx_By_Float
imports Complex_Main Code_Target_Int
begin

text‹WARNING!› This theory implements mathematical reals by machine reals
  (floats). This is inconsistent. See the proof of False at the end of the
  theory, where an equality on mathematical reals is (incorrectly) disproved
  by mapping it to machine reals.

  The value command cannot display real results yet.

  The only legitimate use of this theory is as a tool for code generation
  purposes.
›

context
begin

qualified definition real_of_integer :: "integer  real"
  where [code_abbrev]: "real_of_integer = of_int  int_of_integer"

end

code_datatype Code_Real_Approx_By_Float.real_of_integer (/) :: real  real  real

lemma [code_unfold del]: "numeral k  real_of_rat (numeral k)"
  by simp

lemma [code_unfold del]: "- numeral k  real_of_rat (- numeral k)"
  by simp

context
begin

qualified definition real_of_int :: int  real
  where [code_abbrev]: real_of_int = of_int

lemma [code]: "real_of_int = Code_Real_Approx_By_Float.real_of_integer  integer_of_int"
  by (simp add: fun_eq_iff Code_Real_Approx_By_Float.real_of_integer_def real_of_int_def)

qualified definition exp_real :: real  real
  where [code_abbrev, code del]: exp_real = exp

qualified definition sin_real :: real  real
  where [code_abbrev, code del]: sin_real = sin

qualified definition cos_real :: real  real
  where [code_abbrev, code del]: cos_real = cos

qualified definition tan_real :: real  real
  where [code_abbrev, code del]: tan_real = tan

end

lemma [code]: Ratreal r = (case quotient_of r of (p, q)  real_of_int p / real_of_int q)
  by (cases r) (simp add: quotient_of_Fract of_rat_rat)

lemma [code]: inverse r = 1 / r for r :: real
  by (fact inverse_eq_divide)

declare [[code drop: HOL.equal :: real  real  bool
  (≤) :: real  real  bool
  (<) :: real  real  bool
  plus :: real  real  real
  times :: real  real  real
  uminus :: real  real
  minus :: real  real  real
  divide :: real  real  real
  sqrt
  ln :: real  real
  pi
  arcsin
  arccos
  arctan]]

code_reserved SML Real

code_printing
  type_constructor real 
    (SML) "real"
    and (OCaml) "float"
    and (Haskell) "Prelude.Double" (*Double precision*)
| constant "0 :: real" 
    (SML) "0.0"
    and (OCaml) "0.0"
    and (Haskell) "0.0"
| constant "1 :: real" 
    (SML) "1.0"
    and (OCaml) "1.0"
    and (Haskell) "1.0"
| constant "HOL.equal :: real  real  bool" 
    (SML) "Real.== ((_), (_))"
    and (OCaml) "Pervasives.(=)"
    and (Haskell) infix 4 "=="
| class_instance real :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*)
| constant "(≤) :: real  real  bool" 
    (SML) "Real.<= ((_), (_))"
    and (OCaml) "Pervasives.(<=)"
    and (Haskell) infix 4 "<="
| constant "(<) :: real  real  bool" 
    (SML) "Real.< ((_), (_))"
    and (OCaml) "Pervasives.(<)"
    and (Haskell) infix 4 "<"
| constant "(+) :: real  real  real" 
    (SML) "Real.+ ((_), (_))"
    and (OCaml) "Pervasives.( +. )"
    and (Haskell) infixl 6 "+"
| constant "(*) :: real  real  real" 
    (SML) "Real.* ((_), (_))"
    and (Haskell) infixl 7 "*"
| constant "uminus :: real  real" 
    (SML) "Real.~"
    and (OCaml) "Pervasives.( ~-. )"
    and (Haskell) "negate"
| constant "(-) :: real  real  real" 
    (SML) "Real.- ((_), (_))"
    and (OCaml) "Pervasives.( -. )"
    and (Haskell) infixl 6 "-"
| constant "(/) :: real  real  real" 
    (SML) "Real.'/ ((_), (_))"
    and (OCaml) "Pervasives.( '/. )"
    and (Haskell) infixl 7 "/"
| constant "sqrt :: real  real" 
    (SML) "Math.sqrt"
    and (OCaml) "Pervasives.sqrt"
    and (Haskell) "Prelude.sqrt" 
| constant Code_Real_Approx_By_Float.exp_real 
    (SML) "Math.exp"
    and (OCaml) "Pervasives.exp"
    and (Haskell) "Prelude.exp"
| constant ln 
    (SML) "Math.ln"
    and (OCaml) "Pervasives.ln"
    and (Haskell) "Prelude.log"
| constant Code_Real_Approx_By_Float.sin_real 
    (SML) "Math.sin"
    and (OCaml) "Pervasives.sin"
    and (Haskell) "Prelude.sin"
| constant Code_Real_Approx_By_Float.cos_real 
    (SML) "Math.cos"
    and (OCaml) "Pervasives.cos"
    and (Haskell) "Prelude.cos"
| constant Code_Real_Approx_By_Float.tan_real 
    (SML) "Math.tan"
    and (OCaml) "Pervasives.tan"
    and (Haskell) "Prelude.tan"
| constant pi 
    (SML) "Math.pi"
    (*missing in OCaml*)
    and (Haskell) "Prelude.pi"
| constant arcsin 
    (SML) "Math.asin"
    and (OCaml) "Pervasives.asin"
    and (Haskell) "Prelude.asin"
| constant arccos 
    (SML) "Math.scos"
    and (OCaml) "Pervasives.acos"
    and (Haskell) "Prelude.acos"
| constant arctan 
    (SML) "Math.atan"
    and (OCaml) "Pervasives.atan"
    and (Haskell) "Prelude.atan"
| constant Code_Real_Approx_By_Float.real_of_integer 
    (SML) "Real.fromInt"
    and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
    and (Haskell) "Prelude.fromIntegral (_)"

notepad
begin
  have "cos (pi/2) = 0" by (rule cos_pi_half)
  moreover have "cos (pi/2)  0" by eval
  ultimately have False by blast
end

end