Re: [isabelle] Lifting variables in theorem



I don’t recognise much in the code any more, but you could consider Drule.export_without_context.


Larry Paulson


On 31 Jan 2014, at 16:11, Moa Johansson <moa.johansson at chalmers.se> 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.