Move NUM_FLOOR and NUM_CEILING to realaxTheory

Author: binghe

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            *)
 (*                                                                           *)