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
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:
> "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 |)
> (|Xcoord = _, Ycoord = _, color = _, ... = _ |).
> Is there any (easy) way to do it ? Do I have to use the internal lemmas of
> the record package ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and