[isabelle-dev] Sup{} for type nat

[Tobias Nipkow]

I would have liked something like that on more than one occasion.

Tobias

On 12/05/2020 16:41, Lawrence Paulson wrote:
> 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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200512/dcc38461/attachment.bin>