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