Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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:59:46 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA05627;
          Thu, 26 Jan 1995 11:48:02 -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 AA05622;
          Thu, 26 Jan 1995 11:48:01 -0700
Received: from oberon.inmos.co.uk (oberon.inmos.co.uk [138.198.35.8]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with ESMTP id KAA03149 
          for <info-hol@cs.uidaho.edu>; Thu, 26 Jan 1995 10:44:53 -0800
Received: from frogland.inmos.co.uk by oberon.inmos.co.uk;
          Thu, 26 Jan 1995 18:44:43 GMT
From: David Shepherd <des@inmos.co.uk>
Message-Id: <7595.9501261836@frogland.inmos.co.uk>
Subject: Changes in REWRITE_TAC? (fwd)
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Thu, 26 Jan 1995 18:36:43 +0000 (GMT)
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 2924

schneide has said:
> As I am currently switching from HOL90.6 to HOL90.7, I wondered
> that a (very long) proof did not work with HOL90.7 although I
> did it without problems in HOL90.6. The problem is
> the following subgoal:
> 
> 
> 
> set_goal([(--`~(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)`--)],
>    (--`q (d + t0) \/
>        (b1 (d + t0) ==>
>         (?q.
>           (!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))))) ==>
>        (?q.
>          (!t'.
>            ~(q (t + t0)) /\
>            (q (SUC (t' + t + t0)) = q (t' + t + t0) \/ b2 (t' + t + t0))) /\
>          (!t'. q (t' + t + t0) \/ (b2 (t' + t + t0) ==> x (t' + t + t0))))`--));
> 
> If "e(ASM_REWRITE_TAC[]);" is applied then in HOL90.6 the following 
> subgoal is obtained:
> 
> 1 subgoal:
> (--`(?q.
>       (!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)))) ==>
>     (?q.
>       (!t'.
>         ~(q (t + t0)) /\
>         (q (SUC (t' + t + t0)) = q (t' + t + t0) \/ b2 (t' + t + t0))) /\
>       (!t'. q (t' + t + t0) \/ (b2 (t' + t + t0) ==> x (t' + t + t0))))`--)
> =============================
>  .....
> 
> 
> but in HOL90.7 I get
> 
> 
> 1 subgoal:
> val it =
>   (--`(?q.
>         (!t''.
>           ~(q (SUC n + t0)) /\
>           (q (SUC (t'' + SUC n + t0)) =
>            q (t'' + SUC n + t0) \/ b2 (t'' + SUC n + t0))) /\
>         (!t''.
>           q (t'' + SUC n + t0) \/
>           (b2 (t'' + SUC n + t0) ==> x (t'' + SUC n + t0)))) ==>
>       (?q.
>         (!t'.
>           ~(q (t + t0)) /\
>           (q (SUC (t' + t + t0)) = q (t' + t + t0) \/ b2 (t' + t + t0))) /\
>         (!t'. q (t' + t + t0) \/ (b2 (t' + t + t0) ==> x (t' + t + t0))))`--)
>   ____________________________

Looks like a bug in 90.6 to me .... you have the assumption

(--`d = SUC n`--)

which isn't causing any rewrites in your 90.6 output

--------------------------------------------------------------------------
                               david shepherd
 SGS-THOMSON Microelectronics Ltd, 1000 aztec west, bristol bs12 4sq, u.k.
          tel/fax: +44 1454 611638/617910    email: des@inmos.co.uk
               www: http://www.inmos.co.uk/~des/welcome.html
       "whatever you don't want, you don't want negative advertising"