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?
The commands interpretation and interpret only register those facts from locales that are not already in scope from previous interpretations. The ring locale is a sub-locale of comm_group with the prefix add and precisely the parameter instantiation you are giving in the first interpretation. Since all these facts are already available (albeit under a different name), interpret does not add them once more. In the interpretation additivee, the instantiation of the parameters is different, so the facts from the locale are added.