[isabelle] class instance of a record extension



Hello all,

I would like to make a class instance of a record extension but I cannot find 
any lemma to manipulate the fields of this record extension.

Concretely, here is an example:
-----
record point =
  Xcoord :: nat
  Ycoord :: nat

instance point_ext_type :: (countable) countable
proof (rule countable_classI [of "%p. to_nat (Xcoord p, Ycoord p, more p)"])
qed (auto)

record cpoint = point +
  color :: nat
-----

and I would like to prove this:
-----
instance cpoint_ext_type :: (countable) countable
-----

I would so need a mean to access the color and more fields of a 
cpoint_ext_type, and to be able to prove things about them.

I tried this:
-----
definition
  "cpoint_ext_type_encode p
	= (let p' = point.extend undefined p in to_nat (color p', more p'))"
-----

but then I did not find a way to convert a variable of type cpoint_ext_type 
into something like "(|color = _, ... = _ |)" which would allow to simplify
(|Xcoord = _, Ycoord = _, ... = p |)
into
(|Xcoord = _, Ycoord = _, color = _, ... = _ |).

Is there any (easy) way to do it ? Do I have to use the internal lemmas of the 
record package ?

Regards,

Mathieu





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