[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
Tobias Nipkow
nipkow at in.tum.de
Wed Feb 9 15:39:48 CET 2011
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
More information about the isabelle-dev
mailing list