src/HOL/Library/Code_Real_Approx_By_Float.thy
author haftmann
Tue Feb 19 19:44:10 2013 +0100 (2013-02-19)
changeset 51188 9b5bf1a9a710
parent 51143 0a2371e7ced3
child 51542 738598beeb26
permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
     1 (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
     2 
     3 theory Code_Real_Approx_By_Float
     4 imports Complex_Main "~~/src/HOL/Library/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 notepad
   155 begin
   156   have "cos (pi/2) = 0" by (rule cos_pi_half)
   157   moreover have "cos (pi/2) \<noteq> 0" by eval
   158   ultimately have "False" by blast
   159 end
   160 
   161 end
   162