Re: [isabelle] more Isabelle2007 conversion pains



Stefan Berghofer wrote:
Jeremy Dawson wrote:
I don't understand what you say about "violates the principle of information hiding". If anything provable using x.unfold or x.defs can be proved using 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), 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)})

Dear Stefan,

I think there is some misunderstanding here. I don't care how the inductive set is defined, logically, internally. The point is, if I'm not mistaken, that the above equality is still true in Isabelle2007. That is, the truth of this equality does not depend on the "design decision" of the way how inductive sets (or predicates) are defined. You would provide a "stable interface" by continuing to make it available.
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 whay can't they be included in the inductive set package as previously?

More importantly, may I suggest that it would be good policy on the part of the developers to ensure that new developments are made to be backward 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.
Well, they are mentioned in the HOL Logic document (including the version of 22 November 2007 (that is, I think, the one distributed with Isabelle 2007)
For about 3 years recently I worked on a particular project where they generally would use the latest development version of Isabelle. It seems to me that during that time, about half my time on the project was spent doing useful work and about half was spent changing my work in response 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.
Well, I have a rather vague recollection of hearing that the AFP is only interested in proofs written in Isar. Is that correct?
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.

Well, thanks - there is also the question of whether it is worthwhile for anyone to bother with doing this, since I'm managing fine with Isabelle2005. Maybe I'll email you separately on this.

regards,

Jeremy Dawson

Regards,
Stefan







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