Re: [isabelle] Problems with Logic.mk_implies + compose_tac



Hi Matej,

Two interesting things have happened. The first is that Goal.prove has lifted your meta-quantified conclusion (/\s1 s2. P s1 s2) into a schematically quantified theorem (P ?s1 ?s2). The internal ==> implications within your conclusion sg2 are now treated together with the sg1 ==> sg2 implication as a group of assumptions. This may make compose_tac surprise you. You've told it you want to have only 1 new goal - if I recall correctly that will be the final assumption of the supplied theorem, so try rotating the sg1 assumption to the end.

If that fails, you could try to stop Goal.prove lifting your meta-quantification. Playing around with the (invisible) protect constant might help you - look up protectI or protectD, No promises. Alternatively you could sidestep Goal.prove entirely by creating Thm.trivial from sg1 ==> sg2 and applying your tactic to eliminate the first assumption.

Can't be bothered firing up Isabelle on a weekend to test any of these strategies for you. Good luck.

Yours,
    Thomas.

________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Matej Urbas [mu232 at cam.ac.uk]
Sent: Saturday, July 09, 2011 10:37 PM
To: Isabelle Users Mailing List
Subject: [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

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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