*To*: philipp.kuefner at tu-berlin.de*Subject*: Re: [isabelle] Making records instances of classes*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Fri, 25 Mar 2011 09:30:56 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1300970976.2506.28.camel@pasus>*References*: <1300970976.2506.28.camel@pasus>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Dear Philipp, in Isabelle 2011, the type for extensible records is no longer called

> * Records: logical foundation type for records does not carry a > '_type' suffix any longer (obsolete due to authentic syntax). > INCOMPATIBILITY. Hence, the following should work now: record ('a, 'b) Tuple = first :: "'a" second :: "'b" instance Tuple_ext :: (finite, finite, finite) finite Hope this helps, Andreas Philipp Küfner schrieb:

Dear all, In July 2010 there was a discussion on Making records instances of classes. As far as I can see the presented solution (see below) does not work with the current version of Isabelle (2011) anymore (due to the new implementation of records). So does anyone know how to handle this problem now? Thanks a lot, PhilippOn 09/07/2010, at 4:56 PM, Andreas Lochbihler wrote:Behind the scenes, the package achieves this by defining a more general type for Tuple called Tuple_ext_type, which takes another type variable. Then, the type ('a, 'b) Tuple is just a type abbreviation for ('a, 'b, unit) Tuple_ext_type. For subrecord types, this additional type variable is instantiated to some other type which stores the additional information. Type classes can only be instantiated for "logical" type constructors, not for abbreviations like Tuple. In your example, you would have to instantiate Tuple_ext_type itself. Note that this instantiation then also applies to all subrecords you might ever define. record ('a, 'b) Tuple = first :: "'a" second :: "'b" instance Tuple_type_ext :: (finite, finite, finite) finiteThanks Andreas! Perhaps this could make its way into the distributed Isabelle documentation and/or examples? Also Florian Haftmann sent me this complete chunk of proof text off-list, for which I am grateful: record ('a, 'b) Tuple = first :: "'a" second :: "'b" instance Tuple_ext_type :: (finite, finite, finite) finite proof let ?U = "UNIV :: ('a, 'b, 'c) Tuple_ext_type set" { fix x :: "('a, 'b, 'c) Tuple_scheme" have "∃a b c. x = Tuple_ext a b c" by (cases x) simp } then have U: "?U = (\<lambda>((a, b), c). Tuple_ext a b c) ` ((UNIV × UNIV) × UNIV)" by (auto simp add: image_def) show "finite ?U" by (simp add: U) qed cheers peter

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-48352 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] Making records instances of classes***From:*Philipp Küfner

- Previous by Date: [isabelle] 2nd CfP: THedu'11 at CADE
- Next by Date: [isabelle] Vector of bools
- Previous by Thread: [isabelle] Making records instances of classes
- Next by Thread: Re: [isabelle] Making records instances of classes
- Cl-isabelle-users March 2011 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