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
```