# Re: [isabelle] Making records instances of classes

On 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) finite
Thanks 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
--
http://peteg.org/

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