VERSION 2 January 14, 2023

The HOL System

TUTORIAL

University of Cambridge  DSTO  SRI International

Preface

This volume contains a tutorial on the HOL system. It is one of three documents making up the documentation for HOL:

(i) TUTORIAL: a tutorial introduction to HOL.

(ii) DESCRIPTION: a description of higher order logic, the ML programming language, and theorem proving methods in the HOL system;

(iii) REFERENCE: the reference documentation of the tools available in HOL.

These three documents will be referred to by the short names (in small slanted capitals) given above.

This document, TUTORIAL, is intended to be the first item read by new users of HOL. It provides a self-study introduction to the structure and use of the system. The tutorial is intended to give a ‘hands-on’ feel for the way HOL is used, but it does not systematically explain all the underlying principles (DESCRIPTION, explains these). After working through TUTORIAL the reader should be capable of using HOL for simple tasks, and should also be in a position to consult the other two documents.

Getting started

Chapter 1 explains how to get and install HOL. Once this is done, the potential HOL user should become familiar with the following subjects:

1. The programming meta-language ML, and how to interact with it through an editor.

2. The formal logic supported by the HOL system (higher order logic) and its manipulation via ML.

3. Forward proof and derived rules of inference.

4. Goal directed proof, tactics and tacticals.

Chapters 1–5 introduce these topics. The remaining three chapters contain examples of complete pieces of work.

• Chapter 6 consists of a worked example: the specification and verification of a simple sequential parity checker. The intention is to accomplish two things: (i) to present a complete piece of work with HOL; and (ii) to give an idea of what it is like to use the HOL system for a tricky proof.

• Chapter 7 shows how a special purpose proof tool (a conjunction normaliser) can be implemented and optimised. It illustrates methods for ‘tuning’ proof generating programs and discusses trade-offs between generality and efficiency.

• Chapter 8 is a proof of the Binomial Theorem in a ring. It is a medium sized worked example whose subject matter is probably more widely known than any specific piece of hardware or software. The small amount of algebra and mathematical notation needed to state and prove the Binomial Theorem is presented; the notation is expressed in HOL, and the structure of the proof is outlined.

TUTORIAL has been kept short so that new users of HOL can get going as fast as possible. Sometimes details have been simplified. It is recommended that as soon as a topic in TUTORIAL has been digested, the relevant bits of DESCRIPTION and REFERENCE be studied.

Exercises

The directory:

    hol/Training/exercises

contains exercises (with solutions) in the use of HOL. It is recommended that these exercises be studied in conjunction with reading TUTORIAL and DESCRIPTION.

Courseware

The directory:

    hol/Training/course

contains the L^{A}TEX sources for an intensive course on HOL developed by Tom Melham. These are intended to be a resource for anyone who wishes to teach HOL.

Case studies

The previous version of TUTORIAL contained a number of advanced case studies. These are now separate documents in the directory:

hol/Training/studies

The case studies in this directory are:

1. microprocessor: the specification and verification of a simple microprocessor, due to Jeff Joyce (joyce@cs.ubc.ca). This case study illustrates the state-of-the-art in an already mature area. Several new techniques are illustrated, including the use of temporal logic embedded in HOL for reasoning about asynchronous processes.

2. protocols: the specification and verification of a sliding window protocol, due to Rachel Cardell-Oliver (rco@cam.sri.com). This case study shows a new and rapidly evolving application of the HOL system that is currently an active area of research at Cambridge. There have been significant developments in this field since this study was written.

3. int mod: modular arithmetic of integers developed as an application of the group theory library, due to Elsa Gunter (elsa@research.att.com). This case study is a comprehensive tutorial on how one might conduct mathematical proof in type theory. It shows how to apply the abstract group theory library, which she wrote, to the development of a particular mathematical theory (modular arithmetic). Her paper Doing Algebra in Simple Type Theory is included with the case study for the reader’s convenience (it is also to be published elsewhere).

The case studies use different styles of proof in HOL, different ways of laying out ML code, etc. These reflect the differing aesthetic tastes and backgrounds of the authors. It is not intended that any of the styles is to be considered ‘standard’. There may eventually emerge a ‘Manual of Proof Style for HOL’, but it would be premature to try to write one now. It is a considerable virtue of Milner’s LCF approach to theorem proving that it so smoothly accommodates such a wide variety of styles, and yet maintains complete logical security.

The reader is warned that the case studies were developed for HOL88 Version 1.10 and it is possible that they will need to be modified to run in later versions of HOL. vi Preface

Contents

1 Getting and Installing HOL 1 1.1 Getting HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 The info-hol mailing list . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.3 Installing HOL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Building HOL from sources . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.4.1 Steps to make HOL under Unix . . . . . . . . . . . . . . . . . . . . 6 1.5 Other HOL users . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.6 HOL performance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.7 The HOL licence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.8 The REFERENCE browser . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 Introduction to ML 11 2.1 How to interact with ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 The HOL Logic 15 3.1 Overview of higher order logic . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

4 Introduction to Proof with HOL 27

4.1 Forward proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

4.1.1 Derived rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.2 Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4.3 Tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

5 Goal Oriented Proof: Tactics and Tacticals 37 5.1 Using tactics to prove theorems . . . . . . . . . . . . . . . . . . . . . . . . 41 5.2 Tacticals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

    5.2.1 THENL : tactic -> tactic list -> tactic . . . . . . . . . . . . 44
    5.2.2 THEN : tactic -> tactic -> tactic . . . . . . . . . . . . . . . . 45
    5.2.3 ORELSE : tactic -> tactic -> tactic . . . . . . . . . . . . . . 46

5.2.4 REPEAT : tactic -> tactic . . . . . . . . . . . . . . . . . . . . . 46 5.3 Some tactics built into HOL . . . . . . . . . . . . . . . . . . . . . . . . . . 47

5.3.1 REWRITE TAC : thm list -> tactic . . . . . . . . . . . . . . . . 47

5.3.2 CONJ TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.3.3 EQ TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.3.4 DISCH TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.3.5 GEN TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.3.6 IMP RES TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . 49 5.3.7 STRIP TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . 49 5.3.8 SUBST TAC : thm list -> thm . . . . . . . . . . . . . . . . . . . . 49 5.3.9 ACCEPT TAC : thm -> tactic . . . . . . . . . . . . . . . . . . . . 50 5.3.10 ALL TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 5.3.11 NO TAC : tactic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

6 Example: a simple parity checker 51 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 6.2 Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.3 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 6.4 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 6.5 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

6.5.1 Exercise 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 6.5.2 Exercise 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

7 How to program a proof tool 65 7.1 A simple implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 7.2 A more efficient implementation . . . . . . . . . . . . . . . . . . . . . . . . 72 7.3 An even more efficient implementation . . . . . . . . . . . . . . . . . . . . 74 7.4 Further optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 7.5 Normalizing all subterms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

7.5.1 Exercise 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 7.5.2 Exercise 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

8 Example: the Binomial Theorem 87 8.1 Pascal’s Triangle and the Binomial Theorem . . . . . . . . . . . . . . . . . 87 8.2 The Binomial Coefficients . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 8.3 Monoids, Groups and Commutative Rings . . . . . . . . . . . . . . . . . . 90

8.3.1 Associativity and Commutativity . . . . . . . . . . . . . . . . . . . 90 8.3.2 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 8.3.3 Groups . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 8.3.4 Rings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

8.4 Powers, Reductions, Ranges and Sums . . . . . . . . . . . . . . . . . . . . 96 8.4.1 Scalar powers in a monoid . . . . . . . . . . . . . . . . . . . . . . . 97 8.4.2 Reduction in a monoid . . . . . . . . . . . . . . . . . . . . . . . . . 97 8.4.3 Subranges of the natural numbers . . . . . . . . . . . . . . . . . . . 98 8.4.4 Σ-notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98

8.5 The Binomial Theorem for a Commutative Ring . . . . . . . . . . . . . . . 99 8.6 The Binomial Theorem for Integers . . . . . . . . . . . . . . . . . . . . . . 100 8.7 Principal lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

References 105

Chapter 1

Getting and Installing HOL

This chapter describes how to get the HOL system and how to install it. There is also a discussion of the optional Licence Agreement. It is assumed that a Sun workstation running Unix is being used, but the instructions that follow should apply mutatis mutandis to other platforms. Unix is not, however, a pre-requisite for using the system. HOL may be run an Apple Macintosh, where the system exhibits acceptable performance, and we are always interested in ports to other platforms. See Section 1.6 for details of HOL’s performance on various systems.

1.1 Getting HOL

The HOL system can either be obtained on tape from:

      Mike Gordon  hol-support%cam.sri.com
      University of Cambridge  hol-support@cl.cam.ac.uk

Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG, UK.

or on tape or by anonymous FTP from:

      Phil Windley  windley@cs.uidaho.edu

Department of Computer Science

University of Idaho

Moscow, ID 83843, USA.

To obtain HOL sources on tape, send a 450 foot Sun cassette or a 600 foot standard magnetic tape to one of the above contacts, together with sufficient funds to pay the cost of return postage. HOL is available via anonymous FTP at ted.cs.uidaho.edu (129.101.100.20) in the directory ~ftp/pub/hol.

1.2 The info-hol mailing list

Phil Windley has started a mailing list: info-hol@iris.eecs.ucdavis.edu which he set up to serve as a forum for discussing HOL and disseminating news about it. If you wish to be on this list (which is recommended for all users of HOL), or know of other people

who should be included, email to: info-hol-request@iris.eecs.ucdavis.edu.

1.3 Installing HOL

It is assumed that the HOL sources have been obtained and placed on a directory hol. The contents of this directory are likely to change over time, but it should contain the following:

Principal Files on the HOL Distribution Directory

File name  Description  File type
READ-ME  Description of directory hol  Text
Licence  L^{A}TEX source for optional HOL licence  Directory

Versions.2.01 Changes file since HOL88.2.0  Text

Versions  Previous changes files since HOL88.1.0  Directory
Makefile  Unix makefile for hol  Text
lisp  Lisp sources of HOL  Directory
ml  ML sources of HOL  Directory
theories  Built-in theories and files to construct them Directory
Library  HOL system library  Directory
Manual  Files for HOL system documentation  Directory
Training  Course material and exercises  Directory
help  Help files for HOL system  Directory
contrib  Misc. contributed HOL software  Directory
hol  Executable hol system (may be absent)  Executable
LOG  Log of a successful make (may be absent)  Text

The session in the box below shows a typical distribution directory. The HOL distribution has been mounted on a Sun running Unix on the directory /usr/groups/hol/sun3 sos.

All sessions in this documentation will be displayed in boxes with a number in the top right hand corner. This number indicates whether the session is a new one (when the number will be 1) or the continuation of a session started in an earlier box. Consecutively numbered boxes are assumed to be part of a single continuous session. The Unix prompt for the sessions is %, so lines beginning with this prompt were typed by the user. After entering the HOL system (see below), the user is prompted with # for an expression or command of the HOL meta-language ML; lines beginning with this are thus ML expressions or declarations. Lines not beginning with % or # are system output. The meta-language ML is introduced in Chapter 2.

1

 % pwd
 /usr/groups/hol/sun3_sos
 % ls -F
 LOG             Manual/         Versions/       hol*            theories/
 Library/        READ-ME         basic-hol*      hol-lcf*
 Licence/        Training/       contrib/        lisp/
 Makefile        Version.2.01    help/           ml/
 % ls -lF hol
 -rwxrwxr-x  1 tfm       3555997 May 18 20:18 hol*

If there is a suitable executable file hol in your distribution directory (as there is in the directory shown above), then it should be tried to see if it works. This is illustrated by continuing the session started above. The executable files hol-lcf and basic-hol are intermediate states in the construction of hol and can be deleted (see Makefile for more information).

2

 % hol
            ________________
    |___|    |    /_\  |__|__|  |       |__|  |  |  |
    |      |__|__/   \  __|  __| |  |__|  |  |__|  |__
           HOL88 Version 2.01 (Sun3/Franz), built on May 18 1992
 #

Note the ML prompt symbol #. Simple experiments with HOL can now be done directly, but for various theorem proving activities the system needs to be configured so that it knows where to find theory files and libraries. If the location of hol on your machine is, say:

    /usr/users/fred/dir1/dir2/hol

then HOL can be configured to know about this directory by typing:

    install `/usr/users/fred/dir1/dir2/hol`;;

to the running system. This is illustrated by continuing the session started above:

3

 #install `/usr/users/fred/dir1/dir2/hol`;;
 HOL installed (`/usr/users/fred/dir1/dir2/hol`)
 () : void
 #

4 Chapter 1. Getting and Installing HOL

An alternative to using the install command is to set the environment variable HOLPATH

in the shell. This variable contains the name of the directory in which the system is installed in much the same form as that expected by install. So, if this alternative method was being used to tell our existing system where its new installation area was, the following command would be required before invoking the system (C-shell is assumed):

    % setenv HOLPATH /usr/users/fred/dir1/dir2/hol

To eliminate the need to install the hol directory every time the system is used, an executable image can be saved with the installation already done. This is done by executing:

   save `name`;;

which will create a (large) executable file called name containing a saved state of the HOL system.

4

 #save `my-hol`;;
 () : void
 #quit();;
 % ls -l my-hol
 -rwxr-xr-x  1 hol       3601861 May 19 20:36 my-hol*
 %

This session also shows how to get out of HOL by typing:

    quit();;

After saving a copy of HOL, the new system (my-hol in the session above) can be used to run HOL without having to install local path names.

1

 % my-hol
            ________________
    |___|    |    /_\  |__|__|  |       |__|  |  |  |
    |      |__|__/   \  __|  __| |  |__|  |  |__|  |__
           HOL88 Version 2.01 (Sun3/Franz), built on May 18 1992
 #

Alas, the scenario sketched above does not always work:

1. There may not be a file hol on your distribution.

2. There may be a file hol, but it is not executable on your machine.

3. The file hol might execute, but the attempt to save a new version with local path names may fail (this is usually due to incompatibility between different versions of Unix).

1.4. Building HOL from sources 5

In case 1 or 2 you will need to rebuild HOL from sources (see Section 1.4). In case 3, it is probably best to eventually rebuild HOL, but you can survive for a while without doing this by always setting HOLPATH or by typing: install `path/hol`;; whenever you start (for a suitable string path), e.g. /usr/users/fred/dir1/dir2. If install is being used, as an alternative to this is to create a file called hol-init.ml in your home directory that contains the above install command. When HOL is run, the first thing it does is to look for a file called hol-init.ml and if one is found any commands in it are executed.

1

 % echo 'install `/usr/users/fred/dir1/dir2/hol`;;' > ~/hol-init.ml
 % cat ~/hol-init.ml
 install `/usr/users/fred/dir1/dir2/hol`;;
 % hol
            ________________
    |___|    |    /_\  |__|__|  |       |__|  |  |  |
    |      |__|__/   \  __|  __| |  |__|  |  |__|  |__
           HOL88 Version 2.01 (Sun3/Franz), built on May 18 1992

 HOL installed (`/usr/users/fred/dir1/dir2/hol`)
 () : void

 File hol-init loaded
 () : void
 #

Note that hol not my-hol was used, and the installation was done automatically.

• N.B. In order to be able to compile ML files (see the section ‘Compiling ML files’ in DESCRIPTION) it is also necessary to install a suitable Lisp system and compiler (called ‘Liszt’ for Franz Lisp). This is unlikely to be necessary for normal users of HOL. How to do this installation is described in Section 1.4 below.

1.4 Building HOL from sources

Under Unix, the HOL system is normally built using a makefile (hol/Makefile in the distribution). If you are not using a Unix machine, then see the directory hol/contrib/non-unix for instructions on proceeding.

The rest of this section explains how to build the HOL system under Unix using the make program. It is suggested that if you are familiar with this program then you should read hol/Makefile. If you are not familiar with make, then the instructions that follow should be sufficient (unless something unexpected goes wrong).

1.4.1 Steps to make HOL under Unix

Perform the following steps in the order given:

1. Delete the old system and object files by changing to the directory hol and then typing

(C-shell is assumed): setenv HOLdir .; make -e clobber; unsetenv HOLdir

2. Edit the following definitions in hol/Makefile. LispType is the first uncommented line in the file (lines begining with # are comments; Makefile starts with a large number of comments):

LispType= the type of Lisp used

Obj= the file extension of compiled object files

Lisp= the path name of the Lisp executable file

HOLdir= the absolute path name of the directory hol

The value of LispType should be franz for Franz Lisp and cl for Common Lisp (CL). The value of Obj should be o for Franz Lisp, Kyoto CL or Austin Kyoto CL, it should be lbin for Lucid CL and fasl for Allegro CL. For example, if Austin Kyoto CL is used and its executable image is /usr/bin/akcl, and

the hol directory is /usr/users/fred/dir1/dir2/hol then Makefile should contain:
   LispType=cl
   Obj=o
   Lisp=/usr/bin/akcl
   HOLdir=/usr/users/fred/dir1/dir2/hol

3. If you are using Franz Lisp, the following two definitions will also have to be changed. They are concerned with the location of the lisp compiler, liszt.

Liszt= the path name of the liszt executable

LisztComm= the command to be issued by hol to call liszt

In general, LisztComm will be the same as Liszt. For example, if the compiler is /usr/bin/liszt then the definitions would look like:

   Liszt=/usr/bin/liszt
   LisztComm=/usr/bin/liszt

Ignore this step if you are not using Franz Lisp.

4. Commence the rebuilding of hol by typing (in the directory hol) the following command:

   make all >& NEW-LOG&

This should be done overnight as, assuming all goes well, it will take many hours. The result will be a new executable file hol in the directory hol. The two files hol-lcf and basic-hol created during the build may be deleted after it has completed.

If these steps do not work, then you will need to get a hacker who understands the make program to look at Makefile. The file LOG on the distribution tape is a record of the execution of make used to build the system (warning: this file may not be present, or may be incomplete).

1.5. Other HOL users 7

1.5 Other HOL users

Users interested in research projects that make use of HOL are directed to the directory hol/contrib/hol users. The L^{A}TEX source for a list of short project descriptions is located there. The list does not represent all ongoing research, but only those projects for which users of the system have supplied us with a précis. We encourage new users of the system to inform us regarding its application so that we may update this list.

1.6 HOL performance

The following table contains the results of running the HOL benchmark found in the directory hol/contrib/benchmark on a variety of platforms using different lisps.

Benchmark Results

Machine  Lisp  Memory Window System Run Time
Sun3/260  Franz Lisp (38.92) 16Mb  NONE  147.6 sec
Sun3/80  Franz Lisp (38.92) 12Mb  X (R4)  256.4 sec
Sun3/260  AKCL  16Mb  NONE  538.6 sec
Sun3/80  AKCL  12Mb  X (R4)  830.5 sec
Sparc SLC  Allegro  16Mb  X (R4)  214.4 sec
Sparc SLC  AKCL  16Mb  X (R4)  278.2 sec
Sparc IPC  Allegro  16Mb  X (R4)  174.9 sec
Sparc IPC  AKCL  16Mb  X (R4)  235.2 sec
Sparc1  Allegro  16Mb  SunView  223.5 sec
Sparc1  Allegro  16Mb  X (R4)  229.6 sec
Sparc1  AKCL  16Mb  SunView  280.4 sec
Sparc1+  Allegro  28Mb  NONE  182.4 sec
Sparc1+  AKCL  28Mb  NONE  233.1 sec
SparcServ  Lucid  64Mb  NONE  102.7 sec
SparcServ  AKCL  64Mb  NONE  238.4 sec
Sparc2  Allegro  32Mb  SunView  124.1 sec
Sparc2  AKCL  32Mb  SunView  148.0 sec
HP9000/750  AKCL  32Mb  HP VUE  83.2 sec
DS5000/200  KCL  48Mb  NONE  287.6 sec
33MHz 486 PC Procyon 3.0  8Mb  Windows 3.0 151.9 sec
Macintosh IIfx Procyon 2.1  8Mb  Mac OS  302.5 sec
Macintosh IIci Procyon 2.1  8Mb  Mac OS  371.6 sec

1.7 The HOL licence

HOL is a public domain system and is available free. The bulk of the system is based on code written, in alphabetical order, by Mike Gordon, Gerard Huet (and others at Inria), Tom Melham, Robin Milner, Lockwood Morris, Malcolm Newey, Larry Paulson and Chris Wadsworth. Many others have supplied parts of the system, bugfixes etc.

Some users have asked to be issued with a HOL licence. This is to legitimate their use of the system for commercial purposes and to guarantee continued access. After consultation with Robin Milner and the Cambridge University computing service (who have experience with software licencing), the licence agreement given below was produced (the L^{A}TEX source for a typeset version is in the directory Licence at the top of the HOL distribution tape). The primary aims of the licence are:

(i) to prevent us being ‘ripped off’ or sued;

(ii) to prevent people claiming to have done a proof using HOL when in fact they used their own insecure modifications of it (in this case the licence merely requires the system to be called something else, it does not prevent such modifications being made).

The signing of the licence is optional, but encouraged. Users of HOL are free to redistribute the system to others provided they let Mike Gordon know in writing. The simplest way to do this is to ask the party to whom HOL is given to sign the licence and send it to Mike.

1.8 The REFERENCE browser

There is an X-windows documentation browser available with HOL, written by Sara Kalvala. This is not part of the HOL system, but is distributed with the sources in hol/contrib/Xhelp; it provides convenient access to the reference manual REFERENCE and is likely to be very useful to new users.

1.8. The REFERENCE browser 9

Distribution Agreement for the HOL System

The University of Cambridge Computer Laboratory is prepared to make available to:

hereafter referred to as ‘the User’, the HOL proof assistant system, hereafter referred to as ‘the Software’, subject to the following terms:

1. The University of Edinburgh, the University of Cambridge and Inria, hereafter referred to as ‘the Developers’, retain the copyright and all other legal rights to those parts of the software that they respectively developed, and they confirm that the sum of such parts constitute the whole. The User will ensure that the software in all its derivations carries a copyright notice of the form:

© University of Edinburgh, © University of Cambridge, © Inria

2. The User may employ the Software for any personal or internal purpose, but not as part or whole of any system to be distributed for commercial gain. The User shall be entitled to develop derivations of the Software and to make the Software and its derivations available to others, without charge, for research and for evaluating products developed by the User.

3. The User shall not declare theorems to have been proved using HOL unless they were proved with an authorized version of the HOL system. An executable binary file supplied by the Developers, or built using a Makefile supplied by them, constitutes an authorized version of HOL. Versions of HOL developed by the User are not authorized unless so designated, in writing, by the Developers.

4. The User will notify the University of Cambridge Computer Laboratory, in writing, of any significant derivations of the Software made by the User. The User will also notify the University of Cambridge Computer Laboratory, in writing, of all persons or organizations to whom such derivations are distributed.

5. The Software is made available on an as is basis; no guarantee of maintenance or reliability is provided by the Developers.

6. The User shall not hold the Developers liable for any consequences arising from use of the Software whether by himself or by any other party. The User shall indemnify the Developers and their staff against any claim by any third party arising from or in connection with the use of the Software, other than a claim for copyright infringement.

Signed:. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Position: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Date: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

10 Chapter 1. Getting and Installing HOL

Introduction to ML

This chapter is a brief introduction to the meta-language ML. The aim is just to give a feel for what it is like to interact with the language. A more detailed introduction can be found in

DESCRIPTION.

2.1 How to interact with ML

ML is an interactive programming language like Lisp. At top level one can evaluate expressions and perform declarations. The former results in the expression’s value and type being printed, the latter in a value being bound to a name.

The normal way to interact with ML is to configure the workstation screen so that there are two windows:

(i) An editor window into which ML commands are initially typed and recorded.

(ii) A shell window (or non-Unix equivalent) which is used to evaluate the commands.

A common way to achieve this is to work inside Emacs with a text window and a shell window.

After typing a command into the edit (text) window it can be transferred to the shell and evaluated in HOL by ‘cut-and-paste’. In Emacs this is done by copying the text into a buffer and then ‘yanking’ it into the shell. On an IBM PC it can be done using a proprietary window system; on a Macintosh it can be done using the Mac’s window system. The advantage of working via an editor is that if the command has an error, then the text can simply be edited and used again; it also records the commands in a file which can then be used again (via a batch load) later. In Emacs, the shell window also records the session, including both input from the user and the system’s response. The sessions in this tutorial were produced this way. These sessions are split into segments displayed in boxes with a number in their top right hand corner (to indicate their position in the complete session).

The interactions in these boxes should be understood as occurring in sequence. For example, variable bindings made in earlier boxes are assumed to persist to later ones. To enter the HOL system one types hol to Unix.^{1} The HOL system then prints a sign-on message and puts one into ML. The ML prompt is #, so lines beginning with # are typed by the user and other lines are the system’s response.

1The Unix prompt is %.

12 Chapter 2. Introduction to ML

1

 % hol
           _________
    |___|__|   |  |   |     |__|  |__|
    |      |  |   |__|   |__|__|  |__|
           Version 2.0 (Sun3/Franz), built on Sep 1 1991
 #1.[2;3;4;5];;
 [1; 2; 3; 4; 5] : int list

The ML expression 1.[2;3;4;5] has the form e_{1} op e_{2} where e_{1} is the expression 1 (whose value is the integer 1), e_{2} is the expression [2;3;4;5] (whose value is a list of four integers) and op is the infixed operator ‘.’ which is like Lisp’s cons function. Other list processing functions include hd (car in Lisp), tl (cdr in Lisp) and null (null in Lisp). The double semicolon ‘;;’ terminates a top-level phrase. The system’s response is shown on the line not starting with a prompt. It consists of the value of the expression followed, after a colon, by its type. The ML type checker infers the type of expressions using methods invented by Robin Milner [7]. The type int list is the type of ‘lists of integers’; list is a unary type operator. The type system of ML is very similar to the type system of the HOL logic which is explained in Chapter 3.

The value of the last expression evaluated at top-level in ML is always remembered in a variable called it.

2

 #let l = it;;
 l = [1; 2; 3; 4; 5] : int list
 #tl l;;
 [2; 3; 4; 5] : int list
 #hd it;;
 2 : int
 #tl(tl(tl(tl(tl l))));;
 [] : int list

Following standard λ-calculus usage, the application of a function f to an argument x can be written without brackets as f x (although the more conventional f(x) is also allowed). The expression f x_{1} x_{2} ⋯ x_{n} abbreviates the less intelligible expression (⋯((f x_{1})x_{2})⋯)x_{n} (function application is left associative).

Declarations have the form let x_{1}=e_{1} and ⋯ and x_{n}=e_{n} and result in the value of each expression e_{i} being bound to the name x_{i}.

3

 #let l1 = [1;2;3] and l2 = [`a`;`b`;`c`];;
 l1 = [1; 2; 3] : int list
 l2 = [`a`; `b`; `c`] : string list

ML expressions like `a`, `b`, `foo` etc. are strings and have type string. Any sequence of ASCII characters can be written between the quotes. The function words splits a single string into a list of single character strings, using space as separator.

2.1. How to interact with ML 13

4

#words`a b c`;;
[`a`; `b`; `c`] : string list

An expression of the form (e_{1},e_{2}) evaluates to a pair of the values of e_{1} and e_{2}. If e_{1} has type σ_{1} and e_{2} has type σ_{2} then (e_{1},e_{2}) has type σ_{1}#σ_{2}. A tuple (e_{1},…,e_{n}) is equivalent to (e_{1},(e_{2},…,e_{n})) (i.e. ‘,’ is right associative). The brackets around pairs and tuples are optional; the system doesn’t print them. The first and second components of a pair can be extracted with the ML functions fst and snd respectively.

5

#(1,true,`abc`);;
(1,true, `abc`) : (int # bool # string)
#snd it;;
(true, `abc`) : (bool # string)

#fst it;;
true : bool

The ML expressions true and false denote the two truth values of type bool.

ML types can contain the type variables *, **, ***, etc. Such types are called polymorphic. A function with a polymorphic type should be thought of as possessing all the types obtainable by replacing type variables by types. This is illustrated below with the function zip.

Functions are defined with declarations of the form let f v_{1} … v_{n} = e where each v_{i} is either a variable or a pattern built out of variables.^{2} Recursive functions are declared with letrec instead of let.

The function zip, below, converts a pair of lists ([x_{1};…;x_{n}], [y_{1};…;y_{n}]) to a list of pairs [(x_{1},y_{1});…;(x_{n},y_{n})].

6

#letrec zip(l1,l2) =
#if null l1 or null l2
# then []
# else (hd l1,hd l2).zip(tl l1,tl l2);;
zip = - : ((* list # ** list) -> (* # **) list)
#zip([1;2;3],[`a`;`b`;`c`]);;
[(1,`a`); (2,`b`); (3,`c`)] : (int # string) list

Functions may be curried, i.e. take their arguments ‘one at a time’ instead of as a tuple. This is illustrated with the function curried_zip below:

7

#let curried_zip l1 l2 = zip(l1,l2);;
curried_zip = - : (* list -> ** list -> (* # **) list)
#let zip_num = curried_zip [0;1;2];;
zip_num = - : (* list -> (int # *) list)
#zip_num [`a`;`b`;`c`];;
[(0, `a`); (1, `b`); (2, `c`)] : (int # string) list

2The chapters on ML in DESCRIPTION give exact details.

14 Chapter 2. Introduction to ML

Curried functions are useful because they can be ‘partially applied’ as illustrated above by the partial application of curried_zip to [0;1;2] which results in the function zip_num.

The evaluation of an expression either succeeds or fails. In the former case, the evaluation returns a value; in the latter case the evaluation is aborted and a failure string (usually the name of the function that caused the failure) is passed to whatever invoked the evaluation. This context can either propagate the failure (this is the default) or it can trap it. These two possibilities are illustrated below. A failure trap is an expression of the form e_{1}?e_{2}. An expression of this form is evaluated by first evaluating e_{1}. If the evaluation succeeds (i.e. doesn’t fail) then the value of e_{1}?e_{2} is the value of e_{1}. If the evaluation of e_{1} fails, then the value of e_{1}?e_{2} is obtained by evaluating e_{2}.

8

 #hd[];;
 evaluation failed     hd
 #hd[] ? `hd applied to empty list`;;
 `hd applied to empty list` : string

The sessions above are enough to give a feel for ML. For a much longer example, which illustrates most of the main features of the language, see the introduction to ML in DESCRIPTION.

In the next chapter, the logic supported by the HOL system (higher order logic) will be introduced, together with the tools in ML for manipulating it.

The HOL Logic

The HOL system supports higher order logic. This is a version of predicate calculus with three main extensions:

• Variables can range over functions and predicates (hence ‘higher order’).

• The logic is typed.

• There is no separate syntactic category of formulae (terms of type bool fulfill their role).

3.1 Overview of higher order logic

It is assumed the reader is familiar with predicate logic. The syntax and semantics of the particular logical system supported by HOL is described in detail in DESCRIPTION. The table below summarizes the notation used.

Terms of the HOL Logic

Kind of term  HOL notation Standard notation Description
Truth  T  ⊤  true
Falsity  F  ⊥  false
Negation  ~t  ¬t  not t
Disjunction  t_{1}\/t_{2}  t_{1} ∨ t_{2}  t_{1} or t_{2}
Conjunction  t_{1}/\t_{2}  t_{1} ∧ t_{2}  t_{1} and t_{2}
Implication  t_{1}==>t_{2}  t_{1} ⇒ t_{2}  t_{1} implies t_{2}
Equality  t_{1}=t_{2}  t_{1} = t_{2}  t_{1} equals t_{2}
∀-quantification !x.t  ∀x. t  for all x : t
∃-quantification ?x.t  ∃x. t  for some x : t
ε-term  @x.t  εx. t  an x such that: t
Conditional  (t=>t_{1}|t_{2})  (t → t_{1}, t_{2})  if t then t_{1} else t_{2}

16 Chapter 3. The HOL Logic

Terms of the HOL logic are represented in ML by an abstract type^{1} called term. They are normally input between quotation marks, and anything between a pair of quotation symbols is parsed as a logical term. For example, the expression "x /\ y ==> z" evaluates in ML to a term representing x∧y⇒z. Terms can be manipulated by various built-in ML functions. For example, the ML function dest_imp with ML type term -> term # term splits an implication into a pair of terms consisting of its antecedent and consequent, and the ML function dest_conj of type term -> term # term splits a conjunction into its two conjuncts.

1Abstract types appear to the user as primitive types with a collection of operations; they are described in DESCRIPTION

1

#"x /\ y ==> z";;
"x /\ y ==> z" : term
#dest_imp it;;
("x /\ y", "z") : (term # term)
#dest_conj(fst it);;
("x", "y") : (term # term)

Terms of the HOL logic are quite similar to ML expressions, and this can at first be confusing. Indeed, terms of the logic have types similar to those of ML expressions. For example, "(1,2)" is an ML expression with ML type term. The HOL type of this term is num#num. By contrast, the ML expression ("1","2") has type term#term.

The types of HOL terms form an ML type called type. Expressions having the form ": ⋯ " evaluate to logical types. The built-in function type_of has ML type term->type and returns the logical type of a term.

2

#"(1,2)";;
"1,2" : term
#type_of it;;
":num # num" : type
#("1","2");;
("1", "2") : (term # term)
#type_of(fst it);;
":num" : type

To try to minimise confusion between the logical types of HOL terms and the ML types of ML expressions, the former will be referred to as object language types and the latter as metalanguage types. For example, "(1,T)" is an ML expression that has meta-language type term and evaluates to a term with object language type ":num#bool".

3

#"(1,T)";;
"1,T" : term
#type_of it;;
":num # bool" : type

HOL terms can be input using explicit quotation, as above, or they can be constructed using ML constructor functions. The function mk_var constructs a variable from a string and a type. In the example below, three variables of type bool are constructed. These are used later.

\underline{3.2. Terms 17}

4

#let x = mk_var(`x`,":bool")
#and y = mk_var(`y`,":bool")
#and z = mk_var(`z`,":bool");;
x = "x" : term
y = "y" : term
z = "z" : term

The constructors mk_conj and mk_imp construct conjunctions and implications respectively.

5

#let t = mk_imp(mk_conj(x,y),z);;
t = "x /\ y ==> z" : term

3.2 Terms

There are only four different kinds of terms:

1. Variables.

2. Constants.

3. Function applications: "t_{1} t_{2}".

4. λ-abstractions: "\x.t".

Both variables and constants have a name and a type; the difference is that constants cannot be bound by quantifiers, and their type is fixed when they are declared (see below). The type checking algorithm uses the types of constants to infer the types of variables in the same quotation. If there is not enough type information a type checking error results:

6

#"~x";;
"~x" : term
#"x";;
Indeterminate types:  "x:?"
evaluation failed     types indeterminate in quotation

In the first case, the HOL type checker used the known type bool->bool of ~ to deduce that the variable x must have type bool. In the second case, it cannot deduce the type of x. Unlike in ML, there must be enough information in a quotation to fully determine the type of all subterms. The default ‘scope’ of type information for type checking is a single quotation, so a type in one quotation cannot affect the type-checking of another. This scoping can be altered by using the sticky type facility, which can be used to give default types to variables (see the appropriate section of DESCRIPTION for details). If there is not enough contextuallydetermined type information to resolve the types of all variables in a quotation, then it is necessary to explicitly indicate the required types by using "term:type" as illustrated below.

7

#"x:num";;
"x" : term
#type_of it;;
":num" : type

Functions have types of the form σ_{1}->σ_{2}, where σ_{1} and σ_{2} are the types of the domain and range of the function, respectively.

8

#type_of "==>";;
":bool -> (bool -> bool)" : type
#type_of "+";;
":num -> (num -> num)" : type

Both + and ==> are infixes. The session below illustrates this; it also illustrates object language versus meta-language types.

9

#"(x+1), (t1==>t2)";;
"x + 1,(t1 ==> t2)" : term
#type_of it;;
":num # bool" : type
#"x=1","t1==>t2";;
("x = 1", "t1 ==> t2") : (term # term)
#type_of(fst it), type_of(snd it);;
(":bool", ":bool") : (type # type)

The types of constants are declared in theories; this is described in Section 3.3.

An application t_{1} t_{2} is badly typed if t_{1} is not a function:

10

#"1 2";;
Badly typed application of:  "1"
   which has type:           ":num"
to the argument term:        "2"
   which has type:           ":num"
evaluation failed     mk_comb in quotation

or if it is a function, but t_{2} is not in its range:

11

#"~1";;
Badly typed application of:  "$~"
   which has type:           ":bool -> bool"
to the argument term:        "1"
   which has type:           ":num"
evaluation failed     mk_comb in quotation

The dollar in front of ~ indicates that the constant has a special syntactic status (in this case a non-standard precedence). Putting $ in front of any symbol causes the parser to ignore any special syntactic status (like being an infix) it might have.

3.3. Theories 19

12

 #"$==> t1 t2";;
 "t1 ==> t2" : term

Lambda-terms, or λ-terms, denote functions. The symbol ‘\’ is used as an ASCII approximation to λ. Thus ‘\x.t’ should be read as ‘λx. t’. For example, "\x. x+1" is a term that denotes the function n ↦ n+1.

13

 #"\x.x+1";;
 "\x. x + 1" : term
 #type_of it;;
 ":num -> num" : type

3.3 Theories

The result of a session with the HOL system is an object called a theory. This object is closely related to what a logician would call a theory, but there are some differences arising from the needs of mechanical proof. A HOL theory, like a logician’s theory, contains sets of types, constants, definitions and axioms. In addition, however, a HOL theory contains an explicit list of theorems that have been proved from the axioms and definitions. Logicians normally do not need to distinguish theorems that have actually been proved from those that could be proved, hence they do not normally consider sets of proven theorems as part of a theory; rather, they take the theorems of a theory to be the (often infinite) set of all consequences of the axioms and definitions. Another difference between logicians’ theories and HOL theories is that, for logicians, theories are relatively static objects, but in HOL they can be thought of as potentially extendable. For example, the HOL system provides tools for adding to theories and combining theories. A typical interaction with HOL consists in combining some existing theories, making some definitions, proving some theorems and then saving the resulting new theory.

The purpose of the HOL system is to provide tools to enable well-formed theories to be constructed. All the theorems of such theories are logical consequences of the definitions and axioms of the theory. The HOL system ensures that only well-formed theories can be constructed by allowing theorems to be created by formal proof only.

A theory is represented in the HOL system as a collection of files, called theory files. Each file has a name of the form name.th, where name is a string supplied by the user.

Theory files are structured hierarchically to represent sequences of extensions of an initial theory called HOL. Each theory file making up a theory records some types, constants, axioms and theorems, together with pointers to other theory files called its parents. This collection of reachable files is called the ancestry of the theory file. Axioms, definitions and theorems are named in the HOL system by two strings: the name of the theory file where they are stored, together with a name within that file supplied by the user. Specifically, axioms, definitions and theorems are named by a pair of strings ⟨thy, name⟩ where thy is the name of the theory current when the item was declared and name is a specific name supplied by the user (see the functions

new_axiom, new_definition etc. below).

A typical piece of work with the HOL system consists in a number of sessions. In the first of these a new theory, T say, is created by extending existing theories with a number of definitions. The concrete result of the session will be a theory file T .th whose contents are created during the session and whose ancestry represents the desired logical theory. In subsequent sessions this theory is extended by proving new theorems which will be stored in the file T .th. The logical meaning of these sessions is that a new extension to T is created which replaces the old version. Subsequent pieces of work can build on (i.e. extend) the definitions and theorems of T by making it a parent of new theories.

There are two modes of working with HOL: draft mode and proof mode. In draft mode, inconsistencies can be introduced by asserting inconsistent axioms, but in proof mode only consistency preserving actions (namely valid proof) can be done. Draft mode is analogous to ‘super user mode’ in Unix, in that it gives access to dangerous facilities. Everything that can be done in proof mode can be done in draft mode, but not vice versa.

There is always a current theory, whose name is given by the function current_theory. This function maps the value void, written ‘()’ in ML, to a string giving the name of the current theory. Thus the ML expression current_theory () evaluates to a string giving the name of the current theory. Initially HOL is in proof mode with current theory called HOL. So evaluating current_theory () immediately after initiating a HOL session gives the value `HOL`, as can be seen in the session shown below:

1

 % hol
           _________
    |___|__|   |  |   |     |__|  |__|
    |      |  |   |__|   |__|__|  |__|
           Version 2.0, built on Sep 1 1991
 #current_theory();;
 `HOL` : string
 #

Executing new_theory`thy` creates a new theory called thy; it fails if there already exists a file thy.th in the current working directory (or in any directory on the current HOL search path, for a description of which, see the appropriate section of DESCRIPTION).

2

 #new_theory `Peano`;;
 () : void

This starts a theory called Peano, which is to be made into a theory containing Peano’s postulates as axioms for the natural numbers.^{2} These postulates, stated informally, are:

P1 There is a number 0.

P2 There is a function Suc called the successor function such that if n is a number then Suc n is a number.

P3 0 is not the successor of any number.

2An elaborate theory of numbers is built into HOL, in which Peano’s postulates are in fact derived theorems rather than postulated as axioms.

P4 If two numbers have the same successor then they are equal.

P5 If a property holds of 0, and if whenever it holds of a number then it also holds of the successor of the number, then the property holds of all numbers. This postulate is called Mathematical Induction.

To fomalize this in HOL a new type is introduced called nat:

3

#new_type 0 `nat`;;
() : void

In general new_type n `op` makes op a new n-ary type operator in the current theory. Constant types are regarded as degenerate type operators with no arguments, thus the new type nat is declared to be a 0-ary type operator. The type operator list is an example of a 1-ary operator, types built with list are written as σ list. The type operator prod is 2-ary, types using it are written as (σ_{1},σ_{2})prod (which can, in fact, be written as σ_{1}#σ_{2}).

The axioms P1 and P2 can now be formalized by declaring two new constants of type nat to represent 0 and Suc.

Evaluating new_constant(`c`,σ) makes c a new constant of type σ in the current theory. This fails if:

(i) not in draft mode;

(ii) there already exists a constant named c in the current theory.

4

#new_constant(`0`, ":nat");;
evaluation failed     new_constant -- 0 clashes with existing constant

The symbol 0 is already a constant of the built-in theory num, and this prevents us using it as a constant of our new theory. The symbol O will be used instead.

5

#new_constant(`O`,":nat");;
() : void
#new_constant(`Suc`, ":nat->nat");;
() : void

The HOL type checker ensures that P1 and P2 hold. P3 is now asserted as an axiom:

6

#new_axiom(`P3`, "!n. ~(O = Suc n)");;
|- !n. ~(O = Suc n)

This creates an axiom in the current theory (i.e. in Peano) called P3. Axiom P4 can be declared similarly:

7

#new_axiom(`P4`, "!m n. (Suc m = Suc n) ==> (m = n)");;
|- !m n. (Suc m = Suc n) ==> (m = n)

The final Peano axiom is Mathematical Induction:

8

#new_axiom(`P5`,"!P. P O /\ (!n. P n ==> P(Suc n)) ==> (!n. P n)");;
|- !P. P O /\ (!n. P n ==> P(Suc n)) ==> (!n. P n)

To inspect the theory, the function print_theory can be used:

9

#print_theory `Peano`;;
The Theory Peano
Parents --  HOL
Types --  ":nat"
Constants --  O ":nat"     Suc ":nat -> nat"
Axioms --
  P3  |- !n. ~(O = Suc n)
  P4  |- !m n. (Suc m = Suc n) ==> (m = n)
  P5  |- !P. P O /\ (!n. P n ==> P(Suc n)) ==> (!n. P n)
******************** Peano ********************
#

To end the session and write out the various declarations into the theory file Peano.th the function close_theory is used.

10

#close_theory();;
() : void
#quit();;
% ls Peano.th
Peano.th
%

The function quit exits from the HOL system.

The preceding session set up a theory called Peano. It is usual to include in ‘Peano arithmetic’ axioms defining addition and multiplication. To do this a new session can be started and the theory extended.

11

% hol
          _________
   |___|__|   |  |   |     |__|  |__|
   |      |  |   |__|   |__|__|  |__|
          Version 2.0 (Sun3/Franz), built on Sep 1 1991
#extend_theory `Peano`;;
Theory Peano loaded
() : void

The two new axioms can now be added, but first constants add and mult must be declared to represent addition and multiplication (the symbols + and * are already in use). These can be declared as infixes using new_infix instead of new_constant.

12

#new_infix(`add`,":nat->nat->nat");;
() : void
#new_infix(`mult`,":nat->(nat->nat)");;
() : void

Constants declared with new_infix must have a type of the form σ->(σ->σ).

Axioms defining add and mult can now be defined.

13

#new_axiom
# (`add_def`,
#  "(!n. O add n = n) /\ (!m n. (Suc m) add n = Suc(m add n))");;
|- (!n. O add n = n) /\ (!m n. (Suc m) add n = Suc(m add n))
#new_axiom
# (`mult_def`,
#  "(!n. O mult n = O) /\ (!m n. (Suc m) mult n = (m mult n) add n)");;
|- (!n. O mult n = O) /\ (!m n. (Suc m) mult n = (m mult n) add n)

The theory Peano has now been extended to contain the new definitions.

This example shows how a theory is set up. How to prove consequences of axioms and definitions is described later. The HOL system contains a built-in theory of numbers called num which contains Peano’s postulates and a (descendent) theory arithmetic containing the definitions of addition (+) and multiplication (*) and other things. In fact, Peano’s postulates are theorems not axioms in the theory num. The primitive constants 0 and SUC (corresponding to O and Suc in Peano) are defined in terms of purely logical notions. In HOL, definitions are a special kind of axiom that are guaranteed to be consistent. The commonest (but not only) form of a definition is:

f x_{1} … x_{n} = t

where f is declared to be a new constant satisfying this equation (and t is a term whose free variables are included in the set {x_{1}, …, x_{n}}). Such definitions cannot be recursive because, for example:

f x = (f x) + 1

would imply 0 = 1 (subtract f x from both sides) and is therefore inconsistent. An example of a definition is:

14

#new_definition(`Double_def`, "Double x = x add x");;
|- !x. Double x = x add x

This definition both declares Double as a new constant of the appropriate type and asserts the defining equation as a definitional axiom.

15

#print_theory `Peano`;;
The Theory Peano
Parents --  HOL
Types --  ":nat"
Constants --
  add ":nat -> (nat -> nat)"     mult ":nat -> (nat -> nat)"
  O ":nat"     Suc ":nat -> nat"     Double ":nat -> nat"
Infixes --
  add ":nat -> (nat -> nat)"     mult ":nat -> (nat -> nat)"
Axioms --
  P3  |- !n. ~(O = Suc n)
  P4  |- !m n. (Suc m = Suc n) ==> (m = n)
  P5  |- !P. P O /\ (!n. P n ==> P(Suc n)) ==> (!n. P n)
  add_def  |- (!n. O add n = n) /\ (!m n. (Suc m) add n = Suc(m add n))
  mult_def
    |- (!n. O mult n = O) /\ (!m n. (Suc m) mult n = (m mult n) add n)
Definitions --  Double_def  |- !x. Double x = x add x
******************** Peano ********************

The use of axioms, as illustrated here, carries considerable danger in general because it is very easy to assert inconsistent axioms. It is thus safer to use only definitions. At first sight this might appear impossible, but in fact all of ordinary mathematics can be developed from logic by definition alone. Showing this was the achievement of Russell and Whitehead in their treatise Principia Mathematica [12]. A theory containing only definitions is called a definitional theory. Many useful definitional theories are built into the HOL system, or available as libraries. Examples include theories of numbers (both natural numbers and integers), sets, bags, finite trees, group theory, properties of fixed points and more. Libraries are constantly being added to HOL and users are encouraged to contribute new theories to the library when they develop them.

The theory of numbers built into HOL is a definitional theory that defines numbers logically. Peano’s postulates are proved from the definitions of the type num and the constants 0 and SUC. It follows from Peano’s postulates that certain kinds of recursion equations are equivalent to non-recursive definitions. There is a built-in theory called prim_rec (for ‘primitive recursion’) that supports this, together with tools for automatically transforming recursion equations into definitions. This is illustrated later but, for example, here are the built-in definitions of + and

*:

16

 #ADD;;
 Definition ADD autoloaded from theory `arithmetic`.
 ADD = |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
 |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
 #MULT;;
 Definition MULT autoloaded from theory `arithmetic`.
 MULT = |- (!n. 0 * n = 0) /\ (!m n. (SUC m) * n = (m * n) + n)
 |- (!n. 0 * n = 0) /\ (!m n. (SUC m) * n = (m * n) + n)

This also illustrates how certain built-in definitions (and theorems) are ‘autoloaded’ from the theories where they are defined (arithmetic in this case).

The theory arithmetic contains too many pre-proved theorems to show in full, but here are the constants, definitions, and the first two (out of 113) theorems.

17

#print_theory `arithmetic`;;
The Theory arithmetic
Parents --  BASIC-HOL     prim_rec
Constants --
+ ":num -> (num -> num)"     - ":num -> (num -> num)"
* ":num -> (num -> num)"     EXP ":num -> (num -> num)"
> ":num -> (num -> bool)"     <= ":num -> (num -> bool)"
>= ":num -> (num -> bool)"     MOD ":num -> (num -> num)"
DIV ":num -> (num -> num)"
Infixes --
+ ":num -> (num -> num)"     - ":num -> (num -> num)"
* ":num -> (num -> num)"     EXP ":num -> (num -> num)"
> ":num -> (num -> bool)"     <= ":num -> (num -> bool)"
>= ":num -> (num -> bool)"     MOD ":num -> (num -> num)"
DIV ":num -> (num -> num)"
Definitions --
ADD  |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
SUB
  |- (!m. 0 - m = 0) /\
     (!m n. (SUC m) - n = (m < n => 0 | SUC(m - n)))
MULT  |- (!n. 0 * n = 0) /\ (!m n. (SUC m) * n = (m * n) + n)
EXP  |- (!m. m EXP 0 = 1) /\ (!m n. m EXP (SUC n) = m * (m EXP n))
GREATER  |- !m n. m > n = n < m
LESS_OR_EQ  |- !m n. m <= n = m < n \/ (m = n)
GREATER_OR_EQ  |- !m n. m >= n = m > n \/ (m = n)
DIVISION
  |- !n.
      0 < n ==>
      (!k. (k = ((k DIV n) * n) + (k MOD n)) /\ (k MOD n) < n)
Theorems --
SUC_NOT  |- !n. ~(0 = SUC n)
ADD_0  |- !m. m + 0 = m
.
.
.

Note that DIV is defined by a constant specification. See DESCRIPTION for further explanation.

Introduction to Proof with HOL

For a logician, a formal proof is a sequence, each of whose elements is either an axiom or follows from earlier members of the sequence by a rule of inference. A theorem is the last element of a proof.

Theorems are represented in HOL by values of an abstract type^{1} thm. The only way to create theorems is by generating a proof. In HOL (following LCF), this consists in applying ML functions representing rules of inference to axioms or previously generated theorems. The sequence of such applications directly corresponds to a logician’s proof.

There are five axioms of the HOL logic and eight primitive inference rules. The axioms are bound to ML names. For example, the Law of Excluded Middle is bound to the ML name

BOOL_CASES_AX:

18

 #BOOL_CASES_AX;;
 |- !t. (t = T) \/ (t = F)

Theorems are printed with a preceding turnstile |- as illustrated above; the symbol ‘!’ is the universal quantifier ‘∀’. Rules of inference are ML functions that return values of type thm. An example of a rule of inference is specialization (or ∀-elimination). In standard ‘natural deduction’ notation this is:

\frac{Γ ⊢ ∀x. t}{Γ ⊢ t[t′/x]}

• t[t′/x] denotes the result of substituting t′ for free occurrences of x in t, with the restriction that no free variables in t′ become bound after substitution.

This rule is represented in ML by a function SPEC,^{2} which takes as arguments a term "a" and a theorem |- !x.t[x] and returns the theorem |- t[a], the result of substituting a for x in t[x].

1

 #let Th1 = BOOL_CASES_AX;;
 Th1 = |- !t. (t = T) \/ (t = F)
 #let Th2 = SPEC "1 = 2" Th1;;
 Th2 = |- ((1 = 2) = T) \/ ((1 = 2) = F)

This session consists of a proof of two steps: using an axiom and applying the rule SPEC; it interactively performs the following proof:

1Abstract types are explained in DESCRIPTION.

2SPEC is not a primitive rule of inference in the HOL logic, but is a derived rule. Derived rules are described in Section 4.1.

28 Chapter 4. Introduction to Proof with HOL

1. ⊢ ∀t. t = ⊤ ∨ t = ⊥ [Axiom BOOL_CASES_AX]

2. ⊢ (1=2) = ⊤ ∨ (1=2) = ⊥ [Specializing line 1 to ‘1=2’]

If the argument to an ML function representing a rule of inference is of the wrong kind, or violates a condition of the rule, then the application fails. For example, SPEC t th will fail if th is not of the form |- !x. · · · or if it is of this form but the type of t is not the same as the type of x, or if the free variable restriction is not met.

2

 #SPEC "1=2" Th2;;
 evaluation failed     SPEC
 #SPEC "1" Th1;;
 evaluation failed     SPEC

As this session illustrates, the failure token does not always indicate the exact reason for failure. The failure conditions for rules of inference are given in REFERENCE.

A proof in the HOL system is constructed by repeatedly applying inference rules to axioms or to previously proved theorems. Since proofs may consist of millions of steps, it is necessary to provide tools to make proof construction easier for the user. The proof generating tools in the HOL system are just those of LCF, and are described later.

The general form of a theorem is t_{1}, …, t_{n} |- t, where t_{1}, …, t_{n} are boolean terms called the assumptions and t is a boolean term called the conclusion. Such a theorem asserts that if its assumptions are true then so is its conclusion. Its truth conditions are thus the same as those for the single term (t_{1}/\…/\t_{n})==>t. Theorems with no assumptions are printed out in the form |- t.

The five axioms and eight primitive inference rules of the HOL logic are described in detail in the document DESCRIPTION. Every value of type thm in the HOL system can be obtained by repeatedly applying primitive inference rules to axioms. When the HOL system is built, the eight primitive rules of inference are defined and the five axioms are bound to their ML names, all other predefined theorems are proved using rules of inference as the system is made.^{3} This is one of the reasons why making hol takes so long.

In the rest of this chapter, the process of forward proof , which has just been sketched, is described in more detail. In Chapter 5 goal directed proof is described, including the important notions of tactics and tacticals, due to Robin Milner.

4.1 Forward proof

Three of the primitive inference rules of the HOL logic are ASSUME (assumption introduction), DISCH (discharging or assumption elimination) and MP (Modus Ponens). These rules will be used to illustrate forward proof and the writing of derived rules.

The inference rule ASSUME generates theorems of the form t |- t. Note, however, that the ML printer prints each assumption as a dot (but this default can be changed; see below). The function dest_thm decomposes a theorem into a pair consisting of list of assumptions and the conclusion. The ML type goal abbreviates (term)list # term, this is motivated in Section 5.

3This is a slight over-simplification.

4.1. Forward proof 29

3

#let Th3 = ASSUME "t1==>t2";;
Th3 = . |- t1 ==> t2
#dest_thm Th3;;
["t1 ==> t2"],"t1 ==> t2" : goal

A sort of dual to ASSUME is the primitive inference rule DISCH (discharging, assumption elimination) which infers from a theorem of the form ⋯ t_{1} ⋯ |- t_{2} the new theorem · · · · · · |- t_{1}==>t_{2}. DISCH takes as arguments the term to be discharged (i.e. t_{1}) and the theorem from whose assumptions it is to be discharged and returns the result of the discharging. The following session illustrates this; it also illustrates what happens when =>, which is part of the syntax of conditional terms (see the table on page 15), is erroneously typed instead of the implication symbol

==>.

4

#let Th4 = DISCH "t1=>t2" Th3;;
need 2 nd branch to conditional
skipping: t2 " Th3 ;; parse failed
#let Th4 = DISCH "t1==>t2" Th3;;
Th4 = |- (t1 ==> t2) ==> t1 ==> t2

Note that the term being discharged need not be in the assumptions; in this case they will be unchanged.

5

#DISCH "1=2" Th3;;
. |- (1 = 2) ==> t1 ==> t2
#dest_thm it;;
(["t1 ==> t2"], "(1 = 2) ==> t1 ==> t2") : goal

In HOL the rule MP of Modus Ponens is specified in conventional notation by:

\frac{Γ_{1} ⊢ t_{1} ⇒ t_{2} Γ_{2} ⊢ t_{1}}{Γ_{1} ∪ Γ_{2} ⊢ t_{2}}

The ML function MP takes argument theorems of the form ⋯ |- t_{1} ==> t_{2} and ⋯ |- t_{1} and returns ⋯ |- t_{2}. The next session illustrates the use of MP and also a common error, namely not supplying the HOL logic type checker with enough information.

6

#let Th5 = ASSUME "t1";;
Indeterminate types:  "t1:?"
evaluation failed     types indeterminate in quotation
#let Th5 = ASSUME "t1:bool";;
Th5 = . |- t1
#let Th6 = MP Th3 Th5;;
Th6 = .. |- t2

The hypotheses of Th6 can be inspected with the ML function hyp, which returns the list of assumptions of a theorem (the conclusion is returned by concl).

7

#hyp Th6;;
["t1 ==> t2"; "t1"] : term list

HOL can be made to print out hypotheses of theorems explicitly by telling ML to use the function print_all_thm instead of the default print_thm.

8

#top_print print_all_thm;;
- : (thm -> void)
#Th5;;
t1 |- t1
#Th6;;
t1 ==> t2, t1 |- t2

Discharging Th6 twice establishes the theorem |- t1 ==> (t1==>t2) ==> t2.

9

#let Th7 = DISCH "t1==>t2" Th6;;
Th7 = t1 |- (t1 ==> t2) ==> t2
#let Th8 = DISCH "t1:bool" Th7;;
Th8 = |- t1 ==> (t1 ==> t2) ==> t2

The sequence of theorems: Th3, Th5, Th6, Th7, Th8 constitutes a proof in HOL of the theorem |- t1 ==> (t1 ==> t2) ==> t2. In stardard logical notation this proof could be written:

1. t_{1} ⇒ t_{2} ⊢ t_{1} ⇒ t_{2} [Assumption introduction]

2. t_{1} ⊢ t_{1} [Assumption introduction]

3. t_{1} ⇒ t_{2}, t_{1} ⊢ t_{2} [Modus Ponens applied to lines 1 and 2]

4. t_{1} ⊢ (t_{1} ⇒ t_{2}) ⇒ t_{2} [Discharging the first assumption of line 3]

5. ⊢ t_{1} ⇒ (t_{1} ⇒ t_{2}) ⇒ t_{2} [Discharging the only assumption of line 4]

4.1.1 Derived rules

A proof from hypothesis th_{1}, …, th_{n} is a sequence each of whose elements is either an axiom, or one of the hypotheses th_{i}, or follows from earlier elements by a rule of inference.

For example, a proof of Γ, t′ ⊢ t from the hypothesis Γ ⊢ t is:

1. t′ ⊢ t′ [Assumption introduction]

2. Γ ⊢ t [Hypothesis]

3. Γ ⊢ t′ ⇒ t [Discharge t′ from line 2]

4.1. Forward proof 31

4. Γ, t′ ⊢ t [Modus Ponens applied to lines 3 and 1]

This proof works for any hypothesis of the form Γ ⊢ t and any boolean term t′ and shows that the result of adding an arbitrary hypothesis to a theorem is another theorem (because the four lines above can be added to any proof of Γ ⊢ t to get a proof of Γ, t′ ⊢ t).^{4} For example, the next session uses this proof to add the hypothesis "t3" to Th6.

10

#let Th9 = ASSUME "t3:bool";;
Th9 = t3 |- t3
#let Th10 = DISCH "t3:bool" Th6;;
Th10 = t1 ==> t2, t1 |- t3 ==> t2
#let Th11 = MP Th10 Th9;;
Th11 = t1 ==> t2, t1, t3 |- t2

A derived rule is an ML procedure that generates a proof from given hypotheses each time it is invoked. The hypotheses are the arguments of the rule. To illustrate this, a rule, called ADD_ASSUM, will now be defined as an ML procedure that carries out the proof above. In standard notation this would be described by:

\frac{Γ ⊢ t}{Γ, t′ ⊢ t}

The ML definition is:

11

#let ADD_ASSUM t th =
# let th9 = ASSUME t
# in
# let th10 = DISCH t th
# in
# MP th10 th9;;
ADD_ASSUM = - : (term -> thm -> thm)
#ADD_ASSUM "t3:bool" Th6;;
t1 ==> t2, t1, t3 |- t2

The body of ADD_ASSUM has been coded to mirror the proof done in session 10 above, so as to show how an interactive proof can be generalized into a procedure. But ADD_ASSUM can be written much more concisely as:

12

#let ADD_ASSUM t th = MP (DISCH t th) (ASSUME t);;
ADD_ASSUM = - : (term -> thm -> thm)
#ADD_ASSUM t3 Th6;;
t1 ==> t2, t1, t3 |- t2

4This property of the logic is called monotonicity.

Another example of a derived inference rule is UNDISCH; this moves the antecedent of an implication to the assumptions.

\frac{Γ ⊢ t_{1} ⇒ t_{2}}{Γ, t_{1} ⊢ t_{2}}

An ML derived rule that implements this is:

13

 #let UNDISCH th =
 # MP th (ASSUME(fst(dest_imp(concl th))));;
 UNDISCH = - : (thm -> thm)
 #Th10;;
 t1 ==> t2, t1 |- t3 ==> t2
 #UNDISCH Th10;;
 t1 ==> t2, t1, t3 |- t2
 #it = Th11;;
 true : bool

Each time UNDISCH Γ ⊢ t_{1} ⇒ t_{2} is executed, the following proof is performed:

1. t_{1} ⊢ t_{1} [Assumption introduction]

2. Γ ⊢ t_{1} ⇒ t_{2} [Hypothesis]

3. Γ, t_{1} ⊢ t_{2} [Modus Ponens applied to lines 2 and 1]

The rules ADD_ASSUM and UNDISCH are the first derived rules defined when the HOL system is built. For a description of the main rules see the section on derived rules in DESCRIPTION.

4.2 Rewriting

An important derived rule is REWRITE_RULE. This takes a list of conjunctions of equations, i.e. a list of theorems of the form:

Γ ⊢ (u_{1} = v_{1}) ∧ (u_{2} = v_{2}) ∧ … ∧ (u_{n} = v_{n})

and a theorem Δ ⊢ t and repeatedly replaces instances of u_{i} in t by the corresponding instance of v_{i} until no further change occurs. The result is a theorem Γ ∪ Δ ⊢ t′ where t′ is the result of rewriting t in this way. The session below illustrates the use of REWRITE_RULE. In it the list of equations is a list rewrite_list containing the pre-proved theorems ADD_CLAUSES and MULT_CLAUSES. These theorems autoload from the theory arithmetic. This means that the first time they are mentioned in a session, which is when rewrite_list is defined, they are automatically fetched and bound to their ML name.

4.2. Rewriting 33

14

#let rewrite_list = [ADD_CLAUSES;MULT_CLAUSES];;
Theorem MULT_CLAUSES autoloaded from theory `arithmetic`.
MULT_CLAUSES =
|- !m n.
    (0 * m = 0) /\
    (m * 0 = 0) /\
    (1 * m = m) /\
    (m * 1 = m) /\
    ((SUC m) * n = (m * n) + n) /\
    (m * (SUC n) = m + (m * n))
Theorem ADD_CLAUSES autoloaded from theory `arithmetic`.
ADD_CLAUSES =
|- (0 + m = m) /\
   (m + 0 = m) /\
   ((SUC m) + n = SUC(m + n)) /\
   (m + (SUC n) = SUC(m + n))
rewrite_list =
[|- (0 + m = m) /\
    (m + 0 = m) /\
    ((SUC m) + n = SUC(m + n)) /\
    (m + (SUC n) = SUC(m + n));
 |- !m n.
     (0 * m = 0) /\
     (m * 0 = 0) /\
     (1 * m = m) /\
     (m * 1 = m) /\
     ((SUC m) * n = (m * n) + n) /\
     (m * (SUC n) = m + (m * n))]
: thm list

15

#REWRITE_RULE rewrite_list (ASSUME "(m+0)<(1*n)+(SUC 0)");;
(m + 0) < ((1 * n) + (SUC 0)) |- m < (SUC n)

This can then be rewritten using a pre-proved theorem LESS_THM:

16

REWRITE_RULE [LESS_THM] it;;
Theorem LESS_THM autoloaded from theory `prim_rec`.
LESS_THM = |- !m n. m < (SUC n) = (m = n) \/ m < n
(m + 0) < ((1 * n) + (SUC 0)) |- (m = n) \/ m < n

REWRITE_RULE is not a primitive in HOL, but is a derived rule. It is inherited from Cambridge LCF and was implemented by Larry Paulson (see his paper [9] for details). In addition to the supplied equations, REWRITE_RULE has some built in standard simplifications:

17

#REWRITE_RULE [] (ASSUME "(T /\ x) \/ F ==> F");;
T /\ x \/ F ==> F |- ~x

The complete list of these built-in rewrites is held in the ML variable basic_rewrites:

18

#basic_rewrites;;
[|- !x. (x = x) = T;
|- !t.
((T = t) = t) /\ ((t = T) = t) /\ ((F = t) = ~t) /\ ((t = F) = ~t);
|- (!t. ~~t = t) /\ (~T = F) /\ (~F = T);
|- !t.
(T /\ t = t) /\
(t /\ T = t) /\
(F /\ t = F) /\
(t /\ F = F) /\
(t /\ t = t);
|- !t.
(T \/ t = T) /\
(t \/ T = T) /\
(F \/ t = t) /\
(t \/ F = t) /\
(t \/ t = t);
|- !t.
(T ==> t = t) /\
(t ==> T = T) /\
(F ==> t = T) /\
(t ==> t = T) /\
(t ==> F = ~t);
|- !t1 t2. ((T => t1 | t2) = t1) /\ ((F => t1 | t2) = t2);
|- !t1 t2. t1 <=> t2 = (t1 = t2);
|- !t. (!x. t) = t;
|- !t. (?x. t) = t;
|- !t1 t2. (\x. t1)t2 = t1;
|- !x. FST x,SND x = x;
|- !x y. FST(x,y) = x;
|- !x y. SND(x,y) = y]
: thm list

There are elaborate facilities in HOL for producing customized rewriting tools which scan through terms in user programmed orders; REWRITE_RULE is the tip of an iceberg, see DESCRIP-TION for more details.

4.3 Tautologies

ICL Defence Systems have supplied a tautology checker as a library program. This takes any term "t" and returns |- t if t is an instance of a tautology of the propositional calculus. This checker is a derived rule and constructs (behind the scenes) a proof of any tautology. It is in the library taut which is loaded with the function load_library.

19

#load_library `taut`;;
Loading library `taut` ...
evaluation failed     load -- foo/Library/taut/taut ml file not found

4.3. Tautologies 35

This error message shows that HOL has not been installed properly; see Chapter 1. The hol being used for this session is on the directory /tmp_mnt/home/flint/mjcg/hol, but:

20

#HOLdir;;
`wonk/foo/mumble` : string

which shows that HOL thinks it is living on wonk/foo/mumble. This is easy to fix:

21

#install `/tmp_mnt/home/flint/mjcg/hol`;;
() : void
HOLdir = `/tmp_mnt/home/flint/mjcg/hol` : string

Now the library taut will load properly.

22

#load_library `taut`;;
Loading library `taut` ...
[fasl /tmp_mnt/home/flint/mjcg/hol/Library/taut/taut_ml.o]
.......................
Library `taut` loaded.
() : void

The following session illustrates TAUT_RULE, which is one of the functions loaded when the library taut is loaded.

23

#TAUT_RULE "((A ==> B) ==> A) ==> A";;
|- ((A ==> B) ==> A) ==> A
#TAUT_RULE "((A ==> B) ==> A) ==> B";;
evaluation failed     TAC_PROOF -- TAUT_TAC - term not a tautology

TAUT_RULE has ML type term -> thm which is abbreviated to conv by ML (the motivation for this name is discussed in the section on conversions in DESCRIPTION).

24

#TAUT_RULE;;
- : conv

Such type abbreviations are discussed in the next chapter.

36 Chapter 4. Introduction to Proof with HOL

Goal Oriented Proof: Tactics and Tacticals

The style of forward proof described in the previous chapter is unnatural and too ‘low level’ for many applications. An important advance in proof generating methodology was made by Robin Milner in the early 1970s when he invented the notion of tactics. A tactic is a function that does two things.

(i) Splits a ‘goal’ into ‘subgoals’.

(ii) Keeps track of the reason why solving the subgoals will solve the goal.

Consider, for example, the rule of ∧-introduction^{1} shown below:

\frac{Γ_{1} ⊢ t_{1} Γ_{2} ⊢ t_{2}}{Γ_{1} ∪ Γ_{2} ⊢ t_{1} ∧ t_{2}}

In HOL, ∧-introduction is represented by the ML function CONJ:

CONJ (Γ_{1} ⊢ t_{1}) (Γ_{2} ⊢ t_{2}) ⇝ (Γ_{1} ∪ Γ_{2} ⊢ t_{1} ∧ t_{2})

This is illustrated in the following new session (note that the session number has been reset to 1):

1

 #top_print print_all_thm;;
 - : (thm -> void)
 #let Th1 = ASSUME "A:bool" and Th2 = ASSUME "B:bool";;
 Th1 = A |- A
 Th2 = B |- B
 #let Th3 = CONJ Th1 Th2;;
 Th3 = A, B |- A /\ B

Suppose the goal is to prove A ∧ B, then this rule says that it is sufficient to prove the two subgoals A and B, because from ⊢ A and ⊢ B the theorem ⊢ A ∧ B can be deduced. Thus:

(i) To prove ⊢ A ∧ B it is sufficient to prove ⊢ A and ⊢ B.

1In higher order logic this is a derived rule; in first order logic it is usually primitive. In HOL the rule is called CONJ and its derivation is given in DESCRIPTION.

38 Chapter 5. Goal Oriented Proof: Tactics and Tacticals

(ii) The justification for the reduction of the goal ⊢ A ∧ B to the two subgoals ⊢ A and ⊢ B is the rule of ∧-introduction.

A goal in HOL is a pair ([t_{1};...;t_{n}],t) of ML type term list # term. An achievement of such a goal is a theorem t_{1},…,t_{n} |- t. A tactic is an ML function that when applied to a goal generates subgoals together with a justification function or validation, which will be an ML derived inference rule, that can be used to infer an achievement of the original goal from achievements of the subgoals.

Aside: ML has a type abbreviating mechanism which is used to give mnemonic names to the various types associated with goal oriented proof. Type abbreviations can be seen by evaluating

print_defined_types():

2

 #print_defined_types();;
   proof = (thm list -> thm)
   goal = (term list # term)
   tactic = ((term list # term) -> subgoals)
   thm_tactic = (thm -> tactic)
   thm_tactical = ((thm -> tactic) -> thm_tactic)
   conv = (term -> thm)
   term_net -- an abstract type
   subgoals = ((term list # term) list # proof)
   goalstack -- an abstract type

The left hand side of these abbreviations can be used anywhere that the right hand side can (abstract types are explained elsewhere). The default is that the printer will print out abbreviations at top-level, but this behaviour can be changed (see the flag print_lettypes in DESCRIPTION). End aside.

If T is a tactic (i.e. an ML function of type tactic) and g is a goal (i.e. an ML function of type goal), then applying T to g (i.e. evaluating the ML expression T g) will result in an object of ML type subgoals, i.e. a pair whose first component is a list of goals and whose second component is a justification function, i.e. has ML type proof.

An example tactic is CONJ_TAC which implements (i) and (ii) above. For example, consider the utterly trivial goal of showing T /\ T, where T is a constant that stands for true:

3

 #let goal1 =([], "T /\ T");;
 goal1 = ([], "T /\ T") : (* list # term)
 #CONJ_TAC goal1;;
 ([([], "T"); ([], "T")], -) : subgoals
 #let goal_list,just_fn = it;;
 goal_list = [([], "T"); ([], "T")] : goal list
 just_fn = - : proof

CONJ_TAC has produced a goal list consisting of two identical subgoals of just showing ([],"T"). Now, there is a preproved theorem in HOL, called TRUTH, that achieves this goal:

 4 #TRUTH;; |- T

\underline{39}

Applying the justification function just_fn to a list of theorems achieving the goals in goal_list results in a theorem achieving the original goal:

5

 #just_fn [TRUTH;TRUTH];;
 |- T /\ T

Although this example is trivial, it does illustrate the essential idea of tactics. Note that tactics are not special theorem-proving primitives; they are just ML functions. For example, the definition of CONJ_TAC is simply:

    let CONJ_TAC (asl,w) =
     let l,r = dest_conj w
     in
     ([(asl,l); (asl,r)], \[th1;th2]. CONJ th1 th2)

The ML function dest_conj splits a conjunction into its two conjuncts: If (asl,"t_{1}/\t_{2}") is a goal, then CONJ_TAC splits it into the list of two subgoals (asl,t_{1}) and (asl,t_{2}). The justification function, \[th1;th2]. CONJ th1 th2 takes a list [th_{1};th_{2}] of theorems and applies the rule CONJ to th_{1} and th_{2}.

To summarize: if T is a tactic and g is a goal, then applying T to g will result in an object of ML type subgoals, i.e. a pair whose first component is a list of goals and whose second component is a justification function, i.e. has ML type proof.

Suppose T g = ([g_{1};…;g_{n}],p). The idea is that g_{1} , …, g_{n} are subgoals and p is a ‘justification’ of the reduction of goal g to subgoals g_{1} , …, g_{n}. Suppose further that the subgoals g_{1} , …, g_{n} have been solved. This would mean that theorems th_{1} , …, th_{n} had been proved such that each th_{i} (1 ≤ i ≤ n) ‘achieves’ the goal g_{i}. The justification p (produced by applying T to g) is an ML function which when applied to the list [th_{1};…;th_{n}] returns a theorem, th, which ‘achieves’ the original goal g. Thus p is a function for converting a solution of the subgoals to a solution of the original goal. If p does this successfully, then the tactic T is called valid. Invalid tactics cannot result in the proof of invalid theorems; the worst they can do is result in insolvable goals or unintended theorems being proved. If T were invalid and were used to reduce goal g to subgoals g_{1} , …, g_{n}, then effort might be spent proving theorems th_{1} , …, th_{n} to achieve the subgoals g_{1} , …, g_{n}, only to find out after the work is done that this is a blind alley because p[th_{1};…;th_{n}] doesn’t achieve g (i.e. it fails, or else it achieves some other goal).

A theorem achieves a goal if the assumptions of the theorem are included in the assumptions of the goal and if the conclusion of the theorems is equal (up to the renaming of bound variables) to the conclusion of the goal. More precisely, a theorem

t_{1}, …, t_{m} |- t

achieves a goal

([u_{1};…;u_{n}],u)

if and only if {t_{1}, …, t_{m}} is a subset of {u_{1}, …, u_{n}} and t is equal to u (up to renaming of bound variables). For example, the goal (["x=y";"y=z";"z=w"],"x=z") is achieved by the theorem x=y, y=z |- x=z (the assumption "z=w" is not needed).

A tactic solves a goal if it reduces the goal to the empty list of subgoals. Thus T solves g if T g = ([],p). If this is the case and if T is valid, then p[] will evaluate to a theorem achieving g. Thus if T solves g then the ML expression snd(T g)[] evaluates to a theorem achieving g.

Tactics are specified using the following notation:

goal
goal_{1} goal_{2} ⋯ goal_{n}

For example, a tactic called CONJ_TAC is described by

\begin{matrix}t_{1} /\ t_{2} \\ t_{1} t_{2} \end{matrix}

Thus CONJ_TAC reduces a goal of the form (Γ,"t_{1}/\t_{2}") to subgoals (Γ,"t_{1}") and (Γ,"t_{2}"). The fact that the assumptions of the top-level goal are propagated unchanged to the two subgoals is indicated by the absence of assumptions in the notation.

Another example is INDUCT_TAC, the tactic for doing mathematical induction on the natural numbers:

!n.t[n]
t[0] {t[n]} t[SUC n]

INDUCT_TAC reduces a goal (Γ,"!n.t[n]") to a basis subgoal (Γ,"t[0]") and an induction step subgoal (Γ ∪ {"t[n]"},"t[SUC n]"). The extra induction assumption "t[n]" is indicated in the tactic notation with set brackets.

6

 #INDUCT_TAC([], "!m n. m+n = n+m");;
 ([([], "!n. 0 + n = n + 0");
   (["!n. m + n = n + m"], "!n. (SUC m) + n = n + (SUC m)")],
  -)
 : subgoals

The first subgoal is the basis case and the second subgoal is the step case.

Tactics generally fail (in the ML sense) if they are applied to inappropriate goals. For example, CONJ_TAC will fail if it is applied to a goal whose conclusion is not a conjunction. Some tactics never fail, for example ALL_TAC

\begin{matrix}t \\ t \end{matrix}

is the ‘identity tactic’; it reduces a goal (Γ,t) to the single subgoal (Γ,t)—i.e. it has no effect. ALL_TAC is useful for writing complex tactics using tacticals (e.g. see the definition of REPEAT in Section 5.2).

5.1. Using tactics to prove theorems 41

5.1 Using tactics to prove theorems

Suppose goal g is to be solved. If g is simple it might be possible to immediately think up a tactic, T say, which reduces it to the empty list of subgoals. If this is the case then executing:

    let gl,p = T g

will bind p to a function which when applied to the empty list of theorems yields a theorem th achieving g. (The declaration above will also bind gl to the empty list of goals.) Thus a theorem achieving g can be computed by executing:

    let th = p[]

This will be illustrated using REWRITE_TAC which takes a list of equations (empty in the example that follows) and tries to prove a goal by rewriting with these equations together with

basic_rewrites:

7

 #let goal2 = ([], "T /\ x ==> x \/ (y /\ F)");;
 goal2 = ([], "T /\ x ==> x \/ y /\ F") : (* list # term)
 #REWRITE_TAC [] goal2;;
 ([], -) : subgoals
 #snd it [];;
 |- T /\ x ==> x \/ y /\ F

Proved theorems are usually stored in the current theory so that they can be used in subsequent sessions.

The built-in function prove_thm of ML type (string # term # tactic) -> thm facilitates the use of tactics: prove_thm(`foo`,t,T) proves the goal ([],t) (i.e. the goal with no assumptions and conclusion t) using tactic T and saves the resulting theorem with name foo on the current theory.

If the theorem is not to be saved, the function prove of type (term # tactic) -> thm can be used. Evaluating prove(t,T) proves the goal ([],t) using T and returns the result without saving it. In both cases the evaluation fails if T does not solve the goal ([],t).

When conducting a proof that involves many subgoals and tactics, it is necessary to keep track of all the justification functions and compose them in the correct order. While this is feasible even in large proofs, it is tedious. HOL provides a package for building and traversing the tree of subgoals, stacking the justification functions and applying them properly; this package was originally implemented for LCF by Larry Paulson.

The subgoal package implements a simple framework for interactive proof. A proof tree is created and traversed top-down. The current goal can be expanded into subgoals using a tactic; the subgoals are pushed onto a goal stack and the justification function onto a proof stack. Subgoals can be considered in any order. If the tactic solves a subgoal (i.e. returns an empty subgoal list), then the package proceeds to the next subgoal in the tree.

The function set_goal of type goal -> void initializes the subgoal package with a new goal. Usually top-level goals have no assumptions; the function g is useful in this case and is defined by:

    let g t = set_goal([],t)

To illustrate the subgoal package the trivial theorem ⊢ ∀m. m + 0 = m will be proved from the definition of addition:

8

#ADD;;
Definition ADD autoloaded from theory `arithmetic`.
ADD = |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))
|- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n))

Notice that ADD specifies 0 + m = m but not m + 0 = m. Of course, ∀m n. m + n = n + m is true, but the first step of the proof is to show ∀m. m + 0 = m from the definition of addition.

1

#g "!m. m+0=m";;
"!m. m + 0 = m"
() : void

This sets up the goal. Next the goal is split into a basis and step case with INDUCT_TAC. To do this the function e (or, equivalently, expand) is used. This applies a tactic to the top goal on the stack, then pushes the resulting subgoals onto the goal stack, then prints the resulting subgoals. If there are no subgoals, the justification function is applied to the theorems solving the subgoals that have been proved and the resulting theorems are printed.

2

#e INDUCT_TAC;;
OK..
2 subgoals
"(SUC m) + 0 = SUC m"
    [ "m + 0 = m" ]
"0 + 0 = 0"

The top of the goal stack is printed last. The basis case is an instance of the definition of addition, so is solved by rewriting with ADD.

3

#e(REWRITE_TAC[ADD]);;
OK..
goal proved
|- 0 + 0 = 0
Previous subproof:
"(SUC m) + 0 = SUC m"
    [ "m + 0 = m" ]

The basis is solved and the goal stack popped so that its top is now the step case, namely showing that (SUC m) + 0 = SUC m under the assumption m + 0 = m. This goal can be solved by rewriting first with the definition of addition:

4

#e(REWRITE_TAC[ADD]);;
OK..
"SUC(m + 0) = SUC m"
    [ "m + 0 = m" ]

5.1. Using tactics to prove theorems 43

and then with the assumption m+0=m. The tactic ASM_REWRITE_TAC is used to rewrite with the assumptions of a goal. It is just like REWRITE_TAC except that it adds the assumptions to the list of equations used for rewriting. For the example here no equations besides the assumptions are needed, so ASM_REWRITE_TAC is given the empty list of equations.

5

#e(ASM_REWRITE_TAC[]);;
OK..
goal proved
. |- SUC(m + 0) = SUC m
. |- (SUC m) + 0 = SUC m
|- !m. m + 0 = m
Previous subproof:
goal proved

The top goal is solved, hence the preceding goal (the step case) is solved too, and since the basis is already solved, the main goal is solved.

The theorem achieving the goal can be extracted from the subgoal package with top_thm:

6

#top_thm();;
|- !m. m + 0 = m

The proof just done can be ‘optimized’. For example, instead of first rewriting with ADD (box 4) and then with the assumptions (box 5), a single rewriting with ADD and the assumptions would suffice. To illustrate, the last two steps of the proof will be ‘undone’ using the function backup which restores the previous state of the goal and theorem stacks.

7

#backup();;
"SUC(m + 0) = SUC m"
    [ "m + 0 = m" ]
() : void
#backup();;
"(SUC m) + 0 = SUC m"
    [ "m + 0 = m" ]

The proof can now be completed in one step instead of two:

8

#e(ASM_REWRITE_TAC[ADD]);;
OK..
goal proved
. |- (SUC m) + 0 = SUC m
|- !m. m + 0 = m
Previous subproof:
goal proved

The order in which goals are attacked can be adjusted using rotate n which rotates the goal stack by n. For example:

9

#backup();backup();;
"(SUC m) + 0 = SUC m"
    [ "m + 0 = m" ]
2 subgoals
"(SUC m) + 0 = SUC m"
    [ "m + 0 = m" ]
"0 + 0 = 0"
() : void
#rotate 1;;
2 subgoals
"0 + 0 = 0"
"(SUC m) + 0 = SUC m"
    [ "m + 0 = m" ]

The top goal is now the step case not the basis case, so expanding with a tactic will apply the tactic to the step case.

10

e(ASM_REWRITE_TAC[ADD]);;
OK..
goal proved
. |- (SUC m) + 0 = SUC m
Previous subproof:
"0 + 0 = 0"

It is possible to do the whole proof in one step, but this requires a compound tactic built using the tactical^{2} THENL. Tacticals are higher order operations for combining tactics.

5.2 Tacticals

A tactical is an ML function that returns a tactic (or tactics) as result. Tacticals may take various parameters; this is reflected in the various ML types that the built-in tacticals have. Some important tacticals in the HOL system are listed below.

5.2.1 THENL : tactic -> tactic list -> tactic

If tactic T produces n subgoals and T_{1}, …, T_{n} are tactics then T THENL[T_{1};…;T_{n}] is a tactic which first applies T and then applies T_{i} to the ith subgoal produced by T. The tactical THENL is useful if one wants to do different things to different subgoals.

THENL can be illustrated by doing the proof of ⊢ ∀m. m + 0 = m in one step.

2This word was invented by Robin Milner: ‘tactical’ is to ‘tactic‘ as ‘functional’ is to ‘function’.

5.2. Tacticals 45

1

#g "!m. m + 0 = m";;
"!m. m + 0 = m"
() : void
#e(INDUCT_TAC THENL [REWRITE_TAC[ADD];ASM_REWRITE_TAC[ADD]]);;
OK..
goal proved
|- !m. m + 0 = m
Previous subproof:
goal proved
() : void
The compound tactic INDUCT_TAC THENL [REWRITE_TAC[ADD];ASM_REWRITE_TAC[ADD]] first

applies INDUCT_TAC and then applies REWRITE_TAC[ADD] to the first subgoal (the basis) and ASM_REWRITE_TAC[ADD] to the second subgoal (the step).

The tactical THENL is useful for doing different things to different subgoals. The tactical THEN can be used to apply the same tactic to all subgoals.

5.2.2 THEN : tactic -> tactic -> tactic

The tactical THEN is an ML infix. If T_{1} and T_{2} are tactics, then the ML expression T_{1} THEN T_{2} evaluates to a tactic which first applies T_{1} and then applies T_{2} to all the subgoals produced by T_{1}.

In fact, ASM_REWRITE_TAC[ADD] will solve the basis as well as the step case of the induction for ∀m. m + 0 = m, so there is an even simpler one-step proof than the one above:

1

#g "!m. m+0 = m";;
"!m. m + 0 = m"
() : void
#e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);;
OK..
goal proved
|- !m. m + 0 = m
Previous subproof:
goal proved

This is typical: it is common to use a single tactic for several goals. Here, for example, are the first four consequences of the definition ADD of addition that are pre-proved when the built-in theory arithmetic HOL is made.

   let ADD_0 =
    prove
     ("!m. m + 0 = m",
      INDUCT_TAC
       THEN ASM_REWRITE_TAC[ADD]);;

    let ADD_SUC =
     prove
      ("!m n. SUC(m + n) = m + SUC n",
       INDUCT_TAC
        THEN ASM_REWRITE_TAC[ADD]);;

    let ADD_CLAUSES =
     prove
      ("(0 + m = m)              /\
        (m + 0 = m)              /\
        (SUC m + n = SUC(m + n)) /\
        (m + SUC n = SUC(m + n))",
       REWRITE_TAC[ADD;ADD_0;ADD_SUC]);;

    let ADD_SYM =
     prove
     ("!m n. m + n = n + m",
      INDUCT_TAC
       THEN ASM_REWRITE_TAC[ADD_0;ADD;ADD_SUC]);;

These proofs are performed when the HOL system is made and the theorems are saved in the theory arithmetic. The complete list of proofs for this built-in theory can be found in the file

theories/mk_arith_thms.ml.

5.2.3 ORELSE : tactic -> tactic -> tactic

The tactical ORELSE is an ML infix. If T_{1} and T_{2} are tactics, then T_{1} ORELSE T_{2} evaluates to a tactic which applies T_{1} unless that fails; if it fails, it applies T_{2}. ORELSE is defined in ML as a curried infix by

(T_{1} ORELSE T_{2}) g = T_{1}g ? T_{2}g

5.2.4 REPEAT : tactic -> tactic

If T is a tactic then REPEAT T is a tactic which repeatedly applies T until it fails. This can be illustrated in conjunction with GEN_TAC, which is specified by:

\begin{matrix}!x.t[x] \\ t[x′] \end{matrix}

• Where x′ is a variant of x not free in the goal or the assumptions.

GEN_TAC strips off one quantifier; REPEAT GEN_TAC strips off all quantifiers:

5.3. Some tactics built into HOL 47

2

#g "!x y z. x+(y+z) = (x+y)+z";;
"!x y z. x + (y + z) = (x + y) + z"
() : void
#e GEN_TAC;;
OK..
"!y z. x + (y + z) = (x + y) + z"
() : void
#e(REPEAT GEN_TAC);;
OK..
"x + (y + z) = (x + y) + z"

5.3 Some tactics built into HOL

This section contains a summary of some of the tactics built into the HOL system (including those already discussed). The tactics given here are those that are used in the parity checking case study.

Recall that the ML type thm_tactic abbreviates theorem->tactic, and the type conv^{3} abbreviates term->thm.

5.3.1 REWRITE TAC : thm list -> tactic

• Summary: REWRITE_TAC[th_{1};…;th_{n}] simplifies the goal by rewriting it with the explicitly given theorems th_{1}, …, th_{n}, and various built-in rewriting rules.

{t_{1}, …, t_{m}}t
{t_{1}, …, t_{m}}t′

where t′ is obtained from t by rewriting with

1. th_{1}, …, th_{n} and

2. the standard rewrites held in the ML variable basic_rewrites.

• Uses: Simplifying goals using previously proved theorems.

• Other rewriting tactics (based on REWRITE_TAC):

1. ASM_REWRITE_TAC adds the assumptions of the goal to the list of theorems used for rewriting.

2. FILTER_ASM_REWRITE_TAC p [th_{1};…;th_{n}] simplifies the goal by rewriting it with the explicitly given theorems th_{1} , …, th_{n} , together with those assumptions of the goal which satisfy the predicate p and also the built-in rewrites in the ML variable

         basic_rewrites.

3The type conv comes from Larry Paulson’s theory of conversions [9].

    3. PURE_ASM_REWRITE_TAC is like ASM_REWRITE_TAC, but it doesn’t use any built-in

rewrites.

4. PURE_REWRITE_TAC uses neither the assumptions nor the built-in rewrites.

5.3.2 CONJ TAC : tactic

• Summary: Splits a goal "t_{1}/\t_{2}" into two subgoals "t_{1}" and "t_{2}".

\begin{matrix}t_{1} /\ t_{2} \\ t_{1} t_{2} \end{matrix}

• Uses: Solving conjunctive goals. CONJ_TAC is invoked by STRIP_TAC (see below).

5.3.3 EQ TAC : tactic

• Summary: EQ_TAC splits an equational goal into two implications (the ‘if-case’ and the ‘only-if’ case):

u = v

                               u ==> v v ==> u

• Use: Proving logical equivalences, i.e. goals of the form “u=v” where u and v are boolean terms.

5.3.4 DISCH TAC : tactic

• Summary: Moves the antecedent of an implicative goal into the assumptions.

\begin{matrix}u ==> v \\ \{u\}v \end{matrix}

• Uses: Solving goals of the form "u ==> v" by assuming "u" and then solving "v". STRIP_TAC (see below) will invoke DISCH_TAC on implicative goals.

5.3.5 GEN TAC : tactic

• Summary: Strips off one universal quantifier.

\begin{matrix}!x.t[x] \\ t[x′] \end{matrix}

Where x′ is a variant of x not free in the goal or the assumptions.

• Uses: Solving universally quantified goals. REPEAT GEN_TAC strips off all universal quantifiers and is often the first thing one does in a proof. STRIP_TAC (see below) applies GEN_TAC to universally quantified goals.

5.3. Some tactics built into HOL 49

5.3.6 IMP RES TAC : tactic

• Summary: IMP_RES_TAC th does a limited amount of automated theorem proving in the form of forward inference; it ‘resolves’ the theorem th with the assumptions of the goal and adds any new results to the assumptions. The specification for IMP_RES_TAC is:

{t_{1}, …, t_{m}}t
{t_{1}, …, t_{m}, u_{1}, …, u_{n}}t

where u_{1}, …, u_{n} are derived by ‘resolving’ the theorem th with the existing assumptions t_{1}, …, t_{m}. Resolution in HOL is not classical resolution, but just Modus Ponens with one-way pattern matching (not unification) and term and type instantiation. The general case is where th is of the canonical form

|- !x_{1}… x_{p}.v_{1} ==> v_{2} ==> … ==> v_{q} ==> v

IMP_RES_TAC th then tries to specialize x_{1}, …, x_{p} in succession so that v_{1}, …, v_{q} match members of {t_{1}, …, t_{m}}. Each time a match is found for some antecedent v_{i}, for i successively equal to 1, 2, …, q, a term and type instantiation is made and the rule of Modus Ponens is applied. If all the antecedents v_{i} (for 1 ≤ i ≤ q) can be dismissed in this way, then the appropriate instance of v is added to the assumptions. Otherwise, if only some initial sequence v_{1}, …, v_{k} (for some k where 1 < k < q) of the assumptions can be dismissed, then the remaining implication:

  |- v_{k+1} ==> . . . ==> v_{q} ==> v

is added to the assumptions.

For a more detailed description of resolution and IMP_RES_TAC, see DESCRIPTION and

REFERENCE.

• Uses: Deriving new results from a previously proved implicative theorem, in combination with the current assumptions, so that subsequent tactics can use these new results.

5.3.7 STRIP TAC : tactic

• Summary: Breaks a goal apart. STRIP_TAC removes one outer connective from the goal,

using CONJ_TAC, DISCH_TAC, GEN_TAC, etc. If the goal is t_{1}/\· · ·/\t_{n} ==> t then DISCH_TAC

makes each t_{i} into a separate assumption.

• Uses: Useful for splitting a goal up into manageable pieces. Often the best thing to do

first is REPEAT STRIP_TAC.

5.3.8 SUBST TAC : thm list -> thm

• Summary: SUBST_TAC[|-u_{1}=v_{1};…;|-u_{n}=v_{n}] converts a goal t[u_{1}, …, u_{n}] to the subgoal form t[v_{1}, …, v_{n}].

• Uses: To make replacements for terms in situations in which REWRITE_TAC is too general or would loop.

5.3.9 ACCEPT TAC : thm -> tactic

• Summary: ACCEPT_TAC th is a tactic that solves any goal that is achieved by th.

• Use: Incorporating forward proofs, or theorems already proved, into goal directed proofs. For example, one might reduce a goal g to subgoals g_{1}, …, g_{n} using a tactic T and then prove theorems th_{1} , …, th_{n} respectively achieving these goals by forward proof. The tactic

    T THENL[ACCEPT_TAC th_{1}; . . .;ACCEPT_TAC th_{n}]

would then solve g, where THENL is the tactical that applies the respective elements of the tactic list to the subgoals produced by T.

5.3.10 ALL TAC : tactic

• Summary: Identity tactic for the tactical THEN (see DESCRIPTION).

• Uses:

1. Writing tacticals (see description of REPEAT in DESCRIPTION).

2. With THENL; for example, if tactic T produces two subgoals and we want to apply T_{1} to the first one but to do nothing to the second, then the tactic to use is

      T THENL[T_{1};ALL_TAC].
5.3.11 NO TAC : tactic

• Summary: Tactic that always fails.

• Uses: Writing tacticals.

Example: a simple parity checker

This chapter consists of a worked example: the specification and verification of a simple sequential parity checker. The intention is to accomplish two things:

(i) To present a complete piece of work with HOL.

(ii) To give a flavour of what it is like to use the HOL system for a tricky proof.

Concerning (ii), note that although the theorems proved are, in fact, rather simple, the way they are proved illustrates the kind of intricate ‘proof engineering’ that is typical. The proofs could be done more elegantly, but presenting them that way would defeat the purpose of illustrating various features of HOL. It is hoped that the small example here will give the reader a feel for what it is like to do a big one.

Readers who are not interested in hardware verification should be able to learn something about the HOL system even if they do not wish to penetrate the details of the parity-checking example used here. The specification and verification of a slightly more complex parity checker is set as an exercise (a solution is provided).

6.1 Introduction

This case study is supported by three files in the HOL distribution directory. These files are:

    hol/Training/parity/PARITY.ml
    hol/Training/parity/RESET_REG.ml
    hol/Training/parity/RESET_PARITY.ml

The file PARITY.ml contains the HOL sessions in this chapter; the files RESET_REG.ml and RESET_PARITY.ml contain the solutions to the exercises described in Section 6.5.

The goal of the case study is to illustrate detailed ‘proof hacking’ on a small and fairly simple example.

The boxes below contain a little session with the HOL system. The interactions in these boxes should be understood as occurring in sequence. For example, variable bindings made in earlier boxes are assumed to persist to later ones. These interactions comprise the specification and verification of a device that computes the parity of a sequence of bits. More specifically, a detailed verification is given of a device with an input in, an output out and the specification that the nth output on out is T if and only if there have been an even number of T’s input on in. A theory named PARITY is constructed; this contains the specification and verification of the device. All the ML input in the boxes below can be found in the file parity/PARITY.ml. It is suggested that the reader interactively input this to get a ‘hands on’ feel for the example.

52 Chapter 6. Example: a simple parity checker

6.2 Specification

The first step is to start up the HOL system and then enter draft mode for a new theory called PARITY. The HOL system is entered by typing hol to Unix.^{1} The HOL system then prints a sign-on message and puts the user into ML. The ML prompt is #, so lines beginning with # are typed by the user and other lines are the system’s response.

1

 gwyndir% hol
        _________
 |___|__|   |  |   |     |__|  |__|
 |      |  |   |__|   |__|__|  |__|
           Version 2.0 (Sun3/Franz), built on Sep 1 1991
 #new_theory`PARITY`;;
 () : void

To specify the device, a primitive recursive function PARITY is defined so that for n > 0, PARITY nf is true if the number of T’s in the sequence f(1), …, f(n) is even.

2

 #let PARITY_DEF =
 # new_prim_rec_definition
 #  (`PARITY_DEF`,
 #   "(PARITY 0 f = T) /\
 #    (PARITY(SUC n)f = (f(SUC n) => ~(PARITY n f) | PARITY n f))");;
 PARITY_DEF =
 |- (!f. PARITY 0 f = T) /\
    (!n f. PARITY(SUC n)f = (f(SUC n) => ~PARITY n f | PARITY n f))

The effect of new_prim_rec_definition is to store the definition of PARITY on the current theory with name PARITY_DEF and to bind the defining theorem to the ML variable with the same name. Notice that there are two name spaces being written into: the names of constants in theories and the names of variables in ML. The user is free to manage these names however he or she wishes (subject to the various lexical requirements), but a common convention is (as here) to give the definition of a constant CON the name CON_DEF in the theory and also in ML. Another commonly-used convention is to use just CON for the theory and ML name of the definition of a constant CON. Unfortunately, the HOL system does not use a uniform convention, but users are recommended to adopt one.

The specification of the parity checking device can now be given as:

   !t. out t = PARITY t in

It is intuitively clear that this specification will be satisfied if the signal^{2} functions in and out satisfy:

1The Unix prompt on the author’s machine is gwyndir%.

2Signals are modelled as functions from numbers, representing times, to booleans.

6.2. Specification 53

   out(0) = T

and

   !t. out(t+1)  =  (in(t+1) => ~(out t) | out t)

This can be verified formally in HOL by proving the following lemma:

   !in out.
    (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~(out t) | out t))
    ==>
    (!t. out t = PARITY t in)

The proof of this is done by Mathematical Induction and, although trivial, is a good illustration of how such proofs are done. The lemma is proved interactively using HOL’s subgoal package. The proof is started by putting the goal to be proved on a goal stack using the function set_goal which takes a goal as argument.

3

 #set_goal
 #([],
 # "!in out.
 #   (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~(out t) | out t))
 #   ==>
 #   (!t. out t = PARITY t in)");;
 "!in out.
   (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t)) ==>
   (!t. out t = PARITY t in)"

The subgoal package prints out the goal on the top of the goal stack. The top goal is expanded by stripping off the universal quantifier (with GEN_TAC) and then making the two conjuncts of the antecedent of the implication into assumptions of the goal (with STRIP_TAC). The ML function expand takes a tactic and applies it to the top goal; the resulting subgoals are pushed on to the goal stack. The message ‘OK..’ is printed out just before the tactic is applied. The resulting subgoal is then printed.

4

 #expand(REPEAT GEN_TAC THEN STRIP_TAC);;
 OK..
 "!t. out t = PARITY t in"
     [ "out 0 = T" ]
     [ "!t. out(SUC t) = (in(SUC t) => ~out t | out t)" ]

Next induction on t is done using INDUCT_TAC, which does induction on the outermost universally quantified variable.

5

#expand INDUCT_TAC;;
OK..
2 subgoals
"out(SUC t) = PARITY(SUC t)in"
    [ "out 0 = T" ]
    [ "!t. out(SUC t) = (in(SUC t) => ~out t | out t)" ]
    [ "out t = PARITY t in" ]
"out 0 = PARITY 0 in"
    [ "out 0 = T" ]
    [ "!t. out(SUC t) = (in(SUC t) => ~out t | out t)" ]

The assumptions of the two subgoals are shown in square brackets. The last goal printed is the one on the top of the stack, which is the basis case. This is solved by rewriting with its assumptions and the definition of PARITY.

6

#expand(ASM_REWRITE_TAC[PARITY_DEF]);;
OK..
goal proved
. |- out 0 = PARITY 0 in
Previous subproof:
"out(SUC t) = PARITY(SUC t)in"
    [ "out 0 = T" ]
    [ "!t. out(SUC t) = (in(SUC t) => ~out t | out t)" ]
    [ "out t = PARITY t in" ]

The top goal is proved, so the system pops it from the goal stack (and puts the proved theorem on a stack of theorems). The new top goal is the step case of the induction. This goal is also solved by rewriting.

7

#expand(ASM_REWRITE_TAC[PARITY_DEF]);;
OK..
goal proved
.. |- out(SUC t) = PARITY(SUC t)in
.. |- !t. out t = PARITY t in
|- !in out.
    (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t)) ==>
    (!t. out t = PARITY t in)
Previous subproof:
goal proved

The goal is proved, i.e. the empty list of subgoals is produced. The system now applies the justification functions produced by the tactics to the lists of theorems achieving the subgoals (starting with the empty list). These theorems are printed out in the order in which they are generated (note that assumptions of theorems are printed as dots).

The ML function

  save_top_thm : string -> thm

6.3. Implementation 55

saves the theorem just proved (i.e. on the top of the theorem stack) in the current theory with a given name.

8

 #let UNIQUENESS_LEMMA = save_top_thm `UNIQUENESS_LEMMA`;;
 UNIQUENESS_LEMMA =
 |- !in out.
     (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t)) ==>
     (!t. out t = PARITY t in)

this saves the theorem in the theory PARITY with name UNIQUENESS_LEMMA and also binds it to an ML variable with the same name.

6.3 Implementation

The lemma just proved suggests that the parity checker can be implemented by holding the parity value in a register and then complementing the contents of the register whenever T is input. To make the implementation more interesting, it will be assumed that registers ‘power up’ storing F. Thus the output at time 0 cannot be taken directly from a register, because the output of the parity checker at time 0 is specified to be T. Another tricky thing to notice is that if t>0, then the output of the parity checker at time t is a function of the input at time t. Thus there must be a combinational path from the input to the output.

The schematic diagram below shows the design of a device that is intended to implement this specification. (The leftmost input to MUX is the selector.) This works by storing the parity of the sequence input so far in the lower of the two registers. Each time T is input at in, this stored value is complemented. Registers are assumed to ‘power up’ in a state in which they are storing F. The second register (connected to ONE) initially outputs F and then outputs T forever. Its role is just to ensure that the device works during the first cycle by connecting the output out to the device ONE via the lower multiplexer. For all subsequent cycles out is connected to l3 and so either carries the stored parity value (if the current input is F) or the complement of this value (if the current input is T).

                            NOT MUX ONE REG            MUX REG in out     l1        l2 l3   l4 l5  • • •

The devices making up this schematic will be modelled with predicates [4]. For example, the predicate ONE is true of a signal out if for all times t the value of out is T.

9

 #let ONE_DEF =
 # new_definition
 #  (`ONE_DEF`, "ONE(out:num->bool) = !t. out t = T");;
 ONE_DEF = |- !out. ONE out = (!t. out t = T)

Note that, as discussed above, ‘ONE_DEF’ is used both as an ML variable and as the name of the definition in the theory PARITY. Note also how ‘:num->bool’ has been added to resolve type ambiguities; without this (or some other type information) the typechecker would not be able to infer that t is to have type num.

The binary predicate NOT is true of a pair of signals (in,out) if the value of out is always the negation of the value of in. Inverters are thus modelled as having no delay. This is appropriate for a register-transfer level model, but not at a lower level.

6.3. Implementation 57

10

#let NOT_DEF =
# new_definition
#  (`NOT_DEF`, "NOT(in,out:num->bool) = !t. out t = ~(in t)");;
NOT_DEF = |- !in out. NOT(in,out) = (!t. out t = ~in t)

The final combinational device needed is a multiplexer. This is a ‘hardware conditional’; the input sw selects which of the other two inputs are to be connected to the output out.

11

#let MUX_DEF =
# new_definition
#  (`MUX_DEF`,
#   "MUX(sw,in1,in2,out:num->bool) =
#     !t. out t = (sw t => in1 t | in2 t)");;
MUX_DEF =
|- !sw in1 in2 out.
    MUX(sw,in1,in2,out) = (!t. out t = (sw t => in1 t | in2 t))

The remaining devices in the schematic are registers. These are unit-delay elements; the values output at time t+1 are the values input at the preceding time t, except at time 0 when the register outputs F.^{3}

12

#let REG_DEF =
# new_definition
# (`REG_DEF`, "REG(in,out:num->bool) =
#              !t. out t = ((t=0) => F | in(t-1))");;
REG_DEF =
|- !in out. REG(in,out) = (!t. out t = ((t = 0) => F | in(t - 1)))

The schematic diagram above can be represented as a predicate by conjoining the relations holding between the various signals and then existentially quantifying the internal lines. This technique is explained elsewhere (e.g. see [3, 4]).

13

#let PARITY_IMP_DEF =
# new_definition
#  (`PARITY_IMP_DEF`,
#   "PARITY_IMP(in,out) =
#    ?l1 l2 l3 l4 l5.
#     NOT(l2,l1) /\ MUX(in,l1,l2,l3) /\ REG(out,l2) /\
#     ONE l4     /\ REG(l4,l5)       /\ MUX(l5,l3,l4,out)");;
PARITY_IMP_DEF =
|- !in out.
    PARITY_IMP(in,out) =
    (?l1 l2 l3 l4 l5.
      NOT(l2,l1) /\
      MUX(in,l1,l2,l3) /\
      REG(out,l2) /\
      ONE l4 /\
      REG(l4,l5) /\
      MUX(l5,l3,l4,out))

3Time 0 represents when the device is switched on.

6.4 Verification

The following theorem will eventually be proved:

  |- !in out. PARITY_IMP(in,out) ==> (!t. out t = PARITY t in)

This states that if in and out are related as in the schematic diagram (i.e. as in the definition of PARITY_IMP), then the pair of signals (in,out) satisfies the specification.

First, the following lemma is proved; the correctness of the parity checker follows from this and UNIQUENESS_LEMMA by the transitivity of ==>.

14

#set_goal
# ([], "!in out.
#         PARITY_IMP(in,out) ==>
#         (out 0 = T) /\
#         !t. out(SUC t) = (in(SUC t) => ~(out t) | out t)");;
"!in out.
  PARITY_IMP(in,out) ==>
  (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t))"

The first step in proving this goal is to rewrite with definitions followed by a decomposition of the resulting goal using STRIP_TAC. The rewriting tactic PURE_REWRITE_TAC is used; this does no built-in simplifications, only the ones explicitly given in the list of theorems supplied as an argument. One of the built-in simplifications used by REWRITE_TAC is |- (x = T) = x. PURE_REWRITE_TAC is used to prevent rewriting with this being done.

15

#expand(PURE_REWRITE_TAC
#        [PARITY_IMP_DEF;ONE_DEF;NOT_DEF;MUX_DEF;REG_DEF]
#        THEN REPEAT STRIP_TAC);;
OK..
2 subgoals
"out(SUC t) = (in(SUC t) => ~out t | out t)"
    [ "!t. l1 t = ~l2 t" ]
    [ "!t. l3 t = (in t => l1 t | l2 t)" ]
    [ "!t. l2 t = ((t = 0) => F | out(t - 1))" ]
    [ "!t. l4 t = T" ]
    [ "!t. l5 t = ((t = 0) => F | l4(t - 1))" ]
    [ "!t. out t = (l5 t => l3 t | l4 t)" ]
"out 0 = T"
    [ "!t. l1 t = ~l2 t" ]
    [ "!t. l3 t = (in t => l1 t | l2 t)" ]
    [ "!t. l2 t = ((t = 0) => F | out(t - 1))" ]
    [ "!t. l4 t = T" ]
    [ "!t. l5 t = ((t = 0) => F | l4(t - 1))" ]
    [ "!t. out t = (l5 t => l3 t | l4 t)" ]

The top goal is the one printed last; its conclusion is out 0 = T and its assumptions are equations relating the values on the lines in the circuit. The natural next step is to expand the top goal by rewriting with the assumptions. However, if this is done the system will go into

6.4. Verification 59

an infinite loop because the equations for out, l2 and l3 are mutually recursive. To prevent looping, rewriting must be done with a non-looping subset of the assumptions.

To enable the assumptions corresponding to particular lines to be selected for rewriting, an ML function lines is defined such that lines `l_{1} … l_{n}` t is true whenever t has the form "!t. l_{i} t = ⋯ " for some l_{i} in the set specified by the string `l_{1} … l_{n}`. The functions words and rator used below are predeclared in ML.

16

 #let lines tok t =
 # (let x = fst(dest_var(rator(lhs(snd(dest_forall t)))))
 #  in
 #  mem x (words tok)) ? false;;
 lines = - : (string -> term -> bool)
FILTER_ASM_REWRITE_TAC(lines`out l4 l5`)[] is a tactic which rewrites with only those

assumptions that involve out, l4 and l5.

17

 #expand(FILTER_ASM_REWRITE_TAC(lines`out l4 l5`)[]);;
 OK..
 goal proved
 ... |- out 0 = T
 Previous subproof:
 "out(SUC t) = (in(SUC t) => ~out t | out t)"
     [ "!t. l1 t = ~l2 t" ]
     [ "!t. l3 t = (in t => l1 t | l2 t)" ]
     [ "!t. l2 t = ((t = 0) => F | out(t - 1))" ]
     [ "!t. l4 t = T" ]
     [ "!t. l5 t = ((t = 0) => F | l4(t - 1))" ]
     [ "!t. out t = (l5 t => l3 t | l4 t)" ]

The first of the two subgoals is proved. Inspecting the remaining goal it can be seen that it will be solved if its left hand side, out(SUC t), is expanded using the assumption:

  !t. out t = (l5 t => l3 t | l4 t)

However, if this assumption is used for rewriting, then all the subterms of the form out t will also be expanded. To prevent this, the messy and ad hoc tactic shown below will be used.

   FIRST_ASSUM
    (\th. if lines`out`(concl th)
           then SUBST_TAC[SPEC "SUC t" th]
           else NO_TAC)

FIRST_ASSUM f is a built-in tactical that applies f in succession to the assumed assumptions of the goal; the tactic resulting from the first successful application is applied. The argument to FIRST_ASSUM used here is:

   (\th. if lines`out`(concl th)
          then SUBST_TAC[SPEC "SUC t" th]
          else NO_TAC)

which converts a theorem of the form:

    |- !t. out t = tm[t]

to a tactic that replaces occurrences of out(SUC t) by tm[SUC t]. All other theorems are mapped to NO_TAC, a tactic that always fails.

18

 #expand
 # (FIRST_ASSUM
 #   (\th. if lines`out`(concl th)
 #          then SUBST_TAC[SPEC "SUC t" th]
 #          else NO_TAC));;
 OK..
 "(l5(SUC t) => l3(SUC t) | l4(SUC t)) = (in(SUC t) => ~out t | out t)"
     [ "!t. l1 t = ~l2 t" ]
     [ "!t. l3 t = (in t => l1 t | l2 t)" ]
     [ "!t. l2 t = ((t = 0) => F | out(t - 1))" ]
     [ "!t. l4 t = T" ]
     [ "!t. l5 t = ((t = 0) => F | l4(t - 1))" ]
     [ "!t. out t = (l5 t => l3 t | l4 t)" ]

The fact that this messy use of FIRST_ASSUM was resorted to in the proof shown above illustrates both the strengths and weaknesses of HOL. Trivial deductions sometimes require elaborate tactics, but on the other hand one never reaches an impasse. HOL experts can prove arbitrarily complicated theorems if they are willing to use sufficient ingenuity. Furthermore, the type discipline ensures that no matter how complicated and ad hoc are the tactics, it is impossible to prove an invalid theorem.

Inspecting the goal above, it can be seen that the next step is to unwind the equations for lines l1, l3, l4 and l5 and then, when this is done, unwind with the equation for line l2.

6.4. Verification 61

19

#expand(FILTER_ASM_REWRITE_TAC(lines`l1 l3 l4 l5`)[]
#        THEN FILTER_ASM_REWRITE_TAC(lines`l2`)[]);;
OK..
"(((SUC t = 0) => F | T) =>
  (in(SUC t) =>
   ~((SUC t = 0) => F | out((SUC t) - 1)) |
   ((SUC t = 0) => F | out((SUC t) - 1))) |
  T) =
 (in(SUC t) => ~out t | out t)"
    [ "!t. l1 t = ~l2 t" ]
    [ "!t. l3 t = (in t => l1 t | l2 t)" ]
    [ "!t. l2 t = ((t = 0) => F | out(t - 1))" ]
    [ "!t. l4 t = T" ]
    [ "!t. l5 t = ((t = 0) => F | l4(t - 1))" ]
    [ "!t. out t = (l5 t => l3 t | l4 t)" ]

This goal can now be solved by rewriting with two standard built-in theorems:

  NOT_SUC   =     |- !n. ~(SUC n = 0)
  SUC_SUB1  =     |- !m. (SUC m) - 1 = m

20

#expand(REWRITE_TAC[NOT_SUC;SUC_SUB1]);;
OK..
Theorem SUC_SUB1 autoloaded from theory `arithmetic`.
SUC_SUB1 = |- !m. (SUC m) - 1 = m
OK..
goal proved
|- (((SUC t = 0) => F | T) =>
    (in(SUC t) =>
     ~((SUC t = 0) => F | out((SUC t) - 1)) |
     ((SUC t = 0) => F | out((SUC t) - 1))) |
    T) =
   (in(SUC t) => ~out t | out t)
..... |- (l5(SUC t) => l3(SUC t) | l4(SUC t)) =
         (in(SUC t) => ~out t | out t)
...... |- out(SUC t) = (in(SUC t) => ~out t | out t)
|- !in out.
    PARITY_IMP(in,out) ==>
    (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t))
Previous subproof:
goal proved

The theorem just proved is named PARITY_LEMMA and saved in the current theory.

21

#let PARITY_LEMMA = save_top_thm `PARITY_LEMMA`;;
PARITY_LEMMA =
|- !in out.
    PARITY_IMP(in,out) ==>
    (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t))

PARITY_LEMMA could have been proved in one step with a single compound tactic. This is illustrated below:

22

#set_goal
# ([], "!in out.
#         PARITY_IMP(in,out) ==>
#         (out 0 = T) /\
#         !t. out(SUC t) = (in(SUC t) => ~(out t) | out t)");;
"!in out.
  PARITY_IMP(in,out) ==>
  (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t))"

This goal can be expanded with a single tactic corresponding to the sequence of tactics that were used interactively.

23

#expand
# (PURE_REWRITE_TAC[PARITY_IMP_DEF;ONE_DEF;NOT_DEF;MUX_DEF;REG_DEF]
#  THEN REPEAT STRIP_TAC
#  THENL
#   [FILTER_ASM_REWRITE_TAC(lines`out l4 l5`)[];ALL_TAC]
#  THEN FIRST_ASSUM
#        (\th. if lines`out`(concl th)
#               then SUBST_TAC[SPEC "SUC t" th]
#               else NO_TAC)
#  THEN FILTER_ASM_REWRITE_TAC(lines`l1 l3 l4 l5`)[]
#  THEN FILTER_ASM_REWRITE_TAC(lines`l2`)[]
#  THEN REWRITE_TAC[NOT_SUC;SUC_SUB1]);;
OK..
goal proved
|- !in out.
    PARITY_IMP(in,out) ==>
    (out 0 = T) /\ (!t. out(SUC t) = (in(SUC t) => ~out t | out t))
Previous subproof:
goal proved

Armed with PARITY_LEMMA, the final theorem is easily proved. This will be done in one step using the ML function prove_thm.

6.5. Exercises 63

24

#let PARITY_CORRECT =
# prove_thm
#  (`PARITY_CORRECT`,
#   "!in out. PARITY_IMP(in,out) ==> (!t. out t = PARITY t in)",
#   REPEAT GEN_TAC
#    THEN DISCH_TAC
#    THEN IMP_RES_TAC PARITY_LEMMA
#    THEN IMP_RES_TAC UNIQUENESS_LEMMA);;
PARITY_CORRECT =
|- !in out. PARITY_IMP(in,out) ==> (!t. out t = PARITY t in)
#close_theory();;
() : void

This completes the proof of the parity checking device.

6.5 Exercises

Two exercises are given in this section: Exercise 1 is straightforward, but Exercise 2 is quite tricky and might take a beginner several days to solve. The solutions to these exercises are in the files:

   hol/Training/parity/RESET_REG.ml
   hol/Training/parity/RESET_PARITY.ml

6.5.1 Exercise 1

Using only the devices ONE, NOT, MUX and REG defined in Section 6.3, design and verify a register RESET_REG with an input in, reset line reset, output out and behaviour specified as follows.

• If reset is T at time t, then the value at out at time t is also T.

• If reset is T at time t or t+1, then the value output at out at time t+1 is T, otherwise it is equal to the value input at time t on in.

This is formalized in HOL by the definition:

  RESET_REG(reset,in,out) =
   (!t. reset t ==> (out t = T)) /\
   (!t. out(t+1) = ((reset t  \/ reset(t+1)) => T | in t))

Note that this specification is only partial; it doesn’t specify the output at time 0 in the case that there is no reset.

The solution to the exercise should be a definition of a predicate RESET_REG_IMP as an existential quantification of a conjunction of applications of ONE, NOT, MUX and REG to suitable line names,^{4} together with a proof of:

  RESET_REG_IMP(reset,in,out) ==> RESET_REG(reset,in,out)

4i.e. a definition of the same form as that of PARITY IMP on page 57.

6.5.2 Exercise 2

1. Formally specify a resetable parity checker that has two boolean inputs reset and in, and one boolean output out with the following behaviour:

The value at out is T if and only if there have been an even number of Ts input at in since the last time that T was input at reset.

2. Design an implementation of this specification built using only the devices ONE, NOT, MUX and REG defined in Section 6.3.

3. Verify the correctness of your implementation in HOL.

How to program a proof tool

Users of HOL can create their own theorem proving tools by combining predefined rules and tactics. The ML type-discipline ensures that only logically sound methods can be used to create values of type thm. In this chapter, a simple but real^{1} example is described.

Several implementations of the tool are given to illustrate various styles of proof programming. The first implementation is the obvious one, but is very slow because of the ‘brute force’ method used. The second implementation produces a much more streamlined proof, but still has a brute force component, namely the use of a tautology checker from the library taut. The third implementation replaces the general tautology checker with a special purpose derived inference rule. The fourth and final implementation uses an optimised implementation of the special purpose rule; understanding it is left as an exercise in using DESCRIPTION.

The timings in this chapter are based on Version 1.12. Later versions of HOL have an optimised tautology checker library due to Richard Boulton. This new tautology checker is actually faster than the special purpose derived rule described in Section 7.3. Thus with the new tautology checker the so called “even more efficient implementation” is actually slower than the program it replaces! This was only discovered (by Juanito Camilleri) during the preparation of Version 2 of the tutorial. Rather than completely rewriting the chapter, it was decided to leave it essentially as it was (except for the addition of this paragraph). The methods that are described are still useful, and there is an important lesson here: optimizations can become obsolete. The really dedicated reader could learn a lot by studying the old and new tautology checker (contrib/icl-taut and Library/taut, respectively) to find out how they work. Besides improving the tautology library, Richard Boulton also reimplemented rewriting using ideas from Tom Melham and Roger Fleming. As a result, in versions later than 1.12 the various rewriting tools are quite a bit faster and generate fewer intermediate theorems.

It is sometimes claimed that ‘LCF-style’ systems can never be practical, because the efficiency needed to handle real examples can only be obtained with decision procedures coded as primitive rules. It is hoped that this chapter, as well as the taut library, shows that the truth of such claims is not obvious. Research is currently in progress to see if a variety of practical decision algorithms can be implemented as efficient derived rules.

The tool described here is a tactic that puts conjunctions into the normal form obtained by right associating, sorting the conjuncts into a canonical order and then removing repetitions. This canonical order uses the built-in polymorphic infix <<, which orders any pair of ML values with the same type.

7.1 A simple implementation

A first implementation uses ‘brute-force’ rewriting with the equations:

1The example is ‘real’ in that the need for it came up last week.

66 Chapter 7. How to program a proof tool

|- (t1 /\ t2) /\ t3 = t1 /\ (t2 /\ t3)     % Associativity          %
|- t1 /\ t2 = t2 /\ t1                     % Symmetry (if t2 << t1) %
|- t1 /\ (t2 /\ t3) = t2 /\ (t1 /\ t3)     % Symmetry (if t2 << t1) %
|- t /\ t = t                              % Cancel repeated terms  %
|- t1 /\ (t1 /\ t2) = t1 /\ t2             % Cancel repeated terms  %

These equations are easily proved using the library taut. Note that HOL Version 1.12 is used in this chapter. Versions of HOL later than 1.12 contain improved rewriting tools and a new version of the library taut (the old version of the library is preserved in the directory

contrib/icl-taut).

1

scaup% hol
       _________
|___|__|   |  |   |     |__|  |__|
|      |  |   |__|   |__|__|  |__|
       Version 1.12 (Sun3/Franz), built on Feb 23 1991
#load_library `taut`;;
Loading library `taut` ...
........................
Library `taut` loaded.
() : void

The library taut defines TAUT_RULE^{2} which converts a term to the corresponding theorem, if the term is a tautology.

2The function TAUT_RULE has been replaced by a function called TAUT_PROVE in the new version of the taut library available in versions of HOL later than 1.12

7.1. A simple implementation 67

2

#let ASSOC = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3";;
ASSOC = |- (t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3
#let SYM1 = TAUT_RULE "t1 /\ t2 = t2 /\ t1";;
SYM1 = |- t1 /\ t2 = t2 /\ t1
#let SYM2 = TAUT_RULE "t1 /\ t2 /\ t3 = t2 /\ t1 /\ t3";;
SYM2 = |- t1 /\ t2 /\ t3 = t2 /\ t1 /\ t3
#let CANCEL1 = TAUT_RULE "t /\ t = t";;
CANCEL1 = |- t /\ t = t
#let CANCEL2 = TAUT_RULE "t1 /\ t1 /\ t2 = t1 /\ t2";;
CANCEL2 = |- t1 /\ t1 /\ t2 = t1 /\ t2

One cannot just use REWRITE_TAC with SYM1 and SYM2, because it would loop. What is needed is a special rewriting tool that will only apply symmetry when terms are out of order. Such a tool can be implemented as a conversion.

Conversions are described in detail in DESCRIPTION. The idea, which is due to Larry Paulson [9], is that a conversion is an ML function that maps a term t_{1} to an equation:

|- t_{1} = t_{2}.

The intention is that a conversion will only apply to a subset of terms: on members of this subset it will generate an equation, on all other terms it will fail. Because conversions are so central to theorem-proving in HOL, the ML type term->thm is abbreviated to conv. Conversions are applied using the function:

   REWR_CONV : thm -> conv

This takes an equation |- t_{1} = t_{2} and generates a conversion (i.e. ML function of type term->thm) that maps any term u that matches t_{1} to the theorem |- u = v, where v is obtained by applying the substitution obtained by matching u with t_{1} to t_{2}. If u doesn’t match t_{1} then the application

of REWR_CONV fails.

3

#REWR_CONV ASSOC "(A /\ B) /\ C";;
|- (A /\ B) /\ C = A /\ B /\ C
#REWR_CONV ASSOC "A /\ (B /\ C)";;
evaluation failed     REWR_CONV: lhs of theorem doesn't match term
#REWR_CONV SYM1 "B /\ A";;
|- B /\ A = A /\ B
#REWR_CONV SYM1 "A \/ B";;
evaluation failed     REWR_CONV: lhs of theorem doesn't match term

For our application, the required conversion should map a conjunction

t_{1} /\ (t_{2_{1}} /\ t_{2_{2}}) in which t_{2_{1}} << t_{1} to the equational theorem:

|- t_{1} /\ (t_{2_{1}} /\ t_{2_{2}}) = t_{2_{1}} /\ (t_{1} /\ t_{2_{2}})

If t_{1} << t_{2_{1}} then the conversion fails (in the ML sense) when applied to t_{1} /\ (t_{2_{1}} /\ t_{2_{2}}). In addition, if the right conjunct is not itself a conjunction, then the conversion should reorder if necessary. More precisely, if the conversion is applied to t_{1} /\ t_{2} where t_{2} is not a conjunction and t_{2} << t_{1}, then it should generate the equation:

|- t_{1} /\ t_{2} = t_{2} /\ t_{1}

Such a conversion is easily implemented in ML using SYM1 and SYM2 proved above, together with the ML syntax processing functions is_conj and dest_conj, where:

   is_conj   : term -> bool
   dest_conj : term -> (term # term)

These are functions that test whether a term is a conjunction, and splits a term into its two conjuncts, respectively. For example:

4

#is_conj "A /\ B";;
true : bool
#is_conj "A \/ B";;
false : bool
#dest_conj "A /\ B";;
("A", "B") : (term # term)
#dest_conj "A \/ B";;
evaluation failed     dest_conj

The implementation of the special purpose conversion, CONJ_ORD_CONV, is now straightforward.

5

#let CONJ_ORD_CONV t =
# let t1,t2 = dest_conj t
# in
# if is_conj t2
#   then (let t21,t22 = dest_conj t2
#         in
#         if t21 << t1 then REWR_CONV SYM2 t else fail)
#   else (if t2  << t1 then REWR_CONV SYM1 t else fail);;
CONJ_ORD_CONV = - : conv

This is illustrated by:

6

#"A:bool" << "B:bool";;
true : bool
#"B:bool" << "C:bool";;
true : bool
#CONJ_ORD_CONV "B /\ A";;
|- B /\ A = A /\ B
#CONJ_ORD_CONV "A /\ B";;
evaluation failed     fail

The process of normalizing a conjunction can be split into four phases:

1. Right associate the conjunction by repeatedly applying:

         REWR_CONV ASSOC

2. Put the conjuncts in canonical order by repeatedly applying:

         CONJ_ORD_CONV

3. Remove repetitions of t of the form t /\ t by repeatedly applying:

         REWR_CONV CANCEL1

4. Remove repetitions of t_{1} in t_{1} /\ (t_{1} /\ t_{2}) by repeatedly applying:

         REWR_CONV CANCEL2

To implement this, a method of repeatedly applying a conversion to subterms of a term is needed. This is provided by the operator

   TOP_DEPTH_CONV : conv -> conv

If c is a conversion then TOP_DEPTH_CONV c is a conversion that repeatedly applies c to all subterms until c is no longer applicable to any subterms. The function TOP_DEPTH_CONV is one of a family of operators that apply conversions throughout terms. Members of this family differ in the order in which subterms are visited and the amount of repetition that is done. For more details, see the chapter on conversions in DESCRIPTION.

7

#let ex1 = "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D";;
ex1 = "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" : term
#REWR_CONV ASSOC ex1;;
evaluation failed     REWR_CONV: lhs of theorem doesn't match term
#TOP_DEPTH_CONV (REWR_CONV ASSOC) ex1;;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D =
   A /\ B /\ C /\ A /\ C /\ A /\ D /\ D

The right hand side of this theorem is ex1 in right-associated form. The conclusion of a theorem can be extracted with the ML function concl and the right hand side of an equation can be extracted with rhs. Thus, continuing the session:

8

#let ex2 = rhs(concl it);;
ex2 = "A /\ B /\ C /\ A /\ C /\ A /\ D /\ D" : term
#TOP_DEPTH_CONV CONJ_ORD_CONV ex2;;
|- A /\ B /\ C /\ A /\ C /\ A /\ D /\ D =
   A /\ A /\ A /\ B /\ C /\ C /\ D /\ D

The right hand side of this is the result of canonicalizing the order of the conjuncts in the left hand side. Next, the repetitions can be eliminated using CANCEL1 and CANCEL2.

9

#let ex3 = rhs(concl it);;
ex3 = "A /\ A /\ A /\ B /\ C /\ C /\ D /\ D" : term
#TOP_DEPTH_CONV (REWR_CONV CANCEL1) ex3;;
|- A /\ A /\ A /\ B /\ C /\ C /\ D /\ D =
   A /\ A /\ A /\ B /\ C /\ C /\ D

10

#let ex4 = rhs(concl it);;
ex4 = "A /\ A /\ A /\ B /\ C /\ C /\ D" : term
#TOP_DEPTH_CONV (REWR_CONV CANCEL2) ex4;;
|- A /\ A /\ A /\ B /\ C /\ C /\ D = A /\ B /\ C /\ D

To make the conjunction normalizer, the four stages just described must be performed in sequence. Conversions can be applied in sequence using the infixed function:

   THENC : conv -> conv -> conv

If c_{1} t_{1} evaluates to |- t_{1}=t_{2} and c_{2} t_{2} evaluates to |- t_{2}=t_{3}, then (c_{1} THENC c_{2}) t_{1} evaluates to |- t_{1}=t_{3}. If the evaluation of c_{1} t_{1} or the evaluation of c_{2} t_{2} fails, then so does the evaluation of c_{1} THENC c_{2}. THENC is justified by the transitivity of equality.

Using THENC, the normalizer is defined by

11

#let CONJ_NORM_CONV =
# TOP_DEPTH_CONV(REWR_CONV ASSOC)   THENC
# TOP_DEPTH_CONV CONJ_ORD_CONV         THENC
# TOP_DEPTH_CONV(REWR_CONV CANCEL1) THENC
# TOP_DEPTH_CONV(REWR_CONV CANCEL2);;
CONJ_NORM_CONV = - : conv
#CONJ_NORM_CONV ex1;;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D

This conversion can now be converted to a rule or tactic using the functions CONV_RULE or CONV_TAC, respectively.

CONV_RULE : conv -> thm -> thm
CONV_TAC  : conv -> tactic

CONV_RULE c (|- t) returns |- t′, where c t evaluates to the equation |- t=t′. CONV_TAC c is a tactic that converts the conclusion of a goal using c. For more details see DESCRIPTION.

12

#let CONJ_NORM_TAC = CONV_TAC CONJ_NORM_CONV;;
CONJ_NORM_TAC = - : tactic

Here is an example. It uses antiquotation: if x is an ML indentifier bound to term, then occurrences of ^x inside a quotation denotes the term bound to x.

13

#g "^ex1 ==> B";;
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> B"
() : void
#e CONJ_NORM_TAC;;
OK..
"A /\ B /\ C /\ D ==> B"

To summarize, here is the ML code implementing the normalizer:

load_library `taut`;;
let ASSOC   = TAUT_RULE "(t1 /\ t2) /\ t3 = t1 /\ t2 /\ t3"
and SYM1    = TAUT_RULE "t1 /\ t2 = t2 /\ t1"
and SYM2    = TAUT_RULE "t1 /\ t2 /\ t3 = t2 /\ t1 /\ t3"
and CANCEL1 = TAUT_RULE "t /\ t = t"
and CANCEL2 = TAUT_RULE "t1 /\ t1 /\ t2 = t1 /\ t2";;
let CONJ_ORD_CONV t =
 let t1,t2 = dest_conj t
 in
 if is_conj t2
   then (let t21,t22 = dest_conj t2
         in
         if t21 << t1 then REWR_CONV SYM2 t else fail)
   else (if t2  << t1 then REWR_CONV SYM1 t else fail);;
let CONJ_NORM_CONV =
 TOP_DEPTH_CONV(REWR_CONV ASSOC)   THENC
 TOP_DEPTH_CONV CONJ_ORD_CONV         THENC
 TOP_DEPTH_CONV(REWR_CONV CANCEL1) THENC
 TOP_DEPTH_CONV(REWR_CONV CANCEL2);;
let CONJ_NORM_TAC = CONV_TAC CONJ_NORM_CONV;;

7.2 A more efficient implementation

The normalizer just given is rather slow. This can be shown by switching on the system timer using the function:

    timer : bool -> bool

Evaluating timer true switches on timing; evaluating timer false switches it off (the previous value of the timing flag is returned). Garbage collection times are also shown, together with a count of the number of intermediate theorems that are generated (which gives an estimate of the number of primitive inferences done).

14

 #timer true;;
 false : bool
 Run time: 0.0s
 #CONJ_NORM_CONV ex1;;
 |- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D
 Run time: 1.1s
 Garbage collection time: 0.5s
 Intermediate theorems generated: 73

Here is a bigger example:

15

 #CONJ_NORM_CONV "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";;
 |- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
     (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
     A /\
     (B /\ C /\ A) /\
     (C /\ A /\ D) /\
     D) /\
    A /\
    (B /\ C /\ A) /\
    (C /\ A /\ D) /\
    D =
    A /\ B /\ C /\ D
 Run time: 38.3s
 Garbage collection time: 11.5s
 Intermediate theorems generated: 16761

The reason that CONJ_CANON_CONV is slow is because of the repeated pattern matching done during rewriting. A much more efficient approach is to normalize the conjunction by ML programming outside the logic, and then to prove that the normalized term is equal to the original one. An even more efficient approach, which is not explored here, would be to avoid having to do this proof by verifing the normalization code by some sort of meta-theoretic reasoning about ML. How to do this in HOL is not clear, but work on this approach has been done in the context of FOL [11], the Boyer-Moore prover [2] and Nuprl [1]. These approaches all use

7.2. A more efficient implementation 73

logically sophisticated extra axioms, called reflection principles, that enable metatheorems to be ‘reflected’ into the logic as object level theorems.

To normalize the term by ML programming, the conjuncts are extracted, repeated elements are deleted and the resulting list is sorted.

HOL already has a predefined function:

   conjuncts : term -> term list

for extracting conjuncts. HOL also has a predefined ML function for removing repeated elements of a list:

   setify : * list -> * list

Both conjuncts and setify are illustrated below:

16

#timer false;;
true : bool
#conjuncts ex1;;
["A"; "B"; "C"; "A"; "C"; "A"; "D"; "D"] : term list
#setify it;;
["B"; "C"; "A"; "D"] : term list
#let ex1_list = it;;
ex1_list = ["B"; "C"; "A"; "D"] : term list

There is a predefined sorting function in ML:

17

#sort;;
sort = - : (((* # *) -> bool) -> * list -> * list)
#sort $< [3;2;5;6;1;1;7;9;3];;
[1; 1; 2; 3; 3; 5; 6; 7; 9] : int list
#sort $<< ex1_list;;
["A"; "B"; "C"; "D"] : term list

Using this function, the list of conjuncts of the normalization of a term is easily computed. The predefined ML function:

   list_mk_conj : term list -> term

can then be used to build the normalized conjunction.

18

#ex1;;
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" : term
#let ex1_norm = list_mk_conj(sort $<< (setify(conjuncts ex1)));;
ex1_norm = "A /\ B /\ C /\ D" : term

The calculation of ex1_norm from ex1 has been done by (unverified) ML code. What is required is the theorem asserting that they are equal. This can be proved using the tautology checker.

19

#TAUT_RULE "^ex1 = ^ex1_norm";;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D

A conversion that normalizes conjunctions is thus:

20

#let CONJ_NORM_CONV2 t =
# if is_conj t
#  then TAUT_RULE "^t = ^(list_mk_conj(sort $<< (setify(conjuncts t))))"
#  else fail;;
CONJ_NORM_CONV2 = - : conv
#CONJ_NORM_CONV2 ex1;;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D

CONJ_CANON_CONV2 is more than an order of magnitude faster than CONJ_CANON_CONV:

21

#timer true;;
false : bool
Run time: 0.0s
#CONJ_NORM_CONV2 "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";;
|- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
   (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
   ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    A /\
    (B /\ C /\ A) /\
    (C /\ A /\ D) /\
    D) /\
   A /\
   (B /\ C /\ A) /\
   (C /\ A /\ D) /\
   D =
   A /\ B /\ C /\ D
Run time: 1.9s
Garbage collection time: 0.5s
Intermediate theorems generated: 1273

7.3 An even more efficient implementation

Although the implementation just given is much faster than the first naive one, it can be improved further by replacing the call to the general tautology checker with a special purpose conjunction-equivalence prover.

To see how this works, the equivalence of ex1 and ex1_norm will first be proved manually. The general form of this proof will then be abstracted into a derived rule.

The goal is to prove that ex1 and ex1_norm are equal.

7.3. An even more efficient implementation 75

22

#timer false;;
true : bool
#g "^ex1 = ^ex1_norm";;
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D"
() : void

The predefined tactic EQ_TAC splits an equation into two implications (see Section 5.3.3).

23

#e EQ_TAC;;
OK..
2 subgoals
"A /\ B /\ C /\ D ==> A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D"
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==> A /\ B /\ C /\ D"
() : void

Each of these can be solved by:

1. moving the antecedent of the implication to the assumption list (using DISCH_TAC, see Section 5.3.4);

2. breaking up the remaining goal (the consequent of the implication) into one subgoal per conjunct (using CONJ_TAC, see Section 5.3.2);

3. solving each of these conjuncts using the antecedent (which is now an assumption)

Step 1–3 are now done interactively.

24

#e DISCH_TAC;;
OK..
"A /\ B /\ C /\ D"
    [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
() : void

CONJ_TAC is repeated using the tactical REPEAT described in Section 5.2.2.

25

 #e (REPEAT CONJ_TAC);;
 OK..
 4 subgoals
 "D"
     [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
 "C"
     [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
 "B"
     [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
 "A"
     [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
 () : void

The final step is to use the assumption "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" to solve each goal. To do this, the assumption is grabbed using the tactical:

    POP_ASSUM : (thm -> tactic) -> tactic

Given a function f : thm -> tactic, the tactic POP_ASSUM f applies f to the (assumed) first assumption of a goal and then applies the tactic created thereby to the original goal minus its top assumption:

    POP_ASSUM f ([t_{1};. . .;t_{n}],t) = f (ASSUME t_{1}) ([t_{2};. . .;t_{n}],t)

ML functions such as f, with type thm -> tactic are abbreviated to thm_tactic (see DE-SCRIPTION for further details).

After grabbing the assumption, it is split into its individual conjunctions using the predefined derived rule:

    CONJUNCTS : thm -> thm list

For example:

26

 #CONJUNCTS(ASSUME "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D");;
 [. |- A; . |- B; . |- C; . |- A; . |- C; . |- A; . |- D; . |- D]
 : thm list

Among the individual conjuncts is the goal, which can thus be solved immediately using ACCEPT_TAC (see Section 5.3.9). The appropriate assumption can be chosen with the predefined tactical MAP_FIRST, which is characterized by:

    MAP_FIRST f [x_{1}; . . . ;x_{n}]  = f(x_{1}) ORELSE . . . ORELSE f(x_{n})

Returning to the proof: the final step is now performed by popping the assumption and applying to it the function obtained by composing CONJUNCTS and MAP_FIRST using the ML infixed function composition operator o (where (f o g)x = g(f(x))).

7.3. An even more efficient implementation 77

27

#e(POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS));;
OK..
goal proved
. |- A
Previous subproof:
3 subgoals
"D"
    [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
"C"
    [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
"B"
    [ "A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D" ]
() : void

The remaining subgoals are solved identically. Stitching together the tactics just used results in:

   EQ_TAC          THEN
   DISCH_TAC       THEN
   REPEAT CONJ_TAC THEN
   POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS)

With this, the entire proof can be done in one step.

28

#g "^ex1 = ^ex1_norm";;
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D"
() : void
#e(EQ_TAC          THEN
#  DISCH_TAC       THEN
#  REPEAT CONJ_TAC THEN
#  POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS));;
OK..
goal proved
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D = A /\ B /\ C /\ D
Previous subproof:
goal proved
() : void

Using this tactic, a derived rule CONJ_EQ can be defined that proves two conjunctions equal. This is what is needed to replace the call to TAUT_RULE. CONJ_EQ is defined with the predefined function:

   PROVE : term # tactic -> theorem

PROVE(t,T) applies the tactic T to the goal ([],t); if this goal is proved by T then the resulting justification is applied to [] to obtain the theorem |- t, which is returned. If T does not solve the goal, then the application of PROVE fails. Using PROVE, the definition of CONJ_EQ is:

   let CONJ_EQ t1 t2 =
    PROVE ("^t1 = ^t2",
           EQ_TAC          THEN
           DISCH_TAC       THEN
           REPEAT CONJ_TAC THEN
           POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS))

Replacing the call to TAUT_RULE in the definition of CONJ_NORM_CONV2 results in:

   let CONJ_NORM_CONV3 t =
    if is_conj t
     then CONJ_EQ t (list_mk_conj(sort $<< (setify(conjuncts t))))
     else fail

Continuing the session:

29

#let CONJ_EQ t1 t2 =
# PROVE ("^t1 = ^t2",
#        EQ_TAC          THEN
#        DISCH_TAC       THEN
#        REPEAT CONJ_TAC THEN
#        POP_ASSUM(MAP_FIRST ACCEPT_TAC o CONJUNCTS));;
CONJ_EQ = - : (term -> conv)
#let CONJ_NORM_CONV3 t =
# if is_conj t
#  then CONJ_EQ t (list_mk_conj(sort $<< (setify(conjuncts t))))
#  else fail;;
CONJ_NORM_CONV3 = - : conv

CONJ_NORM_CONV3 is almost twice as efficient as CONJ_NORM_CONV2. To show this, the timer is switched back on.

30

#timer true;;
false : bool
Run time: 0.0s

Here is the big example with CONJ_NORM_CONV3:

7.4. Further optimizations 79

31

 #CONJ_NORM_CONV3 "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";;
 |- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
     (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
     A /\
     (B /\ C /\ A) /\
     (C /\ A /\ D) /\
     D) /\
    A /\
    (B /\ C /\ A) /\
    (C /\ A /\ D) /\
    D =
    A /\ B /\ C /\ D
 Run time: 1.0s
 Garbage collection time: 0.5s
 Intermediate theorems generated: 775

7.4 Further optimizations

Further improvements are still possible. As an exercise the reader might want to decipher the following highly optimized definition of CONJ_EQ.

The function PROVE_CONJ, defined below, converts a term t to the theorem |- t if that theorem occurs in a supplied list of theorems (ths in the code below), or t is a conjunction each of whose conjuncts occurs in the list. The definition of PROVE_CONJ uses the following predefined ML functions:

   • uncurry f (x,y) = f x y
   • (f # g)(x,y) = (f x , g y)

• find p [x_{1}; …;x_{n}] = the first x_{i} for which p x_{i} is true

and the inference rule CONJ:

\frac{Γ_{1} ⊢ t_{1} Γ_{2} ⊢ t_{2}}{Γ_{1} ∪ Γ_{2} ⊢ t_{1} ∧ t_{2}}

Here is the definition of PROVE_CONJ:

    letrec PROVE_CONJ ths tm =
     (uncurry CONJ ((PROVE_CONJ ths # PROVE_CONJ ths) (dest_conj tm))) ?
     find (\th. concl th = tm) ths

Using this, the optimized CONJ_EQ, called CONJ_EQ2, is defined using IMP_ANTISYM_RULE (a predefined rule):

\frac{Γ_{1} ⊢ t_{1} ⇒ t_{2} Γ_{2} ⊢ t_{2} ⇒ t_{1}}{Γ_{1} ∪ Γ_{2} ⊢ t_{1} = t_{2}}

The definition is:

   let CONJ_EQ2 t1 t2 =
    let imp1 = DISCH t1 (PROVE_CONJ (CONJUNCTS(ASSUME t1)) t2)
    and imp2 = DISCH t2 (PROVE_CONJ (CONJUNCTS(ASSUME t2)) t1)
    in IMP_ANTISYM_RULE imp1 imp2

Loading these ML function definitions into HOL:

32

#letrec PROVE_CONJ ths tm =
# (uncurry CONJ ((PROVE_CONJ ths # PROVE_CONJ ths) (dest_conj tm))) ?
# find (\th. concl th = tm) ths;;
PROVE_CONJ = - : (thm list -> conv)
Run time: 0.0s
#let CONJ_EQ2 t1 t2 =
# let imp1 = DISCH t1 (PROVE_CONJ (CONJUNCTS(ASSUME t1)) t2)
# and imp2 = DISCH t2 (PROVE_CONJ (CONJUNCTS(ASSUME t2)) t1)
# in IMP_ANTISYM_RULE imp1 imp2;;
CONJ_EQ2 = - : (term -> conv)
Run time: 0.0s

A version of CONJ_NORM_CONV that uses CONJ_EQ2 is defined by:

   let CONJ_NORM_CONV4 t =
    if is_conj t
     then CONJ_EQ2 t (list_mk_conj(sort $<< (setify(conjuncts t))))
     else fail

Loading this into ML:

33

#let CONJ_NORM_CONV4 t =
# if is_conj t
#  then CONJ_EQ2 t (list_mk_conj(sort $<< (setify(conjuncts t))))
#  else fail;;
CONJ_NORM_CONV4 = - : conv
Run time: 0.0s

This is even faster than CONJ_NORM_CONV3:

34

#CONJ_NORM_CONV4 "^ex1 /\ (^ex1 /\ (^ex1 /\ ^ex1 /\ ^ex1) /\ ^ex1)";;
|- (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
   (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
   ((A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\
    A /\
    (B /\ C /\ A) /\
    (C /\ A /\ D) /\
    D) /\
   A /\
   (B /\ C /\ A) /\
   (C /\ A /\ D) /\
   D =
   A /\ B /\ C /\ D
Run time: 0.4s
Intermediate theorems generated: 155

7.5. Normalizing all subterms 81

7.5 Normalizing all subterms

There is an important difference in the functionality of CONJ_NORM_CONV and the various optimised versions of it. The difference is that CONJ_NORM_CONV applies to any term, normalizing all subterms that are conjunctions. However the functions CONJ_NORM_CONVn (where n = 2, 3, 4) all fail on non-conjunctions.

35

#CONJ_NORM_CONV "^ex1 ==> ^ex1";;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==>
   A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D =
   A /\ B /\ C /\ D ==> A /\ B /\ C /\ D
Run time: 2.0s
Garbage collection time: 0.6s
Intermediate theorems generated: 1307
#CONJ_NORM_CONV4 "^ex1 => ^ex1";;
need 2 nd branch to conditional
skipping: ex1 " ;; parse failed
#CONJ_NORM_CONV4 "^ex1 ==> ^ex1";;
evaluation failed     fail

What is needed is a function that will apply a conversion to all conjunctive subterms of a term. Such a function is TOP_DEPTH_CONV, however

   TOP_DEPTH_CONV CONJ_NORM_CONV4

would loop, because CONJ_NORM_CONV4 never fails on conjunctions, so TOP_DEPTH_CONV would keep applying it forever! This is easily got around using:

   CHANGED_CONV : conv -> conv

CHANGED_CONV c behaves like c, except that if c has no effect, then CHANGED_CONV c fails.

36

#TOP_DEPTH_CONV(CHANGED_CONV CONJ_NORM_CONV4) "^ex1 ==> ^ex1";;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==>
   A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D =
   A /\ B /\ C /\ D ==> A /\ B /\ C /\ D
Run time: 0.5s
Intermediate theorems generated: 292

Although this works, the scanning through subterms done by TOP_DEPTH_CONV is a bit ‘brute force’. Further efficiency can be obtained by writing a special scanning function that just applies a conversion to maximal conjunctive subterms. This is provided by the code below. The understanding of this is a fairly hard exercise for the reader. The section on conversions in DESCRIPTION should be helpful.

First, an auxiliary derived rule for combining two equations into a single equation by conjoining the left hand sides and the right hand sides.

37

#let MK_CONJ th1 th2 = MK_COMB(AP_TERM "$/\" th1, th2);;
MK_CONJ = - : (thm -> thm -> thm)
Run time: 0.0s

Next a function that conjoins the left hand sides and right hand sides of lists of equations.

38

#letrec MK_CONJL l =
# if null l     then fail
# if null(tl l) then hd l
#               else MK_CONJ (hd l) (MK_CONJL(tl l));;
MK_CONJL = - : proof
Run time: 0.0s

Next, a function that applies a conversion c to all conjunctive subterms of a term. This uses the ML function:

map f [x_{1}; …;x_{n}] = [f x_{1}; …;f x_{n}]

and the rules MK_COMB:

\frac{Γ_{1} ⊢ f = g Γ_{2} ⊢ x = y}{Γ_{1} ∪ Γ_{2} ⊢ f x = g y}

and MK_ABS:

\frac{Γ ⊢ ∀x. t_{1} = t_{2}}{Γ ⊢ (λx. t_{1}) = (λx. t_{2})}

and GEN:

\frac{Γ ⊢ t}{Γ ⊢ ∀x. t}

• Where x is not free in Γ.

and REFL:

\overline{⊢ t = t}

• REFL t = ⊢ t = t.

The definition of CONJ_DEPTH_CONV also uses:

   is_comb   : term -> bool
   dest_comb : term -> (term # term)
   is_abs    : term -> bool
   dest_abs  : term -> (term # term)

which are the tests and destructors for combinations and abstractions, respectively.

39

#letrec CONJ_DEPTH_CONV c tm =
# if is_conj tm
#  then (c THENC (MK_CONJL o map (CONJ_DEPTH_CONV c) o conjuncts)) tm
# if is_comb tm
#  then (let rator,rand = dest_comb tm in
#         MK_COMB (CONJ_DEPTH_CONV c rator, CONJ_DEPTH_CONV c rand))
# if is_abs tm
#  then (let bv,body = dest_abs tm in
#         let bodyth = CONJ_DEPTH_CONV c body in
#         MK_ABS (GEN bv bodyth))
#   else (REFL tm);;
CONJ_DEPTH_CONV = - : (conv -> conv)
Run time: 0.0s

The next session shows that CONJ_DEPTH_CONV is an improvement over TOP_DEPTH_CONV.

40

#CONJ_DEPTH_CONV CONJ_NORM_CONV4 "^ex1 ==> ^ex1";;
|- A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==>
   A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D =
   A /\ B /\ C /\ D ==> A /\ B /\ C /\ D
Run time: 0.4s
Intermediate theorems generated: 95

However, the figures show that we are getting to a point of diminishing returns.

Finally, the tactic for normalizing all conjunctions in a goal is:

41

#let CONJ_NORM_TAC = CONV_TAC (CONJ_DEPTH_CONV CONJ_NORM_CONV4);;
CONJ_NORM_TAC = - : tactic
Run time: 0.0s

This is illustrated by:

42

#g "^ex1 ==> ^ex1 /\ ^ex1_norm";;
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==>
 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ A /\ B /\ C /\ D"
() : void
Run time: 0.1s
#e CONJ_NORM_TAC;;
OK..
"A /\ B /\ C /\ D ==> A /\ B /\ C /\ D"
() : void
Run time: 0.3s
Intermediate theorems generated: 110

To show how much faster the optimized version is, here is the last step repeated with the first version of the tool. The ML function b backs up to the last goal.

43

#b();;
"A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D ==>
 (A /\ (B /\ C /\ A) /\ (C /\ A /\ D) /\ D) /\ A /\ B /\ C /\ D"
() : void
Run time: 0.1s

Expanding with the slow tactic:

44

#e(CONV_TAC CONJ_NORM_CONV);;
OK..
"A /\ B /\ C /\ D ==> A /\ B /\ C /\ D"
() : void
Run time: 3.5s
Garbage collection time: 1.0s
Intermediate theorems generated: 1932

it is 10 times slower and generates almost 20 times as many primitive inference steps! Here is the complete ML program for the optimized normalizer.

   letrec insert ord x l =
    if null l
     then [x]
    if ord(x,hd l)
     then x.l
     else hd l.(insert ord x (tl l));;
   letrec sort ord l =
    if null l
     then []
     else insert ord (hd l) (sort ord (tl l));;

   letrec PROVE_CONJ ths tm =
    (uncurry CONJ ((PROVE_CONJ ths # PROVE_CONJ ths) (dest_conj tm))) ?
    find (\th. concl th = tm) ths;;
   let CONJ_EQ t1 t2 =
    let imp1 = DISCH t1 (PROVE_CONJ (CONJUNCTS(ASSUME t1)) t2)
    and imp2 = DISCH t2 (PROVE_CONJ (CONJUNCTS(ASSUME t2)) t1)
    in IMP_ANTISYM_RULE imp1 imp2;;

   let CONJ_NORM_CONV t =
    if is_conj t
     then CONJ_EQ t (list_mk_conj(sort $<< (setify(conjuncts t))))
     else fail;;

    let MK_CONJ th1 th2 = MK_COMB(AP_TERM "$/\" th1, th2);;
    letrec MK_CONJL l =
     if null l     then fail
     if null(tl l) then hd l
                   else MK_CONJ (hd l) (MK_CONJL(tl l));;
    letrec CONJ_DEPTH_CONV c tm =
     if is_conj tm
      then (c THENC (MK_CONJL o map (CONJ_DEPTH_CONV c) o conjuncts)) tm
     if is_comb tm
      then (let rator,rand = dest_comb tm in
             MK_COMB (CONJ_DEPTH_CONV c rator, CONJ_DEPTH_CONV c rand))
     if is_abs tm
      then (let bv,body = dest_abs tm in
             let bodyth = CONJ_DEPTH_CONV c body in
             MK_ABS (GEN bv bodyth))
      else (REFL tm);;
    let CONJ_NORM_TAC = CONV_TAC (CONJ_DEPTH_CONV CONJ_NORM_CONV);;

Although the optimized implementation is much more efficient, it uses less general methods. An advantage of the simple implementation based on rewriting is that essentially the same algorithm can be used to normalize terms built out of any associative, commutative and idenpotent operation. The two exercises that follow (whose solutions are not supplied) suggest that the reader try to extract general principles from the conjunction normalizer and use these to implement generic tools.

7.5.1 Exercise 1

Implement a normalizer for any associative and commutative operator.

    AC_CANON_CONV : thm # thm -> conv

The two theorem arguments should be the associative and commutative laws for the operator. For example:

    AC_CANON_CONV(ASSOC,SYM1)

would be a canonicalizer for conjunctions. Use the ‘brute force’ rewriting method described at the beginning of this chapter.

7.5.2 Exercise 2

Implement an optimized canonicalizer:

    FAST_AC_CANON_CONV : thm # thm -> conv

This should use tuned rewriting (e.g. a generalization of CONJ_DEPTH_CONV) and be as fast as possible. Try to think up tricks to minimise the amount of general matching and to make every inference count.

86 Chapter 7. How to program a proof tool

Example: the Binomial Theorem

The Binomial Theorem in HOL is a medium sized worked example whose subject matter is more widely known than any specific piece of hardware or software. This chapter introduces the small amount of algebra and mathematical notation needed to state and prove the Binomial Theorem, shows how this is rendered in HOL, and outlines the structure of the proof.

This chapter is also available as the self-contained case study binomial in the directory

Training/studies.

8.1 Pascal’s Triangle and the Binomial Theorem

Pascal’s Triangle^{1} is the infinite triangle of numbers which starts like this:

1

1 1
1 2 1
1 3 3 1
1 4 6 4 1
1 5 10 10 5 1
· · · · · · ·

The construction is as follows. The numbers at the edges are 1s. Each number in the interior is the sum of the number immediately above it and the number to its left in the previous row.

The numbers in Pascal’s Triangle are called Binomial Coefficients. The number in the nth row and kth column (where 0 ≤ k ≤ n, and the topmost row and the leftmost column are numbered 0) is written \binom{n}{k} and pronounced “n choose k”. The coefficients are pronounced this way because \binom{n}{k} turns out to be the number of ways to choose k things out of n things, but that is another story (see for instance Knuth’s book [5]).

A simple form of the Binomial Theorem [6] [8] is the following equation, where a and b are integers and n is any natural number,

(a + b)^{n} = ∑_{k=0}^{n} \binom{n}{k}a^{k}b^{n−k}

The rest of this chapter describes how the Binomial Theorem can be proven in HOL. In fact, a more general theorem is proven, where a and b are elements of an arbitrary commutative ring, but the form displayed here can be derived from the general result.

1According to Knuth [5], the triangle gets its name from its appearance in Blaise Pascal’s Traité du triangle arithmétique in 1653, although the binomial coefficients were known long before then. The earliest surviving description is from the tenth century, in Halāyudha’s commentary on the Hindu classic, the Chandah-Sûtra. The Binomial Theorem itself was first reported in 1676 by Isaac Newton.

88 Chapter 8. Example: the Binomial Theorem

The motivation for the proof of the Binomial Theorem in HOL is tutorial. The proof illustrates specific ways in HOL to represent mathematical notations and manage theorems proven about general structures such as monoids, groups and rings. The following files accompany this chapter

in directory Training/studies/binomial:

mk BINOMIAL.ml The ML program containing the definitions, lemmas and theorems needed to prove the Binomial Theorem in HOL.

BINOMIAL.th The theory file which is generated by mk_BINOMIAL.ml.

BINOMIAL.ml An ML program which loads the theory BINOMIAL and declares a few derived rules and one tactic used in the proof. The Binomial Theorem is bound to the ML identifier

     BINOMIAL.

The chapter is meant to be intelligible without examination of any of the accompanying files. To avoid clutter not every detail is spelt out. Often definitions and theorems are indicated in the form displayed by HOL, rather than as ML source text. Specific details of the ML definitions or tactics can be found in the file mk_BINOMIAL.ml.

The way to work with this case study is first to study this chapter to see the structure of the proof, and then to work interactively with HOL. Start HOL and say:

45

 #loadt `BINOMIAL`;;
 ...
 File BINOMIAL loaded
 () : void
 #BINOMIAL;;
 |- !plus times.
     RING(plus,times) ==>
     (!a b n.
       POWER times n(plus a b) =
       SIGMA(plus,0,SUC n)(BINTERM plus times a b n))

(This is the first display of an interaction with HOL. The difference between lines input to and lines output from HOL is that only the former are preceded by the HOL prompt “#”. A line of ellipsis “...” stands for output from HOL which has been omitted from the display.)

The first input line in the display above loads in all the definitions, theorems, derived rules and the tactic defined for the proof. The second input line asks HOL to print theorem BINOMIAL. The constants used in BINOMIAL are explained later in the chapter. The HOL session is now set up either to make use of BINOMIAL by specialising it to a specific ring, or to study mk_BINOMIAL.ml by using the subgoal package to work through proofs contained in it.

The remainder of the chapter follows the plan:

Section 8.2 shows how to define the number \binom{n}{k} in HOL as the term CHOOSE n k, where CHOOSE is a function defined by primitive recursion.

Section 8.3 shows how to define elementary algebraic concepts like associativity, commutativity, monoid, group and ring in HOL, and how to apply theorems proved in the general case to particular situations.

8.2. The Binomial Coefficients 89

Section 8.4 shows how to define the iterated operations of raising a term to a power and reducing (summing) a list of terms. These operations are part of the everyday mathematical language used to state the Binomial Theorem, but they are not built-in to HOL and so need to be defined. This section and the previous two together describe enough definitions in HOL to state the Binomial Theorem.

Section 8.5 shows how the Binomial Theorem is proven in HOL. The proof is by induction, and depends on three main lemmas.

Section 8.6 outlines how to apply the general theorem to a particular case: the ring of integers.

Appendix 8.7 states the principal lemmas used to prove the theorem. Some of these are ad hoc but others could be reused elsewhere.

8.2 The Binomial Coefficients

The definition of the binomial coefficients as the numbers in Pascal’s Triangle is formalised in three equations:

\binom{n}{0} = 1

\binom{0}{k + 1} = 0

\binom{n + 1}{k + 1} = \binom{n}{k + 1} + \binom{n}{k}

(These actually define \binom{n}{k} to be 0 if k > n, but this is consistent with Pascal’s Triangle: think of the spaces to the right of the triangle as filled with 0’s.) The desire is to define a constant CHOOSE in HOL such that for all numbers n, k in the type num, CHOOSE n k denotes the number \binom{n}{k}. Unfortunately these three equations cannot be used directly as the definition of CHOOSE in HOL because they are not in the form of a base case (when n = 0) together with an inductive case (when n > 0).

To work towards the definition, consider a term that specifies a base case and an inductive case intended to be equivalent to the three equations above:

46

 let base_and_inductive: term =
     "(CHOOSE 0 k = ((0 = k) => 1 | 0)) /\
      (CHOOSE (SUC n) k =
          ((0 = k) => 1 | (CHOOSE n (k-1)) + (CHOOSE n k)))";;

The theory prim_rec contains a primitive recursion theorem which says that any base case and inductive case identifies a unique function, fn:

47

 #num_Axiom;;
 |- !e f. ?! fn.
     (fn 0 = e) /\
     (!n. fn (SUC n) = f (fn n) n)

Given the theorem prim_rec, the builtin function prove_rec_fn_exists can prove that there is a function that satisfies the property specified by the term base_and_inductive:

48

 #let RAW_CHOOSE_DEF = prove_rec_fn_exists num_Axiom base_and_inductive;;
 RAW_CHOOSE_DEF =
 |- ?CHOOSE.
     (!k. CHOOSE 0 k = ((0 = k) => 1 | 0)) /\
     (!n k.
       CHOOSE(SUC n)k = ((0 = k) => 1 | (CHOOSE n(k - 1)) + (CHOOSE n k)))

These equations would not do as the only definition of CHOOSE due to the presence of the conditional operator, which makes rewriting difficult. But having obtained the theorem RAW_CHOOSE_DEF it is easy to prove there is a function which satisfies the original three equations:

49

 CHOOSE_DEF_LEMMA =
 |- ?CHOOSE.
     (!n. CHOOSE n 0 = 1) /\
     (!k. CHOOSE 0(SUC k) = 0) /\
     (!n k. CHOOSE(SUC n)(SUC k) = (CHOOSE n(SUC k)) + (CHOOSE n k))

Now the constant CHOOSE can be specified as originally desired:

50

 #let CHOOSE_DEF =
 #    new_specification `CHOOSE_DEF` [`constant`,`CHOOSE`] CHOOSE_DEF_LEMMA;;
 CHOOSE_DEF =
 |- (!n. CHOOSE n 0 = 1) /\
    (!k. CHOOSE 0(SUC k) = 0) /\
    (!n k. CHOOSE(SUC n)(SUC k) = (CHOOSE n(SUC k)) + (CHOOSE n k))

Two elementary properties of the binomial coefficients can now be proven by induction:

51

 CHOOSE_LESS = |- !n k. n < k ==> (CHOOSE n k = 0)
 CHOOSE_SAME = |- !n. CHOOSE n n = 1

8.3 Monoids, Groups and Commutative Rings

8.3.1 Associativity and Commutativity

An algebraic structure is a set equipped with some operators that obey some laws. An elementary example of such a structure is the pair (A, +), where A is a set and + is a binary operator on A that obeys the laws of associativity,

a + (b + c) = (a + b) + c

and commutativity,

a + b = b + a

How might these laws be represented in HOL? The simplest scheme is to deal with structures of the form (σ, +), where σ is a type of the HOL logic, and + is a HOL term of type σ → σ → σ. Notice that the set in the structure is represented as a HOL type: see the theory group presented in Elsa Gunter’s case study of Modular Arithmetic for a more sophisticated approach where the set in a structure can be a subset of a HOL type.

The two laws can be defined as two constants in HOL:

8.3. Monoids, Groups and Commutative Rings 91

52

#let ASSOCIATIVE =
#    new_definition (`ASSOCIATIVE`,
#      "!plus: *->*->*. ASSOCIATIVE plus =
#          (!a b c. plus a (plus b c) = plus (plus a b) c)");;
...
#let COMMUTATIVE =
#    new_definition (`COMMUTATIVE`,
#      "!plus: *->*->*. COMMUTATIVE plus =
#          (!a b. plus a b = plus b a)");;

By instantiating the type variable * and specialising the variable plus these constants are applicable to any particular structure of the form (σ, + : σ → σ → σ).

A simple example to illustrate this methodology is a permutation theorem about an arbitrary associative commutative operator (which is called PERM in file mk_BINOMIAL.ml). It is worthwhile going through the proof in detail because it illustrates how a difficulty in making use of

assumptions like ASSOCIATIVE plus and COMMUTATIVE plus can be solved.

53

#g "!plus: *->*->*.
#       ASSOCIATIVE plus /\ COMMUTATIVE plus ==>
#           !a b c. plus (plus a b) c = plus b (plus a c)";;

The first step is to strip off the quantifiers, and break up the implication:

54

#e (REPEAT STRIP_TAC);;
OK..
"plus(plus a b)c = plus b(plus a c)"
    [ "ASSOCIATIVE plus" ]
    [ "COMMUTATIVE plus" ]

The next step is to rewrite plus a b to plus b a on the left-hand side, from the assumption COMMUTATIVE plus. If the theorem was about a specific operator, such as $+: num->num->num from the theory of numbers in HOL, the rewriting could be done with REWRITE_TAC and the specific commutativity theorem, such as ADD_SYM:

|- !m n. m + n = n + m.

But in the general case all that is available is the definition of COMMUTATIVE plus which cannot be used directly with REWRITE_TAC to swap the terms a and b. One approach is first to prove the following equation from the definition COMMUTATIVE plus,

COMMUTATIVE plus |- !a b. plus a b = plus b a,

and then to use the equation with REWRITE_TAC in the same way as one might use ADD_SYM. This is a valid tactic because the assumption COMMUTATIVE plus is already present in the assumption list. A little forward proof achieves the first step, the derivation of the equation:

55

#top_print print_all_thm;;
- : (thm -> void)
#let forwards = fst(EQ_IMP_RULE (SPEC "plus: *->*->*" COMMUTATIVE));;
forwards = |- COMMUTATIVE plus ==> (!a b. plus a b = plus b a)
#let eqn = UNDISCH forwards;;
eqn = COMMUTATIVE plus |- !a b. plus a b = plus b a

This forward proof is a special case of a derived rule of the logic,

\frac{Γ ⊢ ∀x. t_{1} = t_{2}}{Γ, t_{1}[t′/x] ⊢ t_{2}[t′/x]}

which can be coded as the ML function SPEC_EQ:

56

 #let SPEC_EQ v th = UNDISCH(fst(EQ_IMP_RULE (SPEC v th)));;
 SPEC_EQ = - : (term -> thm -> thm)

Now the equation eqn can be used to prove swap terms a and b:

57

 #e(SUBST1_TAC (SPECL ["a:*";"b:*"] eqn));;
 OK..
 "plus(plus b a)c = plus b(plus a c)"
     [ "ASSOCIATIVE plus" ]
     [ "COMMUTATIVE plus" ]

Now that the terms appear in both sides in the same order but with different grouping, associativity can be used to make the grouping on both sides the same. Again the definition of ASSOCIATIVE cannot be used directly, but the derived rule SPEC_EQ obtains from the definition an equation analogous to eqn which can be used:

58

 #e(REWRITE_TAC [SPEC_EQ "plus: *->*->*" ASSOCIATIVE]);;
 OK..
 goal proved
 ...
 |- !plus.
     ASSOCIATIVE plus /\ COMMUTATIVE plus ==>
     (!a b c. plus(plus a b)c = plus b(plus a c))

The point of this example was to illustrate how to prove theorems about an arbitrary operator whose behaviour is specified by general predicates like ASSOCIATIVE and COMMUTATIVE. The main difficulty is in deriving equations for use with rewriting or substitution. The solution used in the example and extensively in the proof of the Binomial Theorem is to derive equations using the derived rule SPEC_EQ. Another derived rule, SPEC_IMP, is used extensively and is a variant

of SPEC_EQ:

\frac{Γ ⊢ ∀x. t_{1} ⇒ t_{2}}{Γ, t_{1}[t′/x] ⊢ t_{2}[t′/x]}

59

 #let SPEC_IMP v th = UNDISCH(SPEC v th);;
 SPEC_IMP = - : (term -> thm -> thm)

Two following two rules are versions of SPEC_EQ and SPEC_IMP generalised to take lists of variables rather than just one:

60

 SPECL_EQ = - : (term list -> thm -> thm)
 SPECL_IMP = - : (term list -> thm -> thm)

The final new derived rule used in the proof of the Binomial Theorem is STRIP_SPEC_IMP, a variant of SPEC_IMP, which splits up a conjunction in the antecedent into separate assumptions:

\frac{Γ ⊢ ∀x. (t_{1} ∧ ⋯ ∧ t_{n}) ⇒ t_{n+1}}{Γ, t_{1}[t′/x], …, t_{n}[t′/x] ⊢ t_{n+1}[t′/x]}

61

 #let STRIP_SPEC_IMP v th =
 #    UNDISCH_ALL(SPEC v (CONV_RULE (ONCE_DEPTH_CONV ANTE_CONJ_CONV) th));;
 STRIP_SPEC_IMP = - : (term -> thm -> thm)

There are other methods for proving theorems which are conditional on predicates such as ASSOCIATIVE and COMMUTATIVE. One is to rewrite with the definition before assuming the predicate (see, for instance, the proof of RIGHT_CANCELLATION in mk_BINOMIAL.ml). This method is fine for small proofs, but in larger proofs it presents the problem of how to specify a particular assumption on the assumption list. Another method is to put the predicates on the assumption list, and use resolution to extract the body of the definition (see the proof of UNIQUE_LEFT_INV). When the assumption list is not short this is rather a blunt instrument, in the sense that resolution can find many more theorems than the one desired, and is also rather computationally costly when compared to carefully constructing a theorem with SPEC_EQ and its variants.

8.3.2 Monoids

A monoid is a structure (M, +) where M is a set, + is an associative binary operator on M, such that there is an identity element, u ∈ M, which is a left and right identity of +, that is, it satisfies u + a = a + u = a for all a ∈ M. When the operator is written as +, the structure (M, +) is called an additive monoid and the identity element is written as 0; otherwise if the operator is written as ×, the structure (M, ×) is called a multiplicative monoid and the identity element is written as 1.

62

 #let RAW_MONOID =
 #    new_definition (`RAW_MONOID`,
 #      "!plus: *->*->*. MONOID plus =
 #          ASSOCIATIVE plus /\
 #          (?u. (!a. plus a u = a) /\ (!a. plus u a = a))");;

This definition is inconvenient to manipulate as it stands, because of the presence of the existential quantifier. However it is possible via Hilbert’s ϵ-operator to specify a function Id such that Id plus stands for an identity element of plus, if such exists. In fact it is easy to prove that the identity element in a monoid is unique. The first step is to prove that there exists a function Id with the property just described:

63

 ID_LEMMA =
 |- ?Id.
     !plus.
      (?u. (!a. plus u a = a) /\ (!a. plus a u = a)) ==>
      (!a. plus(Id plus)a = a) /\ (!a. plus a(Id plus) = a)

The proof of ID_LEMMA uses Hilbert’s ϵ-operator to construct a witness for the outer existential quantifier,

    \plus.@u:*.(!a:*. (plus u a = a)) /\ (!a. (plus a u = a))

Given ID_LEMMA, the constant Id is specified as follows:

64

 #let ID = new_specification `Id` [`constant`, `Id`] ID_LEMMA;;
 ID =
 |- !plus.
     (?u. (!a. plus u a = a) /\ (!a. plus a u = a)) ==>
     (!a. plus(Id plus)a = a) /\ (!a. plus a(Id plus) = a)

The condition that Id plus is a left and right identity is expressed by the predicates LEFT_ID and RIGHT_ID, respectively:

65

 LEFT_ID = |- !plus. LEFT_ID plus = (!a. plus(Id plus)a = a)
 RIGHT_ID = |- !plus. RIGHT_ID plus = (!a. plus a(Id plus) = a)

Given these abbreviations it is easy to prove in HOL that if a left and right identity element exists, then it is unique:

66

 UNIQUE_LEFT_ID =
 |- !plus.
     LEFT_ID plus /\ RIGHT_ID plus ==>
     (!l. (!a. plus l a = a) ==> (Id plus = l))
 UNIQUE_RIGHT_ID =
 |- !plus.
     LEFT_ID plus /\ RIGHT_ID plus ==>
     (!r. (!a. plus a r = a) ==> (Id plus = r))

The use of these last two theorems is to help identify the element Id plus for some specific plus, such as $+ from the theory of arithmetic. The abbreviations LEFT_ID and RIGHT_ID admit a new characterisation of the predicate MONOID, which is easier to manipulate in HOL

than RAW_MONOID:

67

 MONOID =
 |- !plus. MONOID plus = LEFT_ID plus /\ RIGHT_ID plus /\ ASSOCIATIVE plus

8.3.3 Groups

A group is a monoid in which every element is invertible.

68

 RAW_GROUP =
 |- !plus.
     Group plus =
     MONOID plus /\
     (!a. ?b. (plus b a = Id plus) /\ (plus a b = Id plus))

An alternative characterisation of Group^{2} which makes the existential quantification implicit can be had by specifying a function Inv so that, if Group plus holds, then the element Inv plus a is an inverse of a. The function Inv is specified in a way analogous to the specification of Id. First a lemma is proven which says there does exist a function Inv with the property desired:

2The mixed case identifier Group is used rather than GROUP, because the latter is already defined in Elsa Gunter’s theory group, a parent of her theory integer, which needs to coexist with the present theory so that integers can be used as an example ring (Section 8.6).

69

INV_LEMMA =
|- ?Inv.
    !plus.
     (!a. ?b. (plus b a = Id plus) /\ (plus a b = Id plus)) ==>
     (!a.
       (plus(Inv plus a)a = Id plus) /\ (plus a(Inv plus a) = Id plus))

Given this lemma, which is proven by an easy tactic almost the same as the one for ID_LEMMA, the constant Inv can be specified:

70

#let INV =
#    new_specification `Inv` [`constant`, `Inv`] INV_LEMMA;;

The predicates which say that Inv produces left and right inverses are defined as new constants:

71

LEFT_INV =
|- !plus. LEFT_INV plus = (!a. plus(Inv plus a)a = Id plus)
RIGHT_INV =
|- !plus. RIGHT_INV plus = (!a. plus a(Inv plus a) = Id plus)

Finally, the alternative characterisation of Group can be proven:

72

GROUP = |- Group plus = MONOID plus /\ LEFT_INV plus /\ RIGHT_INV plus

The theory of groups has been developed only as far as needed to prove the Binomial Theorem; Appendix 8.7 shows the one lemma, RIGHT_CANCELLATION, specifically about groups.

8.3.4 Rings

A ring is a structure (R, +, ×) such that structure (R, +) is a group, structure (R, ×) is a monoid, addition, +, is commutative, and multiplication, ×, distributes (on both sides) over addition. A commutative ring is a ring in which multiplication is commutative. The word ring is used in the remainder of this chapter and in the HOL code to mean a commutative ring:

73

RING =
|- !plus times.
    RING(plus,times) =
    Group plus /\
    COMMUTATIVE plus /\
    MONOID times /\
    COMMUTATIVE times /\
    LEFT_DISTRIB(plus,times) /\
    RIGHT_DISTRIB(plus,times)

LEFT_DISTRIB and RIGHT_DISTRIB are new constants defined by the theorems:

74

LEFT_DISTRIB =
|- !plus times.
    LEFT_DISTRIB(plus,times) =
    (!a b c. times a(plus b c) = plus(times a b)(times a c))
RIGHT_DISTRIB =
|- !plus times.
    RIGHT_DISTRIB(plus,times) =
    (!a b c. times(plus a b)c = plus(times a c)(times b c))

Notice that the definition of RING abbreviates a conjunction of predicates, some of which are atomic, in the sense that they are some basic property of plus or times or both, and some are compound, in the sense that they abbreviate a further conjunction of properties. The definition is a tree of predicates with atomic ones like LEFT_DISTRIB and ASSOCIATIVE, at the leaves, and compound ones like Group and MONOID, at the branches. Many theorems conditional on RING(plus,times) need to make use of both atomic and compound predicates contained in the tree. To make access to all these predicates easy, the following lemma is proven, which makes explicit all the predicates in the tree:

75

RING_LEMMA =
|- RING(plus,times) ==>
RING(plus,times) /\
Group plus /\
MONOID plus /\
LEFT_ID plus /\
RIGHT_ID plus /\
ASSOCIATIVE plus /\
LEFT_INV plus /\
RIGHT_INV plus /\
COMMUTATIVE plus /\
MONOID times /\
LEFT_ID times /\
RIGHT_ID times /\
ASSOCIATIVE times /\
COMMUTATIVE times /\
LEFT_DISTRIB(plus,times) /\
RIGHT_DISTRIB(plus,times)

Goals of the form,

!plus times. RING(plus,times) ==> ...

are consistently tackled with the following tactic, which uses RING_LEMMA to add all the atomic and compound predicates in the tree to the assumption list:

76

#let RING_TAC =
#    GEN_TAC THEN GEN_TAC THEN
#    DISCH_THEN (\th. STRIP_ASSUME_TAC (MP RING_LEMMA th));;

The one lemma about rings needed here, RING_0, is stated in Appendix 8.7.

8.4 Powers, Reductions, Ranges and Sums

The aim of this section is to explain how the mathematical notation ∑_{k=0}^{n} \binom{n}{k}a^{k}b^{n−k} can be rendered in HOL. If this is written out more explicitly than necessary for human consumption it looks like this:

∑_{k=0}^{n} \binom{n}{k} · (a^{k} × b^{n−k})

8.4. Powers, Reductions, Ranges and Sums 97

where × is multiplication in the ring, and where exponentiation and · stand for the scalar powers of multiplication and addition, respectively. Since binomial coefficients were treated in Section 8.2, what remain to be defined in this section are scalar powers and the Σ-notation. The latter is tackled in three steps: reduction of a list of monoid elements; generation of lists comprising subranges of natural numbers, [n, n + 1, …, n + k − 1]; and finally the reduction of a list of ring elements indexed by a subrange of the natural numbers.

8.4.1 Scalar powers in a monoid

If (M, +) and (M, ×) are additive and multiplicative monoids respectively, the scalar powers of addition and multiplication are defined informally by the following equations, where n > 0:

n · a = \overbrace{a + ⋯ + a}^{n}
a^{n} = \overbrace{a × ⋯ × a}^{n}

When n = 0, n · a = 0 and a^{n} = 1.

Scalar power is defined in HOL via the constant POWER which is defined by primitive recursion:

77

 POWER =
 |- (!plus a. POWER plus 0 a = Id plus) /\
    (!plus n a. POWER plus(SUC n)a = plus a(POWER plus n a))

Three lemmas about POWER are stated in Appendix 8.7.

8.4.2 Reduction in a monoid

This section makes use of the standard HOL theory of lists, in particular the constants NIL, CONS, APPEND and MAP, definition by primitive recursion and proof by induction. The theory of lists is described in DESCRIPTION.

If (M, +) is a monoid, then the reduction of a list [a_{1}, …, a_{n}], where each a_{i} is an element of M, is the sum,

a_{1} + ⋯ + a_{n},

or the monoid’s identity element if n = 0.

Reduction is represented in HOL by the constant REDUCE, with type,

REDUCE : (*->*->*) -> (*)list -> *

and which is defined by primitive recursion on lists on its second argument:

78

 #let REDUCE =
 #  new_list_rec_definition (`REDUCE`,
 #    "(!plus. (REDUCE plus NIL) = (Id plus):*) /\
 #     (!plus (a:*) as. REDUCE plus (CONS a as) = plus a (REDUCE plus as))");;
 REDUCE =
 |- (!plus. REDUCE plus[] = Id plus) /\
    (!plus a as. REDUCE plus(CONS a as) = plus a(REDUCE plus as))

Three lemmas about REDUCE are stated in Appendix 8.7.

8.4.3 Subranges of the natural numbers

The constant RANGE, which is a curried function of two numbers, is defined by primitive recursion so that,

RANGE m n = [m, m + 1, …, m + n − 1]

This definition means that the subrange is the first n numbers starting at m. In particular, when n = 0 the list is empty. Appendix 8.7 states two simple properties of RANGE

RANGE generates a subrange given its least element and length; an alternative method is to generate the subrange given its two endpoints, via a constant INTERVAL which satisfies the equation:

INTERVAL m n = \{ \begin{matrix}[m, m + 1, …, n] & if m ≤ n \\ [] & otherwise \end{matrix}

For comparison, the two methods are definable in HOL as follows:

79

 #let RANGE =
 #    new_recursive_definition false num_Axiom `RANGE`
 #      "(RANGE m 0 = NIL) /\
 #       (RANGE m (SUC n) = CONS m (RANGE (SUC m) n))";;
 #
 #let INTERVAL =
 #    new_recursive_definition false num_Axiom `INTERVAL`
 #      "(INTERVAL m 0 =
 #          (m > 0) => NIL | [0]) /\
 #      (INTERVAL m (SUC n) =
 #          (m > (SUC n)) => NIL | APPEND (INTERVAL m n) ([SUC n]))";;

8.4.4 Σ-notation

The standard Σ-notation is defined informally by the equation,

∑_{i=m}^{n} a_{i} = \{ \begin{matrix}a_{m} + a_{m+1} + ⋯ + a_{n} & if m ≤ n \\ 0 & otherwise \end{matrix}

Therefore the standard Σ-notation is naturally definable via a subrange generated by INTERVAL. An alternative notation, naturally definable via RANGE, can be defined informally as follows:

∑_{i=m}^{(n)} a_{i} = \{ \begin{matrix}a_{m} + a_{m+1} + ⋯ + a_{m+n−1} & if n > 0 \\ 0 & otherwise \end{matrix}

The brackets around the n above the Σ distinguish this notation from the standard one.

This second notation is used in the HOL proof of the Binomial Theorem. The difference between the two is just that the standard notation is definable via INTERVAL, and the second via RANGE. The second notation was chosen entirely because the constant RANGE is easier to manipulate in HOL than INTERVAL, which is because the latter has a more complex definition. The disadvantage of this choice is that the proof of the theorem uses a non-standard notation, but that’s all the difference is: notation. If desired, the Binomial Theorem stated in the standard notation could be trivially deduced from its non-standard statement.

The non-standard Σ-notation is defined in HOL as the following abbreviation:

8.5. The Binomial Theorem for a Commutative Ring 99

80

 #let SIGMA =
 #    new_definition (`SIGMA`,
 #      "SIGMA (plus,m,n) f = REDUCE plus (MAP f (RANGE m n)): *");;

Note that an indexed term a_{i} is represented in HOL as a function f of type num -> *.

Appendix 8.7 states several properties of SIGMA; their proofs make use of properties of MAP from the theory list, and also the lemmas about REDUCE and RANGE.

The functions REDUCE and RANGE are needed here only to define SIGMA, and in fact could be omitted if SIGMA were to be defined directly using primitive recursion. It is worth going to the trouble of defining REDUCE and RANGE, however, because they are likely to be useful in other situations.

8.5 The Binomial Theorem for a Commutative Ring

This section outlines the proof. For full details see the tactics in mk_BINOMIAL.ml.

The statement and proof of the Binomial Theorem use a new HOL constant, BINTERM, to abbreviate indexed terms of the form λk. \binom{n}{k}·a^{n−k} ×b^{k}. BINTERM is defined as a curried function as follows:

81

 #let BINTERM_DEF =
 #    new_definition (`BINTERM_DEF`,
 #      "BINTERM (plus: *->*->*) (times: *->*->*) a b n k =
 #          POWER plus (CHOOSE n k)
 #              (times (POWER times (n-k) a) (POWER times k b))");;

This abbreviation lets the Binomial Theorem be stated and proven in HOL as follows:

82

 BINOMIAL =
 |- !plus times.
     RING(plus,times) ==>
     (!a b n.
       POWER times n(plus a b) =
       SIGMA(plus,0,SUC n)(BINTERM plus times a b n))

In outline, the proof proceeds as follows. The following equation is proven by induction on n:

(a + b)^{n} = ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k}

When n = 0 both sides reduce to the multiplicative identity element, 1, of the ring. For the inductive step, the equation is assumed for n, and the following goal must be proven:

(a + b)^{n+1} = ∑_{k=0}^{(n+2)} \binom{n + 1}{k}a^{n+1−k}b^{k}

Three lemmas are used in the inductive step:

∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} = a × ∑_{k=1}^{(n)} \binom{n}{k}a^{n+1−k}b^{k} + b × ∑_{k=0}^{(n)} \binom{n}{k}a^{n+1−k}b^{k} (LEMMA 1)

a × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k} = a^{n+1} + a × ∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k}  (LEMMA 2)

b × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k} = b × ∑_{k=0}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b^{n+1}  (LEMMA 3)

LEMMA_1 is the key to the inductive step. The three stages of the inductive step are indicated (a),

(b) and (c) in ML comments. Step (a) expands the right-hand side of the goal with LEMMA_1:

rhs = a^{n+1} + a × ∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b × ∑_{k=0}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b^{n+1}

Step (b) expands the left-hand side with the induction hypothesis:

lhs = (a + b) ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k}

Finally, in step (c) the expansions of the two sides are shown to be the same, using distributivity of × over +, associativity of +, and LEMMA_2 and LEMMA_3:

lhs = a × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k} + b × ∑_{k=0}^{(n+1)} \binom{n}{k}a^{n−k}b^{k}

= a^{n+1} + a × ∑_{k=1}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b × ∑_{k=0}^{(n)} \binom{n + 1}{k}a^{n+1−k}b^{k} + b^{n+1}
= rhs

8.6 The Binomial Theorem for Integers

The previous sections have dealt with the material in theory BINOMIAL, concerning how to prove the Binomial Theorem for an arbitrary ring. A natural next step is to produce some specific commutative ring, and prove a Binomial Theorem for it, as an instance of the general case.

To see how to do so for Elsa Gunter’s theory of integers, take a look at the file mk BINOMIAL integer.ml, contained in directory Training/studies/binomial. When loaded into HOL, this ML file proves that the integers are a ring—by quoting laws contained in the theory integer—and then derives a Binomial Theorem for the integers—by Modus Ponens from the general theorem

BINOMIAL.

8.7 Principal lemmas

Binomial coefficients, CHOOSE:

8.7. Principal lemmas 101

83

CHOOSE_LESS = |- !n k. n < k ==> (CHOOSE n k = 0)
CHOOSE_SAME = |- !n. CHOOSE n n = 1

Algebraic laws:

84

RIGHT_CANCELLATION =
|- !plus. Group plus ==> (!a b c. (plus b a = plus c a) ==> (b = c))
RING_0 =
|- !plus times.
    RING(plus,times) ==>
    (!a. times(Id plus)a = Id plus) /\ (!a. times a(Id plus) = Id plus)

Scalar powers:

85

POWER_1 = |- !plus. MONOID plus ==> (POWER plus 1 a = a)
POWER_DISTRIB =
|- !plus times.
    RING(plus,times) ==>
    (!a b n. times a(POWER plus n b) = POWER plus n(times a b))
POWER_ADD =
|- !plus.
    MONOID plus ==>
    (!m n a. POWER plus(m + n)a = plus(POWER plus m a)(POWER plus n a))

Reduction of lists:

86

REDUCE_APPEND =
|- !plus.
    MONOID plus ==>
    (!as bs.
      REDUCE plus(APPEND as bs) = plus(REDUCE plus as)(REDUCE plus bs))
REDUCE_MAP_MULT =
|- !plus times.
    RING(plus,times) ==>
    (!a bs. REDUCE plus(MAP(times a)bs) = times a(REDUCE plus bs))
REDUCE_MAP =
|- !plus.
    MONOID plus /\ COMMUTATIVE plus ==>
    (!f g as.
      REDUCE plus(MAP(\k. plus(f k)(g k))as) =
      plus(REDUCE plus(MAP f as))(REDUCE plus(MAP g as)))

Subranges of the natural numbers:

87

RANGE_TOP = |- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]
RANGE_SHIFT = |- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)

8.7. Principal lemmas 103

Σ-notation:

88

SIGMA_ID = |- !plus m f. SIGMA(plus,m,0)f = Id plus
SIGMA_LEFT_SPLIT =
|- !plus m n f. SIGMA(plus,m,SUC n)f = plus(f m)(SIGMA(plus,SUC m,n)f)
SIGMA_RIGHT_SPLIT =
|- !plus.
    MONOID plus ==>
    (!m n f. SIGMA(plus,m,SUC n)f = plus(SIGMA(plus,m,n)f)(f(m + n)))
SIGMA_SHIFT =
|- !plus m n f. SIGMA(plus,SUC m,n)f = SIGMA(plus,m,n)(f o SUC)
SIGMA_MULT_COMM =
|- !plus times.
    RING(plus,times) ==>
    (!m n a f.
      times a(SIGMA(plus,m,n)f) = SIGMA(plus,m,n)((times a) o f))
SIGMA_PLUS_COMM =
|- !plus.
    MONOID plus /\ COMMUTATIVE plus ==>
    (!f g m n.
      plus(SIGMA(plus,m,n)f)(SIGMA(plus,m,n)g) =
      SIGMA(plus,m,n)(\k. plus(f k)(g k)))
SIGMA_EXT =
|- !plus.
    MONOID plus ==>
    (!f g m n.
      (!k. k < n ==> (f(m + k) = g(m + k))) ==>
      (SIGMA(plus,m,n)f = SIGMA(plus,m,n)g))

Terms from the Binomial Theorem:

89

BINTERM_0 =
|- !plus times.
    RING(plus,times) ==>
    (!a b n. BINTERM plus times a b n 0 = POWER times n a)
BINTERM_n =
|- !plus times.
    RING(plus,times) ==>
    (!a b n. BINTERM plus times a b n n = POWER times n b)

104 Chapter 8. Example: the Binomial Theorem

References

[1] S.F. Allen, R.L. Constable, D.J. Howe and W.E. Aitken, ‘The Semantics of Reflected Proof’, Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pp. 95–105, 1990.

[2] R.S. Boyer and J S. Moore, ‘Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures’, in: The Correctness Problem in Computer Science, edited by R.S. Boyer and J S. Moore, Academic Press, New York, 1981.

[3] A.J. Camilleri, T.F. Melham and M.J.C. Gordon, ‘Hardware Verification using Higher-Order Logic’, in: From HDL Descriptions to Guaranteed Correct Circuit Designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble, September 1986, edited by D. Borrione (North-Holland, 1987), pp. 43–67.

[4] M. Gordon, ‘Why higher-order Logic is a good formalism for specifying and verifying hardware’, in: Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh Workshop on VLSI , edited by G. Milne and P.A. Subrahmanyam (North-Holland, 1986), pp. 153–177.

[5] Donald. E. Knuth. The Art of Computer Programming. Volume 1/Fundamental Algorithms. Addison-Wesley, second edition, 1973.

[6] Saunders Mac Lane and Garrett Birkhoff. Algebra. Collier-MacMillan Limited, London, 1967.

[7] R. Milner, ‘A Theory of Type Polymorphism in Programming’, Journal of Computer and System Sciences, Vol. 17 (1978), pp. 348–375.

[8] George D. Mostow, Joseph H. Sampson, and Jean-Pierre Meyer. Fundamental Structures of Algebra. McGraw-Hill Book Company, 1963.

[9] L. Paulson, ‘A Higher-Order Implementation of Rewriting’, Science of Computer Programming, Vol. 3, (1983), pp. 119–149.

[10] L. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge Tracts in Theoretical Computer Science 2 (Cambridge University Press, 1987).

[11] R.E. Weyhrauch, ‘Prolegomena to a theory of mechanized formal reasoning’, Artificial Intelligence 3(1), 1980, pp. 133–170.

[12] A.N. Whitehead and B. Russell, Principia Mathematica, 3 volumes (Cambridge University Press, 1910–3).