Move NUM_FLOOR/NUM_CEILING to realaxTheory

[binghe]

Hi,

The floor and ceiling of real numbers are more naturally defined on integers (see INT_FLOOR and INT_CEILING in intrealTheory), but the NUM_FLOOR and NUM_CEILING defined in realTheory are still useful (they only work on positive reals) sometimes:

val NUM_FLOOR_def = zDefine`
   NUM_FLOOR (x:real) = LEAST (n:num). real_of_num (n+1) > x`;

val NUM_CEILING_def = zDefine`
   NUM_CEILING (x:real) = LEAST (n:num). x <= real_of_num n`;

The problem is that both NUM_FLOOR and INT_FLOOR are overloaded by flr (so is clg for NUM_CEILING, etc.), and currently there's no good way to set preferences to NUM_FLOOR. Since real_of_rat was opened somewhere in the middle of dependencies, this has become a problem.

For example, in examples/probability/large_numberTheory (NOTE: the whole probability theory was developed without using any integers, directly), I had to use the following code to put NUM_FLOOR over INT_FLOOR:

val _ = bring_to_front_overload "flr" {Name = "NUM_FLOOR",   Thy = "real"};
val _ = bring_to_front_overload "clg" {Name = "NUM_CEILING", Thy = "real"};

I was thinking (also due to some discussions on Discord) that putting NUM_FLOOR and NUM_CEILING into the operator list of realLib.prefer_real may help, but actually it doesn't: I cannot call prefer_real() in large_numberTheory where extreals should be preferred. Instead, I had to use deprecate_int () and deprecate_rat () to disable the parsing preferences of integers and rationals.

To minimize incompatibilities, I think it's reasonable to add a new function realLib.prefer_num_floor, focusing on these two operators. (Other solutions are welcome.) This is what's done in this PR.

--Chun

[mn200]

If you only want to prefer two constants in a child theory, I think getting the user to write

Overload flr = “real$NUM_FLOOR”
Overload clg = “real$NUM_CEILING”

is a more light-weight solution.

[binghe]

If you only want to prefer two constants in a child theory, I think getting the user to write

Overload flr = “real$NUM_FLOOR”
Overload clg = “real$NUM_CEILING”

is a more light-weight solution.

So, redefine the same overloads will get them in higher priority? Alright, I'll cancel the new function. Can we still keep the changes in realSyntax and the movements of constants?

[mn200]

Yes, that's explicitly desired behaviour of overload_on (which lies behind Overload), and allows micro-tweaks to default priorities.

But yes, please keep the other changes; making realSyntax better is very desirable.

[binghe]

Canceled the new function, and now I re-defined those overloads in large_numberTheory.

[mn200]

Thanks!