3 \def\isabellecontext{fun{\isadigit{0}}}%
18 \begin{isamarkuptext}%
19 \subsection{Definition}
20 \label{sec:fun-examples}
22 Here is a simple example, the \rmindex{Fibonacci function}:%
25 \isacommand{fun}\isamarkupfalse%
26 \ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
27 {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
28 {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
29 {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequoteclose}%
30 \begin{isamarkuptext}%
32 This resembles ordinary functional programming languages. Note the obligatory
33 \isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
34 defines the function in one go. Isabelle establishes termination automatically
35 because \isa{fib}'s argument decreases in every recursive call.
37 Slightly more interesting is the insertion of a fixed element
38 between any two elements of a list:%
41 \isacommand{fun}\isamarkupfalse%
42 \ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
43 {\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
44 {\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
45 {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
46 \begin{isamarkuptext}%
48 This time the length of the list decreases with the
49 recursive call; the first argument is irrelevant for termination.
51 Pattern matching\index{pattern matching!and \isacommand{fun}}
52 need not be exhaustive and may employ wildcards:%
55 \isacommand{fun}\isamarkupfalse%
56 \ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
57 {\isachardoublequoteopen}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
58 {\isachardoublequoteopen}last\ {\isacharparenleft}{\isacharunderscore}{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
59 \begin{isamarkuptext}%
60 Overlapping patterns are disambiguated by taking the order of equations into
61 account, just as in functional programming:%
64 \isacommand{fun}\isamarkupfalse%
65 \ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
66 {\isachardoublequoteopen}sep{\isadigit{1}}\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
67 {\isachardoublequoteopen}sep{\isadigit{1}}\ {\isacharunderscore}\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
68 \begin{isamarkuptext}%
70 To guarantee that the second equation can only be applied if the first
71 one does not match, Isabelle internally replaces the second equation
72 by the two possibilities that are left: \isa{sep{\isadigit{1}}\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} and
73 \isa{sep{\isadigit{1}}\ a\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}}. Thus the functions \isa{sep} and
74 \isa{sep{\isadigit{1}}} are identical.
76 Because of its pattern matching syntax, \isacommand{fun} is also useful
77 for the definition of non-recursive functions:%
80 \isacommand{fun}\isamarkupfalse%
81 \ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
82 {\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequoteclose}\ {\isacharbar}\isanewline
83 {\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequoteclose}%
84 \begin{isamarkuptext}%
85 After a function~$f$ has been defined via \isacommand{fun},
86 its defining equations (or variants derived from them) are available
87 under the name $f$\isa{{\isachardot}simps} as theorems.
88 For example, look (via \isacommand{thm}) at
89 \isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define
90 the same function. What is more, those equations are automatically declared as
93 \subsection{Termination}
95 Isabelle's automatic termination prover for \isacommand{fun} has a
96 fixed notion of the \emph{size} (of type \isa{nat}) of an
97 argument. The size of a natural number is the number itself. The size
98 of a list is its length. For the general case see \S\ref{sec:general-datatype}.
99 A recursive function is accepted if \isacommand{fun} can
100 show that the size of one fixed argument becomes smaller with each
103 More generally, \isacommand{fun} allows any \emph{lexicographic
104 combination} of size measures in case there are multiple
105 arguments. For example, the following version of \rmindex{Ackermann's
106 function} is accepted:%
109 \isacommand{fun}\isamarkupfalse%
110 \ ack{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
111 {\isachardoublequoteopen}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isacharequal}\ Suc\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline
112 {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
113 {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}ack{\isadigit{2}}\ n\ {\isacharparenleft}Suc\ m{\isacharparenright}{\isacharparenright}\ m{\isachardoublequoteclose}%
114 \begin{isamarkuptext}%
115 The order of arguments has no influence on whether
116 \isacommand{fun} can prove termination of a function. For more details
117 see elsewhere~\cite{bulwahnKN07}.
119 \subsection{Simplification}
120 \label{sec:fun-simplification}
122 Upon a successful termination proof, the recursion equations become
123 simplification rules, just as with \isacommand{primrec}.
124 In most cases this works fine, but there is a subtle
125 problem that must be mentioned: simplification may not
126 terminate because of automatic splitting of \isa{if}.
127 \index{*if expressions!splitting of}
128 Let us look at an example:%
131 \isacommand{fun}\isamarkupfalse%
132 \ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
133 {\isachardoublequoteopen}gcd\ m\ n\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
134 \begin{isamarkuptext}%
136 The second argument decreases with each recursive call.
137 The termination condition
139 \ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
141 is proved automatically because it is already present as a lemma in
142 HOL\@. Thus the recursion equation becomes a simplification
143 rule. Of course the equation is nonterminating if we are allowed to unfold
144 the recursive call inside the \isa{else} branch, which is why programming
145 languages and our simplifier don't do that. Unfortunately the simplifier does
146 something else that leads to the same problem: it splits
147 each \isa{if}-expression unless its
148 condition simplifies to \isa{True} or \isa{False}. For
149 example, simplification reduces
151 \ \ \ \ \ gcd\ m\ n\ {\isacharequal}\ k%
155 \ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
157 where the condition cannot be reduced further, and splitting leads to
159 \ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
161 Since the recursive call \isa{gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}} is no longer protected by
162 an \isa{if}, it is unfolded again, which leads to an infinite chain of
163 simplification steps. Fortunately, this problem can be avoided in many
166 The most radical solution is to disable the offending theorem
167 \isa{split{\isacharunderscore}if},
168 as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
169 approach: you will often have to invoke the rule explicitly when
170 \isa{if} is involved.
172 If possible, the definition should be given by pattern matching on the left
173 rather than \isa{if} on the right. In the case of \isa{gcd} the
174 following alternative definition suggests itself:%
177 \isacommand{fun}\isamarkupfalse%
178 \ gcd{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
179 {\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
180 {\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ n\ {\isacharequal}\ gcd{\isadigit{1}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}%
181 \begin{isamarkuptext}%
183 The order of equations is important: it hides the side condition
184 \isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, not all conditionals can be
185 expressed by pattern matching.
187 A simple alternative is to replace \isa{if} by \isa{case},
188 which is also available for \isa{bool} and is not split automatically:%
191 \isacommand{fun}\isamarkupfalse%
192 \ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
193 {\isachardoublequoteopen}gcd{\isadigit{2}}\ m\ n\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
194 \begin{isamarkuptext}%
196 This is probably the neatest solution next to pattern matching, and it is
199 A final alternative is to replace the offending simplification rules by
200 derived conditional ones. For \isa{gcd} it means we have to prove
204 \isacommand{lemma}\isamarkupfalse%
205 \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}gcd\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
212 \isacommand{apply}\isamarkupfalse%
213 {\isacharparenleft}simp{\isacharparenright}\isanewline
214 \isacommand{done}\isamarkupfalse%
224 \isacommand{lemma}\isamarkupfalse%
225 \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd\ m\ n\ {\isacharequal}\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
232 \isacommand{apply}\isamarkupfalse%
233 {\isacharparenleft}simp{\isacharparenright}\isanewline
234 \isacommand{done}\isamarkupfalse%
243 \begin{isamarkuptext}%
245 Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}.
246 Now we can disable the original simplification rule:%
249 \isacommand{declare}\isamarkupfalse%
250 \ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
251 \begin{isamarkuptext}%
252 \index{induction!recursion|(}
253 \index{recursion induction|(}
255 \subsection{Induction}
256 \label{sec:fun-induction}
258 Having defined a function we might like to prove something about it.
259 Since the function is recursive, the natural proof principle is
260 again induction. But this time the structural form of induction that comes
261 with datatypes is unlikely to work well --- otherwise we could have defined the
262 function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
263 proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
264 recursion pattern of the particular function $f$. We call this
265 \textbf{recursion induction}. Roughly speaking, it
266 requires you to prove for each \isacommand{fun} equation that the property
267 you are trying to establish holds for the left-hand side provided it holds
268 for all recursive calls on the right-hand side. Here is a simple example
269 involving the predefined \isa{map} functional on lists:%
272 \isacommand{lemma}\isamarkupfalse%
273 \ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep\ x\ xs{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}map\ f\ xs{\isacharparenright}{\isachardoublequoteclose}%
280 \begin{isamarkuptxt}%
282 Note that \isa{map\ f\ xs}
283 is the result of applying \isa{f} to all elements of \isa{xs}. We prove
284 this lemma by recursion induction over \isa{sep}:%
287 \isacommand{apply}\isamarkupfalse%
288 {\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
289 \begin{isamarkuptxt}%
291 The resulting proof state has three subgoals corresponding to the three
292 clauses for \isa{sep}:
294 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
295 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline
296 \ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline
297 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
298 \isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}%
300 The rest is pure simplification:%
303 \isacommand{apply}\isamarkupfalse%
304 \ simp{\isacharunderscore}all\isanewline
305 \isacommand{done}\isamarkupfalse%
314 \begin{isamarkuptext}%
315 \noindent The proof goes smoothly because the induction rule
316 follows the recursion of \isa{sep}. Try proving the above lemma by
317 structural induction, and you find that you need an additional case
320 In general, the format of invoking recursion induction is
322 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
323 \end{quote}\index{*induct_tac (method)}%
324 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
325 name of a function that takes $n$ arguments. Usually the subgoal will
326 contain the term $f x@1 \dots x@n$ but this need not be the case. The
327 induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
329 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
330 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline
331 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
332 {\isasymLongrightarrow}~P~u~v%
334 It merely says that in order to prove a property \isa{P} of \isa{u} and
335 \isa{v} you need to prove it for the three cases where \isa{v} is the
336 empty list, the singleton list, and the list with at least two elements.
337 The final case has an induction hypothesis: you may assume that \isa{P}
338 holds for the tail of that list.
339 \index{induction!recursion|)}
340 \index{recursion induction|)}%
359 %%% TeX-master: "root"