Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <10685-0@swan.cl.cam.ac.uk>; Fri, 3 Apr 1992 00:14:36 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04482; Thu, 2 Apr 92 14:57:56 -0800 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA04478; Thu, 2 Apr 92 14:57:49 -0800 Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <10526-0@swan.cl.cam.ac.uk>; Thu, 2 Apr 1992 23:57:50 +0100 To: weitzman@cambridge.oracorp.com (Adam Weitzman) Cc: info-hol@ted.cs.uidaho.edu Subject: Re: Theorem conjuncts In-Reply-To: Your message of Wed, 01 Apr 92 17:02:58 -0500. <9204012202.AA16974@longvalley.cambridge.oracorp.com> Date: Thu, 02 Apr 92 23:57:46 +0100 From: John Harrison Message-Id: <"swan.cl.ca.528:02.03.92.22.57.52"@cl.cam.ac.uk> Adam Weitzman asks: > Is there any way to take a theorem which is a conjunction of terms and turn > it into a bunch of smaller theorems...? Yes, there's an inference rule CONJUNCTS that does precisely that. I give the doc file below. There are a few examples in the "reduce" library of using it as you describe, to do one goal-directed proof for several theorems. There's a similar rule BODY_CONJUNCTS that also strips away universal quantifiers. I've just noticed it's missing from the "SEE ALSO" field for CONJUNCTS. I'll add it in the 2.01 documentation. John. ------------------------------------------------------------------------------ CONJUNCTS : (thm -> thm list) SYNOPSIS Recursively splits conjunctions into a list of conjuncts. DESCRIPTION Flattens out all conjuncts, regardless of grouping. Returns a singleton list if the input theorem is not a conjunction. A |- t1 /\ t2 /\ ... /\ tn ----------------------------------- CONJUNCTS A |- t1 A |- t2 ... A |- tn FAILURE CONDITIONS Never fails. EXAMPLES Suppose the identifier th is bound to the theorem: A |- (x /\ y) /\ z /\ w Application of CONJUNCTS to th returns the following list of theorems: [A |- x; A |- y; A |- z; A |- w] : thm list SEE ALSO CONJ_LIST, LIST_CONJ, CONJ, CONJUNCT1, CONJUNCT2, CONJ_PAIR. ------------------------------------------------------------------------------