[isabelle-dev] enumerating infinite sets of well-ordered elements
Christian Sternagel
c.sternagel at gmail.com
Wed Jun 12 09:05:54 CEST 2013
Dear all,
I find myself considering the following cases every now and then:
1) If we know that some property P is true for infinitely many elements
of a well-ordered set (all my use-cases so far, just concern natural
numbers) it is in principle trivial to enumerate them in increasing
order. Thus it should also be trivial to do so in Isabelle.
2) For a well-ordered set of elements and a fixed element N, assume that
for every i >= N there is a j > i, s.t., the predicate P i j holds. Thus
it is in principle trivial to construct a chain f, s.t., for all i, we
have P (f i) (f (Suc i)) and "f i < f (Suc i)". Again this should be
trivial in Isabelle.
Why not add corresponding functions and lemmas to the library?
Please find attached a theory that handles these cases. The names of the
locales are not ideal (please provide better ones ;)). Note that the
first locale "infinitely_many1" is a generalization of "infinitely_many"
from theory Seq of the AFP entry Abstract-Rewriting. Currently the
attached theory is part of AFP/Well-Quasi-Orders.
cheers
chris
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Least_Enum.thy
Type: application/x-example
Size: 2218 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130612/cb676d85/attachment.bin>
More information about the isabelle-dev
mailing list