Isabelle rejects a proof found by Zenon

[johnyf]

Isabelle rejects a proof found by Zenon for a theorem that admits another proof that Isabelle accepts. The following two modules demonstrate this issue.

--------------------------------- MODULE test4 ---------------------------------
(* Zenon proves this theorem, but Isabelle rejects the proof. *)

Support(R) == { p[1]:  p \in DOMAIN R } \cup { p[2]:  p \in DOMAIN R }

THEOREM
    ASSUME
        NEW R,
        \E S:  (S \X S) = (DOMAIN R)
    PROVE
        LET T == Support(R)
        IN (DOMAIN R) = (T \X T)
    BY DEF Support

================================================================================

-------------------------------- MODULE test5 ----------------------------------
(* Isabelle successfully checks this proof of the same theorem. *)

Support(R) == { p[1]:  p \in DOMAIN R } \cup { p[2]:  p \in DOMAIN R }

THEOREM
    ASSUME
        NEW R,
        \E S:  (S \X S) = (DOMAIN R)
    PROVE
        LET T == Support(R)
        IN (DOMAIN R) = (T \X T)
    <1> DEFINE T == Support(R)
    <1>1. PICK S:  (DOMAIN R) = (S \X S)
        OBVIOUS
    <1>2. SUFFICES T = S
        BY <1>1
    <1>3. T \subseteq S
        BY <1>1 DEF Support
    <1>4. S \subseteq T
        <3> SUFFICES ASSUME NEW u \in S
                     PROVE u \in T
            OBVIOUS
        <3> QED
            BY <1>1 DEF Support
    <1> QED
        BY <1>3, <1>4

================================================================================

The tail of output from tlapm -v -C test4.tla is:

(* trying obligation 1 generated from file "./test4.tla", line 12, characters 5-6 *)
(* ... using SMT(v3) *)
>>> Type assignments:
  R : (Tuple_[*;*] -> *)
  sk_S : Set(*)
>>> Unexpanded operators: ---

launching process: "file=test4.tlaps/tlapm_bcba2d.smt; PATH="${PATH}:/some/path/tlaps/bin"; cvc3 -lang smt2 "$file" >test4.tlaps/tlapm_bcba2d.smt.out"
(* ... using zenon version [253] (timeout: 10.000000s) *)
launching process: "file=test4.tlaps/tlapm_86a0c8.znn; PATH="${PATH}:/some/path/tlaps/bin"; zenon -p0 -x tla -oisar -max-time 1d "$file" >test4.tlaps/tlapm_86a0c8.znn.out"
(* created new "test4.tlaps/test4.thy" *)
(* fingerprints written in "test4.tlaps/fingerprints" *)
Checking the proofs with Isabelle. This may take a long time.
(* Isabelle interaction log in "test4.tlaps/isabelle.log" *)
(* Isabelle parsing "test4.tlaps/test4.thy" ... done *)
(* Obligation checking trace follows. *)
(* +1 *)
Isabelle/TLA+ rejected the proof of obligation 1.
See "test4.tlaps/isabelle.log" for details.

Part of isabelle.log is:

*** TLAPS ENTER 1

*** Failed to finish proof

*** At command "by" (line 78 of "/some/path/test4.tlaps/test4.thy")

Exception- TOPLEVEL_ERROR raised

Line 78 of test4.thy is:

have z_Hca: "(?z_hcb=?z_hs)" using z_Hbw by clarsimp

Environment:

>>> tlapm --version
1.4.3 (build 34695)

>>> zenon -v
zenon version 0.7.2 [a253] 2013-03-04

>>> cvc3 -version
This is CVC3 version 2.4.1

>>> isabelle version
Isabelle2011-1: October 2011

>>> lsb_release -a
Description:    Debian GNU/Linux 9.0 (stretch)

Other tools (Z3, Spass, ls4) are present, but from what I understand they are irrelevant in this case.

For completeness, the tail of output from tlapm -v C test5.tla (the successfully checked proof) is:

(* created new "test5.tlaps/test5.thy" *)
(* fingerprints written in "test5.tlaps/fingerprints" *)
Checking the proofs with Isabelle. This may take a long time.
(* Isabelle interaction log in "test5.tlaps/isabelle.log" *)
(* Isabelle parsing "test5.tlaps/test5.thy" ... done *)
(* Obligation checking trace follows. *)
(* +1 +9 +4 -4 -1 -9 *)
Proof checking done. No errors found.