Proof Pearl: The Marriage Theorem
We describe two formal proofs of the finite version of Hall's Marriage
Theorem performed with the proof assistant Isabelle/HOL, one by Halmos
and Vaughan and one by Rado. The distinctive feature of our
formalisation is that instead of sequences (often found in statements
of this theorem) we employ indexed families, thus avoiding tedious
reindexing of sequences.
pdf
BibTeX:
@inproceedings{JiangN-CPP11,
author={Dongchen Jiang and Tobias Nipkow},
title={Proof Pearl: The Marriage Theorem},
booktitle={Certified Programs and Proofs (CPP 2011)},
editor={Jouannaud and Shao},
publisher=Springer,series=LNCS,volume={7068},pages={394-399},year=2011}