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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
