Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Fri, 24 Mar 1995 12:36:22 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199503240236.MAA29553@vega.anu.edu.au>
To: info-hol@leopard.cs.byu.edu, shaw@cs.ucdavis.edu
Subject: Re: HOL sets


Rob Shaw writes:

>  ......
>  It sounds as if aci has proven that this always works when the function
>  is commutative and associative over the set elems?

Actually, the aci package gives a really nice theorem which is probably
one of the very few significant mathematical facts that have been first
enunciated with the help of a proof assistant such as HOL.  I have called
it Chou's Theorem and refer to it as such whenever talking or writing about
lifting binary operators to act over sets.  Ching Tsun showed that there
is a unique function that lifts any assocociative, commutative operator
(with identity) to act over an index set.

CHOU'S THEOREM

    ?! OP.  !op id. (  !a b c. op a (op b c) = op (op a b) c  /\
                       !a b. op a b = op b a  /\
                       !a. op a id = a  )
                    ==>  !f. (OP op id) f {} = id  /\
                         !f x S. (OP op id) f (x INSERT S)
                                     =  (x IN S) =>   (OP op id) f S
                                                  |   op (f x) ((OP op id) f S)

(The hypothesis says that op is associative & commutative and that id is its
 identity.  (OP op id) is the operator obtained by lifting it to operate over
 an index set.)

In the case that the binary operator to be lifted does not have an identity,
then the situation is not so elegant but is similar.  (You don't get unique
existence and the base case for the recursive expression of the lifted operator
says what happens on a singleton index set rather than the empty set.)

Malcolm