More properties of INT_FLOOR and INT_CEILING

[binghe]

Hi,

Recently I started needing INT_FLOOR and INT_CEILING of intrealTheory and immediately found that the existing set of theorems are missing some notable (and nice) ones, e.g. the following two "negated properties" (proof is from [1]) at the end of a chain of newly added theorems:

   [INT_CEILING_NEG]  Theorem (intrealTheory)      
      ⊢ ∀x. ⌈-x⌉ = -⌊x⌋

   [INT_FLOOR_NEG]  Theorem      
      ⊢ ∀x. ⌊-x⌋ = -⌈x⌉

However, I must say that all new proofs are quite simple, because the existing theorems (some proofs are hard) have indeed provided an axiomatic system where all the remaining properties of INT_FLOOR and INT_CEILING can be derived from just the existing ones without going into their original definition by LEAST bindings.

Besides, I also added a new definition for the "Fractional part" [2] of real numbers. Although there's no much supporting theorems for it, I believe this definition is famous and sometimes occurs in other definitions:

   [frac_def]  Definition      
      ⊢ ∀x. frac x = x − real_of_int ⌊x⌋

Furthermore, for the is_int predicate, I added the following alternative definitions:

   [is_int_alt]  Theorem      
      ⊢ ∀x. is_int x ⇔ x = real_of_int ⌈x⌉
   
   [is_int_eq_frac_0]  Theorem      
      ⊢ ∀x. is_int x ⇔ frac x = 0
   
   [is_int_thm]  Theorem      
      ⊢ ∀x. is_int x ⇔ ⌊x⌋ = ⌈x⌉

I also cleaned up the script by explicitly opening arithmeticTheory, realTheory and intLib and then removed all functions calls with their prefixes. I think this is in the right direction causing no other issues.

Regards,

Chun Tian

[1] https://proofwiki.org/wiki/Floor_of_Negative_equals_Negative_of_Ceiling
[2] https://en.wikipedia.org/wiki/Fractional_part

[mn200]

Thanks for this: it's nice to see this theory getting some love.