Как передать предположения интерпретации локали

Постараюсь прокомментировать ваш вопрос. Пожалуйста, не стесняйтесь задавать дополнительные вопросы в комментариях, если вы обнаружите, что моих комментариев недостаточно для ответа на ваш вопрос.

Во-первых, я хотел бы отметить, что в стандартной документации Isabelle существует хороший учебник по локали и интерпретации локалей. Название документа «Учебное пособие по локали и интерпретации локалей» (автор Клеменс Балларин). Документ также содержит несколько полезных ссылок.

После изучения учебника и ссылок может оказаться полезным просмотреть раздел 5.7 в документе «Справочное руководство Isabelle/Isar».

I would like to use some properties of my structure in the proof required by a locale interpretation

В описании интерпретации локали в справочном руководстве указано, что

Locales may be instantiated, and the resulting instantiated declarations added to the current context. This requires proof (of the instantiated specification) and is called locale interpretation.

Когда вы вызываете команду interpretation с набором правильно сформулированных аргументов, цели, выполняемые командой, зависят исключительно от аргументов. Доказательство, которое вы предоставляете для подтверждения выполненных целей, не повлияет на «полученные экземпляры объявлений». Таким образом, технически не имеет значения, используете ли вы свойства своих функций, которые вы явно упомянули, чтобы доказать интерпретацию.

I would like to interpret then the set of my elements as a structurethat satisfy some locale, e.g. monoid:interpretation "{s . P s}" :: monoid "(add)" "(zero)"

Если вы посмотрите на спецификацию команды interpretation в справочном руководстве (раздел 5.7.3), вы поймете, что в качестве входного аргумента команда принимает «выражение локали». «Выражение локали» описано в разделе 5.7.1 справочного руководства. Здесь я привожу значительно упрощенное (неполное) описание выражения локали:

qualifier : name pos_insts

Поле «квалификатор» является необязательным, а поле «имя» зарезервировано для имени локали, которую вы пытаетесь интерпретировать. Следовательно, выражение "{s . P s}" :: monoid "(add)" "(zero)", которое вы указали в своем вопросе, не является допустимым выражением локали. Я могу только догадываться, что вы хотели использовать одинарное двоеточие вместо двойного двоеточия ::, то есть "{s . P s}" : monoid "(add)" "(zero)", и я продолжу ответ, исходя из этого предположения.

В приведенном вами примере «квалификатор» — это "{s . P s}", «имя» — это monoid, а «pos_insts», по сути, являются терминами, указанными после имени.

Вернувшись к документации, вы также найдете описание поля «квалификатор»:

Instances have an optional qualifier which applies to names in declarations

...

Qualifiers only affect name spaces; they play no role in determining whether one locale instance subsumes another.

Таким образом, указанный вами квалификатор "{s . P s}" может влиять только на имена объявлений. Это никак не повлияет на отстреливаемые командой цели и ее вывод.

interpretation "{s . P s}" : monoid "(add)" "(zero)"

Возвращаясь к вашему примеру, если вы имеете в виду локаль monoid из теории HOL-Groups, то, если вы изучите ее спецификацию, а также спецификацию локали semigroup, вы сможете сделать вывод, что локаль monoid имеет два параметра, которые связаны с ним: f и z. Других параметров нет, и «набор носителей» моноида, связанного с локалью, состоит из всех терминов данного типа.

locale monoid = semigroup +
  fixes z :: 'a ("❙1")
  assumes left_neutral [simp]: "❙1 ❙* a = a"
  assumes right_neutral [simp]: "a ❙* ❙1 = a"

В заключение, локаль monoid из теории HOL-Groups не подходит для представления моноида на явном множестве носителей, являющемся собственным подмножеством термов данного типа.

Для вашего приложения вам нужно будет использовать локаль, представляющую моноид на явном наборе несущих, например, локаль monoid из теории HOL-Algebra.Group. Примеры его интерпретации вы можете увидеть в теории HOL-Algebra.IntRing.

ОБНОВИТЬ

По просьбе автора вопроса, заданного в комментариях, привожу пример интерпретации локали monoid из теории HOL-Algebra.Group:

theory SO_Question
  imports "HOL-Algebra.Group"

begin

abbreviation even_monoid :: "int monoid" ("?⇩2") where 
  "even_monoid ≡ ⦇carrier = {x. x mod 2 = 0}, mult = (+), one = 0::int⦈"

interpretation even_monoid: monoid ?⇩2
  by unfold_locales auto+

end