Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <11087-0@swan.cl.cam.ac.uk>; Fri, 17 Jul 1992 23:11:06 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17009;
          Fri, 17 Jul 92 14:56:47 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from leopard.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA17004; Fri, 17 Jul 92 14:56:41 -0700
Received: by leopard.cs.uidaho.edu (16.7/1.34) id AA00457;
          Fri, 17 Jul 92 14:59:49 -0700
From: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Message-Id: <9207172159.AA00457@leopard.cs.uidaho.edu>
Subject: More help on recursion over sets
To: info-hol@edu.uidaho.cs.ted (HOL Mailing List)
Date: Fri, 17 Jul 92 14:59:49 PDT
Mailer: Elm [revision: 66.33]

Nope, our discussion isn't over yet.

I have a function which is part of my state.

 foo = (\x:*. ARB:**)

This function is updated with each iteration of state.
It was easy to define a function change_foo_sing.

 change_foo_sing = (\(foo:*->**) (new_x:*).
    (\x. (x = new_x) => (new_value) | (foo x)))

I must be able to get

 (change_foo foo {} = foo) /\
 (change_foo foo (x INSERT x_set) = change_foo (change_foo_sing x) x_set)

somehow.

The previous discussion and the definition of CARD seem to be of no help,
because both depend on recursion over numbers, while this situation
doesn't involve numbers at all.

If anyone has any pointers at all as to how I could go about this,
I would be grateful.  Otherwise, I will probably take a week or
so bumbling around before I will find anything.

Thanks.

Phil.
--
Philip Weiss	Laboratory for Applied Logic	weiss@leopard.cs.uidaho.edu
(Disclaimer: My views are not their views)	weiss872@snake.cs.uidaho.edu