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

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.


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