The simplicity of the new code compared with the old suggests that this
treatment is easier to understand, so we should give it a try.
It is interesting that local scopes within structured proofs generate theorems
with nonzero indices, but of course that is a separate matter.
Larry
On 8 Feb
This indeed is probably one of the chief reasons for the existing arrangements.
Larry
On 9 Feb 2011, at 08:36, Alexander Krauss wrote:
An incompatibility that will not be reported by tests is that
intermediate goal states, where nonzero indexnames are quite frequent,
will look significantly
On Wed, 9 Feb 2011, Gerwin Klein wrote:
I don't mind either way, but I'd like to point out that the _tac
instantiations are everything but out of fashion. I'm fully aware that
they are bad style, rely on dynamic names, etc, but there is no way
around them if you write apply style.
Having
On Wed, 9 Feb 2011, Tobias Nipkow wrote:
It is interesting that local scopes within structured proofs generate
theorems with nonzero indices, but of course that is a separate
matter.
Yes, that is a new aspect that was introduced around 1998/1999.
I would be more interested in the why than
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 =
On 02/09/2011 03:39 PM, 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 =
On Wed, 9 Feb 2011, Alexander Krauss wrote:
I don't think that anybody wants to say (or imply) anything like that.
As I understood it, this particular point (Why do nonzero indexnames
show up in this situation, and shouldn't they rather be normalized to
zero as they are in other situations
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
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
