Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <05476-0@swan.cl.cam.ac.uk>; Mon, 10 Aug 1992 16:59:58 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25227; Mon, 10 Aug 92 08:45:05 -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 AA25222; Mon, 10 Aug 92 08:44:52 -0700 Received: from razorbill.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <05188-0@swan.cl.cam.ac.uk>; Mon, 10 Aug 1992 16:43:30 +0100 To: info-hol@edu.uidaho.cs.ted Subject: Re: need more pattern support? In-Reply-To: Your message of Mon, 10 Aug 92 16:24:52 +0100. <"swan.cl.ca.831:10.07.92.15.25.05"@cl.cam.ac.uk> Date: Mon, 10 Aug 92 16:43:24 +0100 From: Jim Grundy Message-Id: <"swan.cl.ca.190:10.07.92.15.43.33"@cl.cam.ac.uk> > Is anyone working on making HOL a little more flexible in these areas? > I remember hearing that someone was working on tupled quantification; > another useful contribution would allow HOL "functions" to look more like > functions in Standard ML. Too great of a task? > > Ray Toal > I think there are two of us working on this. Wim Ploegaerts has a collection of tuple functions including some for tupled quantifications. I don't know what Wim's intentions for this are but they could be in contrib when HOL 2.01 is released. I am working on a Library for tuples containing a comprehensive set of tuple manipualting functions and a tupled equivalent for every HOL function that uses quantifiers. The code is finished now and I can mail it to anybody who wants. The documentation .......... well I just haven't found the energy. This table lists the corespondance between the unpaired functions provided by the basic HOL system and the paired functions provided by my Library. There are lots of other functions besides these which are excusively for tuples. +---------------------------+---------------------------+ | Unpaired | Paired | +---------------------------+---------------------------+ | ALPHA | PALPHA | | ALPHA_CONV | PALPHA_CONV | | GEN_ALPHA_CONV | GEN_PALPHA_CONV | | BETA_CONV | PBETA_CONV | | BETA_RULE | PBETA_RULE | | BETA_TAC | PBETA_TAC | | LIST_BETA_CONV | LIST_PBETA_CONV | | RIGHT_BETA | RIGHT_PBETA | | RIGHT_LIST_BETA | RIGHT_LIST_PBETA | | ETA_CONV | PETA_CONV | | ABS | PABS | | ABS_CONV | PABS_CONV | | HALF_MK_ABS | HALF_MK_PABS | | MK_ABS | MK_PABS | | EXT | PEXT | | X_FUN_EQ_CONV | P_FUN_EQ_CONV | | CHOOSE | PCHOOSE | | CHOOSE_TAC | PCHOOSE_TAC | | CHOOSE_THEN | PCHOOSE_THEN | | X_CHOOSE_TAC | P_PCHOOSE_TAC | | X_CHOOSE_THEN | P_PCHOOSE_THEN | | AND_EXISTS_CONV | AND_PEXISTS_CONV | | EXISTENCE | PEXISTENCE | | EXISTS | PEXISTS | | EXISTS_AND_CONV | PEXISTS_AND_CONV | | EXISTS_EQ | PEXISTS_EQ | | EXISTS_IMP | PEXISTS_IMP | | EXISTS_IMP_CONV | PEXISTS_IMP_CONV | | EXISTS_NOT_CONV | PEXISTS_NOT_CONV | | EXISTS_OR_CONV | PEXISTS_OR_CONV | | EXISTS_TAC | PEXISTS_TAC | | EXISTS_UNIQUE_CONV | PEXISTS_UNIQUE_CONV | | LEFT_AND_EXISTS_CONV | LEFT_AND_PEXISTS_CONV | | LEFT_IMP_EXISTS_CONV | LEFT_IMP_PEXISTS_CONV | | LEFT_OR_EXISTS_CONV | LEFT_OR_PEXISTS_CONV | | MK_EXISTS | MK_PEXISTS | | NOT_EXISTS_CONV | NOT_PEXISTS_CONV | | OR_EXISTS_CONV | OR_PEXISTS_CONV | | RIGHT_AND_EXISTS_CONV | RIGHT_AND_PEXISTS_CONV | | RIGHT_IMP_EXISTS_CONV | RIGHT_IMP_PEXISTS_CONV | | RIGHT_OR_EXISTS_CONV | RIGHT_OR_PEXISTS_CONV | | SWAP_EXISTS_CONV | SWAP_PEXISTS_CONV | | AND_FORALL_CONV | AND_PFORALL_CONV | | FORALL_AND_CONV | PFORALL_AND_CONV | | FORALL_EQ | PFORALL_EQ | | FORALL_IMP_CONV | PFORALL_IMP_CONV | | FORALL_NOT_CONV | PFORALL_NOT_CONV | | FORALL_OR_CONV | PFORALL_OR_CONV | | LEFT_AND_FORALL_CONV | LEFT_AND_PFORALL_CONV | | LEFT_IMP_FORALL_CONV | LEFT_IMP_PFORALL_CONV | | LEFT_OR_FORALL_CONV | LEFT_OR_PFORALL_CONV | | NOT_FORALL_CONV | NOT_PFORALL_CONV | | OR_FORALL_CONV | OR_PFORALL_CONV | | RIGHT_AND_FORALL_CONV | RIGHT_AND_PFORALL_CONV | | RIGHT_IMP_FORALL_CONV | RIGHT_IMP_PFORALL_CONV | | RIGHT_OR_FORALL_CONV | RIGHT_OR_PFORALL_CONV | | FILTER_GEN_TAC | FILTER_PGEN_TAC | | GEN | PGEN | | GENL | PGENL | | GEN_TAC | PGEN_TAC | | X_GEN_TAC | P_PGEN_TAC | | SELECT_CONV | PSELECT_CONV | | SELECT_ELIM | PSELECT_ELIM | | SELECT_EQ | PSELECT_EQ | | SELECT_INTRO | PSELECT_INTRO | | SELECT_RULE | PSELECT_RULE | | GSPEC | GPSPEC | | ISPEC | IPSPEC | | ISPECL | IPSPECL | | SPEC | PSPEC | | SPECL | PSPECL | | SPEC_ALL | PSPEC_ALL | | SPEC_TAC | PSPEC_TAC | | SPEC_VAR | PSPEC_PAIR | | SKOLEM_CONV | PSKOLEM_CONV | | X_SKOLEM_CONV | P_PSKOLEM_CONV | +---------------------------+---------------------------+ MATCH_MP and MATCH_MP_TAC not done yet All the functions handle tuples of arbitrary structure. (ie PGEN "((w,x),(y,z))") They also work for nontuples (ie PGEN "x" = GEN "x") ie they are considered to be tuples of size 1. Anyone thinking of using my code should know that some of the functions (PGEN and PSPEC for exaple) can be pretty slow when given big/complex structures. (P_PSKOLEM_CONV is very slow). I would like to get this finished in time for the next release of HOL, but that is not a promise. Jim