Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 24 Nov 1992 10:20:38 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08653; Tue, 24 Nov 92 01:57:53 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08648; Tue, 24 Nov 92 01:57:24 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Tue, 24 Nov 1992 09:56:25 +0000 To: toal@edu.ucla.cs (Ray J. Toal) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: list theorems with destructors In-Reply-To: Your message of Mon, 23 Nov 92 21:09:57 -0800. <9211240509.AA23292@hapuna.cs.ucla.edu> Date: Tue, 24 Nov 92 09:56:18 +0000 From: Richard Boulton Message-Id: <"nene.cl.ca.120:24.11.92.09.56.27"@cl.cam.ac.uk> Ray, you ask whether the following is a theorem in HOL: "!n s1 s2. (n = HD s2) /\ (s1 = TL s2) ==> (s2 = CONS n s1)" I believe not. Consider the following case: s2 = [] s1 = (@x. x = TL []) n = (@x. x = HD []) I use the epsilon notation to emphasise that TL [] and HD [] do actually have values, we just don't know what they are. More simply: s1 = TL [] n = HD [] With these values, (n = HD s2) /\ (s1 = TL s2) = (HD [] = HD []) /\ (TL [] = TL []) = T but, (s2 = CONS n s1) = ([] = CONS (HD []) (TL [])) = F because [] and CONS are always distinct. One might imagine that CONS (HD []) (TL []) = [] but the theorem `CONS' in HOL has a condition: |- !l. ~NULL l ==> (CONS(HD l)(TL l) = l) You need to add a similar condition to your conjecture for it to be a theorem: "!n s1 s2. ~(NULL s2) /\ (n = HD s2) /\ (s1 = TL s2) ==> (s2 = CONS n s1)" Your other conjecture is also false for similar reasons: "!s1 s2. (s1 = TL s2) ==> ~NULL s2" The counter-example is as above. Richard.