[isabelle-dev] [isabelle] match_tac, schematic and bound variables
makarius at sketis.net
Mon Aug 19 23:08:18 CEST 2013
On Mon, 19 Aug 2013, Tobias Nipkow wrote:
> Am 17/08/2013 15:20, schrieb Makarius:
>> On Thu, 15 Aug 2013, Lawrence Paulson wrote:
>>> I think that the only way to achieve the documented behaviour is to replace
>>> all schematic variables in the goal by Frees before attempting resolution.
> Which can be done safely outside the kernel.
>> If you would do that for the quais-match mode of unify.ML in general it would
>> probably break down everything else.
>> Doing the above in user space instead, in the actual application at hand (which
>> was not explained on this thread so far) it might turn out trivial.
> So every application that needs matching should implement it separately?
So far the actual application and its concrete approach was not really
explained on this thread. It is bread-and-butter in the use of the
operations around pattern.ML and unify.ML to look closely what they can do
and what not. I have my own catalogue of things that just don't work, e.g
see this recent incident here
concerning "?P x" where x has function type.
I don't think that it is realistic to "fix" these highly complex modules
without causing much greater harm. To get it really right, someone would
have to sit down and spend substantial time and effort on it, and
preferably do some formal proofs about the whole complex. Actually
integrating an improved implementation would then be a second step, with
the usual surprises to be expected, when things at the very bottom are
changed and other tools expect the old behaviour, even it was a bad one.
More information about the isabelle-dev