*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] more Isabelle2007 conversion pains*From*: berghofe at mailbroy.informatik.tu-muenchen.de*Date*: Fri, 30 May 2008 18:59:44 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <483B6872.7060902@rsise.anu.edu.au>*References*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com> <48240A4F.1070006@in.tum.de> <48278BA3.6090206@nicta.com.au> <48325DC2.9080904@rsise.anu.edu.au> <483A7E0B.60902@in.tum.de> <483B6872.7060902@rsise.anu.edu.au>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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

**References**:**[isabelle] Reasoning about k-fold cartesian products***From:*Denis Bueno

**Re: [isabelle] Reasoning about k-fold cartesian products***From:*Tobias Nipkow

**Re: [isabelle] Reasoning about k-fold cartesian products***From:*Michael Norrish

**[isabelle] lemmas following from inductive definitions***From:*Jeremy Dawson

**Re: [isabelle] lemmas following from inductive definitions***From:*Stefan Berghofer

**[isabelle] more Isabelle2007 conversion pains***From:*Jeremy Dawson

- Previous by Date: [isabelle] Herlihy, Milner, Hoare, O'Hearn etc.: LASER summer school
- Next by Date: [isabelle] Proof-Carrying Code workshop PCC 2008
- Previous by Thread: [isabelle] more Isabelle2007 conversion pains
- Next by Thread: [isabelle] Hiding import of SList
- Cl-isabelle-users May 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list