Re: [isabelle] more Isabelle2007 conversion pains



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






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