이사벨 : 벡터의 최대 값

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

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