[isabelle] How to "code abstract" over nested types



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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.