[isabelle-dev] bnf_decl axiomatization

[Makarius]

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