[isabelle-dev] [isabelle] match_tac, schematic and bound variables
nipkow at in.tum.de
Mon Aug 19 08:11:16 CEST 2013
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 ;-)
> 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.)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev