Re: [isabelle] Instantiate schematic variable in apply-script



You could always try something like this:

	apply (rule asm_rl [of "a = foo x"])

Larry Paulson


On 27 Sep 2011, at 15:38, Peter Lammich wrote:

> On 09/27/2011 09:28 AM, Lars Noschinski wrote:
>> On 26.09.2011 19:02, Peter Lammich wrote:
>>> Hi all,
>>> 
>>> I have a subgoal of the form
>>> [| ... |] ==>  a = ?f x
>>> 
>>> The proof is to instantiate ?f to function "foo", and then
>>> invoke the simplifier. How to do this instantiation, i.e. is there a
>>> method instantiate with that I can do:
>>>   apply (instantiate ?f = foo)
>> 
>> My usual approach would be to avoid introducing ?f, i.e. sufficiently
>> instantiate the rule which introduced ?f (using the [of]-attribute).
> Unfortunately, this approach is no solution in my case, where ?f is
> introduced by exhaustively applying a bunch of
> elim - rules "apply (elim elim_rules)". The rules in "elim_rules" are a
> verification condition generator, that I definitely do not
> want to instantiate by hand before the actual verification conditions
> are generated.
> 
> 
> Best,
>  Peter
> 






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