[isabelle-dev] Redundant equations in function declarations

[Makarius]

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:

changeset:   24356:65fd09a7243f
user:        krauss
date:        Mon Aug 20 20:36:19 2007 +0200
files:       src/HOL/Tools/function_package/fundef_datatype.ML
description:
issue a warning, when encountering redundant equations (covered by 
prece3ding clauses)

changeset:   42947:fcb6250bf6b4
user:        krauss
date:        Sun May 22 20:59:13 2011 +0200
files:       src/HOL/Tools/Function/fun.ML
description:
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 
function package.


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 
scopes etc.)

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?)


 	Makarius