*To*: Isabelle Users Mailing List <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Matej Urbas <mu232 at cam.ac.uk>*Date*: Sat, 09 Jul 2011 13:37:14 +0100

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

**Follow-Ups**:**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Thomas Sewell

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

**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Holger Gast

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

- Previous by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Previous by Thread: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list