Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Sat, 10 Apr 1993 22:17:30 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12191;
          Sat, 10 Apr 93 12:02:53 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Makaha.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA12186;
          Sat, 10 Apr 93 12:02:47 -0700
Received: by makaha.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA13636;
          Sat, 10 Apr 93 12:02:41 -0700
Date: Sat, 10 Apr 93 12:02:41 -0700
From: toal@edu.ucla.cs (Ray J. Toal)
Message-Id: <9304101902.AA13636@makaha.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: "Unification" in HOL

Hi,

I was wondering what would be the best way to "automate" proving
goals like the following:

"E e q1 0 q /\ C c2 q q2"
    [ "E' e s1 q1 s q" ]
    [ "s = CONS 0 s1'" ]
    [ "C' c2 s1' q s2 q2" ]
    [ "C c2 q q2" ]
    [ "E e q1(HD s)q" ]
    [ "TL s = s1" ]

Of course the goal is easy to solve but I'm interseted in a finer approach
which reduces the goal above to

"HD s = 0"

I think the problem may be of general interest because "matching" is not
really relevant, that is, "E e q1 0 q" and "E e q1(HD s)q" do not match in
the HOL sense because neither "HD s" nor "0" is a variable.

In general it would be useful to reduce any number of conjuncts, even
existentially quantified, to equalities on their subterms that do not
match.  I have been using REDUCE in the ind_defs library and Donald
Syme's "smarttacs" contribution quite successfully but neither can handle
"matches" not involving variables.

Does anyone have any ideas or comments?  

Thanks

Ray Toal