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



Nils,

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

For your second question (not needed to answer the first) the ML function prop_of gives the content of a theorem as a term, which (by default) gets printed out in all its detail.

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








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