Isabelle: максимальное значение в векторе

Question

Я хотел бы найти максимум в векторе натуральных чисел. Вектор (т. Е. 'Vec'), однако, отличается от Set или List. Я думал о нескольких идеях, которые не работали, например, выравнивание или снятие типа 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))" 

Answer 1

Максимальный оператор Max имеет тип 'a set => 'a, т.е. извлекает максимальный элемент из (конечного) множества. Векторы (тип (a, b) vec) по существу являются функциями от индексов к записям с абстракцией, записанными как χ i. _, и приложениями как v $ _.

Теперь вы хотите получить максимальное значение в диапазоне от вектора. С учетом вышесказанного, вы можете использовать функцию range и изложить применение функции на векторах:

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

Это может быть упрощено до

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

Если вы хотите максимальную запись вектора без отображения степени над вектором, следующие работы (где op $ v является эта-сокращением %j. v $ j):

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