Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 15 Sep 1992 17:38:10 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03282; Tue, 15 Sep 92 09:25:04 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA03277; Tue, 15 Sep 92 09:24:50 -0700 Received: from heron.cl.cam.ac.uk (user ww) by swan.cl.cam.ac.uk with SMTP (PP-6.2) to cl; Tue, 15 Sep 1992 17:23:33 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Library for handling restriced quantifiers Date: Tue, 15 Sep 92 17:23:17 +0100 From: Wai Wong Message-Id: <"swan.cl.ca.004:15.08.92.16.23.41"@cl.cam.ac.uk> I've just put a library `res_quan` for handling restriced quantifiers in the HOL/contrib directory (which will be distributed with version 2.01). The library contains a set of syntax functions, derived inference rules, conversions and tactics for handling restriced quatifiers (mostly RES_FORALL). There is also a conditional rewriting tactic. A READ-ME file is included in the directory acting as a brief documentation. It is appended at the end of this message. It works with HOL version 2.0 as well. Anyone interested in having it before Version 2.01 is distributed please send me message. Any comments, suggestions are very welcome. Wai + ===================================================================== + | | | LIBRARY : res_quan | | | | DESCRIPTION : library for dealing with restricted quantifiers. | | | | AUTHOR : Wai WONG | | DATE : Aug 1992 | | | | ACKNOWLEGMENT : Thanks to Andy Gordon who gave me the source of some | | of the functions in this library. | | | + ===================================================================== + + --------------------------------------------------------------------- + | | | FILES: | | | + --------------------------------------------------------------------- + mk_res_quan.ml --- create the theory res_quan which contains a number of useful theorems about restricted quatifiers. res_quan.ml --- for loading the library. load_res_quan.ml --- for loading the libary. res_rules.ml --- source of ML functions. + --------------------------------------------------------------------- + | | | TO REBUILD THE LIBRARY: | | | + --------------------------------------------------------------------- + 1) edit the pathnames in the Makefile (if necessary) 2) type "make clobber" 3) type "make all" + --------------------------------------------------------------------- + | | | TO USE THE LIBRARY: | | | + --------------------------------------------------------------------- + Ensure that the directory more_lists is on the search path. Type "load_library `res_quan`;;" + --------------------------------------------------------------------- + | | | DOCUMENTATION: | | | + --------------------------------------------------------------------- + Proper document to be written later. In the absence of proper document, a list of all user function in the library is provided below. For more details, please read the comments in the source files. SYNTAX FUNCTIONS ================ Functions in this section are analogous to mk_forall, dest_forall etc. mk_res_quan = - : (string -> string -> (term # term # term) -> term) mk_res_forall = - : ((term # term # term) -> term) mk_res_exists = - : ((term # term # term) -> term) mk_res_select = - : ((term # term # term) -> term) mk_res_abstract = - : ((term # term # term) -> term) list_mk_res_forall = - : (((term # term) list # term) -> term) dest_res_quan = - : (string -> string -> term -> (term # term # term)) dest_res_forall = - : (term -> (term # term # term)) dest_res_exists = - : (term -> (term # term # term)) dest_res_select = - : (term -> (term # term # term)) dest_res_abstract = - : (term -> (term # term # term)) strip_res_forall = - : (term -> ((term # term) list # term)) is_res_forall = - : (term -> bool) is_res_exists = - : (term -> bool) is_res_select = - : (term -> bool) is_res_abstract = - : (term -> bool) DERIVED INFERENCE RULES ======================= RES_SPEC = - : (term -> thm -> thm) RES_SPECL = - : (term list -> thm -> thm) RES_SPEC_ALL = - : (thm -> thm) These are analogous to SPEC, SPECL, SPEC_ALL. RES_HALF_SPEC = - : (thm -> thm) RES_GEN = - : (term -> term -> thm -> thm) COND_REWR_CANON = - : (thm -> thm) TACTICS AND TACTICALS ===================== RES_GEN_TAC = - : tactic RES_EXISTS_TAC = - : (term -> tactic) These are analogous to GEN_TAC, EXISTS_TAC. RES_IMP_RES_THEN = - : thm_tactical RES_RES_THEN = - : (thm_tactic -> tactic) RES_IMP_RES_TAC = - : thm_tactic RES_RES_TAC = - : tactic These are analogous to IMP_RES_THEN, RES_THEN, IMP_RES_TAC and RES_TAC. COND_REWRITE_THEN = - : (tactic list -> tactic -> thm_tactic) COND_REWRITE_TAC = - : thm_tactic RES_REWRITE_THEN = - : (tactic list -> tactic -> thm_tactic) RES_REWRITE_TAC = - : thm_tactic Conditional rewriting and rewriting with restricted quatification. CONVERSIONS =========== RES_FORALL_CONV = - : conv LIST_RES_FORALL_CONV = - : conv Eliminate restricted forall. IMP_RES_FORALL_CONV = - : conv Introduce restriced forall. RES_FORALL_AND_CONV = - : conv AND_RES_FORALL_CONV = - : conv Distribute restriced forall over AND and the reverse. RES_FORALL_SWAP_CONV = - : conv Swap two restriced forall. CONJ_IMP_CONV = - : conv A limited IMP_CANON. FUNCTIONS FOR CONSTANT DEFINITIONS ================================== new_gen_res_definition = - : (string -> (string # term) -> thm) new_res_definition = - : ((string # term) -> thm) new_infix_res_definition = - : ((string # term) -> thm) new_binder_res_definition = - : ((string # term) -> thm) Functions for making definition with restrict universal quantified variables.