Re: [isabelle] Finding the instantiation of a variable



Hi Steve,

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 file "HOL/Isar_Examples/Drinker.thy".

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 probably relevant:

Stefan Berghofer. Program Extraction in simply-typed Higher Order Logic.
TYPES 2002
http://www4.informatik.tu-muenchen.de/~berghofe/papers/TYPES2002.pdf

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

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.

Alex





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