Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Message-Id: <9207151820.AA09648@leopard.cs.uidaho.edu>
Subject: Re: Recursive definition over sets
To: info-hol@edu.uidaho.cs.ted (HOL Mailing List)
Date: Wed, 15 Jul 92 11:20:58 PDT
In-Reply-To: <10065.9207151716@frogland.inmos.co.uk>; from "David Shepherd" at Jul 15, 92 6:16 pm
Mailer: Elm [revision: 66.33]

> 
> Phil Weiss has said:
> > 
> > I was wondering about this just yesterday.  I could not think of a
> > way.  The only idea I had was to examine the way CARD was defined
> > in 'mk_sets.ml'.  I got another idea on how I could perform the
> > same operation without recursion, but instead using the @ operator.
> > 
> > I do not know how this will turn out.  I may have to go back and
> > define the operation using some form of recursion if it turns
> > out proofs using this definition are too difficult.
> 
> don't think that this is possible (assuming your using the infinite
> set theory) as consider
> 
> SUM I {x | T}
> 
> (not sure i've got the set syntax correct)
> 
> then the result of this is the sum of all numbers which you can prove to
> be greater than any number. but since its of type :num its 0 or SUC n for
> some n and hence you'd get a contradiction.
> 

I would attempt to do this the same way CARD is defined, which restricts
it's definition to those sets which are finite, i.e.

  FINITE s ==>
   blah blah blah

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