add Code_Real_Approx_By_Float
authorhoelzl
Mon Nov 14 11:50:52 2011 +0100 (2011-11-14 ago)
changeset 4548334d07cf7d207
parent 45482 8f32682f78fe
child 45485 7a0975c9dd26
add Code_Real_Approx_By_Float
src/HOL/IsaMakefile
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Nov 14 09:25:05 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 14 11:50:52 2011 +0100
     1.3 @@ -435,6 +435,7 @@
     1.4    Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
     1.5    Library/Code_Char_ord.thy Library/Code_Integer.thy			\
     1.6    Library/Code_Natural.thy Library/Code_Prolog.thy			\
     1.7 +  Library/Code_Real_Approx_By_Float.thy					\
     1.8    Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
     1.9    Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
    1.10    Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy	\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 11:50:52 2011 +0100
     2.3 @@ -0,0 +1,148 @@
     2.4 +(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
     2.5 +
     2.6 +theory Code_Real_Approx_By_Float
     2.7 +imports Complex_Main "~~/src/HOL/Library/Code_Integer"
     2.8 +begin
     2.9 +
    2.10 +text{* \textbf{WARNING} This theory implements mathematical reals by machine
    2.11 +reals (floats). This is inconsistent. See the proof of False at the end of
    2.12 +the theory, where an equality on mathematical reals is (incorrectly)
    2.13 +disproved by mapping it to machine reals.
    2.14 +
    2.15 +The value command cannot display real results yet.
    2.16 +
    2.17 +The only legitimate use of this theory is as a tool for code generation
    2.18 +purposes. *}
    2.19 +
    2.20 +code_type real
    2.21 +  (SML   "real")
    2.22 +  (OCaml "float")
    2.23 +
    2.24 +code_const Ratreal
    2.25 +  (SML "error/ \"Bad constant: Ratreal\"")
    2.26 +
    2.27 +code_const "0 :: real"
    2.28 +  (SML   "0.0")
    2.29 +  (OCaml "0.0")
    2.30 +declare zero_real_code[code_unfold del]
    2.31 +
    2.32 +code_const "1 :: real"
    2.33 +  (SML   "1.0")
    2.34 +  (OCaml "1.0")
    2.35 +declare one_real_code[code_unfold del]
    2.36 +
    2.37 +code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    2.38 +  (SML   "Real.== ((_), (_))")
    2.39 +  (OCaml "Pervasives.(=)")
    2.40 +
    2.41 +code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
    2.42 +  (SML   "Real.<= ((_), (_))")
    2.43 +  (OCaml "Pervasives.(<=)")
    2.44 +
    2.45 +code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
    2.46 +  (SML   "Real.< ((_), (_))")
    2.47 +  (OCaml "Pervasives.(<)")
    2.48 +
    2.49 +code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
    2.50 +  (SML   "Real.+ ((_), (_))")
    2.51 +  (OCaml "Pervasives.( +. )")
    2.52 +
    2.53 +code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
    2.54 +  (SML   "Real.* ((_), (_))")
    2.55 +  (OCaml "Pervasives.( *. )")
    2.56 +
    2.57 +code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
    2.58 +  (SML   "Real.- ((_), (_))")
    2.59 +  (OCaml "Pervasives.( -. )")
    2.60 +
    2.61 +code_const "uminus :: real \<Rightarrow> real"
    2.62 +  (SML   "Real.~")
    2.63 +  (OCaml "Pervasives.( ~-. )")
    2.64 +
    2.65 +code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
    2.66 +  (SML   "Real.'/ ((_), (_))")
    2.67 +  (OCaml "Pervasives.( '/. )")
    2.68 +
    2.69 +code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
    2.70 +  (SML   "Real.== ((_:real), (_))")
    2.71 +
    2.72 +code_const "sqrt :: real \<Rightarrow> real"
    2.73 +  (SML   "Math.sqrt")
    2.74 +  (OCaml "Pervasives.sqrt")
    2.75 +declare sqrt_def[code del]
    2.76 +
    2.77 +definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
    2.78 +
    2.79 +lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
    2.80 +  unfolding real_exp_def ..
    2.81 +
    2.82 +code_const real_exp
    2.83 +  (SML   "Math.exp")
    2.84 +  (OCaml "Pervasives.exp")
    2.85 +declare real_exp_def[code del]
    2.86 +declare exp_def[code del]
    2.87 +
    2.88 +hide_const (open) real_exp
    2.89 +
    2.90 +code_const ln
    2.91 +  (SML   "Math.ln")
    2.92 +  (OCaml "Pervasives.ln")
    2.93 +declare ln_def[code del]
    2.94 +
    2.95 +code_const cos
    2.96 +  (SML   "Math.cos")
    2.97 +  (OCaml "Pervasives.cos")
    2.98 +declare cos_def[code del]
    2.99 +
   2.100 +code_const sin
   2.101 +  (SML   "Math.sin")
   2.102 +  (OCaml "Pervasives.sin")
   2.103 +declare sin_def[code del]
   2.104 +
   2.105 +code_const pi
   2.106 +  (SML   "Math.pi")
   2.107 +  (OCaml "Pervasives.pi")
   2.108 +declare pi_def[code del]
   2.109 +
   2.110 +code_const arctan
   2.111 +  (SML   "Math.atan")
   2.112 +  (OCaml "Pervasives.atan")
   2.113 +declare arctan_def[code del]
   2.114 +
   2.115 +code_const arccos
   2.116 +  (SML   "Math.scos")
   2.117 +  (OCaml "Pervasives.acos")
   2.118 +declare arccos_def[code del]
   2.119 +
   2.120 +code_const arcsin
   2.121 +  (SML   "Math.asin")
   2.122 +  (OCaml "Pervasives.asin")
   2.123 +declare arcsin_def[code del]
   2.124 +
   2.125 +definition real_of_int :: "int \<Rightarrow> real" where
   2.126 +  "real_of_int \<equiv> of_int"
   2.127 +
   2.128 +code_const real_of_int
   2.129 +  (SML "Real.fromInt")
   2.130 +  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
   2.131 +
   2.132 +lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
   2.133 +  unfolding real_of_int_def ..
   2.134 +
   2.135 +hide_const (open) real_of_int
   2.136 +
   2.137 +declare number_of_real_code [code_unfold del]
   2.138 +
   2.139 +lemma "False"
   2.140 +proof-
   2.141 +  have "cos(pi/2) = 0" by(rule cos_pi_half)
   2.142 +  moreover have "cos(pi/2) \<noteq> 0" by eval
   2.143 +  ultimately show "False" by blast
   2.144 +qed
   2.145 +
   2.146 +definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))"
   2.147 +
   2.148 +export_code test
   2.149 +  in OCaml file -
   2.150 +
   2.151 +end
     3.1 --- a/src/HOL/Library/ROOT.ML	Mon Nov 14 09:25:05 2011 +0100
     3.2 +++ b/src/HOL/Library/ROOT.ML	Mon Nov 14 11:50:52 2011 +0100
     3.3 @@ -3,4 +3,5 @@
     3.4  
     3.5  use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
     3.6    "Product_Lattice",
     3.7 -  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
     3.8 +  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*),
     3.9 +  "Code_Real_Approx_By_Float" ];