Advanced Definition Principles
General-Purpose Definition
Definition takes a high-level specification of a HOL function, and
attempts to define the function in the logic. If this attempt is
successful, the specification is derived from the definition. The
derived specification is returned to the user, and also stored in
the current theory. Definition may be used to define
abbreviations, recursive functions, and mutually recursive
functions.
The basic form of a Definition is
Definition defname[attrs]:
fn-spec
End
or
Definition defname[attrs]:
fn-spec
Termination
tactic
End
The latter form maps to a call to tDefine; the former to xDefine
(or Define). (See their entries of in \REFERENCE{} for more
details.) The termination argument is only needed when defining
certain recursive functions. (See Section 7.6 for more
details on the support of recursive functions, and mutually
recursive functions and the full syntax of the fn-spec above.)
Note that this is not valid ML syntax. Instead, HOL is using
lexical pre-processing to transform the above into something more
complicated underneath. To make this reasonable, there are
constraints introduced on the syntax above: all keywords
(Definition, Termination and End) must appear in column 1 of
the input (hard against the left margin in one's input source file).
In both cases, the defname is taken to be the name of the theorem
stored to disk (it does not have a suffix such as _def appended
to it), and is also the name of the local SML binding. The
attributes given by attrs can be any standard attribute (such as
simp), and/or drawn from Definition-specific options:
- The attribute
schematicallows the definition to be schematic. (See Section 7.6.3 for more details.) - The attribute
nocomputestops the definition from being added to the global compset used byEVAL. This is equivalent tozDefine. (See Section 8.6 and also the corresponding entry in \REFERENCE{} for more details.) - The attribute
induction=inamemakes the induction theorem that is automatically derived for definitions with interesting termination be callediname. If this is omitted, the name chosen will be derived from thedefnameof the definition: ifdefnameends with_defor_DEF, the induction name will replace this suffix with_indor_INDrespectively; otherwise the induction name will simply bedefnamewith_indappended.
Note that, whether or not the induction= attribute is used, the
induction theorem is always made available as an SML binding under
the appropriate name. This means that one does not need to follow
one's definition with a call to something like DB.fetch or
theorem just to make the induction theorem available at the SML
level.
Datatypes
Although the HOL logic provides primitive definition principles allowing new types to be introduced, the level of detail is very fine-grained. The style of datatype definitions in functional programming languages provides motivation for a high level interface for defining algebraic datatypes.
The Datatype function supports the definition of such data types;
the specifications of the types may be recursive, mutually
recursive, nested recursive, and involve records. The syntax of
declarations that Datatype accepts is found in Table
7.2.1
Table: Datatype declaration syntax. An atomic-type is a single
token that denotes a hol_type (e.g. num, real, or 'a).
Datatype `[binding ;]* binding`
binding ::= ident = constructor-spec
| ident = record-spec
constructor-spec ::= [clause |]* clause
clause ::= ident ty-spec*
ty-spec ::= ( hol_type ) | atomic-type
record-spec ::= <| [ident : hol_type ;]* ident : hol_type ;? |>
HOL maintains an underlying database of datatype facts called the
TypeBase. This database is used to support various high-level
proof tools (see the bossLib section of the Libraries chapter),
and is augmented
whenever a Datatype declaration is made. When a datatype is
defined by Datatype, the following information is derived and
stored in the database.
- initiality theorem for the type
- injectivity of the constructors
- distinctness of the constructors
- structural induction theorem
- case analysis theorem
- definition of the ‘case’ constant for the type
- congruence theorem for the case constant
- definition of the ‘size’ of the type
When the HOL system starts up, the TypeBase already contains the
relevant entries for the types bool, prod, num, option, and
list.
Example: Binary trees
The following ML declaration of a data type of binary trees
datatype ('a,'b) btree = Leaf of 'a
| Node of ('a,'b) btree * 'b * ('a,'b) btree
could be declared in HOL with a call to the Datatype function:
Datatype `btree = Leaf 'a | Node btree 'b btree`
Also: good practice in script files is to make sure that everything is an ML declaration, so the above should really appear as
val _ = Datatype `btree = Leaf 'a | Node btree 'b btree`
To reduce the verbiage of the above, there is a special syntax (akin
to Theorem and Definition), allowing one to instead write
> Datatype:
btree = Leaf 'a | Node btree 'b btree
End
<<HOL message: Defined type: "btree">>
As with the other forms, the keywords here must be in column 1.
Note that in all forms, any type parameters for the new type are not mentioned: the type variables are always ordered alphabetically.
This subtle point bears repeating: the format of datatype definitions does not have enough information to always determine the order of arguments to the introduced type operators. Thus, when defining a type that is polymorphic in more than one argument, there is a question of what the order of the new operator's arguments will be. For another example, if one defines
Datatype: sum = C1 'left | C2 'right
End
and then writes ('a,'b)sum, will the 'a value be under the C1
or C2 constructor? The system chooses to make the arguments
corresponding to variables appear in the order given by the
dictionary ordering of the names of the variables occurring in the
definition. Thus, in the example given, the 'a of ('a,'b)sum
will be the argument to the C1 constructor because 'left comes
before 'right in the standard (ASCII) dictionary ordering.
Further examples
In the following, we shall give an overview of the kinds of types
that may be defined by Datatype.
To start, enumerated types can be defined as in the following example:
> Datatype:
enum = A1 | A2 | A3 | A4 | A5
| A6 | A7 | A8 | A9 | A10
| A11 | A12 | A13 | A14 | A15
| A16 | A17 | A18 | A19 | A20
| A21 | A22 | A23 | A24 | A25
| A26 | A27 | A28 | A29 | A30
End
<<HOL message: Defined type: "enum">>
Other non-recursive types may be defined as well:
> Datatype:
foo = N num | B bool | Fn ('a -> 'b) | Pr ('a # 'b)
End
<<HOL message: Defined type: "foo">>
Turning to recursive types, we have already seen a type of binary trees having polymorphic values at internal nodes. This time, we will declare it in “paired” format.
> Datatype:
tree = Leaf2 'a | Node2 (tree # 'b # tree)
End
<<HOL message: Defined type: "tree">>
This specification seems closer to the declaration that one might make in ML, but can be more difficult to deal with in proof than the curried format used above.
The basic syntax of the named lambda calculus is easy to describe:
> Datatype:
lambda = Var string
| Const 'a
| Comb lambda lambda
| Abs lambda lambda
End
<<HOL message: Defined type: "lambda">>
The syntax for ‘de Bruijn’ terms is roughly similar:
> Datatype:
dB = Var2 string
| Const2 'a
| Bound num
| Comb2 dB dB
| Abs2 dB
End
<<HOL message: Defined type: "dB">>
Arbitrarily branching trees may be defined by allowing a node to hold the list of its subtrees. In such a case, leaf nodes do not need to be explicitly declared.
> Datatype:
ntree = Node3 'a (ntree list)
End
<<HOL message: Defined type: "ntree">>
A type of ‘first order terms’ can be declared as follows:
> Datatype:
term = Var3 string | Fnapp (string # term list)
End
<<HOL message: Defined type: "term">>
Mutually recursive types may also be defined. The following, extracted by Elsa Gunter from the Definition of Standard ML, captures a subset of Core ML.
> Datatype:
atexp = var_exp string
| let_exp dec exp ;
exp = aexp atexp
| app_exp exp atexp
| fn_exp match ;
match = match rule
| matchl rule match ;
rule = rule pat exp ;
dec = val_dec valbind
| local_dec dec dec
| seq_dec dec dec ;
valbind = bind pat exp
| bindl pat exp valbind
| rec_bind valbind ;
pat = wild_pat
| var_pat string
End
<<HOL message: Defined types: "pat", "atexp", "exp", "match", "rule", "dec", "valbind">>
Simple record types may be introduced using the <| ... |>
notation.
> Datatype:
state = <| Reg1 : num; Reg2 : num; Waiting : bool |>
End
<<HOL message: Defined type: "state">>
The use of record types may be recursive. For example, the following declaration could be used to formalize a simple file system.
> Datatype:
file = Text string | Dir directory
;
directory = <| owner : string ;
files : (string # file) list |>
End
<<HOL message: Defined types: "file", "directory">>
Type definitions that fail
Now we address some types that cannot be declared with Datatype.
In some cases they cannot exist in HOL at all; in others, the type
can be built in the HOL logic, but Datatype is not able to make
the definition.
First, an empty type is not allowed in HOL, so the following attempt is doomed to fail.
> Datatype: tyfail1 = A tyfail1
End
Exception- HOL_ERR
(at Datatype.Datatype:
at ind_types.define_type:
at Lib.tryfind: all applications failed) raised
So called ‘nested types’, which are occasionally quite useful,
cannot at present be built with Datatype:
> Datatype: tyfail2 = LeafX 'a | NodeX (('a # 'a) tyfail2)
End
Exception- HOL_ERR
(at Datatype.Datatype:
at Datatype.to_tyspecs: Omit arguments to new type:"tyfail2") raised
Types may not recurse on either side of function arrows. Recursion
on the right is consistent (see the theory inftree), but
Datatype is not capable of defining algebraic types that require
it. Thus, examples such as the following will fail:
> Datatype: tyfail3 = Nil | Cons 'a ('b -> tyfail3)
End
Exception- HOL_ERR
(at Datatype.Datatype:
at ind_types.define_type:
at ind_types.define_type_nested:
Can't find definition for nested type: fun) raised
Recursion on the left must fail for cardinality reasons. For
example, HOL does not allow the following attempt to model the
untyped lambda calculus (note the -> in the clause for the Abs
constructor):
> Datatype: tyfail4 = VarX string
| ConstX 'a
| CombX tyfail4 tyfail4
| AbsX (tyfail4 -> tyfail4)
End
Exception- HOL_ERR
(at Datatype.Datatype:
at ind_types.define_type:
at ind_types.define_type_nested:
Can't find definition for nested type: fun) raised
Theorems arising from a datatype definition
The consequences of an invocation of Datatype are stored in the
current theory segment and in TypeBase. The principal
consequences of a datatype definition are the primitive recursion
and induction theorems. These provide the ability to define simple
functions over the type, and an induction principle for the type.
Thus, for a type named ty, the primitive recursion theorem is
stored under ty_Axiom and the induction theorem is put under
ty_induction. Other consequences include the distinctness of
constructors (ty_distinct), and the injectivity of constructors
(ty_11). A ‘degenerate’ version of ty_induction is also stored
under ty_nchotomy: it provides for reasoning by cases on the
construction of elements of ty. Finally, some special-purpose
theorems are stored: for example, ty_case_cong holds a congruence
theorem for “case” statements on elements of ty. These case
statements are defined by ty_case_def. Also, a definition of the
“size” of the type is added to the current theory, under the name
ty_size_def.
For example, invoking
> Datatype:
ntree2 = NLeaf num | NNode ntree2 ntree2
End
<<HOL message: Defined type: "ntree2">>
results in the definitions
> val ntree2_case_def = DB.fetch "-" "ntree2_case_def";
val ntree2_size_def = DB.fetch "-" "ntree2_size_def";
val ntree2_case_def =
⊢ (∀a f f1. ntree2_CASE (NLeaf a) f f1 = f a) ∧
∀a0 a1 f f1. ntree2_CASE (NNode a0 a1) f f1 = f1 a0 a1: thm
val ntree2_size_def =
⊢ (∀a. ntree2_size (NLeaf a) = 1 + a) ∧
∀a0 a1.
ntree2_size (NNode a0 a1) = 1 + (ntree2_size a0 + ntree2_size a1): thm
being added to the current theory. Note that the generated
theorems are not bound at the SML top level by default; the
reader has to retrieve them from the theory database
explicitly, as the DB.fetch "-" "...name..." calls above
illustrate. The case constant (here ntree2_CASE) allows
pretty case expressions; see Section 7.5 below. The
following theorems about the datatype are also proved and
stored in the current theory.
> val ntree2_Axiom = DB.fetch "-" "ntree2_Axiom";
val ntree2_induction = DB.fetch "-" "ntree2_induction";
val ntree2_nchotomy = DB.fetch "-" "ntree2_nchotomy";
val ntree2_11 = DB.fetch "-" "ntree2_11";
val ntree2_distinct = DB.fetch "-" "ntree2_distinct";
val ntree2_case_cong = DB.fetch "-" "ntree2_case_cong";
val ntree2_Axiom =
⊢ ∀f0 f1. ∃fn.
(∀a. fn (NLeaf a) = f0 a) ∧
∀a0 a1. fn (NNode a0 a1) = f1 a0 a1 (fn a0) (fn a1): thm
val ntree2_induction =
⊢ ∀P. (∀n. P (NLeaf n)) ∧ (∀n n0. P n ∧ P n0 ⇒ P (NNode n n0)) ⇒ ∀n. P n:
thm
val ntree2_nchotomy = ⊢ ∀nn. (∃n. nn = NLeaf n) ∨ ∃n n0. nn = NNode n n0: thm
val ntree2_11 =
⊢ (∀a a'. NLeaf a = NLeaf a' ⇔ a = a') ∧
∀a0 a1 a0' a1'. NNode a0 a1 = NNode a0' a1' ⇔ a0 = a0' ∧ a1 = a1': thm
val ntree2_distinct = ⊢ ∀a1 a0 a. NLeaf a ≠ NNode a0 a1: thm
val ntree2_case_cong =
⊢ ∀M M' f f1.
M = M' ∧ (∀a. M' = NLeaf a ⇒ f a = f' a) ∧
(∀a0 a1. M' = NNode a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒
ntree2_CASE M f f1 = ntree2_CASE M' f' f1': thm
When a type involving records is defined, many more definitions are made and added to the current theory.
A mutually recursive type definition results in the above theorems and definitions being added for each of the defined types.
Record Types
Record types are convenient ways of bundling together a number of
component types, and giving those components names so as to
facilitate access to them. Record types are semantically
equivalent to big pair (product) types, but the ability to label
the fields with names of one's own choosing is a great
convenience. Record types as implemented in HOL are similar to
C's struct types and to Pascal's records.
Done correctly, record types provide useful maintainability
features. If one can always access the fieldn field of a record
type by simply writing record.fieldn, then changes to the type
that result in the addition or deletion of other fields will not
invalidate this reference. One failing in SML's record types is
that they do not allow the same maintainability as far as
(functional) updates of records are concerned. The HOL
implementation allows one to write
rec with fieldn := new_value
which replaces the old value of fieldn in the record rec with
new_value. This expression will not need to be changed if
another field is added, modified or deleted from the record's
original definition.
Defining a record type
Record types are defined with the function Datatype, as
previously discussed. For example, to create a record type called
person with boolean, string and number fields called employed,
name and age, one would enter:
> Datatype:
person = <| employed : bool ; age : num ; name : string |>
End
<<HOL message: Defined type: "person">>
The order in which the fields are entered is not significant. As
well as defining the type (called person), the datatype
definition function also defines two other sets of constants.
These are the field access functions and functional update
functions.
The field access functions have names of the form
record-type_field. These functions can be used directly,
or one can use standard field selection notation to access the
values of a record's field. Thus, one would write the expression
bob.employed in order to return the value of bob's employed
field. The alternative, person_employed bob, works, but would
be printed using the first syntax, with the full-stop.
The functional update functions are given the names
"record-type_field_fupd" for each field in the type. They
take two arguments, a function and a record to be updated. The
function parameter is an endomorphism on the field type, so that
the resulting record is the same as the original, except that the
specified field has had the given function applied to it to
generate the new value for that field. They can be written with
the keyword with and the updated_by operator. Thus
> ``bob with employed updated_by $~``;
val it = “bob with employed updated_by $¬”: term
is a record value identical to the bob except that the boolean
value in the employed field has been inverted. (bob here is
just a free HOL variable of type person; we don't need to bind
it to a specific value to talk about this syntax.)
Additionally, there is syntactic sugar available to let one write
a record with one of its fields replaced by a specific value.
This is done by using the := operator instead of updated_by:
> ``bob with employed := T``;
val it = “bob with employed := T”: term
This form is translated at parse-time to be a use of the
corresponding functional update, along with a use of the
$\mathsf{K}$-combinator from the combin theory. Thus, the above
example is really
> ``bob with employed updated_by (K T)``;
val it = “bob with employed := T”: term
which is in turn a pretty form of
> ``person_employed_fupd (K T) bob``;
val it = “bob with employed := T”: term
If a chain of updates is desired, then multiple updates can be
specified inside <|-|> pairs, separated by semi-colons, thus:
> ``bob with <| age := 10; name := "Child labourer" |>``;
val it = “bob with <|age := 10; name := "Child labourer"|>”: term
Both update forms (using updated_by and :=) can be used in a
chain of updates.
Specifying record literals
The parser accepts lists of field specifications between
<|-|> pairs without the with keyword. These translate to
sequences of updates of an arbitrary value (literally, the HOL
value ARB), and are treated as literals. Thus,
> ``<| age := 21; employed := F; name := "Layabout" |>``;
val it = “<|age := 21; employed := F; name := "Layabout"|>”: term
Using the theorems produced by record definition
As well as defining the type and the functions described above,
record type definition also proves a suite of useful theorems.
These are all saved (using save_thm) in the current segment.
Some are also added to the TypeBase's simplifications for the
type, so they will be automatically applied when simplifying with
the srw_ss() simpset, or with the tactics RW_TAC and SRW_TAC
(see Section 8.5).
All of the theorems are saved under names that begin with the name of the type. The list below is a sample of the theorems proved. The identifying strings are suffixes appended to the name of the type in order to generate the final name of the theorem.
_accessors- The definitions of the accessor functions. This theorem is
installed in the
TypeBase. _fn_updates- The definitions of the functional update functions.
_accfupds- A theorem that states simpler forms for expressions that are
of the form $\mathit{field}_i\,(\mathit{field}_j\mathtt{\_fupd}\;f\;r)$.
If $i = j$, then the RHS is $f(\mathit{field}_i(r))$, if not,
it is $(\mathit{field}_i\;r)$. This theorem is installed in
the
TypeBase. _component_equality- A theorem stating that $(r_1 = r_2) \equiv \bigwedge_i (\mathit{field}_i(r_1) = \mathit{field}_i(r_2))$.
_fupdfupds- A theorem stating that
$\mathit{field}_i\mathtt{\_fupd}\;f\,(\mathit{field}_i\mathtt{\_fupd}\;g\;r) =
\mathit{field}_i\mathtt{\_fupd}\;(f \circ g)\;r$.
This theorem is installed in the
TypeBase. _fupdcanon- A theorem that states commutativity results for all possible
pairs of field updates. They are constructed in such a way
that if used as rewrites, they will canonicalise sequences of
updates. Thus, for all $i < j$, the equation
$\mathit{field}_j\mathtt{\_fupd}\;f\;(\mathit{field}_i\mathtt{\_fupd}\;g\;r)$
$=$
$\mathit{field}_i\mathtt{\_fupd}\;g\;(\mathit{field}_j\mathtt{\_fupd}\;f\;r)$
is generated. This theorem is installed in the
TypeBase.
Big records
The size of certain theorems proved in the record type package
increases as the square of the number of fields in the record.
(In particular, the update canonicalisation and acc_fupd
theorems have this property.) To avoid this problem, users
should define a system of hierarchically nested sub-records if
their records are getting too large.
Quotient Types
HOL provides a library for defining new types which are quotients of existing types, with respect to partial equivalence relations. This library is described in “Higher Order Quotients in Higher Order Logic” [HOQ], from which the following description is taken.
The quotient library is accessed by opening quotientLib, which
makes all its tools and theorems accessible.
The definition of new types corresponding to the quotients of existing types by equivalence relations is called “lifting” the types from a lower, more representational level to a higher, more abstract level. Both levels describe similar objects, but some details which are apparent at the lower level are no longer visible at the higher level. The logic is simplified.
Simply forming a new type does not complete the quotient operation. Rather, one wishes to recreate the pre-existing logical environment at the new, higher, and more abstract level. This includes not only the new types, but also new versions of the constants that form and manipulate values of those types, and also new versions of the theorems that describe properties of those constants. All of these form a logical layer, above which all the lower representational details may be safely and forever forgotten.
This can be done in a single call of the main tool of this package.
define_quotient_types :
{types: {name: string,
equiv: thm} list,
defs: {def_name: string,
fname: string,
func: Term.term,
fixity: Parse.fixity} list,
tyop_equivs : thm list,
tyop_quotients : thm list,
tyop_simps : thm list,
respects : thm list,
poly_preserves : thm list,
poly_respects : thm list,
old_thms : thm list} ->
thm list
define_quotient_types takes a single argument which is a record
with the following fields.
types is a list of records, each of which contains two fields: name, which is the name of a new quotient type to be created, and equiv, which is either (1) a theorem that a binary relation $R$ is an equivalence relation (see [HOQ] §4) of the form
$$\mathtt{|-}\ \forall x\ y.\ R\ x\ y \Leftrightarrow (R\ x = R\ y),$$
or (2) a theorem that $R$ is a nonempty partial equivalence relation, (see [HOQ] §5) of the form
$$\mathtt{|-}\ (\exists x.\ R\ x\ x) \wedge (\forall x\ y.\ R\ x\ y \Leftrightarrow R\ x\ x \wedge R\ y\ y \wedge (R\ x = R\ y)).$$
The process of forming the new quotient types is described in [HOQ] §8.
defs is a list of records specifying the constants to be lifted.
Each record contains the following four fields: func is an HOL
term, which must be a single constant, which is the constant to
be lifted. fname is the name of the new constant being defined
as the lifted version of func. fixity is the HOL fixity of
the new constant being created, as specified in the HOL structure
Parse. def_name is the name under which the new constant
definition is to be stored in the current theory. The process of
defining lifted constants is described in [HOQ] §9.
tyop_equivs is a list of conditional equivalence theorems for type operators (see [HOQ] §4.1). These are used for bringing into regular form theorems on new type operators, so that they can be lifted (see [HOQ] §11 and §12).
tyop_quotients is a list of conditional quotient theorems for type operators (see [HOQ] §5.2). These are used for lifting both constants and theorems.
tyop_simps is a list of theorems used to simplify type operator
relations and map functions, e.g., for pairs,
|- ($= ### $=) = $= and |- (I ## I) = I.
The rest of the arguments refer to the general process of lifting theorems over the quotients being defined, as described in [HOQ] §10.
respects is a list of theorems about the respectfulness of the constants being lifted. These theorems are described in [HOQ] §10.1.
poly_preserves is a list of theorems about the preservation of polymorphic constants in the HOL logic across a quotient operation. In other words, they state that any quotient operation preserves these constants as a homomorphism. These theorems are described in [HOQ] §10.2.
poly_respects is a list of theorems showing the respectfulness of the polymorphic constants mentioned in poly_preserves. These are described in [HOQ] §10.3.
old_thms is a list of theorems concerning the lower, representative types and constants, which are to be automatically lifted and proved at the higher, more abstract quotient level. These theorems are described in [HOQ] §10.4.
define_quotient_types returns a list of theorems, which are the
lifted versions of the old_thms.
A similar function, define_quotient_types_rule, takes a single
argument which is a record with the same fields as above except
for old_thms, and returns an SML function of type thm -> thm.
This result, typically called LIFT_RULE, is then used to lift
the old theorems individually, one at a time.
For backwards compatibility with the excellent quotients package
EquivType created by John Harrison (which provided much
inspiration), the following function is also provided:
define_equivalence_type :
{name: string,
equiv: thm,
defs: {def_name: string,
fname: string,
func: Term.term,
fixity: Parse.fixity} list,
welldefs : thm list,
old_thms : thm list} ->
thm list
This function is limited to a single quotient type, but may be
more convenient when the generality of define_quotient_types is
not needed. This function is defined in terms of
define_quotient_types as
fun define_equivalence_type {name,equiv,defs,welldefs,old_thms} =
define_quotient_types
{types=[{name=name, equiv=equiv}], defs=defs, tyop_equivs=[],
tyop_quotients=[FUN_QUOTIENT],
tyop_simps=[FUN_REL_EQ,FUN_MAP_I], respects=welldefs,
poly_preserves=[FORALL_PRS,EXISTS_PRS],
poly_respects=[RES_FORALL_RSP,RES_EXISTS_RSP],
old_thms=old_thms};
Case Expressions
Case constructs are an important feature of functional programming languages such as Standard ML. They provide a very compact and convenient notation for multi-way selection among the values of several expressions. HOL provides such a feature in the form of case expressions. Case expressions can simplify the expression of complicated branches between different cases or combinations of cases.
Pattern matching and case expressions are not directly supported
by higher order logic. Thus, some effort is needed to support
them in HOL. There are two implementations of case expressions
in HOL. The parser supports case expressions, which it compiles
into decision trees based on if-then-else expressions and
case-constants as introduced by datatype definitions. The
pretty-printer presents these complicated decision trees as
nicely readable case expressions again. In addition, there is
patternMatchesLib, which provides a formalisation of case
expressions based on Hilbert's choice operator. Following the
name of the main function, these are called Pmatch case
expressions.
The benefit of decision-tree case expressions is that the whole semantic complexity is handled by the parser and pretty-printer. The resulting terms are simple. However, one needs to trust the complicated, lengthy case expression code in the parser and pretty-printer. Moreover, the internal structure might differ considerably from the input and is hard to predict. In some cases there can be a serious blow-up in size.
Pmatch case expressions are simple to parse and pretty-print. They support more features than decision-tree ones. There are guards, unbound variables in patterns and a wider variety of supported patterns in general. There is no size-blowup or surprising internal structure. Therefore, code generated from Pmatch case expressions tends to be better. However, this comes at the price of a much heavier machinery to reason about Pmatch case expressions.
Decision-tree case expressions
By default, HOL uses decision-tree case expressions. Let the non-terminal term stand for any HOL term and the non-terminal cpat represent any constructor pattern, i.e., any HOL term containing only literals, datatype constructors and variables. Then, the syntax of decision-tree case expressions is given by
$$\mathit{term} ::= \mathtt{case}\;\mathit{term}\;\mathtt{of}\;\mathtt{|}^?\; \mathit{cpat}\;\mathtt{=>}\;\mathit{term}\; (\mathtt{|}\;\mathit{cpat}\;\mathtt{=>}\;\mathit{term})^*$$
The choice in the rule allows the use of more uniform syntax, where every case is preceded by a vertical bar. Omitting the bar, which is what the pretty-printer does when the syntax is printed, conforms to the syntax used by SML.
Case expressions consider their list of pattern expressions in
sequence to see if they match the test expression. Matching
means that there is an assignment for the bound variables of
that pattern expressions such that it equals the test
expression. The first pattern which successfully matches causes
its associated result expression to be evaluated with the
matching variable assignment. The resulting value is yielded as
the value of the entire case expression. If no pattern
expression matches, the result of the case expression is ARB.
Since decision-tree case expressions support only constructor
patterns, it is guaranteed that if a pattern expression matches,
the resulting variable assignment is uniquely determined.
A simple example of a case expression is
case n of
0 => "none"
| 1 => "one"
| 2 => "two"
| _ => "many"
This could have been expressed using several “if-then-else” constructs, but the case expression is much more compact and clean, with the selection between various choices made clearly evident. Internally though, it is compiled to nested “if-then-else” statements.
In addition to literals as patterns, as above, patterns may be
constructor expressions. Many standard HOL types have
constructors, including num, list, and option. A simple
example using constructor patterns is (notice the optional bar
in front of the first case).
case spouse(employee) of
| NONE => "single"
| SOME s => "married to " ++ name_of s
HOL supports a rich structure of case expressions using a single notation. The format is related to that of definitions of recursive functions, as described in Section 7.6. In addition, case expressions may contain literals as patterns, either singly or as elements of deeply nested patterns.
Decision-tree case expressions may test values of any type. If
the test expression is a type with constructors, then the
patterns may be expressed using the constructors applied to
arguments, as for example SOME s in the example above. A free
variable within the constructor pattern, for example s in the
pattern SOME s, becomes bound to the corresponding value within
the value of the test expression, and can be used within the
associated result expression for that pattern.
In addition to the constructors of standard types in HOL, constructor patterns may also be used for types created by use of the datatype definition facility described in Section 7.2, including user-defined types.
Whether or not the test expression is a type with constructors,
the patterns may be expressed using the appropriate literals of
that type, if any such literals exist. A complex pattern may
contain either or both of literals and constructor patterns
nested within it. However, literals and constructors may not be
mixed as alternatives of each other within the same case
expression, except insofar as a particular pattern may be both a
literal and also a (0-ary) constructor of its type, as for
example 0 (zero) is both a literal and a constructor of the
type num. The session below demonstrates the way in which
such an improper mixture is misinterpreted. In this pattern, the
constructor pattern SUC m is given as an alternative to the
literal patterns 1 and 2. This makes this attempted case
expression invalid. Deleting either group of rows would resolve
the conflict, and make the expression valid. Note that the
pattern 0 is acceptable to either group.
> “case n of
0 => "none"
| 1 => "one"
| 2 => "two"
| SUC m => "many"”;
Exception- HOL_ERR
(at Pmatch.mk_case: case expression mixes literals with non-literals.) raised
Patterns can be nested as well, as shown in the first example
below, where the function parents returns a pair containing the
person's father and/or mother, where each is represented by
NONE if deceased. This shows the nesting of option patterns
within a pair pattern, and also the use of a wildcard _ to
match the cases not given.
case parents(john) of
(NONE,NONE) => "orphan"
| _ => "not an orphan"
A second example, using nested literal patterns and a wildcard in each row:
case a of
(1, y, z) => y + z
| (x, 2, z) => x - z
| (x, y, 3) => x * y
Since decision-tree case expressions are compiled internally to
a decision tree, the result of this compilation might look quite
different from the input. Rows might be reordered or modified,
there might be several new rows generated, and new variables or
the ARB constant may also be introduced to properly represent
the case expression. Moreover, the exact result depends on
complicated heuristics to decide which case-split to perform
next in the decision tree. For non-trivial case expressions the
result can be hard to predict.
For example, consider the second case expression above. Using the default heuristic, this compiles to a reasonably small decision tree that is pretty-printed well. The exact combination of equality tests with if-then-else and the case constant for products that this term produces can be seen by turning off the case-expression pretty-printer:
> set_trace "pp_cases" 0; ... output elided ...
> “case a of
(1,y,z) => y + z
| (x,2,z) => x - z
| (x,y,3) => x * y”;
<<HOL message: mk_functional:
pattern completion has added 1 clause to the original specification.>>
val it =
“pair_CASE a
(λv v1.
pair_CASE v1
(λy z.
literal_case
(λx.
if x = 1 then y + z
else
literal_case
(λy'.
if y' = 2 then x − z
else
literal_case
(λv10. if v10 = 3 then x * y' else ARB)
z) y) v))”: term
Other heuristics result in more complicated terms:
> Pmatch.set_classic_heuristic (); ... output elided ...
> “case a of
(1,y,z) => y + z
| (x,2,z) => x - z
| (x,y,3) => x * y”;
<<HOL message: mk_functional:
pattern completion has added 5 clauses to the original specification.>>
val it =
“case a of
(1,2,3) => 2 + 3
| (1,2,v10) => 2 + v10
| (1,y,3) => y + 3
| (1,y,z) => y + z
| (x,2,3) => x − 3
| (x,2,z') => x − z'
| (x,y',3) => x * y'
| (x,y',v24) => ARB”: term
> PmatchHeuristics.set_heuristic PmatchHeuristics.pheu_last_col; ... output elided ...
> “case a of
(1,y,z) => y + z
| (x,2,z) => x - z
| (x,y,3) => x * y”;
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
val it =
“case a of
(1,y,z) => y + z
| (x,2,3) => x − 3
| (x,y',3) => x * y'
| (x,2,z') => x − z'
| (x,v13,z') => ARB”: term
> Pmatch.set_default_heuristic (); ... output elided ...
> “case a of
(1,y,z) => y + z
| (x,2,z) => x - z
| (x,y,3) => x * y”;
<<HOL message: mk_functional:
pattern completion has added 1 clause to the original specification.>>
val it =
“case a of
(1,y,z) => y + z
| (x,2,z) => x − z
| (x,y',3) => x * y'
| (x,y',v10) => ARB”: term
This is just a brief description of some of the expressive capabilities of the case expression with patterns. Many more examples of patterns are provided in Section 7.6 on the definition of recursive functions.
Pmatch case expressions
The library patternMatchesLib supports another form of case
expression. If pmatch syntax is enabled (via
patternMatchesSyntax.temp_enable_pmatch() or
enable_pmatch()), the pmatch keyword can be used to parse
Pmatch-based terms. If we turn off the library's
pretty-printing, we can see how the example expression we used
earlier is rendered:
> patternMatchesSyntax.temp_enable_pmatch(); ... output elided ...
> set_trace "use pmatch_pp" 0; ... output elided ...
> “pmatch a of
(1, y, z) => y + z
| (x, 2, z) => x - z
| (x, y, 3) => x * y”;
val it =
“PMATCH a
[PMATCH_ROW (λ(y,z). (1,y,z)) (λ(y,z). T) (λ(y,z). y + z);
PMATCH_ROW (λ(x,z). (x,2,z)) (λ(x,z). T) (λ(x,z). x − z);
PMATCH_ROW (λ(x,y). (x,y,3)) (λ(x,y). T) (λ(x,y). x * y)]”: term
One can see that in contrast to decision-tree case expressions the internal representation of Pmatch case expressions is very close to the input. No fancy parsing is required to turn the input into the internal representation, and conversely, printing (when enabled) can easily produce the syntax that the user chose as input.
Pmatch case expressions are more expressive than decision-tree based ones. The syntax allowed for decision-tree case expressions is a subset of the syntax of Pmatch ones. In addition, Pmatch case expressions support guards. Moreover, arbitrary terms instead of just ones using literals and constructors can be used as patterns. One has full control over the variables bound by patterns. Bound variables can even be used more than once in a pattern.
$$ \begin{aligned} \mathit{term} & ::= \mathtt{pmatch}\;\mathit{term}\;\mathtt{of}\;\mathtt{|}^?\;\mathit{clause}\;(\mathtt{|}\;\mathit{clause})^*\\ \mathit{clause} & ::= \mathit{vardecl}^?\;\mathit{term}\; (\mathtt{when}\;\mathit{term})^? \;\mathtt{=>}\; \mathit{term} \\ \mathit{vardecl} & ::= \mathtt{(}\mathit{vars}^?\mathtt{)}\;\mathtt{.|}\;\;\;\mid\;\;\;\mathit{vars}\;\mathtt{.|}\\ \mathit{vars} & ::= \mathit{var}\;\;\;\mid\;\;\;\mathit{var}\;\mathtt{,}\;\mathit{vars} \end{aligned} $$
If a when-guard is omitted, it defaults to true (T).
Omitting the declaration of variables bound by a pattern means
that all variables used in the pattern are bound (as with the
decision-tree syntax). Variables whose names start with an
underscore are always bound, no matter whether they appear in
the list of bound variables. This is convenient for using
wildcard notations.
These extensions of the basic case expression syntax allow the expression of some interesting concepts using case expressions. One can for example express division with remainder using Pmatch case expressions:
!n c.
0 < c ==>
((pmatch n of (q,r) .| q * c + r when r < c => (q,r)) =
(n DIV c,n MOD c))
Notice that
- the guard is used to make the match unique;
- listing the bound variables of the pattern
q * c + rexplicitly allowscto not be bound by the pattern; and - the pattern (of form $qc + r$) would not be supported by decision-tree case expressions because it is not a constructor pattern.
Another interesting option is to use bound variables multiple
times. The following case expression states for example that a
list l starts with two copies of the same element:
pmatch l of | x::x::_ => T | _ => F
The price for this increased expressive power and the simpler,
more trustworthy parsing and pretty-printing is that the semantic
complexity now needs to be dealt with inside the logic. The
patternMatchesLib library provides the necessary machinery in
the form or conversions, rules, simpsets, and other technology.
For example, patternMatchesLib enhances bossLib's standard
simpsets with the conversions to deal with Pmatch case
expressions. Therefore, in practice Pmatch case expressions
are as convenient to use as decision-tree based case expressions.
In fact, the explicit case expression structure provided by
Pmatch case expressions allows simplifications not easily
possible for decision-tree case expressions. The standard tools
can only (partially) evaluate decision-tree case expressions.
This evaluation usually destroys the case expression view. This
is illustrated by the following example, which adds a row that is
subsumed by a later one to our running example:
> SIMP_CONV (srw_ss()) []
“pmatch (x,y,z) of
(1,y,z) => y + z
| (x,2,4) => x - 4 (* subsumed by next row *)
| (x,2,z) => x - z
| (x,y,3) => x * y”;
val it =
⊢ (pmatch (x,y,z) of
(1,y,z) => y + z
| (x,2,4) => x − 4
| (x,2,z) => x − z
| (x,y,3) => x * y) =
pmatch (x,y,z) of (1,y,z) => y + z | (x,2,z) => x − z | (x,y,3) => x * y:
thm
> SIMP_CONV (srw_ss()) []
“case (x,y,z) of
(1,y,z) => y + z
| (x,2,4) => x - 4
| (x,2,z) => x - z
| (x,y,3) => x * y”;
<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
val it =
⊢ (case (x,y,z) of
(1,y,z) => y + z
| (x,2,4) => x − 4
| (x,2,3) => x − 3
| (x,2,z') => x − z'
| (x,y',3) => x * y'
| (x,y',v14) => ARB) =
if x = 1 then y + z
else if y = 2 then
if z = 4 then x − 4 else if z = 3 then x − 3 else x − z
else if z = 3 then x * y
else ARB: thm
There are many more tools for working with Pmatch case
expressions. There are, for example, tools for removing
multiple variable binding or guards. One can translate between
Pmatch and decision-tree case expressions. There are tools for
proving exhaustiveness of Pmatch case expressions or for
removing redundant rows. For more details, please consult the
patternMatchesLib documentation in Section
8.9.
Recursive Functions
HOL provides a function definition mechanism based on the
wellfounded recursion theorem proved in relationTheory, discussed
in Section 5.5.3. With the Definition syntax, users
provide a high-level, possibly recursive, specification of a
function, and HOL attempts to define the function in the logic.
This technology may be used to define abbreviations, recursive
functions, and mutually recursive functions. An induction theorem
may be generated as a by-product of this activity. This induction
theorem follows the recursion structure of the function, and may
be useful when proving properties of the function. The definition
technology is not always successful in attempting to make the
specified definition, usually because an automatic termination
proof fails; in that case, another entrypoint, Hol_defn, which
defers the termination proof to the user, can be used. Once a
termination argument is found, it can be provided as part of the
final Definition syntax (See Section 7.1 for
more details.) The technology underlying Definition and
Hol_defn is explained in detail in Slind (Slind 1999).
For example,
> Definition last0_def:
(last0 [] = 0) /\
(last0 [x] = x) /\
(last0 (h::t) = last0 t)
End
Equations stored under "last0_def".
Induction stored under "last0_ind".
val last0_def =
⊢ last0 [] = 0 ∧ (∀x. last0 [x] = x) ∧
∀v3 v2 h. last0 (h::v2::v3) = last0 (v2::v3): thm
The fn-spec in the syntax of Definition and Hol_defn is
quoted syntax representing a conjunction of equations. The
specified function(s) may be phrased using ML-style
pattern-matching. The fn-spec should conform with the grammar
in Table 7.6.
$$ \begin{aligned} \mathit{fn\text{-}spec} & ::= \mathit{eqn} \\ & \;\mid\; (\mathit{eqn}) \wedge \mathit{fn\text{-}spec} \\[2pt] \mathit{eqn} & ::= \mathit{alphanumeric}\ \mathit{pat} \ldots \mathit{pat} = \mathit{term} \\[2pt] \mathit{pat} & ::= \mathit{variable} \\ & \;\mid\; \mathit{wildcard} \\ & \;\mid\; \mathit{cname} \\ & \;\mid\; (\mathit{cname}_n\ \mathit{pat}_1 \ldots \mathit{pat}_n) \\[2pt] \mathit{cname} & ::= \mathit{alphanumeric}\ \mid\ \mathit{symbolic} \\[2pt] \mathit{wildcard} & ::= \mathtt{\_\_} \\ & \;\mid\; \mathtt{\_\_}\,\mathit{wildcard} \end{aligned} $$
Table: Syntax of Function Declaration.
Pattern expansion
In general, Definition attempts to derive exactly the specified
conjunction of equations. However, the rich syntax of patterns
allows some ambiguity. For example, the input
Definition f_def:
(f 0 _ = 1) /\
(f _ 0 = 2)
End
is ambiguous at f 0 0: should the result be 1 or 2? This
ambiguity is dealt with in the usual way for compilers and
interpreters for functional languages: namely, the conjunction of
equations is treated as being applied left-conjunct first, followed
by processing the right conjunct. Therefore, in the example above,
the value of f 0 0 is 1. In the implementation, ambiguities
arising from such overlapping patterns are systematically
translated away in a pre-processing step.
Another case of ambiguity in patterns is shown above: the
specification is incomplete since it does not tell how f should
behave when applied to two non-zero arguments: e.g.,
f (SUC m) (SUC n). In the implementation, such missing clauses
are filled in, and have the value ARB. This `pattern-completion'
step is a way of turning descriptions of partial functions into
total functions suitable for HOL. However, since the user has not
completely specified the function, the system takes that as a hint
that the user is not interested in using the function at the
missing-but-filled-in clauses, and so such clauses are dropped from
the final theorem.
In summary, Definition will derive the unambiguous and complete
equations
f 0 v0 = 1 /\ f (SUC v3) 0 = 2 /\ f (SUC v1) (SUC v2) = ARB
from the above ambiguous and incomplete equations. The odd-looking variable names are due to the pre-processing steps described above. Depending on the analysis of the pattern-matching (see Section 7.5 for how this is done, and how it can be tweaked), the theorem returned from a definition may look rather unlike the original input. In this particular case, the post-processing needs only drop the last conjunct, which was not part of the original user-specification, yielding:
val f_def = ⊢ ∀v3 v0. f 0 v0 = 1 ∧ f (SUC v3) 0 = 2: thm
Termination
When processing the specification of a recursive function,
Definition must perform a termination proof. It automatically
constructs termination conditions for the function, and invokes a
termination prover in an attempt to prove the termination
conditions. If the function is primitive recursive, in the sense
that it exactly follows the recursion pattern of a previously
declared HOL datatype, then this proof always succeeds, and
Definition stores the derived equations in the current theory
segment. Otherwise, the function is not an instance of primitive
recursion, and the termination prover may succeed or fail. If the
automatic termination proof fails, the user-provided termination
argument (if any) after the Termination keyword is attempted. If
this also fails, then the Definition fails. If it succeeds, then
Definition stores the specified equations in the current theory
segment. An induction theorem customized for the defined function
is also stored in the current segment. Note, however, that an
induction theorem is not stored for primitive recursive functions,
since that theorem would be identical to the induction theorem
resulting from the declaration of the datatype.
Part of the process of the automatic termination proof involves
the use of “termination simplification” theorems. These encode
facts about the way in which arguments to desired functions may be
smaller than originals. For example, with the theory of
fixed-width words (see Section 5.3.8) in the
context, the theorem WORD_PRED_THM is included in this set:
wordsTheory.WORD_PRED_THM
⊢ ∀m. m ≠ words$n2w 0 ⇒
words$w2n (words$word_sub m (words$n2w 1)) < words$w2n m
If a function is defined recursively with a word argument being
decremented with every call, including this theorem will let the
automatic procedure prove termination.
The set of theorems used in this way can be augmented by using the
tfl_termsimp theorem attribute when a theorem is proved.
Storing definitions in the theory segment
The name given in the use of the Definition syntax is used both
to store the definition in the current theory and is also bound to
the same theorem within the ML environment. If there is an
associated induction theorem, its name is derived as follows:
- If the principal name ends with
_defor with_DEF, then the induction theorem is the same as the principal name with the suffix replaced by_indor_INDrespectively. - Otherwise, the induction theorem is the principal name with
_indadded as a suffix. - Finally, the user may override these choices by adding an
induction_thm=name attribute to the principal name.
Function definition examples
We will give a number of examples that display the range of
functions that may be defined with Definition. First, we have a
recursive function that uses “destructors” in the recursive call.
> Definition fact_def:
fact x = if x = 0 then 1 else x * fact(x-1)
End
Equations stored under "fact_def".
Induction stored under "fact_ind".
val fact_def = ⊢ ∀x. fact x = if x = 0 then 1 else x * fact (x − 1): thm
Since fact is not primitive recursive, an induction theorem for
fact is generated and stored in the current theory.
> fact_ind; (* DB.fetch "-" "fact_ind" would also work *)
val it = ⊢ ∀P. (∀x. (x ≠ 0 ⇒ P (x − 1)) ⇒ P x) ⇒ ∀v. P v: thm
Next we have a recursive function with relatively complex
pattern-matching. We use the induction= “attribute” to require a
non-standard name for the generated induction theorem.
> Definition flatten[induction=flat_ind]:
(flatten [] = [])
/\ (flatten ([]::rst) = flatten rst)
/\ (flatten ((h::t)::rst) = h::flatten(t::rst))
End
<<HOL message: inventing new type variable names: 'a>>
Equations stored under "flatten".
Induction stored under "flat_ind".
val flatten =
⊢ flatten [] = [] ∧ (∀rst. flatten ([]::rst) = flatten rst) ∧
∀t rst h. flatten ((h::t)::rst) = h::flatten (t::rst): thm
> flat_ind;
val it =
⊢ ∀P. P [] ∧ (∀rst. P rst ⇒ P ([]::rst)) ∧
(∀h t rst. P (t::rst) ⇒ P ((h::t)::rst)) ⇒
∀v. P v: thm
Next we define a curried recursive function, which uses wildcard expansion and pattern-matching pre-processing.
> Definition min_def: (min (SUC x) (SUC y) = min x y + 1)
/\ (min ____ ____ = 0)
End
<<HOL message: mk_functional:
pattern completion has added 1 clause to the original specification.>>
Equations stored under "min_def".
Induction stored under "min_ind".
val min_def =
⊢ (∀y x. min (SUC x) (SUC y) = min x y + 1) ∧ (∀v1. min 0 v1 = 0) ∧
∀v3. min (SUC v3) 0 = 0: thm
Next we make a primitive recursive definition. Note that no induction theorem is generated in this case.
> Definition filter:
(filter P [] = [])
/\ (filter P (h::t) = if P h then h::filter P t
else filter P t)
End
<<HOL message: inventing new type variable names: 'a>>
Definition has been stored under "filter"
val filter =
⊢ (∀P. filter P [] = []) ∧
∀P h t. filter P (h::t) = if P h then h::filter P t else filter P t: thm
Definition may also be used to define mutually recursive
functions. For example, we can define a datatype of propositions
and a function for putting a proposition into negation normal form
as follows. First we define a datatype, named prop, of boolean
formulas:
> Datatype:
prop = VARp 'a | NOTp prop | ANDp prop prop
| ORp prop prop
End
<<HOL message: Defined type: "prop">>
Then two mutually recursive functions nnfpos and nnfneg are
defined:
> Definition nnfpos_def:
(nnfpos (VARp x) = VARp x)
/\ (nnfpos (NOTp p) = nnfneg p)
/\ (nnfpos (ANDp p q) = ANDp (nnfpos p) (nnfpos q))
/\ (nnfpos (ORp p q) = ORp (nnfpos p) (nnfpos q))
/\ (nnfneg (VARp x) = NOTp (VARp x))
/\ (nnfneg (NOTp p) = nnfpos p)
/\ (nnfneg (ANDp p q) = ORp (nnfneg p) (nnfneg q))
/\ (nnfneg (ORp p q) = ANDp (nnfneg p) (nnfneg q))
End
<<HOL message: inventing new type variable names: 'a>>
Equations stored under "nnfpos_def".
Induction stored under "nnfpos_ind".
val nnfpos_def =
⊢ (∀x. nnfpos (VARp x) = VARp x) ∧ (∀p. nnfpos (NOTp p) = nnfneg p) ∧
(∀q p. nnfpos (ANDp p q) = ANDp (nnfpos p) (nnfpos q)) ∧
(∀q p. nnfpos (ORp p q) = ORp (nnfpos p) (nnfpos q)) ∧
(∀x. nnfneg (VARp x) = NOTp (VARp x)) ∧
(∀p. nnfneg (NOTp p) = nnfpos p) ∧
(∀q p. nnfneg (ANDp p q) = ORp (nnfneg p) (nnfneg q)) ∧
∀q p. nnfneg (ORp p q) = ANDp (nnfneg p) (nnfneg q): thm
Definition may also be used to define non-recursive functions:
> Definition fdef: fdef x (y,z) = (x + 1 = y DIV z)
End
Definition has been stored under "fdef"
val fdef = ⊢ ∀x y z. fdef x (y,z) ⇔ x + 1 = y DIV z: thm
Finally, Definition may also be used to define non-recursive
functions with complex pattern-matching. The pattern-matching
pre-processing of Definition can be convenient for this purpose,
but can also generate a large number of equations. It may also
return theorems that do not look quite like what was originally
input. For more on this, see the discussion of case expressions
(into which the clauses in a Definition are converted internally)
in Section 7.5.
When termination is not automatically proved
If the termination proof for a prospective definition fails, the
invocation of the definitional machinery fails. In such
situations, the user must supply a termination argument explicitly.
The primitive machinery for beginning this operation is the ML
function Hol_defn:
Hol_defn : string -> term quotation -> Defn.defn
Hol_defn makes the requested definition, but defers the proof of
termination to the user. For setting up termination proofs, there
are several useful entrypoints, namely
Defn.tgoal : Defn.defn -> GoalstackPure.proofs
Defn.tprove : Defn.defn * tactic -> thm * thm
Defn.tgoal is analogous to set_goal and Defn.tprove is
analogous to prove. Thus, Defn.tgoal is used to take the
result of Hol_defn and set up a goal for proving termination of
the definition.
Example
An invocation of Define on the following equations for Quicksort
will currently fail, since the termination proof is currently
beyond the capabilities of the naive termination prover. Instead,
we make an application of Hol_defn:
> val qsort_defn =
Hol_defn "qsort"
`(qsort ord [] = []) /\
(qsort ord (h::t) =
qsort ord (FILTER (\x. ord x h) t)
++ [h] ++
qsort ord (FILTER (\x. ~(ord x h)) t))`;
<<HOL message: inventing new type variable names: 'a>>
val qsort_defn =
HOL function definition (recursive)
Equation(s) :
[...] ⊢ qsort ord [] = []
[...]
⊢ qsort ord (h::t) =
qsort ord (FILTER (λx. ord x h) t) ⧺ [h] ⧺
qsort ord (FILTER (λx. ¬ord x h) t)
Induction :
[...]
⊢ ∀P. (∀ord. P ord []) ∧
(∀ord h t.
P ord (FILTER (λx. ¬ord x h) t) ∧ P ord (FILTER (λx. ord x h) t) ⇒
P ord (h::t)) ⇒
∀v v1. P v v1
Termination conditions :
0. ∀t h ord. R (ord,FILTER (λx. ¬ord x h) t) (ord,h::t)
1. ∀t h ord. R (ord,FILTER (λx. ord x h) t) (ord,h::t)
2. WF R: DefnBase.defn
which returns a value of type defn, but does not try to prove
termination.
The type defn has a prettyprinter installed for it: the above
output is typical, showing the components of a defn in an
understandable format. Although it is possible to directly work
with elements of type defn, it is more convenient to invoke
Defn.tgoal, which sets up a termination proof in a goalstack.
> Defn.tgoal qsort_defn;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
∃R. WF R ∧ (∀t h ord. R (ord,FILTER (λx. ¬ord x h) t) (ord,h::t)) ∧
∀t h ord. R (ord,FILTER (λx. ord x h) t) (ord,h::t)
The goal is to find a wellfounded relation on the arguments to
qsort and show that the arguments to qsort are in the
relation.
The function WF_REL_TAC is almost invariably used at this point
to initiate the termination proof. Clearly, qsort terminates
because the list argument gets shorter. Invoking WF_REL_TAC with
the appropriate measure function results in two subgoals, both of
which are easy to prove.
> e (WF_REL_TAC `measure (LENGTH o SND)`);
OK..
1 subgoal:
val it =
(∀t h ord. LENGTH (FILTER (λx. ¬ord x h) t) < LENGTH (h::t)) ∧
∀t h ord. LENGTH (FILTER (λx. ord x h) t) < LENGTH (h::t)
Execution of WF_REL_TAC has automatically proved the
wellfoundedness of the termination relation
measure (LENGTH o SND) and the remainder of the goal has been
simplified into a pair of easy goals.
Once both goals are proved, we can encapsulate the
termination proof/tactic into the Termination section of a
Definition. As long as the tactic does indeed prove the
termination conditions, the recursion equations and induction
theorem are stored in the current theory segment before the
recursion equations are returned:
> Definition qsort_def:
(qsort ord [] = []) /\
(qsort ord (h::t) =
qsort ord (FILTER (\x. ord x h) t) ++ [h] ++
qsort ord (FILTER (\x. ~(ord x h)) t))
Termination
WF_REL_TAC `measure (LENGTH o SND)` THEN cheat
End
<<HOL message: inventing new type variable names: 'a>>
Equations stored under "qsort_def".
Induction stored under "qsort_ind".
val qsort_def =
⊢ (∀ord. qsort ord [] = []) ∧
∀t ord h.
qsort ord (h::t) =
qsort ord (FILTER (λx. ord x h) t) ⧺ [h] ⧺
qsort ord (FILTER (λx. ¬ord x h) t): thm
As we have not specified a special name for it, the custom
induction theorem for our function can be obtained under the name
qsort_ind, or by using fetch, which returns named elements in
the specified theory.2
> DB.fetch "-" "qsort_ind";
val it =
⊢ ∀P. (∀ord. P ord []) ∧
(∀ord h t.
P ord (FILTER (λx. ¬ord x h) t) ∧ P ord (FILTER (λx. ord x h) t) ⇒
P ord (h::t)) ⇒
∀v v1. P v v1: thm
The induction theorem produced by Definition can be applied by
recInduct. See the bossLib section of the Libraries chapter
for details.
Techniques for proving termination
There are two problems to deal with when trying to prove termination. First, one has to understand, intuitively and then mathematically, why the function under consideration terminates. Second, one must be able to phrase this in HOL. In the following, we shall give a few examples of how this is done.
There are a number of basic and advanced means of specifying wellfounded relations. The most common starting point for dealing with termination problems for recursive functions is to find some function, known as a measure under which the arguments of a function call are larger than the arguments to any recursive calls that result.
For a very simple starter example, consider the following definition of a function that computes the greatest common divisor of two numbers:
> val gcd_defn =
Hol_defn "gcd"
`(gcd (0,n) = n) /\
(gcd (m,n) = gcd (n MOD m, m))`;
val gcd_defn =
HOL function definition (recursive)
Equation(s) :
[..] ⊢ gcd (0,n) = n
[..] ⊢ gcd (SUC v2,n) = gcd (n MOD SUC v2,SUC v2)
Induction :
[..]
⊢ ∀P. (∀n. P (0,n)) ∧ (∀v2 n. P (n MOD SUC v2,SUC v2) ⇒ P (SUC v2,n)) ⇒
∀v v1. P (v,v1)
Termination conditions :
0. ∀v2 n. R (n MOD SUC v2,SUC v2) (SUC v2,n)
1. WF R: DefnBase.defn
> Defn.tgoal gcd_defn;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
∃R. WF R ∧ ∀v2 n. R (n MOD SUC v2,SUC v2) (SUC v2,n)
The invocation gcd(m,n) recurses in its first argument, and
since we know that m is not 0, it is the case that n MOD m is
smaller than m. The way to phrase the termination of gcd in
HOL is to use a measure function to map from the domain of
gcd — a pair of numbers — to a number. The definition of
measure in HOL is equivalent to
prim_recTheory.measure_thm
⊢ ∀f x y. measure f x y ⇔ f x < f y
Now we must pick out the argument position to measure and invoke
WF_REL_TAC:
> e (WF_REL_TAC ‘measure FST’);
OK..
val it =
Initial goal proved.
⊢ (gcd (0,n) = n ∧ gcd (SUC v2,n) = gcd (n MOD SUC v2,SUC v2)) ∧
∀P. (∀n. P (0,n)) ∧ (∀v2 n. P (n MOD SUC v2,SUC v2) ⇒ P (SUC v2,n)) ⇒
∀v v1. P (v,v1): proof
The built-in reasoning then suffices to prove the remaining goal.
Weighting functions
Sometimes one needs a measure function that is itself recursive.
For example, consider a type of binary trees and a function that
linearizes trees. The algorithm works by rotating the tree until
it gets a LeafB in the left branch, then it recurses into the
right branch. At the end of execution the tree has been
linearized.
> Datatype: btreeB = LeafB | BrhB btreeB btreeB
End ... output elided ...
> val Unbal_defn =
Hol_defn "Unbal"
`(Unbal LeafB = LeafB)
/\ (Unbal (BrhB LeafB bt) = BrhB LeafB (Unbal bt))
/\ (Unbal (BrhB (BrhB bt1 bt2) bt) = Unbal (BrhB bt1 (BrhB bt2 bt)))`;
val Unbal_defn =
HOL function definition (recursive)
Equation(s) :
[...] ⊢ Unbal LeafB = LeafB
[...] ⊢ Unbal (BrhB LeafB bt) = BrhB LeafB (Unbal bt)
[...] ⊢ Unbal (BrhB (BrhB bt1 bt2) bt) = Unbal (BrhB bt1 (BrhB bt2 bt))
Induction :
[...]
⊢ ∀P. P LeafB ∧ (∀bt. P bt ⇒ P (BrhB LeafB bt)) ∧
(∀bt1 bt2 bt.
P (BrhB bt1 (BrhB bt2 bt)) ⇒ P (BrhB (BrhB bt1 bt2) bt)) ⇒
∀v. P v
Termination conditions :
0. ∀bt bt2 bt1. R (BrhB bt1 (BrhB bt2 bt)) (BrhB (BrhB bt1 bt2) bt)
1. ∀bt. R bt (BrhB LeafB bt)
2. WF R: DefnBase.defn
The termination conditions above can be turned into an interactive
goal with Defn.tgoal:
> Defn.tgoal Unbal_defn;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
∃R. WF R ∧
(∀bt bt2 bt1. R (BrhB bt1 (BrhB bt2 bt)) (BrhB (BrhB bt1 bt2) bt)) ∧
∀bt. R bt (BrhB LeafB bt)
Since the size of the tree is unchanged in the last clause in the
definition of Unbal, a simple size measure will not work.
Instead, we can assign weights to nodes in the tree such that the
recursive calls of Unbal decrease the total weight in every
case. One such assignment is
> Definition Weight_def:
(Weight (LeafB) = 0) /\
(Weight (BrhB x y) = (2 * Weight x) + (Weight y) + 1)
End
Definition has been stored under "Weight_def"
val Weight_def =
⊢ Weight LeafB = 0 ∧ ∀x y. Weight (BrhB x y) = 2 * Weight x + Weight y + 1:
thm
Now we can invoke WF_REL_TAC:
> e (WF_REL_TAC `measure Weight`);
OK..
1 subgoal:
val it =
(∀bt bt2 bt1.
Weight (BrhB bt1 (BrhB bt2 bt)) < Weight (BrhB (BrhB bt1 bt2) bt)) ∧
∀bt. Weight bt < Weight (BrhB LeafB bt)
Both conjuncts of this goal are quite easy to prove.
The technique of “weighting” nodes in a datatype in order to prove termination also goes by the name of polynomial interpretation. It must be admitted that finding the correct weighting for a termination proof is more an art than a science. Typically, one makes a guess and then tries the termination proof to see if it works.
Lexicographic combinations
Occasionally, there's a combination of factors that complicate the termination argument. For example, the following specification describes a naive pattern matching algorithm on strings (represented as lists here). The function takes four arguments: the first, $p$, is the remainder of the pattern being matched. The second, $\mathit{rst}$, is the remainder of the string being searched. The third argument, $p_0$, holds the original pattern to be matched. The fourth argument, $s$, is the string being searched.
> val match_defn =
Hol_defn "match"
`(match [] __ __ __ = T) /\
(match __ [] __ __ = F) /\
(match (a::pp) (b::ss) p0 s =
if a=b then match pp ss p0 s
else
if NULL(s) then F
else
match p0 (TL s) p0 (TL s))`; ... output elided ...
> Definition Match_def: Match pat str = match pat str pat str
End
<<HOL message: inventing new type variable names: 'a>>
Definition has been stored under "Match_def"
val Match_def = ⊢ ∀pat str. Match pat str ⇔ match pat str pat str: thm
The first clause of the definition states that if $p$ becomes
exhausted, then a match has been found; the function returns T.
The second clause represents the case where $s$ becomes exhausted
but $p$ is not, in which case the function returns F. The
remaining case is when there's more searching to do; the function
checks if the head of the pattern $p$ is the same as the head of
$\mathit{rst}$. If yes, then the search proceeds recursively,
using the tail of $p$ and the tail of $\mathit{rst}$. If no, that
means that $p$ has failed to match, so the algorithm advances one
character ahead in $s$ and starts matching from the beginning of
$p_0$. If $s$ is empty, however, then we return F. Note that
$\mathit{rst}$ and $s$ both represent the string being searched:
$\mathit{rst}$ is a “local” version of $s$: we recurse into
$\mathit{rst}$ as long as there are matches with the pattern $p$.
However, if the search eventually fails, then $s$, which
“remembers” where the search started from, is used to restart the
search.
So much for the behaviour of the function. Why does it terminate?
There are two recursive calls. The first call reduces the size of
$p$ and $\mathit{rst}$, and leaves the other arguments unchanged.
The second call can increase the size of $p$ and $\mathit{rst}$,
but reduces the size $s$. This is a classic situation in which to
use a lexicographic ordering: some arguments to the function are
reduced in some recursive calls, and some others are reduced in
other recursive calls. Recall that LEX is an infix operator,
defined in pairTheory as follows:
pairTheory.LEX_DEF
⊢ ∀R1 R2. R1 LEX R2 = (λ(s,t) (u,v). R1 s u ∨ s = u ∧ R2 t v)
In the second recursive call, the length of s is reduced, and in
the first it stays the same. This motivates having the length of
the $s$ be the first component of the lexicographic combination,
and the length of $\mathit{rst}$ as the second component.
Formally, we want to map from the four-tuple of arguments into a
lexicographic combination of relations. This is enabled by
inv_image from relationTheory:
relationTheory.inv_image_def
⊢ ∀R f. inv_image R f = (λx y. R (f x) (f y))
The desired relation maps from the four-tuple of arguments into a pair of numbers $(m,n)$, where $m$ is the length of the fourth argument, and $n$ is the length of the second argument. These lengths are then compared lexicographically with respect to less-than ($<$).
> Defn.tgoal match_defn; ... output elided ...
> e (WF_REL_TAC `inv_image($< LEX $<) (\(w,x,y,z). (LENGTH z,LENGTH x))`);
OK..
1 subgoal:
val it =
(∀ss s b a.
a ≠ b ∧ ¬NULL s ⇒
LENGTH (TL s) < LENGTH s ∨
LENGTH (TL s) = LENGTH s ∧ LENGTH (TL s) < LENGTH (b::ss)) ∧
∀ss a. LENGTH ss < LENGTH (a::ss)
The first conjunct needs a case-split on s before it is proved by
rewriting, and the second is also easy to prove by rewriting.
How termination conditions are synthesized
It is occasionally important to understand, at least in part, how
Hol_defn constructs termination constraints. In some cases, it
is even necessary for users to influence this process in order to
have correct termination constraints extracted. The process is
driven by so-called congruence theorems for particular HOL
constants. For example, consider the following recursive
definition of factorial:
fact n = if n=0 then 1 else n * fact (n-1)
In the absence of knowledge of how the “if-then-else” construct
affects the context of recursive calls, Hol_defn would extract
the termination constraints:
0. WF R
1. !n. R (n - 1) n
which are unprovable, because the context of the recursive call
has not been taken account of. This example is in fact not a
problem for HOL, since the following congruence theorem is known
to Hol_defn:
|- !b b' x x' y y'.
(b = b') /\
(b' ==> (x = x')) /\
(~b' ==> (y = y')) ==>
((if b then x else y) = (if b' then x' else y'))
This theorem is understood by Hol_defn as an ordered sequence of
instructions to follow when the termination condition extractor
hits an “if-then-else”. The theorem is read as follows: when an
instance "if $B$then$X$else$Y$" is encountered while the
extractor traverses the function definition, do the following:
-
Traverse $B$ and extract termination conditions $\mathit{TCs}(B)$ from any recursive calls in it. This returns a theorem $\mathit{TCs}(B) \vdash B = B'$.
-
Assume $B'$ and extract termination conditions from any recursive calls in $X$. This returns a theorem $\mathit{TCs}(X) \vdash X = X'$.
-
Assume $\neg B'$ and extract termination conditions from any recursive calls in $Y$. This returns a theorem $\mathit{TCs}(Y) \vdash Y = Y'$.
-
By equality reasoning with (1), (2), and (3), derive the theorem $$\mathit{TCs}(B) \cup \mathit{TCs}(X) \cup \mathit{TCs}(Y) \vdash (\mathtt{if}\ B\ \mathtt{then}\ X\ \mathtt{else}\ Y) = (\mathtt{if}\ B'\ \mathtt{then}\ X'\ \mathtt{else}\ Y')$$
-
Replace "
if$B$then$X$else$Y$" by "if$B'$then$X'$else$Y'$".
The termination conditions are accumulated until the extraction
process finishes, and appear as hypotheses in the final result.
Thus the extracted termination conditions for fact are
0. WF R
1. !n. ~(n = 0) ==> R (n - 1) n
and are easy to prove. The notion of context of a recursive
call is defined by the set of congruence rules used in extracting
termination conditions. This set can be obtained by invoking
DefnBase.read_congs, and manipulated by DefnBase.add_cong,
DefnBase.drop_cong and DefnBase.export_cong. The “add” and
“drop” functions only affect the current state of the congruence
database; in contrast, the “export” function provides a way for
theories to specify that a particular theorem should be added to
the congruence database in all descendant theories.
Higher-order recursion and congruence rules
A “higher-order” recursion is one in which a higher-order function
is used to apply the recursive function to arguments. In order
for the correct termination conditions to be proved for such a
recursion, congruence rules for the higher order function must be
known to the termination condition extraction mechanism.
Congruence rules for common higher-order functions, e.g., MAP,
EVERY, and EXISTS for lists, are already known to the
mechanism. However, at times, one must manually prove and install
a congruence theorem for a new user-defined higher-order function.
For example, suppose we define a higher-order function SIGMA for
summing the results of a function in a list.
> Definition SIGMA_def:
(SIGMA f [] = 0) /\
(SIGMA f (h::t) = f h + SIGMA f t)
End ... output elided ...
We then use SIGMA in the definition of a function for summing the
results of a function in a arbitrarily (finitely) branching tree.
> Datatype: ltree = LNode 'a (ltree list)
End ... output elided ...
Defn.Hol_defn
"ltree_sigma"
`ltree_sigma f (LNode v tl) = f v + SIGMA (ltree_sigma f) tl`;
In this definition, SIGMA is applied to a partial application
(ltree_sigma f) of the function being defined. Such a situation
is called a higher-order recursion. Since the recursive call of
ltree_sigma is not fully applied, special efforts have to be
made to extract the correct termination conditions. Otherwise, the
following unhappy situation results:
<<HOL message: inventing new type variable names: 'a>>
val it =
HOL function definition (recursive)
Equation(s) :
[..] ⊢ ltree_sigma f (LNode v tl) = f v + SIGMA (λa. ltree_sigma f a) tl
Induction :
[..] ⊢ ∀P. (∀f v tl. (∀a. P f a) ⇒ P f (LNode v tl)) ⇒ ∀v v1. P v v1
Termination conditions :
0. ∀tl v f a. R (f,a) (f,LNode v tl)
1. WF R: defn
The termination conditions for ltree_sigma seem to require
finding a wellfounded relation R such that the pair (f,a) is
R-less than (f, LNode v tl). However, this is a hopeless
task, since there is no relation between a and LNode v tl,
besides the fact that they are both ltrees. The termination
condition extractor has not performed properly, because it didn't
know a congruence rule for SIGMA. Such a congruence theorem is
the following:
SIGMA_CONG =
|- !l1 l2 f g.
(l1=l2) /\ (!x. MEM x l2 ==> (f x = g x)) ==>
(SIGMA f l1 = SIGMA g l2)
Once Hol_defn has been told about this theorem, via DefnBase's
add_cong or export_cong functions, or by using a cong
attribute on a theorem when it is saved,
the termination conditions extracted for the definition are now
provable, since a is a proper subterm of LNode v tl.
> val _ = DefnBase.add_cong SIGMA_CONG;
> Defn.Hol_defn "ltree_sigma"
`ltree_sigma f (LNode v tl) = f v + SIGMA (ltree_sigma f) tl`;
<<HOL message: inventing new type variable names: 'a>>
val it =
HOL function definition (recursive)
Equation(s) :
[..] ⊢ ltree_sigma f (LNode v tl) = f v + SIGMA (λa. ltree_sigma f a) tl
Induction :
[..]
⊢ ∀P. (∀f v tl. (∀a. MEM a tl ⇒ P f a) ⇒ P f (LNode v tl)) ⇒ ∀v v1. P v v1
Termination conditions :
0. ∀v f tl a. MEM a tl ⇒ R (f,a) (f,LNode v tl)
1. WF R: defn
Recursion schemas
In higher order logic, very general patterns of recursion, known as recursion schemas or sometimes program schemas, can be defined. One example is the following:
$$ \mathsf{linRec}(x) = \mathtt{if}\;d(x)\;\mathtt{then}\;e(x)\;\mathtt{else}\;f(\mathsf{linRec}(g\;x)) $$
In this specification, the variables $d$, $e$, $f$, and $g$ are functions, that, when instantiated in different ways, allow $\mathsf{linRec}$ to implement different recursive functions. In this, $\mathsf{linRec}$ is like many other higher order functions. However, notice that if $d(x) = \mathsf{F}$, $f(x) = x+1$, and $g(x) = x$, then the resulting instantiation of $\mathsf{linRec}$ could be used to obtain a contradiction:
$$ \mathsf{linRec}(x) = \mathsf{linRec}(x) + 1 $$
This is not, however, derivable in HOL, because recursion schemas
are defined by instantiating the wellfounded recursion theorem,
and therefore certain abstract termination constraints arise that
must be satisfied before recursion equations can be used in an
unfettered manner. The entrypoint for defining a schema is
TotalDefn.DefineSchema, which can also be targeted by using the
schematic attribute with the Definition syntax.
On the $\mathsf{linRec}$ example it behaves as follows (note that
the schematic variables should only occur on the right-hand side
of the definition when making the definition of a schema):
> Definition linRec_def[schematic]:
linRec (x:'a) = if d(x) then e(x) else f(linRec(g x))
End
<<HOL message: inventing new type variable names: 'b>>
<<HOL message: Definition is schematic in the following variables:
"d", "e", "f", "g">>
<<HOL message: Unable to add linRec_def to global compset>>
Equations stored under "linRec_def".
Induction stored under "linRec_ind".
val linRec_def =
[..]
⊢ ∀x f e. linRec d e f g x = if d x then e x else f (linRec d e f g (g x)):
thm
The hypotheses of the returned theorem hold the abstract termination constraints. A similarly constrained induction theorem is also stored in the current theory segment.
> hyp linRec_def;
val it = [“∀x. ¬d x ⇒ R (g x) x”, “WF R”]: term list
These constraints are abstract, since they place termination
requirements on variables that have not yet been instantiated.
Once instantiations for the variables are found, then the
constraints may be eliminated by finding a suitable wellfounded
relation for R and then proving the other constraints.
Inductive Relations
Inductive definitions are made with the special Inductive syntax
form, which wraps the underlying function Hol_reln, which is in
turn found in the bossLib structure. The resulting definitions
and theorems are handled with functions defined in the library
IndDefLib. The Inductive syntax and Hol_reln function take a
term quotation as input and attempt to define the relations there
specified. The input term quotation must parse to a term that
conforms to the following grammar:
$$ \begin{aligned} \langle\mathit{inputFormat}\rangle & ::= \langle\mathit{clause}\rangle\;\land\; \langle\mathit{inputFormat}\rangle \;\mid\;\langle\mathit{clause}\rangle \\ \langle\mathit{clause}\rangle & ::= (\forall x_1 \dots x_n.\;\langle\mathit{hypothesis}\rangle \;\Rightarrow\;\langle\mathit{conclusion}\rangle) \\ & \;\mid\; (\forall x_1 \dots x_n.\;\langle\mathit{conclusion}\rangle) \\ \langle\mathit{conclusion}\rangle & ::= \langle\mathit{con}\rangle\;\mathit{sv}_1\;\mathit{sv}_2\dots \\ \langle\mathit{hypothesis}\rangle & ::= \text{any term} \\ \langle\mathit{con}\rangle & ::= \text{a new relation constant} \end{aligned} $$
The (optional) $\mathit{sv}_i$ terms that appear after a constant name are so-called “schematic variables”. The same variables must always follow all new constants throughout the definition. These variables and the names of the constants-to-be must not be quantified over in each $\langle\mathit{clause}\rangle$. A $\langle\mathit{clause}\rangle$ should have no other free variables. Any that occur will be universally quantified as part of the process of definition, and a warning message emitted. (Universal quantifiers at the head of the clause can be used to bind free variables, but it is also permissible to use existential quantification in the hypotheses. If a clause has no free variables, it is permissible to have no universal quantification.)
A successful invocation of this definitional principle returns three important theorems $\mathit{rules}$, $\mathit{ind}$ and $\mathit{cases}$. Each is also stored in the current theory segment.
-
$\mathit{rules}$ is a conjunction of implications that will be the same as the input term quotation; the theorem is saved under the name
<stem>_rules, where<stem>is the name of the first relation defined by the function (if usingHol_reln), or as provided by the user, when using theInductivesyntax. -
$\mathit{ind}$ is the induction principle for the relations, saved under the name
<stem>_ind. -
$\mathit{cases}$ is the so-called “cases” or “inversion” theorem for the relations, saved under the name
<stem>_cases. A cases theorem is of the form(!a0 .. an. R1 a0 .. an = <R1's first rule possibility> \/ <R1's second rule possibility> \/ ...) /\ (!a0 .. am. R2 a0 .. am = <R2's first rule possibility> \/ <R2's second rule possibility> \/ ...) /\ ...and is used to decompose an element in the relation into the possible ways of obtaining it by the rules.
If the “stem” of the first constant defined in a set of clauses is
such that resulting ML bindings in an exported theory file will
result in illegal ML, then the xHol_reln function should be
used. The xHol_reln function is analogous to the xDefine
function for defining recursive functions (see Section
7.6).
Alternatively, the Inductive syntax can be used, requiring the
user to specify the stem, but saving on verbosity: instead of
writing
val (foo_rules,foo_ind,foo_cases) = Hol_reln`
...
`;
one writes
Inductive foo:
...
End
where, as with other special syntaxes, the keywords (Inductive
and End) have to be in the leftmost column of the source file.
Additionally, users can automatically export each rule as a
theorem by assigning a name using the square-bracket syntax. The
appropriate format is [~Name:], where Name acts as the
placeholder for the rule name. Inside the square brackets, the
tilde (~) is optional; if included, it prefixes the exported
rule name with <stem>_. For instance, the following example
will export rules as rule1 and foo_rule2.
Inductive foo:
[rule1:]
...
[~rule2:]
...
...
End
Strong induction principles
So called “strong” versions of induction principles (in which
instances of the relation being defined appear as extra
hypotheses), are automatically proved when an inductive definition
is made.
The strong induction principle for a relation is used when the
Induct_on tactic is used.
Adding monotone operators
New constants may occur recursively throughout rules' hypotheses,
as long as it can be shown that the rules remain monotone with
respect to the new constants. Hol_reln automatically attempts
to prove such monotonicity results, using a set of theorems held
in a reference IndDefLib.the_monoset. Monotonicity theorems
must be of the form
$$ \mathit{cond}_1 \land \cdots \land \mathit{cond}_m \Rightarrow (\mathit{Op}\;\mathit{arg}_1 \dots \mathit{arg}_n \Rightarrow \mathit{Op}\;\mathit{arg}'_1 \dots \mathit{arg}'_n) $$
where each $\mathit{arg}$ and $\mathit{arg}'$ term must be a variable, and where there must be as many $\mathit{cond}_i$ terms as there are arguments to $\mathit{Op}$ that vary. Each $\mathit{cond}_i$ must be of the form
$$ \forall \vec{v}.\;\mathit{arg}\;\vec{v} \Rightarrow \mathit{arg}'\;\vec{v} $$
where the vector of variables $\vec{v}$ may be empty, and where the $\mathit{arg}$ and $\mathit{arg}'$ may actually be reversed (as in the rule for negation).
For example, the monotonicity rule for conjunction is
$$ (P \Rightarrow P') \land (Q \Rightarrow Q') \Rightarrow (P \land Q \Rightarrow P' \land Q') $$
The monotonicity rule for the EVERY operator in the theory of
lists (see Section 5.4.1), is
$$ (\forall x.\;P(x) \Rightarrow Q(x)) \Rightarrow (\mathtt{EVERY}\;P\;\ell \Rightarrow \mathtt{EVERY}\;Q\;\ell) $$
With a monotonicity result available for an operator such as
EVERY, it is then possible to write inductive definitions where
hypotheses include mention of the new relation as arguments to
the given operators.
Monotonicity results that the user derives may be stored in the
global the_monoset variable by using the export_mono function,
or the mono theorem attribute. This function takes a string
naming a theorem in the current theory segment, and adds that
theorem to the monotonicity theorems immediately, and in such a
way that this situation will also obtain when the current theory
is subsequently reloaded.
Examples
A simple example of defining two mutually recursive relations is the following:
> Inductive EVEN_ODD:
EVEN 0 /\
(!n. ODD n ==> EVEN (n + 1)) /\
(!n. EVEN n ==> ODD (n + 1))
End
val EVEN_ODD_cases =
⊢ (∀a0. EVEN a0 ⇔ a0 = 0 ∨ ∃n. a0 = n + 1 ∧ ODD n) ∧
∀a1. ODD a1 ⇔ ∃n. a1 = n + 1 ∧ EVEN n: thm
val EVEN_ODD_ind =
⊢ ∀EVEN' ODD'.
EVEN' 0 ∧ (∀n. ODD' n ⇒ EVEN' (n + 1)) ∧ (∀n. EVEN' n ⇒ ODD' (n + 1)) ⇒
(∀a0. EVEN a0 ⇒ EVEN' a0) ∧ ∀a1. ODD a1 ⇒ ODD' a1: thm
val EVEN_ODD_rules =
⊢ EVEN 0 ∧ (∀n. ODD n ⇒ EVEN (n + 1)) ∧ ∀n. EVEN n ⇒ ODD (n + 1): thm
The next example shows how to inductively define the reflexive
and transitive closure of relation $R$, which we write as rtc.
Note that R, as a schematic variable, is not quantified in the
rules. This is appropriate because it is rtc R that has the
inductive characterisation, not rtc itself.
> Inductive rtc:
(!x. rtc R x x) /\
(!x z. (?y. R x y /\ rtc R y z) ==> rtc R x z)
End
<<HOL message: inventing new type variable names: 'a>>
<<HOL message: Treating "R" as schematic variable>>
val rtc_cases = ⊢ ∀R a0 a1. rtc R a0 a1 ⇔ a1 = a0 ∨ ∃y. R a0 y ∧ rtc R y a1:
thm
val rtc_ind =
⊢ ∀R rtc'.
(∀x. rtc' x x) ∧ (∀x z. (∃y. R x y ∧ rtc' y z) ⇒ rtc' x z) ⇒
∀a0 a1. rtc R a0 a1 ⇒ rtc' a0 a1: thm
val rtc_rules =
⊢ ∀R. (∀x. rtc R x x) ∧ ∀x z. (∃y. R x y ∧ rtc R y z) ⇒ rtc R x z: thm
Inductive definitions may be used to define multiple relations,
as in the definition of EVEN and ODD. The relations may or
may not be mutually recursive. The clauses for each relation
need not be contiguous.
Proofs with inductive relations
The “rules” theorem of an inductive relation provides a
straightforward way of proving arguments belong to a relation. If
confronted with a goal of the form R x y, one might make
progress by performing a MATCH_MP_TAC (or perhaps, an
HO_MATCH_MP_TAC) with one of the implications in the “rules”
theorem.
The “cases” theorem can be used for the same purpose because it is
an equality, of the general form R x y $\Leftrightarrow$ $\ldots$.
Because the right-hand side of this theorem will often include
other occurrences of the relation, it is generally not safe to
simply rewrite with it.
The rewriting-control directives Once, SimpLHS and SimpRHS
can be useful here.
In addition, the “cases” theorem can be used as an “elimination”
form: if one has an assumption of the form R x y, rewriting this
(perhaps with FULL_SIMP_TAC if the term occurs in the goal's
assumptions) into the possible ways it may have come about is
often a good approach.
Inductive relations naturally also support proof by induction. Because an inductive relation is the least relation satisfying the given rules, one can use induction to show goals of the form
!x y. R x y ==> P
where P is an arbitrary predicate likely including references to
variables x and y.
The low-level approach to goals of this form is to apply
HO_MATCH_MP_TAC R_ind
A slightly more high-level approach is use the Induct_on
tactic, which will actually use the automatically generated
“strong” induction principle.3
(This tactic is also used to perform structural inductions over
algebraic data types; see the bossLib section of the Libraries
chapter.) When
performing a rule induction, the quotation passed to Induct_on
should be of the constant, perhaps also applied to arguments.
Indeed, if there are multiple instances of an R-term in the
goal, then quoting arguments allows selection of the correct term
to induct on. Thus, one can write invocations such as
Induct_on `R (f x) y`
Coinductive Relations
HOL supports coinductive relational definitions by the function
Hol_coreln in the bossLib structure (or with the special
CoInductive syntax). Hol_coreln shares the same input syntax
with Hol_reln. A successful invocation of this definitional
principle returns three important theorems $\mathit{rules}$,
$\mathit{coind}$ and $\mathit{cases}$. Each is also stored in the
current theory segment.
- $\mathit{rules}$ is a conjunction of implications that will be
the same as the input term quotation; the theorem is saved
under the name
<stem>_rules, where<stem>is the name of the first relation defined by the function (if usingHol_coreln), or as provided by the user, when using theCoInductivesyntax. - $\mathit{coind}$ is the coinduction principle for the relations,
saved under the name
<stem>_coind. - $\mathit{cases}$ is the so-called “cases” or “inversion”
theorem for the relations, saved under the name
<stem>_cases, and is used to decompose an element in the relation into the possible ways of obtaining it by the rules.
Note that “schematic variables” are also supported by
Hol_coreln, while there is no concept of “strong coinduction
principles” here. HOL's core coalgebra types (llist, path and
lbtree) are all based on coinductive relations. See Section
5.5.4 for a sample usage of coinductive relations on
bisimulation.
-
HOL also supports another syntax for datatype definition through the
Hol_datatypeentrypoint. For more details on this syntax, seeHol_datatype's entry in \REFERENCE. ↩ -
In a call to
fetch, the first argument denotes a theory; the current theory may be specified by"-". ↩ -
To get an approximation of the
Induct_oncall, one might write something likeHO_MATCH_MP_TAC R_strongind. ↩