[isabelle-dev] Legacy feature

[Makarius]

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