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.