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
Least_Enum.thy
Description: application/example
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
