vector - Isabelle: ベクトルの最大値

Question

自然数のベクトルの最大値を見つけたいです。ただし、ベクトル (つまり、「vec」) は、セットまたはリストとは異なる型です。vec の型のレベリングやリフティング、再帰関数の定義など、うまくいかないアイデアをいくつか考えました。

ベクトルの最大値を取得するために提案する解決策は何ですか?

(*
IMPORTS:
  "~~/src/HOL/Algebra/Ring"
  "~~/src/HOL/Library/Numeral_Type"
  "~~/src/HOL/Library/Permutations"
  "~~/src/HOL/Library/Polynomial"
  "~~/src/HOL/Big_Operators"

 vec (VECTOR) is from Finite_Cartesian_Product
 degree is from Polynomial
 Max is from Big_Operators
*)

(* The problem is that "Max" from Big_Operators is not working on vectors! *)
definition maxdeg:: "('a::zero poly)^'n ⇒ nat" where "maxdeg v = Max(χ i . degree(v$i))"