On 08/24/2010 06:35 PM, Makarius wrote:
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.
Why is the safeness of this equality-elimination not a property only
dependent on the "foundation layer"?
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.
I don't get this response:
if a Free x is not mentioned in any assumes, the elimination of a hyp
x=t can not affect provability of the goal,
because any deductions involving x can be done with an arbitrary term of
the same type (esp. t) instead, right?
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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
