如何在 Isabelle 中使用附加参数定义活页夹的语法？

Question

我想在 Isabelle 中定义一个语法结构，其形式为 c ? x. p，其中 c 和 p 是值，x 是变量。此构造应转换为 Input c (λx. p)。这似乎无法通过 binder 注释来完成，因为此构造有一个额外的参数 c，而且不能绑定多个变量。我如何定义这样的结构？

Answer 1

这可以使用低级 syntax 和 translations 工具实现。假设 c 的类型为 channel，p 和 Input c (λx. p) 的类型为 process，并且所需的优先级为 100，则可以定义构造如下：

syntax
  "_Input" :: "channel ⇒ pttrn ⇒ process ⇒ process"
  ("(3_ ? _./ _)" [101, 0, 100] 100)
translations
  "c ? x. P" ⇌ "CONST Input c (λx. P)"

这些类型的语法定义在 Isabelle/Isar 参考手册的第 8.2.1 小节中进行了描述。要理解上述解决方案，查看第 8.2.2 和 8.2.3 小节可能会有所帮助，它们部分解释了更高级别的 infix、infixl、infixr、和 binder 构造可以被翻译成低级定义。此外，查看 $ISABELLE_HOME/src/HOL/Set.thy 中集合理解构造的定义可能会有用。

如何在 Isabelle 中使用附加参数定义活页夹的语法？

How can I define syntax for a binder with an additional argument in Isabelle?

syntax

isabelle