Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <08951-0@swan.cl.cam.ac.uk>; Tue, 16 Jun 1992 14:47:52 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18126; Tue, 16 Jun 92 06:39:01 -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 AA18121; Tue, 16 Jun 92 06:38:55 -0700 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <08670-0@swan.cl.cam.ac.uk>; Tue, 16 Jun 1992 14:39:05 +0100 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list) Subject: Re: ISPEC definition In-Reply-To: Your message of Tue, 16 Jun 92 13:06:36 +0700. <199206161106.AA16633@infix.cs.ruu.nl> Date: Tue, 16 Jun 92 14:38:55 +0100 From: John Harrison Message-Id: <"swan.cl.ca.678:16.05.92.13.39.15"@cl.cam.ac.uk> Here's the definition of ISPEC from the HOL-2 sources. Suggest you press for an upgrade to HOL 2 though; it has many improvements over 1.11. If you have FTP access, you could always pull down the new HOL just to find the bits of code you want (a bit wasteful perhaps!) In case anyone has forgotten, the main HOL FTP sites are: ted.cs.uidaho.edu [129.101.100.20] in directory "pub/hol" ftp.cl.cam.ac.uk [128.232.0.56] in directory "hol" John. % --------------------------------------------------------------------- % % ISPEC: specialization, with type instantation if necessary. % % % % A |- !x:ty.tm % % ----------------------- ISPEC "t:ty'" % % A |- tm[t/x] % % % % (where t is free for x in tm, and ty' is an instance of ty) % % --------------------------------------------------------------------- % let ISPEC t th = let x,tm = dest_forall(concl th) ? failwith `ISPEC: input theorem not universally quantified` in let _,inst = match x t ? failwith `ISPEC: can't type-instantiate input theorem` in (SPEC t (INST_TYPE inst th) ? failwith `ISPEC: type variable free in assumptions`);;