Re: [isabelle] Isabelle Foundation & Certification

Dear Larry,

Thank you for the clarification. I agree that you are making an important

Iâm not sure whether the other problem will be fixed.

One might be tempted to throw up hands and proclaim that the theorem prover
cannot be expected to check that your definitions actually make sense; at
best it can check that they are consistent. However, thinking about this
problem just now, I realised that something similar to the existing
AutoQuickcheck could be helpful: something that says "you seem to be trying
to prove this the hard way, but it's actually very simple because your
assumptions imply False!".


On 17 September 2015 at 21:56, Larry Paulson <lp15 at> wrote:

> Thanks for giving this example.
> As people seem to have misunderstood my position, let me try again,
> because important points are being overlooked.
> Of course I think that this circularity check ought to be made. I was
> under the impression that this patch had been made already. Nevertheless, I
> do not believe that it poses any immediate problem for users.
> Over the whole of the 1990s, it was possible to introduce cyclic
> definitions in Isabelle, and this possibility was specifically mentioned in
> the documentation. To do this required making three separate steps: you had
> to introduce some A, then define some B in terms of A, and finally define A
> in terms of B. Anybody who thinks they are in danger of doing this
> accidentally really should be working in another field.  Certainly none of
> our existing users were affected when we tightened up our checks. Nobody
> had made this mistake.
> The reason I keep stressing this point is that I regularly see work where
> the definitions donât make any sense, even though they are noncircular. It
> is very easy to do. You verify some mechanism and you include some
> well-definedness predicate on states that can never be satisfied. Then you
> prove âWD(x) ==> P(x)". Ph.D. supervisors and referees do to overlook such
> things, even when they are blatant. And then it is necessary to argue with
> the referees because âthe proof has been checked by machineâ.
> I am sure that this type definition problem will be fixed in time for the
> next release. Iâm not sure whether the other problem will be fixed.
> Larry Paulson
> > On 17 Sep 2015, at 07:14, Holger Blasum <hbl at> wrote:
> >
> > Hello Larry, list,
> >
> > On 09-16, Larry Paulson wrote:
> >> It would be interesting to find out how these problems were identified:
> whether they were looked for out of curiosity, or whether on the other hand
> they manifested themselves in the course of an actual proof.
> >
> > I can give more detail for the case of EURO-MILS: We were made aware of
> > "Isabelle Isar-Reference Manual (Version 2013-2, pp. 103): "It is at
> > the discretion of the user to avoid malformed theory specifications!"[1]
> > Hence first attempt was to rule out use of "consts"[2].
> > This resulted in people even becoming more curious and playing
> > with Kuncar/Popescu.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.