src/HOL/Library/Code_Real_Approx_By_Float.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45496 5c0444d2abfe
child 46530 d5d14046686f
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 hide_const (open) real_of_int
   133 
   134 declare number_of_real_code [code_unfold del]
   135 
   136 lemma "False"
   137 proof-
   138   have "cos(pi/2) = 0" by(rule cos_pi_half)
   139   moreover have "cos(pi/2) \<noteq> 0" by eval
   140   ultimately show "False" by blast
   141 qed
   142 
   143 end