Re: [isabelle] Redefine or hook into the outer-syntax keywords
On Tue, 20 Oct 2015, Cezary Kaliszyk wrote:
Is it possible to redefine the outer-syntax keyword "theorem"
or hook into it?
Not any more. See this NEWS item in Isabelle2015:
* Outer syntax commands are managed authentically within the theory
context, without implicit global state. Potential for accidental
INCOMPATIBILITY, make sure that required theories are really imported.
The keyword "authentic" is Isabelle jargon. It means, formal entities are
really what they are, and cannot be redefined dynamically in a later
context by re-using an existing name.
It has required many years to get there -- the command table was one of
the last hold-outs of non-authentic things, more like a LISP toplevel than
something derived from ML. The change means it is now as serious, as e.g.
the consts table or the fact table. (It is hard to believe today that the
fact name space was non-authentic until 2007).
Whenever we made such steps towards a more serious formal environment,
there was a lot of resistance, especially from power-users who found it
useful to do odd things when nobody was looking. And every time the
tightening of the system revealed embarassing situations in some
I am in the process of defining a new object logic. There, I would like
the keyword "theorem" to analyze the user-given statement, and add
assumptions to it.
There is nothing special about the keyword "theorem", it just happens to
be a predefined specification element in Isabelle/Pure. It should be
possible to invent another name for another concept, and evade that.
Even better, one could think about general ways to augment statements by
additional context material, then it would work everywhere where "prop"
entities may occur, not just a few commands that are somehow "patched".
E.g. you could try to put this into Trueprop-like syntax tricks.
This archive was generated by a fusion of
Pipermail (Mailman edition) and