Re: [isabelle] Lifting variables in theorem



I don't know about recent versions of Isabelle, but in Isabelle2005 the function Drule.standard does this (plus some other useful things).

I see subsequent emails in the thread talk about contexts - again I don't know about subsequent versions of Isabelle, but in Isabelle 2005 contexts (as I understand the way the word is used nowadays) are not part of a theorem.

Of course current versions of Isabelle may use different functions to do this, and possibly it may not be so easy nowadays

Cheers,

Jeremy


On 02/01/2014 03:11 AM, Moa Johansson wrote:
Hi,

I'm currently porting some functionality from the HipSpec lemma discovery system into Isabelle. I have run into a small problem:

What is the proper way of "lifting" the variables in a theorem to meta-variables?
I.e. when the theorem P x = Q y has been proved, I need to convert all Frees (here let's assume they are x,y) to Vars, getting P ?x = Q ?y.

This happens automatically when performing proofs interactively. Basically, I think I want to have almost the functionality of the function Goal.prove, but as this raises an error when the tactic fails it doesn't quite fit.
Seems like this should be quite simple to do, perhaps this is what Thm.generalize is for? If so, what are its expected arguments? Seems like the first two are lists of all the type-variable and variable names we want to lift, but what is the int?

Grateful for tips!

Moa






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