Home
About
Submission Guidelines
Updating entries
Search
Index
Download

 

 

SourceForge.net Logo
project summary

 

Well-Quasi-Orders

Title: Well-Quasi-Orders
Author: Christian Sternagel (c-sterna /at/ jaist /dot/ ac /dot/ jp)
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.
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://afp.sf.net/entries/Well_Quasi_Orders},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Status: [ok] This is the development version, revision 9ce4a76615bb, of this entry, generated for Isabelle revision 0e70511cbba9. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

Proof outline
Proof document
Browse theories
Download this entry
Older releases: