Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Tue, 24 Nov 1992 05:25:01 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08487;
          Mon, 23 Nov 92 21:10:50 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Hapuna.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA08482;
          Mon, 23 Nov 92 21:10:41 -0800
Received: by hapuna.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA23292;
          Mon, 23 Nov 92 21:09:57 -0800
Date: Mon, 23 Nov 92 21:09:57 -0800
From: toal@edu.ucla.cs (Ray J. Toal)
Message-Id: <9211240509.AA23292@hapuna.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: list theorems with destructors
Cc: toal@edu.ucla.cs


Hi,



I hate to use destructors, but they came up in an application.  Are
any of the following theorems of HOL? (n:*, s:* list, etc.)

  "~?n. n = HD[]"

  "~?s. s = TL[]"

  "!n s1 s2. (n = HD s2) /\ (s1 = TL s2) ==> (s2 = CONS n s1)"

  "!s1 s2. (s1 = TL s2) ==> ~NULL s2"

Note use of TL and *not* TAIL.  I don't think the first two are theorems
since, I would guess, HD[] = @x. HD[] = x because all functions are
total in HOL.  But the last two seem "reasonable" to me, and I can't seem
to find a way to prove them without relying on something similar to
the first two.


Thanks

Ray Toal