Изабель: интерпретация локали о записи не доказана

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)

Но я не могу получить доступ к фактам из локали группы. Typing

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инстанцирование параметров отличается, поэтому добавляются факты из локали.