Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <25856-0@swan.cl.cam.ac.uk>; Fri, 14 Feb 1992 10:30:54 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07758; Fri, 14 Feb 92 02:18:33 -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 AA07754; Fri, 14 Feb 92 02:18:26 -0800 Received: from puffin.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <25238-0@swan.cl.cam.ac.uk>; Fri, 14 Feb 1992 10:20:05 +0000 To: shb@com.oracorp.sparta Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Huge expressions Date: Fri, 14 Feb 92 10:19:46 +0000 From: btg@uk.ac.cam.cl Message-Id: <"swan.cl.ca.258:14.01.92.10.20.17"@cl.cam.ac.uk> As pointed out by John Harrison, my work on the SECD proof encountered some rather large expressions (approximately 2000 line terms). The expressions contained many repeated occurrences of the same term, but as you can imagine was incomprehensible. Only by abbreviating the frequently occurring large expressions could the quite simple structure of the entire expression be appreciated. By abbreviation, I mean the introduction of new variables which are globally substituted for the larger term, and an assumption added which gives the binding of the variable. Note that the use of abbreviation may interfere with solving the goal. I found occassions when I would abbreviate the terms to determine the correct tactic to be applied, and then undo the abbreviations to manipulate some part of the term. The tactic I used (same name as John Harrison's) is in the contrib library of the HOL distribution, in the file: .../contrib/btg-tactics/abbrev_tac.ml It is documented there as well. Brian Graham