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



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


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)))"
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





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