tutorial

[For HOL Kananaskis 1] June 17, 2002The HOL SystemTUTORIALPrefaceThis volume contains a tutorial on the HOL system. It is one of three documents makingup the documentation for HOL:(i) TUTORIAL: a tutorial introduction to HOL.(ii) DESCRIPTION: a description of higher order logic, the ML programming lan guage, 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 rst item read by new users of HOL.It provides a self-study introduction to the structure and use of the system. The tu torial is intended to give a ‘hands on’ feel for the way HOL is used, but it does notsystematically explain all the underlying principles (DESCRIPTION, explains these). Afterworking 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 startedChapter 1 explains how to get and install HOL. Once this is done, the potential HOL usershould become familiar with the following subjects:1. The programming meta language ML, and how to interact with it through an edi tor.2. The formal logic supported by the HOL system (higher order logic) and its manip ulation via ML.3. Forward proof and derived rules of inference.4. Goal directed proof, tactics and tacticals.iiiiv ...