Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
我开始使用 Isabelle HOL,并想尝试构建某种组合证明。我一开始就采用了 Cayley 的公式。
这里是: 对于每个正整数 n,n 个标记顶点上的树数为 n^{n-2}。
在伊莎贝尔身上怎么会这样?我假设我必须定义树,但那又如何呢?
任何帮助或相关文章和/或代码将不胜感激!提前致谢
证明的想法是:
定义树(或使用任何现有的树)
按照纸质证明证明
card {tree. nodes tree = n \<and> canonical tree} = n ^ (n-2)
其中nodes给出了节点的数量,并且canonical是树被标准化的某种不变量(例如,你有正确的标签从 0 到 n-1)。
nodes
canonical
我已经尝试证明或定义任何东西,但我怀疑这在 Isabelle 中是一个很难开始的定理,因为我预计您将需要更多关于图的一般定理,或者您需要在双射上做很多工作,因为事实上节点被标记。