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 applications.

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 MHonArc.