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