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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
