*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] more Isabelle2007 conversion pains*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Tue, 10 Jun 2008 13:05:13 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4847F15D.4040005@in.tum.de>*References*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com> <48240A4F.1070006@in.tum.de> <48278BA3.6090206@nicta.com.au> <48325DC2.9080904@rsise.anu.edu.au> <483A7E0B.60902@in.tum.de> <483B6872.7060902@rsise.anu.edu.au> <20080530185944.7l56wdapwgkos8oo@mailbroy.informatik.tu-muenchen.de> <48434379.3020308@rsise.anu.edu.au> <4847F15D.4040005@in.tum.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Stefan Berghofer wrote:

Jeremy Dawson wrote:I don't understand what you say about "violates the principle ofinformationhiding". If anything provable using x.unfold or x.defs can be provedusing the 'official' rules, then surely the 'official' rules contain(at least) the same information as x.unfold or x.defs.Dear Jeremy,on Wikipedia (http://en.wikipedia.org/wiki/Information_hiding), Ifound thefollowing definition of "information hiding": The principle of information hiding is the hiding of design decisions in a computer program that are most likely to change, thus protectingother parts of the program from change if the design decision ischanged.The protection involves providing a stable interface which shields the remainder of the program from the implementation (the details that are most likely to change). In the context of the inductive definition package, the "design decision" is the way how inductive sets (or predicates) are defined, and the "other parts of the program" that should be protected from change are the proofs about inductively defined sets. Moreover, the "stable interface" that we provide is the introduction, induction and case analysis rules. This also means that proofs relying on an inductive set being defined (or "implemented") in a particular way (such as proofs involving x.defs) will no longer work once the definition has changed. In the old inductive definition package, an inductive set was defined by forming the least fixpoint of a function on the complete lattice of setsof n-tuples, whereas the new inductive command defines inductivepredicatesas a least fixpoint of a function on the complete lattice of n-arypredicates,and the inductive_set command is just a wrapper for the inductivecommand.For example, the definition of rtrancl in Isabelle2005 is r^* == lfp (%S. {x. (EX a. x = (a, a)) | (EX a b c. x = (a, c) & (a, b) : S & (b, c) : r)})

Dear Stefan,

whereas in Isabelle2007, it is r^** == lfp (%p x1 x2. (EX a. x1 = a & x2 = a) | (EX a b c. x1 = a & x2 = c & p a b & r b c)) r^* == {(xa, x). (%x xa. (x, xa) : r)^** xa x}If I can prove x.unfold or x.defs using the 'official' rules, thenwhay can't they be included in the inductive set package as previously?More importantly, may I suggest that it would be good policy on thepart of the developers to ensure that new developments are made to bebackward compatible where possible?We really tried very hard to ensure backward compatibility whenintroducingthe new inductive definition package. In particular, we put a lot of workin the implementation of the inductive_set wrapper that allows most oftheproofs using inductive sets to be ported to Isabelle2007 with a minimalamount of changes. However, the x.defs and x.unfold rules are really abitobscure in my opinion, which is why they were not mentioned in thetutorialeither.

For about 3 years recently I worked on a particular project wherethey generally would use the latest development version of Isabelle.It seems to me that during that time, about half my time on theproject was spent doing useful work and about half was spent changingmy work in response to changes in Isabelle.I can understand your frustration, but with thousands of Isabelletheoriesout there, it is almost impossible to achieve that none of the changes we make affects any of these theories.A good way of ensuring that your theories will still work with newerversionsof Isabelle is to submit them to the AFP.

Once your theories are in the AFP,every developer who makes a change that breaks any of the theories inthe AFP(or the Isabelle distribution) is responsible for fixing it, which isusuallynot too difficult, since the developer knows what kind of changes hehas made.Finally, let me assure you that I am happy to assist in porting any ofyourproofs about inductive definitions to Isabelle2007.

regards, Jeremy Dawson

Regards, Stefan

**Follow-Ups**:**Re: [isabelle] more Isabelle2007 conversion pains***From:*Tobias Nipkow

**References**:**Re: [isabelle] more Isabelle2007 conversion pains***From:*Jeremy Dawson

**Re: [isabelle] more Isabelle2007 conversion pains***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] Defining infinite streams recursively
- Next by Date: [isabelle] CFP: JAR Special Issue on OS Verification
- Previous by Thread: Re: [isabelle] more Isabelle2007 conversion pains
- Next by Thread: Re: [isabelle] more Isabelle2007 conversion pains
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list