# HG changeset patch
# User bulwahn
# Date 1310211718 -7200
# Node ID 6b2bdc57155b7f945cdbac8dc6c18e24df820621
# Parent  1ba5331b462384d38771d7fe964bcc5fd56c7f06
adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)

diff -r 1ba5331b4623 -r 6b2bdc57155b src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy	Sat Jul 09 13:41:58 2011 +0200
@@ -141,9 +141,9 @@
 
 subsection {* Floor function *}
 
-definition
-  floor :: "'a::archimedean_field \<Rightarrow> int" where
-  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+class floor_ceiling = archimedean_field +
+  fixes floor :: "'a \<Rightarrow> int"
+  assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
 
 notation (xsymbols)
   floor  ("\<lfloor>_\<rfloor>")
@@ -151,9 +151,6 @@
 notation (HTML output)
   floor  ("\<lfloor>_\<rfloor>")
 
-lemma floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
-  unfolding floor_def using floor_exists1 by (rule theI')
-
 lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
   using floor_correct [of x] floor_exists1 [of x] by auto
 
@@ -273,7 +270,7 @@
 subsection {* Ceiling function *}
 
 definition
-  ceiling :: "'a::archimedean_field \<Rightarrow> int" where
+  ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
   [code del]: "ceiling x = - floor (- x)"
 
 notation (xsymbols)
diff -r 1ba5331b4623 -r 6b2bdc57155b src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/HOL/Rat.thy	Sat Jul 09 13:41:58 2011 +0200
@@ -739,6 +739,20 @@
   qed
 qed
 
+instantiation rat :: floor_ceiling
+begin
+
+definition [code del]:
+  "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+  fix x :: rat
+  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+    unfolding floor_rat_def using floor_exists1 by (rule theI')
+qed
+
+end
+
 lemma floor_Fract: "floor (Fract a b) = a div b"
   using rat_floor_lemma [of a b]
   by (simp add: floor_unique)
diff -r 1ba5331b4623 -r 6b2bdc57155b src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/HOL/RealDef.thy	Sat Jul 09 13:41:58 2011 +0200
@@ -793,6 +793,20 @@
     done
 qed
 
+instantiation real :: floor_ceiling
+begin
+
+definition [code del]:
+  "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+  fix x :: real
+  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+    unfolding floor_real_def using floor_exists1 by (rule theI')
+qed
+
+end
+
 subsection {* Completeness *}
 
 lemma not_positive_Real: