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, 26 Jan 1995 18:10:31 +0000 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA03443; Thu, 26 Jan 1995 10:56:16 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA03428; Thu, 26 Jan 1995 10:56:10 -0700 Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id JAA02781 for ; Thu, 26 Jan 1995 09:53:11 -0800 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Wed, 25 Jan 1995 08:58:24 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <18172-0@i80fs2.ira.uka.de>; Wed, 25 Jan 1995 08:58:40 +0100 To: info-hol@cs.uidaho.edu Subject: Changes in IMP_RES_TAC? Date: Wed, 25 Jan 1995 08:58:39 +0100 From: schneide Message-Id: <"i80fs2.ira.174:25.01.95.07.58.41"@ira.uka.de> Again there is a differenc between HOL90.7 and HOL90.6. Consider the following goal val g = ([(--`b2 (x' + t + t0):bool`--),(--`x' + t < d`--),(--`t' <= x'`--), (--`!z. fn1 (SUC (z + x'))`--),(--`d <= t' + t`--),(--`n = t + p`--), (--`d = t + p + 1`--), (--`(fn1 0 = F) /\ (!n. fn1 (SUC n) = fn1 n \/ b2 (n + t + t0))`--), (--`!t''. q' (t'' + d + t0) \/ (b2 (t'' + d + t0) ==> x (t'' + d + t0))`--), (--`!t''. ~(q' (d + t0)) /\ (q' (SUC (t'' + d + t0)) = q' (t'' + d + t0) \/ b2 (t'' + d + t0))`--),(--`~(q (d + t0))`--), (--`d <= SUC n`--),(--`~(b1 (t + t0))`--),(--`t < d`--), (--`!t. q (SUC (SUC ((t + n) + t0)))`--), (--`!t. t <= SUC n ==> ~(q (t + t0))`--), (--`!t. q (t + t0) \/ b1 (t + t0) \/ (b2 (t + t0) ==> x (t + t0))`--), (--`!t. ~(q t0) /\ (q (SUC (t + t0)) = q (t + t0) \/ b1 (t + t0))`--), (--`d = SUC n`--),(--`~(b1(t0:num))`--), (--`(!t. t < d ==> ~(b1 (t + t0))) /\ b1 (d + t0)`--)], (--`b2 (t' + t + t0) ==> x (t' + t + t0)`--)); and the tactic IMP_RES_TAC(EQT_ELIM(ARITH_CONV--`(t'<=x')==>(x'+t(t'+t x (t' + t + t0)`--) ============================= (--`(!t. t < d ==> ~(b1 (t + t0))) /\ b1 (d + t0)`--) (--`~(b1 t0)`--) (--`d = SUC n`--) (--`!t. ~(q t0) /\ (q (SUC (t + t0)) = q (t + t0) \/ b1 (t + t0))`--) (--`!t. q (t + t0) \/ b1 (t + t0) \/ (b2 (t + t0) ==> x (t + t0))`--) (--`!t. t <= SUC n ==> ~(q (t + t0))`--) (--`!t. q (SUC (SUC ((t + n) + t0)))`--) (--`t < d`--) (--`~(b1 (t + t0))`--) (--`d <= SUC n`--) (--`~(q (d + t0))`--) (--`!t''. ~(q' (d + t0)) /\ (q' (SUC (t'' + d + t0)) = q' (t'' + d + t0) \/ b2 (t'' + d + t0))`--) (--`!t''. q' (t'' + d + t0) \/ (b2 (t'' + d + t0) ==> x (t'' + d + t0))`--) (--`(fn1 0 = F) /\ (!n. fn1 (SUC n) = fn1 n \/ b2 (n + t + t0))`--) (--`d = t + p + 1`--) (--`n = t + p`--) (--`d <= t' + t`--) (--`!z. fn1 (SUC (z + x'))`--) (--`t' <= x'`--) (--`x' + t < d`--) (--`b2 (x' + t + t0)`--) (--`t' + t < d`--) (--`!d' t. SUC n + t < d' ==> d + t < d'`--) while HOL90.7 derives a additional assumption: 1 subgoal: val it = (--`b2 (t' + t + t0) ==> x (t' + t + t0)`--) ____________________________ (--`(!t. t < d ==> ~(b1 (t + t0))) /\ b1 (d + t0)`--) (--`~(b1 t0)`--) (--`d = SUC n`--) (--`!t. ~(q t0) /\ (q (SUC (t + t0)) = q (t + t0) \/ b1 (t + t0))`--) (--`!t. q (t + t0) \/ b1 (t + t0) \/ (b2 (t + t0) ==> x (t + t0))`--) (--`!t. t <= SUC n ==> ~(q (t + t0))`--) (--`!t. q (SUC (SUC ((t + n) + t0)))`--) (--`t < d`--) (--`~(b1 (t + t0))`--) (--`d <= SUC n`--) (--`~(q (d + t0))`--) (--`!t''. ~(q' (d + t0)) /\ (q' (SUC (t'' + d + t0)) = q' (t'' + d + t0) \/ b2 (t'' + d + t0))`--) (--`!t''. q' (t'' + d + t0) \/ (b2 (t'' + d + t0) ==> x (t'' + d + t0))`--) (--`(fn1 0 = F) /\ (!n. fn1 (SUC n) = fn1 n \/ b2 (n + t + t0))`--) (--`d = t + p + 1`--) (--`n = t + p`--) (--`d <= t' + t`--) (--`!z. fn1 (SUC (z + x'))`--) (--`t' <= x'`--) (--`x' + t < d`--) (--`b2 (x' + t + t0)`--) (--`t' + t < d`--) (--`!d' t''. (t' + t) + t'' < d' ==> d + t'' < d'`--) (--`!d' t. SUC n + t < d' ==> d + t < d'`--) : goalstack Did IMP_RES_TAC change?