I can see the technical reason for having to rename sometimes (almost never, as you write), but disagree with renaming by default. But I am glad that at least top-level theorems are not subject to this - I assume scope intrusion can happen there as well?
Tobias Makarius schrieb: > On Wed, 9 Feb 2011, Tobias Nipkow wrote: > >> 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. > > The surface language of Isar could force it more into that direction, > but brute force is against the Isar philosophy. > > > If we look at the example more generally in terms of local contexts and > scopes, it is one of the situations where freeze_thaw and its funny > variant freeze_thaw_robust are both broken. In general you can have > this situation: > > { > - fix local parameters > - get other term material into scope > - export result > } > > Due to the middle part, certain names might have to be changed. This > happens *rarely* but it happens, and I did have a concrete crash of > Larry's freeze_thaw around 1997/1998 when I started to think about Isar > contexts more systematically. > > So instead of trying hard to rename almost never, to please people > superficially, the potential renaming happens all the time. Thus tools > have a chance to work correctly in the general situation. > > > Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev