Isabelle:向量中的最大值 [英] Isabelle: maximum value in a vector

问题描述

我想在自然数向量中找到最大值.向量(即"vec")与集合或列表的类型不同.我想到了一些无效的想法，例如调平或提升vec的类型或定义递归函数.

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

推荐答案

最大运算符Max具有类型'a set => 'a，即从(有限)集中检索最大元素.向量(类型(a, b) vec)本质上是从索引到条目的函数，其抽象写为χ i. _，应用程序写为v $ _.

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 $ _.

您现在想要获得向量范围内的最大值.考虑到以上几点，您可以使用range函数并在矢量上说明该函数的应用程序:

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

这可以简化为

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

如果只想让向量的最大入口数不首先映射向量，则可以使用以下方法(其中op $ v是%j. v $ j的eta-contract):

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

这篇关于Isabelle:向量中的最大值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！