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; Tue, 21 Dec 1993 17:02:42 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA04371; Tue, 21 Dec 1993 09:11:23 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA04367; Tue, 21 Dec 1993 09:11:11 -0700 Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA16517; Tue, 21 Dec 1993 08:09:11 -0800 Received: from ira.uka.de by iraun1.ira.uka.de id <26002-0@iraun1.ira.uka.de>; Tue, 21 Dec 1993 12:26:09 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <01974-0@i80fs2.ira.uka.de>; Tue, 21 Dec 1993 12:26:57 +0100 Date: Tue, 21 Dec 93 12:26:56 EST From: reetz To: send@ira.uka.de, info-hol@cs.uidaho.edu Cc: wishnu@cs.ruu.nl Subject: RE: Help with DEPTH_CONV Message-Id: <"i80fs2.ira.976:21.11.93.11.27.00"@ira.uka.de> Wishnu writes: >Can anyone kindly explain why is the following application of >DEPTH_CONV is wrong: > #DEPTH_CONV CONTRAPOS_CONV "!x:*. P x ==> p" ;; Executing CONTRAPOS_CONV once produces a term, where it can be applied again: !DESCRIPTION ! !When applied to an implication P ==> Q, the conversion CONTRAPOS_CONV !returns the theorem: ! ! |- (P ==> Q) = (~Q ==> ~P) ! So DEPTH_CONV runs into an infinite loop. Just use ONCE_DEPTH_CONV instead: - ONCE_DEPTH_CONV CONTRAPOS_CONV (--`!x:'a.P x ==> p`--); val it = |- (!x. P x ==> p) = (!x. ~p ==> ~(P x)) : thm :) Ralf (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)