Изабель: Как я могу разместить фиксированные аргументы в нотации mixfix? - PullRequest
Новая
       8

Изабель: Как я могу разместить фиксированные аргументы в нотации mixfix?

0 голосов
/ 03 февраля 2019

Скажем, у меня есть следующее определение рефлексивного и транзитивного замыкания отношения, где отношения представлены двоичными предикатами: 

inductive
  closure :: "(['a, 'a] ⇒ bool) ⇒ (['a, 'a] ⇒ bool)"
  for ℛ (infix "→" 50)
where
  gen:
    "x → y ⟹ closure (→) x y" |
  refl:
    "closure (→) x x" |
  trans:
    "⟦closure (→) x y; closure (→) y z⟧ ⟹ closure (→) x z"

Я хочу иметь более хороший синтаксис для приложений closure.Скажем, я бы хотел написать x *(→)* y для closure (→) x y.Проблема в том, что порядок аргументов в этой записи не соответствует порядку аргументов функции closure.

Я подумал, что, возможно, использование \<index> может помочь.К сожалению, документация \<index> в Справочном руководстве Isabelle / Isar очень краткая, и я не мог понять этого.Я немного поиграл с \<index>, но не нашел никакого приемлемого решения.

Меня удивило то, что, очевидно, \<index> переводится в ⇘some_index⇙, судя по некоторым сообщениям об ошибках, которые я получил.Я пытался использовать ⇘ℛ⇙, чтобы отметить позицию, в которой должно идти базовое отношение, но это тоже не сработало.

Ответы [ 2 ]

0 голосов
/ 04 февраля 2019

Для переключения аргументов лучше всего использовать аббревиатуру.(syntax / translations тоже работает, но сокращения следует отдавать предпочтение, потому что они работают в любом контексте (локали, классы типов, ...) и проверяются типами.) К счастью, inductive позволяет одновременно объявлятьсокращения вместе с индуктивным определением.Уравнения для сокращений должны быть на первом месте.Вот как это работает для вашего примера: 

inductive closure :: "(['a, 'a] ⇒ bool) ⇒ (['a, 'a] ⇒ bool)"
  and closure_syntax :: "['a, ['a, 'a] ⇒ bool, 'a] ⇒ bool" ("(_ ⇧*(_)⇧* _)" [999,0,999] 100)
  for ℛ (infix "→" 50)
  where
  "x ⇧*(→)⇧* y ≡ closure (→) x y"
| gen: "x → y ⟹ x ⇧*(→)⇧* y"
| refl: "x ⇧*(→)⇧* x"
| trans: "⟦x ⇧*(→)⇧* y; y ⇧*(→)⇧* z⟧ ⟹ x ⇧*(→)⇧* z"

Элемент синтаксиса \<index> в наше время используется редко, потому что локали достигают аналогичного эффекта и обычно более гибки.Смысл \<index> заключается в том, что вы можете объявить параметр как (structure), и он будет автоматически вставлен туда, где анализатор видит \<index> в синтаксической грамматике.Таким образом, он позволяет вам не повторять параметр structure, но локали обычно работают лучше.

0 голосов
/ 04 февраля 2019

Вы, вероятно, захотите использовать syntax и translations, например: 

syntax "_closure" :: "['a, (['a, 'a] ⇒ bool), 'a] ⇒ (['a, 'a] ⇒ bool)" ("(_ *'(_')* _)")
translations "x *(ℛ)* y" ⇌ "CONST closure (ℛ) x y"

Они также описаны в isar-ref.pdf, с некоторыми примерами, всплывающими в файлах теории источников (гипер-поиск должен включить их).

...