HolSmt: add some support for tuples

Again, this is a temporary stop-gap measure until we can translate function
definitions to SMT-LIB format, so that SMT solvers can reason about them.

As it is, due to the above limitation this won't be able to solve some goals
(witness the two disabled tests) but it does allow solving the simpler ones.

Of the tests that were enabled, all work with Z3 proof reconstruction.

src/HolSmt/SmtLib.sml

@@ -576,7 +576,8 @@ in
       (if simp_let then Library.LET_SIMP_TAC else ALL_TAC) THEN
       SIMP_TAC pureSimps.pure_ss
         [integerTheory.INT_MIN, integerTheory.INT_MAX, integerTheory.INT_ABS,
-         realaxTheory.real_min, realaxTheory.real_max, realTheory.abs] THEN
+         realaxTheory.real_min, realaxTheory.real_max, realTheory.abs,
+         pairTheory.PAIR_EQ, pairTheory.FST, pairTheory.SND] THEN
       Library.WORD_SIMP_TAC THEN
       Library.SET_SIMP_TAC THEN
       Tactic.BETA_TAC

src/HolSmt/selftest.sml

@@ -642,30 +642,31 @@ in
     (``(x, y) = (x, z)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x, y) = (z, y)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x, y) = (y, x)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``((x, y) = (y, x)) = (x = y)``, [(*thm_AUTO,*) thm_YO]),
+    (``((x, y) = (y, x)) = (x = y)``, [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``((x, y, z) = (y, z, x)) <=> (x = y) /\ (y = z)``,
-      [(*thm_AUTO,*) thm_YO]),
-    (``((x, y) = (u, v)) <=> (x = u) /\ (y = v)``, [thm_AUTO, thm_YO]),
+      [(*thm_AUTO,*) thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``((x, y) = (u, v)) <=> (x = u) /\ (y = v)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (``y = FST (x, y)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``x = FST (x, y)``, [thm_AUTO, thm_YO]),
-    (``(FST (x, y, z) = FST (u, v, w)) = (x = u)``, [thm_AUTO, thm_YO]),
+    (``x = FST (x, y)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(FST (x, y, z) = FST (u, v, w)) = (x = u)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``(FST (x, y, z) = FST (u, v, w)) <=> (x = u) /\ (y = w)``,
       [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
 
-    (``y = SND (x, y)``, [thm_AUTO, thm_YO]),
+    (``y = SND (x, y)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``x = SND (x, y)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(SND (x, y, z) = SND (u, v, w)) = (y = v)``,
        [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(SND (x, y, z) = SND (u, v, w)) = (z = w)``,
        [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(SND (x, y, z) = SND (u, v, w)) <=> (y = v) /\ (z = w)``,
-      [thm_AUTO, thm_YO]),
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``(FST (x, y) = SND (x, y)) = (x = y)``, [thm_AUTO, thm_YO]),
-    (``(FST p = SND p) = (p = (SND p, FST p))``, [(*thm_AUTO,*) thm_YO]),
+    (``(FST (x, y) = SND (x, y)) = (x = y)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(FST p = SND p) = (p = (SND p, FST p))``,
+      [(*thm_AUTO, thm_CVC,*) thm_YO(*, thm_Z3, thm_Z3p*)]),
     (``((\p. FST p) (x, y) = (\p. SND p) (x, y)) = (x = y)``,
-      [thm_AUTO, thm_YO]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO(*, thm_Z3, thm_Z3p*)]),
 
     (* words (i.e., bit vectors) *)