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

[Andreas Schropp]

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