isabelle - 伊莎贝尔组合证明凯莱公式

Question

我开始使用 Isabelle HOL，并想尝试构建某种组合证明。我一开始就采用了 Cayley 的公式。

这里是： 对于每个正整数 n，n 个标记顶点上的树数为 n^{n-2}。

在伊莎贝尔身上怎么会这样？我假设我必须定义树，但那又如何呢？

任何帮助或相关文章和/或代码将不胜感激！提前致谢

标签： isabellehol

Answer 1

证明的想法是：

1. 定义树（或使用任何现有的树）

2. 按照纸质证明证明

card {tree. nodes tree = n \<and> canonical tree} = n ^ (n-2)

其中nodes给出了节点的数量，并且canonical是树被标准化的某种不变量（例如，你有正确的标签从 0 到 n-1）。

我已经尝试证明或定义任何东西，但我怀疑这在 Isabelle 中是一个很难开始的定理，因为我预计您将需要更多关于图的一般定理，或者您需要在双射上做很多工作，因为事实上节点被标记。