src/HOL/Archimedean_Field.thy
 changeset 43704 47b0be18ccbe parent 41959 b460124855b8 child 43732 6b2bdc57155b
equal inserted replaced
43694:93dcfcf91484 43704:47b0be18ccbe
`   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   "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"`
`   146   [code del]: "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   "ceiling x = - floor (- x)"`
`   277   [code del]: "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)`