
WellQuasiOrders
Title: 
WellQuasiOrders 
Author:

Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)

Submission date: 
20120413 
Abstract: 
Based on Isabelle/HOL's type class for preorders,
we introduce a type class for wellquasiorders (wqo)
which is characterized by the absence of "bad" sequences
(our proofs are along the lines of the proof of NashWilliams,
from which we also borrow terminology). Our main results are
instantiations for the product type, the list type, and a type of finite trees,
which (almost) directly follow from our proofs of (1) Dickson's Lemma, (2)
Higman's Lemma, and (3) Kruskal's Tree Theorem. 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.
 If the set A is wqo then the set of finite trees over A is wqo.
The research was funded by the Austrian Science Fund (FWF): J3202. 
Change history: 
[20120611]: Added Kruskal's Tree Theorem.
[20121219]: New variant of Kruskal's tree theorem for terms (as opposed to
variadic terms, i.e., trees), plus finite version of the tree theorem as
corollary.
[20130516]: Simplified construction of minimal bad sequences.
[20140709]: Simplified proofs of Higman's lemma and Kruskal's tree theorem,
based on homogeneous sequences.
[20160103]: An alternative proof of Higman's lemma by open induction.
[20170608]: Proved (classical) equivalence to inductive definition of
almostfull relations according to the ITP 2012 paper "Stop When You Are
AlmostFull" by Vytiniotis, Coquand, and Wahlstedt. 
BibTeX: 
@article{Well_Quasi_OrdersAFP,
author = {Christian Sternagel},
title = {WellQuasiOrders},
journal = {Archive of Formal Proofs},
month = apr,
year = 2012,
note = {\url{http://isaafp.org/entries/Well_Quasi_Orders.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
AbstractRewriting, Open_Induction 
Used by: 
DecreasingDiagramsII, MyhillNerode 
