[isabelle] New AFP entry: Well-Quasi-Orders by Christian Sternagel
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Well-Quasi-Orders by Christian Sternagel
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Sun, 22 Apr 2012 11:25:15 +0200
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:11.0) Gecko/20120327 Thunderbird/11.0.1
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