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。