# HG changeset patch
# User Achim D. Brucker <adbrucker@0x5f.org>
# Date 1658733861 -3600
# Node ID f1141438b4db25ed33c6f8870d251832aa5be40c
# Parent  8b0dbfbde0320e5b167ce1cb899dd00c88945aa7
more correct approximation (contributed by Achim Brucker)

diff -r 8b0dbfbde032 -r f1141438b4db src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Aug 08 20:27:54 2022 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Mon Jul 25 08:24:21 2022 +0100
@@ -20,14 +20,69 @@
   purposes.
 \<close>
 
+definition Realfract :: \<open>real \<Rightarrow> real \<Rightarrow> real\<close>
+  where \<open>Realfract p q = p / q\<close>
+
+code_datatype Realfract
+
+context
+begin
+
+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)
+
+qualified definition exp_real :: \<open>real \<Rightarrow> real\<close>
+  where [code_abbrev, code del]: \<open>exp_real = exp\<close>
+
+qualified definition sin_real :: \<open>real \<Rightarrow> real\<close>
+  where [code_abbrev, code del]: \<open>sin_real = sin\<close>
+
+qualified definition cos_real :: \<open>real \<Rightarrow> real\<close>
+  where [code_abbrev, code del]: \<open>cos_real = cos\<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>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>plus :: 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]]
+
+code_reserved SML Real
+
 code_printing
   type_constructor real \<rightharpoonup>
     (SML) "real"
     and (OCaml) "float"
 
 code_printing
-  constant Ratreal \<rightharpoonup>
-    (SML) "error/ \"Bad constant: Ratreal\""
+  constant Realfract \<rightharpoonup> (SML) "_/ '// _"
 
 code_printing
   constant "0 :: real" \<rightharpoonup>
@@ -80,132 +135,55 @@
     and (OCaml) "Pervasives.( '/. )"
 
 code_printing
-  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
-    (SML) "Real.== ((_:real), (_))"
-
-code_printing
   constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
     (SML) "Math.sqrt"
     and (OCaml) "Pervasives.sqrt"
-declare sqrt_def[code del]
-
-context
-begin
-
-qualified definition real_exp :: "real \<Rightarrow> real"
-  where "real_exp = exp"
-
-lemma exp_eq_real_exp [code_unfold]: "exp = real_exp"
-  unfolding real_exp_def ..
-
-end
 
 code_printing
-  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
+  constant Code_Real_Approx_By_Float.exp_real \<rightharpoonup>
     (SML) "Math.exp"
     and (OCaml) "Pervasives.exp"
-declare Code_Real_Approx_By_Float.real_exp_def[code del]
-declare exp_def[code del]
 
 code_printing
   constant ln \<rightharpoonup>
     (SML) "Math.ln"
     and (OCaml) "Pervasives.ln"
-declare ln_real_def[code del]
 
 code_printing
-  constant cos \<rightharpoonup>
+  constant Code_Real_Approx_By_Float.cos_real \<rightharpoonup>
     (SML) "Math.cos"
     and (OCaml) "Pervasives.cos"
-declare cos_def[code del]
 
 code_printing
-  constant sin \<rightharpoonup>
+  constant Code_Real_Approx_By_Float.sin_real \<rightharpoonup>
     (SML) "Math.sin"
     and (OCaml) "Pervasives.sin"
-declare sin_def[code del]
 
 code_printing
   constant pi \<rightharpoonup>
     (SML) "Math.pi"
     and (OCaml) "Pervasives.pi"
-declare pi_def[code del]
 
 code_printing
   constant arctan \<rightharpoonup>
     (SML) "Math.atan"
     and (OCaml) "Pervasives.atan"
-declare arctan_def[code del]
 
 code_printing
   constant arccos \<rightharpoonup>
     (SML) "Math.scos"
     and (OCaml) "Pervasives.acos"
-declare arccos_def[code del]
 
 code_printing
   constant arcsin \<rightharpoonup>
     (SML) "Math.asin"
     and (OCaml) "Pervasives.asin"
-declare arcsin_def[code del]
-
-definition real_of_integer :: "integer \<Rightarrow> real"
-  where "real_of_integer = of_int \<circ> int_of_integer"
 
 code_printing
-  constant real_of_integer \<rightharpoonup>
+  constant Code_Real_Approx_By_Float.real_of_integer \<rightharpoonup>
     (SML) "Real.fromInt"
     and (OCaml) "Pervasives.float/ (Big'_int.to'_int (_))"
 
-context
-begin
-
-qualified definition real_of_int :: "int \<Rightarrow> real"
-  where [code_abbrev]: "real_of_int = of_int"
-
-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_unfold del]: "0 \<equiv> (of_rat 0 :: real)"
-  by simp
-
-lemma [code_unfold del]: "1 \<equiv> (of_rat 1 :: real)"
-  by simp
-
-lemma [code_unfold del]: "numeral k \<equiv> (of_rat (numeral k) :: real)"
-  by simp
-
-lemma [code_unfold del]: "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
-  by simp
-
-end
-
-code_printing
-  constant Ratreal \<rightharpoonup> (SML)
-
-definition Realfract :: "int \<Rightarrow> int \<Rightarrow> real"
-  where "Realfract p q = of_int p / of_int q"
-
-code_datatype Realfract
-
-code_printing
-  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
-
-lemma [code]: "Ratreal r = case_prod Realfract (quotient_of r)"
-  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
-
-declare [[code drop: "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
-  "plus :: real \<Rightarrow> real \<Rightarrow> real"
-  "uminus :: real \<Rightarrow> real"
-  "minus :: real \<Rightarrow> real \<Rightarrow> real"
-  "times :: real \<Rightarrow> real \<Rightarrow> real"
-  "divide :: real \<Rightarrow> real \<Rightarrow> real"
-  "(<) :: real \<Rightarrow> real \<Rightarrow> bool"
-  "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"]]
-
-lemma [code]: "inverse r = 1 / r" for r :: real
-  by (fact inverse_eq_divide)
-
 notepad
 begin
   have "cos (pi/2) = 0" by (rule cos_pi_half)