[isabelle-dev] Safe approach to hypothesis substitution

[Andreas Schropp]

On 08/25/2010 07:57 AM, Thomas Sewell wrote:
> It's interesting that my innocent thread on hypothesis substitution has been hijacked into a discussion about context-aware coding guidelines.

Sorry for that. ^^

> I'm trying to steer clear of contexts - it would seem more elegant to me if there was a purely tactical solution to this problem.
>    

Well as you said

    There's no truly safe way to delete an equality on a Free variable without inspecting the whole context.
       


> To answer Andreas' question about blast_hyp_subst_tac:
>
> I made some attempts, but it seemed that making blast_hyp_subst_tac share behaviour or even code with the other versions led to incompatibilities I didn't really understand. The patch I sent keeps blast_hyp_subst_tac strictly in compatibility mode with previous behaviour.

Ahh, ok.

> I think you've outlined why there was a problem - blast is guessing incorrectly what the tactic will do. Perhaps in the future the Hypsubst ML structure could export its eq_var and triv_asm term inspection functions so blast would have a better idea what it would do (assuming blast can construct accurately what the subgoal passed would be).
>    

Blast has a different term structure with Skolems replacing 
Goal-Parameters etc. In the current architecture
there seems to be no easy way to get a subgoal of the search back as an 
isabelle subgoal.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100825/dcd7301d/attachment-0002.html>