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
