locale - Isabelle: locale interpration about record fails in proof

Question

Using the Algebra library, I encountered the following problem. In a proof I wanted to interpret the additive structure of a ring as a group. Here is a sample code:

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)

But I can't access the facts from the group locale. Typing

thm additive.m_assoc

gives the message "Undefined fact". However, it works when I define the additive structure with the monoid.make command:

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

thm additivee.m_assoc

It also works if I try to do the same for the multiplicative structure, or if I remove

interpret ring R by fact

Any ideas about what's going on?

Answer 1

这些命令interpretation仅interpret注册那些尚未在先前解释范围内的语言环境中的事实。ring语言环境是comm_group具有前缀的子语言环境，add并且正是您在第一个解释中给出的参数实例化。由于所有这些事实都已经可用（尽管名称不同），interpret因此不再添加它们。在解释additivee中，参数的实例化是不同的，因此添加了来自 locale 的事实。