# HG changeset patch
# User haftmann
# Date 1497987719 -7200
# Node ID 2463cba9f18f0b82a6daa9adf5adc0550a339238
# Parent  bc5e6461f759f622cd29b7c3882de2d96604a214
stripped code pre/postprocessor setup for real from superfluous rules

diff -r bc5e6461f759 -r 2463cba9f18f src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Jun 21 17:13:55 2017 +0100
+++ b/src/HOL/Real.thy	Tue Jun 20 21:41:59 2017 +0200
@@ -1319,11 +1319,6 @@
 
 subsection \<open>Numerals and Arithmetic\<close>
 
-lemma [code_abbrev]:   (*FIXME*)
-  "real_of_int (numeral k) = numeral k"
-  "real_of_int (- numeral k) = - numeral k"
-  by simp_all
-
 declaration \<open>
   K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
     (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
@@ -1634,39 +1629,29 @@
 text \<open>Formal constructor\<close>
 
 definition Ratreal :: "rat \<Rightarrow> real"
-  where [code_abbrev, simp]: "Ratreal = of_rat"
+  where [code_abbrev, simp]: "Ratreal = real_of_rat"
 
 code_datatype Ratreal
 
 
-text \<open>Numerals\<close>
-
-lemma [code_abbrev]: "(of_rat (of_int a) :: real) = of_int a"
-  by simp
-
-lemma [code_abbrev]: "(of_rat 0 :: real) = 0"
-  by simp
+text \<open>Quasi-Numerals\<close>
 
-lemma [code_abbrev]: "(of_rat 1 :: real) = 1"
-  by simp
-
-lemma [code_abbrev]: "(of_rat (- 1) :: real) = - 1"
-  by simp
-
-lemma [code_abbrev]: "(of_rat (numeral k) :: real) = numeral k"
-  by simp
-
-lemma [code_abbrev]: "(of_rat (- numeral k) :: real) = - numeral k"
-  by simp
+lemma [code_abbrev]:
+  "real_of_rat (numeral k) = numeral k"
+  "real_of_rat (- numeral k) = - numeral k"
+  "real_of_rat (rat_of_int a) = real_of_int a"
+  by simp_all
 
 lemma [code_post]:
-  "(of_rat (1 / numeral k) :: real) = 1 / numeral k"
-  "(of_rat (numeral k / numeral l) :: real) = numeral k / numeral l"
-  "(of_rat (- (1 / numeral k)) :: real) = - (1 / numeral k)"
-  "(of_rat (- (numeral k / numeral l)) :: real) = - (numeral k / numeral l)"
+  "real_of_rat 0 = 0"
+  "real_of_rat 1 = 1"
+  "real_of_rat (- 1) = - 1"
+  "real_of_rat (1 / numeral k) = 1 / numeral k"
+  "real_of_rat (numeral k / numeral l) = numeral k / numeral l"
+  "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)"
+  "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)"
   by (simp_all add: of_rat_divide of_rat_minus)
 
-
 text \<open>Operations\<close>
 
 lemma zero_real_code [code]: "0 = Ratreal 0"