Re: [isabelle] Finding the instantiation of a variable
Does anyone know how one would go about finding the instantiation of a
variable in ML? Say, if I can obtain the proof term for the theorem 'EX f x.
f x > 0', how do I work with the proof term in order to find the
instantiations of 'f' and 'x'?
There are at least two ways in which your question can be understood:
a) Given a proof of "EX x. P x", you want to extract the term "t" that
was used to prove the existential statement
b) Given a proof of "EX x. P x", you want to find any term t such that
"P t" holds.
to a) This is not possible in general. Note that Isabelle/HOL implements
classical logic, which allows existential statements without providing
the values that are proved to exists. So there is no "instantiation"
that can be extracted, at least in general. You can find a simple
example of such a proof (of the well-known Drinker's Principle) in the
If the proof you have does not involve classical reasoning, then your
problem can be solved in principle. But even then, the proof may be more
than just an application of the rule "exI". Then the following paper is
Stefan Berghofer. Program Extraction in simply-typed Higher Order Logic.
to b) If you just need some value that satisfies the property, then you
can of course always use the choice operator and write "SOME x. P x". Of
course this does not contain any information, but sometimes it is
Would the first step be to reconstruct the proof using
Reconstruct.reconstruct_proof? If so, what would subsequent steps involve?
Reconstructing is usually the first thing to do if you want to do
anything useful with a proof term. Further, I don't know. Maybe the
extraction described in the paper above does what you want (but I am not
sure what exactly you want).
Any help will be appreciated.
Actually, what is your application for this? It seems to be a rather
unusual way of using Isabelle. If you give us some more concrete
information about the big picture, i.e., what functionality do you want
to realise in the end, then you might get more helpful answers.
This archive was generated by a fusion of
Pipermail (Mailman edition) and