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

[Tobias Nipkow]

I can see the technical reason for having to rename sometimes (almost
never, as you write), but disagree with renaming by default. But I am
glad that at least top-level theorems are not subject to this - I assume
scope intrusion can happen there as well?

Tobias

Makarius schrieb:
> On Wed, 9 Feb 2011, 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.
> 
> The surface language of Isar could force it more into that direction,
> but brute force is against the Isar philosophy.
> 
> 
> If we look at the example more generally in terms of local contexts and
> scopes, it is one of the situations where freeze_thaw and its funny
> variant freeze_thaw_robust are both broken.  In general you can have
> this situation:
> 
>   {
>     - fix local parameters
>     - get other term material into scope
>     - export result
>   }
> 
> Due to the middle part, certain names might have to be changed. This
> happens *rarely* but it happens, and I did have a concrete crash of
> Larry's freeze_thaw around 1997/1998 when I started to think about Isar
> contexts more systematically.
> 
> So instead of trying hard to rename almost never, to please people
> superficially, the potential renaming happens all the time.  Thus tools
> have a chance to work correctly in the general situation.
> 
> 
>     Makarius