Re: [isabelle] Replacing COMP

On Tue, 30 Jul 2013, Tobias Nipkow wrote:

Am 29/07/2013 22:39, schrieb Makarius:
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.

Can you give a concrete example where the use of COMP leads to something the
Isabelle user needs to be protected from?

COMP is conceptually outside the Isabelle/Pure framework (Paulson 1989) and the Isabelle/Isar proof language (Wenzel 1999). It violates certain assumptions about the structure of rules.

We've had a recent isabelle-users thread on COMP in May, with the typical situation that someone does not understand the purpose of !! and ==> yet, is surprised about its behaviour in rule composition, and wants to bypass it without understanding the consequences.

Before everything is repeated, see especially this explanation by Larry:

Even in its internal use COMP came out of use in recent years -- the "INCR" variants are more frequent now, but none of that is for regular use, it is just too complicated.

We've had a few breakdowns on the isabelle-dev mailing list this year already, coming on us from distant past. This resulted in Thm.bicompose in 8 variants (one function with 3 funny flags), where INCR_COMP and COMP_INCR are just the tip of the iceberg. Just formally, such diversity cannot be part of a public programming API in Isabelle/ML. I am even myself never quite sure which of the many COMP variants need to be used when building certain system infrastructure.

For Isabelle/Isar the Isabelle2013/NEWS claims that it is really obsolete, based on empirical information from AFP as usual. So far this thread did not show a counterexample yet, but it might still come. (If all fails users may always define their own Isar attributes as explained in the isar-ref manual, but I don't think this will be required.)


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