Well-Quasi-Orders

Title:	Well-Quasi-Orders
Author:	Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date:	2012-04-13
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 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:	[2012-06-11]: Added Kruskal's Tree Theorem. [2012-12-19]: 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. [2013-05-16]: Simplified construction of minimal bad sequences. [2014-07-09]: Simplified proofs of Higman's lemma and Kruskal's tree theorem, based on homogeneous sequences. [2016-01-03]: An alternative proof of Higman's lemma by open induction. [2017-06-08]: Proved (classical) equivalence to inductive definition of almost-full relations according to the ITP 2012 paper "Stop When You Are Almost-Full" by Vytiniotis, Coquand, and Wahlstedt.
BibTeX:	@article{Well_Quasi_Orders-AFP, author = {Christian Sternagel}, title = {Well-Quasi-Orders}, journal = {Archive of Formal Proofs}, month = apr, year = 2012, note = {\url{http://isa-afp.org/entries/Well_Quasi_Orders.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Abstract-Rewriting, Open_Induction
Used by:	Decreasing-Diagrams-II, Myhill-Nerode, Polynomials, Saturation_Framework, Saturation_Framework_Extensions
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry