The Java analogy is a bit odd. There you have the choice between following the standard and not following it. But when instantiating a thm obtained from a proof block, you are at the mercy of the renaming chosen by the system. And if the system choses a different index tomorrow, practically all those instantiations break. But if the indices are normalized, then only those "almost never" cases break.
Tobias Makarius schrieb: > On Wed, 9 Feb 2011, Tobias Nipkow wrote: > >> I can see the technical reason for having to rename sometimes (almost >> never, as you write), but disagree with renaming by default. > > In 2005/2006 I have myself reconsidered this question again thoroughly, > and concluded that it is the less surprising way. I even consulted with > Christian as the Nominal expert at that point and he agreed :-) > > A related profane example from the Java. The JVM has UTF-16 encoding > for unicode and almost always there is a one-to-one correspondence > between characters and code-points. In rare cases they have to use 2 > characters to represent symbols from some newer variant unicode > standard. Since this happens rarely, practically no Java program treats > it correctly, violating the official standards. If they would have used > UTF-8 instead (which did not exist when Java emerged) programmers would > be used to multi-byte sequences regularly and we could now have \<A> as > 𝒜 without crashing the editor. > > >> But I am glad that at least top-level theorems are not subject to this >> - I assume scope intrusion can happen there as well? > > The toplevel works a bit differently (there is also a formal flag to > distinguish "statement mode" from "proof body mode"). An interesting > challenge for toplevel results are the morphisms that are applied to > move between hypothetical contexts and application contexts. There is > also an interaction with the "of" and "where" attributes here. One of > the long-pending reforms is move instantiation out of this dangerous > zone, for example. (I am pondering this for quite some years already. > Someday all the Mikado sticks will have been removed in proper order.) > > > Anyway, conversation about Isabelle history (past and future) is > interesting, but there is a whole lot of work in the pipeline (work that > has been thought through for a long time already). > > > Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
