Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: info-hol@edu.uidaho.cs.ted (HOL Mailing List)
Subject: Re: Recursive definition over sets
In-Reply-To: Your message of Wed, 15 Jul 92 11:20:58 -0700. <9207151820.AA09648@leopard.cs.uidaho.edu>
Date: Wed, 15 Jul 92 23:43:52 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.377:15.06.92.22.44.04"@cl.cam.ac.uk>


One approach is to prove that a finite set can be put in bijection with 

  {m:num| m < n} 

for some n. (I think this is proved somewhere in the CARD section of the sets 
library.) It is straightforward to define the sum over the indexing set of 
natural numbers using normal primitive recursive definitions. Proving this is 
independent of the ordering is possible by induction; in fact I have done this 
for the special case of sums of real numbers:

  |- !n p. (!y. y < n ==> ?!x. x < n /\ (p(x) = y))
              ==> !f. Sum(0,n)(\n. f(p n)) = Sum(0,n) f

[I define Sum(0,SUC n) f = f(0) + f(1) + ... + f(n); Sum(0,0) = 0. Think
 of p as a permutation of {m:num| m < n}]

The result can then be transferred to the sets you are interested in.

Probably the result would say something like, combining the two previous
examples from Ching Tsun and Phil Weiss:

  |- ?SUM. !f S. FINITE S ==> (SUM f {} = 0) /\
                              (SUM f (x INSERT S) = (x IN S) =>
                                        (SUM f S) | (f x + SUM f S))

In doing this generically, you would have to address the issue of whether the
operation is meaningful for the null set (sums obviously are, but "max" and
"min" arguably aren't). If there's no neutral element then you would probably
add "~(S = NULL)" to the precondition. If on the other hand you do have some
neutral "0" for the operation (i.e. |- !x. 0 + x = x), you could meaningfully
weaken the precondition to "FINITE (S INTERSECT {x | ~(f(x) = 0)})" in the
above theorem.

Maybe someone else can think of a more elegant solution.

John.