The HOL Logic in ML

In this chapter, the concrete representation of the HOL logic is described. This involves describing the ML functions that comprise the interface to the logic (up to and including §Theorems); the quotation, parsing, and printing of logical types and terms §Quotations; the representation of theorems (§Theorems); the representation of theories (§Theories); the fundamental HOL theory bool (§bool); the primitive rules of inference (§Rules); and the methods for extending theories (throughout §Theories and also later in §bossLib). It is assumed that the reader is familiar with ML. If not, the introduction to ML in Getting Started with HOL in the TUTORIAL Part should be read first.

The HOL system provides the ML types hol_type and term which implement the types and terms of the HOL logic, as defined in §LOGIC. It also provides primitive ML functions for creating and manipulating values of these types. Upon this basis the HOL logic is implemented. The key idea of the HOL system, due to Robin Milner, and discussed in this chapter, is that theorems are represented as an abstract ML type whose only pre-defined values are axioms, and whose only operations are rules of inference. This means that the only way to construct theorems in HOL is to apply rules of inference to axioms or existing theorems; hence the consistency of the logic is preserved.

The purpose of the meta-language ML is to provide a programming environment in which to build theorem proving tools to assist in the construction of proofs. When the HOL system is built, a range of useful theorems is pre-proved and a set of tools pre-defined. The basic system thus offers a rich initial environment; users can further enrich it by implementing their own application specific tools and building their own application specific theories.

Types

The allowed types depend on which type constants have been declared in the current theory. See §Theories for details of how such declarations are made. There are two primitive constructor functions for values of type hol_type

    mk_vartype : string -> hol_type
    mk_thy_type :
      {Args: hol_type list, Thy: string, Tyop: string} -> hol_type

The function mk_vartype constructs a type variable with a given name; it gives a warning if the name is not an allowable type variable name (i.e., not an apostrophe (') followed by an alphanumeric). The function mk_thy_type constructs a compound type from a record {Tyop,Thy,Args} where Tyop is a string representing the name of the type operator, Thy is a string representing the theory that Tyop was declared in, and Args is a list of types representing the arguments to the operator. Function types $\sigma_1\to\sigma_2$ of the logic are represented in ML as though they were compound types $(\sigma_1,\sigma_2)$fun (in §LOGIC, however, function types were not regarded as compound types).

The evaluation of $$ \mathtt{mk\_thy\_type}\{\mathtt{Tyop} = \mathit{name},\, \mathtt{Thy} = \mathit{thyname},\, \mathtt{Args} = [\sigma_1, \cdots ,\sigma_n]\} $$ fails if

1. $\mathit{name}$ is not a type operator of theory $\mathit{thyname}$;
2. $\mathit{name}$ is a type operator of theory $\mathit{thyname}$, but its arity is not $n$;
3. $\mathit{thyname}$ is not the name of a theory in the current context.

For example, mk_thy_type{Tyop="bool", Thy="min", Args=[]} evaluates to an ML value of type hol_type representing the type bool.

Type constants may be bound to ML values and need not be repeatedly constructed: e.g., the type built by mk_thy_type{Tyop="bool", Thy="min", Args=[]} is abbreviated by the ML value bool. Similarly, function types may be constructed with the infix ML function -->. A few common type variables have been constructed and bound to ML identifers, e.g., alpha is the type variable 'a and beta is the type variable 'b. Thus the ML code alpha --> bool is equal to, but much more concise than

> mk_thy_type{Tyop="fun", Thy="min",
              Args=[mk_vartype "'a",
                    mk_thy_type{Tyop="bool", Thy="min", Args=[]}]}
val it = “:α -> bool”: hol_type

There are two primitive destructor functions for values of type hol_type:

    dest_vartype : hol_type -> string
    dest_thy_type :
      hol_type -> {Args: hol_type list, Thy: string, Tyop: string}

The function dest_vartype extracts the name of a type variable. A compound type is destructed by the function dest_thy_type into the name of the type operator, the name of the theory it was declared in, and a list of the argument types; dest_vartype and dest_thy_type are thus the inverses of mk_vartype and mk_thy_type, respectively. The destructors fail on arguments of the wrong form.

Terms

The four primitive kinds of terms of the logic are described in §LOGIC. The ML functions for manipulating these are described in this section. There are also derived terms that are described in §Derived Syntactic Forms.

At any time, the terms that may be constructed depends on which constants have been declared in the current theory. See §Theories for details of how such declarations are made.

There are four primitive constructor functions for values of type term:

    mk_var : string * hol_type -> term

mk_var($x$,$\sigma$) evaluates to a variable with name $x$ and type $\sigma$; it always succeeds.

    mk_thy_const :
      {Name: string, Thy: string, Ty: hol_type} -> term

mk_thy_const{Name =$\;\mathit{c}$,Thy =$\;\mathit{thyname}$,Ty =$\;\sigma$} evaluates to a term representing the constant with name $c$ and type $\sigma$; it fails if:

1. $c$ is not the name of a constant in the theory $\mathit{thyname}$;
2. $\sigma$ is not an instance of the generic type of $c$ (the generic type of a constant is established when the constant is defined; see §Theories).

    mk_comb : term * term -> term

mk_comb($t_1$,$t_2$) evaluates to a term representing the combination $t_1\ t_2$. It fails if:

1. the type of $t_1$ does not have the form $\sigma_1\to\sigma_2$;
2. the type of $t_1$ has the form $\sigma_1\to\sigma_2$, but the type of $t_2$ is not equal to $\sigma_1$.

    mk_abs : term * term -> term

mk_abs($x$,$t$) evaluates to a term representing the abstraction $\lambda x.\;t$; it fails if $x$ is not a variable.

There are four primitive destructor functions on terms:

    dest_var : term -> string * hol_type
    dest_thy_const :
      term -> {Name: string, Thy: string, Ty: hol_type}
    dest_comb : term -> term * term
    dest_abs : term -> term * term

These are the inverses of mk_var, mk_thy_const, mk_comb and mk_abs, respectively. They fail when applied to terms of the wrong form. Other useful destructor functions are rator, rand, bvar, body, lhs and rhs. See §REFERENCE for details.

The function

    type_of : term -> hol_type

returns the type of a term.

The function

    aconv : term -> term -> bool

implements the $\alpha$-convertibility test for $\lambda$-calculus terms. From the point of view of the HOL logic, $\alpha$-convertible terms are identical. A variety of other functions are available for performing $\beta$-reduction (beta_conv), $\eta$-reduction (eta_conv), substitution (subst), type instantiation (inst), computation of free variables (free_vars) and other common term operations. See §REFERENCE for more details.

Quotations, Parsing and Printing

It would be tedious to always have to input types and terms using the constructor functions. The HOL system, adapting the approach taken in LCF, has special quotation parsers for HOL types and terms which enable types and terms to be input using a fairly standard syntax. For example, the ML expression “:bool -> bool” denotes exactly the same value (of ML type hol_type) as

> mk_thy_type{
   Tyop = "fun",Thy = "min",
   Args = [
     mk_thy_type{Tyop = "bool", Thy = "min", Args = []},
     mk_thy_type{Tyop = "bool", Thy = "min", Args = []}
   ]}
val it = “:bool -> bool”: hol_type

and the expression “\x. x + 1” can be used instead of

> val numty = mk_thy_type{Tyop="num",Thy="num",Args=[]}
val numty = “:num”: hol_type
> val tedious = mk_abs
   (mk_var("x",numty),
    mk_comb(mk_comb (
      mk_thy_const {
        Name="+",Thy="arithmetic",Ty=numty --> numty --> numty
      },
      mk_var("x", numty)
      ),
      mk_comb(
        mk_thy_const{
          Name="NUMERAL", Thy="arithmetic", Ty=numty-->numty
        },
        mk_comb(
          mk_thy_const{
            Name="BIT1", Thy="arithmetic", Ty=numty-->numty
          },
          mk_thy_const{
            Name="ZERO", Thy="arithmetic", Ty=numty
          }))));
val tedious = “λx. x + 1”: term
> val parsed = ``\x. x + 1``;
val parsed = “λx. x + 1”: term
> aconv tedious parsed;
val it = true: bool

The HOL printer, which is integrated into the ML toplevel loop, also outputs types and terms using this syntax. Types are printed in the form “:$\mathit{type}$”. For example, the ML value of type hol_type representing $\alpha\to(\mathtt{ind}\to\mathtt{bool})$ would be printed out as below:

> let
    val ind_ty = mk_thy_type{Tyop="ind", Thy="min", Args=[]}
  in
    alpha --> (ind --> bool)
  end;
val it = “:α -> ind -> bool”: hol_type

Similarly, terms are printed in the form “$\mathit{term}$”, as in the session above printing the term “$\lambda$x. x + 1”. The leading colon is used to distinguish a type quotation from a term quotation: the former have the form “:$\cdots$” and the latter have the form “$\cdots$”.

Lexical Matters

The name of a HOL variable can be any ML string, but the quotation mechanism will parse only names that are identifiers (see §Identifiers below). Using non-identifiers as variable names is discouraged except in special circumstances (for example, when writing derived rules that generate variables with names that are guaranteed to be different from existing names). The name of a type variable in the HOL logic is formed by a prime/apostophe (') followed by an alphanumeric which itself contains no prime (see §Type Variable Names for examples). The name of a type constant or a term constant in the HOL logic can be any identifier, although some names are treated specially by the HOL parser and printer and should therefore be avoided.

Identifiers

In addition to special forms already present in the relevant grammar, a HOL identifier can be of two forms:

1. A finite sequence of alphanumerics starting with a letter. The underscore character is considered a digit character, and so can occur after an identifier's first letter. Greek characters (roughly Unicode range U+0370 to U+03FF) are also letters, except for $\lambda$~(U+03BB), which is treated as a symbol. HOL is case-sensitive: upper and lower case letters are considered to be different.

   Digits are the ASCII characters 0–9, the underscore character, and the Unicode subscripts and superscripts. The apostrophe character is special: it is not a letter, but can appear as part of an alphanumeric term identifier after the first letter. It must appear at the start of a type variable's name, and can also appear in the term context as a sequence of apostrophes on their own.

2. A symbolic identifier, i.e., a finite sequence formed by any combination of the ASCII symbols and the Unicode symbols. The basic ASCII symbols are

     #  ?  +  *  /  \  =  <  >  &  %  @  !  :  |  -  ^  `
   

   Use of the caret and back-tick characters is complicated by the fact that these characters have special meaning in the quotation mechanism; see §Quotations and Antiquotations. The dollar-sign ($) can also be used to form symbolic identifiers, but only in tokens where it is the only symbol. Thus, $, $$, and $$$ will all lex as identifiers.

   This restriction arises because of the other uses to which the dollar sign is put:

   • The dollar can be used as an escaping mechanism to remove special syntactic treatment of other identifiers. Thus, $+ and $if are effectively special forms of the tokens + and if respectively.
   • Finally, the dollar can also be used as a namespace separator character, giving unambiguous “long form” identifiers. For example, the token bool$COND is an unambiguous way of writing the COND constant from theory segment bool.

   The ASCII grouping symbols (braces, brackets, and parentheses), and the tilde (~), full-stop (.), comma (,), semi-colon (;) and hyphen (-) characters are called non-aggregating characters. Unless the desired token is already present in the grammar, these characters do not combine with themselves or other symbolic characters. Thus, the string "((" is viewed as two tokens, as are +; and "-+".

   Unicode code characters that are not letters or digits are regarded as symbolic. The non-aggregating Unicode characters are listed in the table below:

Table: Non-aggregating Unicode characters

3. A number is a string of one or more digits. If not the initial digit, an underscore can be used within the sequence to provide spacing. In order to distinguish different types of numbers a single character suffix may be used: for example 3n is a natural number while 3i is an integer. The 0x and 0b prefixes may also be used to change the base of the number. If the 0x prefix is used, hexadecimal ‘digits’ a–f and A–F can also be used. See also §Numerals.

Separators

The separators used by the HOL lexical analyser are (with ASCII codes in brackets):

space (32), carriage return (13), line feed (10), tab (^I, 9), form feed (^L, 12)

Special identifiers

The following valid identifiers are used by the grammar in the theory of booleans, and thus in all descendant theories as well. They should not be used as the name of a variable or a constant unless the user is very confident of their ability to mess with grammars.

   let  in  and  \  .  ;  =>  |  :  :=  with  updated_by  case  of

Type variable names

The name of a type variable in the HOL logic is a string beginning with a prime (') followed by an alphanumeric which itself contains no prime; for example all of the following are valid type variable names except for the last:

   'a   'b   'cat   'A11   'g_a_p   'f'oo

User tokens

In general, a HOL user has a great deal of freedom to create their own syntax, involving special tokens quite apart from variables and names for constants. For example, the if-then-else syntax for the conditional operator has special tokens (the “if”, “then” and “else”) that are not names for variables, nor constants (the underlying constant is actually called COND). In order to make sure that the operations of printing and parsing tokens are suitably inverse to each other, users should not create tokens that include whitespace, or the comment strings ((* and *)).

Literals

There are two classes of literal in HOL's term syntax: numbers and strings (which latter also includes a treatment of character literals). String literals are a convenient way to write large terms of type :char list; numerals are a convenient way to write values of type :num. In addition, both string and numeric literals can be injected into other types, so that, for example, it is possible to write 23 and have the system see it as a rational number. For more on these syntaxes, see §Numerals and §Strings.

Unicode vs ASCII

As the definition of parsed in the session above suggests, there are ASCII alternatives to the Unicode syntax. To repeat that definition:

> val parsed = ``\x. x + 1``;
val parsed = “λx. x + 1”: term

The backslash can be used instead of $\lambda$, and the `` symbol can be used instead of both the “ and ” symbols. Similarly, the logical connectives have both ASCII and Unicode forms (see §Grammar below), and either can be used (even within the same term), except that the begin- and end-delimiters must be of the same type. Usually the system prefers to print its output with the Unicode symbols. Thus:

> val t1 = ``!x y. x < y ==> ?z. x + z = y``;
val t1 = “∀x y. x < y ⇒ ∃z. x + z = y”: term

> val t2 = “∀x. ∃y. x < y ∧ y < x + 1”;
val t2 = “∀x. ∃y. x < y ∧ y < x + 1”: term

> val t3 = ``!x. ∃y. x < y /\ y < x + 1``;
val t3 = “∀x. ∃y. x < y ∧ y < x + 1”: term

§Parsing and Printing has more detailed information about the capabilities of the term and type parsing and printing facilities in the system. The remainder of this section provides a brief overview of what is possible.

Type Inference

Notice that there is no explicit type information in \x.x+1. The HOL type checker knows that 1 has type :num and + has type :num->(num->num). From this information it can infer that both occurrences of x in \x. x+1 could have type :num. This is not the only possible type assignment; for example, the first occurrence of x could have type bool and the second one have type :num. In that case there would be two different variables with name x, namely x$_{\mathtt{bool}}$ and x$_{\mathtt{num}}$, the second of which is free. However, the only way to construct a term with this second type assignment is by using the ML API, since the type checker uses the heuristic that all variables in a term with the same name have the same type. This is illustrated in the following session.

> ``x = (x = 1)``;
Exception- HOL_ERR
  (at Preterm.type-analysis: on line 1, characters 7-11:
       
Type error in function application.
  Function: $= x :num -> bool
  Argument: x = 1 :bool
  Reason: Attempt to unify different type operators: num$num a...
) raised

The desired value can be directly constructed by the primitive constructor functions:

> mk_eq
  (mk_var("x",bool),
   mk_eq(mk_var("x",numty),
         numSyntax.mk_numeral (Arbnum.fromString "1")));
val it = “x ⇔ x = 1”: term

The original quotation type checker was designed and implemented by Robin Milner. It employs heuristics like the one above to infer a sensible type for all variables occurring in a term.

At times, the user may want to control the exact type of a subterm. To support such functionality, types can be explicitly indicated by following any subterm with a colon and then a type. For example, “f(x:num):bool” will type check with f and x getting types :num->bool and :num respectively. This treatment of types within quotations is inherited from LCF.

Parentheses and Precedence

As with programming languages, the grammar governing the parsing of terms and types includes a notion of precedence. As with standard mathematics, for example, if we write 2 + 3 * 6, we expect this to denote the abstract syntax tree that groups the 3 and 6 together, giving a value of 20 for the term. Again as is usual, to adjust parses in the face of precedence one can use parentheses:

> EVAL “2 + 3 * 6”;
val it = ⊢ 2 + 3 * 6 = 20: thm

> EVAL “(2 + 3) * 6”;
val it = ⊢ (2 + 3) * 6 = 30: thm

Function application can be seen as an invisible high-precedence (or “tightly binding”) infix operator so that f x + 6 is an addition term, with the application of f to x being added to 6. This makes HOL syntax more like functional programming: one typically doesn't bother to write f(x) because f x suffices. Of course, sometimes arguments do need parentheses. For example, f(x + 6).

Finally, drawing inspiration from the Haskell programming language, HOL also supports the dollar-sign as a low precedence function application symbol. In this way, one has an option that can result in needing to write fewer parentheses:

> EVAL “FACT $ SUC $ 2 + 3”;
val it = ⊢ FACT (SUC (2 + 3)) = 720: thm

Note that, as above, the pretty-printer will always print terms with the “invisible” function application symbol and parentheses as necessary, even if they were input with dollar-signs.

Viewing the Grammar

The behaviour of the HOL quotation parser and printer is determined by the current grammar. Thus, a familiarity with the basic vocabulary of the standard collection of HOL theories is important if one is to use HOL effectively. One can examine the current grammar used by the parser with the functions type_grammar and term_grammar.

For example, in the following session, we see that the type grammar used in the startup context of HOL has the type operators fun, sum, prod, list, recspace, num, option, one, cv, ind, and bool:

> type_grammar();
val it =
   Rules:
     (50)   TY  ::=  TY -> TY [fun] (R-associative)
     (60)   TY  ::=  TY + TY [sum] (R-associative)
     (70)   TY  ::=  TY # TY [prod] (R-associative)
            TY  ::=  bool | cv | (TY, TY) fun | ind | TY itself |
                     TY list | num | one | TY option |
                     (TY, TY) prod | TY recspace | TY set |
                     (TY, TY) sum | unit
            TY  ::=  TY[TY] (array type)
   Type abbreviations:
     bool             = min$bool              
     cv               = cv$cv                 
     (α, β) fun       = (α, β) min$fun        
     ind              = min$ind               
     α itself         = α bool$itself         
     α list           = α list$list           
     num              = num$num               
     one              = one$one                [not printed]
     α option         = α option$option       
     (α, β) prod      = (α, β) pair$prod      
     α recspace       = α ind_type$recspace   
     α set            = (α, min$bool) min$fun  [not printed]
     (α, β) sum       = (α, β) sum$sum        
     unit             = one$one               :
   type_grammar.grammar

Also, fun, sum, and prod have infix notation (->), (+), and (#), respectively, with different binding strengths: # (with 70) binds stronger than + (60), which binds stronger than -> (50). All postfix type operators bind more strongly than the infixes.

The next session shows the (abbreviated) output from invoking the term_grammar function in the startup HOL environment. The deleted output includes more rules, a listing of all constants known to the system, including prefix operators, and a list of all overloadings currrently in force. The grammar rules shown include precedence levels, concrete syntax, and how various forms map to actual names (e.g., if-then-else maps to the name COND, and ⇒ maps to actual name ==>).

> term_grammar();
[...Lines elided...]
                | TM "|->" TM  [  combinpp.leftarrow]
                | TM "⇎" TM  [<=/=>] | TM "<=/=>" TM  
                | TM "⇔" TM  [<=>] | TM "<=>" TM  
                    (non-associative)
   (200)  TM  ::= TM "⇨ᵣ" TM  [suspendimp] | TM "⇒" TM  [==>]
                | TM "==>" TM  
                    (R-associative)
   (300)  TM  ::= TM "∨" TM  [\/] | TM "\/" TM     (R-associative)
   (310)  TM  ::= TM ":>" TM     (L-associative)
   (320)  TM  ::= TM "=+" TM  [UPDATE]   (non-associative)
   (400)  TM  ::= TM "⅋ᵣ" TM  [resconj] | TM "∧" TM  [/\]
                | TM "/\" TM  
                    (R-associative)
   (425)  TM  ::= TM "refines" TM   | TM "partitions" TM  
                | TM "equiv_on" TM   | TM "∉" TM  [NOTIN]
                | TM "NOTIN" TM   | TM "∈" TM  [IN] | TM "IN" TM  
                    (non-associative)
   (450)  TM  ::= TM "≼" TM  [<<=] | TM "<<=" TM  
                | TM "PERMUTES" TM   | TM "HAS_SIZE" TM  
                | TM "⊂" TM  [PSUBSET] | TM "PSUBSET" TM  
                | TM "⊆" TM  [SUBSET] | TM "SUBSET" TM  
                | TM "≥" TM  [>=] | TM ">=" TM   | TM "≤" TM  [<=]
                | TM "<=" TM   | TM ">" TM   | TM "<" TM  
                | TM "⊆ᵣ" TM  [RSUBSET] | TM "RSUBSET" TM  
                | TM "≠" TM   | TM "<>" TM   | TM "=" TM  
[...Output elided...]

Namespace control

In order to provide convenience, the parser deals with overloading and ambiguity. Overloading of numeric literals is discussed in §Overloading of Arithmetic Operators, although any symbol may be overloaded, not just numerals. At times such flexibility is quite useful; however, it can happen that one wishes to explicitly designate a particular constant. In that case, the notation $\mathit{thy}$$$\mathit{const}$ may be used in the parser to designate the constant $\mathit{const}$ declared in theory $\mathit{thy}$. In the following example, the less-than operator is explicitly specified.

> “prim_rec$< x y”;
val it = “x < y”: term

Note how the < symbol is not treated as an infix by the parser when given in “fully-qualified” form. Syntactically, such tokens are never given special treatment by the parser of HOL's concrete syntax.

Ways to Construct Types and Terms

The table below shows ML expressions for various kinds of type quotations. The expressions in the same row are equivalent.

Table: Building Types via Quotations or ML

Equivalent ways of inputting the four primitive kinds of term are shown in the next table.

Table: Building Primitive Terms

The following shows a few of these in action:

> val c = mk_const("CONS",
                   mk_vartype("'a") -->
                   mk_type("list", [mk_vartype("'a")]) -->
                   “:'a list”)
val c = “CONS”: term

> dest_thy_const c;
val it = {Name = "CONS", Thy = "list", Ty = “:α -> α list -> α list”}:
   {Name: string, Thy: string, Ty: hol_type}

In addition to the kinds of terms in the tables above, the parser also supports the following syntactic abbreviations.

Table: Syntactic abbreviations

Theorems

In §LOGIC, the notion of deduction was introduced in terms of sequents, where a sequent is a pair whose second component is a formula being asserted (a conclusion), and whose first component is a set of formulas (hypotheses). Based on this was the notion of a deductive system: a set of pairs, whose second component is a sequent, and whose first component is a list of sequents. The concept of a sequent following from a list of sequents via a deductive system was then defined: a sequent follows from a list of sequents if the sequent is the last element of some chain of sequents, each of whose elements is either in the list, or itself follows from the list along with earlier elements of the chain, via the deductive system.

A notation for `follows from' was then introduced. That a sequent $(\{t_1,\dots,t_n\},\ t)$ follows from a set of sequents $\Delta$, via a deductive system 𝒟, is denoted by: $t_1,\dots,t_n\vdash_{𝒟,\Delta} t$. (It was noted that where either 𝒟 or Δ were clear by context, their mention could be omitted; and where the set of hypotheses was empty, its mention could be omitted.)

A sequent that follows from the empty set of sequents via a deductive system is called a \textit{theorem} of that deductive system. That is, a theorem is the last element of a proof (in the sense of §LOGIC) from the empty set of sequents. When a pair $(L,(Γ,t))$ belongs to a deductive system, and the list $L$ is empty, then the sequent $(\Gamma,t)$ is called an axiom. Any pair $(L,(Γ,t))$ belonging to a deductive system is called a primitive inference of the system, with hypotheses¹ $L$ and conclusion $(Γ,t)$.

A formula in the abstract is represented concretely in HOL by a term whose HOL type is :bool. Therefore, a term of type :bool is used to represent a member of the set of hypotheses of a sequent; and likewise to represent the conclusion of a sequent. Sets in this context are represented by an implementation of the ML signature HOLset supporting operations such as member and union.

A theorem in the abstract is represented concretely in the HOL system by a value with the ML abstract type thm. The type thm has a destructor function

    dest_thm : thm -> term list * term

which returns a pair consisting of a list of the hypotheses and the conclusion, respectively, of a theorem. The order of assumptions in the list should not be relied on. Using dest_thm, two further destructor functions are derived:

    hyp : thm -> term list
    concl : thm -> term

\noindent for extracting the hypothesis list and the conclusion, respectively, of a theorem. A theorem's hypotheses are also available in the set form with the function

    hypset : thm -> term set

The ML type thm does not have a primitive constructor function. In this way, the ML type system protects the HOL logic from the arbitrary and unrecorded construction of theorems, which would compromise the consistency of the logic. (Functions which return theorems as values, e.g., functions representing primitive inferences, are discussed in §Primitive Rules.)

It was mentioned in §LOGIC that the deductive system of HOL includes four axioms.² In that manual, the axioms were presented in abstract form. Concretely, axioms are just theorem values that are introduced through the use of the ML function new_axiom (see §Theory Operations below). For example, the axiom BOOL_CASES_AX mentioned in §LOGIC is printed in HOL as follows (where T and F are the HOL logic's constants representing truth and falsity, respectively):

> BOOL_CASES_AX;
val it = ⊢ ∀t. (t ⇔ T) ∨ (t ⇔ F): thm

Note the special print format, with the $\vdash$ notation used to indicate ML type thm status; as well as the absence of HOL quotation marks in the ML context.

The session below illustrates the use of the destructor functions:

> hyp BOOL_CASES_AX;
val it = []: term list

> concl BOOL_CASES_AX;
val it = “∀t. (t ⇔ T) ∨ (t ⇔ F)”: term

> type_of it;
val it = “:bool”: hol_type

In addition to the print conventions mentioned above, the printing of theorems prints hypotheses as periods (i.e., full stops or dots). The flag show_assums allows theorems to be printed with hypotheses shown in full. These points are illustrated with a theorem inferred, for example purposes, from another axiom mentioned in §LOGIC, SELECT_AX.

> val th = UNDISCH (SPEC_ALL SELECT_AX);
val th =  [.] ⊢ P ($@ P): thm

> show_assums := true;
val it = (): unit

> th;
val it =  [P x] ⊢ P ($@ P): thm

Primitive Rules of Inference of the HOL Logic

The primitive rules of inference of the logic were described abstractly in §LOGIC. The descriptions relied on meta-variables $t$, $t_1$, $t_2$, and so on. In the HOL logic, infinite families of primitive inferences are grouped together and thought of as single primitive inference schemes. Each family contains all the concrete instances of one particular inference ‘pattern’. These can be produced, in abstract form, by instantiating the meta-variables in LOGIC’s rules to concrete terms.

In HOL, primitive inference schemes are represented by ML functions that return theorems as values. That is, for particular HOL terms, the ML functions return the instance of the theorem at those terms. The ML functions are part of the ML abstract type thm: although thm has no primitive constructors, it has (eight) operations which return theorems as values: ASSUME, REFL, BETA_CONV, SUBST, ABS, INST_TYPE, DISCH and MP.

The ML functions that implement the primitive inference schemes in the HOL system are described below. The same notation is used here as in §LOGIC: hypotheses above a horizontal line and conclusion beneath. The machine-readable ASCII notation is used for the logical constants.

Assumption Introduction

    ASSUME : term -> thm

    ------------
       t |- t

ASSUME “$t$” evaluates to $t$ |- $t$. Failure occurs if $t$ is not of type bool.

Reflexivity

    REFL : term -> thm

    --------------
       |- t = t

REFL “$t$” evaluates to |- $t = t$. A call to REFL never fails.

Beta-Conversion

    BETA_CONV : term -> thm

    -----------------------------
       |- (λx. t₁)t₂ = t₁[t₂/x]

• where $t_1$[$t_2$/$x$] denotes the result of substituting $t_2$ for $x$ in $t_1$, with suitable renaming of variables to prevent free variables in $t_2$ becoming bound after substitution. The substitution $t_1[t_2/x]$ is always defined.

BETA_CONV “$(\lambda x.\;t_1)t_2$” evaluates to the theorem |- $(\lambda x.\;t_1)t_2 = t_1[t_2/x]$. Failure occurs if the argument to BETA_CONV is not a $\beta$-redex (i.e., is not of the form $(\lambda x.\;t_1)t_2$).

Substitution

    SUBST : (term,thm)Lib.subst -> term -> thm -> thm

       Γ₁ |- t1 = t1'   ...  Γₙ |- tn = tn'   Γ |- t[t1,...,tn]
    --------------------------------------------------------------
                Γ₁ ∪ ... ∪ Γₙ ∪ Γ |- t[t1',...tn']

• where $t[t_1,\ldots,t_n]$ denotes a term $t$ with some free occurrences of the terms $t_1$, $\dots$, $t_n$ singled out and $t[t'_1,\ldots,t'_n]$ denotes the result of simultaneously replacing each such occurrences of $t_i$ by $t'_i$ (for $1{\leq}i {\leq} n$), with suitable renaming of variables to prevent free variables in $t_i'$ becoming bound after substitution.

The first argument to SUBST is a list of what are effectively pairs in the widely used (τ₁,τ₂)Lib.subst ML type. Each element in these lists is a record of type {redex:τ₁,residue:τ₂} with the intention that the redex value is to be replaced by the residue value. Such values can be constructed with the infix arrow |->, so that, for example:

> 3 |-> "foo";
val it = {redex = 3, residue = "foo"}: {redex: int, residue: string}

In SUBST, the redex values are variables $x_i$ and the theorems are $\Gamma_i\vdash t_i = t'_i$. The second argument is a template term $t[x_1,\ldots,x_n]$ in which occurrences of the variable $x_i$ (where $1 \leq i\leq n$) are used to mark the places where substitutions with $\Gamma_i \vdash t_i = t'_i$ are to be done. Thus

  SUBST [“x1” |-> (Γ₁ |- t1 = t1'), ..., “xn” |-> (Γₙ |- tn = tn')]
        t[x1,...xn]
        (Γ |- t[t1,...tn])

returns ∪ᵢΓᵢ ∪ Γ|- t[t1',...,tn']. Failure occurs if:

1. any of the arguments are of the wrong form;
2. the type of $x_i$ is not equal to the type of $t_i$ for some $1\leq i\leq n$.

The following is a somewhat contrived example of using SUBST:

> val th1 = EVAL “1 + 1”;
val th1 = ⊢ 1 + 1 = 2: thm
> val th2 = EVAL “2 * 3”;
val th2 = ⊢ 2 * 3 = 6: thm

> val template = “x + y + x = 10”;
val template = “x + y + x = 10”: term

> val th = EVAL “(1 + 1) + (2 * 3) + (1 + 1)”
val th = ⊢ 1 + 1 + 2 * 3 + (1 + 1) = 10: thm

> val result = SUBST [“x:num” |-> th1, “y:num” |-> th2] template th
val result = ⊢ 2 + 6 + 2 = 10: thm

Abstraction

    ABS : term -> thm -> thm

          Γ |- t1 = t2
    --------------------------
      Γ |- (λx. t1) = (λx. t2)

• where x is not free in Γ.

ABS “x” (Γ |- t1 = t2) returns the theorem Γ |- (λx. t1) = (λx. t2). Failure occurs if x is not a variable, or x occurs free in any assumption in Γ.

Type Instantiation

    INST_TYPE : (hol_type, hol_type) Lib.subst -> thm -> thm

                          Γ |- t
    ---------------------------------------------------
      Γ[σ₁,...,σₙ/α₁,...,αₙ] |- t[σ₁,...,σₙ/α₁,...,αₙ]

• where $t[\sigma_1,\dots,\sigma_n/\alpha_1,\dots,\alpha_n]$ denotes the result of substituting (in parallel) the types $\sigma_1$ to $\sigma_n$ for the type variables $\alpha_1$ to $\alpha_n$ in term $t$. Similarly, $\Gamma[\sigma_1,\dots,\sigma_n/\alpha_1,\dots,\alpha_n]$ denotes the result of performing the same substitution to all of the hypotheses in the set $\Gamma$.

INST_TYPE[α₁ |-> σ₁,...,αₙ |-> σₙ] th returns the result of instantiating each occurrence of αᵢ in the theorem th to σᵢ (for $1 \leq \mathtt{i} \leq n$). Failure occurs if an αᵢ is not a type variable.

For example:

> show_types := true;
val it = (): unit
> INST_TYPE [“:α” |-> “:num”] listTheory.LENGTH;
val it =
   ⊢ LENGTH ([] :num list) = (0 :num) ∧
     ∀(h :num) (t :num list). LENGTH (h::t) = SUC (LENGTH t): thm

Discharging an Assumption

    DISCH : term -> thm -> thm

          Γ |- t₂
    ------------------------
      Γ - {t₁} |- t₁ ⇒ t₂

• Γ - {t₁} denotes the set obtained by removing t₁ from Γ (note that t₁ need not occur in Γ; in this case Γ - t₁ = Γ).

DISCH t₁ (Γ |- t₂) evaluates to the theorem Γ - {t₁} |- t₁ ⇒ t₂. DISCH fails if the term given as its first argument is not of type :bool.

Modus Ponens

    MP : thm -> thm -> thm

       Γ₁ |- t₁ ⇒ t₂       Γ₂ |- t₁
    ---------------------------------
          Γ₁ ∪ Γ₂ |- t₂

MP takes two theorems (in the order shown above) and returns the result of applying Modus Ponens; it fails if the arguments are not of the right form.

Oracles

HOL extends the LCF tradition by allowing the use of an oracle mechanism, enabling arbitrary formulas to become elements of the thm type. By use of this mechanism, HOL can utilize the results of arbitrary proof procedures. In spite of such liberalness, one can still make strong assertions about the security of ML objects of type thm.

To avoid unsoundness, a tag is attached to any theorem coming from an oracle. This tag is propagated through every inference that the theorem participates in (much as ordinary assumptions are propagated in the inference rule MP). If it happens that falsity becomes derived, the offending oracle can be found by examining the tags component of the theorem. A theorem proved without use of any oracle will have an empty tag, and can thus be considered to have been proved solely by deductive steps in the HOL logic.

A tagged theorem can be created via

    mk_oracle_thm : string -> term list * term -> thm

which directly creates the requested theorem and attaches the given tag to it. The tag is created with a call to

    read : string -> tag

As well as providing principled access to the results of external reasoners, tags are used to implement some useful ‘system’ operations on theorems. For example, one can directly create a theorem via the function mk_thm. The tag MK_THM gets attached to each theorem created with this call. This allows users to directly create useful theorems, e.g., to use as test data for derived rules of inference. Another tag is used to implement so-called ‘validity checking’ for tactics.

The tags in a theorem can be viewed by setting Globals.show_tags to true.

> Globals.show_tags := true;
val it = (): unit

> mk_thm([], Term `F`);
val it = [oracles: MK_THM] [axioms: ] [] ⊢ F: thm

There are three elements to the left of the turnstile in the fully printed representation of a theorem: the first two³ comprise the tags component and the third is the standard assumption list. The tag component of a theorem can be extracted by

    tag : thm -> tag

and pretty-printed by

    pp_tag : tag -> pretty

Theories

In §LOGIC a theory is described as a $4$-tuple

$$𝒯 = \langle \mathsf{Struc}_𝒯, \mathsf{Sig}_𝒯, \mathsf{Axioms}_𝒯, \mathsf{Theorems}_𝒯\rangle $$

where

1. $\mathsf{Struc}_𝒯$ is the type structure of 𝒯;
2. $\mathsf{Sig}_𝒯$ is the signature of 𝒯;
3. $\mathsf{Axioms}_𝒯$ is the set of axioms of 𝒯;
4. $\mathsf{Theorems}_𝒯$ is the set of theorems of 𝒯.

In the implementation of HOL, theories are structured hierarchically to represent sequences of extensions called segments of an initial theory called min. A theory segment is not really a logical concept, but rather a means of representing theories in the HOL system. Each segment records some types, constants, axioms and theorems, together with pointers to other segments called its parents. The theory represented by a segment is obtained by taking the union of all the types, constants, axioms and theorems in the segment, together with the types, constants, axioms and theorems in all the segments reachable by following pointers to parents. This collection of reachable segments is called the ancestry of the segment.

ML functions for theory operations

A typical piece of work with the HOL system consists in a number of sessions. In the first of these, a new theory, 𝒯 say, is created by importing some existing theory segments, making a number of definitions, and perhaps proving and storing some theorems in the current segment. Then the current segment (named $\mathit{name}$ say) is exported. The concrete result will be an ML module $\mathsf{name}$Theory whose contents is the current theory segment created during the session and whose ancestry represents the desired logical theory 𝒯. Subsequent work sessions can access the definitions and theorems of 𝒯 by importing $name$Theory; this avoids having to load the tools and replay the proofs that created $name$Theory in the first place.

The naming of data in theories is based on the names given to segments. Specifically an axiom, definition, specification or theorem is accessed by an ML long identifier $\mathit{thy}$Theory.$\mathit{name}$, where $\mathit{thy}$ is the name of the theory segment current when the item was declared and $\mathit{name}$ is a specific name supplied by the user (see the functions new_axiom, new_definition, below). Different items can have the same specific name if the associated segment is different. Thus each theory segment provides a separate namespace of ML bindings of HOL items.

Various additional pieces of information are stored in a theory segment, including the parsing status of the constants (e.g., whether they are infixes or binders).

Determining the Context

There is always a \emph{current theory} which is the theory represented by the current theory segment together with its ancestry. The name of the current theory segment is returned by the ML function:

    current_theory : unit -> string

When an interactive HOL session begins, some theories will already be in the logical context. The exact set of theories in context will vary. If hol --bare is used, then only min and bool will be loaded. When the hol executable is used, a richer context is loaded.

The exact set of theories loaded can be determined with the ancestry command.

    ancestry : string -> string list

This function provides a general mechanism for examining the structure of the theory hierarchy. The argument is the name of a theory (or "-" as an abbreviation for the current theory), to which ancestry will respond with a list of the argument's ancestors in the theory hierarchy.

> ancestry "-";
val it =
   ["ConseqConv", "quantHeuristics", "patternMatches", "ind_type",
    "divides", "While", "cv", "reduce", "one", "sum", "option",
    "quotient", "pair", "combin", "sat", "normalForms", "relation",
    "min", "bool", "marker", "num", "prim_rec", "arithmetic",
    "numeral", "basicSize", "numpair", "pred_set", "list",
    "rich_list", "indexedLists", "hol"]: string list

Creating a Theory Segment

A new theory segment is created by a call to new_theory.

    new_theory : string -> unit

This allocates a new ‘area’ where subsequent theory operations take effect.

A call to new_theory "$\mathit{name}$" fails if:

• $\mathit{name}$ is not an alphanumeric starting with a letter; or

• there is a theory already named $\mathit{name}$ in the ancestry of the current segment.

On startup, the current theory segment of HOL is named scratch, which is an empty theory, having a useful collection of theories in its ancestry. Typically, a user would begin by loading whatever extra logical context is required for the work at hand.

The current theory segment acts as a kind of scratchpad. Elements stored in the current segment may be overwritten by subsequent additions, or deleted outright. Any theory elements built from overwritten or deleted elements are held to be out-of-date, and will not be included in the theory when it is finally exported. Out-of-date constants and types are detected by the HOL printer, which will print them surrounded by odd-looking syntax to alert the user.

In contrast to the current segment, (proper) ancestor segments may not be altered.

Loading Prebuilt Theories

Since HOL theories are represented by ML modules, when one is working interactively, one can import an existing theory segment by importing the corresponding module.

    load : string -> unit

\noindent Executing load "$\mathit{name}$Theory" imports the first occurrence of $\mathit{name}$Theory to be found along the loadPath into the session. Any unloaded ancestors of $\mathit{name}$ will be loaded before loading of $\mathit{name}$Theory continues. Note that load can not be used in ML files that are to be compiled; it can only be used in the interactive system.

Adding to the Current Theory

The following ML functions add types and terms to the current theory segment. In typical usage, these functions will not be needed since higher-level definition facilities will invoke these as necessary. However, these functions can be useful for those writing proof tools and derived definition principles.

    new_type : string * int -> unit

Executing new_type("$\mathit{op}$", $n$) makes $\mathit{op}$ a new $n$-ary type operator in the current theory. If $\mathit{op}$ is not an allowed name for a type, a warning will be issued.

    new_constant : string * hol_type -> unit

Executing new_constant("$c$", $\sigma$) makes $c_{\sigma'}$ a new constant of the current theory, for all $c_{\sigma'}$ where $\sigma'$ is an instance of $\sigma$. The type $\sigma$ is called the generic type of $c$. If $c$ is not an allowed name for a constant, a warning will be issued.

    new_axiom : string * term -> thm

Executing new_axiom("$\mathit{name}$",$t$) declares the sequent ([],$t$) to be an axiom of the current theory with name $\mathit{name}$. Failure occurs if:

• the type of $t$ is not bool; or
• $t$ contains out-of-date constants or types, $i.e.$, constants or types that have been re-declared after $t$ was built.

Once a theorem has been proved, it can be saved with the function

    save_thm : string * thm -> thm

Evaluating save_thm("$\mathit{name}$",$\mathit{th}$) will save the theorem $\mathit{th}$ with name $\mathit{name}$ in the current theory segment. In addition, various tools can be primed to pay particular attention to saved theorems through the use of special attributes. Such attributes are indicated by appending the list of the attribute names to the $\mathit{name}$. Thus, to indicate the simp attribute (for which, see discussion of the stateful simpset in §Stateful Simpset, one can write

    save_thm("name[simp]", th)

Multiple attributes can be listed between the square brackets, separated by commas.

There are also attributes controlling the way in which a theorem is saved, rather than affecting possible consumers of that theorem. The first, local, is used to create theorems that will not be exported to disk, but which are important locally. Such local theorems can have other attributes attached to them, which will have their effect within the given session/script-file. The second, unlisted, makes the theorem more difficult to access. This is appropriate when the theorem is being saved for the consumption of particular tools (which fact might be indicated by the use of other attributes), but the theorem is otherwise uninteresting, and unlikely to be something that a user is going to want to stumble across when searching or surveying theories. Concretely: unlisted theorems do not appear in theory signature files (so: cannot be accessed with the xTheory.thm_name syntax); and unlisted theorems will not be returned as the results of searches made for theorems using the functions in the DB module.

Instead of using the ML function save_thm, a special Theorem syntax is available for use in script files. One can write

   Theorem name = th

to achieve the same effect as an SML declaration

   val name = save_thm("name", th);

Attributes can also be added; for example:

   Theorem name[simp] = th

If one wishes to prove a goal with a tactic (see Chapter 4), and store the resulting theorem, the combination of these actions can be achieved with the store_thm function:

    store_thm : string * term * tactic -> thm

A call to store_thm(name,$t$,tac) results in the application of tac to goal $t$. If the tactic is successful, the resulting theorem is saved under the name name, as before. Also as before, theorem attributes can be added to the name.

Finally, again for use in script files only, there is a Theorem syntax to replace store_thm, reducing the need to write the same name twice, and giving a cleaner appearance. One can write

   Theorem name[attr1,attr2,...]:
     ...goal statement...
   Proof
     ...tactic...
   QED

The goal statement in this form is not an arbitrary term value, but must use the surface syntax used by the system parser (see §Quotations, Parsing and Printing). For example:

   Theorem IMP_CLAUSE[simp]:
     !p. (p ==> p) <=> T
   Proof
     rpt strip_tac
   QED

(The tactic above is shown to illustrate the Proof/QED shape of the form rather than the proof itself; closing this goal will need a little more than rpt strip_tac.) Note further that the Proof and QED keywords must occur in the leftmost column of the script file so that the parser can know when the term and tactic arguments terminate.

Instead of writing Theorem foo[local,...], one can write Triviality foo[...]. NB: This form has been deprecated and will be removed in a future release.

The choice to use Theorem syntax, or to use store_thm or save_thm directly is a matter of users' aesthetic preference. But recall: if writing library code to prove and store theorems, the underlying store_thm must be used, as the special treatment of the Theorem keyword is only available in script files.

Exporting a Theory

Once a theory segment has been constructed, it can be written out to a file, which, after compilation, can be imported into future sessions.

    export_theory : unit -> unit

When export_theory is called, all out-of-date entities are removed from the current segment. Also, the parenthood of the theory is computed. The current theory segment is written to a file nameTheory.sml, and the file nameTheory.sig, which documents the contents of name, is also written. Notice that the exported theory is not compiled by HOL. That is left to an external tool, Holmake (see the section on Holmake), which maintains dependencies among collections of HOL theory segments.

ML functions for accessing theories

The arguments of ML type string to new_axiom, new_definition, etc., are the names of the corresponding axioms and definitions. These names are used when accessing theories with the functions axiom, definition, etc., described below.

The current theory can be extended by adding new parents, types, constants, axioms and definitions. Theories that are in the ancestry of the current theory cannot be extended in this way; they can be thought of as frozen.

There are various functions for loading the contents of theory files:

    parents : string -> string list
    types : string -> (string * int) list
    constants : string -> term list

The first argument is the name of a theory (which must be in the ancestry of the current theory segment); the result is a list of the components of the theory. The name of the current theory can be abbreviated by "-". For example, parents "-" returns the parents of the current theory.

In the case of types a list of name-arity pairs is returned. Individual axioms, definitions and theorems can be read from the current theory using the following ML functions:

    axiom : string -> thm
    definition : string -> thm
    theorem : string -> thm

The first argument is the user supplied name of the axiom, definition or theorem in the current theory. Further, a list of all of a theory's axioms, definitions and theorems can be retrieved with the ML functions:

    axioms : string -> (string * thm) list
    definitions : string -> (string * thm) list
    theorems : string -> (string * thm) list

The contents of the current theory can be printed in a readable format using the function print_theory.

Functions for creating definitional extensions

There are three kinds of definitional extensions: constant definitions, constant specifications and type definitions.

Constant Definitions

In §LOGIC a constant definition over a signature $\Sigma_{\Omega}$ is defined to be an equation, i.e., a formula of the form $c_{\sigma}=t_{\sigma}$, such that:

1. $c$ is not the name of any constant in $\Sigma_{\Omega}$;
2. $t_{\sigma}$ is a closed term in $\mathsf{Terms}_{\Sigma_{\Omega}}$;
3. all the type variables occurring in $t_{\sigma}$ occur in $\sigma$.

In HOL, definitions can be slightly more general than this, in that an equation: $$ c\ v_1\ \cdots\ v_n\ =\ t $$ is allowed to be a definition where $v_1$, $\dots$, $v_n$ are variable structures (i.e., tuples of distinct variables). Such an equation is logically equivalent to: $$ c\ =\ \lambda v_1\ \cdots\ v_n.\ t $$ which is a definition in the sense of §LOGIC if (i), (ii) and (iii) hold.

The following ML function creates a new definition in the current theory.

    new_definition : string * term -> thm

Evaluating new_definition("name", “$c\ v_1\ \cdots\ v_n\ =\ t$”) declares the sequent $(\{\},\ c = \lambda v_1\ \cdots\ v_n.\ t)$ to be a constant definition of the current theory. The name associated with the definition in this theory is name. Failure occurs if:

1. $t$ contains free variables that are not in any of the variable structures $v_1$, $\dots$, $v_n$ (this is equivalent to requiring $\lambda v_1\ \cdots\ v_n.\ t$ to be a closed term);
2. there is a type variable in $v_1$, $\dots$, $v_n$ or $t$ that does not occur in the type of $c$.

Constant Specifications

In §LOGIC a constant specification for a theory $\mathcal{T}$ is defined to be a pair: $$ \langle (c_1,\ldots,c_n),\ \forall {x_1}_{\sigma_1} \cdots {x_n}_{\sigma_n}.\ t_{\mathtt{bool}} \rangle $$ such that:

1. $c_1$, $\dots$, $c_n$ are distinct names;
2. $\forall {x_1}_{\sigma_1} \cdots {x_n}_{\sigma_n}.\ t_{\mathtt{bool}} \in \mathsf{Terms}_{\mathcal{T}}$;
3. $tyvars(\forall {x_1}_{\sigma_1} \cdots {x_n}_{\sigma_n}.\ t_{\mathtt{bool}}) \subseteq tyvars(\sigma_i)$ for $1 \leq i \leq n$;
4. $\exists {x_1}_{\sigma_1}\ \cdots\ {x_n}_{\sigma_n}.\ t \in \mathsf{Theorems}_{\mathcal{T}}$.

The following ML function is used to make constant specifications in the HOL system.

    new_specification : string * string list * thm -> thm

Evaluating:

   new_specification("name", ["c1", ..., "cn"],
                     |- ?x1 ... xn. t[x1, ..., xn])

simultaneously introduces new constants named $c_1$, $\dots$, $c_n$ satisfying the property: $$ \vdash t[c_1, \ldots, c_n] $$ This theorem is stored, with name name, as a definition in the current theory segment. A call to new_specification fails if:

1. the theorem argument has a non-empty assumption list;
2. there are free variables in the theorem argument;
3. $c_1$, $\dots$, $c_n$ are not distinct variables;
4. the type of some $c_i$ does not contain all the type variables which occur in the term \x1 ... xn. t[x1, ..., xn].

Type Definitions

In §LOGIC it is explained that defining a new type $(\alpha_1,\ldots,\alpha_n)\mathit{op}$ in a theory $\mathcal{T}$ consists of introducing $\mathit{op}$ as a new $n$-ary type operator and $$ \vdash \exists f_{(\alpha_1,\ldots,\alpha_n)\mathit{op} \to \sigma}.\ \mathsf{TyDef}\ p\ f $$ as a new axiom, where $p$ is a predicate characterizing a non-empty subset of an existing type $\sigma$. Formally, a type definition for a theory $\mathcal{T}$ is a 3-tuple $$ \langle \sigma,\ (\alpha_1,\ldots,\alpha_n)\mathit{op},\ p_{\sigma\to\mathtt{bool}} \rangle $$ where:

1. $\sigma \in \mathsf{Types}_{\mathcal{T}}$ and $tyvars(\sigma) \in \{\alpha_1, \ldots, \alpha_n\}$;
2. $\mathit{op}$ is not the name of a type constant in $\mathsf{Struc}_{\mathcal{T}}$;
3. $p \in \mathsf{Terms}_{\mathcal{T}}$ is a closed term of type $\sigma\to\mathtt{bool}$ and $tyvars(p) \subseteq \{\alpha_1, \ldots, \alpha_n\}$;
4. $\exists x_{\sigma}.\ p\ x \subseteq \mathsf{Theorems}_{\mathcal{T}}$.

The following ML function makes a type definition in the HOL system.

    new_type_definition : string * thm -> thm

If $t$ is a term of type $\sigma$->bool containing $n$ distinct type variables, then evaluating:

   new_type_definition("op", |- ?x. t x)

results in op being declared as a new $n$-ary type operator characterized by the definitional axiom:

   |- ?rep. TYPE_DEFINITION t rep

which is stored as a definition with the automatically generated name op_TY_DEF. The constant TYPE_DEFINITION is defined in the theory bool by:

   |- TYPE_DEFINITION (P:'a->bool) (rep:'b->'a) =
       (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
       (!x. P x = (?x'. x = rep x'))

Executing new_type_definition("op", |- ?$x$. $t\ x$) fails if:

1. $t$ does not have a type of the form $\sigma$->bool.

Defining Bijections

The result of a type definition using new_type_definition is a theorem which asserts only the existence of a bijection from the type it defines to the corresponding subset of an existing type. To introduce constants that in fact denote such a bijection and its inverse, the following ML function is provided:

    define_new_type_bijections :
      {ABS: string, REP: string, name: string, tyax: thm} -> thm

This function takes a record {ABS, REP, name, tyax}. The tyax argument must be a definitional axiom of the form returned by new_type_definition. The name argument is the name under which the constant definition (a constant specification, in fact) made by define_new_type_bijections will be stored in the current theory segment, and the ABS and REP arguments are user-specified names for the two constants that are to be defined. These constants are defined so as to denote mutually inverse bijections between the defined type, whose definition is given by the supplied theorem, and the representing type of this defined type.

Evaluating:

  define_new_type_bijections
       {name="name", ABS="abs", REP="rep",
        tyax = |- ?rep:newty->ty. TYPE_DEFINITION P rep}

automatically defines two new constants abs:ty->newty and rep:ty->newty such that:

   |- (!a. abs(rep a) = a) /\ (!r. P r = (rep(abs r) = r))

This theorem, which is the defining property for the constants abs and rep, is stored under the name "name" in the current theory segment. It is also the value returned by define_new_type_bijections. The theorem states that abs is the left inverse of rep and — for values satisfying P — that rep is the left inverse of abs.

A call to define_new_type_bijections name abs rep th fails if:

1. th is not a theorem of the form returned by new_type_definition.

Properties of Type Bijections

The following ML functions are provided for proving that the bijections introduced by define_new_type_bijections are injective (one-to-one) and surjective (onto):

    prove_rep_fn_one_one : thm -> thm
    prove_rep_fn_onto : thm -> thm
    prove_abs_fn_one_one : thm -> thm
    prove_abs_fn_onto : thm -> thm

The theorem argument to each of these functions must be a theorem of the form returned by define_new_type_bijections:

   |- (!a. abs(rep a) = a) /\ (!r. P r = (rep(abs r) = r))

If th is a theorem of this form, then evaluating prove_rep_fn_one_one th proves that the function rep is one-to-one, and returns the theorem:

   |- !a a'. (rep a = rep a') = (a = a')

Likewise, prove_rep_fn_onto th proves that rep is onto the set of values that satisfy P:

   |- !r. P r = (?a. r = rep a)

Evaluating prove_abs_fn_one_one th proves that abs is one-to-one for values that satisfy P, and returns the theorem:

   |- !r r'. P r ==> P r' ==> ((abs r = abs r') = (r = r'))

And evaluating prove_abs_fn_onto th proves that abs is onto, returning the theorem:

   |- !a. ?r. (a = abs r) /\ P r

All four functions will fail if applied to any theorem that does not have the form of a theorem returned by define_new_type_bijections. None of these functions saves anything in the current theory.

1. Note that ‘hypotheses’ and ‘conclusion’ are also used for the components of sequents. ↩

2. This is a simplification: in fact the various axioms are an extension of the basic logic. ↩

3. Tags are also used for tracking the use of axioms in proofs. ↩