[isabelle-dev] produce term patterns

[Makarius]

On Fri, 3 Sep 2010, Florian Haftmann wrote:

> 	@{term "\<lambda>x. x"}
> 	@{prop "id = \<lambda>x. x"}
>
> These antiquotations do not permit Vars -- a design decision for which I
> remember there was a striking cause which I don't remember, though
> (maybe somebody else can comment on this).

This merely follows the principle of uniformity: Isar has certain rules 
about treating terms in a context, and the ML text embedded into Isar 
follows the very same rules.

The Isar principle behind all this: the text is always fixed, i.e. you say 
explicitly what you mean.  This rules out schematic statements, where you 
would say: "let's prove something, guess what". Thus schematic variables 
in Isar text became free for use as term abbreviations.  If you observe 
the Isar proof machinery carefully, you will notice that schematic 
variables only ever occur in the internal machine state -- for historical 
reasons that is printed to the user in a very raw way.

Back to antiquotations: the surprise comes from the way rule instantiation 
works, because you need to give variables outside the context, that are 
part of imported rules.  Here you see a remaining omission in the 
implementation of ML antiquotations -- in the Calculemus/PLMMS 2007 paper 
by Chaieb/Wenzel we sketched many more things that are still not 
implemented.


> A possible workaround in your situation could be to use cpat, e.g.
>
> 	@{cpat "..."} |> Thm.term_of

Yes, this is the workaround that is still valid for the time being, until 
more serious rule instantiation is implemented within the antiquotation 
framework.


 	Makarius