Well Quasi Orders
Well-Quasi-Orders. 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.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Sternagel, Christian: A mechanized proof of Higman’s lemma by open induction (2020)
- Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
- Sternagel, Christian; Thiemann, René: Formalizing Knuth-Bendix orders and Knuth-Bendix completion (2011)