merged

--- a/src/HOL/IsaMakefile	Mon Nov 14 11:14:06 2011 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 14 12:29:19 2011 +0100
@@ -435,6 +435,7 @@
   Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
   Library/Code_Char_ord.thy Library/Code_Integer.thy			\
   Library/Code_Natural.thy Library/Code_Prolog.thy			\
+  Library/Code_Real_Approx_By_Float.thy					\
   Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
   Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
   Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy	\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Nov 14 12:29:19 2011 +0100
@@ -0,0 +1,148 @@
+(* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
+
+theory Code_Real_Approx_By_Float
+imports Complex_Main "~~/src/HOL/Library/Code_Integer"
+begin
+
+text{* \textbf{WARNING} This theory implements mathematical reals by machine
+reals (floats). This is inconsistent. See the proof of False at the end of
+the theory, where an equality on mathematical reals is (incorrectly)
+disproved by mapping it to machine reals.
+
+The value command cannot display real results yet.
+
+The only legitimate use of this theory is as a tool for code generation
+purposes. *}
+
+code_type real
+  (SML   "real")
+  (OCaml "float")
+
+code_const Ratreal
+  (SML "error/ \"Bad constant: Ratreal\"")
+
+code_const "0 :: real"
+  (SML   "0.0")
+  (OCaml "0.0")
+declare zero_real_code[code_unfold del]
+
+code_const "1 :: real"
+  (SML   "1.0")
+  (OCaml "1.0")
+declare one_real_code[code_unfold del]
+
+code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
+  (SML   "Real.== ((_), (_))")
+  (OCaml "Pervasives.(=)")
+
+code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
+  (SML   "Real.<= ((_), (_))")
+  (OCaml "Pervasives.(<=)")
+
+code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
+  (SML   "Real.< ((_), (_))")
+  (OCaml "Pervasives.(<)")
+
+code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
+  (SML   "Real.+ ((_), (_))")
+  (OCaml "Pervasives.( +. )")
+
+code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
+  (SML   "Real.* ((_), (_))")
+  (OCaml "Pervasives.( *. )")
+
+code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
+  (SML   "Real.- ((_), (_))")
+  (OCaml "Pervasives.( -. )")
+
+code_const "uminus :: real \<Rightarrow> real"
+  (SML   "Real.~")
+  (OCaml "Pervasives.( ~-. )")
+
+code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
+  (SML   "Real.'/ ((_), (_))")
+  (OCaml "Pervasives.( '/. )")
+
+code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
+  (SML   "Real.== ((_:real), (_))")
+
+code_const "sqrt :: real \<Rightarrow> real"
+  (SML   "Math.sqrt")
+  (OCaml "Pervasives.sqrt")
+declare sqrt_def[code del]
+
+definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+
+lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
+  unfolding real_exp_def ..
+
+code_const real_exp
+  (SML   "Math.exp")
+  (OCaml "Pervasives.exp")
+declare real_exp_def[code del]
+declare exp_def[code del]
+
+hide_const (open) real_exp
+
+code_const ln
+  (SML   "Math.ln")
+  (OCaml "Pervasives.ln")
+declare ln_def[code del]
+
+code_const cos
+  (SML   "Math.cos")
+  (OCaml "Pervasives.cos")
+declare cos_def[code del]
+
+code_const sin
+  (SML   "Math.sin")
+  (OCaml "Pervasives.sin")
+declare sin_def[code del]
+
+code_const pi
+  (SML   "Math.pi")
+  (OCaml "Pervasives.pi")
+declare pi_def[code del]
+
+code_const arctan
+  (SML   "Math.atan")
+  (OCaml "Pervasives.atan")
+declare arctan_def[code del]
+
+code_const arccos
+  (SML   "Math.scos")
+  (OCaml "Pervasives.acos")
+declare arccos_def[code del]
+
+code_const arcsin
+  (SML   "Math.asin")
+  (OCaml "Pervasives.asin")
+declare arcsin_def[code del]
+
+definition real_of_int :: "int \<Rightarrow> real" where
+  "real_of_int \<equiv> of_int"
+
+code_const real_of_int
+  (SML "Real.fromInt")
+  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
+
+lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
+  unfolding real_of_int_def ..
+
+hide_const (open) real_of_int
+
+declare number_of_real_code [code_unfold del]
+
+lemma "False"
+proof-
+  have "cos(pi/2) = 0" by(rule cos_pi_half)
+  moreover have "cos(pi/2) \<noteq> 0" by eval
+  ultimately show "False" by blast
+qed
+
+definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))"
+
+export_code test
+  in OCaml file -
+
+end

--- a/src/HOL/Library/ROOT.ML	Mon Nov 14 11:14:06 2011 +0100
+++ b/src/HOL/Library/ROOT.ML	Mon Nov 14 12:29:19 2011 +0100
@@ -3,4 +3,5 @@
 
 use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
   "Product_Lattice",
-  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
+  "Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*),
+  "Code_Real_Approx_By_Float" ];