Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Date: Tue, 23 Nov 1993 23:07:07 -0800
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9311240707.AA20685@mahogany.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Subject: Need "an undefined value", but not what you think.


I may eventually need to denote "an undefined value" in HOL, in 
such a way that it isn't even reflexive. This is not as strange
as it sounds. For instance,

 does 23/0 = 22/0 ?

In certain circles the answer is arguably "maybe", in the sense
that you shouldn't be able to prove or disprove the above equality.
My concern is with elements "beyond" the end of a list, such as 

 (EL 9 [1;2;3])

It turns out this is provably equal to (EL 10 [0;1;2;3]), as the
theorem

 ! lst i e. (EL i lst) = (EL (SUC i) (CONS e list))

has a one-line proof. Why is (EL 9 [1;2;3]) equal to some term 
other than itself? 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])? I want
to eventually work with a version of lists such that indexing 
beyond the end of one is "an undefined value" in the way that
12/0 is "an undefined value". But I can't just define myEL to be 
something like

myEL i l = (i in bounds) => (EL i l) | UNDEF

because UNDEF = UNDEF, which is not what I want. Is there any way
for me to define lists such that (EL 9 [1;2;3]) can be proved
neither equal nor unequal to any term that is not (EL 9 [1;2;3]) ??

Thanx!

Rob Shaw