Isabelle：我怎样才能在 mixfix 表示法中定位固定参数？答案

【问题标题】：Isabelle: How can I position fixed arguments in mixfix notation?Isabelle：我怎样才能在 mixfix 表示法中定位固定参数？
【发布时间】：2019-02-03 20:47:55
【问题描述】：

假设我对关系的自反和传递闭包有以下定义，其中关系由二元谓词表示：

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 的应用程序提供更好的语法。假设我希望能够为closure (→) x y 写x *(→)* y。问题是这个符号中的参数顺序与函数closure的参数顺序不匹配。

我认为使用\<index> 可能会有所帮助。不幸的是，Isabelle/Isar Reference Manual 中的\<index> 的文档非常简洁，我无法真正理解它。我用\<index> 玩了一下，但没有找到任何可行的解决方案。

让我感到困惑的是，从我收到的一些错误消息来看，\<index> 显然被翻译成⇘some_index⇙。我尝试使用⇘ℛ⇙ 标记基本关系应该去的位置，但这也不起作用。

【问题讨论】：

标签： syntax isabelle

【解决方案1】：

要切换参数，缩写是最好的选择。（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 参数，但语言环境通常效果更好。

【讨论】：

【解决方案2】：

您可能希望使用syntax 和translations，例如：

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

这些也记录在 isar-ref.pdf 中，一些示例在源理论文件中浮动（超搜索应该打开这些）。

【讨论】：