[isabelle-dev] [isabelle] match_tac, schematic and bound variables

[Makarius]

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 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-July/msg00084.html 
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.


 	Makarius