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); Wed, 13 Jan 1993 12:20:04 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA25671;
          Wed, 13 Jan 93 04:06:47 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA25666;
          Wed, 13 Jan 93 04:06:37 -0800
Received: from dipper.cl.cam.ac.uk (user mjcg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Wed, 13 Jan 1993 12:05:32 +0000
Received: by dipper.cl.cam.ac.uk (4.1/SMI-3.0DEV3) id AA08011;
          Wed, 13 Jan 93 12:05:19 GMT
Date: Wed, 13 Jan 93 12:05:19 GMT
From: Mike.Gordon@uk.ac.cam.cl
Message-Id: <9301131205.AA08011@dipper.cl.cam.ac.uk>
To: des@uk.co.inmos
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: David Shepherd's message of Wed, 13 Jan 1993 10:50:49 +0000 (GMT) <2981.9301131050@frogland.inmos.co.uk>
Subject: Bottleneck in HOL (was Re: BETA_CONV)



Here is a simple way to introduce "proof accelerators" cleanly and to
flag their uses.  Suppose you have a function:

   tool : term -> term

written in ML (e.g. a model checker). Then if one defines a constant:

   new_definition(`TOOL_DEF`, "TOOL = F");;

one can convert the function tool into a proof rule:

   TOOL : term -> thm

by

   let TOOL tool = 
    let TOOL_F = SUBS[definition `-` `TOOL_DEF`](ASSUME "TOOL")
    in 
    \t. CONTR (tool t) TOOL_F;;

(note that SUBS is only done when the ML function TOOL is defined, not
every time it is used) then TOOL t will prove the theorem:

   TOOL |- t

by applying tool (plus an application of CONTR, which is fast).  It
marks the theorems "proved" using the tool with a mnemonic assumption
"TOOL". Such assumptions could be discharged away by redoing the proof
without using the acelerator. Whether this was worth doing would
depend of the level of assurance required.

Mike