试图理解 Isabelle/HOL 中的“语法”关键字答案

【问题标题】：Trying to understand "syntax" keyword in Isabelle/HOL试图理解 Isabelle/HOL 中的“语法”关键字
【发布时间】：2017-11-11 01:02:37
【问题描述】：

我正在尝试了解 Isabelle/HOL 中线性逻辑的实现：https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html syntax 关键字代表什么，代码是什么意思：

syntax
  "_Trueprop" :: "single_seqe" ("((_)/ ⊢ (_))" [6,6] 5)
  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")

在哪里可以找到syntax 关键字的文档？我在计算机科学第 828 卷讲义中找到了关于 infixr 和翻译规则的详尽文档。但我找不到关于 syntax 的类似文档。

【问题讨论】：

标签： syntax isabelle

【解决方案1】：

参考手册第 8.5.2 节（自 Isabelle 2016-1 起）中对此进行了描述：“原始语法和翻译”。

那里的第一行意味着添加一个语法规则，说明P ⊢ Q 解析为_Trueprop P Q。 ILL.thy 的下一行给出了 parse_translation，稍后在参考手册的同一部分中进行了描述。这个翻译告诉 Isabelle 将 _Trueprop 翻译成 K (single_tr Trueprop) 并且 Trueprop 在文件顶部被声明为未解释的常量。你会看到还有一个print_translation，它控制着漂亮的打印机。

【讨论】：