Isabelle combinatoric proof Cayley's formula

Question

I am getting started with Isabelle HOL and want to try to construct a combinatorial proof of some kind. I took Cayley's formula for the start.

Here it is: For every positive integer n, the number of trees on n labeled vertices is n^{n-2}.

How would one work wit something like that in Isabelle? I am assuming I will have to define trees, but then what?

Any help or related articles and or codes would be very much appreciated! Thanks in advance

Answer 1

The idea of the proof would be:

1. define trees (or use any existing one)

2. follow a paper proof by that proves that

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

where nodes gives the number of nodes and canonical is some kind of invariant that the tree is normalized (e.g., you have correct labels going from 0 to n-1).

I have tried proving or defining anything, but I suspect that this is a hard theorem to start with in Isabelle, because I expect that you will need either more general theorems on graphs or you will need to work a lot on bijection due the fact that the node are labeled.