Email Gateway (Aug 19 2022 at 14:01): Email Gateway (Aug 19 2022 at 14:01):From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle expert,
I was trying to convert coefficients of a polynomial (from
HOL/Library/Polynomial.thy) into a vector (from
HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy). However, the
most straightforward definition fails:
definition poly_to_vec :: "'a::zero poly ⇒ ('a, 'b) vec" where
"poly_to_vec p= (χ i. coeff p i)"
due to "Type unification failed: No type arity nat :: finite".
Alternatively, as we have function "coeffs :: 'a poly ⇒ 'a list", which
converts coefficients of a polynomial into a list, it would also suffice
if I can define
definition list_to_vec :: "'a list => ('a, 'b) vec"
Any help would be greatly appreciated.
PS: it seems to me that wrapping indices of a vector as a finite type is
a little bit hard to work with. For example, I didn't find a method to
calculate the size of a vector in the library (please correct me if I
was wrong), and a method I can find online seems indirect either:
definition vec_length :: "('a, 'b::finite) vec => nat" where
"vec_length v = card {i. ? c. c = (vec_nth v) i}"
Best regards,
Email Gateway (Aug 19 2022 at 14:01):From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t think that using vector types for this purpose is a good idea. Their purpose (John Harrison invented this trick of using a finite index type) is to formalise the set R^n for some fixed n. But a function that takes an arbitrary polynomial will have to yield vectors of various types. I suggest using lists and the function coeffs that you mention.
Larry
Last updated: Apr 25 2024 at 20:15 UTC