[isabelle-dev] Sup{} for type nat

[Lawrence Paulson]

We provide the functions Sup (supremum) and Max (maximum). I am pretty sure that the Max of a set should be an element of that set and therefore we properly do not define Max{}. However, the supremum of a set merely needs to be an upper bound and therefore we should define Sup{} = 0 for the natural numbers. I have tried making this change and it is possible to build Main without any other changes, but it’s clear that a dozen or two proofs are likely to break elsewhere.

I can do this, but would anybody like to comment on whether it is appropriate? It would certainly be convenient to be able to refer to Sup S regardless of whether S is empty.

Larry