Re: [isabelle] Lifting variables in theorem
- To: <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] Lifting variables in theorem
- From: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>
- Date: Sat, 1 Feb 2014 14:07:16 +1100
- In-reply-to: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se>
- References: <4B8F827F-81E0-4526-A3C3-07D35B11E013@chalmers.se>
- User-agent: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130110 Thunderbird/17.0.2
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
On 02/01/2014 03:11 AM, Moa Johansson wrote:
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and