Arity of NEW operator in `tlapm`

[Ioannis Filippidis <jfili...@xxxxxxxxx>]

I am trying to prove that the image of a finite set under an operator is finite (relevant to [1]),

to reuse it at multiple places. If I write a proof similar to that of `ImageOfFinite` below
for some specific operator `Op`, for example:

<2> DEFINE

    Op(u, a, b) == u

    f == [u \in S |-> Op(u, arg1, arg2)]
<2>1. f \in Surjection(S, H)
    BY DEF Surjection, Hdef
<2> QED
    BY <2>1, ..., FS_Surjection

then `tlapm -v -C` proves it, and I don't see any intermediate errors (using version 1.4.3).

`tlapm` proves correct also the module `test2` below, but with an error from the SMT backend (see below),

which can probably be ignored, because only the Isabelle backend supports the declaration `NEW Op(_)` [2].

However, if I change the assumption to `NEW Op(_, _)` in `ImageOfFinite`,
or the operator application to `Op(x)` in `ImageOfFinite2`,
then the proof is again successful, but SANY detects the errors.

Question 1: If SANY detects no errors and `tlapm` proves module `test2` correct,

should I assume that the arity of operator declarations as those in module `test2`

has been taken into account correctly?

Question 2: Is there an approach simpler/better than a couple of theorems for different arities to

prove that `IsFiniteSet(S)` implies `IsFiniteSet( { Op(x, ...):  x \in S } )`

as a theorem that we can reuse?

Sidenote: To invoke `ImageOfFinite3` successfully, I had to hide the definition of `S`,

but at least I didn't rewrite a proof like that of `ImageOfFinite`.

```
*** Fatal exception:
Type Checking error: Expected function type for:

a_Opunde_1a

 but got this: u

 in function application:

(_APPLY {a_Opunde_1a} x)
test2.tlaps/tlapm_d7953c.smt:50: this is the location of the error

...

Checking the proofs with Isabelle. This may take a long time.
(* Isabelle interaction log in "test2.tlaps/isabelle.log" *)
(* Isabelle parsing "test2.tlaps/test2.thy" ... done *)
(* Obligation checking trace follows. *)
(* +5 -5 +7 -7 *)
Proof checking done. No errors found.
```


------------------------------- MODULE test2 --------------------------------
LEMMA ImageOfFinite ==
    ASSUME
        NEW S, NEW Op(_),
        IsFiniteSet(S)
    PROVE
        LET
            Img == { Op(x):  x \in S }
        IN
            /\ IsFiniteSet(Img)
            /\ Cardinality(Img) <= Cardinality(S)
    <1> DEFINE
        Img == { Op(x):  x \in S }
        f == [x \in S |-> Op(x)]
    <1>1. f \in Surjection(S, Img)
        BY DEF Surjection
    <1> QED
        BY <1>1, FS_Surjection

COROLLARY ImageOfFinite2 ==
    ASSUME
        NEW S, NEW arg2, NEW Op(_, _),
        IsFiniteSet(S)
    PROVE
        LET
            Img == { Op(x, arg2):  x \in S }
        IN
            /\ IsFiniteSet(Img)
            /\ Cardinality(Img) <= Cardinality(S)
    BY ImageOfFinite

COROLLARY ImageOfFinite3 ==
    ASSUME
        NEW S, NEW arg2, NEW arg3, NEW Op(_, _, _),
        IsFiniteSet(S)
    PROVE
        LET
            Img == { Op(x, arg2, arg3):  x \in S }
        IN
            /\ IsFiniteSet(Img)
            /\ Cardinality(Img) <= Cardinality(S)
    BY ImageOfFinite
============================================================================

[1] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/library/FiniteSetTheorems.tla#L108
[2] http://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html

Best regards,

ioannis