Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Redefine or hook into the outer-syntax keywords

Email Gateway (Aug 22 2022 at 11:47):

From: Cezary Kaliszyk <cezarykaliszyk@gmail.com>
Dear all,

Is it possible to redefine the outer-syntax keyword "theorem"
or hook into it?

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.

I have so far been working with a different outer-syntax keyword
("mytheorem"), but I wonder if it would also be possible to use the
existing
keywords "theorem", "lemma" etc.

Regards,

Cezary

Email Gateway (Aug 22 2022 at 11:47):

From: Makarius <makarius@sketis.net>
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.

Makarius

Last updated: Apr 19 2024 at 16:20 UTC