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

[Tobias Nipkow]

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