Maximum Cardinality Matching

A matching in a graph G is a subset M of the edges of G such that no two share an endpoint. A matching has maximum cardinality if its cardinality is at least as large as that of any other matching. An odd-set cover OSC of a graph G is a labeling of the nodes of G with integers such that every edge of G is either incident to a node labeled 1 or connects two nodes labeled with the same number i ≥ 2. Theorem 1 (Edmonds [2]). Let M be a matching in a graph G and let OSC be an odd-set cover of G. For any i ≥ 0, let ni be the number of nodes labeled i. If |M | = n1 + i≥2 bni/2c then M is a maximum cardinality matching. We provide an Isabelle proof of Edmonds theorem. For an expla