Isabelle：關於記錄的語言環境interpration在證明中失敗

Question

使用代數庫時，我遇到了以下問題。在一個證明中，我想把一個環的加性結構解釋爲一個組。這裏是一個示例代碼：

theory aaa 
imports "~~/src/HOL/Algebra/Ring" 
begin 

lemma assumes "ring R" 
shows "True" 
proof- 
interpret ring R by fact 
interpret additive: comm_group "⦇carrier = carrier R, mult = add R, one = zero R⦈" by(unfold_locales) 

但我無法從組語言環境訪問事實。打字

thm additive.m_assoc 

給出消息「未定義的事實」。然而，它的工作原理，當我定義與monoid.make命令添加劑結構：

interpret additivee: comm_group "monoid.make (carrier R) (add R) (zero R)" sorry 

thm additivee.m_assoc 

，如果我嘗試了乘法結構做同樣的，或者如果我刪除

interpret ring R by fact 

它也適用關於發生什麼事的任何想法？

Answer 1

命令interpretation和interpret僅註冊那些來自之前解釋中的範圍之外的語言環境的事實。 ring語言環境是comm_group的子語言環境，其前綴爲add，正是您在第一種解釋中給出的參數實例化。由於所有這些事實已經可用（儘管名稱不同），因此interpret不再添加它們。在解釋additivee中，參數的實例化是不同的，所以添加了來自語言環境的事實。