[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Arity of NEW operator in tlapm

I am trying to prove that the image of a finite set under an operator is finite (relevant to ),
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(_) .

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
============================================================================

 https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/library/FiniteSetTheorems.tla#L108

Best regards,
ioannis