\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.

 Nevertheless the simplifier can be instructed to perform \texttt{case}-splits

 by adding the appropriate rule to the simpset:

 \begin{ttbox}

 by(simp_tac (simpset() addsplits [split_list_case]) 1);

 \end{ttbox}\indexbold{*addsplits}

 solves the initial goal outright, which \texttt{Simp_tac} alone will not do.

 In general, every datatype $t$ comes with a rule

 \texttt{$t$.split} that can be added to the simpset either

 locally via \texttt{addsplits} (see above), or permanently via

 \begin{ttbox}

 Addsplits [\(t\).split];

 \end{ttbox}\indexbold{*Addsplits}

 Split-rules can be removed globally via \ttindexbold{Delsplits} and locally

 via \ttindexbold{delsplits} as, for example, in

 \begin{ttbox}

 by(simp_tac (simpset() addsimps [\(\dots\)] delsplits [split_if]) 1);

 \end{ttbox}

 \subsubsection{Permutative rewrite rules}

 A rewrite rule is {\bf permutative} if the left-hand side and right-hand side

 are the same up to renaming of variables.  The most common permutative rule

 is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.  Such

 rules are problematic because once they apply, they can be used forever.

 The simplifier is aware of this danger and treats permutative rules

 separately. For details see~\cite{Isa-Ref-Man}.

 \subsubsection{Tracing}

 \indexbold{tracing the simplifier}

 Using the simplifier effectively may take a bit of experimentation.  Set the

 \verb$trace_simp$ flag to get a better idea of what is going on:

 \begin{ttbox}\makeatother

 {\out  1. rev [x] = []}

 \ttbreak

 set trace_simp;

 by(Simp_tac 1);

 \ttbreak\makeatother

 {\out Applying instance of rewrite rule:}

 {\out rev (?x # ?xs) == rev ?xs @ [?x]}

 {\out Rewriting:}

 {\out rev [x] == rev [] @ [x]}

 \ttbreak

 {\out Applying instance of rewrite rule:}

 {\out rev [] == []}

 {\out Rewriting:}

 {\out rev [] == []}

 \ttbreak\makeatother

 {\out Applying instance of rewrite rule:}

 {\out [] @ ?y == ?y}

 {\out Rewriting:}

 {\out [] @ [x] == [x]}

 \ttbreak

 {\out Applying instance of rewrite rule:}

 {\out ?x # ?t = ?t == False}

 {\out Rewriting:}

 {\out [x] = [] == False}

 \ttbreak

 {\out Level 1}

 {\out rev [x] = []}

 {\out  1. False}

 \end{ttbox}

 In more complicated cases, the trace can be enormous, especially since

 invocations of the simplifier are often nested (e.g.\ when solving conditions

 of rewrite rules).

 \subsection{How it works}

 \label{sec:SimpHow}

 \subsubsection{Higher-order patterns}

 \subsubsection{Local assumptions}

 \subsubsection{The preprocessor}

 \section{Induction heuristics}

 \label{sec:InductionHeuristics}

 The purpose of this section is to illustrate some simple heuristics for

 inductive proofs. The first one we have already mentioned in our initial

 example:

 \begin{quote}

 {\em 1. Theorems about recursive functions are proved by induction.}

 \end{quote}

 In case the function has more than one argument

 \begin{quote}

 {\em 2. Do induction on argument number $i$ if the function is defined by

 recursion in argument number $i$.}

 \end{quote}

 When we look at the proof of

 \begin{ttbox}\makeatother

 (xs @ ys) @ zs = xs @ (ys @ zs)

 \end{ttbox}

 in \S\ref{sec:intro-proof} we find (a) \texttt{\at} is recursive in the first

 argument, (b) \texttt{xs} occurs only as the first argument of \texttt{\at},

 and (c) both \texttt{ys} and \texttt{zs} occur at least once as the second

 argument of \texttt{\at}. Hence it is natural to perform induction on

 \texttt{xs}.

 The key heuristic, and the main point of this section, is to

 generalize the goal before induction. The reason is simple: if the goal is

 too specific, the induction hypothesis is too weak to allow the induction

 step to go through. Let us now illustrate the idea with an example.

 We define a tail-recursive version of list-reversal,

 i.e.\ one that can be compiled into a loop:

 \begin{ttbox}

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

 The behaviour of \texttt{itrev} is simple: it reverses its first argument by

 stacking its elements onto the second argument, and returning that second

 argument when the first one becomes empty.

 We need to show that \texttt{itrev} does indeed reverse its first argument

 provided the second one is empty:

 \begin{ttbox}

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

 There is no choice as to the induction variable, and we immediately simplify:

 \begin{ttbox}

 \input{Misc/induct_auto.ML}\ttbreak\makeatother

 {\out1. !!a list. itrev list [] = rev list\(\;\)==> itrev list [a] = rev list @ [a]}

 \end{ttbox}

 Just as predicted above, the overall goal, and hence the induction

 hypothesis, is too weak to solve the induction step because of the fixed

 \texttt{[]}. The corresponding heuristic:

 \begin{quote}

 {\em 3. Generalize goals for induction by replacing constants by variables.}

 \end{quote}

 Of course one cannot do this na\"{\i}vely: \texttt{itrev xs ys = rev xs} is

 just not true --- the correct generalization is

 \begin{ttbox}\makeatother

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

 If \texttt{ys} is replaced by \texttt{[]}, the right-hand side simplifies to

 \texttt{rev xs}, just as required.

 In this particular instance it is easy to guess the right generalization,

 but in more complex situations a good deal of creativity is needed. This is

 the main source of complications in inductive proofs.

 Although we now have two variables, only \texttt{xs} is suitable for

 induction, and we repeat our above proof attempt. Unfortunately, we are still

 not there:

 \begin{ttbox}\makeatother

 {\out 1. !!a list.}

 {\out       itrev list ys = rev list @ ys}

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

 \end{ttbox}

 The induction hypothesis is still too weak, but this time it takes no

 intuition to generalize: the problem is that \texttt{ys} is fixed throughout

 the subgoal, but the induction hypothesis needs to be applied with

 \texttt{a \# ys} instead of \texttt{ys}. Hence we prove the theorem

 for all \texttt{ys} instead of a fixed one:

 \begin{ttbox}\makeatother

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

 This time induction on \texttt{xs} followed by simplification succeeds. This

 leads to another heuristic for generalization:

 \begin{quote}

 {\em 4. Generalize goals for induction by universally quantifying all free

 variables {\em(except the induction variable itself!)}.}

 \end{quote}

 This prevents trivial failures like the above and does not change the

 provability of the goal. Because it is not always required, and may even

 complicate matters in some cases, this heuristic is often not

 applied blindly.

 A final point worth mentioning is the orientation of the equation we just

 proved: the more complex notion (\texttt{itrev}) is on the left-hand

 side, the simpler \texttt{rev} on the right-hand side. This constitutes

 another, albeit weak heuristic that is not restricted to induction:

 \begin{quote}

   {\em 5. The right-hand side of an equation should (in some sense) be

     simpler than the left-hand side.}

 \end{quote}

 The heuristic is tricky to apply because it is not obvious that

 \texttt{rev xs \at\ ys} is simpler than \texttt{itrev xs ys}. But see what

 happens if you try to prove the symmetric equation!

 \section{Case study: compiling expressions}

 \label{sec:ExprCompiler}

 The task is to develop a compiler from a generic type of expressions (built

 up from variables, constants and binary operations) to a stack machine.  This

 generic type of expressions is a generalization of the boolean expressions in

 \S\ref{sec:boolex}.  This time we do not commit ourselves to a particular

 type of variables or values but make them type parameters.  Neither is there

 a fixed set of binary operations: instead the expression contains the

 appropriate function itself.

 \begin{ttbox}

 \input{CodeGen/expr}\end{ttbox}

 The three constructors represent constants, variables and the combination of

 two subexpressions with a binary operation.

 The value of an expression w.r.t.\ an environment that maps variables to

 values is easily defined:

 \begin{ttbox}

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

 The stack machine has three instructions: load a constant value onto the

 stack, load the contents of a certain address onto the stack, and apply a

 binary operation to the two topmost elements of the stack, replacing them by

 the result. As for \texttt{expr}, addresses and values are type parameters:

 \begin{ttbox}

 \input{CodeGen/instr}\end{ttbox}

 The execution of the stack machine is modelled by a function \texttt{exec}

 that takes a store (modelled as a function from addresses to values, just

 like the environment for evaluating expressions), a stack (modelled as a

 list) of values and a list of instructions and returns the stack at the end

 of the execution --- the store remains unchanged:

 \begin{ttbox}

 \input{CodeGen/exec}\end{ttbox}

 Recall that \texttt{hd} and \texttt{tl}

 return the first element and the remainder of a list.

 Because all functions are total, \texttt{hd} is defined even for the empty

 list, although we do not know what the result is. Thus our model of the

 machine always terminates properly, although the above definition does not

 tell us much about the result in situations where \texttt{Apply} was executed

 with fewer than two elements on the stack.

 The compiler is a function from expressions to a list of instructions. Its

 definition is pretty much obvious:

 \begin{ttbox}\makeatother

 \input{CodeGen/comp}\end{ttbox}

 Now we have to prove the correctness of the compiler, i.e.\ that the

 execution of a compiled expression results in the value of the expression:

 \begin{ttbox}

 exec s [] (comp e) = [value s e]

 \end{ttbox}

 This is generalized to

 \begin{ttbox}

 \input{CodeGen/goal2.ML}\end{ttbox}

 and proved by induction on \texttt{e} followed by simplification, once we

 have the following lemma about executing the concatenation of two instruction

 sequences:

 \begin{ttbox}\makeatother

 \input{CodeGen/goal2.ML}\end{ttbox}

 This requires induction on \texttt{xs} and ordinary simplification for the

 base cases. In the induction step, simplification leaves us with a formula

 that contains two \texttt{case}-expressions over instructions. Thus we add

 automatic case splitting as well, which finishes the proof:

 \begin{ttbox}

 \input{CodeGen/simpsplit.ML}\end{ttbox}

 We could now go back and prove \texttt{exec s [] (comp e) = [value s e]}

 merely by simplification with the generalized version we just proved.

 However, this is unnecessary because the generalized version fully subsumes

 its instance.

 \section{Total recursive functions}

 \label{sec:recdef}

 \index{*recdef|(}

 Although many total functions have a natural primitive recursive definition,

 this is not always the case. Arbitrary total recursive functions can be

 defined by means of \texttt{recdef}: you can use full pattern-matching,

 recursion need not involve datatypes, and termination is proved by showing

 that each recursive call makes the argument smaller in a suitable (user

 supplied) sense.

 \subsection{Defining recursive functions}

 Here is a simple example, the Fibonacci function:

 \begin{ttbox}

 consts fib  :: nat => nat

 recdef fib "measure(\%n. n)"

     "fib 0 = 0"

     "fib 1 = 1"

     "fib (Suc(Suc x)) = fib x + fib (Suc x)"

 \end{ttbox}

 The definition of \texttt{fib} is accompanied by a \bfindex{measure function}

 \texttt{\%n.$\;$n} that maps the argument of \texttt{fib} to a natural

 number. The requirement is that in each equation the measure of the argument

 on the left-hand side is strictly greater than the measure of the argument of

 each recursive call. In the case of \texttt{fib} this is obviously true

 because the measure function is the identity and \texttt{Suc(Suc~x)} is

 strictly greater than both \texttt{x} and \texttt{Suc~x}.

 Slightly more interesting is the insertion of a fixed element

 between any two elements of a list:

 \begin{ttbox}

 consts sep :: "'a * 'a list => 'a list"

 recdef sep "measure (\%(a,xs). length xs)"

     "sep(a, [])     = []"

     "sep(a, [x])    = [x]"

     "sep(a, x#y#zs) = x # a # sep(a,y#zs)"

 \end{ttbox}

 This time the measure is the length of the list, which decreases with the

 recursive call; the first component of the argument tuple is irrelevant.

 Pattern matching need not be exhaustive:

 \begin{ttbox}

 consts last :: 'a list => bool

 recdef last "measure (\%xs. length xs)"

     "last [x]      = x"

     "last (x#y#zs) = last (y#zs)"

 \end{ttbox}

 Overlapping patterns are disambiguated by taking the order of equations into

 account, just as in functional programming:

 \begin{ttbox}

 recdef sep "measure (\%(a,xs). length xs)"

     "sep(a, x#y#zs) = x # a # sep(a,y#zs)"

     "sep(a, xs)     = xs"

 \end{ttbox}

 This defines exactly the same function \texttt{sep} as further above.

 \begin{warn}

 Currently \texttt{recdef} only accepts functions with a single argument,

 possibly of tuple type.

 \end{warn}

 When loading a theory containing a \texttt{recdef} of a function $f$,

 Isabelle proves the recursion equations and stores the result as a list of

 theorems $f$.\texttt{rules}. It can be viewed by typing

 \begin{ttbox}

 prths \(f\).rules;

 \end{ttbox}

 All of the above examples are simple enough that Isabelle can determine

 automatically that the measure of the argument goes down in each recursive

 call. In that case $f$.\texttt{rules} contains precisely the defining

 equations.

 In general, Isabelle may not be able to prove all termination conditions

 automatically. For example, termination of

 \begin{ttbox}

 consts gcd :: "nat*nat => nat"

 recdef gcd "measure ((\%(m,n).n))"

     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

 \end{ttbox}

 relies on the lemma \texttt{mod_less_divisor}

 \begin{ttbox}

 0 < n ==> m mod n < n

 \end{ttbox}

 that is not part of the default simpset. As a result, Isabelle prints a

 warning and \texttt{gcd.rules} contains a precondition:

 \begin{ttbox}

 (! m n. 0 < n --> m mod n < n) ==> gcd (m, n) = (if n=0 \dots)

 \end{ttbox}

 We need to instruct \texttt{recdef} to use an extended simpset to prove the

 termination condition:

 \begin{ttbox}

 recdef gcd "measure ((\%(m,n).n))"

   simpset "simpset() addsimps [mod_less_divisor]"

     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

 \end{ttbox}

 This time everything works fine and \texttt{gcd.rules} contains precisely the

 stated recursion equation for \texttt{gcd}.

 When defining some nontrivial total recursive function, the first attempt

 will usually generate a number of termination conditions, some of which may

 require new lemmas to be proved in some of the parent theories. Those lemmas

 can then be added to the simpset used by \texttt{recdef} for its

 proofs, as shown for \texttt{gcd}.

 Although all the above examples employ measure functions, \texttt{recdef}

 allows arbitrary wellfounded relations. For example, termination of

 Ackermann's function requires the lexicographic product \texttt{**}:

 \begin{ttbox}

 recdef ack "measure(\%m. m) ** measure(\%n. n)"

     "ack(0,n)         = Suc n"

     "ack(Suc m,0)     = ack(m, 1)"

     "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"

 \end{ttbox}

 For details see~\cite{Isa-Logics-Man} and the examples in the library.

 \subsection{Deriving simplification rules}

 Once we have succeeded to prove all termination conditions, we can start to

 derive some theorems. In contrast to \texttt{primrec} definitions, which are

 automatically added to the simpset, \texttt{recdef} rules must be included

 explicitly, for example as in

 \begin{ttbox}

 Addsimps fib.rules;

 \end{ttbox}

 However, some care is necessary now, in contrast to \texttt{primrec}.

 Although \texttt{gcd} is a total function, its defining equation leads to

 nontermination of the simplifier, because the subterm \texttt{gcd(n, m mod

   n)} on the right-hand side can again be simplified by the same equation,

 and so on. The reason: the simplifier rewrites the \texttt{then} and

 \texttt{else} branches of a conditional if the condition simplifies to

 neither \texttt{True} nor \texttt{False}.  Therefore it is recommended to

 derive an alternative formulation that replaces case distinctions on the

 right-hand side by conditional equations. For \texttt{gcd} it means we have

 to prove

 \begin{ttbox}

            gcd (m, 0) = m

 n ~= 0 ==> gcd (m, n) = gcd(n, m mod n)

 \end{ttbox}

 To avoid nontermination during those proofs, we have to resort to some low

 level tactics:

 \begin{ttbox}

 Goal "gcd(m,0) = m";

 by(resolve_tac [trans] 1);

 by(resolve_tac gcd.rules 1);

 by(Simp_tac 1);

 \end{ttbox}

 At this point it is not necessary to understand what exactly

 \texttt{resolve_tac} is doing. The main point is that the above proof works

 not just for this one example but in general (except that we have to use

 \texttt{Asm_simp_tac} and $f$\texttt{.rules} in general). Try the second

 \texttt{gcd}-equation above!

 \subsection{Induction}

 Assuming we have added the recursion equations (or some suitable derived

 equations) to the simpset, we might like to prove something about our

 function. Since the function is recursive, the natural proof principle is

 again induction. But this time the structural form of induction that comes

 with datatypes is unlikely to work well---otherwise we could have defined the

 function by \texttt{primrec}. Therefore \texttt{recdef} automatically proves

 a suitable induction rule $f$\texttt{.induct} that follows the recursion

 pattern of the particular function $f$. Roughly speaking, it requires you to

 prove for each \texttt{recdef} equation that the property you are trying to

 establish holds for the left-hand side provided it holds for all recursive

 calls on the right-hand side. Applying $f$\texttt{.induct} requires its

 explicit instantiation. See \S\ref{sec:explicit-inst} for details.

 \index{*recdef|)}