在證明isabelle/hol中的解釋時的多態「修復」語句

Question

我在試圖證明多變量多項式的一些基本事實，因此需要一個多度的類型。

type_synonym 'v multi_degree = "'v ⇒ nat" 

這裏也有一些涉及到有限的支持，更多的東西，但這並不 真正重要的一個問題：爲了模擬這個，我 從自然數一些不明類型的變量名 的使用部分功能。然後我定義添加 多度明顯逐點方式：

definition zero_degree :: "'v multi_degree" where "zero_degree = (λ v. 0)" 

definition md_plus :: "'v multi_degree ⇒ 'v multi_degree ⇒ 'v multi_degree" (infix "⊕" 70) where 
    "(d1 ⊕ d2) = (λ v. d1 v + d2 v)" 

lemma assoc_md_plus [simp]: "d1 ⊕ (d2 ⊕ d3) = (d1 ⊕ d2) ⊕ d3" 
    by (rule; simp add: md_plus_def) 

lemma ident_zero_degree [simp]: "d ⊕ zero_degree = d" and "zero_degree ⊕ d = d" 
    by (auto simp add: md_plus_def zero_degree_def) 

lemma sym_md_plus: "d ⊕ d' = d' ⊕ d" 
    by (rule; simp add: md_plus_def) 

現在我想說的是，除多度的有 可交換獨異的結構。寫在明顯的事情是一樣的東西 這樣：

interpretation md: comm_monoid "op ⊕" "zero_degree" 
proof 

到目前爲止好：輸出

goal (3 subgoals): 
1. ⋀a b c. (a ⊕ b) ⊕ c = a ⊕ (b ⊕ c) 
2. ⋀a b. a ⊕ b = b ⊕ a 
3. ⋀a. a ⊕ zero_degree = a 

，我絕對可以證明！但是，如果我現在寫

interpretation md: comm_monoid "op ⊕" "zero_degree" 
proof 
    fix a 
    show "a ⊕ zero_degree = a" by simp 

然後我得到警告

Introduced fixed type variable(s): 'c in "a__" 

有沒有辦法避免的警告？現在，我已經被騙了，並證明 解釋與

interpretation md: comm_monoid "op ⊕" "zero_degree" 
    by (unfold_locales; simp?; rule sym_md_plus) 

其工作原理，但並不完全清楚未來的讀者......

Answer 1

只要寫fix a :: "'a multi_degree"。如果沒有其他限制，Isabelle會選擇'a作爲類型變量。不過，我認爲它是明確地實際綁定類型變量的好方式，例如，

interpretation md: comm_monoid "op ⊕" "zero_degree :: 'a multi_degree" 
proof 
    fix a :: "'a multi_degree" 

還有一個備註：您可能要考慮使用typedef，然後定義所有你想要它定義與提升/傳輸功能引入新的類型multi_degree。 （請參閱相應的手冊）

這樣做的好處是您可以實例化適當的類型類（如comm_monoid_add），並且不必隨身攜帶區域設置假設。此外，您可以編寫+和0而不是⊕和zero_degree。