Как передать предположения в интерпретацию локали - PullRequest
Новая
       61

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

1 голос
/ 30 мая 2019

Я хотел бы использовать некоторые свойства моей структуры в доказательстве, требуемом для интерпретации локали

В качестве примера, предположим, что я определил предикат P и доказал некоторые леммы (add является закрытой двоичной операцией, add является ассоциативным и существует zero нейтральный элемент) о операции add над элементами которые удовлетворяют предикату P

Я бы хотел интерпретировать набор моих элементов как структуру, которая удовлетворить некоторые локали, например, monoid

interpretation "{s . P s}" :: monoid "(add)" "(zero)"
unfolding
  monoid_def
using
  add_is_associative
  zero_is_neutral

но тогда в целях моего доказательства я не смог понять, что все элементы на самом деле удовлетворяют предикат P, и я остался с общей целью такой как add zero a = a, который я уже доказал для элементов в моем наборе.

Как добиться в моей цели, чтобы все элементы удовлетворяли предикату P?

1 Ответ

1 голос
/ 30 мая 2019

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

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

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

Я хотел бы использовать некоторые свойства моей структуры в доказательстве требуется для интерпретации локали

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

Локали могут быть созданы, а результирующие объявления добавлены в текущий контекст. Это требует доказательств (из конкретизированная спецификация) и называется интерпретация локали .

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

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

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

Экземпляры имеют дополнительный квалификатор, который применяется к именам в заявления

...

Определители влияют только на пространства имен; они не играют никакой роли в определение того, относится ли один экземпляр языкового стандарта к другому.

Таким образом, указанный вами спецификатор "{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
...