Re: [isabelle] Replacing COMP

On Mon, 29 Jul 2013, René Neumann wrote:

Now I'm porting to Isabelle2013, where COMP has been removed.

In such situations, the NEWS file is the first place to look.  It says:

* Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
use regular rule composition via "OF" / "THEN", or explicit proof
structure instead.  Note that Isabelle/ML provides a variety of
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
with some care where this is really required.

Unfortunately, THEN is no sufficient replacement as the resulting
foo_impl has a remaining "asm ==> asm" in the premises, which is ugly.

The usual game is to write statements and proofs in a way that one does not have to disobey the nice structure of rules provided by Larry Paulson in 1989. There are many ways to do that, but from the given example it is hard to guess what is right.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.