On Fri, 17 Feb 2012, Christian Sternagel wrote:
Dear Developers,
I find it slightly odd to get warnings like
### Legacy feature! Old 'axioms' command -- use 'axiomatization' instead
in places like HOL.thy. The reason is that (at least for me) this theory is
the first place to look how things are done, but the warning (which I only
see when actually loading the theory -- and usually I only browse the
corresponding html page) indicates that things should be done differently.
I vaguely remember a talk by Franz Regensburger from 1994 when he could
still paste HOL.thy onto his slides to explain the foundations of
Isabelle/HOL. Later that initial file become overcrowded with delicate
things for bootstrapping the system, so it lost its model character.
I've done my own re-engeneering of HOL basics around 2000, it ended up in
my PhD thesis as Isar example. It is now in
~/isabelle/repos/src/HOL/ex/Higher_Order_Logic.thy
There is also a simpler ~/isabelle/repos/src/FOL/ex/First_Order_Logic.thy
that is also part of the isar-ref manual as an explanation of how logics
are bootstrapped in a clean room setting.
Other people have refined the understanding of Isabelle/Pure vs.
Isabelle/HOL further, e.g. Stefan Berghofer in his work on proof terms.
If you want to look further around concerning "HOL" in general, beyond
Isabelle/HOL, you should read certain papers by Christoph Benzmüller about
more fine-grained variants of lambda equalities in the logical basis.
Why not use 'axiomatization' here?
Axiomatizations are always delicate, and there is a subtle difference in
the scope of free variables in old 'axioms' vs. 'axiomatization'. The
latter follows the simultaneous scheme that is standard since 10 years or
so. Thus "lemma a: A and b: B sorry" and "axiomatization a: A and b: B"
should produce the same result. While 'axioms' takes each proposition
separate, like most other old specification commands that are already
eliminated. (Maybe someone still remembers the "unify_consts" in-joke of
old primrec.)
More recently the Prover IDE has provided more support to visualize scopes
and inferred types in the editor view, so it has become easier to update
old axiomatizations reliably. This is a slow ongoing process, and but
HOL.thy will probably the last one.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
