# HG changeset patch
# User bulwahn
# Date 1310232513 -7200
# Node ID a6ca7b83612fb1039dd0a4e9c9301f91b4169910
# Parent  6b2bdc57155b7f945cdbac8dc6c18e24df820621
adding code equations to execute floor and ceiling on rational and real numbers

diff -r 6b2bdc57155b -r a6ca7b83612f src/HOL/Archimedean_Field.thy
--- 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>")
diff -r 6b2bdc57155b -r a6ca7b83612f src/HOL/Rat.thy
--- 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
 
diff -r 6b2bdc57155b -r a6ca7b83612f src/HOL/RealDef.thy
--- 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"