# Re: [isabelle] Lifting variables in theorem

On Fri, 31 Jan 2014, Moa Johansson wrote:

`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.
`

`Note that "lifting of variables" has a special meaning in Isabelle
``terminology, according to Larry. The "implementation" manual section
``2.4.2 explains that to some extent, but you won't need that here.
`

`Above, the question is where x and y were coming from. Just using
``undeclared Free variables causes lots of headaches -- one needs to
``understand both the normal Isabelle context discipline and what happens
``without that to get things work.
`

`It is easier to rely on the normal context discipline by default, and
``trust that this things work (they had more than a decade to mature).
`

This happens automatically when performing proofs interactively.

This is because a statement like
lemma "x = x"
has an implicit "eigen context" around it
lemma
fixes x :: 'a
shows "x = x"

`So you state something for fixed x :: 'a, and get the result for arbitrary
``?x :: ?'a (the type generalization is subject to Hindley-Milner
``polymorphism).
`

`Basically, I think I want to have almost the functionality of the
``function Goal.prove
`

`See implementation manual section 6.3 on Goal.prove. It allows you to
``provide fixes and assumes just like a toplevel statement, but that needs
``to be explicit in Isabelle/ML. You can also build up the context
``separately, and export proven results from it.
`

but as this raises an error when the tactic fails it doesn't quite fit.

`I don't understand that. It seems to refer implicitly to a particular
``approach used here. Do you want to use local variables within a tactic?
``Then just fix them, and export whatever you prove, and they become
``schematic.
`

`Seems like this should be quite simple to do, perhaps this is what
``Thm.generalize is for?
`

`Thm.generalize is a primitive inference, so it is primitive, not simple.
``You can ignore that, unless you want to understand the implementation of
``the system. Mixing primitive things with the simple high-level things
``usually leads to something complicated.
`
Makarius

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