Re: [isabelle] class instance of a record extension



I have finally found a way to transform a variable p of type point_ext_type 
into (|color = _, ... = _|) with:
(case_tac "point.extend undefined p", simp add:point.defs)

but does there exist a better way to do this and to access record extensions 
fields ?

Mathieu

Le jeudi 12 août 2010 11:16:17, Mathieu Giorgino a écrit :
> 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.