Email Gateway (Aug 18 2022 at 11:56): Email Gateway (Aug 18 2022 at 11:56):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Stefan Berghofer wrote:
Stefan,
thanks. But I now find a similar problem: the theorems x.mono, x.unfold
and x.defs
seem to have disappeared. Actually it seems the theorems x.mono,
x.unfold already don't appear in Isabelle2005 for new-style theory
files, but you could use an old-style theory file, or (sometimes) derive
x.unfold from x.defs.
But in Isabelle2007 you can't use an old-style theory file and even
x.defs doesn't seem to exist. Where have all these theorems gone?
Regards,
Jeremy
Email Gateway (Aug 18 2022 at 11:57):From: stefan.berghofer@in.tum.de
Quoting Jeremy Dawson <jeremy@rsise.anu.edu.au>:
Dear Jeremy,
the problem with these rules is that they expose the internal representation
of inductive sets or predicates, which violates the principle of information
hiding. Since the internal representation has been changed recently, proofs
using these rules would not have worked any longer anyway, so I decided to
remove them. The 'official' way of proving something about an inductive
definition is to use the introduction, induction and case analysis rules,
and indeed all proofs using the x.unfold or x.defs rules can easily be
rewritten to use these 'official' rules.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 11:57):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
berghofe@mailbroy.informatik.tu-muenchen.de wrote:
Dear Stefan,
Thanks for your reply.
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.
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?
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.
Now I'm doing different work, with a mass of Isabelle theories which
work for Isabelle2005. If I don't adapt them to Isabelle 2007 (and I
obviously have a strong incentive not to do so) it means that any
further work I do is in Isabelle2005; this means that if someone else
does similar things in Isabelle2007, neither of us can use each other's
work. This is not a good idea, but it is a natural consequence of the
significant incompatibilities which have often been a consequence of
recent developments in Isabelle.
Regards,
Jeremy Dawson
Email Gateway (Aug 18 2022 at 11:58):From: Stefan Berghofer <berghofe@in.tum.de>
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)})
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)+
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 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.
Regards,
Stefan
Email Gateway (Aug 18 2022 at 12:00):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
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 isr^* == 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
Email Gateway (Aug 18 2022 at 12:00):From: Tobias Nipkow <nipkow@in.tum.de>
Well, I have a rather vague recollection of hearing that the AFP is only
interested in proofs written in Isar. Is that correct?
It does not say so anywhere. And some contributions are not in Isar.
Although we do have a preference for Isar and may ask for revisions of
particularly brittle theories before adding them.
Tobias
Last updated: May 03 2024 at 04:19 UTC