[isabelle-dev] Redundant equations in function declarations

[Makarius]

On Tue, 29 May 2012, Lawrence Paulson wrote:

> I am marking some student work submitted for the Cambridge Isabelle 
> course, and have seen some examples where students have gone terribly 
> wrong because they overlooked the warning “Ignoring redundant equation" 
> in a function definition. This sort of mistake could happen to anybody, 
> and it means that proofs are being undertaken on the basis of a mistaken 
> definition. Somebody reading the theory could also overlook this 
> mistake, which goes against the idea that structured proofs should be 
> readable without being executed.
>
> I propose that this particular warning should become a fatal error.

I cannot say anything specific about the function package -- by default 
such things are done the right way, until someone who really understands 
it says something else.


Generally the issue of different degrees of warnings vs. errors is a very 
old one, and used to be intertwined with the infathomable ways of Proof 
General filtering and rearranging prover messages. In Isabelle/jEdit the 
rules are a bit different, more close to the real output of the prover 
(which can be sometimes confusion for other reasons).

Anyway, in our recent Isabelle tutorial, I was surprised how well the 
current scheme of warnings or errors of the main packages already works in 
typical theory development, e.g. when datatype constructors are added or 
removed, and consecutive function definitions (and proofs) need to be 
adapted.

The warnings were shown nicely in the Prover IDE, although some fine 
points still need to be addressed.  It is better to invest the time here, 
than to optimize for the old Proof General model, which tends to require 
more rudeness for messages to be seen by the user.


 	Makarius