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.0) 
          id <08115-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 10:39:04 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11632;
          Fri, 24 Jul 92 02:27:37 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11627;
          Fri, 24 Jul 92 02:26:39 -0700
Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk;
          Fri, 24 Jul 92 10:17:03 BST
From: David Shepherd <des@uk.co.inmos>
Message-Id: <5397.9207240916@frogland.inmos.co.uk>
Subject: Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY
To: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Date: Fri, 24 Jul 92 10:16:56 BST
Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
In-Reply-To: <9207231810.AA27324@leopard.cs.uidaho.edu>; from "Phil Weiss" at Jul 23, 92 11:10 am
X-Mailer: ELM [version 2.3 PL11]

Phil Weiss has said:
> 
> Could anyone tell me if they have managed to prove
> 
> GSPEC (\x. (<any expression>, F)) = EMPTY
> 
> for all expressions?  Or if they have written a conversion?
> 
> The only way I have found which is usable in all cases is three
> steps
> 
>   REWRITE_TAC [GSPEC_DEF]
>   BETA_TAC
>   REWRITE_TAC [PAIR_EQ]

try making it into a conversion

i.e.

let GSPEC_EMPTY_CONV = ((RATOR_CONV o RAND_CONV)
                        ((REWRITE_CONV GSPEC_DEF) THENC
                         ((RAND_CONV o ABS_CONV o RAND_CONV o ABS_CONV)
                          ((RAND_CONV BETA_CONV) THENC (REWRITE_CONV PAIR_EQ)
                           THENC (RAND_CONV(REWRITE_CONV((CONJUNCT1 o SPEC_ALL)EQ_CLAUSES)))
                           THENC (REWRITE_CONV((el 4 o CONJUNCTS o SPEC_ALL)AND_CLAUSES))))
                         THENC (RAND_CONV o ABS_CONV)(REWRITE_CONV EXISTS_SIMP)
                         THENC (REWRITE_CONV(SYM EMPTY_DEF))
                         )
                        THENC REWRITE_CONV(REFL_CLAUSE));;
                         
and then use

CONV_TAC(ONCE_DEPTH_CONV GSPEC_EMPTY_CONV)
         ^^^^^^^^^^^^^^^
         or whatever

and this will only touch the terms you want


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"i speak latin to god,   spanish to men,   french to women 
		 and german to my horse."             - charles v of spain