Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: the sets and pred_sets libraries.
Date: Thu, 23 Jan 92 17:41:54 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.297:23.00.92.17.42.17"@cl.cam.ac.uk>

Regarding my previous message:

> The point of this post is to ask if anyone uses the theorems about
> the properties of functions expressed in pred_sets by the constants:
>
>   -->, -->>, >-->, <-->, ...etc
>
> If so, then I suppose this stuff from pred_sets will have to be
> rewritten, not to mention incorporated into the sets library as well.

enough users have asked for the retention of this stuff for something
like it to be installed in both sets and pred_sets.  I have therefore
added to the sets library the following definitions of injective (>-->)
and surjective (-->>) functions:

    INJ_DEF =
    |- !f s t.
        INJ f s t =
        (!x. x IN s ==> (f x) IN t) /\
        (!x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y))

    SURJ_DEF =
    |- !f s t.
        SURJ f s t =
        (!x. x IN s ==> (f x) IN t) /\
        (!x. x IN t ==> (?y. y IN s /\ (f y = x)))

The function f in these definitions has type :*->**, rather than the
type *->* originally used in the corresponding definitions of >--> and
-->>.  A bijection (used to be "<-->" in pred_sets) is now defined by:

    BIJ_DEF = |- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t

And the theorems about inverses have been replaced by the definitions
(actually, constant specifications) of a left inverse function LINV:

    LINV_DEF = |- !f s t. INJ f s t ==> (!x. x IN s ==> (LINV f s(f x) = x))

and a right inverse function RINV:

    RINV_DEF = |- !f s t. SURJ f s t ==> (!x. x IN t ==> (f(RINV f s x) = x))

Most of the theorems about >-->, -->> and <--> in the old pred_sets
library now have analogues about the new functions INJ, BIJ, and SURJ
in the sets library.

This, I expect, is how matters will stand in the next release of the
system.  That is, the above definitions (and some theorems that follow
from them) will be installed in the sets library (and documented).
The library pred_sets will then be made exactly parallel to sets, with
the same names for theorems and an almost identical manual.

If there are any objections/suggestions, please let me know right away.

Thanks,
Tom