Isabelle：多項式次數乘以常數

Question

我正在與圖書館HOL/Library/Polynomial.thy合作。

一個簡單的屬性不起作用。例如，中2x *2度等於2x程度 -

我如何證明引理（即去掉 「對不起」）：

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 

。

從Manuel的答案，解決我一直在尋找：

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:]，你有

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

最顯而易見的方法來解決這個問題是假設x ≠ 0。

但是，這還不夠，因爲你只假定'a是一個交換環。但是，在交換環中，一般情況下，可以有零個因子。考慮交換環ℤ/4ℤ。讓x = 2和y = [:0,2:]。 Then y * [:x:] = [:0,4:]，but 4 = 0 in ℤ/4ℤ。因此y * [:x:] = 0，因此，再次，

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

所以，你真正需要的是以下兩種之一：

1. 假設x ≠ 0和 'A :: IDOM，而不是' 一個:: comm_ring 。 IDOM代表「積分結構域」和，即簡單地用1和無零除數
2. 交換環更一般地，假設x不是零除數
3. 甚至更​​一般地，假設x * y ≠ 0，或者相當於x倍y的先導係數不爲0

此外，在Isar證明中⋀的使用在某些時候有些問題。這樣做的「正確」的伊薩爾方法是：

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

相關引理是degree_mult_eq和degree_smult_eq，你會發現他們需要的係數類型是一個IDOM。這適用於我上面描述的第一種情況，我認爲其他兩種需要更多的手動推理。

編輯：只是一個小提示：您可以通過鍵入

find_theorems "degree (_ * _)" 

如果你嘗試應用它顯示了degree_mult_eq您的情況（與comm_ring）找到這樣的定理，你會發現它失敗了，即使這些條款似乎匹配。如果是這樣的話，它通常是一個類型的問題，所以你可以寫類似

from [[show_sorts]] degree_mult_eq 

，看看由引理需要的類型和種類都和它說idom。