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

[Lawrence Paulson]

I was about to change the documentation to say just that, only to discover that almost exactly the same change was made in November 2008.

wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:321:   \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:322:   bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:323:   @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
wenzelm 50072 Wed Nov 07 16:02:43 2012 +0100     src/Doc/IsarImplementation/Tactic.thy:324:   not instantiate schematic variables in the goal state.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:321: 
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:322:   Flexible subgoals are not updated at will, but are left alone.
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:323:   Strictly speaking, matching means to treat the unknowns in the goal
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:324:   state as constants; these tactics merely discard unifiers that would
wenzelm 28783 Thu Nov 13 22:05:49 2008 +0100 doc-src/IsarImplementation/Thy/tactic.thy:325:   update the goal state.

Larry

On 19 Aug 2013, at 12:30, Tobias Nipkow <nipkow at in.tum.de> wrote:

> 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