[isabelle] Problems with Logic.mk_implies + compose_tac



Dear all,

I am having a bit of problems using 'compose_tac' with an intermediate
theorem (produced with mk_implies + Goal.prove). I hope you do not mind
if I ask for a hint.


Here is the problematic example:

I have this subgoal (call it sg1):

        ⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A; s1 ∈ B; s2 ∈ A; s2 ∉ B⟧ ⟹
        ∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B

Then an external tool is invoked, which returns another goal (call it
sg2):

        ⋀s1 s2. ⟦distinct[s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧ ⟹ (∃s1 s2.
        distinct[s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B)

I want to 'replace' the current subgoal sg1 with sg2. Therefore I make a
meta-implication and prove it with 'Goal.prove':

        val intert = Logic.mk_implies (sg2, sg1)
        val interThm = Goal.prove ctxt [] [] inter1 (K ((auto_tac
        (clasimpset_of ctxt)) THEN (ALLGOALS (Intuitionistic.prover_tac
        ctxt NONE))))

where interThm becomes:

        ⟦⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧ ⟹ ∃s1 s2.
        distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B; distinct
        [?s1.0, ?s2.0]; ?s1.0 ∈ A; ?s1.0 ∈ B; ?s2.0 ∈ A; ?s2.0 ∉ B⟧ ⟹
        ∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B

The next step is to use interThm in 'compose_tac', which is applied on
the original goal sg1:

        compose_tac (false, interThm, 1) i

which fails.


Does it fail because of schematic variables? Is it possible to tell
'Goal.prove' to not produce them?

Apologies for the length, and thank you in advance for your help.

Best,
---
Matej

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.