[isabelle-dev] bnf_decl axiomatization

[Makarius]

This is a continuation of the thread: "code_pred" introduces axioms? 
(October / November 2013).

Back then, on Thu, 31 Oct 2013, Andreas Lochbihler wrote:

> When Lukas told me about the axioms about three years ago, he said that 
> indeed these axioms only specify new constants which the inductify 
> option of code_pred introduces for code generation. He wanted to 
> somewhen implement proper definitions for these constants, but never 
> found the time.

Axioms "that only specify new constants" are of course an euphemism.  It 
is the nature of axiomatization that the slightest mistake, either 
conceptually on paper or in the implementation, destroys the whole logical 
environment.

After the above incident, I looked around systematically for more such 
surprises in main HOL or its libraries.

A remanining item on the list is 'bnd_decl'.  How does that fit in the 
picture?  Why have an axiomatic version of something that has been 
properly founded on top of existing Isabelle/HOL in a purely definitional 
manner?


Just syntactically, anything that is axiomatic should be clearly visible 
as such, to avoid the surprise when a user thinks to switch on the light, 
but has in fact pushed the "nuke" button.


 	Makarius