Theory "intreal"

Parents     real   integer

Signature

Constant Type
INT_CEILING :real -> int
INT_FLOOR :real -> int
is_int :real -> bool
real_of_int :int -> real

Definitions

real_of_int 
|- ∀i. real_of_int i = if i < 0 then -&Num (-i) else &Num i
INT_FLOOR_def 
|- ∀x. flr x = LEAST_INT i. real_of_int (i + 1) > x
INT_CEILING_def 
|- ∀x. clg x = LEAST_INT i. x ≤ real_of_int i
is_int_def 
|- ∀x. is_int x ⇔ (x = real_of_int (flr x))