Re: [isabelle] Lifting variables in theorem



Am 31.01.2014 17:28, schrieb Jasmin Blanchette:
Hi Moa,

Am 31.01.2014 um 17:11 schrieb Moa Johansson <moa.johansson at chalmers.se>:

I'm currently porting some functionality from the HipSpec lemma discovery system into Isabelle.
Great!

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?
You might want to have a look at "Drule.generalize". It provides a slightly higher-level interface, without the mysterious "int".

Hi Moa,

an even higher-level interface that also works in a localized setting is the following:

Proof_Context.export names_ctxt ctxt

Here ctxt is the context in which your theorem lives (in particular the one that knows about free variables that are not really free but e.g., fixed by a locale). The second context (names_ctxt) is the enriched version of ctxt where the variables to be exported have been declared (e.g., via names_ctxt = Variable.declare_thm thm ctxt).

Dmitriy




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