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