*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

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

**Follow-Ups**:**Re: [isabelle] Lifting variables in theorem***From:*Makarius

- Next by Date: Re: [isabelle] Lifting variables in theorem
- Next by Thread: Re: [isabelle] Lifting variables in theorem
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list