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



this helped. thank you.

2012/1/25 Elsa L Gunter <egunter at illinois.edu>

>  I don't know if this will get you closer to what you want, but if you
> truly already know "A", then you can create a specialized rule/theorem by
>
> lemmas exI_fromA = exI [where x = "A"]
>
> I hope this might help.
> ---Elsa
>
>
>
> On 1/25/12 7:26 AM, Nils Jähnig wrote:
>
> i forgot "val" in my attempt
> val tac = let val x = @{term "A"} in rtac @{thm exI} 1 end
>
>
> 2012/1/25 Nils Jähnig <jaehnig at mi.fu-berlin.de> <jaehnig at mi.fu-berlin.de>
>
>  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.