[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Makarius]

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