Added a proof-checking interface to the Cadical SAT solver

(https://github.com/arminbiere/cadical). This is highly analogous to
the existing interfaces to Minisat and zchaff in "Minisat/*" and uses
some very similar code for CNF transformation. Among other facilities,
this makes available a Cadical-powered tautology checker, with the
LRAT proof produced by Cadical (it is tidied up with lrat-trim in the
standard flow) checked in the HOL Light kernel. For example:

  # CADICAL_PROVE `(p ==> q) <=> (p <=> p /\ q)`;;
  val it : thm = |- p ==> q <=> p <=> p /\ q

Added a proof that a polygon with all its vertices on the unit circle
is closed under complex multiplication iff the vertices are the n'th
complex roots of unity for some n. This is based on the discussion
here, in particular the observation from Dario extending Carl
Schildkraut's proof of the original problem to an equivalence:

  https://math.stackexchange.com/questions/4892153

Fixed a printer bug where interface maps were not reversed on printing
for binders. Also made a few minor name changes in the embedded logics
to avoid using "true" and "false", to make room for using those as
alternative names for T and F.

Made a few useful improvements to SET_TAC and SET_RULE. First of all,
they now deal with conditionals at least to some extent (the previous
failure to do so was a basic bug). They also use streamlined versions
of certain "write away set concepts" rules such as UNIONS_GSPEC, which
can be helpful preprocessing to make the eventual MESON problem
easier, or even provable at all. Here are a couple of trivial examples
that now work but didn't previously:

  SET_RULE `IMAGE (f:A->B) s = UNIONS {{f x} | x IN s}`;;

  SET_RULE `{a,b} DELETE (a:A) = if a = b then {} else {b}`;;

Made a few tiny optimizations to basic rules like CONJUNCT1 by
switching the implementation from PROVE_HYP to the underlying
primitive rules DEDUCT_ANTISYM_RULE and EQ_MP. This has the advantage
of skipping a check that in context we know is redundant (whether the
PROVE_HYP is non-trivial in the sense that the assumption is not there
to start with).

Added a few new theorems (mainly in support of the polygon example
above):

        BILINEAR_IN_AFFINE_HULL
        BILINEAR_IN_CONVEX_HULL
        FINITE_SUBGROUP_OF_SETWISE
        SIMPLEX_FURTHEST_LT_EXISTS

as well as generalizing these two existing theorems by removing the
finiteness assumption (hence perhaps making the "SIMPLEX" in the name
a bit misleading):

        SIMPLEX_FURTHEST_LT
        SIMPLEX_FURTHEST_LE_EXISTS

Arithmetic/arithprov.ml

@@ -563,7 +563,7 @@ let PROV_DEFINABLE = prove
 (* ------------------------------------------------------------------------- *)
 
 let GODEL_CRUDE = prove
- (`!Ax. definable {gform p | p IN Ax} ==> ?p. ~(true p <=> Ax |-- p)`,
+ (`!Ax. definable {gform p | p IN Ax} ==> ?p. ~(arithtrue p <=> Ax |-- p)`,
  REPEAT STRIP_TAC THEN MP_TAC TARSKI_THEOREM THEN
  FIRST_X_ASSUM(MP_TAC o MATCH_MP PROV_DEFINABLE) THEN
  MATCH_MP_TAC(TAUT `(~c ==> (a <=> b)) ==> a ==> ~b ==> c`) THEN

Arithmetic/fol.ml

@@ -87,8 +87,8 @@ let holds = new_recursive_definition form_RECURSION
  (holds v (!! x p) <=> !a. holds ((x|->a) v) p) /\
  (holds v (?? x p) <=> ?a. holds ((x|->a) v) p)`;;
 
-let true_def = new_definition
- `true p <=> !v. holds v p`;;
+let arithtrue = new_definition
+ `arithtrue p <=> !v. holds v p`;;
 
 let VALMOD = prove
  (`!v x y a. ((x |-> y) v) a = if a = x then y else v(a)`,
@@ -245,9 +245,9 @@ let HOLDS_VALMOD_OTHER = prove
 (* ------------------------------------------------------------------------- *)
 
 let AXIOMS_TRUE = prove
- (`!p. axiom p ==> true p`,
+ (`!p. axiom p ==> arithtrue p`,
  MATCH_MP_TAC axiom_INDUCT THEN
- REWRITE_TAC[true_def] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[holds] THENL
+ REWRITE_TAC[arithtrue] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[holds] THENL
  [CONV_TAC TAUT;
  CONV_TAC TAUT;
  SIMP_TAC[];
@@ -275,12 +275,12 @@ let AXIOMS_TRUE = prove
  MESON_TAC[]]);;
 
 let THEOREMS_TRUE = prove
- (`!A p. (!q. q IN A ==> true q) /\ A |-- p ==> true p`,
+ (`!A p. (!q. q IN A ==> arithtrue q) /\ A |-- p ==> arithtrue p`,
  GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  DISCH_TAC THEN MATCH_MP_TAC proves_INDUCT THEN
  ASM_SIMP_TAC[TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN
  REWRITE_TAC[IN; AXIOMS_TRUE] THEN
- SIMP_TAC[holds; true_def]);;
+ SIMP_TAC[holds; arithtrue]);;
 
 (* ------------------------------------------------------------------------- *)
 (* Variant variables for use in renaming substitution. *)

Arithmetic/godel.ml

@@ -405,7 +405,7 @@ let HSENTENCE_FIX_STRONG = prove
  (`!A Arep.
  (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
  ==> !v. holds v (hsentence Arep) <=> A |-- Not(hsentence Arep)`,
- REWRITE_TAC[hsentence; true_def; HOLDS_FIXPOINT] THEN
+ REWRITE_TAC[hsentence; arithtrue; HOLDS_FIXPOINT] THEN
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP ARITH_PROV) THEN
  REWRITE_TAC[IN] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
@@ -415,14 +415,14 @@ let HSENTENCE_FIX_STRONG = prove
 let HSENTENCE_FIX = prove
  (`!A Arep.
  (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
- ==> (true(hsentence Arep) <=> A |-- Not(hsentence Arep))`,
- REWRITE_TAC[true_def] THEN MESON_TAC[HSENTENCE_FIX_STRONG]);;
+ ==> (arithtrue(hsentence Arep) <=> A |-- Not(hsentence Arep))`,
+ REWRITE_TAC[arithtrue] THEN MESON_TAC[HSENTENCE_FIX_STRONG]);;
 
 let GSENTENCE_FIX = prove
  (`!A Arep.
  (!v t. holds v (Arep t) <=> (termval v t) IN IMAGE gform A)
- ==> (true(gsentence Arep) <=> ~(A |-- gsentence Arep))`,
- REWRITE_TAC[true_def; holds; gsentence] THEN
+ ==> (arithtrue(gsentence Arep) <=> ~(A |-- gsentence Arep))`,
+ REWRITE_TAC[arithtrue; holds; gsentence] THEN
  MESON_TAC[HSENTENCE_FIX_STRONG]);;
 
 (* ------------------------------------------------------------------------- *)
@@ -433,10 +433,10 @@ let ground = new_definition
  `ground t <=> (FVT t = {})`;;
 
 let complete_for = new_definition
- `complete_for P A <=> !p. P p /\ true p ==> A |-- p`;;
+ `complete_for P A <=> !p. P p /\ arithtrue p ==> A |-- p`;;
 
 let sound_for = new_definition
- `sound_for P A <=> !p. P p /\ A |-- p ==> true p`;;
+ `sound_for P A <=> !p. P p /\ A |-- p ==> arithtrue p`;;
 
 let consistent = new_definition
  `consistent A <=> ~(?p. A |-- p /\ A |-- Not p)`;;
@@ -463,14 +463,14 @@ let DEFINABLE_BY_ONEVAR = prove
  MESON_TAC[]);;
 
 let CLOSED_NOT_TRUE = prove
- (`!p. closed p ==> (true(Not p) <=> ~(true p))`,
- REWRITE_TAC[closed; true_def; holds] THEN
+ (`!p. closed p ==> (arithtrue(Not p) <=> ~(arithtrue p))`,
+ REWRITE_TAC[closed; arithtrue; holds] THEN
  MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
 
 let G1 = prove
  (`!A. definable_by (SIGMA 1) (IMAGE gform A)
  ==> ?G. PI 1 G /\ closed G /\
- (sound_for (PI 1 INTER closed) A ==> true G /\ ~(A |-- G)) /\
+ (sound_for (PI 1 INTER closed) A ==> arithtrue G /\ ~(A |-- G)) /\
  (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
  GEN_TAC THEN
  REWRITE_TAC[sound_for; INTER; IN_ELIM_THM; DEFINABLE_BY_ONEVAR] THEN
@@ -493,14 +493,14 @@ let G1 = prove
  ALL_TAC] THEN
  ABBREV_TAC `G = gsentence (\t. formsubst ((a |-> t) V) Arep)` THEN
  REPEAT STRIP_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
- SUBGOAL_THEN `true(Not G)` MP_TAC THENL
+ SUBGOAL_THEN `arithtrue(Not G)` MP_TAC THENL
  [FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[IN] THEN
  REWRITE_TAC[SIGMA; SIGMAPI_CLAUSES] THEN ASM_MESON_TAC[closed; FV; PI];
  ALL_TAC] THEN
  FIRST_ASSUM(SUBST1_TAC o MATCH_MP CLOSED_NOT_TRUE) THEN
  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
- SUBGOAL_THEN `true False` MP_TAC THENL
- [ALL_TAC; REWRITE_TAC[true_def; holds]] THEN
+ SUBGOAL_THEN `arithtrue False` MP_TAC THENL
+ [ALL_TAC; REWRITE_TAC[arithtrue; holds]] THEN
  FIRST_X_ASSUM MATCH_MP_TAC THEN
  REWRITE_TAC[closed; IN; SIGMA; SIGMAPI_CLAUSES; FV] THEN
  ASM_MESON_TAC[CONSISTENT_ALT]);;
@@ -517,14 +517,14 @@ let COMPLETE_SOUND_SENTENCE = prove
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(fun th -> X_GEN_TAC `p:form` THEN MP_TAC(SPEC `Not p` th)) THEN
  REWRITE_TAC[SIGMAPI_CLAUSES] THEN
- REWRITE_TAC[closed; FV; true_def; holds] THEN
+ REWRITE_TAC[closed; FV; arithtrue; holds] THEN
  ASM_MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
 
 let G1_TRAD = prove
  (`!A. consistent A /\
  complete_for (SIGMA 1 INTER closed) A /\
  definable_by (SIGMA 1) (IMAGE gform A)
- ==> ?G. PI 1 G /\ closed G /\ true G /\ ~(A |-- G) /\
+ ==> ?G. PI 1 G /\ closed G /\ arithtrue G /\ ~(A |-- G) /\
  (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
  REWRITE_TAC[SIGMA] THEN REPEAT STRIP_TAC THEN
  MP_TAC(SPEC `A:form->bool` G1) THEN ASM_REWRITE_TAC[SIGMA; PI] THEN

Arithmetic/pa.ml

@@ -1,5 +1,5 @@
 (* ========================================================================= *)
-(* Two interesting axiom systems: full Peano Arithmetic and Robinson's Q. *)
+(* The full Peano arithmetic axiom system.  *)
 (* ========================================================================= *)
 
 (* ------------------------------------------------------------------------- *)
@@ -12,30 +12,34 @@
 (* ------------------------------------------------------------------------- *)
 
 let PA_RULES,PA_INDUCT,PA_CASES = new_inductive_definition
- `(!s. PA(Not (Z === Suc(s)))) /\
- (!s t. PA(Suc(s) === Suc(t) --> s === t)) /\
- (!t. PA(t ++ Z === t)) /\
- (!s t. PA(s ++ Suc(t) === Suc(s ++ t))) /\
- (!t. PA(t ** Z === Z)) /\
- (!s t. PA(s ** Suc(t) === s ** t ++ s)) /\
- (!p i j. ~(j IN FV(p))
+ `PA(!!1 (Not (Z === Suc(V 1)))) /\
+ PA(!!0 (!!1 (Suc(V 0) === Suc(V 1) --> V 0 === V 1))) /\
+ PA(!!1 (V 1 ++ Z === V 1)) /\
+ PA(!!0 (!!1 (V 0 ++ Suc(V 1) === Suc(V 0 ++ V 1)))) /\
+ PA(!!1 (V 1 ** Z === Z)) /\
+ PA(!!0 (!!1 (V 0 ** Suc(V 1) === V 0 ** V 1 ++ V 0))) /\
+ PA(!!0 (!!1 (V 0 <<= V 1 <-> ??2 (V 0 ++ V 2 === V 1)))) /\
+ PA(!!0 (!!1 (V 0 << V 1 <-> Suc(V 0) <<= V 1))) /\
+ (!i j p. ~(j IN FV(p))
  ==> PA
  ((??i (V i === Z && p)) &&
  (!!j (??i (V i === V j && p)
  --> ??i (V i === Suc(V j) && p)))
  --> !!i p))`;;
 
 let PA_SOUND = prove
- (`!A p. (!a. a IN A ==> true a) /\ (PA UNION A) |-- p ==> true p`,
+ (`!A p. (!a. a IN A ==> arithtrue a) /\ (PA UNION A) |-- p ==> arithtrue p`,
  REPEAT STRIP_TAC THEN MATCH_MP_TAC THEOREMS_TRUE THEN
  EXISTS_TAC `PA UNION A` THEN
  ASM_SIMP_TAC[IN_UNION; TAUT `(a \/ b ==> c) <=> (a ==> c) /\ (b ==> c)`] THEN
  REWRITE_TAC[IN] THEN MATCH_MP_TAC PA_INDUCT THEN
- REWRITE_TAC[true_def; holds; termval] THEN
+ REWRITE_TAC[arithtrue; holds; termval] THEN
  REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
- [SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; EXP; SUC_INJ; NOT_SUC] THEN ARITH_TAC;
+ [SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; EXP; SUC_INJ; NOT_SUC; valmod;
+ ARITH_EQ; MESON[LE_EXISTS] `(?d. m + d = n) <=> m <= n`] THEN
+ ARITH_TAC;
  ALL_TAC] THEN
- MAP_EVERY X_GEN_TAC [`q:form`; `i:num`; `j:num`] THEN
+ MAP_EVERY X_GEN_TAC [`i:num`; `j:num`; `q:form`] THEN
  ASM_CASES_TAC `j:num = i` THEN
  ASM_REWRITE_TAC[VALMOD; VALMOD_VALMOD_BASIC] THEN
  SIMP_TAC[HOLDS_VALMOD_OTHER] THENL [MESON_TAC[]; ALL_TAC] THEN
@@ -47,27 +51,3 @@ let PA_SOUND = prove
  [REPEAT STRIP_TAC THEN MATCH_MP_TAC HOLDS_VALUATION THEN
  ASM_REWRITE_TAC[valmod] THEN ASM_MESON_TAC[];
  GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[]]);;
-
-(* ------------------------------------------------------------------------- *)
-(* Robinson's axiom system Q. *)
-(* *)
-(* <<(forall m n. S(m) = S(n) ==> m = n) /\ *)
-(* (forall n. ~(n = 0) <=> exists m. n = S(m)) /\ *)
-(* (forall n. 0 + n = n) /\ *)
-(* (forall m n. S(m) + n = S(m + n)) /\ *)
-(* (forall n. 0 * n = 0) /\ *)
-(* (forall m n. S(m) * n = n + m * n) /\ *)
-(* (forall m n. m <= n <=> exists d. m + d = n) /\ *)
-(* (forall m n. m < n <=> S(m) <= n)>>;; *)
-(* ------------------------------------------------------------------------- *)
-
-let robinson = new_definition
- `robinson =
- (!!0 (!!1 (Suc(V 0) === Suc(V 1) --> V 0 === V 1))) &&
- (!!1 (Not(V 1 === Z) <-> ??0 (V 1 === Suc(V 0)))) &&
- (!!1 (Z ++ V 1 === V 1)) &&
- (!!0 (!!1 (Suc(V 0) ++ V 1 === Suc(V 0 ++ V 1)))) &&
- (!!1 (Z ** V 1 === Z)) &&
- (!!0 (!!1 (Suc(V 0) ** V 1 === V 1 ++ V 0 ** V 1))) &&
- (!!0 (!!1 (V 0 <<= V 1 <-> ??2 (V 0 ++ V 2 === V 1)))) &&
- (!!0 (!!1 (V 0 << V 1 <-> Suc(V 0) <<= V 1)))`;;

Arithmetic/sigmacomplete.ml

@@ -572,12 +572,12 @@ let G1_ROBINSON = prove
  consistent A /\ A |-- robinson
  ==> ?G. PI 1 G /\
  closed G /\
- true G /\
+ arithtrue G /\
  ~(A |-- G) /\
  (sound_for (SIGMA 1 INTER closed) A ==> ~(A |-- Not G))`,
  REPEAT STRIP_TAC THEN MATCH_MP_TAC G1_TRAD THEN
  ASM_REWRITE_TAC[complete_for; INTER; IN_ELIM_THM] THEN
- X_GEN_TAC `p:form` THEN REWRITE_TAC[IN; true_def] THEN STRIP_TAC THEN
+ X_GEN_TAC `p:form` THEN REWRITE_TAC[IN; arithtrue] THEN STRIP_TAC THEN
  MATCH_MP_TAC modusponens THEN EXISTS_TAC `robinson` THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC PROVES_MONO THEN
  EXISTS_TAC `{}:form->bool` THEN REWRITE_TAC[EMPTY_SUBSET] THEN
@@ -595,10 +595,10 @@ let complete = new_definition
  `complete A <=> !p. closed p ==> A |-- p \/ A |-- Not p`;;
 
 let sound = new_definition
- `sound A <=> !p. A |-- p ==> true p`;;
+ `sound A <=> !p. A |-- p ==> arithtrue p`;;
 
 let semcomplete = new_definition
- `semcomplete A <=> !p. true p ==> A |-- p`;;
+ `semcomplete A <=> !p. arithtrue p ==> A |-- p`;;
 
 let generalize = new_definition
  `generalize vs p = ITLIST (!!) vs p`;;
@@ -607,8 +607,8 @@ let closure = new_definition
  `closure p = generalize (list_of_set(FV p)) p`;;
 
 let TRUE_GENERALIZE = prove
- (`!vs p. true(generalize vs p) <=> true p`,
- REWRITE_TAC[generalize; true_def] THEN
+ (`!vs p. arithtrue(generalize vs p) <=> arithtrue p`,
+ REWRITE_TAC[generalize; arithtrue] THEN
  LIST_INDUCT_TAC THEN REWRITE_TAC[ITLIST; holds] THEN GEN_TAC THEN
  FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [GSYM th]) THEN
  MESON_TAC[VALMOD_REPEAT]);;
@@ -631,7 +631,7 @@ let CLOSED_CLOSURE = prove
  SIMP_TAC[SET_OF_LIST_OF_SET; FV_FINITE; DIFF_EQ_EMPTY]);;
 
 let TRUE_CLOSURE = prove
- (`!p. true(closure p) <=> true p`,
+ (`!p. arithtrue(closure p) <=> arithtrue p`,
  REWRITE_TAC[closure; TRUE_GENERALIZE]);;
 
 let PROVABLE_CLOSURE = prove
@@ -654,24 +654,24 @@ let DEFINABLE_ONEVAR = prove
  MESON_TAC[]);;
 
 let CLOSED_TRUE_OR_FALSE = prove
- (`!p. closed p ==> true p \/ true(Not p)`,
- REWRITE_TAC[closed; true_def; holds] THEN REPEAT STRIP_TAC THEN
+ (`!p. closed p ==> arithtrue p \/ arithtrue(Not p)`,
+ REWRITE_TAC[closed; arithtrue; holds] THEN REPEAT STRIP_TAC THEN
  ASM_MESON_TAC[HOLDS_VALUATION; NOT_IN_EMPTY]);;
 
 let SEMCOMPLETE_IMP_COMPLETE = prove
  (`!A. semcomplete A ==> complete A`,
  REWRITE_TAC[semcomplete; complete] THEN MESON_TAC[CLOSED_TRUE_OR_FALSE]);;
 
 let SOUND_CLOSED = prove
- (`sound A <=> !p. closed p /\ A |-- p ==> true p`,
+ (`sound A <=> !p. closed p /\ A |-- p ==> arithtrue p`,
  REWRITE_TAC[sound] THEN EQ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
  MESON_TAC[TRUE_CLOSURE; PROVABLE_CLOSURE; CLOSED_CLOSURE]);;
 
 let SOUND_IMP_CONSISTENT = prove
  (`!A. sound A ==> consistent A`,
  REWRITE_TAC[sound; consistent; CONSISTENT_ALT] THEN
- SUBGOAL_THEN `~(true False)` (fun th -> MESON_TAC[th]) THEN
- REWRITE_TAC[true_def; holds]);;
+ SUBGOAL_THEN `~(arithtrue False)` (fun th -> MESON_TAC[th]) THEN
+ REWRITE_TAC[arithtrue; holds]);;
 
 let SEMCOMPLETE_SOUND_EQ_CONSISTENT = prove
  (`!A. semcomplete A ==> (sound A <=> consistent A)`,

Arithmetic/tarski.ml

@@ -319,9 +319,9 @@ let HOLDS_IFF_FIXPOINT = prove
 
 let CARNAP = prove
  (`!x q. ?p. (FV(p) = FV(q) DELETE x) /\
- true (p <-> qsubst (x,numeral(gform p)) q)`,
+ arithtrue (p <-> qsubst (x,numeral(gform p)) q)`,
  REPEAT GEN_TAC THEN EXISTS_TAC `fixpoint x q` THEN
- REWRITE_TAC[true_def; HOLDS_IFF_FIXPOINT; FV_FIXPOINT]);;
+ REWRITE_TAC[arithtrue; HOLDS_IFF_FIXPOINT; FV_FIXPOINT]);;
 
 (* ------------------------------------------------------------------------- *)
 (* Hence Tarski's theorem on the undefinability of truth. *)
@@ -334,11 +334,11 @@ let definable = new_definition
  `definable s <=> ?p x. !v. holds v p <=> (v(x)) IN s`;;
 
 let TARSKI_THEOREM = prove
- (`~(definable {gform p | true p})`,
+ (`~(definable {gform p | arithtrue p})`,
  REWRITE_TAC[definable; IN_ELIM_THM; NOT_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`p:form`; `x:num`] THEN DISCH_TAC THEN
  MP_TAC(SPECL [`x:num`; `Not p`] CARNAP) THEN
  DISCH_THEN(X_CHOOSE_THEN `q:form` (MP_TAC o CONJUNCT2)) THEN
- SIMP_TAC[true_def; holds; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY] THEN
+ SIMP_TAC[arithtrue; holds; HOLDS_QSUBST; FVT_NUMERAL; NOT_IN_EMPTY] THEN
  ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[VALMOD_BASIC; TERMVAL_NUMERAL] THEN
- REWRITE_TAC[true_def; GFORM_INJ] THEN MESON_TAC[]);;
+ REWRITE_TAC[arithtrue; GFORM_INJ] THEN MESON_TAC[]);;