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

[Tobias Nipkow]

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