[isabelle-dev] Redundant equations in function declarations
makarius at sketis.net
Thu May 31 22:23:02 CEST 2012
On Tue, 29 May 2012, Makarius wrote:
> On Tue, 29 May 2012, Lawrence Paulson wrote:
>> I'm not talking about user interfaces or models. I am saying that function
>> definitions containing entirely redundant equations should be rejected,
>> also in batch mode.
> Maybe you can do some routine investigations why the current situation
> (63021e59cbf0) of the function package is the way it is.
I've now spent myself the canonical 10 min looking through the history.
The relevant changesets are:
date: Mon Aug 20 20:36:19 2007 +0200
issue a warning, when encountering redundant equations (covered by
date: Sun May 22 20:59:13 2011 +0200
fun command produces warning when patterns are incomplete (somewhat
analogous to primrec)
This does not say anything special, just that Alex Krauss added the
warning in an early version of the function package in 2007, and did not
remove or change it in a more recent refinement in 2011. Maybe it just
imitates the way of ML.
So I continue not claiming any expertise on this specific detail of the
Generally, the best "strength" of messages by the system is difficult to
determine. Proof General and the OCaml toplevel are very rude in the
sense that they stop at the first hard error. Compared to that, Poly/ML
is much better at error recovery, say to present a partially type-checked
piece of source with IDE markup. (I've recently shown the Isabelle/ML IDE
to some local OCaml experts and they were quite impressed by the quality
of the feedback from its static analysis produced in real time as the user
types the text.)
The Isabelle Prover IDE for logical part is still a bit crude here: it
skips over failed commands and retains any of the markup produced so far.
This also means a hard error is not so hard after all, and can sometimes
cause more confusion than a soft one, because the binding of the formal
entity to be defined will be absent from the context. Thus the scoping in
later text can change unexpectedly for the user: e.g. a bad function "foo"
used later in formal text becomes a free variable (luckily with the Haribo
color effect, which will gradually include more and more details about
So far I've only fine-tuned some messages sporadically, whenever grossly
confusing situations have shown up. Often it just means to propagate the
formal position information correctly. The basic interaction model and
the possibilities for extra markup are very relevant to get this right.
Optimizing for Proof General is different than optimizing for
Isabelle/jEdit. (Anyway, does anybody step forward to continue
maintenance of Isabelle Proof General?)
More information about the isabelle-dev