HolSmt: add tests for real division

Real division has been supported by HolSmt for many years, but it's
always nice to have some tests for it, corresponding to similar tests
that we have for the ints and nums.

Author: someplaceguy

src/HolSmt/selftest.sml

@@ -676,7 +676,39 @@ 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]),
+    (``(~42:real) / ~42 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~1:real) / ~42 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:real) / ~42 = 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(1:real) / ~42 = ~1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(42:real) / ~42 = ~1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~42:real) / ~1 = 42``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~1:real) / ~1 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(0:real) / ~1 = 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(1:real) / ~1 = ~1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(42:real) / ~1 = ~42``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~42:real) / 1 = ~42``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~1:real) / 1 = ~1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(0:real) / 1 = 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(1:real) / 1 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(42:real) / 1 = 42``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~42:real) / 42 = ~1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(~1:real) / 42 = ~1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:real) / 42 = 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(1:real) / 42 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(42:real) / 42 = 1``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) / 1 = x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) / ~1 = ~x``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) / 42 <= x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
+    (``(x:real) / 42 <= abs x``, [thm_AUTO, thm_CVC, thm_Z3_v4, thm_Z3p_v4]),
+
+    (``((x:real) / 42 = x) = (x = 0)``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) / 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
+    (``(x:real) / 0 = 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(0:real) / 0 = 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(0:real) / 0 = 1``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
+    (``(0:real) / 0 = 1 / 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p_v4]),
+    (``(x:real) / 0 = x / 0``, [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_v4]),
     (``x < 0 ==> (x:real) / 42 > x``,