Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Sat, 20 Aug 1994 22:01:07 -0700
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9408210501.AA09642@ice.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: Useful(?) set thm available


I don't know if this is useful to anyone or not, but it seems like
it might be. I'm working alot with specs that I want to "execute"
via rewriting, and I use finite_sets for several objects in the system.

In order to define an "executable" (i.e. a constructive, recursive)
lookup function for finite sets, one needs a theorem like:

SEARCH_BY_KEY =
|- ?searchByKey.
    (!kf err k. searchByKey{}kf err k = err) /\
    (!s kf err k e.
      searchByKey(e INSERT s)kf err k =
      ((~validKeyFun(e INSERT s)kf) =>
       err |
       ((kf e = k) => e | searchByKey s kf err k)))

I have this theorem for (*)set's and key functions (*->**) (e.g. a
key function might be ProcState -> Pid). I used the same method
as the finite_sets authors' construction of the CARD function.

The validKeyFun predicate just says that it gives a unique value for
each element:

let validKeyFun = new_definition
  (`validKeyFun`,
   "validKeyFun (s:(*)set) (f:*->**) = (INJ f s (IMAGE f s))");;

Let me know if anyone would like this proof. 

Rob