Re: [isabelle] Isabelle Foundation & Certification



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 sysgo.com> 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.