Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 24 Nov 1993 11:02:42 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02228;
          Wed, 24 Nov 1993 03:43:39 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA02224;
          Wed, 24 Nov 1993 03:42:51 -0700
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA06576; Wed, 24 Nov 93 02:40:33 -0800
Received: from coot.cl.cam.ac.uk (user pc (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 24 Nov 1993 10:39:48 +0000
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@cs.uidaho.edu, Paul.Curzon@cl.cam.ac.uk
Subject: Re: Need "an undefined value", but not what you think.
In-Reply-To: Your message of "Tue, 23 Nov 93 23:07:07 PST." <9311240707.AA20685@mahogany.cs.ucdavis.edu>
Date: Wed, 24 Nov 93 10:39:32 +0000
From: Paul Curzon <Paul.Curzon@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:035870:931124104005"@cl.cam.ac.uk>

> It is not as undefined as I would like! Is 
> it somehow equal to (EL 9 [2;3;4]) or to (EL 8 [1;2;3])?


From the definition is as it is you can not prove or disprove the
above - you have no information about ithem.

If you dont want:

|- (EL 9 [1;2;3]) = (EL 8 [2;3])

You could define a new version of EL (say WOMBAT) using
new_specification to include the in bounds restriction:

val wombat = prove(
(--`
?WOMBAT. !n l. n <= LENGTH (l:'a list) ==> (WOMBAT n l = EL n l)`--),

EXISTS_TAC (--`EL:num->'a list->'a`--) THEN
REWRITE_TAC[]
);
val wombat = |- ?WOMBAT. !n l. n <= LENGTH l ==> (WOMBAT n l = EL n l) : thm


- new_specification
{consts = [{const_name = "WOMBAT", fixity = Prefix}],
           name = "WOMBAT", sat_thm = wombat};

val it = |- !n l. n <= LENGTH l ==> (WOMBAT n l = EL n l) : thm
 

If n is in bounds then WOMBAT is the same as EL. If it is out of
bounds, all you can prove is eg

|- F ==> (WOMBAT 9 [1;2;3] = EL 9 [1;2;3])

|- F ==> (WOMBAT 8 [2;3] = EL 8 [2;3])

ie
|- (WOMBAT 9 [1;2;3] ~= EL 9 [1;2;3])
|- (WOMBAT 8 [2;3] ~= EL 8 [2;3])

Thus now all you know is what they are not equal to (if that is
any better).

Paul Curzon.