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

[Makarius]

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