Re: [isabelle] Isabelle Foundation & Certification



Am Donnerstag, den 17.09.2015, 12:56 +0100 schrieb Larry Paulson:
[..]
> 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.

If such a circle happens in the _one_ theory file and is as obvious as
this one, maybe the developer should be working in another field. But we
get a bigger and bigger type class hierarchy and we started a couple of
years ago to use type classes in type definitions. I work a lot with the
type class hierarchy but some parts are still blurry to me. The last
time Florian printed it out, it was a huge poster!

For large developments in Isabelle, one imports a lot of theories and
uses a lot of automatic proof methods. What happens if my definitions
are completely fine, but a freak combination of theories I import allows
Sledgehammer to prove false?

 - Johannes



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