*To*: Matej Urbas <mu232 at cam.ac.uk>*Subject*: Re: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Holger Gast <gast at informatik.uni-tuebingen.de>*Date*: Mon, 11 Jul 2011 11:37:09 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1310215039.3708.28.camel@toncka.urbas.si>*References*: <1310215039.3708.28.camel@toncka.urbas.si>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.17) Gecko/20110424 Lightning/1.0b2 Thunderbird/3.1.10

Hi Matej, > 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. > [...] > 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. The short answer is: If you use Goal.prove_internal instead of Goal.prove, your approach works just fine. (See the code below.) The function Goal.prove_internal is merely a wrapper for Goal.init / Goal.conclude (+ introducing & discharging assumptions), and init/conclude perform the internal fiddling with the invisible protect constant for you. A quick grep over the sources shows that prove_internal and compose_tac are used by tools and internal code, presumably to do similar low-level goal manipulations. I'm sure this solution is not entirely orthodox, but since it worked for me in many similar situations where I needed precise control over the entire subgoal structure, I thought I'd share it none the less. Holger lemma sg1: "⋀s1 s2. ⟦distinct [s1, s2]; s1 ∈ A; s1 ∈ B; s2 ∈ A; s2 ∉ B⟧ ⟹ ∃s1 s2. distinct [s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B" apply (tactic {* SUBGOAL (fn (sg1,i) => let val ctxt = @{context} val sg2 = @{term "⋀s1 s2. ⟦distinct[s1, s2]; s1 ∈ A ∩ B; s2 ∈ A - B⟧ ⟹ (∃s1 s2. distinct[s1, s2] ∧ s1 ∈ A ∧ s2 ∈ B)"} val intert = Logic.mk_implies (sg2, sg1) val intert_cterm = Thm.cterm_of (ProofContext.theory_of ctxt) intert val _ = tracing ("Have "^Syntax.string_of_term @{context} intert) val interThm = Goal.prove_internal [] intert_cterm (K ((auto_tac (clasimpset_of ctxt)) THEN (ALLGOALS (Intuitionistic.prover_tac ctxt NONE)))) val _ = tracing ("Interm: "^Display.string_of_thm @{context} interThm) in compose_tac (false, interThm, 1) i end) 1 *})

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

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

**References**:**[isabelle] Problems with Logic.mk_implies + compose_tac***From:*Matej Urbas

- Previous by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Next by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Previous by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- 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