Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <1532.9311241135@frogland.inmos.co.uk>
Subject: Re: Need "an undefined value", but not what you think.
To: Paul.Curzon@cl.cam.ac.uk (Paul Curzon)
Date: Wed, 24 Nov 1993 11:35:15 +0000 (GMT)
Cc: info-hol@cs.uidaho.edu (info-hol mailing list)
In-Reply-To: <"swan.cl.cam.:057860:931124113057"@cl.cam.ac.uk> from "Paul Curzon" at Nov 24, 93 11:30:26 am
Content-Type: text
Content-Length: 1445

Paul Curzon has said:
> Ooops: a correction to what I just said

....

> >For EL what needs to be done is instead of (in HOL90 syntax) the
> >definition:
> >
> >val EL = new_recursive_definition
> >      {name = "EL",
> >       fixity = Prefix,
> >       rec_axiom = num_Axiom,
> >       def = --`(!l. EL 0 l = (HD l:'a)) /\
> >                (!l:'a list. !n. EL (SUC n) l = EL n (TL l))`--};
> 
> 
> How does this help in the example given? You still have the clause:
> 
>  EL (SUC n) l = EL n (TL l))
> 
> so
>    EL 10 [0;1;2;3] = EL (SUC 9) [0;1;2;3]
>                    = EL 9 (TL [0;1;2;3])
>                    = EL 9 [1;2;3]

I think another correction is in order ... what you have quoted is 
my copying the current definition which I precede by saying "instead of
this" and follow with the alternative I'm suggesting.

However, my alternative still "suffers" from

|- EL 10 [0,1,2,3] = EL 9 [1,2,3]

However I think *this* is reasonable. Also

|- ! a b c d x y z. EL 10 [a,b,c,d] = EL 9 [x,y,z]

which, perhaps could be claimed to be less reasonable. However it does 
ensure

~|- EL 10 [1,2,3] = EL 9 [1,2,3]

which was the main original intent.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"you might think that   ---   I couldn't possibly comment"