Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <07534-0@swan.cl.cam.ac.uk>; Fri, 28 Feb 1992 18:10:23 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26316; Fri, 28 Feb 92 09:43:16 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from panther.cs.uidaho.edu by ted.cs.uidaho.edu (16.6/1.34) id AA26305; Fri, 28 Feb 92 09:43:11 -0800 Received: from localhost by panther.cs.uidaho.edu with SMTP id AA13011 (5.65c/IDA-1.4.4 for info-hol@ted); Fri, 28 Feb 1992 09:49:15 -0800 Message-Id: <199202281749.AA13011@panther.cs.uidaho.edu> To: info-hol@edu.uidaho.cs.ted Subject: Re: Partial instantiation In-Reply-To: Your message of Fri, 28 Feb 92 11:18:40 -0500. <9202281618.AA02689@sparta.oracorp.com> Date: Fri, 28 Feb 92 09:49:14 -0800 From: Phil Windley X-Mts: smtp On Fri, 28 Feb 92 11:18:40 EST, shb@oracorp.com wrote: +------------ | Can someone give me a convenient way of partially instantiating | universally-quantified conclusions? For x, y, z, t nums I'd like to be | able to go, say, from !x y z t. f(x,y,z,t) to !x y t. f(x,y,3,t). | SPECL doesn't seem to be able to do it, and I'd like to avoid having to | use combinations of SPEC and GEN. The following recursive definition applies GEN and SPEC for you. I presume that you just didn't want to do it manually. Examples follow. let X_SPEC tm v thm = let tml = (fst o strip_forall o concl) thm in letrec SPEC1_aux tml sthm = (tml = []) => sthm | ((hd tml) = tm) => (SPEC v sthm) | (GEN (hd tml) (SPEC1_aux (tl tml) (SPEC (hd tml) sthm))) in SPEC1_aux tml thm;; %---------------------------------------------------------------- Here's a test X_SPEC "m:num" "5" LESS_EQ_LESS_EQ_MONO;; X_SPEC "n:num" "5" LESS_EQ_LESS_EQ_MONO;; X_SPEC "p:num" "5" LESS_EQ_LESS_EQ_MONO;; X_SPEC "q:num" "5" LESS_EQ_LESS_EQ_MONO;; X_SPEC "r:num" "5" LESS_EQ_LESS_EQ_MONO;; ----------------------------------------------------------------% Cheers, --phil--