在Isabelle中，尖括号和双星号是什么意思？

Question

我想了解some Isabelle code，并且有一些我不理解的语法。我没有在教程中看到它们，包括与Isabelle2017发行版捆绑的两个，“Isabelle / HOL中的编程和证明”和“Isabelle / Isar参考手册”。事实上，他们是符号，再加上Isabelle非常小的用户群，这意味着答案非常不具备google功能。

第一个是高角括号⟨ ⟩，第二个是双星号**，它在输出控制台中呈现为∧*（与ASCII ^明显不同）。

这是一个example;

lemma pre_fifth_pure [simp]:
  "triple net failures (a ** b ** c ** d ** ⟨ P ⟩) cod post =
   (P ⟶ triple net failures (a ** b ** c ** d) cod post)"

尖括号似乎总是围绕着一个命题。 triple函数的定义暗示(a ** b ** c ** d)是state_element set ⇒ bool类型，其中state_element只是一堆构造函数的结合;

datatype state_element =
    StackHeightElm "nat"
  | StackElm "nat * w256" ... (* 20 lines like this *)

这两个语法是否相关？ (a ** b ** c ** d)怎么可能成为一个功能？为什么它有不同数量的星星划分的东西？这是以某种方式自定义语法吗？这些奥秘比比皆是。

Answer 1

Isabelle提供了丰富的机制来定义自己的符号。因此，当人们检查他人写的理论时，遇到不熟悉的语法是很常见的。

使用Isabelle / jEdit，您可以按Ctrl键（Cmd for Mac）并单击语法和名称以跳转到其定义站点（参见Isabelle/jEdit Manual的3.5）。

有零星的instances，这可能不起作用。然后，您可以尝试在理论文本中键入print_syntax，它将输出当前内部语法配置的所有规则（参见Isabelle/Isar Reference Manual的8.4.4）。希望你至少能够找出一些符号来自哪个理论。人们应该假设仁慈的理论作者会避免破坏超链接功能的语法设置。

对于这里的具体问题，**是sep_conj中https://github.com/pirapira/eth-isabelle/blob/master/sep_algebra/Separation_Algebra.thy#L108的语法糖，而⟨ _ ⟩是来自pure的https://github.com/pirapira/eth-isabelle/blob/master/Hoare/Hoare.thy#L257的糖，如Alex found out。