[isabelle-dev] bnf_decl axiomatization

[Makarius]

On Tue, 13 May 2014, Dmitriy Traytel wrote:

> Cf. 5fff4dc31d34.

I've spent 15min longer to inspect that version again.  It first looks 
like a variant of typedecl.ML or typedef.ML, which is fine, but looking 
more closely where the axiomatization really happens reveals 
"prepare_def", which happens to be pulled into the ML context by one of 
the initial "open" statements.

This means you trust the result of the large code base behind that, from 
the definitional BNF contstruction, and assert some terms produced there 
as axioms.  You as the author of the code base might have reasons to trust 
it, but that is also the danger.  If this would be relevant for production 
use, it would have to be obvious for someone else to inspect.


Note that the not-so-trivial HOL typedef implementation takes care to keep 
all the critical parts of the implementation in that one file, which is 
further substructured to isolate the main spot where it happens.

Some years ago, I even made the non-emptiness check "passive" and thus 
more fail-safe, in the sense that the ML code produces some propositions 
that are later used to finsh the proof (and "unlock" the conditional 
results), instead of analysing propositions taken from elsewhere.


Anyway, the explicit bnf_axiomatizations in HOL/Library is formally no 
problem.  It is clear to users what they get, and there are no hidden 
dependencies on it in main HOL.


 	Makarius