From ac823581b90c1f54595e6d7a8943641411ebdc61 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Mon, 11 Mar 2024 02:40:48 +0000
Subject: [PATCH 01/27] HolSmt: fix `let ... and ...` SMT-LIB translation

The SMT-LIB term translator couldn't handle parallel definitions
properly. This commit fixes that.
---
 src/HolSmt/SmtLib.sml | 24 +++++++++++++++---------
 1 file changed, 15 insertions(+), 9 deletions(-)

diff --git a/src/HolSmt/SmtLib.sml b/src/HolSmt/SmtLib.sml
index 31b03f60f4..df7fc9a516 100644
--- a/src/HolSmt/SmtLib.sml
+++ b/src/HolSmt/SmtLib.sml
@@ -421,18 +421,24 @@ local
     end
     handle Feedback.HOL_ERR _ =>
 
-    (* let binder - somewhat similar to quantifiers, but we only
-       translate one let at a time (so we don't have to worry about
-       semantic differences caused by parallel vs. sequential let) *)
+    (* let binder - somewhat similar to quantifiers *)
     let
-      val (M, N) = boolSyntax.dest_let tm
-      val (var, body) = Term.dest_abs M
-      val (acc, (Ndecls, N)) = translate_term (acc, (bounds, N))
-      val (bounds, name) = create_bound_name (bounds, var)
+      val (bindings, body) = pairSyntax.dest_anylet tm
+      val (vars, bodies) = ListPair.unzip bindings
+      (* we should translate the bodies without first creating the bound names *)
+      val bounds_bodies = List.map (fn body => (bounds, body)) bodies
+      val (acc, decls_bodies) = Lib.foldl_map translate_term (acc, bounds_bodies)
+      (* now we can create the bound names *)
+      val (bounds, smtvars) = Lib.foldl_map create_bound_name (bounds, vars)
+      val decls_bodies_smtvars = ListPair.zipEq (decls_bodies, smtvars)
+      val (decls, smtbinds) = List.foldl (fn (((d, b), v), (decls, smtbinds)) =>
+        (d @ decls, "(" ^ v ^ " " ^ b ^ ")" :: smtbinds)) ([], [])
+          decls_bodies_smtvars
+      val bindings_str = String.concatWith " " (List.rev smtbinds)
       val (acc, (bodydecls, body)) = translate_term (acc, (bounds, body))
     in
-      (acc, (Ndecls @ bodydecls,
-        "(let ((" ^ name ^ " " ^ N ^ ")) " ^ body ^ ")"))
+      (acc, (decls @ bodydecls,
+        "(let (" ^ bindings_str ^ ") " ^ body ^ ")"))
     end
     handle Feedback.HOL_ERR _ =>
 

From 1c03152867cbbf2a33b378627c92a2e8128cd933 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Sun, 10 Mar 2024 01:07:10 +0000
Subject: [PATCH 02/27] HolSmt: add support for div and mod

---
 src/HolSmt/HolSmtScript.sml    | 68 +++++++++++++++++++++++++++++-----
 src/HolSmt/SmtLib.sml          | 11 ++++--
 src/HolSmt/SmtLib_Theories.sml | 10 ++++-
 src/HolSmt/selftest.sml        | 12 +++++-
 4 files changed, 85 insertions(+), 16 deletions(-)

diff --git a/src/HolSmt/HolSmtScript.sml b/src/HolSmt/HolSmtScript.sml
index ad5dc815f5..adc443eb0c 100644
--- a/src/HolSmt/HolSmtScript.sml
+++ b/src/HolSmt/HolSmtScript.sml
@@ -2,6 +2,8 @@
 
 (* Various theorems for HolSmtLib *)
 
+  val op >> = Tactical.>>
+
   val T = tautLib.TAUT_PROVE
   val P = bossLib.PROVE []
   val S = simpLib.SIMP_PROVE (simpLib.++ (simpLib.++ (simpLib.++
@@ -12,6 +14,9 @@
   val W = wordsLib.WORD_DECIDE
   val B = blastLib.BBLAST_PROVE
 
+  val I = simpLib.SIMP_PROVE (simpLib.++ (simpLib.++
+    (bossLib.arith_ss, intSimps.INT_RWTS_ss), intSimps.INT_ARITH_ss))
+
   (* simplify 't' using 'thms', then prove the simplified term using
      'TAUT_PROVE' *)
   fun U thms t =
@@ -29,6 +34,52 @@
   val _ = Theory.new_theory "HolSmt"
   val _ = ParseExtras.temp_loose_equality()
 
+  (* constants used in SMT-LIB *)
+
+  val smtdiv_def = bossLib.Define
+    `smtdiv (i: int) (j: int) = if 0 < j then i / j else -(i / -j)`
+
+  val smtmod_def = bossLib.Define
+    `smtmod (i: int) (j: int) = i % ABS j`
+
+  (* Note that according to SMT-LIB's `Ints` theory, `div` and `mod` must match
+     Boute's Euclidean definition, that is, they must satisfy the formula:
+
+     !m n. n <> 0 ==>
+       let q = smtdiv m n
+       and r = smtmod m n
+       in
+         (m = n * q + r /\ 0 <= r /\ r <= (ABS n) - 1)
+
+     We prove this as a test case in `selftest.sml` *)
+
+  (* theorems used for arithmetic operators *)
+
+  val _ = s ("SMT_NUM_MUL", I [] ``!m n. m * n = Num (&m * &n)``)
+  val _ = s ("SMT_NUM_DIV", I [smtdiv_def]
+    ``!k n. n <> 0 ==> (k DIV n = Num (smtdiv (&k) (&n)))``)
+  val _ = s ("SMT_NUM_MOD", I [smtmod_def]
+    ``!k n. n <> 0 ==> (k MOD n = Num (smtmod (&k) (&n)))``)
+  val _ = s ("SMT_INT_DIV", I [smtdiv_def]
+    ``!i j. j <> 0 ==> (i / j =
+        if 0 < j then smtdiv i j else -(smtdiv (-i) j))``)
+  val _ = s ("SMT_INT_MOD", I [smtmod_def, integerTheory.INT_ABS]
+    ``!i j. j <> 0 ==> (i % j =
+        if 0 < j then smtmod i j else -(smtmod (-i) j))``)
+  val _ = s ("SMT_INT_QUOT", Tactical.prove (
+    ``!i j. j <> 0 ==> (i quot j =
+        if 0 <= i then smtdiv i j else smtdiv (-i) (-j))``,
+          bossLib.rw [smtdiv_def, integerTheory.int_div, integerTheory.int_quot]
+          >> bossLib.Cases_on `i = 0` >> bossLib.fs [] >> intLib.ARITH_TAC))
+  val _ = s ("SMT_INT_REM", Tactical.prove (
+    ``!i j. j <> 0 ==> (i rem j =
+        if 0 <= i then smtmod i j else -(smtmod (-i) j))``,
+          let
+            open integerTheory
+          in
+            bossLib.rw [smtmod_def, int_mod, int_rem, int_div, int_quot, INT_ABS]
+            >> intLib.ARITH_TAC
+          end))
 
   (* constants used by Z3 *)
 
@@ -478,10 +529,10 @@
     ``(x = y) \/ ((x =+ z) f y = f y)``)
   val _ = s ("t005", Tactical.prove
     (``(f = g) \/ (f (array_ext f g) <> g (array_ext f g))``,
-    Tactical.THEN (Tactic.DISJ_CASES_TAC
-        (Thm.SPEC ``?x. f x <> g x`` boolTheory.EXCLUDED_MIDDLE),
-      Tactical.THEN (Rewrite.REWRITE_TAC [array_ext_def],
-        bossLib.METIS_TAC []))))
+      Tactic.DISJ_CASES_TAC
+        (Thm.SPEC ``?x. f x <> g x`` boolTheory.EXCLUDED_MIDDLE)
+      >> Rewrite.REWRITE_TAC [array_ext_def]
+      >> bossLib.METIS_TAC []))
 
   val _ = s ("t006", A ``((x :int) <> y) \/ (x <= y)``)
   val _ = s ("t007", A ``((x :int) <> y) \/ (x >= y)``)
@@ -500,11 +551,10 @@
     let
       val RW = bossLib.RW_TAC (bossLib.++ (bossLib.bool_ss, fcpLib.FCP_ss))
     in
-      Tactical.THEN (RW [],
-        Tactical.THEN (Tactic.EXISTS_TAC ``0 :num``,
-          Tactical.THEN (RW [wordsTheory.DIMINDEX_GT_0,
-              wordsTheory.word_1comp_def],
-            tautLib.TAUT_TAC)))
+      RW []
+      >> Tactic.EXISTS_TAC ``0 :num``
+      >> RW [wordsTheory.DIMINDEX_GT_0, wordsTheory.word_1comp_def]
+      >> tautLib.TAUT_TAC
     end))
   val _ = s ("t018", W ``(x = y) ==> x ' i ==> y ' i``)
   val _ = s ("t019", S ``(1w = ~(x :word1)) \/ x ' 0``)
diff --git a/src/HolSmt/SmtLib.sml b/src/HolSmt/SmtLib.sml
index df7fc9a516..cc3b89238a 100644
--- a/src/HolSmt/SmtLib.sml
+++ b/src/HolSmt/SmtLib.sml
@@ -90,8 +90,8 @@ local
     (intSyntax.minus_tm, apfst_K "-"),
     (intSyntax.plus_tm, apfst_K "+"),
     (intSyntax.mult_tm, apfst_K "*"),
-    (* (..., "div"), *)
-    (* (..., "mod"), *)
+    (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, apfst_K "div"),
+    (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, apfst_K "mod"),
     (intSyntax.absval_tm, apfst_K "abs"),
     (intSyntax.leq_tm, apfst_K "<="),
     (intSyntax.less_tm, apfst_K "<"),
@@ -628,14 +628,17 @@ in
        are being used. For now we just manually add a few useful ones. *)
     val facts =
     let
-      open arithmeticTheory integerTheory
+      open arithmeticTheory integerTheory HolSmtTheory
     in
       if !include_theorems then [
         (* arithmeticTheory *)
         GREATER_DEF, GREATER_EQ, MIN_DEF, MAX_DEF,
         (* integerTheory *)
-        INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN, INT_MUL,
+        INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN,
         INT_OF_NUM, INT_POS,
+        (* HolSmtTheory *)
+        SMT_NUM_MUL, SMT_NUM_DIV, SMT_NUM_MOD, SMT_INT_DIV, SMT_INT_MOD,
+        SMT_INT_QUOT, SMT_INT_REM,
         (* others *)
         int_arithTheory.INT_NUM_SUB,
         realaxTheory.real_min, realaxTheory.real_max, realTheory.abs
diff --git a/src/HolSmt/SmtLib_Theories.sml b/src/HolSmt/SmtLib_Theories.sml
index 81b7419dcb..37a667b543 100644
--- a/src/HolSmt/SmtLib_Theories.sml
+++ b/src/HolSmt/SmtLib_Theories.sml
@@ -270,7 +270,10 @@ in
       ("-", leftassoc intSyntax.mk_minus),
       ("+", leftassoc intSyntax.mk_plus),
       ("*", leftassoc intSyntax.mk_mult),
-      (* FIXME: add parsing of div and mod *)
+      ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+      ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),
@@ -332,7 +335,10 @@ in
       ("-", leftassoc intSyntax.mk_minus),
       ("+", leftassoc intSyntax.mk_plus),
       ("*", leftassoc intSyntax.mk_mult),
-      (* FIXME: add parsing of div and mod *)
+      ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+      ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 2b24734380..f65c8bacd5 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -1095,7 +1095,17 @@ in
     (``x IN P INTER UNIV <=> x IN P``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``x IN P INTER Q <=> x IN Q INTER P``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``x IN P INTER (Q INTER R) <=> x IN (P INTER Q) INTER R``,
-      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p])
+      [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+
+    (* prove that HolSmt$smtdiv and HolSmt$smtmod match Boute's Euclidean
+       definition, i.e. that they match SMT-LIB's `Ints` theory's definition of
+       integer div and mod *)
+    (``!m n. n <> 0 ==>
+         let q = HolSmt$smtdiv m n
+         and r = HolSmt$smtmod m n
+         in
+           (m = n * q + r /\ 0 <= r /\ r <= (ABS n) - 1)``,
+      [(*thm_AUTO, thm_CVC,*) thm_Z3_v4(*, thm_Z3p*)])
 
   ]  (* tests *)
 end

From 414750367e8b7facc75f3331cac72f40777835d3 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 03:04:16 +0000
Subject: [PATCH 03/27] HolSmt: fix hang in arith Z3 proof replay

The previous workaround for ARITH_PROVE failing to prove some terms
changed the `th_lemma_arith` proof handler to use COOPER_PROVE
instead.

However, COOPER_PROVE sometimes is too slow and appears to hang when
replaying some Z3 proofs.

This commit changes the `th_lemma_arith` handler to first try
ARITH_PROVE which is much faster, and only if it fails, then try
COOPER_PROVE.
---
 src/HolSmt/Z3_ProofReplay.sml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 777c483411..c091ae6885 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -1077,10 +1077,13 @@ local
              term that contains type real is provable by integer
              arithmetic *)
           profile "th_lemma[arith](3.1)(real)" RealField.REAL_ARITH t'
-        else
-          (* the following should be reverted to use ARITH_PROVE instead of
-             COOPER_PROVE when issue HOL-Theorem-Prover/HOL#1203 is fixed *)
-          profile "th_lemma[arith](3.2)(int)" intLib.COOPER_PROVE t'
+        else (
+          profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t'
+          (* the following should be removed when issue
+             HOL-Theorem-Prover/HOL#1203 is fixed *)
+          handle Feedback.HOL_ERR _ =>
+            profile "th_lemma[arith](3.3)(cooper)" intLib.COOPER_PROVE t'
+        )
       val subst = List.map (fn (term, var) => {redex = var, residue = term})
         (Redblackmap.listItems dict)
     in

From 7fb89ebdf8c330e24b2c6a1e817cc9e33c24fd08 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 03:16:29 +0000
Subject: [PATCH 04/27] HolSmt: add some arithmetic theorems

SMT_NUM_ADD and SMT_NUM_SUB were meant to be used in place of INT_ADD
and INT_NUM_SUB for optimization reasons.

However, this causes a regression in proof replay in one of the
self-tests. Since this regression is not straightforward to fix,
these theorems are not being used yet.

NUM_OF_INT was also added to the default set of theorems since it
helps solve some `num`-related goals.
---
 src/HolSmt/HolSmtScript.sml | 3 +++
 src/HolSmt/SmtLib.sml       | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/HolSmt/HolSmtScript.sml b/src/HolSmt/HolSmtScript.sml
index adc443eb0c..88a05e997e 100644
--- a/src/HolSmt/HolSmtScript.sml
+++ b/src/HolSmt/HolSmtScript.sml
@@ -55,6 +55,9 @@
 
   (* theorems used for arithmetic operators *)
 
+  val _ = s ("SMT_NUM_ADD", A ``!m n. m + n = Num (&m + &n)``)
+  val _ = s ("SMT_NUM_SUB", A
+    ``!m n. m - n = if (&m:int) <= &n then 0n else Num (&m - &n)``)
   val _ = s ("SMT_NUM_MUL", I [] ``!m n. m * n = Num (&m * &n)``)
   val _ = s ("SMT_NUM_DIV", I [smtdiv_def]
     ``!k n. n <> 0 ==> (k DIV n = Num (smtdiv (&k) (&n)))``)
diff --git a/src/HolSmt/SmtLib.sml b/src/HolSmt/SmtLib.sml
index cc3b89238a..ded9ae6baa 100644
--- a/src/HolSmt/SmtLib.sml
+++ b/src/HolSmt/SmtLib.sml
@@ -634,8 +634,8 @@ in
         (* arithmeticTheory *)
         GREATER_DEF, GREATER_EQ, MIN_DEF, MAX_DEF,
         (* integerTheory *)
-        INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN,
-        INT_OF_NUM, INT_POS,
+        INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN, INT_OF_NUM,
+        INT_POS, NUM_OF_INT,
         (* HolSmtTheory *)
         SMT_NUM_MUL, SMT_NUM_DIV, SMT_NUM_MOD, SMT_INT_DIV, SMT_INT_MOD,
         SMT_INT_QUOT, SMT_INT_REM,

From b6330a8aa9229c0e1ffc6c8b9a29ab117209e0af Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 03:38:41 +0000
Subject: [PATCH 05/27] HolSmt: enable DIV tests

---
 src/HolSmt/selftest.sml | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index f65c8bacd5..15ca6f3544 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -274,15 +274,18 @@ in
     (``(x:num) * 42 = 42 * x``,
       [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
 
-    (``(0:num) DIV 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:num) DIV 1 = 1``, [thm_AUTO, thm_YO]),
-    (``(42:num) DIV 1 = 42``, [thm_AUTO, thm_YO]),
-    (``(0:num) DIV 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:num) DIV 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(42:num) DIV 42 = 1``, [thm_AUTO, thm_YO]),
-    (``(x:num) DIV 1 = x``, [thm_AUTO, thm_YO]),
-    (``(x:num) DIV 42 <= x``, [thm_AUTO, thm_YO]),
-    (``((x:num) DIV 42 = x) = (x = 0)``, [thm_AUTO, thm_YO]),
+    (``(0:num) DIV 1 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(1:num) DIV 1 = 1``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(42:num) DIV 1 = 42``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(0:num) DIV 42 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(1:num) DIV 42 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(42:num) DIV 42 = 1``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:num) DIV 1 = x``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:num) DIV 42 <= x``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``((x:num) DIV 42 = x) = (x = 0)``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``(x:num) DIV 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:num) DIV 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:num) DIV 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),

From 0d8246dd16cb827a991d5e6bc6f9d53ecab333af Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 03:58:22 +0000
Subject: [PATCH 06/27] HolSmt: parse `div0` and `mod0` in Z3 proofs

Unfortunately, these operators don't seem to be documented.

However, from a quick reading of the Z3 source code, it seems that
they seem to be similar to `div` and `mod`, but they seem to be used
to indicate that Z3 can't prove that the divisor is non-zero.
---
 src/HolSmt/SmtLib_Theories.sml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/HolSmt/SmtLib_Theories.sml b/src/HolSmt/SmtLib_Theories.sml
index 37a667b543..21ef226284 100644
--- a/src/HolSmt/SmtLib_Theories.sml
+++ b/src/HolSmt/SmtLib_Theories.sml
@@ -337,8 +337,12 @@ in
       ("*", leftassoc intSyntax.mk_mult),
       ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
         (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+      ("div0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
       ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
         (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
+      ("mod0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),

From 5fe3bad4db43047a3f12420ebb985c71cc0afe94 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 05:57:33 +0000
Subject: [PATCH 07/27] HolSmt: major fixes for Z3 replay of `th_lemma_arith`
 rule

The `th_lemma_arith` was running into several issues. The following
changes were made:

1. The `generalize_ite` procedure was removed, since the arithmetic
decision procedures can handle `if ... then ... else ...` now. It was
causing replay failures because some terms were not provable unless
the decision procedures could inspect the `if` bodies.

2. The arithmetic decision procedures don't understand `smtdiv` and
`smtmod`; so before proving the term, we now rewrite it with the
definitions of these functions.

3. A workaround was also implemented for some instances of the
following issue:

https://github.com/HOL-Theorem-Prover/HOL/issues/1207

Namely, the integer decision procedures cannot decide some terms
containing `ABS` and `Num`, so we rewrite them when possible.
---
 src/HolSmt/Z3_ProofReplay.sml | 61 +++++++++++------------------------
 1 file changed, 19 insertions(+), 42 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index c091ae6885..2e8cea30be 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -13,9 +13,13 @@ local
 
   open Z3_Proof
 
+  val op >> = Tactical.>>
+
   val ERR = Feedback.mk_HOL_ERR "Z3_ProofReplay"
   val WARNING = Feedback.HOL_WARNING "Z3_ProofReplay"
 
+  val smtdiv_def = HolSmtTheory.smtdiv_def
+  val smtmod_def = HolSmtTheory.smtmod_def
   val ALL_DISTINCT_NIL = HolSmtTheory.ALL_DISTINCT_NIL
   val ALL_DISTINCT_CONS = HolSmtTheory.ALL_DISTINCT_CONS
   val NOT_MEM_NIL = HolSmtTheory.NOT_MEM_NIL
@@ -451,39 +455,6 @@ local
     Thm.TRANS (Thm.TRANS l_eq_l' l'_eq_r') (Thm.SYM r_eq_r')
   end
 
-  (* replaces distinct if-then-else terms by distinct variables;
-     returns the generalized term and a map from ite-subterms to
-     variables (treating anything but combinations as atomic, i.e.,
-     this function does NOT descend into lambda-abstractions) *)
-  fun generalize_ite t =
-  let
-    fun aux (dict, t) =
-      if boolSyntax.is_cond t then (
-        case Redblackmap.peek (dict, t) of
-          SOME var =>
-          (dict, var)
-        | NONE =>
-          let
-            val var = Term.genvar (Term.type_of t)
-          in
-            (Redblackmap.insert (dict, t, var), var)
-          end
-      ) else (
-        let
-          val (l, r) = Term.dest_comb t
-          val (dict, l) = aux (dict, l)
-          val (dict, r) = aux (dict, r)
-        in
-          (dict, Term.mk_comb (l, r))
-        end
-        handle Feedback.HOL_ERR _ =>
-          (* 't' is not a combination *)
-          (dict, t)
-      )
-  in
-    aux (Redblackmap.mkDict Term.compare, t)
-  end
-
   (* Returns a proof of `t` given a list of theorems as inputs. It relies on
      `metisLib.METIS_TAC` to find a proof. The returned theorem will have as
      hypotheses all the hypotheses of all the input theorems. *)
@@ -1071,24 +1042,30 @@ local
 
   val z3_th_lemma_arith = th_lemma_wrapper "arith" (fn (state, t) =>
     let
-      val (dict, t') = generalize_ite t
-      val thm = if term_contains_real_ty t' then
+      fun tactic (goal as (_, term)) =
+        if term_contains_real_ty term then
           (* 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)" RealField.REAL_ARITH t'
+          profile "th_lemma[arith](3.1)(real)" RealField.REAL_ARITH_TAC goal
         else (
-          profile "th_lemma[arith](3.2)(int)" intLib.ARITH_PROVE t'
+          profile "th_lemma[arith](3.2)(int)" intLib.ARITH_TAC goal
           (* the following should be removed when issue
              HOL-Theorem-Prover/HOL#1203 is fixed *)
           handle Feedback.HOL_ERR _ =>
-            profile "th_lemma[arith](3.3)(cooper)" intLib.COOPER_PROVE t'
+            profile "th_lemma[arith](3.3)(cooper)" intLib.COOPER_TAC goal
         )
-      val subst = List.map (fn (term, var) => {redex = var, residue = term})
-        (Redblackmap.listItems dict)
+      val thm = Tactical.prove (t,
+        (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic
+           decision procedures can solve terms containing these functions *)
+        PURE_REWRITE_TAC[HolSmtTheory.smtdiv_def, HolSmtTheory.smtmod_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]
+        >> tactic)
     in
-      (* cache 'thm', instantiate to undo 'generalize_ite' *)
-      (state_cache_thm state thm, Thm.INST subst thm)
+      (* cache 'thm' *)
+      (state_cache_thm state thm, thm)
     end)
 
   val z3_th_lemma_array = th_lemma_wrapper "array" (fn (state, t) =>

From 62e89d7a8cdaf5549ce807e5d85452351a74f3d2 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 06:53:15 +0000
Subject: [PATCH 08/27] HolSmt: implement `iff-false` Z3 proof rule

---
 src/HolSmt/Z3_Proof.sml       | 1 +
 src/HolSmt/Z3_ProofParser.sml | 2 ++
 src/HolSmt/Z3_ProofReplay.sml | 8 ++++++++
 3 files changed, 11 insertions(+)

diff --git a/src/HolSmt/Z3_Proof.sml b/src/HolSmt/Z3_Proof.sml
index c1e36900f5..22f3908e99 100644
--- a/src/HolSmt/Z3_Proof.sml
+++ b/src/HolSmt/Z3_Proof.sml
@@ -37,6 +37,7 @@ struct
                      | DEF_AXIOM of Term.term
                      | ELIM_UNUSED of Term.term
                      | HYPOTHESIS of Term.term
+                     | IFF_FALSE of proofterm * Term.term
                      | IFF_TRUE of proofterm * Term.term
                      | INTRO_DEF of Term.term
                      | LEMMA of proofterm * Term.term
diff --git a/src/HolSmt/Z3_ProofParser.sml b/src/HolSmt/Z3_ProofParser.sml
index 591efde7e6..aabdace41c 100644
--- a/src/HolSmt/Z3_ProofParser.sml
+++ b/src/HolSmt/Z3_ProofParser.sml
@@ -122,6 +122,7 @@ local
     (* the following is used in `(_ th-lemma arith ...)` inference rules *)
     ("farkas",          builtin_name "farkas"),
     ("hypothesis",      zero_prems "hypothesis"),
+    ("iff-false",       one_prem "iff-false"),
     ("iff-true",        one_prem "iff-true"),
     ("intro-def",       zero_prems "intro-def"),
     ("lemma",           one_prem "lemma"),
@@ -342,6 +343,7 @@ local
       ("def-axiom",       zero_prems_pt DEF_AXIOM),
       ("elim-unused",     zero_prems_pt ELIM_UNUSED),
       ("hypothesis",      zero_prems_pt HYPOTHESIS),
+      ("iff-false",       one_prem_pt IFF_FALSE),
       ("iff-true",        one_prem_pt IFF_TRUE),
       ("intro-def",       zero_prems_pt INTRO_DEF),
       ("lemma",           one_prem_pt LEMMA),
diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 2e8cea30be..266ccbb398 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -610,6 +610,12 @@ local
   fun z3_hypothesis (state, t) =
     (state, Thm.ASSUME t)
 
+  (*   ... |- ~p
+     ------------
+     ... |- p = F *)
+  fun z3_iff_false (state, thm, _) =
+    (state, Drule.EQF_INTRO thm)
+
   (*   ... |- p
      ------------
      ... |- p = T *)
@@ -1274,6 +1280,8 @@ local
         zero_prems state_proof "elim_unused" z3_elim_unused x continuation
     | thm_of_proofterm (state_proof, HYPOTHESIS x) continuation =
         zero_prems state_proof "hypothesis" z3_hypothesis x continuation
+    | thm_of_proofterm (state_proof, IFF_FALSE x) continuation =
+        one_prem state_proof "iff_false" z3_iff_false x continuation
     | thm_of_proofterm (state_proof, IFF_TRUE x) continuation =
         one_prem state_proof "iff_true" z3_iff_true x continuation
     | thm_of_proofterm (state_proof, INTRO_DEF x) continuation =

From 064d49747f326dc6ba9569ae5e1491c7ee0f9720 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 09:13:39 +0000
Subject: [PATCH 09/27] HolSmt: enable the remaining div and mod tests

---
 src/HolSmt/selftest.sml | 190 +++++++++++++++++++++++++---------------
 1 file changed, 120 insertions(+), 70 deletions(-)

diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 15ca6f3544..b62b65f4e6 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -292,15 +292,17 @@ in
     (``(0:num) DIV 0 = 1``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:num) DIV 0 = x DIV 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``(0:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(42:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(0:num) MOD 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:num) MOD 42 = 1``, [thm_AUTO, thm_YO]),
-    (``(42:num) MOD 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(x:num) MOD 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(x:num) MOD 42 < 42``, [thm_AUTO, thm_YO]),
-    (``((x:num) MOD 42 = x) = (x < 42)``, [thm_AUTO, thm_YO]),
+    (``(0:num) MOD 1 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(1:num) MOD 1 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(42:num) MOD 1 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(0:num) MOD 42 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(1:num) MOD 42 = 1``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(42:num) MOD 42 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
+    (``(x:num) MOD 1 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:num) MOD 42 < 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``((x:num) MOD 42 = x) = (x < 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``(x:num) MOD 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:num) MOD 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:num) MOD 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -308,9 +310,10 @@ in
     (``(x:num) MOD 0 = x MOD 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (* cf. arithmeticTheory.DIVISION *)
-    (``((x:num) = x DIV 1 * 1 + x MOD 1) /\ x MOD 1 < 1``, [thm_AUTO, thm_YO]),
+    (``((x:num) = x DIV 1 * 1 + x MOD 1) /\ x MOD 1 < 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``((x:num) = x DIV 42 * 42 + x MOD 42) /\ x MOD 42 < 42``,
-      [thm_AUTO, thm_YO]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
 
     (``MIN (x:num) y <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``MIN (x:num) y <= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
@@ -354,32 +357,52 @@ in
     (``~1 * (x:int) = ~x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``(x:int) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (``(~42:int) / ~42 = 1``, [thm_AUTO, thm_YO]),
-    (``(~1:int) / ~42 = 0``, [thm_AUTO, thm_YO]),
-    (``(0:int) / ~42 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) / ~42 = ~1``, [thm_AUTO, thm_YO]),
-    (``(42:int) / ~42 = ~1``, [thm_AUTO, thm_YO]),
-    (``(~42:int) / ~1 = 42``, [thm_AUTO, thm_YO]),
-    (``(~1:int) / ~1 = 1``, [thm_AUTO, thm_YO]),
-    (``(0:int) / ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) / ~1 = ~1``, [thm_AUTO, thm_YO]),
-    (``(42:int) / ~1 = ~42``, [thm_AUTO, thm_YO]),
-    (``(~42:int) / 1 = ~42``, [thm_AUTO, thm_YO]),
-    (``(~1:int) / 1 = ~1``, [thm_AUTO, thm_YO]),
-    (``(0:int) / 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) / 1 = 1``, [thm_AUTO, thm_YO]),
-    (``(42:int) / 1 = 42``, [thm_AUTO, thm_YO]),
-    (``(~42:int) / 42 = ~1``, [thm_AUTO, thm_YO]),
-    (``(~1:int) / 42 = ~1``, [thm_AUTO, thm_YO]),
-    (``(0:int) / 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) / 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(42:int) / 42 = 1``, [thm_AUTO, thm_YO]),
-    (``(x:int) / 1 = x``, [thm_AUTO, thm_YO]),
-    (``(x:int) / ~1 = ~x``, [thm_AUTO, thm_YO]),
+    (``(~42:int) / ~42 = 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) / ~42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) / ~42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) / ~42 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) / ~42 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~42:int) / ~1 = 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) / ~1 = 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) / ~1 = 0``, [thm_AUTO, (*thm_CVC*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) / ~1 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) / ~1 = ~42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~42:int) / 1 = ~42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) / 1 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) / 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) / 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) / 1 = 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~42:int) / 42 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) / 42 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) / 42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) / 42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) / 42 = 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) / 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) / ~1 = ~x``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``(x:int) / 42 <= x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:int) / 42 <= ABS x``, [thm_AUTO, thm_YO(*, thm_Z3, thm_Z3p*)]),
+    (``(x:int) / 42 <= ABS x``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3_v4(*, thm_Z3p*)]),
     (``((x:int) / 42 = x) = (x = 0)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``(x:int) / 42 = x <=> x = 0 \/ x = ~1``, [thm_AUTO, thm_YO]),
+    (``(x:int) / 42 = x <=> x = 0 \/ x = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``(x:int) / 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:int) / 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:int) / 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -389,41 +412,64 @@ in
 
     (* cf. integerTheory.int_div *)
     (``(x:int) < 0 ==> (x / 1 = ~(~x / 1) + if ~x % 1 = 0 then 0 else ~1)``,
-      [thm_AUTO, thm_YO]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``(x:int) < 0 ==> (x / 42 = ~(~x / 42) + if ~x % 42 = 0 then 0 else ~1)``,
-      [thm_AUTO, thm_YO]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``0 <= (x:int) ==> (x / ~42 = ~(x / 42) + if x % 42 = 0 then 0 else ~1)``,
-      [thm_AUTO, thm_YO]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``0 <= (x:int) ==> (x / ~1 = ~(x / 1) + if x % 1 = 0 then 0 else ~1)``,
-      [thm_AUTO, thm_YO]),
-    (``(x:int) < 0 ==> (x / ~42 = ~x / 42)``, [thm_AUTO, thm_YO]),
-    (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``, [thm_AUTO, thm_YO]),
-
-    (``(~42:int) % ~42 = 0``, [thm_AUTO, thm_YO]),
-    (``(~1:int) % ~42 = ~1``, [thm_AUTO, thm_YO]),
-    (``(0:int) % ~42 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) % ~42 = ~41``, [thm_AUTO, thm_YO]),
-    (``(42:int) % ~42 = 0``, [thm_AUTO, thm_YO]),
-    (``(~42:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(~1:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(0:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(42:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(~42:int) % 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(~1:int) % 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(0:int) % 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) % 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(42:int) % 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(~42:int) % 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(~1:int) % 42 = 41``, [thm_AUTO, thm_YO]),
-    (``(0:int) % 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(1:int) % 42 = 1``, [thm_AUTO, thm_YO]),
-    (``(42:int) % 42 = 0``, [thm_AUTO, thm_YO]),
-    (``(x:int) % 1 = 0``, [thm_AUTO, thm_YO]),
-    (``(x:int) % ~1 = 0``, [thm_AUTO, thm_YO]),
-    (``(x:int) % 42 < 42``, [thm_AUTO, thm_YO]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) < 0 ==> (x / ~42 = ~x / 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+
+    (``(~42:int) % ~42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) % ~42 = ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) % ~42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) % ~42 = ~41``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) % ~42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~42:int) % ~1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) % ~1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) % ~1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) % ~1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) % ~1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~42:int) % 1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) % 1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) % 1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~42:int) % 42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(~1:int) % 42 = 41``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(0:int) % 42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(1:int) % 42 = 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(42:int) % 42 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) % ~1 = 0``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) % 42 < 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``((x:int) % 42 = x) = (x < 42)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
-    (``((x:int) % 42 = x) <=> (0 <= x) /\ (x < 42)``, [thm_AUTO, thm_YO]),
+    (``((x:int) % 42 = x) <=> (0 <= x) /\ (x < 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
     (``(x:int) % 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:int) % 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:int) % 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -431,10 +477,14 @@ in
     (``(x:int) % 0 = x % 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (* cf. integerTheory.int_mod *)
-    (``(x:int) % ~42 = x - x / ~42 * ~42``, [thm_AUTO, thm_YO]),
-    (``(x:int) % ~1 = x - x / ~1 * ~1``, [thm_AUTO, thm_YO]),
-    (``(x:int) % 1 = x - x / 1 * 1``, [thm_AUTO, thm_YO]),
-    (``(x:int) % 42 = x - x / 42 * 42``, [thm_AUTO, thm_YO]),
+    (``(x:int) % ~42 = x - x / ~42 * ~42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) % ~1 = x - x / ~1 * ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) % 1 = x - x / 1 * 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+    (``(x:int) % 42 = x - x / 42 * 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
 
     (``ABS (x:int) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),

From 85cde15465dd1a8cca03a95ca20d48a5b2306a86 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 09:25:57 +0000
Subject: [PATCH 10/27] HolSmt: work around NotFound exn in ARITH_PROVE

This commit contains a workaround for the following issue:

https://github.com/HOL-Theorem-Prover/HOL/issues/1209
---
 src/HolSmt/Z3_ProofReplay.sml | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 266ccbb398..8970cdf69e 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -957,8 +957,13 @@ local
 
         if profile "rewrite(11.0)(contains_real)" term_contains_real_ty t then
           profile "rewrite(11.1)(REAL_ARITH)" RealField.REAL_ARITH t
-        else
+        else (
           profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t
+            (* the following is a workaround for:
+               https://github.com/HOL-Theorem-Prover/HOL/issues/1209 *)
+            handle NotFound =>
+              raise ERR "z3_rewrite" "ARITH_PROVE raised NotFound"
+        )
     in
       (state_cache_thm state thm, thm)
     end
@@ -1048,6 +1053,8 @@ local
 
   val z3_th_lemma_arith = th_lemma_wrapper "arith" (fn (state, t) =>
     let
+      fun cooper goal =
+        profile "th_lemma[arith](3.3)(cooper)" intLib.COOPER_TAC goal
       fun tactic (goal as (_, term)) =
         if term_contains_real_ty term then
           (* this is just a heuristic - it is quite conceivable that a
@@ -1056,10 +1063,12 @@ local
           profile "th_lemma[arith](3.1)(real)" RealField.REAL_ARITH_TAC goal
         else (
           profile "th_lemma[arith](3.2)(int)" intLib.ARITH_TAC goal
-          (* the following should be removed when issue
-             HOL-Theorem-Prover/HOL#1203 is fixed *)
-          handle Feedback.HOL_ERR _ =>
-            profile "th_lemma[arith](3.3)(cooper)" intLib.COOPER_TAC goal
+          (* the following two exception handlers are workarounds for these two
+             issues:
+             https://github.com/HOL-Theorem-Prover/HOL/issues/1203
+             https://github.com/HOL-Theorem-Prover/HOL/issues/1209 *)
+          handle NotFound => cooper goal
+          handle Feedback.HOL_ERR _ => cooper goal
         )
       val thm = Tactical.prove (t,
         (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic

From 6133bcf3d49c75bff7513f70ce71ab7d962ab3f4 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 09:43:12 +0000
Subject: [PATCH 11/27] HolSmt: work around Z3 bug in `hypothesis` proof rule

In some proof certificates, Z3 emits a `hypothesis` inference rule
without discharging it later with a `lemma` rule. This causes some
proofs to fail at the end of the proof replay procedure, because
they end up containing an extra hypothesis.

Fortunately, so far all such undischarged hypothesis rules were of the
form `p = p`, so for now we can easily work around this issue by
creating such theorems without adding an assumption.

This workaround allows us to enable proof replay for 5 more
self-tests.
---
 src/HolSmt/Z3_ProofReplay.sml | 16 +++++++++++++++-
 src/HolSmt/selftest.sml       | 10 +++++-----
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 8970cdf69e..5a38c75825 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -608,7 +608,21 @@ local
   (* introduces a local hypothesis (which must be discharged by
      'z3_lemma' at some later point in the proof) *)
   fun z3_hypothesis (state, t) =
-    (state, Thm.ASSUME t)
+    (* FIXME: The following is a workaround for a yet-to-be-filed Z3 issue where
+       a hypothesis is introduced but is not discharged by `z3_lemma` at any
+       point in the proof. So far, all such hypotheses have assumed the form
+       `p = p`, which can easily be proved without introducing an assumption. *)
+    if boolSyntax.is_eq t then
+      let
+        val (lhs, rhs) = boolSyntax.dest_eq t
+      in
+        if Term.term_eq lhs rhs then
+          (state, Thm.REFL lhs)
+        else
+          (state, Thm.ASSUME t)
+      end
+    else
+      (state, Thm.ASSUME t)
 
   (*   ... |- ~p
      ------------
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index b62b65f4e6..6850d79f7b 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -281,11 +281,11 @@ in
     (``(1:num) DIV 42 = 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``(42:num) DIV 42 = 1``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
     (``(x:num) DIV 1 = x``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:num) DIV 42 <= x``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``((x:num) DIV 42 = x) = (x = 0)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:num) DIV 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:num) DIV 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:num) DIV 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -302,7 +302,7 @@ in
     (``(x:num) MOD 42 < 42``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``((x:num) MOD 42 = x) = (x < 42)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:num) MOD 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:num) MOD 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:num) MOD 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -313,7 +313,7 @@ in
     (``((x:num) = x DIV 1 * 1 + x MOD 1) /\ x MOD 1 < 1``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``((x:num) = x DIV 42 * 42 + x MOD 42) /\ x MOD 42 < 42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``MIN (x:num) y <= x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),
     (``MIN (x:num) y <= y``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p_v4]),

From 5db3618b31bcc94c62070d68daf4da6ace4ec409 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 10:39:08 +0000
Subject: [PATCH 12/27] HolSmt: merge z3_lemma_arith and z3_rewrite's arith

Since these two decision procedures need to handle the same kind of
terms (including smtdiv / smtmod rewrites), this commit merges them.
---
 src/HolSmt/Z3_ProofReplay.sml | 68 +++++++++++++++++------------------
 1 file changed, 34 insertions(+), 34 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 5a38c75825..c3720a87e5 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -468,6 +468,38 @@ local
     Tactical.TAC_PROOF ((HOLset.listItems asms, t), metisLib.METIS_TAC thms)
   end
 
+  (* Returns a proof of `t` using arithmetic decision procedures. This function
+     is used by both `z3_th_lemma_arith` and `z3_rewrite`. *)
+  fun arith_prove t =
+    let
+      fun cooper goal =
+        profile "arith_prove(cooper)" intLib.COOPER_TAC goal
+      fun tactic (goal as (_, term)) =
+        if term_contains_real_ty term then
+          (* this is just a heuristic - it is quite conceivable that a
+             term that contains type real is provable by integer
+             arithmetic *)
+          profile "arith_prove(real)" RealField.REAL_ARITH_TAC goal
+        else (
+          profile "arith_prove(int)" intLib.ARITH_TAC goal
+          (* the following two exception handlers are workarounds for these two
+             issues:
+             https://github.com/HOL-Theorem-Prover/HOL/issues/1203
+             https://github.com/HOL-Theorem-Prover/HOL/issues/1209 *)
+          handle NotFound => cooper goal
+          handle Feedback.HOL_ERR _ => cooper goal
+        )
+    in
+      Tactical.prove (t,
+        (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic
+           decision procedures can solve terms containing these functions *)
+        PURE_REWRITE_TAC[HolSmtTheory.smtdiv_def, HolSmtTheory.smtmod_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]
+        >> tactic)
+    end
+
   (***************************************************************************)
   (* implementation of Z3's inference rules                                  *)
   (***************************************************************************)
@@ -969,15 +1001,7 @@ local
         profile "rewrite(10)(BBLAST)" blastLib.BBLAST_PROVE t
         handle Feedback.HOL_ERR _ =>
 
-        if profile "rewrite(11.0)(contains_real)" term_contains_real_ty t then
-          profile "rewrite(11.1)(REAL_ARITH)" RealField.REAL_ARITH t
-        else (
-          profile "rewrite(11.2)(ARITH_PROVE)" intLib.ARITH_PROVE t
-            (* the following is a workaround for:
-               https://github.com/HOL-Theorem-Prover/HOL/issues/1209 *)
-            handle NotFound =>
-              raise ERR "z3_rewrite" "ARITH_PROVE raised NotFound"
-        )
+        profile "rewrite(11)(arith)" arith_prove t
     in
       (state_cache_thm state thm, thm)
     end
@@ -1067,31 +1091,7 @@ local
 
   val z3_th_lemma_arith = th_lemma_wrapper "arith" (fn (state, t) =>
     let
-      fun cooper goal =
-        profile "th_lemma[arith](3.3)(cooper)" intLib.COOPER_TAC goal
-      fun tactic (goal as (_, term)) =
-        if term_contains_real_ty term then
-          (* 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)" RealField.REAL_ARITH_TAC goal
-        else (
-          profile "th_lemma[arith](3.2)(int)" intLib.ARITH_TAC goal
-          (* the following two exception handlers are workarounds for these two
-             issues:
-             https://github.com/HOL-Theorem-Prover/HOL/issues/1203
-             https://github.com/HOL-Theorem-Prover/HOL/issues/1209 *)
-          handle NotFound => cooper goal
-          handle Feedback.HOL_ERR _ => cooper goal
-        )
-      val thm = Tactical.prove (t,
-        (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic
-           decision procedures can solve terms containing these functions *)
-        PURE_REWRITE_TAC[HolSmtTheory.smtdiv_def, HolSmtTheory.smtmod_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]
-        >> tactic)
+      val thm = profile "th_lemma[arith](3)" arith_prove t
     in
       (* cache 'thm' *)
       (state_cache_thm state thm, thm)

From 351fe7470f06e1653bbf070c7d5d71f975bf624d Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 12:10:32 +0000
Subject: [PATCH 13/27] HolSmt: try harder to replay arithmetic proof steps

This commit adds some tactics which help prove some arithmetic proof
steps that intLib.{ARITH,COOPER}_TAC can't deal with.

These are basically some workarounds for:

https://github.com/HOL-Theorem-Prover/HOL/issues/1207

This allows us to enable proof replay for the remaining arithmetic
test cases that didn't already have proof replay enabled, with the
exception of the very last test case (because we can't replay
nonlinear arithmetic proof steps).

That said, I don't expect these workarounds to be very reliable.

Ideally, it would be better to improve HOL4's linear arithmetic
decision procedures.
---
 src/HolSmt/Z3_ProofReplay.sml |  16 ++++-
 src/HolSmt/selftest.sml       | 116 +++++++++++++++++-----------------
 2 files changed, 72 insertions(+), 60 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index c3720a87e5..551ff1272b 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -13,6 +13,7 @@ local
 
   open Z3_Proof
 
+  val op ++ = bossLib.++
   val op >> = Tactical.>>
 
   val ERR = Feedback.mk_HOL_ERR "Z3_ProofReplay"
@@ -474,7 +475,7 @@ local
     let
       fun cooper goal =
         profile "arith_prove(cooper)" intLib.COOPER_TAC goal
-      fun tactic (goal as (_, term)) =
+      fun arith_tactic (goal as (_, term)) =
         if term_contains_real_ty term then
           (* this is just a heuristic - it is quite conceivable that a
              term that contains type real is provable by integer
@@ -489,6 +490,10 @@ local
           handle NotFound => cooper goal
           handle Feedback.HOL_ERR _ => cooper goal
         )
+      val TRY = Tactical.TRY
+      val ap_tactic =
+        TRY AP_TERM_TAC >> TRY arith_tactic
+        >> TRY AP_THM_TAC >> TRY arith_tactic
     in
       Tactical.prove (t,
         (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic
@@ -497,7 +502,14 @@ local
         (* 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]
-        >> tactic)
+        (* if `arith_tactic` doesn't work at first, don't give up immediately;
+           instead let's try additional tactics *)
+        >> TRY arith_tactic
+        >> bossLib.RW_TAC (bossLib.arith_ss ++ intSimps.INT_RWTS_ss ++
+             intSimps.INT_ARITH_ss ++ realSimps.REAL_ARITH_ss)
+               [Conv.GSYM integerTheory.INT_NEG_MINUS1]
+        >> TRY arith_tactic
+        >> Tactical.rpt (Tactical.CHANGED_TAC ap_tactic))
     end
 
   (***************************************************************************)
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 6850d79f7b..78497977ac 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -358,51 +358,51 @@ in
     (``(x:int) * 42 = 42 * x``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
     (``(~42:int) / ~42 = 1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) / ~42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(0:int) / ~42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(1:int) / ~42 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) / ~42 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~42:int) / ~1 = 42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) / ~1 = 1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(0:int) / ~1 = 0``, [thm_AUTO, (*thm_CVC*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(0:int) / ~1 = 0``, [thm_AUTO, (*thm_CVC*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(1:int) / ~1 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) / ~1 = ~42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~42:int) / 1 = ~42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) / 1 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(0:int) / 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(1:int) / 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(0:int) / 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(1:int) / 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) / 1 = 42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~42:int) / 42 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) / 42 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(0:int) / 42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(1:int) / 42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) / 42 = 1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(x:int) / 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:int) / 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) / ~1 = ~x``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) / 42 <= x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:int) / 42 <= ABS x``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3_v4(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``((x:int) / 42 = x) = (x = 0)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:int) / 42 = x <=> x = 0 \/ x = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) / 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:int) / 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:int) / 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -412,64 +412,64 @@ in
 
     (* cf. integerTheory.int_div *)
     (``(x:int) < 0 ==> (x / 1 = ~(~x / 1) + if ~x % 1 = 0 then 0 else ~1)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) < 0 ==> (x / 42 = ~(~x / 42) + if ~x % 42 = 0 then 0 else ~1)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``0 <= (x:int) ==> (x / ~42 = ~(x / 42) + if x % 42 = 0 then 0 else ~1)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``0 <= (x:int) ==> (x / ~1 = ~(x / 1) + if x % 1 = 0 then 0 else ~1)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) < 0 ==> (x / ~42 = ~x / 42)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``(~42:int) % ~42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) % ~42 = ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(0:int) % ~42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(1:int) % ~42 = ~41``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) % ~42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~42:int) % ~1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) % ~1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(0:int) % ~1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(1:int) % ~1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) % ~1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~42:int) % 1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) % 1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(0:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(1:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(0:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(1:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) % 1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~42:int) % 42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) % 42 = 41``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(0:int) % 42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(1:int) % 42 = 1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(42:int) % 42 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
-    (``(x:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
+    (``(x:int) % 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) % ~1 = 0``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) % 42 < 42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``((x:int) % 42 = x) = (x < 42)``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``((x:int) % 42 = x) <=> (0 <= x) /\ (x < 42)``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) % 0 = x``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(x:int) % 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
     (``(0:int) % 0 = 0``, [sat_CVC, sat_YO, sat_Z3, sat_Z3p]),
@@ -478,13 +478,13 @@ in
 
     (* cf. integerTheory.int_mod *)
     (``(x:int) % ~42 = x - x / ~42 * ~42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) % ~1 = x - x / ~1 * ~1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) % 1 = x - x / 1 * 1``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(x:int) % 42 = x - x / 42 * 42``,
-      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3(*, thm_Z3p*)]),
+      [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
     (``ABS (x:int) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),

From 898d8f5d0ff4d9810ddb53783cb2c4491b511996 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Tue, 12 Mar 2024 14:55:08 +0000
Subject: [PATCH 14/27] HolSmt: update documentation

---
 Manual/Description/HolSmt.tex                 | 14 +++++++-------
 Manual/Translations/IT/Description/HolSmt.tex | 14 +++++++-------
 2 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Manual/Description/HolSmt.tex b/Manual/Description/HolSmt.tex
index 2e9bcf8237..c145bf9ceb 100644
--- a/Manual/Description/HolSmt.tex
+++ b/Manual/Description/HolSmt.tex
@@ -164,12 +164,12 @@ \subsection{Interface}
 formulas) can be found in \ml{SmtLib\_Parser.sml}, with auxiliary
 functions in \ml{SmtLib\_\{Logics,Theories\}.sml}.
 
-The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{int}
-and \holtxt{real}, fixed-width word types, and the following terms:
-equality, Boolean connectives, quantifiers, numeric literals,
-arithmetic operators, comparison operators, function application, and
-various word operations.  Notably, the SMT-LIB interface does
-\emph{not} support type \holtxt{num}, data types or records, and
+The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{num},
+\holtxt{int} and \holtxt{real}, fixed-width word types, and the
+following terms: equality, Boolean connectives, quantifiers, numeric
+literals, arithmetic operators, comparison operators, function
+application, and various word operations.  Notably, the SMT-LIB
+interface does \emph{not} support data types or records, and
 higher-order formulas.  See the files mentioned above and the examples
 in \ml{selftest.sml} for further details.
 
@@ -194,7 +194,7 @@ \subsection{Interface}
 \subsection{Installing SMT solvers}
 
 \ml{HolSmtLib} has been tested with cvc5~1.1.0, Yices~1.0.40, and
-Z3~4.12.4. Later versions may or may not work.  (Yices~2 is not
+Z3~4.12.6. Later versions may or may not work.  (Yices~2 is not
 supported.)  To use \ml{HolSmtLib}, you need to install at least one
 of these SMT solvers on your machine.  As mentioned before, Yices
 supports a larger fragment of higher-order logic than Z3, but proof
diff --git a/Manual/Translations/IT/Description/HolSmt.tex b/Manual/Translations/IT/Description/HolSmt.tex
index 2e9bcf8237..c145bf9ceb 100644
--- a/Manual/Translations/IT/Description/HolSmt.tex
+++ b/Manual/Translations/IT/Description/HolSmt.tex
@@ -164,12 +164,12 @@ \subsection{Interface}
 formulas) can be found in \ml{SmtLib\_Parser.sml}, with auxiliary
 functions in \ml{SmtLib\_\{Logics,Theories\}.sml}.
 
-The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{int}
-and \holtxt{real}, fixed-width word types, and the following terms:
-equality, Boolean connectives, quantifiers, numeric literals,
-arithmetic operators, comparison operators, function application, and
-various word operations.  Notably, the SMT-LIB interface does
-\emph{not} support type \holtxt{num}, data types or records, and
+The SMT-LIB~2 translation supports types \holtxt{bool}, \holtxt{num},
+\holtxt{int} and \holtxt{real}, fixed-width word types, and the
+following terms: equality, Boolean connectives, quantifiers, numeric
+literals, arithmetic operators, comparison operators, function
+application, and various word operations.  Notably, the SMT-LIB
+interface does \emph{not} support data types or records, and
 higher-order formulas.  See the files mentioned above and the examples
 in \ml{selftest.sml} for further details.
 
@@ -194,7 +194,7 @@ \subsection{Interface}
 \subsection{Installing SMT solvers}
 
 \ml{HolSmtLib} has been tested with cvc5~1.1.0, Yices~1.0.40, and
-Z3~4.12.4. Later versions may or may not work.  (Yices~2 is not
+Z3~4.12.6. Later versions may or may not work.  (Yices~2 is not
 supported.)  To use \ml{HolSmtLib}, you need to install at least one
 of these SMT solvers on your machine.  As mentioned before, Yices
 supports a larger fragment of higher-order logic than Z3, but proof

From 60b04835aa13711f9273fd1f0ea3ee43f4988193 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 02:22:04 +0000
Subject: [PATCH 15/27] HolSmt: fix workaround for extra hypothesis in proof
 replay

The previously-implemented workaround might have an issue where if Z3
introduces an hypothesis of the form `P = P` but then *doesn't* forget
to discharge it, we might fail to replay the `lemma` proof rule
because we avoided adding an assumption.

Instead, this commit fixes the workaround so that we remove the extra
hypothesis at the end of the proof replay procedure, i.e. only when we
are sure that Z3 *did* forget to discharge the hypothesis.
---
 src/HolSmt/Z3_ProofReplay.sml | 40 +++++++++++++++++++++++------------
 1 file changed, 26 insertions(+), 14 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 551ff1272b..0fe84ea6cf 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -652,20 +652,6 @@ local
   (* introduces a local hypothesis (which must be discharged by
      'z3_lemma' at some later point in the proof) *)
   fun z3_hypothesis (state, t) =
-    (* FIXME: The following is a workaround for a yet-to-be-filed Z3 issue where
-       a hypothesis is introduced but is not discharged by `z3_lemma` at any
-       point in the proof. So far, all such hypotheses have assumed the form
-       `p = p`, which can easily be proved without introducing an assumption. *)
-    if boolSyntax.is_eq t then
-      let
-        val (lhs, rhs) = boolSyntax.dest_eq t
-      in
-        if Term.term_eq lhs rhs then
-          (state, Thm.REFL lhs)
-        else
-          (state, Thm.ASSUME t)
-      end
-    else
       (state, Thm.ASSUME t)
 
   (*   ... |- ~p
@@ -1547,6 +1533,28 @@ local
     HOLset.foldl remove_hyp thm bad_hyps
   end
 
+  (* FIXME: The following is a workaround for a yet-to-be-filed Z3 issue where
+     a hypothesis is introduced in a `hypothesis` rule but is not discharged by
+     a `lemma` rule at any point in the proof. So far, all such hypotheses have
+     assumed the form `p = p`, which can easily be discharged here. *)
+  fun remove_extra_hyps (asserted, thm) =
+  let
+    val extra_hyps = HOLset.difference (Thm.hypset thm, asserted)
+    fun remove_hyp (hyp, thm) =
+      if boolSyntax.is_eq hyp then
+        let
+          val (lhs, rhs) = boolSyntax.dest_eq hyp
+        in
+          if Term.term_eq lhs rhs then
+            Drule.PROVE_HYP (Thm.REFL lhs) thm
+          else
+            thm
+        end
+      else
+        thm
+  in
+    HOLset.foldl remove_hyp thm extra_hyps
+  end
 in
   (* For unit tests *)
   val remove_definitions = remove_definitions
@@ -1577,6 +1585,10 @@ in
     val final_thm = profile "check_proof(remove_definitions)" remove_definitions
       (#definition_hyps state, #var_set state, thm)
 
+    (* workaround for Z3 bug *)
+    val final_thm = profile "check_proof(remove_extra_hyps)" remove_extra_hyps
+      (#asserted_hyps state, final_thm)
+
     (* check that the final theorem contains no hyps other than those
        that have been asserted *)
     val _ = profile "check_proof(hypcheck)" HOLset.isSubset (Thm.hypset final_thm,

From d72e1ed0fe50fa20029c96cd9926fde24c7ebedd Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 12:01:51 +0000
Subject: [PATCH 16/27] Add Euclidean div and mod, plus some num/int theorems

---
 src/integer/integerScript.sml | 64 +++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/src/integer/integerScript.sml b/src/integer/integerScript.sml
index e5853a9468..81dafa3b45 100644
--- a/src/integer/integerScript.sml
+++ b/src/integer/integerScript.sml
@@ -3502,6 +3502,70 @@ val LEAST_INT_DEF = new_definition ("LEAST_INT_DEF",
 
 val _ = set_fixity "LEAST_INT" Binder
 
+(*---------------------------------------------------------------------------*)
+(* Euclidean div and mod                                                     *)
+(*---------------------------------------------------------------------------*)
+
+val EDIV_DEF = new_definition ("EDIV_DEF",
+  ``ediv i j = if 0 < j then i / j else -(i / -j)``)
+
+val EMOD_DEF = new_definition ("EMOD_DEF",
+  ``emod i j = i % ABS j``)
+
+(*---------------------------------------------------------------------------*)
+(* Theorems used for converting div/mod operations into ediv and emod        *)
+(*---------------------------------------------------------------------------*)
+
+val INT_DIV_EDIV = store_thm("INT_DIV_EDIV",
+  Term`!i j. j <> 0 ==> i / j = if 0 < j then ediv i j else -ediv (-i) j`,
+  simp[EDIV_DEF, INT_DIV_NEG, INT_NEGNEG])
+
+val INT_MOD_EMOD = store_thm("INT_MOD_EMOD",
+  Term`!i j. j <> 0 ==> i % j = if 0 < j then emod i j else -emod (-i) j`,
+  METIS_TAC[INT_MOD_NEG, INT_NEGNEG, INT_NOT_LT, INT_LT_LE, EMOD_DEF, INT_ABS])
+
+val INT_QUOT_EDIV = store_thm("INT_QUOT_EDIV",
+  Term`!i j. j <> 0 ==> i quot j = if 0 <= i then ediv i j else ediv (-i) (-j)`,
+  simp[EDIV_DEF, int_quot, int_div, INT_DIV_NEG, INT_NEGNEG] THEN
+  METIS_TAC[INT_NEG_0, NUM_OF_INT, INT_ADD_LID, INT_LT_LE, INT_NOT_LE,
+    INT_LE_NEG, ZERO_DIV, ZERO_MOD, NUM_LT])
+
+val INT_REM_EMOD = store_thm("INT_REM_EMOD",
+  Term`!i j. j <> 0 ==> i rem j = if 0 <= i then emod i j else -emod (-i) j`,
+  REPEAT GEN_TAC THEN
+  STRIP_TAC THEN
+  simp[EMOD_DEF, int_rem, int_mod, int_quot, int_div, INT_ABS_EQ0] THEN
+  simp[INT_ABS] THEN
+  Cases_on `j < 0` THEN
+  simp[INT_NEGNEG] THEN
+  METIS_TAC[INT_MUL_CALCULATE, INT_LE_NEG, INT_LT_LE, INT_NOT_LE, INT_SUB_NEG2,
+    INT_NEG_SUB, INT_NEG_EQ0])
+
+(*---------------------------------------------------------------------------*)
+(* Theorems used for converting num operators into int operators             *)
+(*---------------------------------------------------------------------------*)
+
+val NUM_INT_ADD = store_thm("NUM_INT_ADD",
+  Term`!m n. m + n = Num (&m + &n)`,
+  REWRITE_TAC [INT_ADD, NUM_OF_INT])
+
+val NUM_INT_SUB = store_thm("NUM_INT_SUB",
+  Term`!m n. m - n = if &m <= &n then 0n else Num (&m - &n)`,
+  METIS_TAC[INT_LE, INT_SUB, NUM_OF_INT, NOT_LESS_EQUAL, LESS_IMP_LESS_OR_EQ,
+    SUB_EQ_0, INT_LE])
+
+val NUM_INT_MUL = store_thm("NUM_INT_MUL",
+  Term`!m n. m * n = Num (&m * &n)`,
+  REWRITE_TAC [INT_MUL, NUM_OF_INT])
+
+val NUM_INT_EDIV = store_thm("NUM_INT_EDIV",
+  Term`!n m. m <> 0 ==> n DIV m = Num (ediv (&n) (&m))`,
+  METIS_TAC[EDIV_DEF, INT_POS, INT_LT_LE, INT_DIV, NUM_OF_INT])
+
+val NUM_INT_EMOD = store_thm("NUM_INT_EMOD",
+  Term`!n m. m <> 0 ==> n MOD m = Num (emod (&n) (&m))`,
+  METIS_TAC[EMOD_DEF, INT_ABS_NUM, INT_MOD, NUM_OF_INT])
+
 (*---------------------------------------------------------------------------*)
 
 val _ = BasicProvers.export_rewrites

From 064412bf966296f5c43525176b570e3b6c9b181f Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 12:25:37 +0000
Subject: [PATCH 17/27] HolSmt: use integerTheory's ediv and emod

Now that integerTheory contains the definitions for Euclidean div and
mod, let's use that instead of redefining these operators in
HolSmtTheory.
---
 src/HolSmt/HolSmtScript.sml    | 50 ----------------------------------
 src/HolSmt/SmtLib.sml          | 12 ++++----
 src/HolSmt/SmtLib_Theories.sml | 12 ++++----
 src/HolSmt/Z3_ProofReplay.sml  |  6 ++--
 src/HolSmt/selftest.sml        | 10 +++----
 5 files changed, 18 insertions(+), 72 deletions(-)

diff --git a/src/HolSmt/HolSmtScript.sml b/src/HolSmt/HolSmtScript.sml
index 88a05e997e..99d9885e3b 100644
--- a/src/HolSmt/HolSmtScript.sml
+++ b/src/HolSmt/HolSmtScript.sml
@@ -34,56 +34,6 @@
   val _ = Theory.new_theory "HolSmt"
   val _ = ParseExtras.temp_loose_equality()
 
-  (* constants used in SMT-LIB *)
-
-  val smtdiv_def = bossLib.Define
-    `smtdiv (i: int) (j: int) = if 0 < j then i / j else -(i / -j)`
-
-  val smtmod_def = bossLib.Define
-    `smtmod (i: int) (j: int) = i % ABS j`
-
-  (* Note that according to SMT-LIB's `Ints` theory, `div` and `mod` must match
-     Boute's Euclidean definition, that is, they must satisfy the formula:
-
-     !m n. n <> 0 ==>
-       let q = smtdiv m n
-       and r = smtmod m n
-       in
-         (m = n * q + r /\ 0 <= r /\ r <= (ABS n) - 1)
-
-     We prove this as a test case in `selftest.sml` *)
-
-  (* theorems used for arithmetic operators *)
-
-  val _ = s ("SMT_NUM_ADD", A ``!m n. m + n = Num (&m + &n)``)
-  val _ = s ("SMT_NUM_SUB", A
-    ``!m n. m - n = if (&m:int) <= &n then 0n else Num (&m - &n)``)
-  val _ = s ("SMT_NUM_MUL", I [] ``!m n. m * n = Num (&m * &n)``)
-  val _ = s ("SMT_NUM_DIV", I [smtdiv_def]
-    ``!k n. n <> 0 ==> (k DIV n = Num (smtdiv (&k) (&n)))``)
-  val _ = s ("SMT_NUM_MOD", I [smtmod_def]
-    ``!k n. n <> 0 ==> (k MOD n = Num (smtmod (&k) (&n)))``)
-  val _ = s ("SMT_INT_DIV", I [smtdiv_def]
-    ``!i j. j <> 0 ==> (i / j =
-        if 0 < j then smtdiv i j else -(smtdiv (-i) j))``)
-  val _ = s ("SMT_INT_MOD", I [smtmod_def, integerTheory.INT_ABS]
-    ``!i j. j <> 0 ==> (i % j =
-        if 0 < j then smtmod i j else -(smtmod (-i) j))``)
-  val _ = s ("SMT_INT_QUOT", Tactical.prove (
-    ``!i j. j <> 0 ==> (i quot j =
-        if 0 <= i then smtdiv i j else smtdiv (-i) (-j))``,
-          bossLib.rw [smtdiv_def, integerTheory.int_div, integerTheory.int_quot]
-          >> bossLib.Cases_on `i = 0` >> bossLib.fs [] >> intLib.ARITH_TAC))
-  val _ = s ("SMT_INT_REM", Tactical.prove (
-    ``!i j. j <> 0 ==> (i rem j =
-        if 0 <= i then smtmod i j else -(smtmod (-i) j))``,
-          let
-            open integerTheory
-          in
-            bossLib.rw [smtmod_def, int_mod, int_rem, int_div, int_quot, INT_ABS]
-            >> intLib.ARITH_TAC
-          end))
-
   (* constants used by Z3 *)
 
   (* exclusive or *)
diff --git a/src/HolSmt/SmtLib.sml b/src/HolSmt/SmtLib.sml
index ded9ae6baa..1600382507 100644
--- a/src/HolSmt/SmtLib.sml
+++ b/src/HolSmt/SmtLib.sml
@@ -90,8 +90,8 @@ local
     (intSyntax.minus_tm, apfst_K "-"),
     (intSyntax.plus_tm, apfst_K "+"),
     (intSyntax.mult_tm, apfst_K "*"),
-    (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, apfst_K "div"),
-    (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, apfst_K "mod"),
+    (Term.prim_mk_const {Thy="integer", Name="ediv"}, apfst_K "div"),
+    (Term.prim_mk_const {Thy="integer", Name="emod"}, apfst_K "mod"),
     (intSyntax.absval_tm, apfst_K "abs"),
     (intSyntax.leq_tm, apfst_K "<="),
     (intSyntax.less_tm, apfst_K "<"),
@@ -628,17 +628,15 @@ in
        are being used. For now we just manually add a few useful ones. *)
     val facts =
     let
-      open arithmeticTheory integerTheory HolSmtTheory
+      open arithmeticTheory integerTheory
     in
       if !include_theorems then [
         (* arithmeticTheory *)
         GREATER_DEF, GREATER_EQ, MIN_DEF, MAX_DEF,
         (* integerTheory *)
         INT, INT_ADD, INT_INJ, INT_LE, INT_LT, INT_MAX, INT_MIN, INT_OF_NUM,
-        INT_POS, NUM_OF_INT,
-        (* HolSmtTheory *)
-        SMT_NUM_MUL, SMT_NUM_DIV, SMT_NUM_MOD, SMT_INT_DIV, SMT_INT_MOD,
-        SMT_INT_QUOT, SMT_INT_REM,
+        INT_POS, NUM_OF_INT, NUM_INT_MUL, NUM_INT_EDIV, NUM_INT_EMOD,
+        INT_DIV_EDIV, INT_MOD_EMOD, INT_QUOT_EDIV, INT_REM_EMOD,
         (* others *)
         int_arithTheory.INT_NUM_SUB,
         realaxTheory.real_min, realaxTheory.real_max, realTheory.abs
diff --git a/src/HolSmt/SmtLib_Theories.sml b/src/HolSmt/SmtLib_Theories.sml
index 21ef226284..ba43e82ad4 100644
--- a/src/HolSmt/SmtLib_Theories.sml
+++ b/src/HolSmt/SmtLib_Theories.sml
@@ -271,9 +271,9 @@ in
       ("+", leftassoc intSyntax.mk_plus),
       ("*", leftassoc intSyntax.mk_mult),
       ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
-        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+        (Term.prim_mk_const {Thy="integer", Name="ediv"}, t1), t2))),
       ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
-        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
+        (Term.prim_mk_const {Thy="integer", Name="emod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),
@@ -336,13 +336,13 @@ in
       ("+", leftassoc intSyntax.mk_plus),
       ("*", leftassoc intSyntax.mk_mult),
       ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
-        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+        (Term.prim_mk_const {Thy="integer", Name="ediv"}, t1), t2))),
       ("div0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
-        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+        (Term.prim_mk_const {Thy="integer", Name="ediv"}, t1), t2))),
       ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
-        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
+        (Term.prim_mk_const {Thy="integer", Name="emod"}, t1), t2))),
       ("mod0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
-        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
+        (Term.prim_mk_const {Thy="integer", Name="emod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),
diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 0fe84ea6cf..3c332dee51 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -19,8 +19,6 @@ local
   val ERR = Feedback.mk_HOL_ERR "Z3_ProofReplay"
   val WARNING = Feedback.HOL_WARNING "Z3_ProofReplay"
 
-  val smtdiv_def = HolSmtTheory.smtdiv_def
-  val smtmod_def = HolSmtTheory.smtmod_def
   val ALL_DISTINCT_NIL = HolSmtTheory.ALL_DISTINCT_NIL
   val ALL_DISTINCT_CONS = HolSmtTheory.ALL_DISTINCT_CONS
   val NOT_MEM_NIL = HolSmtTheory.NOT_MEM_NIL
@@ -496,9 +494,9 @@ local
         >> TRY AP_THM_TAC >> TRY arith_tactic
     in
       Tactical.prove (t,
-        (* rewrite the `smtdiv`, `smtmod` symbols so that the arithmetic
+        (* rewrite the `ediv` and `emod` symbols so that the arithmetic
            decision procedures can solve terms containing these functions *)
-        PURE_REWRITE_TAC[HolSmtTheory.smtdiv_def, HolSmtTheory.smtmod_def]
+        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]
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 78497977ac..e32a7310dd 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -1150,12 +1150,12 @@ in
     (``x IN P INTER (Q INTER R) <=> x IN (P INTER Q) INTER R``,
       [thm_AUTO, thm_CVC, thm_YO, thm_Z3, thm_Z3p]),
 
-    (* prove that HolSmt$smtdiv and HolSmt$smtmod match Boute's Euclidean
-       definition, i.e. that they match SMT-LIB's `Ints` theory's definition of
-       integer div and mod *)
+    (* prove that `ediv` and `emod` match Boute's Euclidean definition, i.e.
+       that they match SMT-LIB's `Ints` theory's definition of integer div and
+       mod *)
     (``!m n. n <> 0 ==>
-         let q = HolSmt$smtdiv m n
-         and r = HolSmt$smtmod m n
+         let q = ediv m n
+         and r = emod m n
          in
            (m = n * q + r /\ 0 <= r /\ r <= (ABS n) - 1)``,
       [(*thm_AUTO, thm_CVC,*) thm_Z3_v4(*, thm_Z3p*)])

From caecc7abcff78ff2cb84fcb0b4e5743dd74c1fa2 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 12:28:42 +0000
Subject: [PATCH 18/27] HolSmt: remove workaround for NotFound exn in ARITH_TAC

Now that #1209 is fixed, we can remove the workaround for it in
HolSmt.
---
 src/HolSmt/Z3_ProofReplay.sml | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index 3c332dee51..d6e06b5fd2 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -471,8 +471,6 @@ local
      is used by both `z3_th_lemma_arith` and `z3_rewrite`. *)
   fun arith_prove t =
     let
-      fun cooper goal =
-        profile "arith_prove(cooper)" intLib.COOPER_TAC goal
       fun arith_tactic (goal as (_, term)) =
         if term_contains_real_ty term then
           (* this is just a heuristic - it is quite conceivable that a
@@ -481,12 +479,10 @@ local
           profile "arith_prove(real)" RealField.REAL_ARITH_TAC goal
         else (
           profile "arith_prove(int)" intLib.ARITH_TAC goal
-          (* the following two exception handlers are workarounds for these two
-             issues:
-             https://github.com/HOL-Theorem-Prover/HOL/issues/1203
-             https://github.com/HOL-Theorem-Prover/HOL/issues/1209 *)
-          handle NotFound => cooper goal
-          handle Feedback.HOL_ERR _ => cooper goal
+          (* the following exception handler is a workaround for this issue:
+             https://github.com/HOL-Theorem-Prover/HOL/issues/1203 *)
+          handle Feedback.HOL_ERR _ =>
+            profile "arith_prove(cooper)" intLib.COOPER_TAC goal
         )
       val TRY = Tactical.TRY
       val ap_tactic =

From 6220a17848fd58bcb54bb9df9df6b55d5859abf0 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 16:13:25 +0000
Subject: [PATCH 19/27] 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 | 3 ++-
 src/HolSmt/selftest.sml       | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index d6e06b5fd2..e0195cc7d5 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/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
diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index e32a7310dd..5eb06b9b85 100644
--- a/src/HolSmt/selftest.sml
+++ b/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

From e14320c73f62d60e2f35a00eb026ec749a4b9535 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 16:48:01 +0000
Subject: [PATCH 20/27] HolSmt: add full battery of `quot` and `rem` tests

---
 src/HolSmt/selftest.sml | 93 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 93 insertions(+)

diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index 5eb06b9b85..de57ab8ed2 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -425,6 +425,55 @@ in
     (``(x:int) < 0 ==> (x / ~1 = ~x / 1)``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
+    (``(~42:int) quot ~42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot ~42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) quot ~1 = 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot ~1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot ~1 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot ~1 = ~42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) quot 1 = ~42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot 1 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot 1 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot 1 = 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) quot 42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) quot 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) quot 42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot 1 = x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot ~1 = ~x``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot 42 <= x``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 42 <= ABS x``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3_v4, thm_Z3p_v4]),
+    (``((x:int) quot 42 = x) = (x = 0)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) quot 42 = x <=> x = 0 \/ x = ~1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 0 = x``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) quot 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) quot 0 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) quot 0 = 1 quot 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) quot 0 = x quot 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+
+    (* cf. integerTheory.int_quot *)
+    (``(x:int) < 0 ==> (x quot 1 = ~(~x quot 1))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) < 0 ==> (x quot 42 = ~(~x quot 42))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``0 <= (x:int) ==> (x quot ~42 = ~(x quot 42))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``0 <= (x:int) ==> (x quot ~1 = ~(x quot 1))``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) < 0 ==> (x quot ~42 = ~x quot 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) < 0 ==> (x quot ~1 = ~x quot 1)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+
     (``(~42:int) % ~42 = 0``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
     (``(~1:int) % ~42 = ~1``,
@@ -487,6 +536,50 @@ in
     (``(x:int) % 42 = x - x / 42 * 42``,
       [thm_AUTO, (*thm_CVC,*) thm_YO, thm_Z3, thm_Z3p_v4]),
 
+    (``(~42:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem ~42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem ~42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem ~42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~42:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(~1:int) rem 42 = ~1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(0:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(1:int) rem 42 = 1``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(42:int) rem 42 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem ~1 = 0``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 42 < 42``, [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``((x:int) rem 42 = x) = (x < 42)``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``((x:int) rem 42 = x) <=> (0 <= x) /\ (x < 42)``,
+      [sat_CVC, sat_Z3, sat_Z3p]),
+    (``((x:int) rem 42 = x) <=> (-42 < x) /\ (x < 42)``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 0 = x``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) rem 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) rem 0 = 0``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(0:int) rem 0 = 1``, [sat_CVC, sat_Z3, sat_Z3p]),
+    (``(x:int) rem 0 = x rem 0``, [thm_AUTO, thm_CVC, thm_Z3, thm_Z3p]),
+
+    (* cf. integerTheory.int_rem *)
+    (``(x:int) rem ~42 = x - x quot ~42 * ~42``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem ~1 = x - x quot ~1 * ~1``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 1 = x - x quot 1 * 1``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+    (``(x:int) rem 42 = x - x quot 42 * 42``,
+      [thm_AUTO, (*thm_CVC,*) thm_Z3, thm_Z3p_v4]),
+
     (``ABS (x:int) >= 0``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``(ABS (x:int) = 0) = (x = 0)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),
     (``(x:int) >= 0 ==> (ABS x = x)``, [thm_AUTO, thm_CVC, thm_YO, thm_Z3_v4, thm_Z3p_v4]),

From 40470928362715aff9408a56c2dbb66bf9aa959a Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Thu, 14 Mar 2024 17:21:12 +0000
Subject: [PATCH 21/27] HolSmt: add `let`, `ediv` and `emod` simps to
 `thm_AUTO`

---
 src/HolSmt/selftest.sml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/HolSmt/selftest.sml b/src/HolSmt/selftest.sml
index de57ab8ed2..f4a0040d03 100644
--- a/src/HolSmt/selftest.sml
+++ b/src/HolSmt/selftest.sml
@@ -107,7 +107,8 @@ fun auto_tac (_, t) =
     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_quot,
-      integerTheory.int_rem]
+      integerTheory.int_rem, integerTheory.EDIV_DEF, integerTheory.EMOD_DEF,
+      boolTheory.LET_THM]
       t
       handle Conv.UNCHANGED =>
         Thm.REFL t

From 9d9dfa2b4ff9f1710e4e055e1872d109c1a2dd98 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Fri, 15 Mar 2024 12:01:30 +0000
Subject: [PATCH 22/27] HolSmt: ignore indices in `rewrite` proof rules

In case `rewrite` proof rules ever come to have indices, let's ignore
them instead of erroring out.
---
 src/HolSmt/Z3_ProofParser.sml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/HolSmt/Z3_ProofParser.sml b/src/HolSmt/Z3_ProofParser.sml
index aabdace41c..ac816d75cf 100644
--- a/src/HolSmt/Z3_ProofParser.sml
+++ b/src/HolSmt/Z3_ProofParser.sml
@@ -139,7 +139,9 @@ local
     ("quant-inst",      list_args_zero_prems "quant-inst"),
     ("quant-intro",     one_prem "quant-intro"),
     ("refl",            zero_prems "refl"),
-    ("rewrite",         zero_prems "rewrite"),
+    (* in `rewrite` proof rules, we currently ignore the indices (if they exist) *)
+    ("rewrite",         (fn token => fn indices => fn prems =>
+      zero_prems "rewrite" token [] prems)),
     ("sk",              zero_prems "sk"),
     ("symm",            one_prem "symm"),
     ("th-lemma",        SmtLib_Theories.list_list (fn token => fn indices =>

From 60269d4a4b20564659ea8f9cf5e1aae5d35377e6 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Sun, 17 Mar 2024 11:38:58 +0000
Subject: [PATCH 23/27] HolSmt: don't get rid of `quot` and `rem` in arithmetic
 rules

It should not be necessary to rewrite these symbols with their
definitions, because from the perspective of SMT solvers, these should
just be functions like any others. Therefore, when replaying
arithmetic proof steps, the proof handler should not need to
understand what `quot` and `rem` are.

This is a partial revert of the following commit:
6220a17848fd58bcb54bb9df9df6b55d5859abf0

It's not clear to me why I introduced this change in the first place,
since the tests do work fine without it. Also, there doesn't seem to
be any performance regression.
---
 src/HolSmt/Z3_ProofReplay.sml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index e0195cc7d5..d6e06b5fd2 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -495,8 +495,7 @@ 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,
-             integerTheory.int_quot, integerTheory.int_rem]
+        >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT]
         (* if `arith_tactic` doesn't work at first, don't give up immediately;
            instead let's try additional tactics *)
         >> TRY arith_tactic

From 044e6ad05722891e60091c081261b1d9d8e1ada8 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Mon, 18 Mar 2024 15:28:46 +0000
Subject: [PATCH 24/27] HolSmt: parse `declare-const` commands

Add support for parsing `declare-const` commands to the SMT-LIB
parser.
---
 src/HolSmt/SmtLib_Parser.sml | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/HolSmt/SmtLib_Parser.sml b/src/HolSmt/SmtLib_Parser.sml
index 57fd2c3d48..adff7adf3a 100644
--- a/src/HolSmt/SmtLib_Parser.sml
+++ b/src/HolSmt/SmtLib_Parser.sml
@@ -451,10 +451,14 @@ local
   end
 
   (* returns an extended 'tmdict' *)
-  fun parse_declare_fun get_token (tydict, tmdict) =
+  fun parse_declare_const_fun parse_types get_token (tydict, tmdict) =
   let
     val name = get_token ()
-    val domain_types = parse_type_list get_token tydict
+    val domain_types =
+      if parse_types then
+        parse_type_list get_token tydict
+      else
+        []
     val range_type = parse_type get_token tydict
     val _ = Library.expect_token ")" (get_token ())
     val tm = Term.mk_var (name,
@@ -469,6 +473,9 @@ local
     (tm, Library.extend_dict ((name, parsefn), tmdict))
   end
 
+  val parse_declare_const = parse_declare_const_fun false
+  val parse_declare_fun = parse_declare_const_fun true
+
   (* returns an extended 'tmdict', and the definition (as a formula) *)
   fun parse_define_fun get_token (tydict, tmdict) =
   let
@@ -538,6 +545,13 @@ local
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
+    | "declare-const" =>
+      let
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-const"
+        val (_, tmdict) = parse_declare_const get_token (tydict, tmdict)
+      in
+        parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
+      end
     | "declare-fun" =>
       let
         val (logic, tydict, tmdict, asserted) = dest_state "declare-fun"

From ca44d4390ee1a69e0cd27db77a1825ba3af1b269 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Mon, 18 Mar 2024 17:16:41 +0000
Subject: [PATCH 25/27] HolSmt: handle end-of-stream when parsing SMT-LIB files

The SMT-LIB file parser was ending up raising an end-of-stream
exception unless the `(exit)` command was present in the SMT-LIB file,
even though the `(exit)` command does not seem to be mandatory
according to the SMT-LIB v2.6 standard.
---
 src/HolSmt/SmtLib_Parser.sml | 58 ++++++++++++++++++++++--------------
 1 file changed, 36 insertions(+), 22 deletions(-)

diff --git a/src/HolSmt/SmtLib_Parser.sml b/src/HolSmt/SmtLib_Parser.sml
index adff7adf3a..a8bf814f74 100644
--- a/src/HolSmt/SmtLib_Parser.sml
+++ b/src/HolSmt/SmtLib_Parser.sml
@@ -513,17 +513,20 @@ local
     (tmdict, definition)
   end
 
-  (* returns the logic's name, its 'tydict', its 'tmdict' extended with
-     declared function symbols, and a list of asserted formulas *)
-  fun parse_commands get_token state =
+  fun dest_state cmd (SOME x) = x
+    | dest_state cmd NONE     =
+        raise ERR "dest_state" ("received " ^ cmd ^ " before set-logic")
+
+  and finalize_state cmd state =
   let
-    fun dest_state cmd =
-      case state of
-        SOME x => x
-      | NONE   => raise ERR "parse_commands" (cmd ^ " issued before set-logic")
-    val _ = Library.expect_token "(" (get_token ())
-    val command = get_token ()
+    val (logic, tydict, tmdict, asserted) = dest_state cmd state
   in
+    (logic, tydict, tmdict, List.rev asserted)
+  end
+
+  (* returns the logic's name, its 'tydict', its 'tmdict' extended with
+     declared function symbols, and a list of asserted formulas *)
+  and parse_command command get_token state =
     case command of "set-info" =>
       let
         val _ = parse_set_info get_token
@@ -540,28 +543,28 @@ local
       end
     | "declare-sort" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "declare-sort"
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-sort" state
         val tydict = parse_declare_sort get_token tydict
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
     | "declare-const" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "declare-const"
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-const" state
         val (_, tmdict) = parse_declare_const get_token (tydict, tmdict)
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
     | "declare-fun" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "declare-fun"
+        val (logic, tydict, tmdict, asserted) = dest_state "declare-fun" state
         val (_, tmdict) = parse_declare_fun get_token (tydict, tmdict)
       in
         parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
       end
     | "define-fun" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "define-fun"
+        val (logic, tydict, tmdict, asserted) = dest_state "define-fun" state
         val (tmdict, def) = parse_define_fun get_token (tydict, tmdict)
         val asserted = def :: asserted
       in
@@ -569,7 +572,7 @@ local
       end
     | "assert" =>
       let
-        val (logic, tydict, tmdict, asserted) = dest_state "assert"
+        val (logic, tydict, tmdict, asserted) = dest_state "assert" state
         val asserted = parse_term get_token (tydict, tmdict) :: asserted
         val _ = Library.expect_token ")" (get_token ())
       in
@@ -577,27 +580,38 @@ local
       end
     | "check-sat" =>
       let
-        val _ = dest_state "check-sat"
+        val _ = dest_state "check-sat" state
         val _ = Library.expect_token ")" (get_token ())
       in
         parse_commands get_token state
       end
     | "get-proof" =>
       let
-        val _ = dest_state "get-proof"
+        val _ = dest_state "get-proof" state
         val _ = Library.expect_token ")" (get_token ())
       in
         parse_commands get_token state
       end
     | "exit" =>
-      let
-        val (logic, tydict, tmdict, asserted) = dest_state "exit"
-        val _ = Library.expect_token ")" (get_token ())
-      in
-        (logic, tydict, tmdict, List.rev asserted)
-      end
+      finalize_state "exit" state
+        before Library.expect_token ")" (get_token ())
     | _ =>
       raise ERR "parse_commands" ("unknown command '" ^ command ^ "'")
+
+  (* returns the logic's name, its 'tydict', its 'tmdict' extended with
+     declared function symbols, and a list of asserted formulas *)
+  and parse_commands get_token state =
+  let
+    val tok = SOME (get_token ())
+      (* assume an error to be end-of-stream *)
+      handle _ => NONE
+  in
+    case tok of
+      NONE => finalize_state "(end-of-stream)" state
+    | SOME t => (
+        Library.expect_token "(" t;
+        parse_command (get_token ()) get_token state
+      )
   end
 
   (* entry point into the parser (i.e., the grammar's start symbol) *)

From 5cbe069db7cb74b1af658226afe4a5cfae44c4d4 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Mon, 18 Mar 2024 17:37:50 +0000
Subject: [PATCH 26/27] HolSmt: parse `assign-bounds` index in arith rules

This commit fixes a parsing error when parsing arithmetic `th-lemma`
inference rules with an `assign-bounds` parameter, i.e.:

((_ th-lemma arith assign-bounds ...) ...)

The error was due to `assign-bounds` not being in the known term
dictionary.
---
 src/HolSmt/Z3_ProofParser.sml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/HolSmt/Z3_ProofParser.sml b/src/HolSmt/Z3_ProofParser.sml
index ac816d75cf..d6bde2f3ab 100644
--- a/src/HolSmt/Z3_ProofParser.sml
+++ b/src/HolSmt/Z3_ProofParser.sml
@@ -111,6 +111,8 @@ local
     ("and-elim",        one_prem "and-elim"),
     (* the following is used in `(_ th-lemma arith ...)` inference rules *)
     ("arith",           builtin_name "arith"),
+    (* the following is used in `(_ th-lemma arith ...)` inference rules *)
+    ("assign-bounds",   builtin_name "assign-bounds"),
     (* the following is used in `(_ th-lemma bv ...)` inference rules *)
     ("bv",              builtin_name "bv"),
     ("asserted",        zero_prems "asserted"),

From d8c49f8115c2259fca2b7f8b3409faf598d6fabe Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Sat, 23 Mar 2024 19:58:36 +0000
Subject: [PATCH 27/27] HolSmt: remove workaround for #1203

Now that all known issues were fixed wrt. ARITH_PROVE not proving
goals that COOPER_PROVE could, we can remove this workaround, thus
making proof replay faster in some cases.
---
 src/HolSmt/Z3_ProofReplay.sml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index d6e06b5fd2..6b2794e025 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -477,13 +477,8 @@ local
              term that contains type real is provable by integer
              arithmetic *)
           profile "arith_prove(real)" RealField.REAL_ARITH_TAC goal
-        else (
+        else
           profile "arith_prove(int)" intLib.ARITH_TAC goal
-          (* the following exception handler is a workaround for this issue:
-             https://github.com/HOL-Theorem-Prover/HOL/issues/1203 *)
-          handle Feedback.HOL_ERR _ =>
-            profile "arith_prove(cooper)" intLib.COOPER_TAC goal
-        )
       val TRY = Tactical.TRY
       val ap_tactic =
         TRY AP_TERM_TAC >> TRY arith_tactic