Yes, that makes sense to me. Cheers, Gerwin
> On 12 May 2020, at 23:01, Peter Lammich <[email protected]> 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 >>> [email protected] >>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev >>> >> >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
