If your analogy with lambda calculus is correct, than there are situations when one must rename something exported from a proof block. That I do not understand. Take this example:
lemma True proof- { fix n::nat have "n=n" by auto } produces "?n2 = ?n2". I do not see why it could not produce ?n = ?n. To continue your analogy with lambda-calculus: I can understand why renaming is necessary in lambda-calculus without reading an implementation manual. Of course, certain implementations of lambda-calculus may rename more than is necessary, for implementation reasons - is that what you mean? Tobias Makarius schrieb: > 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev