On Wed, 9 Feb 2011, Tobias Nipkow wrote:
It is interesting that local scopes within structured proofs generate
theorems with nonzero indices, but of course that is a separate
matter.
Yes, that is a new aspect that was introduced around 1998/1999.
I would be more interested in the why than the when. Generating
unpredictable names does not contribute to stability of proofs.
The stage of 1998/1999 refers the way how Isar generally treats local
fixes, with import and export of results. Apart from introducing a whole
new conceptual level of proper local context, it has also solved older
known problems (e.g. of the "freeze_thaw" family of functions, although
there are still there as legacy). After 1999 there were further aspects
coming in -- I can't give a comprehensive overview right now, apart from
what is written in the implementation manual. (How many people have
actually read it?)
Working with nested scopes naturally involves situation where literal
names cannot be maintained from start to end. Otherwise lambda calculus
with "capture-free substitution" etc. would be trivial. If you take the
res_inst_tac family for example, there is an internal treatment of names
like x, xa, xb that some people know by the jargon name of
"as-they-are-printed", with some funny effects.
There are many more fine points that have shown up and been adressed
concerning the delicate question of contexts, variable scoping, renaming
etc. over years. The discussion right now seems to say: This has all been
nonsense, and should be thrown away.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
