[isabelle-dev] Redundant equations in function declarations

[Lawrence Paulson]

Thank you for investigating. I have been waiting for Alex to present his view.

Naturally, the current treatment resembles ML's.

I continue to believe that reference to IDEs is a distraction. I've seen several instances now (in student work) of nonsensical function definitions caused by putting a “default" case too early in the function definition. Anybody who reads the resulting proof document could easily misinterpret what has been proved. There is no reason to allow a specification to contain material that may contradict another part of the specification. It is precisely analogous to allowing, while ignoring, redefinitions of constants. 

Larry

On 31 May 2012, at 21:23, Makarius wrote:

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