Email Gateway (Aug 18 2022 at 15:48): Email Gateway (Aug 18 2022 at 15:48):From: Mathieu Giorgino <Mathieu.Giorgino@irit.fr>
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
Email Gateway (Aug 18 2022 at 15:48):From: Mathieu Giorgino <Mathieu.Giorgino@irit.fr>
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
Email Gateway (Aug 18 2022 at 15:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Mathieu,
the record package provides the necessary accessors, e.g. having
record 'a foo = Bar 'a
you can access the different fields with
foo.Bar :: ('a, 'b) foo_scheme => 'a
foo.more :: ('a, 'b) foo_scheme => 'b
Hope this helps,
Florian
signature.asc
Last updated: Apr 25 2024 at 20:15 UTC