Isabelle에서 int리스트로 다항식 mod의 계수 얻기

Question

두 다항식의 나눗셈의 나머지 계수의 int list을 얻으려고합니다. 나는 int poly의 두 다항식에서 Polynomial.thy의 mod을 사용하려고 시도해 왔습니다.

Type unification failed: No type arity int :: field 

내 기능은 다음과 같습니다 : 그러나, 나는 오류를 얻고있다

int_list 단순히 각 요소 바닥재에 의해 INT의 목록에 실수의 목록을 변환

fun testFunc :: "int poly ⇒ int poly ⇒ int list" 
where 
    "testFunc p q = int_list (coeffs (p mod q))" 

:

fun int_list :: "real list ⇒ int list" 
where 
    "int_list [] = []" | 
    "int_list lst = [floor (hd lst)] @ int_list (tl lst)" 

을

내 함수를 다음과 같이 정의하면 작동합니다.

fun testFunc :: "'a::field poly ⇒ 'a poly ⇒ int list" 
where 
    "testFunc p q = int_list (coeffs (p mod q))" 

그러나 함수에 전달되는 두 개의 인수는 구체적으로 유형이 int poly입니다. 두 번째 정의를 사용하여 두 개의 다항식 'a::field poly과 'a poly을 전달하면 'a list이 반환되고 int_list 함수를 실행할 수 없습니다.

int_list의 서명을 'a list => int list으로 변경하면 각 요소에 int_of을 사용해야하며 궁극적으로 내 목록의 정수는 평가하지 않습니다. (즉, 나는 [int_of 2, int_of 3]보다는 [2, 3] 같은 것을 얻을, 나는 그 목록과 뭔가를하려고 할 때, int_of x 표현보다는 평가를 반환)의 계수의 int list를 얻을 수

이 가능 두 다항식의 모듈로?

Answer 1

floor 기능은 클래스 floor_ceiling (Archimedean_Field.thy#l140)로 인스턴스화되어있어 유형을 필요로한다.

그래서 나는 'a::floor_ceiling으로 가능한 일반적으로 귀하의 int_list합니다

fun int_list :: "'a::{floor_ceiling} list => int list" where 
    "int_list [] = []" | 
    "int_list lst = [floor (hd lst)] @ int_list (tl lst)" 

유형 poly은 그것에게 mod 기능을 제공합니다 클래스 ring_div, 인스턴스화,하지만 'a::field (Polynomial.thy#l1467)에 대한되었습니다. testFunc가 int_list를 사용

때문에, 나는 'a::{field,floor_ceiling}으로 가능한 일반적으로 귀하의 testFunc합니다

fun testFunc :: "'a::{field,floor_ceiling} poly => 'a poly => int list" 
    where 
    "testFunc p q = int_list (coeffs (p mod q))" 

value "testFunc ([:1,2,3:]::real poly) ([:5,6,7:]::real poly)" 
    (*OUTPUT: "[- (2::int), - (1::int)]" :: "int list" *) 

몇 가지 정보 명령 : 속임수를 썼는지

이

declare[[show_sorts, show_consts]] 
print_classes 
    (*At 'class ring_div', it shows ' poly :: (field) ring_div'.*) 
print_dependencies floor_ceiling 
print_dependencies ring_div