src/HOL/Real/RComplete.thy
 changeset 21404 eb85850d3eb7 parent 21210 c17fd2df4e9e child 22998 97e1f9c2cc46
```--- a/src/HOL/Real/RComplete.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Real/RComplete.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -432,18 +432,19 @@
subsection{*Floor and Ceiling Functions from the Reals to the Integers*}

definition
-  floor :: "real => int"
+  floor :: "real => int" where
"floor r = (LEAST n::int. r < real (n+1))"

-  ceiling :: "real => int"
+definition
+  ceiling :: "real => int" where
"ceiling r = - floor (- r)"

notation (xsymbols)
-  floor  ("\<lfloor>_\<rfloor>")
+  floor  ("\<lfloor>_\<rfloor>") and
ceiling  ("\<lceil>_\<rceil>")

notation (HTML output)
-  floor  ("\<lfloor>_\<rfloor>")
+  floor  ("\<lfloor>_\<rfloor>") and
ceiling  ("\<lceil>_\<rceil>")

@@ -933,9 +934,11 @@
subsection {* Versions for the natural numbers *}

definition
-  natfloor :: "real => nat"
+  natfloor :: "real => nat" where
"natfloor x = nat(floor x)"
-  natceiling :: "real => nat"
+
+definition
+  natceiling :: "real => nat" where
"natceiling x = nat(ceiling x)"

lemma natfloor_zero [simp]: "natfloor 0 = 0"```