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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
