[isabelle-dev] bnf_decl axiomatization

[Dmitriy Traytel]

Am 12.05.2014 16:54, schrieb 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.

Hi Makarius,

the bnf_decl command declares a new type together with its BNF structure
and automatizes the BNF properties. I've put it in HOL/Library only from 
the start,
because of its axiomatic nature.

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 command bnf_decl is a first
   approximation of this: one can directly formalize statements like
   "for all bounded natural functors F have ...". Of course this 
quantification
   happens only on a meta level---no instantiation of the quantifier is
   possible (without trying to resurrect the AWE tool). One example of such
   a formalization is in src/HOL/BNF_Examples/Stream_Processor which
   follows [1, p9, Remark].

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---cf. the formalization of the BNF operations [2]
   associated with our ITP 2014 paper.

Of course, it is relatively easy to construct "not-so-abstract examples" of
BNFs using the concrete, definitional datatype_new declaration (and
pretending to forget the definition afterwards). Thus, it would not be a
huge problem for the Traytel-class if the command would disappear (in
this case I'm less sure about an adequate replacement for the 
Popescu-class.)
or be moved elsewhere (potentially to the AFP?).

Dmitriy

[1] https://personal.cis.strath.ac.uk/neil.ghani/papers/ghani-lmcs09.pdf
[2] http://www21.in.tum.de/~blanchet/codata_impl.tar.gz