Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <14043-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 15:12:13 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11695; Fri, 24 Jul 92 07:01:15 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11690; Fri, 24 Jul 92 07:01:08 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <13892-0@swan.cl.cam.ac.uk>; Fri, 24 Jul 1992 15:02:07 +0100 To: weiss@edu.uidaho.cs.leopard (Phil Weiss) Cc: info-hol@edu.uidaho.cs.ted (HOL Mailing List) Subject: Re: Equivalence of GSPEC(\x. ( ,F)) and EMPTY In-Reply-To: Your message of Thu, 23 Jul 92 11:10:21 -0700. <9207231810.AA27324@leopard.cs.uidaho.edu> Date: Fri, 24 Jul 92 15:02:03 +0100 From: John Harrison Message-Id: <"swan.cl.ca.894:24.06.92.14.02.09"@cl.cam.ac.uk> An alternative in such situations, which is often more efficient, is to prove a general theorem once and for all. In this case we prove: |- !P:*->bool. (GSPEC (\x. (P x,F)) = EMPTY) = T We can't rewrite with this directly, because the actual term is not of the convenient form "P x", but rather "P[x]", i.e. an expression possibly containing x. However it can be put into that form by "unbeta conversion", as illustrated by GSPEC_CONV below. A general way of doing this sort of "higher-order matching" in HOL rewriting is an interesting topic for investigation, I think. John. %----------------------------------------------------------------------------% % LAND_CONV - Applies conversion to left operand of a curried operator % %----------------------------------------------------------------------------% let LAND_CONV = RATOR_CONV o RAND_CONV;; %----------------------------------------------------------------------------% % UNBETA_CONV "v" "tm[v]" = |- tm[v] = (\v. tm[v]) v % %----------------------------------------------------------------------------% let UNBETA_CONV v tm = SYM(BETA_CONV(mk_comb(mk_abs(v,tm),v)));; %----------------------------------------------------------------------------% % Proforma theorem to perform required reduction % %----------------------------------------------------------------------------% let GSPEC_THM = PROVE ("!P:*->bool. (GSPEC (\x. (P x,F)) = EMPTY) = T", GEN_TAC THEN REWRITE_TAC[GSPEC_DEF; EMPTY_DEF] THEN AP_TERM_TAC THEN BETA_TAC THEN REWRITE_TAC[PAIR_EQ]);; %----------------------------------------------------------------------------% % Now package it up as a conversion % %----------------------------------------------------------------------------% let GSPEC_CONV tm = let UBC = (UNBETA_CONV o fst o dest_abs o rand o lhs) tm in ((LAND_CONV o RAND_CONV o ABS_CONV o LAND_CONV) UBC THENC REWRITE_CONV GSPEC_THM) tm;;