1.1 --- a/doc-src/HOL/HOL.tex Thu May 26 14:24:26 2011 +0200
1.2 +++ b/doc-src/HOL/HOL.tex Thu May 26 15:56:39 2011 +0200
1.3 @@ -1589,7 +1589,7 @@
1.4 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).
1.5
1.6 \texttt{List} provides a basic library of list processing functions defined by
1.7 -primitive recursion (see~{\S}\ref{sec:HOL:primrec}). The recursion equations
1.8 +primitive recursion. The recursion equations
1.9 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.
1.10
1.11 \index{list@{\textit{list}} type|)}
1.12 @@ -1938,229 +1938,21 @@
1.13 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
1.14
1.15
1.16 -\section{Recursive function definitions}\label{sec:HOL:recursive}
1.17 -\index{recursive functions|see{recursion}}
1.18 -
1.19 -Isabelle/HOL provides two main mechanisms of defining recursive functions.
1.20 -\begin{enumerate}
1.21 -\item \textbf{Primitive recursion} is available only for datatypes, and it is
1.22 - somewhat restrictive. Recursive calls are only allowed on the argument's
1.23 - immediate constituents. On the other hand, it is the form of recursion most
1.24 - often wanted, and it is easy to use.
1.25 -
1.26 -\item \textbf{Well-founded recursion} requires that you supply a well-founded
1.27 - relation that governs the recursion. Recursive calls are only allowed if
1.28 - they make the argument decrease under the relation. Complicated recursion
1.29 - forms, such as nested recursion, can be dealt with. Termination can even be
1.30 - proved at a later time, though having unsolved termination conditions around
1.31 - can make work difficult.%
1.32 - \footnote{This facility is based on Konrad Slind's TFL
1.33 - package~\cite{slind-tfl}. Thanks are due to Konrad for implementing TFL
1.34 - and assisting with its installation.}
1.35 -\end{enumerate}
1.36 -
1.37 -Following good HOL tradition, these declarations do not assert arbitrary
1.38 -axioms. Instead, they define the function using a recursion operator. Both
1.39 -HOL and ZF derive the theory of well-founded recursion from first
1.40 -principles~\cite{paulson-set-II}. Primitive recursion over some datatype
1.41 -relies on the recursion operator provided by the datatype package. With
1.42 -either form of function definition, Isabelle proves the desired recursion
1.43 -equations as theorems.
1.44 -
1.45 -
1.46 -\subsection{Primitive recursive functions}
1.47 -\label{sec:HOL:primrec}
1.48 -\index{recursion!primitive|(}
1.49 -\index{*primrec|(}
1.50 -
1.51 -Datatypes come with a uniform way of defining functions, {\bf primitive
1.52 - recursion}. In principle, one could introduce primitive recursive functions
1.53 -by asserting their reduction rules as new axioms, but this is not recommended:
1.54 -\begin{ttbox}\slshape
1.55 -Append = Main +
1.56 -consts app :: ['a list, 'a list] => 'a list
1.57 -rules
1.58 - app_Nil "app [] ys = ys"
1.59 - app_Cons "app (x#xs) ys = x#app xs ys"
1.60 -end
1.61 -\end{ttbox}
1.62 -Asserting axioms brings the danger of accidentally asserting nonsense, as
1.63 -in \verb$app [] ys = us$.
1.64 -
1.65 -The \ttindex{primrec} declaration is a safe means of defining primitive
1.66 -recursive functions on datatypes:
1.67 -\begin{ttbox}
1.68 -Append = Main +
1.69 -consts app :: ['a list, 'a list] => 'a list
1.70 -primrec
1.71 - "app [] ys = ys"
1.72 - "app (x#xs) ys = x#app xs ys"
1.73 -end
1.74 -\end{ttbox}
1.75 -Isabelle will now check that the two rules do indeed form a primitive
1.76 -recursive definition. For example
1.77 -\begin{ttbox}
1.78 -primrec
1.79 - "app [] ys = us"
1.80 -\end{ttbox}
1.81 -is rejected with an error message ``\texttt{Extra variables on rhs}''.
1.82 -
1.83 -\bigskip
1.84 -
1.85 -The general form of a primitive recursive definition is
1.86 -\begin{ttbox}
1.87 -primrec
1.88 - {\it reduction rules}
1.89 -\end{ttbox}
1.90 -where \textit{reduction rules} specify one or more equations of the form
1.91 -\[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
1.92 -\dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$
1.93 -contains only the free variables on the left-hand side, and all recursive
1.94 -calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There
1.95 -must be at most one reduction rule for each constructor. The order is
1.96 -immaterial. For missing constructors, the function is defined to return a
1.97 -default value.
1.98 -
1.99 -If you would like to refer to some rule by name, then you must prefix
1.100 -the rule with an identifier. These identifiers, like those in the
1.101 -\texttt{rules} section of a theory, will be visible at the \ML\ level.
1.102 -
1.103 -The primitive recursive function can have infix or mixfix syntax:
1.104 -\begin{ttbox}\underscoreon
1.105 -consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
1.106 -primrec
1.107 - "[] @ ys = ys"
1.108 - "(x#xs) @ ys = x#(xs @ ys)"
1.109 -\end{ttbox}
1.110 -
1.111 -The reduction rules become part of the default simpset, which
1.112 -leads to short proof scripts:
1.113 -\begin{ttbox}\underscoreon
1.114 -Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";
1.115 -by (induct\_tac "xs" 1);
1.116 -by (ALLGOALS Asm\_simp\_tac);
1.117 -\end{ttbox}
1.118 -
1.119 -\subsubsection{Example: Evaluation of expressions}
1.120 -Using mutual primitive recursion, we can define evaluation functions \texttt{evala}
1.121 -and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in
1.122 -{\S}\ref{subsec:datatype:basics}:
1.123 -\begin{ttbox}
1.124 -consts
1.125 - evala :: "['a => nat, 'a aexp] => nat"
1.126 - evalb :: "['a => nat, 'a bexp] => bool"
1.127 -
1.128 -primrec
1.129 - "evala env (If_then_else b a1 a2) =
1.130 - (if evalb env b then evala env a1 else evala env a2)"
1.131 - "evala env (Sum a1 a2) = evala env a1 + evala env a2"
1.132 - "evala env (Diff a1 a2) = evala env a1 - evala env a2"
1.133 - "evala env (Var v) = env v"
1.134 - "evala env (Num n) = n"
1.135 -
1.136 - "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
1.137 - "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
1.138 - "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"
1.139 -\end{ttbox}
1.140 -Since the value of an expression depends on the value of its variables,
1.141 -the functions \texttt{evala} and \texttt{evalb} take an additional
1.142 -parameter, an {\em environment} of type \texttt{'a => nat}, which maps
1.143 -variables to their values.
1.144 -
1.145 -Similarly, we may define substitution functions \texttt{substa}
1.146 -and \texttt{substb} for expressions: The mapping \texttt{f} of type
1.147 -\texttt{'a => 'a aexp} given as a parameter is lifted canonically
1.148 -on the types \texttt{'a aexp} and \texttt{'a bexp}:
1.149 -\begin{ttbox}
1.150 -consts
1.151 - substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"
1.152 - substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"
1.153 -
1.154 -primrec
1.155 - "substa f (If_then_else b a1 a2) =
1.156 - If_then_else (substb f b) (substa f a1) (substa f a2)"
1.157 - "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
1.158 - "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
1.159 - "substa f (Var v) = f v"
1.160 - "substa f (Num n) = Num n"
1.161 -
1.162 - "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
1.163 - "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
1.164 - "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"
1.165 -\end{ttbox}
1.166 -In textbooks about semantics one often finds {\em substitution theorems},
1.167 -which express the relationship between substitution and evaluation. For
1.168 -\texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual
1.169 -induction, followed by simplification:
1.170 -\begin{ttbox}
1.171 -Goal
1.172 - "evala env (substa (Var(v := a')) a) =
1.173 - evala (env(v := evala env a')) a &
1.174 - evalb env (substb (Var(v := a')) b) =
1.175 - evalb (env(v := evala env a')) b";
1.176 -by (induct_tac "a b" 1);
1.177 -by (ALLGOALS Asm_full_simp_tac);
1.178 -\end{ttbox}
1.179 -
1.180 -\subsubsection{Example: A substitution function for terms}
1.181 -Functions on datatypes with nested recursion, such as the type
1.182 -\texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are
1.183 -also defined by mutual primitive recursion. A substitution
1.184 -function \texttt{subst_term} on type \texttt{term}, similar to the functions
1.185 -\texttt{substa} and \texttt{substb} described above, can
1.186 -be defined as follows:
1.187 -\begin{ttbox}
1.188 -consts
1.189 - subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"
1.190 - subst_term_list ::
1.191 - "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"
1.192 -
1.193 -primrec
1.194 - "subst_term f (Var a) = f a"
1.195 - "subst_term f (App b ts) = App b (subst_term_list f ts)"
1.196 -
1.197 - "subst_term_list f [] = []"
1.198 - "subst_term_list f (t # ts) =
1.199 - subst_term f t # subst_term_list f ts"
1.200 -\end{ttbox}
1.201 -The recursion scheme follows the structure of the unfolded definition of type
1.202 -\texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of
1.203 -this substitution function, mutual induction is needed:
1.204 -\begin{ttbox}
1.205 -Goal
1.206 - "(subst_term ((subst_term f1) o f2) t) =
1.207 - (subst_term f1 (subst_term f2 t)) &
1.208 - (subst_term_list ((subst_term f1) o f2) ts) =
1.209 - (subst_term_list f1 (subst_term_list f2 ts))";
1.210 -by (induct_tac "t ts" 1);
1.211 -by (ALLGOALS Asm_full_simp_tac);
1.212 -\end{ttbox}
1.213 -
1.214 -\subsubsection{Example: A map function for infinitely branching trees}
1.215 -Defining functions on infinitely branching datatypes by primitive
1.216 -recursion is just as easy. For example, we can define a function
1.217 -\texttt{map_tree} on \texttt{'a tree} as follows:
1.218 -\begin{ttbox}
1.219 -consts
1.220 - map_tree :: "('a => 'b) => 'a tree => 'b tree"
1.221 -
1.222 -primrec
1.223 - "map_tree f (Atom a) = Atom (f a)"
1.224 - "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"
1.225 -\end{ttbox}
1.226 -Note that all occurrences of functions such as \texttt{ts} in the
1.227 -\texttt{primrec} clauses must be applied to an argument. In particular,
1.228 -\texttt{map_tree f o ts} is not allowed.
1.229 -
1.230 -\index{recursion!primitive|)}
1.231 -\index{*primrec|)}
1.232 -
1.233 -
1.234 -\subsection{General recursive functions}
1.235 -\label{sec:HOL:recdef}
1.236 +\section{Old-style recursive function definitions}\label{sec:HOL:recursive}
1.237 \index{recursion!general|(}
1.238 \index{*recdef|(}
1.239
1.240 +Old-style recursive definitions via \texttt{recdef} requires that you
1.241 +supply a well-founded relation that governs the recursion. Recursive
1.242 +calls are only allowed if they make the argument decrease under the
1.243 +relation. Complicated recursion forms, such as nested recursion, can
1.244 +be dealt with. Termination can even be proved at a later time, though
1.245 +having unsolved termination conditions around can make work
1.246 +difficult.%
1.247 +\footnote{This facility is based on Konrad Slind's TFL
1.248 + package~\cite{slind-tfl}. Thanks are due to Konrad for implementing
1.249 + TFL and assisting with its installation.}
1.250 +
1.251 Using \texttt{recdef}, you can declare functions involving nested recursion
1.252 and pattern-matching. Recursion need not involve datatypes and there are few
1.253 syntactic restrictions. Termination is proved by showing that each recursive