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.