Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 1 Jun 1993 10:52:18 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05723;
          Tue, 1 Jun 93 02:10:19 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA05718;
          Tue, 1 Jun 93 02:10:13 -0700
Received: by infix.cs.ruu.nl id AA05410 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Tue, 1 Jun 1993 11:10:25 +0200
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199306010910.AA05410@infix.cs.ruu.nl>
Subject: Anybode has (Generalized) Min and Max function?
To: info-hol@ted.cs.uidaho.edu (hol mailing list)
Date: Tue, 1 Jun 1993 11:10:25 +0100 (METDST)
X-Mailer: ELM [version 2.4 PL21]
Content-Type: text
Content-Length: 720

Hi,

I may need the following two finctions. Let V be a predicate defining
a subset of Nat_Inf, ie Nat extended with a special value inf which is
defined to be larger than any values in Nat.

    GMIN P = the least element of P if it is non-empty,
             inf else.

    GMAX P = the greatest element of P if one exists,
             else if no such element exists and P is non-empty then inf,
             else if P empty then 0

This is a generalization of the binary MIN and MAX defined in the
more_arithmatic library. 

Does anybody already has the code that defines something like above
and proves their basic properties? I'll be very gratefull if you are
willing to share the code with me.

Thank you.

Wishnu