polynomial-math - 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

.

从曼努埃尔的回答中，我正在寻找的解决方案：

 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