Isabelle：关于记录的语言环境解释无法证明
Isabelle: locale interpration about record fails in proof
使用Algebra库，遇到如下问题。在一个证明中，我想将环的加法结构解释为一个群。这是一个示例代码：
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
给出消息"Undefined fact"。但是，当我使用 monoid.make 命令定义加法结构时，它会起作用：
interpret additivee: comm_group "monoid.make (carrier R) (add R) (zero R)" sorry
thm additivee.m_assoc
如果我尝试对乘法结构做同样的事情，或者如果我删除
，它也有效
interpret ring R by fact
对正在发生的事情有什么想法吗？
命令 interpretation 和 interpret 仅注册那些来自语言环境的事实，这些事实不在先前解释的范围内。 ring 语言环境是 comm_group 的子语言环境，前缀为 add 并且正是您在第一个解释中给出的参数实例化。由于所有这些事实都已经可用（尽管名称不同），interpret 不再添加它们。在解释additivee中，参数的实例化不同，所以添加了locale的事实。
使用Algebra库，遇到如下问题。在一个证明中，我想将环的加法结构解释为一个群。这是一个示例代码：
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
给出消息"Undefined fact"。但是，当我使用 monoid.make 命令定义加法结构时，它会起作用：
interpret additivee: comm_group "monoid.make (carrier R) (add R) (zero R)" sorry
thm additivee.m_assoc
如果我尝试对乘法结构做同样的事情，或者如果我删除
，它也有效interpret ring R by fact
对正在发生的事情有什么想法吗？
命令 interpretation 和 interpret 仅注册那些来自语言环境的事实，这些事实不在先前解释的范围内。 ring 语言环境是 comm_group 的子语言环境，前缀为 add 并且正是您在第一个解释中给出的参数实例化。由于所有这些事实都已经可用（尽管名称不同），interpret 不再添加它们。在解释additivee中，参数的实例化不同，所以添加了locale的事实。