*To*: Nils Jähnig <jaehnig at mi.fu-berlin.de>*Subject*: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?*From*: Lukas Bulwahn <bulwahn at in.tum.de>*Date*: Wed, 25 Jan 2012 16:43:23 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CACU92SCJ-w+1NtskFfsTeg66oj7rkcZni5dG+t_3hfz5Uutn=Q@mail.gmail.com>*References*: <CACU92SCJ-w+1NtskFfsTeg66oj7rkcZni5dG+t_3hfz5Uutn=Q@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:8.0) Gecko/20111124 Thunderbird/8.0

Hello Nils, I suggest you have a look at the tactics in subgoal.ML. Subgoal.FOCUS and friends should be helpful for your quest.

Lukas On 01/25/2012 02:20 PM, Nils Jähnig wrote:

Hello, I was hoping that someone of you could give me a little help with tactics. I try to rewrite an apply-style proof into a tactic, for future automization. my goal: rewrite apply(rule_tac x="A" in exI) as a tactic my attempt: val tac = let x = @{term "A"} in rtac @{thm exI} 1 end my problem: the bound variable x is represented in another way, i.e. I'm substituting nothing with the let-in command. my questions: 1) could somebody tell me, how it will work 2) how can i display the internal representation of a theorem (on ML-level, so that i can see which term instead of x i need to substitute) thanks in advance Nils

**Follow-Ups**:**Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?***From:*Jeremy Dawson

**References**:**[isabelle] how to rewrite rule_tac x="A" in exI as tactic?***From:*Nils Jähnig

- Previous by Date: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?
- Next by Date: [isabelle] 2nd announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)
- Previous by Thread: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?
- Next by Thread: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?
- Cl-isabelle-users January 2012 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