Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <08845-0@swan.cl.cam.ac.uk>; Thu, 13 Feb 1992 19:03:03 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03595;
          Thu, 13 Feb 92 10:46:40 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA03591;
          Thu, 13 Feb 92 10:46:29 -0800
Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl
          id <08658-0@swan.cl.cam.ac.uk>; Thu, 13 Feb 1992 18:48:30 +0000
To: shb@com.oracorp.sparta
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Huge expressions
In-Reply-To: Your message of Thu, 13 Feb 92 09:50:12 -0500. <9202131450.AA08108@sparta.oracorp.com>
Date: Thu, 13 Feb 92 18:48:27 +0000
From: John.Harrison@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.660:13.01.92.18.48.32"@cl.cam.ac.uk>


If you really are stuck with big subexpressions, you can introduce
abbreviations via a simple tactic like:

  let ABBREV_TAC tm =
    let v,t = dest_eq tm in
    CHOOSE_THEN (\th. SUBST_ALL_TAC th THEN ASSUME_TAC th)
                (EXISTS(mk_exists(v,mk_eq(t,v)),t) (REFL t));;

To give a trivial example:

  #g "1 + 1 = 0 + (1 + 1)";;
  "1 + 1 = 0 + (1 + 1)"

  () : void

  #e (ABBREV_TAC "x = 1 + 1");;
  OK..
  "x = 0 + x"
      [ "1 + 1 = x" ]

Even for the small proofs I do, I have found this very valuable on occasion.
For large proofs, it could prove indispensible; I think Brian Graham used
something similar for the SECD proof.

John.