# HG changeset patch
# User hoelzl
# Date 1371811268 -7200
# Node ID 140ae824ea4a8cce1d113b2b4f758c83a3a2deb4
# Parent  c2f30ba4bb98b5a8432262be9b9413e54f77adb3
Code_Real_Approx_By_Float: remove code equations using Ratreal

diff -r c2f30ba4bb98 -r 140ae824ea4a src/HOL/Library/Code_Real_Approx_By_Float.thy
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Jun 21 09:00:26 2013 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Jun 21 12:41:08 2013 +0200
@@ -151,6 +151,50 @@
 
 hide_const (open) real_of_int
 
+code_const Ratreal (SML)
+
+definition Realfract :: "int => int => real"
+where
+  "Realfract p q = of_int p / of_int q"
+
+code_datatype Realfract
+
+code_const Realfract
+  (SML "Real.fromInt _/ '// Real.fromInt _")
+
+lemma [code]:
+  "Ratreal r = split Realfract (quotient_of r)"
+  by (cases r) (simp add: Realfract_def quotient_of_Fract of_rat_rat)
+
+lemma [code, code del]:
+  "(HOL.equal :: real=>real=>bool) = (HOL.equal :: real => real => bool) "
+  ..
+
+lemma [code, code del]:
+  "(plus :: real => real => real) = plus"
+  ..
+
+lemma [code, code del]:
+  "(uminus :: real => real) = uminus"
+  ..
+
+lemma [code, code del]:
+  "(minus :: real => real => real) = minus"
+  ..
+
+lemma [code, code del]:
+  "(times :: real => real => real) = times"
+  ..
+
+lemma [code, code del]:
+  "(divide :: real => real => real) = divide"
+  ..
+
+lemma [code]:
+  fixes r :: real
+  shows "inverse r = 1 / r"
+  by (fact inverse_eq_divide)
+
 notepad
 begin
   have "cos (pi/2) = 0" by (rule cos_pi_half)