Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 13 Jul 1995 13:38:43 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA165557227; Thu, 13 Jul 1995 06:07:07 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA165497212; Thu, 13 Jul 1995 06:06:52 -0600 Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 13 Jul 1995 13:03:39 +0100 X-Mailer: exmh version 1.5.2 12/21/94 To: Wishnu Prasetya Cc: hol mailing list Subject: Re: [Q] pattern matching for existential quatification In-Reply-To: Your message of "Thu, 13 Jul 1995 13:07:51 +0200." Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Thu, 13 Jul 1995 13:03:34 +0100 From: Donald Syme Message-Id: <"swan.cl.cam.:273190:950713120352"@cl.cam.ac.uk> > I want to have a tactic that can prove the following automatically: > > A1; "P x" ?- "?z. P z" > > This is the code I wrote using unifier 'match': > > let MATCH_ASM_EXISTS_TAC (asml,g) = > (FIRST_ASSUM (\thm. (EXISTS_TAC o fst o hd o fst) > (match (snd (dest_exists g)) (concl thm))) > THEN FIRST_ASSUM ACCEPT_TAC) (asml,g) ;; > > Questions: > > 1. I'm not sure if the above is the best way to do it. > 2. Is there perhaps a standard tactic I don't know that ought to > do the same thing? SSMART_EXISTS_TAC in "smarttacs" in the hol88 contrib will do this (and also substantially more complicated things too). SMART_ELIMINATE_TAC in the same directory is also pretty useful. I have hol90 versions for these, which I plan to add to the next release. Contact me if you want them. There is an interesting problem here. SSMART_EXISTS_TAC could work a whole lot more accurately if it knew exactly which constants were 1-1. Why doesn't HOL have a database of 1-1 constants (with the theorems to justify this)? Plenty of other useful tools could take adavantage of such information too (e.g. a general REWRITE_11_TAC would be trivial). Obviously 1-1 theorems are a special case - perhaps there are other such theorem kinds for which databases would also be useful. Don ----------------------------------------------------------------------------- At the lab: At home: The Computer Laboratory Trinity Hall New Museums Site CB2 1TJ University of Cambridge Cambridge, UK CB2 3QG, Cambridge, UK Ph: +44 (0) 1223 334688 Ph: +44 (0) 1223 302521 http://www.cl.cam.ac.uk:80/users/drs1004/ email: Donald.Syme@cl.cam.ac.uk -----------------------------------------------------------------------------