--- a/src/HOL/Archimedean_Field.thy Sat Jul 09 13:41:58 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy Sat Jul 09 19:28:33 2011 +0200
@@ -271,7 +271,7 @@
definition
ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
- [code del]: "ceiling x = - floor (- x)"
+ "ceiling x = - floor (- x)"
notation (xsymbols)
ceiling ("\<lceil>_\<rceil>")
--- a/src/HOL/Rat.thy Sat Jul 09 13:41:58 2011 +0200
+++ b/src/HOL/Rat.thy Sat Jul 09 19:28:33 2011 +0200
@@ -1097,6 +1097,10 @@
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
qed
+lemma rat_floor_code [code]:
+ "floor p = (let (a, b) = quotient_of p in a div b)"
+by (cases p) (simp add: quotient_of_Fract floor_Fract)
+
instantiation rat :: equal
begin
--- a/src/HOL/RealDef.thy Sat Jul 09 13:41:58 2011 +0200
+++ b/src/HOL/RealDef.thy Sat Jul 09 19:28:33 2011 +0200
@@ -1762,6 +1762,9 @@
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
by (simp add: of_rat_divide)
+lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
+ by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code)
+
definition (in term_syntax)
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"