[isabelle] Making records instances of classes



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,

Philipp

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










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