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