Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <3197.9301131243@frogland.inmos.co.uk>
Subject: Re: Bottleneck in HOL (was Re: BETA_CONV)
To: Mike.Gordon@uk.ac.cam.cl
Date: Wed, 13 Jan 1993 12:43:44 +0000 (GMT)
Cc: des@uk.co.inmos, info-hol@edu.uidaho.cs.ted
In-Reply-To: <9301131205.AA08011@dipper.cl.cam.ac.uk> from "Mike.Gordon@cl.cam.ac.uk" at Jan 13, 93 12:05:19 pm
Content-Type: text
Content-Length: 3949

Mike.Gordon@cl.cam.ac.uk has said:
> 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.

This would appear to be a reasonably neat way of documenting the use of
another tool - but, like mk_thm, it relies on users being "honest" as,
unless TOOL_DEF is hidden from them, a user could always fake any
result as being derived from TOOL! At least there is a flag to warn
that something suspicous is going on!

E.g. if the tool were a tautology checker then while

	TAUT_CHECKER |- P

should mean that P is a tautology, as proved by taut_checker, you
can quite simply get from the defn of TAUT_CHECKER to

	TAUT_CHECKER |- F

which clearly isn't.

However, this could possibly be formalised a bit more in HOL.

We start with a type for tools in HOL ":tool" initially this can be 
any (suitably large) type as we will just define new constants. Later
this could be a type for an SML-subset embedded in HOL. In addition
there is a predicate "TOOL_CORRECT:tool->bool". Again initially this is
just used as a constant to flag tool uses, but later it could be given
some definition on embedded SML and HOL for reflection.

In ML we also have a type for tools which is equivalent to
:term#(term->term) - where the fst element is a term of HOL type
":tool" which is the tools name and the second takes a term and returns
another term which is claimed to be equivalent.

now tool use gets introduced as a conversion

let TOOL_CONV tool t =
 (
  let (id,eqgen) = tool in
  let validity_condition = mk_comb("TOOL_CORRECT",id) in
  let t' = eqgen t in
  mk_thm(validity_condition,mk_eq(t,t'))
 ) ? failwith `tool failed`;;

where this is the only mk_thm that is needed. So the result of

TOOL_CONV("taut_checker:tool",taut_checker)"P";;

is

TOOL_CORRECT(taut_checker) |- P = T

(assuming P is checked as a tautlogy).

Using abstract types to bundle ML functions into tools might make
things slightly cleaner (i.e. the tool id would have to be one that was
introduced with the tool declaration).

Finally, if ML and HOL were embedded in HOL in the way that Konrad
Slind suggested for reflections then you could make :tool be the type
of such ML subset programs and define TOOL_CORRECT as the relevant
correctness condition and then discharge these assumptions.

However, I think in the context I described earlier where you are
wanting additional proof performance (i.e. when the theorem prover is
being used as the kernel of a special purpose tool) I think that this
may be unnecessary as a designer isn't going to see if he can remove
depenency on tool X from the verification of his design - s/he will
work on the basis that tool X is probably implemented correctly and use
other testing techniques to add to this confidence.
  

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                New Year Resolution for 1993: Start using capital letters.