Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 9 Feb 1993 13:01:43 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06971; Tue, 9 Feb 93 04:48:28 -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 AA06966; Tue, 9 Feb 93 04:48:19 -0800 Received: from teal.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Tue, 9 Feb 1993 12:46:30 +0000 To: schneide Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Basic Rules In-Reply-To: Your message of Tue, 09 Feb 93 13:13:08 +0700. <9302091215.AA06958@ted.cs.uidaho.edu> Date: Tue, 09 Feb 93 12:46:24 +0000 From: Richard Boulton Message-Id: <"swan.cl.ca.344:09.02.93.12.46.33"@cl.cam.ac.uk> > It is the philosophy of the HOL system to have a (minimal) set of primitive > rules. All other rules should be derived from this set of minimal rules, > since the high level of security is based on this derivation of further > rules. Hence, it cannot be the way to optimize the system by "implementing" > further rules directly using "mk_thm". The important point is that any rules implemented using mk_thm should be trustworthy. Thus, having the smallest number of rules possible is not the most important thing. It is more important for them to be simple, so that they can readily be seen to be correct (or better, can be formally verified). For example, the rule ADD_ASSUM for adding a boolean-valued term to the hypothesis list of a theorem is not one of the `official' primitive inference rules. However, it is very simple. Hence it is worth improving the performance of this rule by implementing it using mk_thm. Its addition to the `primitives' does not significantly reduce our trust in the system. One powerful rule that is `not easily derivable' might well be less trustworthy than dozens of simple rules. Richard.