Abstract

Based on Isabelle/HOL's type class for preorders, we introduce a type class for well-quasi-orders (wqo) which is characterized by the absence of "bad" sequences (our proofs are along the lines of the proof of Nash-Williams, from which we also borrow terminology). Our two main results are instantiations for the product type and the list type, which (almost) directly follow from our proofs of (1) Dickson's Lemma and (2) Higman's Lemma. More concretely:

• If the sets A and B are wqo then their Cartesian product is wqo.
• If the set A is wqo then the set of finite lists over A is wqo.

BibTeX

@incollection{CS-AFP12a,
  author      = "Christian Sternagel",
  title       = "Well-Quasi-Orders",
  booktitle   = "The Archive of Formal Proofs",
  editor      = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher   = "\url{http://afp.sf.net/entries/Well_Quasi_Orders.shtml}",
  year        = 2012,
  month       = apr,
  note        = "Formal proof development"
  ISSN        = "2150-914x",
}