Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 23 Jul 1993 12:36:21 +0100
Received: by ted.cs.uidaho.edu (16.6/2.0) id AA28020;
          Fri, 23 Jul 93 04:26:27 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by cs.uidaho.edu (16.6/2.0) id AA28015;
          Fri, 23 Jul 93 04:26:18 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 23 Jul 1993 12:26:08 +0100
To: schneide <schneide@ira.uka.de>
Cc: Tom.Melham@cl.cam.ac.uk, info-hol@ted.cs.uidaho.edu
Subject: Re: REWRITE_TAC
In-Reply-To: Your message of "Thu, 22 Jul 93 18:56:47 +0700." <9307221714.AA26293@cs.uidaho.edu>
Date: Tue, 20 Jul 93 00:03:45 +0100
From: Tom Melham <Tom.Melham@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:237540:930723112613"@cl.cam.ac.uk>

> Unfortunately, I found out, that ASM_REWRITE_TAC is not the same as
> REPEAT (ONCE_ASM_REWRITE_TAC[]). For example, consider the following
> goal:
> 
> (--`!t. C t 0 = A t 0 /\ B t 0`--)
> =============================
>   (--`!t.
>       ((L t 0 = F = A t 0 = B t 0) /\
>        (L t (SUC 0) = (F => (A t 0 \/ B t 0) | (A t 0 /\ B t 0)))) /\
>       T /\
>       (C t 0 = L t (SUC 0))`--)
> 
> The variables have the following types: A,B,C and L are of type
> num->num->bool and t is of type num.
> 
> REPEAT (ONCE_ASM_REWRITE_TAC[]) proves the above goal, but
> ASM_REWRITE_TAC[] generates an infinite loop.
> 
> Is this okay?

The tactics have a different effect because of the order in which
equations are applied.  What actually happens is that the
assumptions turn into theorems:

   th1 = . |- L t 0 = F = A t 0 = B t 0
   th2 = . |- L t (SUC 0) = (F => (A t 0 \/ B t 0) | (A t 0 /\ B t 0))
   th3 = . |- T = T
   th4 = . |- C t 0 = L t (SUC 0)

The infinite loop comes because of th3, which gets repeatedly applied
by ASM_REWRITE_TAC[].  By contrast, REPEAT(ONCE_ASM_REWRITE_TAC[])
applies the built-in simplifications and checks for the goal
having been solved between each application of th3.

Solution: (1) make sure you never have "T" on the assumption list.
(2) we revise the rewriting tools to always throw away |- T = T.

I vote for (2).

Tom