[isabelle-dev] Safe approach to hypothesis substitution

[Makarius]

On Tue, 24 Aug 2010, Andreas Schropp wrote:

> Naive questions:
>  * why is inspecting the whole context infeasible?
>  * why can't we just collect (and cache?) the Frees occuring in assumptions managed
>    by assumption.ML and never delete equalities involving them?

Assumptions belong to the "foundation" layer, i.e. they are conceptionally 
somehow accidental, even hidden.  This is also the reason why using the 
old "prems" abbreviation is a bad thing: you can never be sure what it 
will contain, because Isar language elements are entitled to extend the 
hypothetical context as required internally, e.g. as done by 'obtain', but 
not by 'have'.

Just like global types/consts/defs, local fixes/assumes merely generate an 
infinite collection of consequences.  The latter is what you are working 
with conceptually, but it is not practical.  So the system provides 
further slots to declare certain consequences of a context to certain 
tools: simp, intro, elim etc.

Anyway, I would prefer if the "non-local" behaviour of hyp_subst could be 
repaired without too many additional complications, i.e. by using the 
visible goal that it is offered in a sensible way.

There are some further problems of hyp_subst that maybe Stefan Berghofer 
still recalls.  We have been standing there many times before, but never 
managed to improve it without too much effort, or breaking too many 
existing proof scripts.  The real trouble only starts when trying the main 
portion of existing applications, and also doing some performance 
measurements ...


 	Makarius