[isabelle-dev] Safe approach to hypothesis substitution

[Andreas Schropp]

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
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>