[isabelle-dev] enumerating infinite sets of well-ordered elements

[Christian Sternagel]

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>