HolSmt: fix Z3 proof replay in real arith w/ rational coefficients

It turns out that the existing Z3 proof reconstruction code was using
RealArith.REAL_ARITH to replay linear arithmetic steps in proofs.

However, RealArith.REAL_ARITH only handles integral coefficients and
therefore proof steps such as `(x: real) / 1r = x` were failing.

To fix this, we simply switch to RealField.REAL_ARITH, which supports
rational coefficients.

This allows us to enable proof reconstruction for 3 more self-tests,
all related to the reals. This also means that all real-related tests
in the self-tests now work with proof reconstruction.

The RealArith->RealField change in the "rewrite" rule handler fixes
proof steps such as these: `(rewrite (= (/ v0 1.0) v0))` and allows
us to reenable the first self-test.

The identical change in the "th_lemma[arith]" rule handler fixes
proof steps such as the following:

((_ |th-lemma| arith farkas -41/42 1) @x76 @x77 false)

... corresponding to:

[.] |- ~(x <= 0r)),  [.] |- 41r / 42r * x <= 0r], F

... which allows us to reenable proof reconstruction for the other two
self-tests.

src/HolSmt/Z3_ProofReplay.sml

@@ -798,7 +798,7 @@ local
         handle Feedback.HOL_ERR _ =>
 
         if term_contains_real_ty t then
-          profile "rewrite(11.1)(REAL_ARITH)" RealArith.REAL_ARITH t
+          profile "rewrite(11.1)(REAL_ARITH)" RealField.REAL_ARITH t
         else
           profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t
     in
@@ -836,7 +836,7 @@ local
           (* this is just a heuristic - it is quite conceivable that a
              term that contains type real is provable by integer
              arithmetic *)
-          profile "th_lemma[arith](3.1)(real)" RealArith.REAL_ARITH t'
+          profile "th_lemma[arith](3.1)(real)" RealField.REAL_ARITH t'
         else
           profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t'
       val subst = List.map (fn (term, var) => {redex = var, residue = term})

src/HolSmt/selftest.sml

@@ -213,9 +213,6 @@ in
 
     (* real *)
 
-    (* Z3 2.19 prints reals as integers in its proofs; I see no way to
-       reliably distinguish between them. *)
-
     (``0r = 0r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``1r = 1r``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``0r = 1r``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -450,9 +447,9 @@ in
     (``1 * (x:real) = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``(x:real) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``x > 0 ==> (x:real) / 42 < x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``x < 0 ==> (x:real) / 42 > x``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (``abs (x:real) >= 0``, [thm_AUTO, thm_YO]),
     (``(abs (x:real) = 0) = (x = 0)``, [thm_AUTO, thm_YO]),