src/HOL/Library/Code_Real_Approx_By_Float.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 47108 2a1953f0d20d
child 51143 0a2371e7ced3
permissions -rw-r--r--
tuned headers;
     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_Integer"
     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_int :: "int \<Rightarrow> real" where
   123   "real_of_int \<equiv> of_int"
   124 
   125 code_const real_of_int
   126   (SML "Real.fromInt")
   127   (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
   128 
   129 lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
   130   unfolding real_of_int_def ..
   131 
   132 lemma [code_unfold del]:
   133   "0 \<equiv> (of_rat 0 :: real)"
   134   by simp
   135 
   136 lemma [code_unfold del]:
   137   "1 \<equiv> (of_rat 1 :: real)"
   138   by simp
   139 
   140 lemma [code_unfold del]:
   141   "numeral k \<equiv> (of_rat (numeral k) :: real)"
   142   by simp
   143 
   144 lemma [code_unfold del]:
   145   "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
   146   by simp
   147 
   148 hide_const (open) real_of_int
   149 
   150 notepad
   151 begin
   152   have "cos (pi/2) = 0" by (rule cos_pi_half)
   153   moreover have "cos (pi/2) \<noteq> 0" by eval
   154   ultimately have "False" by blast
   155 end
   156 
   157 end