Isabelle: maximum value in a vector

问题:

I would like to find the maximum in a vector of natural numbers. Vector (i.e., ‘vec’), however, is a different type than Set or List. I thought about several ideas that did not work, like leveling or lifting the type of vec or the definition of a recursive function.

What solution do you suggest to get the maximum value in a vector?

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

回答1:

The maximum operator Max has type 'a set => 'a, i.e., retrieves the maximum element from a (finite) set. Vectors (type (a, b) vec) are essentially functions from indices to entries with abstraction written as χ i. _ and application as v $ _.

You now want to get the maximum value in the range of a vector. With the above in mind, you can use the range function and spell out the function application on vectors:

 maxdeg v = Max (range (%j. (χ i. degree (v $ i)) $ j))

This can be simplified to

 maxdeg v = Max (range (%i. degree (v $ i)))

If you just want the maximum entry of a vector without mapping degree over vector first, the following works (where op $ v is the eta-contraction of %j. v $ j):

 maxvec v = Max (range (op $ v))