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
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
Basically, I think I want to have almost the functionality of the
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and