入门Isabelle HOL：如何构建Cayley公式的组合证明？

很高兴看到你用Isabelle HOL来形式化Cayley公式——这是个非常经典的组合数学结果，很适合入门形式化证明！下面我会一步步带你走，从基础定义到完整证明的核心步骤，还会给你可复用的代码片段。

第一步：利用Isabelle自带的图论库，避免重复造轮子 #

Isabelle的HOL-Library里已经有成熟的图论定义，包括树的核心属性（连通、无环），完全不用从零开始搭建。你只需要导入这个库：

theory Cayley_Proof
  imports HOL.Graph_Theory
begin

这个库已经帮你定义好了：

• graph：通用图类型（顶点支持任意类型，边是顶点对）
• tree：树的谓词（判定无向图是否连通且无环，顶点数≥1）
• 大量辅助定理，比如“树的边数=顶点数-1”“树至少有两个叶子节点”等，都可以直接调用。

第二步：明确Cayley公式的形式化表述 #

Cayley公式的核心是“n个标记顶点的树的数量为n^(n-2)”，在Isabelle里可以这样精准表述：

theorem cayley_formula:
  fixes n :: nat
  assumes "n ≥ 1"
  shows "card {G. tree G ∧ vertices G = {0..<n}} = n^(n-2)"

这里用{0..<n}作为n个标记顶点的集合，你也可以换成任意大小为n的有限集（比如finite V ∧ card V = n），不过自然数区间更直观易操作。

第三步：选择Prüfer序列作为证明核心 #

最适合形式化的Cayley证明方法是Prüfer序列双射法：每个n顶点的树对应唯一长度为n-2的Prüfer序列，反过来每个序列也对应唯一的树。只要证明这个对应是双射，就能直接推出树的数量等于序列的数量（即n^(n-2)）。

3.1 定义Prüfer序列的生成函数 #

从树生成Prüfer序列的步骤很清晰：

1. 找到树中最小的叶子节点（度数为1的顶点）
2. 记录它的邻居，然后移除这个叶子节点
3. 重复直到剩下2个顶点，得到的序列就是Prüfer序列

对应的Isabelle实现：

fun prufer_sequence :: "'a graph ⇒ 'a list" where
  "prufer_sequence G = (if card (vertices G) ≤ 2 then []
    else let
      leaves = {v ∈ vertices G. degree G v = 1};
      min_leaf = Min leaves;
      neighbor = the (neighbors G min_leaf);
      G' = delete_vertex min_leaf G
    in neighbor # prufer_sequence G')"

注：树的顶点数>2时必然存在叶子节点，所以Min leaves合法；叶子节点只有一个邻居，the (neighbors G min_leaf)不会出错。

3.2 定义Prüfer序列的逆函数 #

从序列生成树的步骤：

1. 初始化每个顶点的度数：序列中出现k次的顶点度数为k+1，其余为1
2. 找到最小的度数为1的顶点v，把它和序列第一个元素u连边，然后v和u的度数各减1
3. 移除序列第一个元素，重复直到序列为空，最后把剩下的两个度数为1的顶点连边

简化版的Isabelle定义（实际形式化时可借助辅助函数跟踪度数，避免重复计算）：

fun prufer_to_tree :: "'a list ⇒ 'a set ⇒ 'a graph" where
  "prufer_to_tree [] V = (if card V = 2 
    then let {u, v} = V in add_edge (empty_graph V) (u, v) 
    else empty_graph V)"
| "prufer_to_tree (u#us) V = (let
    deg = λv. count_list (u#us) v + 1;
    min_leaf = Min {v ∈ V. deg v = 1};
    G' = add_edge (empty_graph V) (min_leaf, u)
  in prufer_to_tree us V)"

3.3 证明双射关系 #

这是核心环节，需要证明两个关键性质：

1. 对任意树G，prufer_to_tree (prufer_sequence G) (vertices G) = G（逆函数能还原原树）
2. 对任意长度为n-2的序列s（元素来自大小为n的集合V），prufer_sequence (prufer_to_tree s V) = s（生成函数能还原原序列）

你可以用归纳法完成证明，比如先证明序列长度的正确性：

lemma prufer_sequence_length:
  fixes G :: "'a graph"
  assumes "tree G"
  shows "length (prufer_sequence G) = card (vertices G) - 2"
  using assms
  apply (induction rule: tree_induct) -- 调用树的专用归纳规则
  apply auto
done

第四步：完成Cayley公式的证明 #

当你确认Prüfer序列和树是双射关系后，就可以直接推导结论：

theorem cayley_formula:
  fixes n :: nat
  assumes "n ≥ 1"
  shows "card {G. tree G ∧ vertices G = {0..<n}} = n^(n-2)"
proof -
  let ?V = "{0..<n}"
  let ?Trees = "{G. tree G ∧ vertices G = ?V}"
  let ?Sequences = "{s ∈ ?V list. length s = n - 2}"
  
  -- 证明树和序列之间存在双射
  define f where "f = λG. prufer_sequence G"
  define g where "g = λs. prufer_to_tree s ?V"
  
  have "bij_betw f ?Trees ?Sequences"
    apply (rule bij_betw_byWitness)
    apply (simp add: f_def g_def)
    apply (metis 你之前证明的逆函数正确性引理)
    apply (metis prufer_sequence_length assms)
    done
  
  -- 计算序列的数量：n^(n-2)
  have "card ?Sequences = n^(n-2)"
    using assms
    apply (simp add: card_list_length) -- 长度为k的序列数量为 (card V)^k
    done
  
  -- 双射的集合大小相等
  thus ?thesis
    using bij_betw_same_card[OF `bij_betw f ?Trees ?Sequences`]
    by simp
qed

实用提示与参考资源 #

• Isabelle内置证明：Isabelle的HOL-Library里已经有完整的Cayley公式证明，路径是HOL/Graph_Theory/Cayley.thy，直接打开学习是最快的入门方式。
• 自动化工具：证明过程中多使用auto、simp、metis等自动化命令，能大幅减少手动推导的工作量；树的归纳可以直接用tree_induct规则。
• 组合数学库：可以参考HOL/Combinatorics库，里面有很多计数相关的引理，能帮你简化数量计算步骤。

内容的提问来源于stack exchange，提问作者Eva