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

[Tobias Nipkow]

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.

To continue your analogy with lambda-calculus: I can understand why
renaming is necessary in lambda-calculus without reading an
implementation manual. Of course, certain implementations of
lambda-calculus may rename more than is necessary, for implementation
reasons - is that what you mean?

Tobias

Makarius schrieb:
> 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 the when. Generating
>> unpredictable names does not contribute to stability of proofs.
> 
> The stage of 1998/1999 refers the way how Isar generally treats local
> fixes, with import and export of results.  Apart from introducing a
> whole new conceptual level of proper local context, it has also solved
> older known problems (e.g. of the "freeze_thaw" family of functions,
> although there are still there as legacy).  After 1999 there were
> further aspects coming in -- I can't give a comprehensive overview right
> now, apart from what is written in the implementation manual.  (How many
> people have actually read it?)
> 
> Working with nested scopes naturally involves situation where literal
> names cannot be maintained from start to end.  Otherwise lambda calculus
> with "capture-free substitution" etc. would be trivial.  If you take the
> res_inst_tac family for example, there is an internal treatment of names
> like x, xa, xb that some people know by the jargon name of
> "as-they-are-printed", with some funny effects.
> 
> There are many more fine points that have shown up and been adressed
> concerning the delicate question of contexts, variable scoping, renaming
> etc. over years.  The discussion right now seems to say: This has all
> been nonsense, and should be thrown away.
> 
> 
>     Makarius