*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?*From*: Jeremy Dawson <jlcaadawson at netspeed.com.au>*Date*: Fri, 27 Jan 2012 17:46:45 +1100*In-reply-to*: <4F20231B.5090107@in.tum.de>*References*: <CACU92SCJ-w+1NtskFfsTeg66oj7rkcZni5dG+t_3hfz5Uutn=Q@mail.gmail.com> <4F20231B.5090107@in.tum.de>*Reply-to*: jeremy at rsise.anu.edu.au*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.13) Gecko/20101209 Fedora/3.1.7-0.35.b3pre.fc14 Thunderbird/3.1.7

Nils, For this you want res_inst_tac, described in the Reference manual. Eg (res_inst_tac [("x", "A")] exI 1)

Jeremy On 01/26/2012 02:43 AM, Lukas Bulwahn wrote:

Hello Nils, I suggest you have a look at the tactics in subgoal.ML. Subgoal.FOCUS and friends should be helpful for your quest. Maybe the Isabelle Programming Tutorial (Cookbook) also tells you a little bit about those functions. 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

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

**Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?***From:*Lukas Bulwahn

- Previous by Date: [isabelle] Signatures for counter-example checkers
- Next by Date: [isabelle] Web site is down?
- Previous by Thread: Re: [isabelle] how to rewrite rule_tac x="A" in exI as tactic?
- Next by Thread: [isabelle] 2nd announcement: workshop on Automation in Proof Assistants (31 Mar - 1 Apr 2012)
- 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