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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
