Fix simplification of real$NUM_CEILING

Closes #1149

src/real/realSimps.sml

@@ -19,7 +19,7 @@ val arith_ss = boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ numSimps.ARITH_ss ++
 
 val SSFRAG = simpLib.register_frag o simpLib.SSFRAG
 
-val real_SS = simpLib.SSFRAG
+val real_SS = SSFRAG
   {name = SOME"real",
    ac = [],
    congs = [],
@@ -65,7 +65,7 @@ val real_SS = simpLib.SSFRAG
      "REAL_MAX_REFL", "REAL_LE_MAX1", "REAL_LE_MAX2", "REAL_MAX_ADD",
      "REAL_MAX_SUB"]};
 
-val real_ac_SS = simpLib.SSFRAG {
+val real_ac_SS = SSFRAG {
   name = SOME"real_ac",
   ac = [(SPEC_ALL REAL_ADD_ASSOC, SPEC_ALL REAL_ADD_SYM),
         (SPEC_ALL REAL_MUL_ASSOC, SPEC_ALL REAL_MUL_SYM)],
@@ -229,9 +229,25 @@ val m = mk_var("m", numSyntax.num)
 fun to_numeraln th = INST [n |-> mk_comb(numSyntax.numeral_tm, n),
                            m |-> mk_comb(numSyntax.numeral_tm, m)] th
 
+val ltnb12 = TAC_PROOF(([], “0 < NUMERAL (BIT1 n) /\ 0 < NUMERAL (BIT2 n)”),
+                       REWRITE_TAC[arithmeticTheory.NUMERAL_DEF,
+                                   arithmeticTheory.BIT1,
+                                   arithmeticTheory.BIT2,
+                                   arithmeticTheory.ADD_CLAUSES,
+                                   prim_recTheory.LESS_0])
+val let_id = TAC_PROOF(([], “LET (\n. n) x = x”),
+                       SIMP_TAC boolSimps.bool_ss [LET_THM])
+
 val op_rwts =
-  [to_numeraln mult_ints, to_numeraln add_ints, flr, NUM_CEILING_NUM_FLOOR,
+  [to_numeraln mult_ints, to_numeraln add_ints, flr,
    REAL_DIV_LZERO, REAL_NEGNEG] @
+  (transform [(x,posneg)] $ SPEC x NUM_CEILING_NUM_FLOOR) @
+  (transform [(x,posneg), (y,nb12)] (
+    SPEC (mk_div(x,y)) NUM_CEILING_NUM_FLOOR)
+             |> map (SIMP_RULE arith_ss [REAL_LE_LDIV_EQ, REAL_LT, REAL_LE,
+                                         REAL_MUL_LZERO, REAL_NEG_LE0,
+                                         ltnb12, flr, let_id])) @
+
    transform [(x,posneg0)] (SPEC_ALL REAL_ADD_LID) @
    transform [(x,posneg)] (SPEC_ALL REAL_ADD_RID) @
    transform [(x,posneg0)] (SPEC_ALL REAL_MUL_LZERO) @

src/real/selftest.sml

@@ -11,54 +11,64 @@ val REAL_ARITH1 = RealArith.REAL_ARITH;
 (* The new port, also suppports rational coefficients *)
 val REAL_ARITH2 = RealField.REAL_ARITH;
 
-val s = SIMP_CONV (bossLib.std_ss ++ REAL_REDUCE_ss) []
+val s = SIMP_CONV (bossLib.std_ss ++ REAL_REDUCE_ss) [LET_THM]
 
-fun test (problem, result) = let
+fun test conv nm (problem, result) = let
   val t2s = trace ("Unicode", 0) term_to_string
-  val padr = StringCvt.padRight #" "
-  val padl = StringCvt.padLeft #" "
-  val p_s = padr 30 (t2s problem)
-  val r_s = padl 10 (t2s result)
-  val _ = tprint (p_s ^ " = " ^ r_s)
-  val th = QCONV s problem
-  val answer = rhs (concl th)
 in
-  if aconv answer result then OK()
-  else die ("FAILED!\n  Got "^term_to_string answer)
+  convtest("[" ^ nm ^ "] " ^ t2s problem ^ " = " ^ t2s result,
+           conv, problem, result)
 end;
 
-val tests = [(``~~3r``, ``3r``),
-             (``3r + 4``, ``7r``),
-             (``3 - 4r``, ``~1r``),
-             (``abs (~20r)``, ``20r``),
-             (``abs (1/6)``, ``1/6``),
-             (``abs (~3/6)``, ``1/2``),
-             (``abs 0``, ``0``),
-             (``3r * 3/4``, ``9/4``),
-             (``6/~8``, ``~3/4``),
-             (``1/3 + 1/2``, ``5/6``),
-             (``1/2 = 0``, ``F``),
-             (``0 + 3r``, ``3r``),
-             (``3r * 0``, ``0r``),
-             (``~0r``, ``0r``),
-             (``1r - 0``, ``1r``),
-             (``1 / 10 + 0r``, ``1r/10``),
-             (``0r + 1 / 10``, ``1r/10``),
-             (``1/2 * 0r``, ``0r``),
-             (``0r * 1/2``, ``0r``)]
-
-val _ = List.app test tests
+val real_reduce_simp_tests = [
+  (“~~3r”        , “3r”),
+  (“3r + 4”      , “7r”),
+  (“3 - 4r”      , “~1r”),
+  (“abs (~20r)”  , “20r”),
+  (“abs (1/6)”   , “1/6”),
+  (“abs (~3/6)”  , “1/2”),
+  (“abs 0”       , “0”),
+  (“3r * 3/4”    , “9/4”),
+  (“6/~8”        , “~3/4”),
+  (“1/3 + 1/2”   , “5/6”),
+  (“1/2 = 0”     , “F”),
+  (“0 + 3r”      , “3r”),
+  (“3r * 0”      , “0r”),
+  (“~0r”         , “0r”),
+  (“1r - 0”      , “1r”),
+  (“1 / 10 + 0r” , “1r/10”),
+  (“0r + 1 / 10” , “1r/10”),
+  (“1/2 * 0r”    , “0r”),
+  (“0r * 1/2”    , “0r”),
+  (“flr 10”      , “10n”),
+  (“clg 12”      , “12n”),
+  (“flr (1/10)”  , “0n”),
+  (“clg (1/10)”  , “1n”),
+  (“flr (131/10)”, “13n”),
+  (“clg (131/10)”, “14n”),
+  (“flr (-2/4)”  , “0n”),
+  (“clg (-2/4)”  , “0n”)
+]
+
+val _ = List.app (test s "simp") real_reduce_simp_tests
+val _ = List.app (test EVAL "EVAL") real_reduce_simp_tests
+
+fun isunch UNCHANGED = true | isunch _ = false
+val _ = List.app (shouldfail {testfn = s, printresult = thm_to_string,
+                              printarg = fn t => "Testing SIMP_CONV “" ^
+                                                 term_to_string t ^
+                                                 "” raises UNCHANGED",
+                              checkexn = isunch})
+                 [“flr x”, “clg x”, “flr (10/x)”, “clg (10/x)”,
+                  “flr (-x/5)”, “clg(-x/5)”]
+
 
 val _ = List.app
           (fn (s1,s2) => tpp_expected
                            {testf=standard_tpp_message, input=s1, output=s2})
           [("realinv 2", "2⁻¹"), ("inv (TC R)", "R⁺ ᵀ")]
 val _ = tpp "¬p ∧ q"                                                   (* UOK *)
 
-fun UNCH_test (n,c,t) =
-  shouldfail {checkexn = fn Conv.UNCHANGED => true | _ => false,
-              printarg = fn t => "UNCHANGED " ^ n ^ ": " ^ term_to_string t,
-              printresult = thm_to_string, testfn = c} t
 fun nftest (r as (n,c,t1,t2)) =
     let
       fun test (t1,t2) = (Exn.capture c t1, Exn.capture c t2)