On Mon, 12 May 2014, Dmitriy Traytel wrote:
There are two classes of users for bnf_decl:
the Popescu-class:
Anybody who would like to be able to quantify over type constructors
in HOL in order to reason abstractly.
the Traytel-class:
Any developer of extensions to the BNF machinery. Here the axiomatic
command provides "the abstract example" with which we usually test our
proof tactics
This sounds both a bit like "testing-unstable-HOL". But there is no
problem to experiment with axiomatizations, if it clear to the user what
it is, and not a seamingly harmless "bnf_decl". So why not just call it
'bnf_axiomatization' following the recent naming trend?
We are already lucky that the old 'rules', 'arities', 'classes' are no
longer there to bomb applications accidentally -- it is all going through
'axiomatization' in the rare situations where this is needed.
Note that apart from logical uncertainty, there is also a technical
problem: axiomatization within a local theory target goes through many
layers, and it is hard to tell what hits the logical core. In the early
days of the local theory infrastructure, I still had the ambition to have
'axiomatization' and a pure version of 'specification' (i.e. 'obtain' for
definitions) included, but I stopped that quickly after it exploded in my
face once or twice.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
