Re: [isabelle] Lifting variables in theorem
Am 31.01.2014 17:28, schrieb Jasmin Blanchette:
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.
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".
an even higher-level interface that also works in a localized setting is
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and