[isabelle-dev] bnf_decl axiomatization
traytel at in.tum.de
Mon May 12 22:43:53 CEST 2014
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.
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
because of its axiomatic nature.
There are two classes of users for bnf_decl:
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
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].
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 
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
or be moved elsewhere (potentially to the AFP?).
More information about the isabelle-dev