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.
License
History
- June 8, 2017
- 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.
- January 3, 2016
- An alternative proof of Higman's lemma by open induction.
- July 9, 2014
- Simplified proofs of Higman's lemma and Kruskal's tree theorem,
based on homogeneous sequences.
- May 16, 2013
- Simplified construction of minimal bad sequences.
- December 19, 2012
- 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.
- June 11, 2012
- Added Kruskal's Tree Theorem.
Topics
Session Well_Quasi_Orders
- Infinite_Sequences
- Minimal_Elements
- Least_Enum
- Almost_Full
- Minimal_Bad_Sequences
- Higman_OI
- Almost_Full_Relations
- Well_Quasi_Orders
- Kruskal
- Kruskal_Examples
- Wqo_Instances
- Multiset_Extension
- Wqo_Multiset