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

[Tobias Nipkow]

Am 19/08/2013 12:45, schrieb Lawrence Paulson:
> Your point of view makes sense on general principles, but not in this particular case.
> 
> I had actually forgotten that these tactics existed. But they form a core part of the classical reasoner, and there are good reasons why they work the way they do. The proof state could be very large, so their "quick and dirty" method of leaving it unchanged (by deleting updates to it, rather than replacing its variables by constants) is necessary to achieve acceptable performance.

I agree and it is not a top priority. But it is an interesting challenge to do
it outside the kernel, and I do wonder if the performance would take a real hit.

> I included these tactics in the documentation in a spirit of openness, and it made sense 20 years ago, when there weren't many developers and anything might be expected to not quite work as advertised in what was obviously a research prototype. But now people have the right to expect things to work as documented. In this case, I would change the documentation, and perhaps make it clear that these are very specialist tools.

That's what I meant. It should merely state explicitly that "these tactics
merely discard unifiers that would update the goal state." can lead to
incompleteness.

Tobias


> Larry
> 
> On 19 Aug 2013, at 07:11, Tobias Nipkow <nipkow at in.tum.de> 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? I have
>> seen more elegant designs ;-)
>>
>> Tobias
>>
>>> Combinators like Subgoal.FOCUS have replaced a lot of old-style tinkering with
>>> goals; within the focused parts things are fixed and don't get instantiated by
>>> accident.  (Tools built on such high-level elements need to be ready to work
>>> with renamings of the original schematic variables. This is the normal situation
>>> in structured proof elements.)
>>>
>>>
>>>    Makarius
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev