\chapter{Functional Programming in HOL}

Although on the surface this chapter is mainly concerned with how to write

functional programs in HOL and how to verify them, most of the

constructs and proof procedures introduced are general purpose and recur in

any specification or verification task.

The dedicated functional programmer should be warned: HOL offers only what

could be called {\em total functional programming} --- all functions in HOL

must be total; lazy data structures are not directly available. On the

positive side, functions in HOL need not be computable: HOL is a

specification language that goes well beyond what can be expressed as a

program. However, for the time being we concentrate on the computable.

\section{An introductory theory}

\label{sec:intro-theory}

Functional programming needs datatypes and functions. Both of them can be

defined in a theory with a syntax reminiscent of languages like ML or

Haskell. As an example consider the theory in Fig.~\ref{fig:ToyList}.

\begin{figure}[htbp]

\begin{ttbox}\makeatother

\input{ToyList/ToyList.thy}\end{ttbox}

\caption{A theory of lists}

\label{fig:ToyList}

\end{figure}

HOL already has a predefined theory of lists called \texttt{List} ---

\texttt{ToyList} is merely a small fragment of it chosen as an example. In

contrast to what is recommended in \S\ref{sec:Basic:Theories},

\texttt{ToyList} is not based on \texttt{Main} but on \texttt{Datatype}, a

theory that contains everything required for datatype definitions but does

not have \texttt{List} as a parent, thus avoiding ambiguities caused by

defining lists twice.

The \ttindexbold{datatype} \texttt{list} introduces two constructors

\texttt{Nil} and \texttt{Cons}, the empty list and the operator that adds an

element to the front of a list. For example, the term \texttt{Cons True (Cons

  False Nil)} is a value of type \texttt{bool~list}, namely the list with the

elements \texttt{True} and \texttt{False}. Because this notation becomes

unwieldy very quickly, the datatype declaration is annotated with an

alternative syntax: instead of \texttt{Nil} and \texttt{Cons}~$x$~$xs$ we can

write \index{#@{\tt[]}|bold}\texttt{[]} and

\texttt{$x$~\#~$xs$}\index{#@{\tt\#}|bold}. In fact, this alternative syntax

is the standard syntax. Thus the list \texttt{Cons True (Cons False Nil)}

becomes \texttt{True \# False \# []}. The annotation \ttindexbold{infixr}

means that \texttt{\#} associates to the right, i.e.\ the term \texttt{$x$ \#

  $y$ \# $z$} is read as \texttt{$x$ \# ($y$ \# $z$)} and not as \texttt{($x$

  \# $y$) \# $z$}.

\begin{warn}

  Syntax annotations are a powerful but completely optional feature. You

  could drop them from theory \texttt{ToyList} and go back to the identifiers

  \texttt{Nil} and \texttt{Cons}. However, lists are such a central datatype

  that their syntax is highly customized. We recommend that novices should

  not use syntax annotations in their own theories.

\end{warn}

Next, the functions \texttt{app} and \texttt{rev} are declared. In contrast

to ML, Isabelle insists on explicit declarations of all functions (keyword

\ttindexbold{consts}).  (Apart from the declaration-before-use restriction,

the order of items in a theory file is unconstrained.) Function \texttt{app}

is annotated with concrete syntax too. Instead of the prefix syntax

\texttt{app}~$xs$~$ys$ the infix $xs$~\texttt{\at}~$ys$ becomes the preferred

form.

Both functions are defined recursively. The equations for \texttt{app} and

\texttt{rev} hardly need comments: \texttt{app} appends two lists and

\texttt{rev} reverses a list.  The keyword \texttt{primrec} indicates that

the recursion is of a particularly primitive kind where each recursive call

peels off a datatype constructor from one of the arguments (see

\S\ref{sec:datatype}).  Thus the recursion always terminates, i.e.\ the

function is \bfindex{total}.

The termination requirement is absolutely essential in HOL, a logic of total

functions. If we were to drop it, inconsistencies could quickly arise: the

``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting

$f(n)$ on both sides.

% However, this is a subtle issue that we cannot discuss here further.

\begin{warn}

  As we have indicated, the desire for total functions is not a gratuitously

  imposed restriction but an essential characteristic of HOL. It is only

  because of totality that reasoning in HOL is comparatively easy.  More

  generally, the philosophy in HOL is not to allow arbitrary axioms (such as

  function definitions whose totality has not been proved) because they

  quickly lead to inconsistencies. Instead, fixed constructs for introducing

  types and functions are offered (such as \texttt{datatype} and

  \texttt{primrec}) which are guaranteed to preserve consistency.

\end{warn}

A remark about syntax.  The textual definition of a theory follows a fixed

syntax with keywords like \texttt{datatype} and \texttt{end} (see

Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).

Embedded in this syntax are the types and formulae of HOL, whose syntax is

extensible, e.g.\ by new user-defined infix operators

(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything

HOL-specific should be enclosed in \texttt{"}\dots\texttt{"}. The same holds

for identifiers that happen to be keywords, as in

\begin{ttbox}

consts "end" :: 'a list => 'a

\end{ttbox}

To lessen this burden, quotation marks around types can be dropped,

provided their syntax does not go beyond what is described in

\S\ref{sec:TypesTermsForms}. Types containing further operators, e.g.\

\texttt{*} for Cartesian products, need quotation marks.

When Isabelle prints a syntax error message, it refers to the HOL syntax as

the \bfindex{inner syntax}.

\section{An introductory proof}

\label{sec:intro-proof}

Having defined \texttt{ToyList}, we load it with the ML command

\begin{ttbox}

use_thy "ToyList";

\end{ttbox}

and are ready to prove a few simple theorems. This will illustrate not just

the basic proof commands but also the typical proof process.

\subsubsection*{Main goal: \texttt{rev(rev xs) = xs}}

Our goal is to show that reversing a list twice produces the original

list. Typing

\begin{ttbox}

\input{ToyList/thm}\end{ttbox}

establishes a new goal to be proved in the context of the current theory,

which is the one we just loaded. Isabelle's response is to print the current proof state:

\begin{ttbox}

{\out Level 0}

{\out rev (rev xs) = xs}

{\out  1. rev (rev xs) = xs}

\end{ttbox}

Until we have finished a proof, the proof state always looks like this:

\begin{ttbox}

{\out Level \(i\)}

{\out \(G\)}

{\out  1. \(G@1\)}

{\out  \(\vdots\)}

{\out  \(n\). \(G@n\)}

\end{ttbox}

where \texttt{Level}~$i$ indicates that we are $i$ steps into the proof, $G$

is the overall goal that we are trying to prove, and the numbered lines

contain the subgoals $G@1$, \dots, $G@n$ that we need to prove to establish

$G$. At \texttt{Level 0} there is only one subgoal, which is identical with

the overall goal.  Normally $G$ is constant and only serves as a reminder.

Hence we rarely show it in this tutorial.

Let us now get back to \texttt{rev(rev xs) = xs}. Properties of recursively

defined functions are best established by induction. In this case there is

not much choice except to induct on \texttt{xs}:

\begin{ttbox}

\input{ToyList/inductxs}\end{ttbox}

This tells Isabelle to perform induction on variable \texttt{xs} in subgoal

1. The new proof state contains two subgoals, namely the base case

(\texttt{Nil}) and the induction step (\texttt{Cons}):

\begin{ttbox}

{\out 1. rev (rev []) = []}

{\out 2. !!a list. rev (rev list) = list ==> rev (rev (a # list)) = a # list}

\end{ttbox}

The induction step is an example of the general format of a subgoal:

\begin{ttbox}

{\out  \(i\). !!\(x@1 \dots x@n\). {\it assumptions} ==> {\it conclusion}}

\end{ttbox}\index{==>@{\tt==>}|bold}

The prefix of bound variables \texttt{!!\(x@1 \dots x@n\)} can be ignored

most of the time, or simply treated as a list of variables local to this

subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.  The

{\it assumptions} are the local assumptions for this subgoal and {\it

  conclusion} is the actual proposition to be proved. Typical proof steps

that add new assumptions are induction or case distinction. In our example

the only assumption is the induction hypothesis \texttt{rev (rev list) =

  list}, where \texttt{list} is a variable name chosen by Isabelle. If there

are multiple assumptions, they are enclosed in the bracket pair

\texttt{[|}\index{==>@\ttlbr|bold} and \texttt{|]}\index{==>@\ttrbr|bold}

and separated by semicolons.

Let us try to solve both goals automatically:

\begin{ttbox}

\input{ToyList/autotac}\end{ttbox}

This command tells Isabelle to apply a proof strategy called

\texttt{Auto_tac} to all subgoals. Essentially, \texttt{Auto_tac} tries to

`simplify' the subgoals.  In our case, subgoal~1 is solved completely (thanks

to the equation \texttt{rev [] = []}) and disappears; the simplified version

of subgoal~2 becomes the new subgoal~1:

\begin{ttbox}\makeatother

{\out 1. !!a list. rev(rev list) = list ==> rev(rev list @ a # []) = a # list}

\end{ttbox}

In order to simplify this subgoal further, a lemma suggests itself.

\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}

We start the proof as usual:

\begin{ttbox}\makeatother

\input{ToyList/lemma1}\end{ttbox}

There are two variables that we could induct on: \texttt{xs} and

\texttt{ys}. Because \texttt{\at} is defined by recursion on

the first argument, \texttt{xs} is the correct one:

\begin{ttbox}

\input{ToyList/inductxs}\end{ttbox}

This time not even the base case is solved automatically:

\begin{ttbox}\makeatother

by(Auto_tac);

{\out 1. rev ys = rev ys @ []}

{\out 2. \dots}

\end{ttbox}

We need another lemma.

\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}}

This time the canonical proof procedure

\begin{ttbox}\makeatother

\input{ToyList/lemma2}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}

leads to the desired message \texttt{No subgoals!}:

\begin{ttbox}\makeatother

{\out Level 2}

{\out xs @ [] = xs}

{\out No subgoals!}

\end{ttbox}

Now we can give the lemma just proved a suitable name

\begin{ttbox}

\input{ToyList/qed2}\end{ttbox}

and tell Isabelle to use this lemma in all future proofs by simplification:

\begin{ttbox}

\input{ToyList/addsimps2}\end{ttbox}

Note that in the theorem \texttt{app_Nil2} the free variable \texttt{xs} has

been replaced by the unknown \texttt{?xs}, just as explained in

\S\ref{sec:variables}.

Going back to the proof of the first lemma

\begin{ttbox}\makeatother

\input{ToyList/lemma1}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}

we find that this time \texttt{Auto_tac} solves the base case, but the

induction step merely simplifies to

\begin{ttbox}\makeatother

{\out 1. !!a list.}

{\out       rev (list @ ys) = rev ys @ rev list}

{\out       ==> (rev ys @ rev list) @ a # [] = rev ys @ rev list @ a # []}

\end{ttbox}

Now we need to remember that \texttt{\at} associates to the right, and that

\texttt{\#} and \texttt{\at} have the same priority (namely the \texttt{65}

in the definition of \texttt{ToyList}). Thus the conclusion really is

\begin{ttbox}\makeatother

{\out     ==> (rev ys @ rev list) @ (a # []) = rev ys @ (rev list @ (a # []))}

\end{ttbox}

and the missing lemma is associativity of \texttt{\at}.

\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}

This time the canonical proof procedure

\begin{ttbox}\makeatother

\input{ToyList/lemma3}\end{ttbox}

succeeds without further ado. Again we name the lemma and add it to

the set of lemmas used during simplification:

\begin{ttbox}

\input{ToyList/qed3}\end{ttbox}

Now we can go back and prove the first lemma

\begin{ttbox}\makeatother

\input{ToyList/lemma1}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}

add it to the simplification lemmas

\begin{ttbox}

\input{ToyList/qed1}\end{ttbox}

and then solve our main theorem:

\begin{ttbox}\makeatother

\input{ToyList/thm}\input{ToyList/inductxs}\input{ToyList/autotac}\end{ttbox}

\subsubsection*{Review}

This is the end of our toy proof. It should have familiarized you with

\begin{itemize}

\item the standard theorem proving procedure:

state a goal; proceed with proof until a new lemma is required; prove that

lemma; come back to the original goal.

\item a specific procedure that works well for functional programs:

induction followed by all-out simplification via \texttt{Auto_tac}.

\item a basic repertoire of proof commands.

\end{itemize}

\section{Some helpful commands}

\label{sec:commands-and-hints}

This section discusses a few basic commands for manipulating the proof state

and can be skipped by casual readers.

There are two kinds of commands used during a proof: the actual proof

commands and auxiliary commands for examining the proof state and controlling

the display. Proof commands are always of the form

\texttt{by(\textit{tactic});}\indexbold{tactic} where \textbf{tactic} is a

synonym for ``theorem proving function''. Typical examples are

\texttt{induct_tac} and \texttt{Auto_tac} --- the suffix \texttt{_tac} is

merely a mnemonic. Further tactics are introduced throughout the tutorial.

%Tactics can also be modified. For example,

%\begin{ttbox}

%by(ALLGOALS Asm_simp_tac);

%\end{ttbox}

%tells Isabelle to apply \texttt{Asm_simp_tac} to all subgoals. For more on

%tactics and how to combine them see~\S\ref{sec:Tactics}.

The most useful auxiliary commands are:

\begin{description}

\item[Printing the current state]

Type \texttt{pr();} to redisplay the current proof state, for example when it

has disappeared off the screen.

\item[Limiting the number of subgoals]

Typing \texttt{prlim $k$;} tells Isabelle to print only the first $k$

subgoals from now on and redisplays the current proof state. This is helpful

when there are many subgoals.

\item[Undoing] Typing \texttt{undo();} undoes the effect of the last

tactic.

\item[Context switch] Every proof happens in the context of a

  \bfindex{current theory}. By default, this is the last theory loaded. If

  you want to prove a theorem in the context of a different theory

  \texttt{T}, you need to type \texttt{context T.thy;}\index{*context|bold}

  first. Of course you need to change the context again if you want to go

  back to your original theory.

\item[Displaying types] We have already mentioned the flag

  \ttindex{show_types} above. It can also be useful for detecting typos in

  formulae early on. For example, if \texttt{show_types} is set and the goal

  \texttt{rev(rev xs) = xs} is started, Isabelle prints the additional output

\begin{ttbox}

{\out Variables:}

{\out   xs :: 'a list}

\end{ttbox}

which tells us that Isabelle has correctly inferred that

\texttt{xs} is a variable of list type. On the other hand, had we

made a typo as in \texttt{rev(re xs) = xs}, the response

\begin{ttbox}

Variables:

  re :: 'a list => 'a list

  xs :: 'a list

\end{ttbox}

would have alerted us because of the unexpected variable \texttt{re}.

\item[(Re)loading theories]\index{loading theories}\index{reloading theories}

Initially you load theory \texttt{T} by typing \ttindex{use_thy}~\texttt{"T";},

which loads all parent theories of \texttt{T} automatically, if they are not

loaded already. If you modify \texttt{T.thy} or \texttt{T.ML}, you can

reload it by typing \texttt{use_thy~"T";} again. This time, however, only

\texttt{T} is reloaded. If some of \texttt{T}'s parents have changed as well,

type \ttindexbold{update}\texttt{();} to reload all theories that have

changed.

\end{description}

Further commands are found in the Reference Manual.

\section{Datatypes}

\label{sec:datatype}

Inductive datatypes are part of almost every non-trivial application of HOL.

First we take another look at a very important example, the datatype of

lists, before we turn to datatypes in general. The section closes with a

case study.

\subsection{Lists}

Lists are one of the essential datatypes in computing. Readers of this tutorial

and users of HOL need to be familiar with their basic operations. Theory

\texttt{ToyList} is only a small fragment of HOL's predefined theory

\texttt{List}\footnote{\texttt{http://www.in.tum.de/\~\relax

    isabelle/library/HOL/List.html}}.

The latter contains many further operations. For example, the functions

\ttindexbold{hd} (`head') and \ttindexbold{tl} (`tail') return the first

element and the remainder of a list. (However, pattern-matching is usually

preferable to \texttt{hd} and \texttt{tl}.)

Theory \texttt{List} also contains more syntactic sugar:

\texttt{[}$x@1$\texttt{,}\dots\texttt{,}$x@n$\texttt{]} abbreviates

$x@1$\texttt{\#}\dots\texttt{\#}$x@n$\texttt{\#[]}.

In the rest of the tutorial we always use HOL's predefined lists.

\subsection{The general format}

\label{sec:general-datatype}

The general HOL \texttt{datatype} definition is of the form

\[

\mathtt{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~

C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~

C@m~\tau@{m1}~\dots~\tau@{mk@m}

\]

where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct

constructor names and $\tau@{ij}$ are types; it is customary to capitalize

the first letter in constructor names. There are a number of

restrictions (such as the type should not be empty) detailed

elsewhere~\cite{Isa-Logics-Man}. Isabelle notifies you if you violate them.

Laws about datatypes, such as \verb$[] ~= x#xs$ and \texttt{(x\#xs = y\#ys) =

  (x=y \& xs=ys)}, are used automatically during proofs by simplification.

The same is true for the equations in primitive recursive function

definitions.

\subsection{Primitive recursion}

Functions on datatypes are usually defined by recursion. In fact, most of the

time they are defined by what is called \bfindex{primitive recursion}.

The keyword \texttt{primrec} is followed by a list of equations

\[ f \, x@1 \, \dots \, (C \, y@1 \, \dots \, y@k)\, \dots \, x@n = r \]

such that $C$ is a constructor of the datatype $t$ and all recursive calls of

$f$ in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. Thus

Isabelle immediately sees that $f$ terminates because one (fixed!) argument

becomes smaller with every recursive call. There must be exactly one equation

for each constructor.  Their order is immaterial.

A more general method for defining total recursive functions is explained in

\S\ref{sec:recdef}.

\begin{exercise}

Given the datatype of binary trees

\begin{ttbox}

\input{Misc/tree}\end{ttbox}

define a function \texttt{mirror} that mirrors the structure of a binary tree

by swapping subtrees (recursively). Prove \texttt{mirror(mirror(t)) = t}.

\end{exercise}

\subsection{\texttt{case}-expressions}

\label{sec:case-expressions}

HOL also features \ttindexbold{case}-expressions for analyzing elements of a

datatype. For example,

\begin{ttbox}

case xs of [] => 0 | y#ys => y

\end{ttbox}

evaluates to \texttt{0} if \texttt{xs} is \texttt{[]} and to \texttt{y} if 

\texttt{xs} is \texttt{y\#ys}. (Since the result in both branches must be of

the same type, it follows that \texttt{y::nat} and hence

\texttt{xs::(nat)list}.)

In general, if $e$ is a term of the datatype $t$ defined in

\S\ref{sec:general-datatype} above, the corresponding

\texttt{case}-expression analyzing $e$ is

\[

\begin{array}{rrcl}

\mbox{\tt case}~e~\mbox{\tt of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\

                           \vdots \\

                           \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m

\end{array}

\]

\begin{warn}

{\em All} constructors must be present, their order is fixed, and nested

patterns are not supported.  Violating these restrictions results in strange

error messages.

\end{warn}

\noindent

Nested patterns can be simulated by nested \texttt{case}-expressions: instead

of

\begin{ttbox}

case xs of [] => 0 | [x] => x | x#(y#zs) => y

\end{ttbox}

write

\begin{ttbox}

case xs of [] => 0 | x#ys => (case ys of [] => x | y#zs => y)

\end{ttbox}

Note that \texttt{case}-expressions should be enclosed in parentheses to

indicate their scope.

\subsection{Structural induction}

Almost all the basic laws about a datatype are applied automatically during

simplification. Only induction is invoked by hand via \texttt{induct_tac},

which works for any datatype. In some cases, induction is overkill and a case

distinction over all constructors of the datatype suffices. This is performed

by \ttindexbold{exhaust_tac}. A trivial example:

\begin{ttbox}

\input{Misc/exhaust.ML}{\out1. xs = [] ==> (case xs of [] => [] | y # ys => xs) = xs}

{\out2. !!a list. xs = a # list ==> (case xs of [] => [] | y # ys => xs) = xs}

\input{Misc/autotac.ML}\end{ttbox}

Note that this particular case distinction could have been automated

completely. See~\S\ref{sec:SimpFeatures}.

\begin{warn}

  Induction is only allowed on a free variable that should not occur among

  the assumptions of the subgoal.  Exhaustion works for arbitrary terms.

\end{warn}

\subsection{Case study: boolean expressions}

\label{sec:boolex}

The aim of this case study is twofold: it shows how to model boolean

expressions and some algorithms for manipulating them, and it demonstrates

the constructs introduced above.

\subsubsection{How can we model boolean expressions?}

We want to represent boolean expressions built up from variables and

constants by negation and conjunction. The following datatype serves exactly

that purpose:

\begin{ttbox}

\input{Ifexpr/boolex}\end{ttbox}

The two constants are represented by the terms \texttt{Const~True} and

\texttt{Const~False}. Variables are represented by terms of the form

\texttt{Var}~$n$, where $n$ is a natural number (type \texttt{nat}).

For example, the formula $P@0 \land \neg P@1$ is represented by the term

\texttt{And~(Var~0)~(Neg(Var~1))}.

\subsubsection{What is the value of boolean expressions?}

The value of a boolean expressions depends on the value of its variables.

Hence the function \texttt{value} takes an additional parameter, an {\em

  environment} of type \texttt{nat~=>~bool}, which maps variables to their

values:

\begin{ttbox}

\input{Ifexpr/value}\end{ttbox}

\subsubsection{If-expressions}

An alternative and often more efficient (because in a certain sense

canonical) representation are so-called \textit{If-expressions\/} built up

from constants (\texttt{CIF}), variables (\texttt{VIF}) and conditionals

(\texttt{IF}):

\begin{ttbox}

\input{Ifexpr/ifex}\end{ttbox}

The evaluation if If-expressions proceeds as for \texttt{boolex}:

\begin{ttbox}

\input{Ifexpr/valif}\end{ttbox}

\subsubsection{Transformation into and of If-expressions}

The type \texttt{boolex} is close to the customary representation of logical

formulae, whereas \texttt{ifex} is designed for efficiency. Thus we need to

translate from \texttt{boolex} into \texttt{ifex}:

\begin{ttbox}

\input{Ifexpr/bool2if}\end{ttbox}

At last, we have something we can verify: that \texttt{bool2if} preserves the

value of its argument.

\begin{ttbox}

\input{Ifexpr/bool2if.ML}\end{ttbox}

The proof is canonical:

\begin{ttbox}

\input{Ifexpr/proof.ML}\end{ttbox}

In fact, all proofs in this case study look exactly like this. Hence we do

not show them below.

More interesting is the transformation of If-expressions into a normal form

where the first argument of \texttt{IF} cannot be another \texttt{IF} but

must be a constant or variable. Such a normal form can be computed by

repeatedly replacing a subterm of the form \texttt{IF~(IF~b~x~y)~z~u} by

\texttt{IF b (IF x z u) (IF y z u)}, which has the same value. The following

primitive recursive functions perform this task:

\begin{ttbox}

\input{Ifexpr/normif}

\input{Ifexpr/norm}\end{ttbox}

Their interplay is a bit tricky, and we leave it to the reader to develop an

intuitive understanding. Fortunately, Isabelle can help us to verify that the

transformation preserves the value of the expression:

\begin{ttbox}

\input{Ifexpr/norm.ML}\end{ttbox}

The proof is canonical, provided we first show the following lemma (which

also helps to understand what \texttt{normif} does) and make it available

for simplification via \texttt{Addsimps}:

\begin{ttbox}

\input{Ifexpr/normif.ML}\end{ttbox}

But how can we be sure that \texttt{norm} really produces a normal form in

the above sense? We have to prove

\begin{ttbox}

\input{Ifexpr/normal_norm.ML}\end{ttbox}

where \texttt{normal} expresses that an If-expression is in normal form:

\begin{ttbox}

\input{Ifexpr/normal}\end{ttbox}

Of course, this requires a lemma about normality of \texttt{normif}

\begin{ttbox}

\input{Ifexpr/normal_normif.ML}\end{ttbox}

that has to be made available for simplification via \texttt{Addsimps}.

How does one come up with the required lemmas? Try to prove the main theorems

without them and study carefully what \texttt{Auto_tac} leaves unproved. This

has to provide the clue.

The necessity of universal quantification (\texttt{!t e}) in the two lemmas

is explained in \S\ref{sec:InductionHeuristics}

\begin{exercise}

  We strengthen the definition of a {\em normal\/} If-expression as follows:

  the first argument of all \texttt{IF}s must be a variable. Adapt the above

  development to this changed requirement. (Hint: you may need to formulate

  some of the goals as implications (\texttt{-->}) rather than equalities

  (\texttt{=}).)

\end{exercise}

\section{Some basic types}

\subsection{Natural numbers}

The type \ttindexbold{nat} of natural numbers is predefined and behaves like

\begin{ttbox}

datatype nat = 0 | Suc nat

\end{ttbox}

In particular, there are \texttt{case}-expressions, for example

\begin{ttbox}

case n of 0 => 0 | Suc m => m

\end{ttbox}

primitive recursion, for example

\begin{ttbox}

\input{Misc/natsum}\end{ttbox}

and induction, for example

\begin{ttbox}

\input{Misc/NatSum.ML}\ttbreak

{\out sum n + sum n = n * Suc n}

{\out No subgoals!}

\end{ttbox}

The usual arithmetic operations \ttindexbold{+}, \ttindexbold{-},

\ttindexbold{*}, \ttindexbold{div} and \ttindexbold{mod} are predefined, as

are the relations \ttindexbold{<=} and \ttindexbold{<}. There is even a least

number operation \ttindexbold{LEAST}. For example, \texttt{(LEAST n.$\,$1 <

  n) = 2} (HOL does not prove this completely automatically).

\begin{warn}

  The operations \ttindexbold{+}, \ttindexbold{-}, \ttindexbold{*} are

  overloaded, i.e.\ they are available not just for natural numbers but at

  other types as well (see \S\ref{sec:TypeClasses}). For example, given

  the goal \texttt{x+y = y+x}, there is nothing to indicate that you are

  talking about natural numbers. Hence Isabelle can only infer that

  \texttt{x} and \texttt{y} are of some arbitrary type where \texttt{+} is

  declared. As a consequence, you will be unable to prove the goal (although

  it may take you some time to realize what has happened if

  \texttt{show_types} is not set).  In this particular example, you need to

  include an explicit type constraint, for example \texttt{x+y = y+(x::nat)}.

  If there is enough contextual information this may not be necessary:

  \texttt{x+0 = x} automatically implies \texttt{x::nat}.

\end{warn}

\subsection{Products}

HOL also has pairs: \texttt{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ *

$\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair

are extracted by \texttt{fst} and \texttt{snd}:

\texttt{fst($x$,$y$) = $x$} and \texttt{snd($x$,$y$) = $y$}. Tuples

are simulated by pairs nested to the right: 

\texttt{($a@1$,$a@2$,$a@3$)} and \texttt{$\tau@1$ * $\tau@2$ * $\tau@3$}

stand for \texttt{($a@1$,($a@2$,$a@3$))} and \texttt{$\tau@1$ * ($\tau@2$ *

$\tau@3$)}. Therefore \texttt{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}.

It is possible to use (nested) tuples as patterns in abstractions, for

example \texttt{\%(x,y,z).x+y+z} and \texttt{\%((x,y),z).x+y+z}.

In addition to explicit $\lambda$-abstractions, tuple patterns can be used in

most variable binding constructs. Typical examples are

\begin{ttbox}

let (x,y) = f z in (y,x)

case xs of [] => 0 | (x,y)\#zs => x+y

\end{ttbox}

Further important examples are quantifiers and sets.

\begin{warn}

Abstraction over pairs and tuples is merely a convenient shorthand for a more

complex internal representation.  Thus the internal and external form of a

term may differ, which can affect proofs. If you want to avoid this

complication, use \texttt{fst} and \texttt{snd}, i.e.\ write

\texttt{\%p.~fst p + snd p} instead of \texttt{\%(x,y).~x + y}.

See~\S\ref{} for theorem proving with tuple patterns.

\end{warn}

\section{Definitions}

\label{sec:Definitions}

A definition is simply an abbreviation, i.e.\ a new name for an existing

construction. In particular, definitions cannot be recursive. Isabelle offers

definitions on the level of types and terms. Those on the type level are

called type synonyms, those on the term level are called (constant)

definitions.

\subsection{Type synonyms}

\indexbold{type synonyms}

Type synonyms are similar to those found in ML. Their syntax is fairly self

explanatory:

\begin{ttbox}

\input{Misc/types}\end{ttbox}\indexbold{*types}

The synonym \texttt{alist} shows that in general the type on the right-hand

side needs to be enclosed in double quotation marks

(see the end of~\S\ref{sec:intro-theory}).

Internally all synonyms are fully expanded.  As a consequence Isabelle's

output never contains synonyms.  Their main purpose is to improve the

readability of theory definitions.  Synonyms can be used just like any other

type:

\begin{ttbox}

\input{Misc/consts}\end{ttbox}

\subsection{Constant definitions}

\label{sec:ConstDefinitions}

The above constants \texttt{nand} and \texttt{exor} are non-recursive and can

therefore be defined directly by

\begin{ttbox}

\input{Misc/defs}\end{ttbox}\indexbold{*defs}

where \texttt{defs} is a keyword and \texttt{nand_def} and \texttt{exor_def}

are arbitrary user-supplied names.

The symbol \texttt{==}\index{==>@{\tt==}|bold} is a special form of equality

that should only be used in constant definitions.

Declarations and definitions can also be merged

\begin{ttbox}

\input{Misc/constdefs}\end{ttbox}\indexbold{*constdefs}

in which case the default name of each definition is $f$\texttt{_def}, where

$f$ is the name of the defined constant.

Note that pattern-matching is not allowed, i.e.\ each definition must be of

the form $f\,x@1\,\dots\,x@n$\texttt{~==~}$t$.

Section~\S\ref{sec:Simplification} explains how definitions are used

in proofs.

\begin{warn}

A common mistake when writing definitions is to introduce extra free variables

on the right-hand side as in the following fictitious definition:

\begin{ttbox}

defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"

\end{ttbox}

Isabelle rejects this `definition' because of the extra {\tt m} on the

right-hand side, which would introduce an inconsistency.  What you should have

written is

\begin{ttbox}

defs  prime_def "prime(p) == !m. (m divides p) --> (m=1 | m=p)"

\end{ttbox}

\end{warn}

\chapter{More Functional Programming}

The purpose of this chapter is to deepen the reader's understanding of the

concepts encountered so far and to introduce an advanced method for defining

recursive functions. The first two sections give a structured presentation of

theorem proving by simplification (\S\ref{sec:Simplification}) and

discuss important heuristics for induction (\S\ref{sec:InductionHeuristics}). They

can be skipped by readers less interested in proofs. They are followed by a

case study, a compiler for expressions (\S\ref{sec:ExprCompiler}).

Finally we present a very general method for defining recursive functions

that goes well beyond what \texttt{primrec} allows (\S\ref{sec:recdef}).

\section{Simplification}

\label{sec:Simplification}

So far we have proved our theorems by \texttt{Auto_tac}, which

`simplifies' all subgoals. In fact, \texttt{Auto_tac} can do much more than

that, except that it did not need to so far. However, when you go beyond toy

examples, you need to understand the ingredients of \texttt{Auto_tac}.

This section covers the tactic that \texttt{Auto_tac} always applies first,

namely simplification.

Simplification is one of the central theorem proving tools in Isabelle and

many other systems. The tool itself is called the \bfindex{simplifier}. The

purpose of this section is twofold: to introduce the many features of the

simplifier (\S\ref{sec:SimpFeatures}) and to explain a little bit how the

simplifier works (\S\ref{sec:SimpHow}).  Anybody intending to use HOL should

read \S\ref{sec:SimpFeatures}, and the serious student should read

\S\ref{sec:SimpHow} as well in order to understand what happened in case

things do not simplify as expected.

\subsection{Using the simplifier}

\label{sec:SimpFeatures}

In its most basic form, simplification means repeated application of

equations from left to right. For example, taking the rules for \texttt{\at}

and applying them to the term \texttt{[0,1] \at\ []} results in a sequence of

simplification steps:

\begin{ttbox}\makeatother

(0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]

\end{ttbox}

This is also known as {\em term rewriting} and the equations are referred

to as {\em rewrite rules}. This is more honest than `simplification' because

the terms do not necessarily become simpler in the process.

\subsubsection{Simpsets}

To facilitate simplification, each theory has an associated set of

simplification rules, known as a \bfindex{simpset}. Within a theory,

proofs by simplification refer to the associated simpset by default.

The simpset of a theory is built up as follows: starting with the union of

the simpsets of the parent theories, each occurrence of a \texttt{datatype}

or \texttt{primrec} construct augments the simpset. Explicit definitions are

not added automatically. Users can add new theorems via \texttt{Addsimps} and

delete them again later by \texttt{Delsimps}.

You may augment a simpset not just by equations but by pretty much any

theorem. The simplifier will try to make sense of it.  For example, a theorem

\verb$~$$P$ is automatically turned into \texttt{$P$ = False}. The details are

explained in \S\ref{sec:SimpHow}.

As a rule of thumb, rewrite rules that really simplify a term (like

\texttt{xs \at\ [] = xs} and \texttt{rev(rev xs) = xs}) should be added to the

current simpset right after they have been proved.  Those of a more specific

nature (e.g.\ distributivity laws, which alter the structure of terms

considerably) should only be added for specific proofs and deleted again

afterwards.  Conversely, it may also happen that a generally useful rule

needs to be removed for a certain proof and is added again afterwards.  The

need of frequent temporary additions or deletions may indicate a badly

designed simpset.

\begin{warn}

  Simplification may not terminate, for example if both $f(x) = g(x)$ and

  $g(x) = f(x)$ are in the simpset. It is the user's responsibility not to

  include rules that can lead to nontermination, either on their own or in

  combination with other rules.

\end{warn}

\subsubsection{Simplification tactics}

There are four main simplification tactics:

\begin{ttdescription}

\item[\ttindexbold{Simp_tac} $i$] simplifies the conclusion of subgoal~$i$

  using the theory's simpset.  It may solve the subgoal completely if it has

  become trivial. For example:

\begin{ttbox}\makeatother

{\out 1. [] @ [] = []}

by(Simp_tac 1);

{\out No subgoals!}

\end{ttbox}

\item[\ttindexbold{Asm_simp_tac}]

  is like \verb$Simp_tac$, but extracts additional rewrite rules from

  the assumptions of the subgoal. For example, it solves

\begin{ttbox}\makeatother

{\out 1. xs = [] ==> xs @ xs = xs}

\end{ttbox}

which \texttt{Simp_tac} does not do.

\item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also

  simplifies the assumptions (without using the assumptions to

  simplify each other or the actual goal).

\item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$,

  but also simplifies the assumptions. In particular, assumptions can

  simplify each other. For example:

\begin{ttbox}\makeatother

\out{ 1. [| xs @ zs = ys @ xs; [] @ xs = [] @ [] |] ==> ys = zs}

by(Asm_full_simp_tac 1);

{\out No subgoals!}

\end{ttbox}

The second assumption simplifies to \texttt{xs = []}, which in turn

simplifies the first assumption to \texttt{zs = ys}, thus reducing the

conclusion to \texttt{ys = ys} and hence to \texttt{True}.

(See also the paragraph on tracing below.)

\end{ttdescription}

\texttt{Asm_full_simp_tac} is the most powerful of this quartet of

tactics. In fact, \texttt{Auto_tac} starts by applying

\texttt{Asm_full_simp_tac} to all subgoals. The only reason for the existence

of the other three tactics is that sometimes one wants to limit the amount of

simplification, for example to avoid nontermination:

\begin{ttbox}\makeatother

{\out  1. ! x. f x = g (f (g x)) ==> f [] = f [] @ []}

\end{ttbox}

is solved by \texttt{Simp_tac}, but \texttt{Asm_simp_tac} and

\texttt{Asm_full_simp_tac} loop because the rewrite rule \texttt{f x = g(f(g

x))} extracted from the assumption does not terminate.  Isabelle notices

certain simple forms of nontermination, but not this one.

\subsubsection{Modifying simpsets locally}

If a certain theorem is merely needed in one proof by simplification, the

pattern

\begin{ttbox}

Addsimps [\(rare_theorem\)];

by(Simp_tac 1);

Delsimps [\(rare_theorem\)];

\end{ttbox}

is awkward. Therefore there are lower-case versions of the simplification

tactics (\ttindexbold{simp_tac}, \ttindexbold{asm_simp_tac},

\ttindexbold{full_simp_tac}, \ttindexbold{asm_full_simp_tac}) and of the

simpset modifiers (\ttindexbold{addsimps}, \ttindexbold{delsimps})

that do not access or modify the implicit simpset but explicitly take a

simpset as an argument. For example, the above three lines become

\begin{ttbox}

by(simp_tac (simpset() addsimps [\(rare_theorem\)]) 1);

\end{ttbox}

where the result of the function call \texttt{simpset()} is the simpset of

the current theory and \texttt{addsimps} is an infix function. The implicit

simpset is read once but not modified.

This is far preferable to pairs of \texttt{Addsimps} and \texttt{Delsimps}.

Local modifications can be stacked as in

\begin{ttbox}

by(simp_tac (simpset() addsimps [\(rare_theorem\)] delsimps [\(some_thm\)]) 1);

\end{ttbox}

\subsubsection{Rewriting with definitions}

Constant definitions (\S\ref{sec:ConstDefinitions}) are not automatically

included in the simpset of a theory. Hence such definitions are not expanded

automatically either, just as it should be: definitions are introduced for

the purpose of abbreviating complex concepts. Of course we need to expand the

definitions initially to derive enough lemmas that characterize the concept

sufficiently for us to forget the original definition completely. For

example, given the theory

\begin{ttbox}

\input{Misc/Exor.thy}\end{ttbox}

we may want to prove \verb$exor A (~A)$. Instead of \texttt{Goal} we use

\begin{ttbox}

\input{Misc/exorgoal.ML}\end{ttbox}

which tells Isabelle to expand the definition of \texttt{exor}---the first

argument of \texttt{Goalw} can be a list of definitions---in the initial goal:

\begin{ttbox}

{\out exor A (~ A)}

{\out  1. A & ~ ~ A | ~ A & ~ A}

\end{ttbox}

In this simple example, the goal is proved by \texttt{Simp_tac}.

Of course the resulting theorem is insufficient to characterize \texttt{exor}

completely.

In case we want to expand a definition in the middle of a proof, we can

simply add the definition locally to the simpset:

\begin{ttbox}

\input{Misc/exorproof.ML}\end{ttbox}

You should normally not add the definition permanently to the simpset

using \texttt{Addsimps} because this defeats the whole purpose of an

abbreviation.

\begin{warn}

If you have defined $f\,x\,y$\texttt{~==~}$t$ then you can only expand

occurrences of $f$ with at least two arguments. Thus it is safer to define

$f$\texttt{~==~\%$x\,y$.}$\;t$.

\end{warn}

\subsubsection{Simplifying \texttt{let}-expressions}

Proving a goal containing \ttindex{let}-expressions invariably requires the

\texttt{let}-constructs to be expanded at some point. Since

\texttt{let}-\texttt{in} is just syntactic sugar for a defined constant

(called \texttt{Let}), expanding \texttt{let}-constructs means rewriting with

\texttt{Let_def}:

%context List.thy;

%Goal "(let xs = [] in xs@xs) = ys";

\begin{ttbox}\makeatother

{\out  1. (let xs = [] in xs @ xs) = ys}

by(simp_tac (simpset() addsimps [Let_def]) 1);

{\out  1. [] = ys}

\end{ttbox}

If, in a particular context, there is no danger of a combinatorial explosion

of nested \texttt{let}s one could even add \texttt{Let_def} permanently via

\texttt{Addsimps}.

\subsubsection{Conditional equations}

So far all examples of rewrite rules were equations. The simplifier also

accepts {\em conditional\/} equations, for example

\begin{ttbox}

xs ~= []  ==>  hd xs # tl xs = xs \hfill \((*)\)

\end{ttbox}

(which is proved by \texttt{exhaust_tac} on \texttt{xs} followed by

\texttt{Asm_full_simp_tac} twice). Assuming that this theorem together with

%\begin{ttbox}\makeatother

\texttt{(rev xs = []) = (xs = [])}

%\end{ttbox}

are part of the simpset, the subgoal

\begin{ttbox}\makeatother

{\out 1. xs ~= [] ==> hd(rev xs) # tl(rev xs) = rev xs}

\end{ttbox}

is proved by simplification:

the conditional equation $(*)$ above

can simplify \texttt{hd(rev~xs)~\#~tl(rev~xs)} to \texttt{rev xs}

because the corresponding precondition \verb$rev xs ~= []$ simplifies to

\verb$xs ~= []$, which is exactly the local assumption of the subgoal.

\subsubsection{Automatic case splits}

Goals containing \ttindex{if}-expressions are usually proved by case

distinction on the condition of the \texttt{if}. For example the goal

\begin{ttbox}

{\out 1. ! xs. if xs = [] then rev xs = [] else rev xs ~= []}

\end{ttbox}

can be split into

\begin{ttbox}

{\out 1. ! xs. (xs = [] --> rev xs = []) \& (xs ~= [] --> rev xs ~= [])}

\end{ttbox}

by typing

\begin{ttbox}

\input{Misc/splitif.ML}\end{ttbox}

Because this is almost always the right proof strategy, the simplifier

performs case-splitting on \texttt{if}s automatically. Try \texttt{Simp_tac}

on the initial goal above.

This splitting idea generalizes from \texttt{if} to \ttindex{case}:

\begin{ttbox}\makeatother

{\out 1. (case xs of [] => zs | y#ys => y#(ys@zs)) = xs@zs}

\end{ttbox}

becomes

\begin{ttbox}\makeatother

{\out 1. (xs = [] --> zs = xs @ zs) &}

{\out    (! a list. xs = a # list --> a # list @ zs = xs @ zs)}

\end{ttbox}

by typing

\begin{ttbox}

\input{Misc/splitlist.ML}\end{ttbox}

In contrast to \texttt{if}-expressions, the simplifier does not split

\texttt{case}-expressions by default because this can lead to nontermination

in case of recursive datatypes.