Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Mon, 18 Jan 1993 08:19:57 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08471;
          Sun, 17 Jan 93 22:07:39 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA08466;
          Sun, 17 Jan 93 22:07:32 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA10190;
          Sun, 17 Jan 93 22:07:02 -0800
Message-Id: <9301180607.AA10190@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: RULE_ASSUM_TAC: a suggestion
Date: Sun, 17 Jan 93 22:07:00 PST
From: chou@edu.ucla.cs

Currently RULE_ASSUM_TAC is defined as follows:

  let RULE_ASSUM_TAC (rule) =
    POP_ASSUM_LIST (\asl. MAP_EVERY ASSUME_TAC (rev (map rule asl))) ;;

I suggest that RULE_ASSUM_TAC use CHECK_ASSUME_TAC instead of ASSUME_TAC:

  let new_RULE_ASSUM_TAC (rule) =
    POP_ASSUM_LIST (\asl. MAP_EVERY CHECK_ASSUME_TAC (rev (map rule asl))) ;;

My reason is as follows.  It seems pretty common that one wishes to
use one (or several) of the assumptions of a goal to rewrite other
assumptions.  Consider the following (admittedly contrived) goal
as an example:

#set_goal(["SUC n = n'"; "f(SUC n) : bool"], "f(n') = f(SUC n) \/ b");;
"f n' = f(SUC n) \/ b"
    [ "f(SUC n)" ]
    [ "SUC n = n'" ]

Clearly ASM_REWRITE_TAC won't work.  But it would if I could first
replace the assumption "f(SUC n)" by "f(n')".  Let's try RULE_ASSUM_TAC:

#e(let asm = ASSUME "SUC n = n'" in
#  RULE_ASSUM_TAC (REWRITE_RULE [asm]) THEN ASSUME_TAC asm);;
OK..
"f n' = f(SUC n) \/ b"
    [ "f n'" ]
    [ "T" ]
    [ "SUC n = n'" ]

Now ASM_REWRITE_TAC still won't work; in fact, it will diverge.
(It wouldn't help either if I had used PURE_REWRITE_RULE.)
However, I could do:

#b();;
"f n' = f(SUC n) \/ b"
    [ "f(SUC n)" ]
    [ "SUC n = n'" ]

#e(let asm = ASSUME "SUC n = n'" in
#  new_RULE_ASSUM_TAC (REWRITE_RULE [asm]) THEN ASSUME_TAC asm);;
OK..
"f n' = f(SUC n) \/ b"
    [ "f n'" ]
    [ "SUC n = n'" ]

#e(ASM_REWRITE_TAC [ ]);;
OK..
goal proved
.. |- f n' = f(SUC n) \/ b
.. |- f n' = f(SUC n) \/ b

#top_thm();;
SUC n = n', f(SUC n) |- f n' = f(SUC n) \/ b


- Ching Tsun