[isabelle-dev] Sup{} for type nat

[Klein, Gerwin (Data61, Kensington NSW)]

Yes, that makes sense to me.

Cheers,
Gerwin

> On 12 May 2020, at 23:01, Peter Lammich <lammich at in.tum.de> wrote:
> 
> 
> Same here. I remember having run into this a few times.
> 
> If we see nat as a semi-lattice, we get a natural definition for finite
> Sup's, "Sup S = fold sup S 0", which precisely matches the 
> "Sup {} = 0".
> 
> --
>  Peter
> 
> On Tue, 2020-05-12 at 16:43 +0200, Tobias Nipkow wrote:
>> 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
>>> 
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev