Re: [isabelle] more Isabelle2007 conversion pains

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 (, 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 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. 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)+

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+

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


Dr. Stefan Berghofer               E-Mail: berghofe at
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  

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