A constructive proof of higman's lemma in Isabelle

Abstract

Higman's lemma, a specific instance of Kruskal's theorem, is an interesting result from the area of combinatorics, which has often been used as a test case for theorem provers. We present a constructive proof of Higman's lemma in the theorem prover Isabelle, based on a paper proof by Coquand and Fridlender. Making use of Isabelle's newly-introduced infrastructure for program extraction, we show how a program can automatically be extracted from this proof, and analyze its computational behaviour. © Springer-Verlag 2004.