Further streamlining of quick-and-dirty evaluation.

--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Jul 25 08:24:21 2022 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Wed Aug 10 18:26:22 2022 +0000
@@ -1,4 +1,6 @@
 (*  Title:      HOL/Library/Code_Real_Approx_By_Float.thy
+    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
+    Author:     Jose Divasón <jose.divasonm at unirioja.es>
     Author:     Florian Haftmann
     Author:     Johannes Hölzl
     Author:     Tobias Nipkow
@@ -20,10 +22,21 @@
   purposes.
 \<close>
 
-definition Realfract :: \<open>real \<Rightarrow> real \<Rightarrow> real\<close>
-  where \<open>Realfract p q = p / q\<close>
+context
+begin
+
+qualified definition real_of_integer :: "integer \<Rightarrow> real"
+  where [code_abbrev]: "real_of_integer = of_int \<circ> int_of_integer"
+
+end
 
-code_datatype Realfract
+code_datatype Code_Real_Approx_By_Float.real_of_integer \<open>(/) :: real \<Rightarrow> real \<Rightarrow> real\<close>
+
+lemma [code_unfold del]: "numeral k \<equiv> real_of_rat (numeral k)"
+  by simp
+
+lemma [code_unfold del]: "- numeral k \<equiv> real_of_rat (- numeral k)"
+  by simp
 
 context
 begin
@@ -31,11 +44,8 @@
 qualified definition real_of_int :: \<open>int \<Rightarrow> real\<close>
   where [code_abbrev]: \<open>real_of_int = of_int\<close>
 
-qualified definition real_of_integer :: "integer \<Rightarrow> real"
-  where [code_abbrev]: "real_of_integer = of_int \<circ> int_of_integer"
-
-lemma [code]: "real_of_int = real_of_integer \<circ> integer_of_int"
-  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
+lemma [code]: "real_of_int = Code_Real_Approx_By_Float.real_of_integer \<circ> integer_of_int"
+  by (simp add: fun_eq_iff Code_Real_Approx_By_Float.real_of_integer_def real_of_int_def)
 
 qualified definition exp_real :: \<open>real \<Rightarrow> real\<close>
   where [code_abbrev, code del]: \<open>exp_real = exp\<close>
@@ -46,33 +56,31 @@
 qualified definition cos_real :: \<open>real \<Rightarrow> real\<close>
   where [code_abbrev, code del]: \<open>cos_real = cos\<close>
 
+qualified definition tan_real :: \<open>real \<Rightarrow> real\<close>
+  where [code_abbrev, code del]: \<open>tan_real = tan\<close>
+
 end
 
-definition Quotreal :: \<open>int \<Rightarrow> int \<Rightarrow> real\<close>
-  where \<open>Quotreal p q = Realfract (of_int p) (of_int q)\<close>
-
-lemma [code]: "Ratreal r = case_prod Quotreal (quotient_of r)"
-  by (cases r) (simp add: Realfract_def Quotreal_def quotient_of_Fract of_rat_rat)
+lemma [code]: \<open>Ratreal r = (case quotient_of r of (p, q) \<Rightarrow> real_of_int p / real_of_int q)\<close>
+  by (cases r) (simp add: quotient_of_Fract of_rat_rat)
 
 lemma [code]: \<open>inverse r = 1 / r\<close> for r :: real
   by (fact inverse_eq_divide)
 
-lemma [code_unfold del]: "numeral k \<equiv> real_of_rat (numeral k)"
-  by simp
-
-lemma [code_unfold del]: "- numeral k \<equiv> real_of_rat (- numeral k)"
-  by simp
-
 declare [[code drop: \<open>HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool\<close>
+  \<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
+  \<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
   \<open>plus :: real \<Rightarrow> real \<Rightarrow> real\<close>
+  \<open>times :: real \<Rightarrow> real \<Rightarrow> real\<close>
   \<open>uminus :: real \<Rightarrow> real\<close>
   \<open>minus :: real \<Rightarrow> real \<Rightarrow> real\<close>
-  \<open>times :: real \<Rightarrow> real \<Rightarrow> real\<close>
   \<open>divide :: real \<Rightarrow> real \<Rightarrow> real\<close>
-  \<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
-  \<open>(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool\<close>
-  sqrt \<open>ln :: real \<Rightarrow> real\<close> pi
-  arcsin arccos arctan]]
+  sqrt
+  \<open>ln :: real \<Rightarrow> real\<close>
+  pi
+  arcsin
+  arccos
+  arctan]]
 
 code_reserved SML Real
 
@@ -80,109 +88,91 @@
   type_constructor real \<rightharpoonup>
     (SML) "real"
     and (OCaml) "float"
-
-code_printing
-  constant Realfract \<rightharpoonup> (SML) "_/ '// _"
-
-code_printing
-  constant "0 :: real" \<rightharpoonup>
+    and (Haskell) "Prelude.Double" (*Double precision*)
+| constant "0 :: real" \<rightharpoonup>
     (SML) "0.0"
     and (OCaml) "0.0"
-
-code_printing
-  constant "1 :: real" \<rightharpoonup>
+    and (Haskell) "0.0"
+| constant "1 :: real" \<rightharpoonup>
     (SML) "1.0"
     and (OCaml) "1.0"
-
-code_printing
-  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+    and (Haskell) "1.0"
+| constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
     (SML) "Real.== ((_), (_))"
     and (OCaml) "Pervasives.(=)"
-
-code_printing
-  constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+    and (Haskell) infix 4 "=="
+| class_instance real :: "HOL.equal" => (Haskell) - (*This is necessary. See the tutorial on code generation, page 29*)
+| constant "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
     (SML) "Real.<= ((_), (_))"
     and (OCaml) "Pervasives.(<=)"
-
-code_printing
-  constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+    and (Haskell) infix 4 "<="
+| constant "(<) :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
     (SML) "Real.< ((_), (_))"
     and (OCaml) "Pervasives.(<)"
-
-code_printing
-  constant "(+) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+    and (Haskell) infix 4 "<"
+| constant "(+) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Real.+ ((_), (_))"
     and (OCaml) "Pervasives.( +. )"
-
-code_printing
-  constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+    and (Haskell) infixl 6 "+"
+| constant "(*) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Real.* ((_), (_))"
-    and (OCaml) "Pervasives.( *. )"
-
-code_printing
-  constant "(-) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
-    (SML) "Real.- ((_), (_))"
-    and (OCaml) "Pervasives.( -. )"
-
-code_printing
-  constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
+    and (Haskell) infixl 7 "*"
+| constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Real.~"
     and (OCaml) "Pervasives.( ~-. )"
-
-code_printing
-  constant "(/) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+    and (Haskell) "negate"
+| constant "(-) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+    (SML) "Real.- ((_), (_))"
+    and (OCaml) "Pervasives.( -. )"
+    and (Haskell) infixl 6 "-"
+| constant "(/) :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Real.'/ ((_), (_))"
     and (OCaml) "Pervasives.( '/. )"
-
-code_printing
-  constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
+    and (Haskell) infixl 7 "/"
+| constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Math.sqrt"
     and (OCaml) "Pervasives.sqrt"
-
-code_printing
-  constant Code_Real_Approx_By_Float.exp_real \<rightharpoonup>
+    and (Haskell) "Prelude.sqrt" 
+| constant Code_Real_Approx_By_Float.exp_real \<rightharpoonup>
     (SML) "Math.exp"
     and (OCaml) "Pervasives.exp"
-
-code_printing
-  constant ln \<rightharpoonup>
+    and (Haskell) "Prelude.exp"
+| constant ln \<rightharpoonup>
     (SML) "Math.ln"
     and (OCaml) "Pervasives.ln"
-
-code_printing
-  constant Code_Real_Approx_By_Float.cos_real \<rightharpoonup>
+    and (Haskell) "Prelude.log"
+| constant Code_Real_Approx_By_Float.sin_real \<rightharpoonup>
+    (SML) "Math.sin"
+    and (OCaml) "Pervasives.sin"
+    and (Haskell) "Prelude.sin"
+| constant Code_Real_Approx_By_Float.cos_real \<rightharpoonup>
     (SML) "Math.cos"
     and (OCaml) "Pervasives.cos"
-
-code_printing
-  constant Code_Real_Approx_By_Float.sin_real \<rightharpoonup>
-    (SML) "Math.sin"
-    and (OCaml) "Pervasives.sin"
-
-code_printing
-  constant pi \<rightharpoonup>
+    and (Haskell) "Prelude.cos"
+| constant Code_Real_Approx_By_Float.tan_real \<rightharpoonup>
+    (SML) "Math.tan"
+    and (OCaml) "Pervasives.tan"
+    and (Haskell) "Prelude.tan"
+| constant pi \<rightharpoonup>
     (SML) "Math.pi"
-    and (OCaml) "Pervasives.pi"
-
-code_printing
-  constant arctan \<rightharpoonup>
+    (*missing in OCaml*)
+    and (Haskell) "Prelude.pi"
+| constant arcsin \<rightharpoonup>
+    (SML) "Math.asin"
+    and (OCaml) "Pervasives.asin"
+    and (Haskell) "Prelude.asin"
+| constant arccos \<rightharpoonup>
+    (SML) "Math.scos"
+    and (OCaml) "Pervasives.acos"
+    and (Haskell) "Prelude.acos"
+| constant arctan \<rightharpoonup>
     (SML) "Math.atan"
     and (OCaml) "Pervasives.atan"
-
-code_printing
-  constant arccos \<rightharpoonup>
-    (SML) "Math.scos"
-    and (OCaml) "Pervasives.acos"
-
-code_printing
-  constant arcsin \<rightharpoonup>
-    (SML) "Math.asin"
-    and (OCaml) "Pervasives.asin"
-
-code_printing
-  constant Code_Real_Approx_By_Float.real_of_integer \<rightharpoonup>
+    and (Haskell) "Prelude.atan"
+| constant Code_Real_Approx_By_Float.real_of_integer \<rightharpoonup>
     (SML) "Real.fromInt"
     and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
+    and (Haskell) "Prelude.fromIntegral (_)"
 
 notepad
 begin