Email Gateway (Aug 22 2022 at 09:26): Email Gateway (Aug 22 2022 at 09:26):From: Wenda Li <wl302@cam.ac.uk>
Dear code generation experts,
With "~~/src/HOL/Library/Polynomial", I have defined an operation:
consts swap_xy:: "'a poly poly ⇒ 'a poly poly"
which, if we treat "'a poly poly" as a bivariate polynomial, swaps the
two variables. In terms of execution, swap_xy should be able to be
implemented using the "transpose" operation on lists. However, the
problems is I am not sure how to write down the code abstract lemma for
nested types like "'a poly poly". A naive try is:
lemma [code abstract]:"coeffs (swap_xy p) = map Poly (transpose (map
coeffs (coeffs p)))" sorry
which doesn't work as I have violated code abstraction by using Poly in
the lemma.
Any advice/suggestion would be greatly appreciated,
Wenda
Email Gateway (Aug 22 2022 at 09:27):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Wenda,
Unfortunately, the code generator cannot handle nested abstract types. In general, you'd
have to define a type isomorphic to "'a poly poly" and lift all your functions to that
type. For 'a poly, however, there is a simpler solution, as the Poly function can be
easily implemented for all lists (rather than just those satisfying the invariant of the
type). Thus, define your own copy of Poly, say Poly', and use Poly' instead of Poly in
your code equation.
definition Poly' :: "'a ::zero list ⇒ 'a poly"
where "Poly' = Poly"
lemma Poly'_code [code]: "coeffs (Poly' p) = strip_while (op = 0) p"
unfolding Poly'_def by(fact coeffs_Poly)
lemma [code abstract]:"coeffs (swap_xy p) = map Poly' (transpose (map coeffs (coeffs p)))"
sorry
Best,
Andreas
Last updated: Apr 26 2024 at 16:20 UTC