Filter
Top Products
Contents
1 Introduction 1
1.1 What is HOL Light? . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Getting started . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Derived rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
I CAML tutorial 7
2 A taste of CAML 9
2.1 Imperative vs functional programming . . . . . . . . . . . . . . . . . 9
2.2 Basic use of CAML . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.3 Bindings and declarations . . . . . . . . . . . . . . . . . . . . . . . . 12
2.4 Evaluation rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.5 Types and polymorphism . . . . . . . . . . . . . . . . . . . . . . . . 15
2.6 Equality of functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3 Further CAML 19
3.1 Basic datatypes and operations . . . . . . . . . . . . . . . . . . . . . 20
3.2 Syntax of CAML phrases . . . . . . . . . . . . . . . . . . . . . . . . 22
3.3 Further examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.4 Type definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.4.1 Pattern matching . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.4.2 Recursive types . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.4.3 Tree structures . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.4.4 The subtlety of recursive types . . . . . . . . . . . . . . . . . 32
4 Effective CAML 35
4.1 Useful combinators . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.2 Writing efficient code . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.2.1 Tail recursion and accumulators . . . . . . . . . . . . . . . . 37
4.2.2 Minimizing consing . . . . . . . . . . . . . . . . . . . . . . . . 39
4.2.3 Forcing evaluation . . . . . . . . . . . . . . . . . . . . . . . . 41
4.3 Imperative features . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.3.1 Exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.3.2 References and arrays . . . . . . . . . . . . . . . . . . . . . . 43
4.3.3 Sequencing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.3.4 Interaction with the type system . . . . . . . . . . . . . . . . 45
II HOL tutorial 47
5 Primitive basis of HOL Light 49
5.1 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
vii