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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
