[isabelle-dev] bnf_decl axiomatization
makarius at sketis.net
Mon May 12 23:10:08 CEST 2014
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.
More information about the isabelle-dev