Filter
Top Products
viii CONTENTS
5.2 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
5.3 Primitive inference rules . . . . . . . . . . . . . . . . . . . . . . . . . 52
5.4 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
5.5 Derived rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.6 Classical axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
6 Implementation in CAML 57
6.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
6.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
6.3 Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
6.4 Some predefined constants . . . . . . . . . . . . . . . . . . . . . . . . 62
7 Parsing and printing 65
7.1 Overloading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
8 Conversions 67
8.1 Conversionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
8.2 Depth conversions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
9 Derived rules 71
9.1 Logical rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
9.2 Rewriting and simplification . . . . . . . . . . . . . . . . . . . . . . . 74
9.3 Ordered rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
9.4 Higher order matching . . . . . . . . . . . . . . . . . . . . . . . . . . 77
9.5 Other rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
10 Tactics 81
10.1 The goalstack . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
10.2 Basic tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
10.3 Tacticals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
10.4 Dealing with assumptions . . . . . . . . . . . . . . . . . . . . . . . . 85
10.5 Model elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
11 Principles of definition 87
11.1 Inductive definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
11.2 Free recursive types . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
12 Mathematical theories 93
12.1 Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
12.2 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
12.3 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
12.4 Well-founded relations . . . . . . . . . . . . . . . . . . . . . . . . . . 96
12.5 Real numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
12.6 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
12.7 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
13 Examples 101
A Compatibility with other HOLs 103