Move NUM_FLOOR/NUM_CEILING to realaxTheory (#1256)

* Add realLib.prefer_num_floor

* Move NUM_FLOOR and NUM_CEILING to realaxTheory

* Canceled prefer_num_floor(), using (redefined) Overload instead

Author: binghe

examples/probability/large_numberScript.sml

@@ -42,11 +42,11 @@ val _ = hide "W";
 val _ = intLib.deprecate_int ();
 val _ = ratLib.deprecate_rat ();
 
-(* NOTE: The above deprecate settings do not cover "flr" and "clg", which
-   are overloaded again in intrealTheory.
+(* Prefer NUM_FLOOR and NUM_CEILING (over INT_FLOOR/INT_CEILING) by redefining
+   their overloads.
  *)
-val _ = bring_to_front_overload "flr" {Name = "NUM_FLOOR",   Thy = "real"};
-val _ = bring_to_front_overload "clg" {Name = "NUM_CEILING", Thy = "real"};
+Overload flr = “realax$NUM_FLOOR”
+Overload clg = “realax$NUM_CEILING”
 
 (* ------------------------------------------------------------------------- *)
 (*  Definitions                                                              *)

src/real/realLib.sig

@@ -11,8 +11,8 @@ sig
   val REAL_ARITH          : term -> thm
   val REAL_ASM_ARITH_TAC  : tactic
 
-   val real_ss : simpLib.simpset
    (* Incorporates simpsets for bool, pair, and arithmetic *)
+   val real_ss : simpLib.simpset
 
    (* syntax *)
    val prefer_real     : unit -> unit

src/real/realScript.sml

@@ -3797,19 +3797,12 @@ val lt_int = store_thm(
     Q.EXISTS_TAC `0` THEN SRW_TAC [][REAL_NEG_LE0]
   ]);
 
-
 (*---------------------------------------------------------------------------*)
-(* Floor and ceiling (nums)                                                  *)
+(* Floor and ceiling (nums) (NOTE: Their definitions are moved to realax)    *)
 (*---------------------------------------------------------------------------*)
 
-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`;
-
-val _ = overload_on ("flr",``NUM_FLOOR``);
-val _ = overload_on ("clg",``NUM_CEILING``);
+Theorem NUM_FLOOR_def   = NUM_FLOOR_def
+Theorem NUM_CEILING_def = NUM_CEILING_def
 
 val lem = SIMP_RULE arith_ss [REAL_POS,REAL_ADD_RID]
               (Q.SPECL[`y`,`&n`,`0r`,`1r`] REAL_LTE_ADD2);

src/real/realSyntax.sig

@@ -12,6 +12,8 @@ sig
   val negate_tm      : term
   val real_injection : term (* the injection from :num -> :real *)
   val inv_tm         : term
+  val NUM_FLOOR_tm   : term
+  val NUM_CEILING_tm : term
 
   (* binary operators *)
   val div_tm         : term

src/real/realSyntax.sml

@@ -1,9 +1,9 @@
 structure realSyntax :> realSyntax =
 struct
-
-  local open realaxTheory in end;
   open HolKernel Abbrev;
 
+  local open realaxTheory numSyntax in end;
+
   val ERR = mk_HOL_ERR "realSyntax";
 
   (* Fundamental terms, mainly constants *)
@@ -12,8 +12,9 @@ struct
   val real_ty = mk_thy_type {Thy = "realax", Tyop = "real", Args = []}
   val bop_ty = real_ty --> real_ty --> real_ty
   val rel_ty = real_ty --> real_ty --> bool
+  val num_ty = numSyntax.num
 
-  val real_injection = mk_raconst("real_of_num", numSyntax.num --> real_ty)
+  val real_injection = mk_raconst("real_of_num", num_ty --> real_ty)
 
   val zero_tm = mk_comb(real_injection, numSyntax.zero_tm)
   val one_tm = mk_comb(real_injection, numSyntax.mk_numeral (Arbnum.fromInt 1))
@@ -23,7 +24,7 @@ struct
   val minus_tm = mk_raconst("real_sub", bop_ty)
   val mult_tm = mk_raconst("real_mul", bop_ty)
   val div_tm = mk_raconst("/", bop_ty)
-  val exp_tm = mk_raconst("pow", real_ty --> numSyntax.num --> real_ty)
+  val exp_tm = mk_raconst("pow", real_ty --> num_ty --> real_ty)
 
   val real_eq_tm = mk_thy_const { Thy = "min", Name = "=", Ty = rel_ty}
   val less_tm = mk_raconst("real_lt", rel_ty)
@@ -34,6 +35,9 @@ struct
   val min_tm = mk_raconst("min", bop_ty)
   val max_tm = mk_raconst("max", bop_ty)
 
+  val NUM_FLOOR_tm   = mk_raconst("NUM_FLOOR",   real_ty --> num_ty);
+  val NUM_CEILING_tm = mk_raconst("NUM_CEILING", real_ty --> num_ty);
+
   (* Functions *)
 
   fun dest1 c fnm nm t = let

src/real/realaxScript.sml

@@ -284,6 +284,18 @@ Proof
   end
 QED
 
+(* Floor and ceiling (nums) *)
+Definition NUM_FLOOR_def[nocompute] :
+   NUM_FLOOR (x:real) = LEAST (n:num). real_of_num (n+1) > x
+End
+
+Definition NUM_CEILING_def[nocompute] :
+   NUM_CEILING (x:real) = LEAST (n:num). x <= real_of_num n
+End
+
+Overload flr = “NUM_FLOOR”
+Overload clg = “NUM_CEILING”
+
 (* ------------------------------------------------------------------------- *)
 (* Some elementary "bootstrapping" lemmas needed by RealArith.sml            *)
 (*                                                                           *)