Re: [isabelle] more Isabelle2007 conversion pains
- To: berghofe at mailbroy.informatik.tu-muenchen.de
- Subject: Re: [isabelle] more Isabelle2007 conversion pains
- From: Jeremy Dawson <jeremy at rsise.anu.edu.au>
- Date: Mon, 02 Jun 2008 10:48:57 +1000
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org> <48240A4F.email@example.com> <48278BA3.firstname.lastname@example.org> <48325DC2.email@example.com> <483A7E0B.firstname.lastname@example.org> <483B6872.email@example.com> <firstname.lastname@example.org>
- User-agent: Thunderbird 22.214.171.124 (X11/20070604)
berghofe at mailbroy.informatik.tu-muenchen.de wrote:
Quoting Jeremy Dawson <jeremy at rsise.anu.edu.au>:
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?
the problem with these rules is that they expose the internal
of inductive sets or predicates, which violates the principle of
hiding. Since the internal representation has been changed recently,
using these rules would not have worked any longer anyway, so I
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.
Thanks for your reply.
I don't understand what you say about "violates the principle of
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and