src/HOL/Library/Code_Real_Approx_By_Float.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 67399 eab6ce8368fa
child 69064 5840724b1d71
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 (*  Title:      HOL/Library/Code_Real_Approx_By_Float.thy
     2     Author:     Florian Haftmann
     3     Author:     Johannes Hölzl
     4     Author:     Tobias Nipkow
     5 *)
     6 
     7 theory Code_Real_Approx_By_Float
     8 imports Complex_Main Code_Target_Int
     9 begin
    10 
    11 text\<open>
    12   \<^bold>\<open>WARNING!\<close> This theory implements mathematical reals by machine reals
    13   (floats). This is inconsistent. See the proof of False at the end of the
    14   theory, where an equality on mathematical reals is (incorrectly) disproved
    15   by mapping it to machine reals.
    16 
    17   The \<^theory_text>\<open>value\<close> command cannot display real results yet.
    18 
    19   The only legitimate use of this theory is as a tool for code generation
    20   purposes.
    21 \<close>
    22 
    23 code_printing
    24   type_constructor real \<rightharpoonup>
    25     (SML) "real"
    26     and (OCaml) "float"
    27 
    28 code_printing
    29   constant Ratreal \<rightharpoonup>
    30     (SML) "error/ \"Bad constant: Ratreal\""
    31 
    32 code_printing
    33   constant "0 :: real" \<rightharpoonup>
    34     (SML) "0.0"
    35     and (OCaml) "0.0"
    36 
    37 code_printing
    38   constant "1 :: real" \<rightharpoonup>
    39     (SML) "1.0"
    40     and (OCaml) "1.0"
    41 
    42 code_printing
    43   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    44     (SML) "Real.== ((_), (_))"
    45     and (OCaml) "Pervasives.(=)"
    46 
    47 code_printing
    48   constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    49     (SML) "Real.<= ((_), (_))"
    50     and (OCaml) "Pervasives.(<=)"
    51 
    52 code_printing
    53   constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    54     (SML) "Real.< ((_), (_))"
    55     and (OCaml) "Pervasives.(<)"
    56 
    57 code_printing
    58   constant "(+) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    59     (SML) "Real.+ ((_), (_))"
    60     and (OCaml) "Pervasives.( +. )"
    61 
    62 code_printing
    63   constant "( * ) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    64     (SML) "Real.* ((_), (_))"
    65     and (OCaml) "Pervasives.( *. )"
    66 
    67 code_printing
    68   constant "(-) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    69     (SML) "Real.- ((_), (_))"
    70     and (OCaml) "Pervasives.( -. )"
    71 
    72 code_printing
    73   constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
    74     (SML) "Real.~"
    75     and (OCaml) "Pervasives.( ~-. )"
    76 
    77 code_printing
    78   constant "(/) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
    79     (SML) "Real.'/ ((_), (_))"
    80     and (OCaml) "Pervasives.( '/. )"
    81 
    82 code_printing
    83   constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
    84     (SML) "Real.== ((_:real), (_))"
    85 
    86 code_printing
    87   constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
    88     (SML) "Math.sqrt"
    89     and (OCaml) "Pervasives.sqrt"
    90 declare sqrt_def[code del]
    91 
    92 context
    93 begin
    94 
    95 qualified definition real_exp :: "real \<Rightarrow> real"
    96   where "real_exp = exp"
    97 
    98 lemma exp_eq_real_exp [code_unfold]: "exp = real_exp"
    99   unfolding real_exp_def ..
   100 
   101 end
   102 
   103 code_printing
   104   constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
   105     (SML) "Math.exp"
   106     and (OCaml) "Pervasives.exp"
   107 declare Code_Real_Approx_By_Float.real_exp_def[code del]
   108 declare exp_def[code del]
   109 
   110 code_printing
   111   constant ln \<rightharpoonup>
   112     (SML) "Math.ln"
   113     and (OCaml) "Pervasives.ln"
   114 declare ln_real_def[code del]
   115 
   116 code_printing
   117   constant cos \<rightharpoonup>
   118     (SML) "Math.cos"
   119     and (OCaml) "Pervasives.cos"
   120 declare cos_def[code del]
   121 
   122 code_printing
   123   constant sin \<rightharpoonup>
   124     (SML) "Math.sin"
   125     and (OCaml) "Pervasives.sin"
   126 declare sin_def[code del]
   127 
   128 code_printing
   129   constant pi \<rightharpoonup>
   130     (SML) "Math.pi"
   131     and (OCaml) "Pervasives.pi"
   132 declare pi_def[code del]
   133 
   134 code_printing
   135   constant arctan \<rightharpoonup>
   136     (SML) "Math.atan"
   137     and (OCaml) "Pervasives.atan"
   138 declare arctan_def[code del]
   139 
   140 code_printing
   141   constant arccos \<rightharpoonup>
   142     (SML) "Math.scos"
   143     and (OCaml) "Pervasives.acos"
   144 declare arccos_def[code del]
   145 
   146 code_printing
   147   constant arcsin \<rightharpoonup>
   148     (SML) "Math.asin"
   149     and (OCaml) "Pervasives.asin"
   150 declare arcsin_def[code del]
   151 
   152 definition real_of_integer :: "integer \<Rightarrow> real"
   153   where "real_of_integer = of_int \<circ> int_of_integer"
   154 
   155 code_printing
   156   constant real_of_integer \<rightharpoonup>
   157     (SML) "Real.fromInt"
   158     and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
   159 
   160 context
   161 begin
   162 
   163 qualified definition real_of_int :: "int \<Rightarrow> real"
   164   where [code_abbrev]: "real_of_int = of_int"
   165 
   166 lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int"
   167   by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
   168 
   169 lemma [code_unfold del]: "0 \<equiv> (of_rat 0 :: real)"
   170   by simp
   171 
   172 lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)"
   173   by simp
   174 
   175 lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)"
   176   by simp
   177 
   178 lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
   179   by simp
   180 
   181 end
   182 
   183 code_printing
   184   constant Ratreal \<rightharpoonup> (SML)
   185 
   186 definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
   187   where "Realfract p q = of_int p / of_int q"
   188 
   189 code_datatype Realfract
   190 
   191 code_printing
   192   constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
   193 
   194 lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
   195   by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
   196 
   197 declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
   198   "plus :: real \<Rightarrow> real \<Rightarrow> real"
   199   "uminus :: real \<Rightarrow> real"
   200   "minus :: real \<Rightarrow> real \<Rightarrow> real"
   201   "times :: real \<Rightarrow> real \<Rightarrow> real"
   202   "divide :: real \<Rightarrow> real \<Rightarrow> real"]]
   203 
   204 lemma [code]: "inverse r = 1 / r" for r :: real
   205   by (fact inverse_eq_divide)
   206 
   207 notepad
   208 begin
   209   have "cos (pi/2) = 0" by (rule cos_pi_half)
   210   moreover have "cos (pi/2) \<noteq> 0" by eval
   211   ultimately have False by blast
   212 end
   213 
   214 end