[isabelle] New AFP entry: Well-Quasi-Orders by Christian Sternagel

Christian Sternagel

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 two main results are instantiations for
the product type and the list type, which (almost) directly follow from our
proofs of (1) Dickson's Lemma and (2) Higman's Lemma. 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 its finite subsets is wqo.

The research was funded by the Austrian Science Fund (FWF): J3202.


Note that this entry is only available in the development version (until the

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.