Re: [isabelle] more Isabelle2007 conversion pains



berghofe at mailbroy.informatik.tu-muenchen.de wrote:
Quoting Jeremy Dawson <jeremy at rsise.anu.edu.au>:

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?

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

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





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