이사벨 : 다항식의 차수를 상수로 곱하면

Question

HOL/Library/Polynomial.thy 라이브러리로 작업하고 있습니다.

간단한 속성이 작동하지 않았습니다.

lemma mylemma: 
    fixes y :: "('a::comm_ring_1 poly)" and x :: "('a::comm_ring_1)" 
    shows "1 = 1" (* dummy *) 
proof- 
have "⋀ x. degree [: x :] = 0" by simp 

from this have "⋀ x y. degree (y * [: x :]) = degree y" sorry 

(* different notation: *) 
from this have "⋀ x y. degree (y * (CONST pCons x 0)) = degree y" sorry 

: (즉, "죄송합니다"제거) 나는 보조 정리를 증명할 수있는 방법

- 예를 들면, 2x *2의 정도는 2x의 정도와 동일합니다. 마누엘의 대답에서

이 솔루션은 내가 찾고 있던 : 문제의 번호가 여기에 있습니다

have 1: "⋀ x. degree [: x :] = 0" by simp 
{ 
    fix y :: "('a::comm_ring_1 poly)" and x :: "('a::comm_ring_1)" 
    from 1 have "degree (y * [: x :]) ≤ degree y" 
    by (metis Nat.add_0_right degree_mult_le) 
} 

Answer 1

.

우선, 표시하려고하는 진술은 모두 x에 적용되지 않습니다. x = 0 및 y이 비수가 인 경우, 예를 들어. y = [:0,1:], 당신은이 x ≠ 0을 가정하는 것입니다 해결하는 가장 확실한 방법

degree (y * [: x :]) = degree 0 = 0 ≠ 1 = degree y 

있습니다.

그러나 이것은 단지 'a을 교환 가능 링으로 가정 했으므로 충분하지 않습니다. 그러나 교환 가능한 고리에서는 일반적으로 제수가 0이 될 수 있습니다. 교환 할 수있는 고리 ℤ/4ℤ을 고려하십시오. x = 2 및 y = [:0,2:]으로 설정하십시오. y * [:x:] = [:0,4:]이지만, 4 = 0은 ℤ/4ℤ입니다. 가정 x ≠ 0과 '대신 :: idom'

1. :: comm_ring : 따라서 y * [:x:] = 0 때문에, 다시

   degree (y * [: x :]) = degree 0 = 0 ≠ 1 = degree y 
   

   그럼, 당신이 정말로 필요한 것은 다음 두 가지 중 하나입니다 . idom 더 일반적으로, x 그 가정은 영 인자

2. 더 일반적으로 가정이 x * y ≠ 0 여부를 단순히 1과 0이없는 제수
3. 과 가환 환이다 "정역"와, 의미, 등가 적으로, x x y의 선행 계수가 0이 아니다.

또한, Isar 증명에서 ⋀의 사용은 때때로 다소 문제가있다. 이 일의 "적절한"ISAR 방법은 다음과 같습니다

fix x :: "'a::idom" and y :: "'a poly" 
assume "x ≠ 0" 
hence "degree (y * [:x:]) = degree y" by simp 

관련 보조 정리는 그들이 idom으로 계수 유형을 필요로하는 볼, degree_mult_eq 및 degree_smult_eq 있습니다. 이것은 위에서 설명한 첫 번째 경우에 효과적이며 나머지 두 가지는 더 수동적 인 추론을 필요로한다고 생각합니다.

편집 : 단지 작은 힌트 : 당신이, 당신이 (comm_ring와) 상황에 그것을 보여줍니다 degree_mult_eq을 적용하려고하면

find_theorems "degree (_ * _)" 

를 입력하여이 같은 정리를 찾을 수 있습니다 당신이 실패하는 것을 발견 할 것이다, 용어가 일치하는 것으로 보입니다. 이런 경우, 당신은 보조 정리가 필요로하는 유형과 종류가 무엇인지 볼 수

from [[show_sorts]] degree_mult_eq 

같은 것을 쓸 수 있도록 그것은 보통 형 문제이며, 그것은 idom을 말한다.