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

Question

我正在努力理解 some Isabelle code，但有些语法我不明白。我没有在教程中看到它们，包括与 Isabelle2017 发行版捆绑在一起的两个 "Programming and Proving in Isabelle/HOL" 和 "The Isabelle/Isar Reference Manual"。事实上，它们是符号，再加上 Isabelle 的用户群非常小，这意味着答案非常不 google-able。

第一个是高尖括号 ⟨ ⟩，第二个是双星号 **，它在输出控制台中呈现为 ∧*（值得注意的是不同于 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/jEdit，您可以按Ctrl（Cmd for Mac) 并单击语法和名称以跳转到它们的定义站点（参见 Isabelle/jEdit Manual 的 3.5）。

有零星的instances where this might not work. Then, you can try typing print_syntax into your theory text, which will output all rules of the current inner syntax configuration (cf. 8.4.4 of Isabelle/Isar Reference Manual)。希望您至少可以通过此弄清楚某些符号来自哪个理论。人们应该假设仁慈的理论作者会避免破坏超链接功能的语法设置。

针对这里的具体问题，**是https://github.com/pirapira/eth-isabelle/blob/master/sep_algebra/Separation_Algebra.thy#L108 and ⟨ _ ⟩ is sugar for pure from https://github.com/pirapira/eth-isabelle/blob/master/Hoare/Hoare.thy#L257, as 中sep_conj的语法糖。

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

In Isabelle, what do the angle brackets and double asterisks mean?

formal-verification

theorem-proving

isabelle

isar