[isabelle-dev] bnf_decl axiomatization
makarius at sketis.net
Mon May 12 16:54:51 CEST 2014
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
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
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.
More information about the isabelle-dev