[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
Andreas Schropp
schropp at in.tum.de
Wed Feb 9 16:12:06 CET 2011
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 = ?n2". I do not see why it could not produce ?n = ?n.
>
AFAIK this question is mostly equivalent to the question
"Why does Variable.export use maxidx instead of reusing names and
relying on an invariant like 'names are always fixed'?"
and the answer I was given (by Makarius in May 2010 in private Email
conversation)
to that question is something like
"tools aren't this well behaved, such an invariant does not hold in
general."
IIRC I even had the pleasure to witness this behaviour in actual code.
Regards,
Andy
More information about the isabelle-dev
mailing list