*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] more Isabelle2007 conversion pains*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Thu, 05 Jun 2008 15:59:57 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <48434379.3020308@rsise.anu.edu.au>*Organization*: Technische Universität München*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>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.13) Gecko/20060417

Jeremy Dawson wrote:

I don't understand what you say about "violates the principle of informationhiding". If anything provable using x.unfold or x.defs can be provedusing the 'official' rules, then surely the 'official' rules contain (atleast) the same information as x.unfold or x.defs.

Dear Jeremy, on Wikipedia (http://en.wikipedia.org/wiki/Information_hiding), I found the following 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 protecting other parts of the program from change if the design decision is changed. 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 sets of n-tuples, whereas the new inductive command defines inductive predicates as a least fixpoint of a function on the complete lattice of n-ary predicates, and the inductive_set command is just a wrapper for the inductive command. 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)}) 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, then whaycan't they be included in the inductive set package as previously?More importantly, may I suggest that it would be good policy on the partof the developers to ensure that new developments are made to bebackward compatible where possible?

We really tried very hard to ensure backward compatibility when introducing the new inductive definition package. In particular, we put a lot of work in the implementation of the inductive_set wrapper that allows most of the proofs using inductive sets to be ported to Isabelle2007 with a minimal amount of changes. However, the x.defs and x.unfold rules are really a bit obscure in my opinion, which is why they were not mentioned in the tutorial either. It therefore made no sense to me to write additional code for proving these obscure rules from the "official" ones, in particular because the few proofs in the Isabelle distributions that were using these rules could easily be adapted. For example, the proof of exec_mono in HOL/Induct/Com.thy in Isabelle2005 looked as follows: lemma exec_mono: "A<=B ==> exec(A) <= exec(B)" apply (unfold exec.defs ) apply (rule lfp_mono) apply (assumption | rule basic_monos)+ done In contrast, the Isabelle2007 version is lemma exec_mono: "A<=B ==> exec(A) <= exec(B)" apply (rule subsetI) apply (simp add: split_paired_all) apply (erule exec.induct) apply blast+ done

For about 3 years recently I worked on a particular project where theygenerally would use the latest development version of Isabelle. Itseems to me that during that time, about half my time on the project wasspent doing useful work and about half was spent changing my work inresponse to changes in Isabelle.

I can understand your frustration, but with thousands of Isabelle theories out 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 newer versions of 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 in the AFP (or the Isabelle distribution) is responsible for fixing it, which is usually not too difficult, since the developer knows what kind of changes he has made. Finally, let me assure you that I am happy to assist in porting any of your proofs about inductive definitions to Isabelle2007. Regards, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

**Follow-Ups**:**Re: [isabelle] more Isabelle2007 conversion pains***From:*Jeremy Dawson

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

- Previous by Date: [isabelle] Finite Datatype
- Next by Date: Re: [isabelle] Isabelle problem
- 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