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



On 09/27/2011 04:38 PM, 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.

Then, I would suggest using rules trans and refl with the of attribute.
I guess in your case:

apply (rule trans)
prefer 2
apply (rule_tac t="foo x" in refl)

might work.


Lukas
Best,
   Peter







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