[isabelle-dev] Safe approach to hypothesis substitution

[Makarius]

On Wed, 25 Aug 2010, Thomas Sewell wrote:

> Indeed bounds, frees and consts can all be seen as the same kind of 
> thing. At the moment the only real benefits of hyp_subst over 
> asm_full_simp are robustness in the case of Vars and the capacity to 
> reorient equations in order to rewrite bounds -> frees -> expressions. 
> Adjusting this to rewrite bounds -> frees -> consts -> expressions would 
> be easy - is this what you are asking for? I don't see this as widely 
> useful, but perhaps you have an application in mind.

Your bounds -> frees -> expressions already sounds quite good.  In the end 
you need to 'prove' it empirically against the existing setup of other 
tools, and usage in concrete applications (Isabelle repos and AFP).  It 
looks like there is a good chance to manage that.


 	Makarius