Another case where Isabelle rejects a proof

[johnyf]

Somewhat similar to #5, though not sure whether due to the same cause. Isabelle rejects the proof of the theorem in module test4, but accepts the proof for the same theorem in module test5.

--------------------------------- MODULE test4 ---------------------------------
(* A proof is found, but Isabelle rejects it. *)

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

THEOREM
    ASSUME
        NEW Foo,
        \A x \in Support(Foo):  Foo[x, x]
    PROVE
        LET
            R == Support(Foo)
            Bar == [t \in R \X R |-> Foo[t[1], t[2]]]
        IN
            \A x \in Support(Bar):  Bar[x, x]
    <1> DEFINE
        R == Support(Foo)
        Bar == [t \in R \X R |-> Foo[t[1], t[2]]]
        Q == Support(Bar)
    <1>1. Q = R
        OMITTED  (* Can be proved, but omitted here for brevity. *)
    <1> QED
        BY <1>1

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

In this case isabelle.log reads

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

and line 124 in test4.thy is:

show FALSE using z_Hcg z_Hci z_Hck z_Hcr z_Hcz by auto

In contrast:

-------------------------------- 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 Foo,
        \A x \in Support(Foo):  Foo[x, x]
    PROVE
        LET
            R == Support(Foo)
            Bar == [t \in R \X R |-> Foo[t[1], t[2]]]
        IN
            \A x \in Support(Bar):  Bar[x, x]
    <1> DEFINE
        R == Support(Foo)
        Bar == [t \in R \X R |-> Foo[t[1], t[2]]]
        Q == Support(Bar)
    <1> HIDE DEF Bar
    <1>1. Q = R
        OMITTED
    <1> QED
        <2>1. SUFFICES ASSUME NEW x \in Q
                       PROVE Bar[x, x]
            BY DEF Bar
        <2>2. x \in R
            BY <1>1, <2>1
        <2>3. << x, x >> \in R \X R
            BY <2>2
        <2>4. Bar[ << x, x >> ] = Foo[ << x, x >> ]
            BY <1>1, <2>3 DEF Bar
        <2>5. Foo[ << x, x >> ]
            BY <2>2
        <2> QED
            BY <2>4, <2>5

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

In module test5, if <1> HIDE DEF Bar is removed, then Isabelle rejects the proof of step <2>3. << x, x >> \in R \X R.