[isabelle-dev] Safe approach to hypothesis substitution
schropp at in.tum.de
Tue Aug 24 19:01:11 CEST 2010
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 ...
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev