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

[Makarius]

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