HolSmt: replay goals containing quot and rem

HOL4's integer arithmetic decision procedures cannot handle `quot` and
`rem`, so proof steps containing these symbols were failing to replay.

This commit rewrites goals containing these symbols to increase the
chances of a successful replay.

`thm_AUTO` was similarly improved, as it had the same limitation and
was failing to prove some of the self-tests.

src/HolSmt/Z3_ProofReplay.sml

@@ -495,7 +495,8 @@ local
         PURE_REWRITE_TAC[integerTheory.EDIV_DEF, integerTheory.EMOD_DEF]
         (* the next rewrites are a workaround for this issue:
            https://github.com/HOL-Theorem-Prover/HOL/issues/1207 *)
-        >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT]
+        >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT,
+             integerTheory.int_quot, integerTheory.int_rem]
         (* if `arith_tactic` doesn't work at first, don't give up immediately;
            instead let's try additional tactics *)
         >> TRY arith_tactic

src/HolSmt/selftest.sml

@@ -106,7 +106,8 @@ fun auto_tac (_, t) =
   let
     val simpset = bossLib.++ (bossLib.srw_ss (), wordsLib.WORD_ss)
     val t_eq_t' = simpLib.SIMP_CONV simpset [integerTheory.INT_ABS,
-      integerTheory.INT_MAX, integerTheory.INT_MIN]
+      integerTheory.INT_MAX, integerTheory.INT_MIN, integerTheory.int_quot,
+      integerTheory.int_rem]
       t
       handle Conv.UNCHANGED =>
         Thm.REFL t