Re: [isabelle] How to "code abstract" over nested types
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)))"
On 26/04/15 14:51, Wenda Li wrote:
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)))"
which doesn't work as I have violated code abstraction by using Poly in the lemma.
Any advice/suggestion would be greatly appreciated,
This archive was generated by a fusion of
Pipermail (Mailman edition) and