[isabelle-dev] Sup{} for type nat

[Peter Lammich]

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