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