src/HOL/Archimedean_Field.thy
changeset 37765 26bdfb7b680b
parent 35028 108662d50512
child 41959 b460124855b8
equal deleted inserted replaced
37764:3489daf839d5 37765:26bdfb7b680b
   141 
   141 
   142 subsection {* Floor function *}
   142 subsection {* Floor function *}
   143 
   143 
   144 definition
   144 definition
   145   floor :: "'a::archimedean_field \<Rightarrow> int" where
   145   floor :: "'a::archimedean_field \<Rightarrow> int" where
   146   [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
   146   "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
   147 
   147 
   148 notation (xsymbols)
   148 notation (xsymbols)
   149   floor  ("\<lfloor>_\<rfloor>")
   149   floor  ("\<lfloor>_\<rfloor>")
   150 
   150 
   151 notation (HTML output)
   151 notation (HTML output)
   272 
   272 
   273 subsection {* Ceiling function *}
   273 subsection {* Ceiling function *}
   274 
   274 
   275 definition
   275 definition
   276   ceiling :: "'a::archimedean_field \<Rightarrow> int" where
   276   ceiling :: "'a::archimedean_field \<Rightarrow> int" where
   277   [code del]: "ceiling x = - floor (- x)"
   277   "ceiling x = - floor (- x)"
   278 
   278 
   279 notation (xsymbols)
   279 notation (xsymbols)
   280   ceiling  ("\<lceil>_\<rceil>")
   280   ceiling  ("\<lceil>_\<rceil>")
   281 
   281 
   282 notation (HTML output)
   282 notation (HTML output)