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; Thu, 22 Jul 1993 18:26:14 +0100
Received: by ted.cs.uidaho.edu (16.6/2.0) id AA26298;
          Thu, 22 Jul 93 10:14:33 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by cs.uidaho.edu (16.6/2.0) id AA26293;
          Thu, 22 Jul 93 10:14:23 -0700
Message-Id: <9307221714.AA26293@cs.uidaho.edu>
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <06811-0@iraun1.ira.uka.de>; Thu, 22 Jul 1993 18:54:51 +0200
Date: Thu, 22 Jul 93 18:56:47 MET DST
From: schneide <schneide@ira.uka.de>
To: info-hol@ted.cs.uidaho.edu
Subject: REWRITE_TAC



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?


N.B. The rewriting generates the following subgoals:

e(ONCE_ASM_REWRITE_TAC[]);
OK..
1 subgoal:
(--`!t. L t (SUC 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))`--)


val it = () : unit
- e(ONCE_ASM_REWRITE_TAC[]);
OK..
1 subgoal:
(--`!t. (F => (A t 0 \/ B t 0) | (A t 0 /\ B 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))`--)


val it = () : unit
- e(ONCE_ASM_REWRITE_TAC[]);
OK..
1 subgoal:
(--`!t. A t 0 /\ B 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))`--)


val it = () : unit
- e(ONCE_ASM_REWRITE_TAC[]);
OK..
1 subgoal:
(--`!t. T`--)
=============================
  (--`!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))`--)


val it = () : unit
- e(ONCE_ASM_REWRITE_TAC[]);
OK..

Goal proved.