1 (* Title: Doc/IsarAdvanced/Functions/Thy/Fundefs.thy
3 Author: Alexander Krauss, TU Muenchen
5 Tutorial for function definitions with the new "function" package.
12 section {* Function Definitions for Dummies *}
15 In most cases, defining a recursive function is just as simple as other definitions:
18 fun fib :: "nat \<Rightarrow> nat"
22 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
25 The syntax is rather self-explanatory: We introduce a function by
26 giving its name, its type and a set of defining recursive
31 The function always terminates, since its argument gets smaller in
33 Since HOL is a logic of total functions, termination is a
34 fundamental requirement to prevent inconsistencies\footnote{From the
35 \qt{definition} @{text "f(n) = f(n) + 1"} we could prove
36 @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}.
37 Isabelle tries to prove termination automatically when a definition
38 is made. In \S\ref{termination}, we will look at cases where this
39 fails and see what to do then.
42 subsection {* Pattern matching *}
44 text {* \label{patmatch}
45 Like in functional programming, we can use pattern matching to
46 define functions. At the moment we will only consider \emph{constructor
47 patterns}, which only consist of datatype constructors and
48 variables. Furthermore, patterns must be linear, i.e.\ all variables
49 on the left hand side of an equation must be distinct. In
50 \S\ref{genpats} we discuss more general pattern matching.
52 If patterns overlap, the order of the equations is taken into
53 account. The following function inserts a fixed element between any
54 two elements of a list:
57 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
59 "sep a (x#y#xs) = x # a # sep a (y # xs)"
63 Overlapping patterns are interpreted as \qt{increments} to what is
64 already there: The second equation is only meant for the cases where
65 the first one does not match. Consequently, Isabelle replaces it
66 internally by the remaining cases, making the patterns disjoint:
71 text {* @{thm [display] sep.simps[no_vars]} *}
74 \noindent The equations from function definitions are automatically used in
78 lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"
81 subsection {* Induction *}
85 Isabelle provides customized induction rules for recursive
86 functions. These rules follow the recursive structure of the
87 definition. Here is the rule @{text sep.induct} arising from the
88 above definition of @{const sep}:
90 @{thm [display] sep.induct}
92 We have a step case for list with at least two elements, and two
93 base cases for the zero- and the one-element list. Here is a simple
94 proof about @{const sep} and @{const map}
97 lemma "map f (sep x ys) = sep (f x) (map f ys)"
98 apply (induct x ys rule: sep.induct)
101 We get three cases, like in the definition.
103 @{subgoals [display]}
110 With the \cmd{fun} command, you can define about 80\% of the
111 functions that occur in practice. The rest of this tutorial explains
116 section {* fun vs.\ function *}
119 The \cmd{fun} command provides a
120 convenient shorthand notation for simple function definitions. In
121 this mode, Isabelle tries to solve all the necessary proof obligations
122 automatically. If a proof fails, the definition is
123 rejected. This can either mean that the definition is indeed faulty,
124 or that the default proof procedures are just not smart enough (or
125 rather: not designed) to handle the definition.
127 By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or
128 solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:
133 \[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}
134 \cmd{fun} @{text "f :: \<tau>"}\\%
136 \hspace*{2ex}{\it equations}\\%
137 \hspace*{2ex}\vdots\vspace*{6pt}
138 \end{minipage}\right]
140 \left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
141 \cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
143 \hspace*{2ex}{\it equations}\\%
144 \hspace*{2ex}\vdots\\%
145 \cmd{by} @{text "pat_completeness auto"}\\%
146 \cmd{termination by} @{text "lexicographic_order"}\vspace{6pt}
150 \begin{isamarkuptext}
152 \noindent Some details have now become explicit:
155 \item The \cmd{sequential} option enables the preprocessing of
156 pattern overlaps which we already saw. Without this option, the equations
157 must already be disjoint and complete. The automatic completion only
158 works with constructor patterns.
160 \item A function definition produces a proof obligation which
161 expresses completeness and compatibility of patterns (we talk about
162 this later). The combination of the methods @{text "pat_completeness"} and
163 @{text "auto"} is used to solve this proof obligation.
165 \item A termination proof follows the definition, started by the
166 \cmd{termination} command. This will be explained in \S\ref{termination}.
168 Whenever a \cmd{fun} command fails, it is usually a good idea to
169 expand the syntax to the more verbose \cmd{function} form, to see
170 what is actually going on.
174 section {* Termination *}
176 text {*\label{termination}
177 The method @{text "lexicographic_order"} is the default method for
178 termination proofs. It can prove termination of a
179 certain class of functions by searching for a suitable lexicographic
180 combination of size measures. Of course, not all functions have such
181 a simple termination argument. For them, we can specify the termination
185 subsection {* The {\tt relation} method *}
187 Consider the following function, which sums up natural numbers up to
188 @{text "N"}, using a counter @{text "i"}:
191 function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
193 "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
194 by pat_completeness auto
197 \noindent The @{text "lexicographic_order"} method fails on this example, because none of the
198 arguments decreases in the recursive call, with respect to the standard size ordering.
199 To prove termination manually, we must provide a custom wellfounded relation.
201 The termination argument for @{text "sum"} is based on the fact that
202 the \emph{difference} between @{text "i"} and @{text "N"} gets
203 smaller in every step, and that the recursion stops when @{text "i"}
204 is greater than @{text "N"}. Phrased differently, the expression
205 @{text "N + 1 - i"} always decreases.
207 We can use this expression as a measure function suitable to prove termination.
211 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
214 The \cmd{termination} command sets up the termination goal for the
215 specified function @{text "sum"}. If the function name is omitted, it
216 implicitly refers to the last function definition.
218 The @{text relation} method takes a relation of
219 type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of
220 the function. If the function has multiple curried arguments, then
221 these are packed together into a tuple, as it happened in the above
224 The predefined function @{term_type "measure"} constructs a
225 wellfounded relation from a mapping into the natural numbers (a
226 \emph{measure function}).
228 After the invocation of @{text "relation"}, we must prove that (a)
229 the relation we supplied is wellfounded, and (b) that the arguments
230 of recursive calls indeed decrease with respect to the
233 @{subgoals[display,indent=0]}
235 These goals are all solved by @{text "auto"}:
242 Let us complicate the function a little, by adding some more
246 function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
249 then (if N = 0 then 0 else foo 0 (N - 1))
250 else i + foo (Suc i) N)"
251 by pat_completeness auto
254 When @{text "i"} has reached @{text "N"}, it starts at zero again
255 and @{text "N"} is decremented.
256 This corresponds to a nested
257 loop where one index counts up and the other down. Termination can
258 be proved using a lexicographic combination of two measures, namely
259 the value of @{text "N"} and the above difference. The @{const
260 "measures"} combinator generalizes @{text "measure"} by taking a
261 list of measure functions.
265 by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
267 subsection {* How @{text "lexicographic_order"} works *}
269 (*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
272 | "fails a (x#xs) = fails (x + a) (x # xs)"
276 To see how the automatic termination proofs work, let's look at an
277 example where it fails\footnote{For a detailed discussion of the
278 termination prover, see \cite{bulwahnKN07}}:
281 \cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
283 \hspace*{2ex}@{text "\"fails a [] = a\""}\\%
284 |\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\
285 \begin{isamarkuptext}
287 \noindent Isabelle responds with the following error:
290 *** Unfinished subgoals:\newline
291 *** (a, 1, <):\newline
292 *** \ 1.~@{text "\<And>x. x = 0"}\newline
293 *** (a, 1, <=):\newline
294 *** \ 1.~False\newline
295 *** (a, 2, <):\newline
296 *** \ 1.~False\newline
298 *** a) @{text "(a, x # xs) -->> (x + a, x # xs)"}\newline
299 *** Measures:\newline
300 *** 1) @{text "\<lambda>x. size (fst x)"}\newline
301 *** 2) @{text "\<lambda>x. size (snd x)"}\newline
302 *** Result matrix:\newline
303 *** \ \ \ \ 1\ \ 2 \newline
305 *** Could not find lexicographic termination order.\newline
306 *** At command "fun".\newline
314 The the key to this error message is the matrix at the bottom. The rows
315 of that matrix correspond to the different recursive calls (In our
316 case, there is just one). The columns are the function's arguments
317 (expressed through different measure functions, which map the
318 argument tuple to a natural number).
320 The contents of the matrix summarize what is known about argument
321 descents: The second argument has a weak descent (@{text "<="}) at the
322 recursive call, and for the first argument nothing could be proved,
323 which is expressed by @{text "?"}. In general, there are the values
324 @{text "<"}, @{text "<="} and @{text "?"}.
326 For the failed proof attempts, the unfinished subgoals are also
327 printed. Looking at these will often point to a missing lemma.
329 % As a more real example, here is quicksort:
332 function qs :: "nat list \<Rightarrow> nat list"
335 | "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
336 by pat_completeness auto
338 termination apply lexicographic_order
340 text {* If we try @{text "lexicographic_order"} method, we get the
342 termination by (lexicographic_order simp:l2)
344 lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
350 section {* Mutual Recursion *}
353 If two or more functions call one another mutually, they have to be defined
354 in one step. Here are @{text "even"} and @{text "odd"}:
357 function even :: "nat \<Rightarrow> bool"
358 and odd :: "nat \<Rightarrow> bool"
362 | "even (Suc n) = odd n"
363 | "odd (Suc n) = even n"
364 by pat_completeness auto
367 To eliminate the mutual dependencies, Isabelle internally
368 creates a single function operating on the sum
369 type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are
370 defined as projections. Consequently, termination has to be proved
371 simultaneously for both functions, by specifying a measure on the
376 by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") auto
379 We could also have used @{text lexicographic_order}, which
380 supports mutual recursive termination proofs to a certain extent.
383 subsection {* Induction for mutual recursion *}
387 When functions are mutually recursive, proving properties about them
388 generally requires simultaneous induction. The induction rule @{text "even_odd.induct"}
389 generated from the above definition reflects this.
391 Let us prove something about @{const even} and @{const odd}:
395 "even n = (n mod 2 = 0)"
396 "odd n = (n mod 2 = 1)"
399 We apply simultaneous induction, specifying the induction variable
400 for both goals, separated by \cmd{and}: *}
402 apply (induct n and n rule: even_odd.induct)
405 We get four subgoals, which correspond to the clauses in the
406 definition of @{const even} and @{const odd}:
407 @{subgoals[display,indent=0]}
408 Simplification solves the first two goals, leaving us with two
409 statements about the @{text "mod"} operation to prove:
415 @{subgoals[display,indent=0]}
417 \noindent These can be handled by Isabelle's arithmetic decision procedures.
426 In proofs like this, the simultaneous induction is really essential:
427 Even if we are just interested in one of the results, the other
428 one is necessary to strengthen the induction hypothesis. If we leave
429 out the statement about @{const odd} (by substituting it with @{term
430 "True"}), the same proof fails:
433 lemma failed_attempt:
434 "even n = (n mod 2 = 0)"
436 apply (induct n rule: even_odd.induct)
439 \noindent Now the third subgoal is a dead end, since we have no
440 useful induction hypothesis available:
442 @{subgoals[display,indent=0]}
447 section {* General pattern matching *}
448 text{*\label{genpats} *}
450 subsection {* Avoiding automatic pattern splitting *}
454 Up to now, we used pattern matching only on datatypes, and the
455 patterns were always disjoint and complete, and if they weren't,
456 they were made disjoint automatically like in the definition of
457 @{const "sep"} in \S\ref{patmatch}.
459 This automatic splitting can significantly increase the number of
460 equations involved, and this is not always desirable. The following
461 example shows the problem:
463 Suppose we are modeling incomplete knowledge about the world by a
464 three-valued datatype, which has values @{term "T"}, @{term "F"}
465 and @{term "X"} for true, false and uncertain propositions, respectively.
468 datatype P3 = T | F | X
470 text {* \noindent Then the conjunction of such values can be defined as follows: *}
472 fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
482 This definition is useful, because the equations can directly be used
483 as simplification rules rules. But the patterns overlap: For example,
484 the expression @{term "And T T"} is matched by both the first and
485 the second equation. By default, Isabelle makes the patterns disjoint by
486 splitting them up, producing instances:
492 @{thm[indent=4] And.simps}
495 \noindent There are several problems with this:
498 \item If the datatype has many constructors, there can be an
499 explosion of equations. For @{const "And"}, we get seven instead of
500 five equations, which can be tolerated, but this is just a small
503 \item Since splitting makes the equations \qt{less general}, they
504 do not always match in rewriting. While the term @{term "And x F"}
505 can be simplified to @{term "F"} with the original equations, a
506 (manual) case split on @{term "x"} is now necessary.
508 \item The splitting also concerns the induction rule @{text
509 "And.induct"}. Instead of five premises it now has seven, which
510 means that our induction proofs will have more cases.
512 \item In general, it increases clarity if we get the same definition
513 back which we put in.
516 If we do not want the automatic splitting, we can switch it off by
517 leaving out the \cmd{sequential} option. However, we will have to
518 prove that our pattern matching is consistent\footnote{This prevents
519 us from defining something like @{term "f x = True"} and @{term "f x
520 = False"} simultaneously.}:
523 function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
532 \noindent Now let's look at the proof obligations generated by a
533 function definition. In this case, they are:
535 @{subgoals[display,indent=0]}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}
537 The first subgoal expresses the completeness of the patterns. It has
538 the form of an elimination rule and states that every @{term x} of
539 the function's input type must match at least one of the patterns\footnote{Completeness could
540 be equivalently stated as a disjunction of existential statements:
541 @{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
542 (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}.}. If the patterns just involve
543 datatypes, we can solve it with the @{text "pat_completeness"}
547 apply pat_completeness
550 The remaining subgoals express \emph{pattern compatibility}. We do
551 allow that an input value matches multiple patterns, but in this
552 case, the result (i.e.~the right hand sides of the equations) must
553 also be equal. For each pair of two patterns, there is one such
554 subgoal. Usually this needs injectivity of the constructors, which
555 is used automatically by @{text "auto"}.
561 subsection {* Non-constructor patterns *}
564 Most of Isabelle's basic types take the form of inductive datatypes,
565 and usually pattern matching works on the constructors of such types.
566 However, this need not be always the case, and the \cmd{function}
567 command handles other kind of patterns, too.
569 One well-known instance of non-constructor patterns are
570 so-called \emph{$n+k$-patterns}, which are a little controversial in
571 the functional programming world. Here is the initial fibonacci
572 example with $n+k$-patterns:
575 function fib2 :: "nat \<Rightarrow> nat"
579 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
581 (*<*)ML "goals_limit := 1"(*>*)
583 This kind of matching is again justified by the proof of pattern
584 completeness and compatibility.
585 The proof obligation for pattern completeness states that every natural number is
586 either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
589 @{subgoals[display,indent=0]}
591 This is an arithmetic triviality, but unfortunately the
592 @{text arith} method cannot handle this specific form of an
593 elimination rule. However, we can use the method @{text
594 "elim_to_cases"} to do an ad-hoc conversion to a disjunction of
595 existentials, which can then be soved by the arithmetic decision procedure.
596 Pattern compatibility and termination are automatic as usual.
598 (*<*)ML "goals_limit := 10"(*>*)
603 termination by lexicographic_order
606 We can stretch the notion of pattern matching even more. The
607 following function is not a sensible functional program, but a
608 perfectly valid mathematical definition:
611 function ev :: "nat \<Rightarrow> bool"
614 | "ev (2 * n + 1) = False"
617 termination by (relation "{}") simp
620 This general notion of pattern matching gives you the full freedom
621 of mathematical specifications. However, as always, freedom should
624 If we leave the area of constructor
625 patterns, we have effectively departed from the world of functional
626 programming. This means that it is no longer possible to use the
627 code generator, and expect it to generate ML code for our
628 definitions. Also, such a specification might not work very well together with
629 simplification. Your mileage may vary.
633 subsection {* Conditional equations *}
636 The function package also supports conditional equations, which are
637 similar to guards in a language like Haskell. Here is Euclid's
638 algorithm written with conditional patterns\footnote{Note that the
639 patterns are also overlapping in the base case}:
642 function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
646 | "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
647 | "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
648 by (elim_to_cases, auto, arith)
649 termination by lexicographic_order
652 By now, you can probably guess what the proof obligations for the
653 pattern completeness and compatibility look like.
655 Again, functions with conditional patterns are not supported by the
660 subsection {* Pattern matching on strings *}
663 As strings (as lists of characters) are normal datatypes, pattern
664 matching on them is possible, but somewhat problematic. Consider the
665 following definition:
668 \noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\%
670 \hspace*{2ex}@{text "\"check (''good'') = True\""}\\%
671 @{text "| \"check s = False\""}
672 \begin{isamarkuptext}
674 \noindent An invocation of the above \cmd{fun} command does not
675 terminate. What is the problem? Strings are lists of characters, and
676 characters are a datatype with a lot of constructors. Splitting the
677 catch-all pattern thus leads to an explosion of cases, which cannot
678 be handled by Isabelle.
680 There are two things we can do here. Either we write an explicit
681 @{text "if"} on the right hand side, or we can use conditional patterns:
684 function check :: "string \<Rightarrow> bool"
686 "check (''good'') = True"
687 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
691 section {* Partiality *}
694 In HOL, all functions are total. A function @{term "f"} applied to
695 @{term "x"} always has the value @{term "f x"}, and there is no notion
697 This is why we have to do termination
698 proofs when defining functions: The proof justifies that the
699 function can be defined by wellfounded recursion.
701 However, the \cmd{function} package does support partiality to a
702 certain extent. Let's look at the following function which looks
703 for a zero of a given function f.
706 function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
708 "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
709 by pat_completeness auto
710 (*<*)declare findzero.simps[simp del](*>*)
713 \noindent Clearly, any attempt of a termination proof must fail. And without
714 that, we do not get the usual rules @{text "findzero.simp"} and
715 @{text "findzero.induct"}. So what was the definition good for at all?
718 subsection {* Domain predicates *}
721 The trick is that Isabelle has not only defined the function @{const findzero}, but also
722 a predicate @{term "findzero_dom"} that characterizes the values where the function
723 terminates: the \emph{domain} of the function. If we treat a
724 partial function just as a total function with an additional domain
725 predicate, we can derive simplification and
726 induction rules as we do for total functions. They are guarded
727 by domain conditions and are called @{text psimps} and @{text
732 \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
733 \hfill(@{text "findzero.psimps"})
736 \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
737 \hfill(@{text "findzero.pinduct"})
742 are doing here is use some tricks to make a total function appear
743 as if it was partial. We can still write the term @{term "findzero
744 (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal
745 to some natural number, although we might not be able to find out
746 which one. The function is \emph{underdefined}.
748 But it is defined enough to prove something interesting about it. We
749 can prove that if @{term "findzero f n"}
750 terminates, it indeed returns a zero of @{term f}:
753 lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
755 txt {* \noindent We apply induction as usual, but using the partial induction
758 apply (induct f n rule: findzero.pinduct)
760 txt {* \noindent This gives the following subgoals:
762 @{subgoals[display,indent=0]}
764 \noindent The hypothesis in our lemma was used to satisfy the first premise in
765 the induction rule. However, we also get @{term
766 "findzero_dom (f, n)"} as a local assumption in the induction step. This
767 allows to unfold @{term "findzero f n"} using the @{text psimps}
768 rule, and the rest is trivial. Since the @{text psimps} rules carry the
769 @{text "[simp]"} attribute by default, we just need a single step:
775 Proofs about partial functions are often not harder than for total
776 functions. Fig.~\ref{findzero_isar} shows a slightly more
777 complicated proof written in Isar. It is verbose enough to show how
778 partiality comes into play: From the partial induction, we get an
779 additional domain condition hypothesis. Observe how this condition
780 is applied when calls to @{term findzero} are unfolded.
786 \begin{minipage}{0.8\textwidth}
788 \isastyle\isamarkuptrue
790 lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
791 proof (induct rule: findzero.pinduct)
792 fix f n assume dom: "findzero_dom (f, n)"
793 and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
794 and x_range: "x \<in> {n ..< findzero f n}"
795 have "f n \<noteq> 0"
798 with dom have "findzero f n = n" by simp
799 with x_range show False by auto
802 from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
803 thus "f x \<noteq> 0"
806 with `f n \<noteq> 0` show ?thesis by simp
808 assume "x \<in> {Suc n ..< findzero f n}"
809 with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
810 with IH and `f n \<noteq> 0`
815 \isamarkupfalse\isabellestyle{tt}
816 \end{minipage}\vspace{6pt}\hrule
817 \caption{A proof about a partial function}\label{findzero_isar}
821 subsection {* Partial termination proofs *}
824 Now that we have proved some interesting properties about our
825 function, we should turn to the domain predicate and see if it is
826 actually true for some values. Otherwise we would have just proved
827 lemmas with @{term False} as a premise.
829 Essentially, we need some introduction rules for @{text
830 findzero_dom}. The function package can prove such domain
831 introduction rules automatically. But since they are not used very
832 often (they are almost never needed if the function is total), this
833 functionality is disabled by default for efficiency reasons. So we have to go
834 back and ask for them explicitly by passing the @{text
835 "(domintros)"} option to the function package:
838 \noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
839 \cmd{where}\isanewline%
842 \noindent Now the package has proved an introduction rule for @{text findzero_dom}:
845 thm findzero.domintros
848 @{thm[display] findzero.domintros}
850 Domain introduction rules allow to show that a given value lies in the
851 domain of a function, if the arguments of all recursive calls
852 are in the domain as well. They allow to do a \qt{single step} in a
853 termination proof. Usually, you want to combine them with a suitable
856 Since our function increases its argument at recursive calls, we
857 need an induction principle which works \qt{backwards}. We will use
858 @{text inc_induct}, which allows to do induction from a fixed number
861 \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}
863 Figure \ref{findzero_term} gives a detailed Isar proof of the fact
864 that @{text findzero} terminates if there is a zero which is greater
865 or equal to @{term n}. First we derive two useful rules which will
866 solve the base case and the step case of the induction. The
867 induction is then straightforward, except for the unusual induction
875 \begin{minipage}{0.8\textwidth}
877 \isastyle\isamarkuptrue
879 lemma findzero_termination:
880 assumes "x \<ge> n" and "f x = 0"
881 shows "findzero_dom (f, n)"
883 have base: "findzero_dom (f, x)"
884 by (rule findzero.domintros) (simp add:`f x = 0`)
886 have step: "\<And>i. findzero_dom (f, Suc i)
887 \<Longrightarrow> findzero_dom (f, i)"
888 by (rule findzero.domintros) simp
890 from `x \<ge> n` show ?thesis
891 proof (induct rule:inc_induct)
892 show "findzero_dom (f, x)" by (rule base)
894 fix i assume "findzero_dom (f, Suc i)"
895 thus "findzero_dom (f, i)" by (rule step)
899 \isamarkupfalse\isabellestyle{tt}
900 \end{minipage}\vspace{6pt}\hrule
901 \caption{Termination proof for @{text findzero}}\label{findzero_term}
906 Again, the proof given in Fig.~\ref{findzero_term} has a lot of
907 detail in order to explain the principles. Using more automation, we
908 can also have a short proof:
911 lemma findzero_termination_short:
912 assumes zero: "x >= n"
913 assumes [simp]: "f x = 0"
914 shows "findzero_dom (f, n)"
916 by (induct rule:inc_induct) (auto intro: findzero.domintros)
919 \noindent It is simple to combine the partial correctness result with the
923 lemma findzero_total_correctness:
924 "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
925 by (blast intro: findzero_zero findzero_termination)
927 subsection {* Definition of the domain predicate *}
930 Sometimes it is useful to know what the definition of the domain
931 predicate looks like. Actually, @{text findzero_dom} is just an
934 @{abbrev[display] findzero_dom}
936 The domain predicate is the \emph{accessible part} of a relation @{const
937 findzero_rel}, which was also created internally by the function
938 package. @{const findzero_rel} is just a normal
939 inductive predicate, so we can inspect its definition by
940 looking at the introduction rules @{text findzero_rel.intros}.
941 In our case there is just a single rule:
943 @{thm[display] findzero_rel.intros}
945 The predicate @{const findzero_rel}
946 describes the \emph{recursion relation} of the function
947 definition. The recursion relation is a binary relation on
948 the arguments of the function that relates each argument to its
949 recursive calls. In general, there is one introduction rule for each
952 The predicate @{term "accp findzero_rel"} is the accessible part of
953 that relation. An argument belongs to the accessible part, if it can
954 be reached in a finite number of steps (cf.~its definition in @{text
955 "Accessible_Part.thy"}).
957 Since the domain predicate is just an abbreviation, you can use
958 lemmas for @{const accp} and @{const findzero_rel} directly. Some
959 lemmas which are occasionally useful are @{text accpI}, @{text
960 accp_downward}, and of course the introduction and elimination rules
961 for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
964 (*lemma findzero_nicer_domintros:
965 "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
966 "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
967 by (rule accpI, erule findzero_rel.cases, auto)+
970 subsection {* A Useful Special Case: Tail recursion *}
973 The domain predicate is our trick that allows us to model partiality
974 in a world of total functions. The downside of this is that we have
975 to carry it around all the time. The termination proof above allowed
976 us to replace the abstract @{term "findzero_dom (f, n)"} by the more
977 concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still
978 there and can only be discharged for special cases.
979 In particular, the domain predicate guards the unfolding of our
980 function, since it is there as a condition in the @{text psimp}
983 Now there is an important special case: We can actually get rid
984 of the condition in the simplification rules, \emph{if the function
985 is tail-recursive}. The reason is that for all tail-recursive
986 equations there is a total function satisfying them, even if they
989 % A function is tail recursive, if each call to the function is either
992 % So the outer form of the
994 %if it can be written in the following
996 % {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
999 The function package internally does the right construction and can
1000 derive the unconditional simp rules, if we ask it to do so. Luckily,
1001 our @{const "findzero"} function is tail-recursive, so we can just go
1002 back and add another option to the \cmd{function} command:
1005 \noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
1006 \cmd{where}\isanewline%
1010 \noindent Now, we actually get unconditional simplification rules, even
1011 though the function is partial:
1017 @{thm[display] findzero.simps}
1019 \noindent Of course these would make the simplifier loop, so we better remove
1020 them from the simpset:
1023 declare findzero.simps[simp del]
1026 Getting rid of the domain conditions in the simplification rules is
1027 not only useful because it simplifies proofs. It is also required in
1028 order to use Isabelle's code generator to generate ML code
1029 from a function definition.
1030 Since the code generator only works with equations, it cannot be
1031 used with @{text "psimp"} rules. Thus, in order to generate code for
1032 partial functions, they must be defined as a tail recursion.
1033 Luckily, many functions have a relatively natural tail recursive
1037 section {* Nested recursion *}
1040 Recursive calls which are nested in one another frequently cause
1041 complications, since their termination proof can depend on a partial
1042 correctness property of the function itself.
1044 As a small example, we define the \qt{nested zero} function:
1047 function nz :: "nat \<Rightarrow> nat"
1050 | "nz (Suc n) = nz (nz n)"
1051 by pat_completeness auto
1054 If we attempt to prove termination using the identity measure on
1055 naturals, this fails:
1059 apply (relation "measure (\<lambda>n. n)")
1063 We get stuck with the subgoal
1065 @{subgoals[display]}
1067 Of course this statement is true, since we know that @{const nz} is
1068 the zero function. And in fact we have no problem proving this
1069 property by induction.
1072 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
1073 by (induct rule:nz.pinduct) auto
1076 We formulate this as a partial correctness lemma with the condition
1077 @{term "nz_dom n"}. This allows us to prove it with the @{text
1078 pinduct} rule before we have proved termination. With this lemma,
1079 the termination proof works as expected:
1083 by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
1086 As a general strategy, one should prove the statements needed for
1087 termination as a partial property first. Then they can be used to do
1088 the termination proof. This also works for less trivial
1089 examples. Figure \ref{f91} defines the 91-function, a well-known
1090 challenge problem due to John McCarthy, and proves its termination.
1096 \begin{minipage}{0.8\textwidth}
1098 \isastyle\isamarkuptrue
1101 function f91 :: "nat \<Rightarrow> nat"
1103 "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
1104 by pat_completeness auto
1107 assumes trm: "f91_dom n"
1108 shows "n < f91 n + 11"
1109 using trm by induct auto
1113 let ?R = "measure (\<lambda>x. 101 - x)"
1116 fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
1118 thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
1120 assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
1121 with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
1122 with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp
1126 \isamarkupfalse\isabellestyle{tt}
1129 \caption{McCarthy's 91-function}\label{f91}
1134 section {* Higher-Order Recursion *}
1137 Higher-order recursion occurs when recursive calls
1138 are passed as arguments to higher-order combinators such as @{term
1139 map}, @{term filter} etc.
1140 As an example, imagine a datatype of n-ary trees:
1145 | Branch "'a tree list"
1148 text {* \noindent We can define a map function for trees, using the predefined
1149 map function for lists. *}
1151 function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
1153 "treemap f (Leaf n) = Leaf (f n)"
1154 | "treemap f (Branch l) = Branch (map (treemap f) l)"
1155 by pat_completeness auto
1158 We do the termination proof manually, to point out what happens
1165 As usual, we have to give a wellfounded relation, such that the
1166 arguments of the recursive calls get smaller. But what exactly are
1167 the arguments of the recursive calls? Isabelle gives us the
1170 @{subgoals[display,indent=0]}
1172 So Isabelle seems to know that @{const map} behaves nicely and only
1173 applies the recursive call @{term "treemap f"} to elements
1174 of @{term "l"}. Before we discuss where this knowledge comes from,
1175 let us finish the termination proof:
1178 show "wf (measure (size o snd))" by simp
1180 fix f l and x :: "'a tree"
1181 assume "x \<in> set l"
1182 thus "((f, x), (f, Branch l)) \<in> measure (size o snd)"
1185 Simplification returns the following subgoal:
1187 @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"}
1189 We are lacking a property about the function @{const
1190 tree_list_size}, which was generated automatically at the
1191 definition of the @{text tree} type. We should go back and prove
1196 lemma tree_list_size[simp]: "x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
1200 Now the whole termination proof is automatic:
1204 by lexicographic_order
1207 subsection {* Congruence Rules *}
1210 Let's come back to the question how Isabelle knows about @{const
1213 The knowledge about map is encoded in so-called congruence rules,
1214 which are special theorems known to the \cmd{function} command. The
1217 @{thm[display] map_cong}
1219 You can read this in the following way: Two applications of @{const
1220 map} are equal, if the list arguments are equal and the functions
1221 coincide on the elements of the list. This means that for the value
1222 @{term "map f l"} we only have to know how @{term f} behaves on
1225 Usually, one such congruence rule is
1226 needed for each higher-order construct that is used when defining
1227 new functions. In fact, even basic functions like @{const
1228 If} and @{const Let} are handled by this mechanism. The congruence
1229 rule for @{const If} states that the @{text then} branch is only
1230 relevant if the condition is true, and the @{text else} branch only if it
1233 @{thm[display] if_cong}
1235 Congruence rules can be added to the
1236 function package by giving them the @{term fundef_cong} attribute.
1238 The constructs that are predefined in Isabelle, usually
1239 come with the respective congruence rules.
1240 But if you define your own higher-order functions, you will have to
1241 come up with the congruence rules yourself, if you want to use your
1242 functions in recursive definitions.
1245 subsection {* Congruence Rules and Evaluation Order *}
1248 Higher order logic differs from functional programming languages in
1249 that it has no built-in notion of evaluation order. A program is
1250 just a set of equations, and it is not specified how they must be
1253 However for the purpose of function definition, we must talk about
1254 evaluation order implicitly, when we reason about termination.
1255 Congruence rules express that a certain evaluation order is
1256 consistent with the logical definition.
1258 Consider the following function.
1261 function f :: "nat \<Rightarrow> bool"
1263 "f n = (n = 0 \<or> f (n - 1))"
1264 (*<*)by pat_completeness auto(*>*)
1267 As given above, the definition fails. The default configuration
1268 specifies no congruence rule for disjunction. We have to add a
1269 congruence rule that specifies left-to-right evaluation order:
1272 \noindent @{thm disj_cong}\hfill(@{text "disj_cong"})
1275 Now the definition works without problems. Note how the termination
1276 proof depends on the extra condition that we get from the congruence
1279 However, as evaluation is not a hard-wired concept, we
1280 could just turn everything around by declaring a different
1281 congruence rule. Then we can make the reverse definition:
1284 lemma disj_cong2[fundef_cong]:
1285 "(\<not> Q' \<Longrightarrow> P = P') \<Longrightarrow> (Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
1288 fun f' :: "nat \<Rightarrow> bool"
1290 "f' n = (f' (n - 1) \<or> n = 0)"
1293 \noindent These examples show that, in general, there is no \qt{best} set of
1296 However, such tweaking should rarely be necessary in
1297 practice, as most of the time, the default set of congruence rules
1303 Since the structure of
1304 congruence rules is a little unintuitive, here are some exercises:
1307 fun mapeven :: "(nat \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat list"
1310 | "mapeven f (x#xs) = (if x mod 2 = 0 then f x # mapeven f xs else x #
1317 Find a suitable congruence rule for the following function which
1318 maps only over the even numbers in a list:
1320 @{thm[display] mapeven.simps}
1324 Try what happens if the congruence rule for @{const If} is
1325 disabled by declaring @{text "if_cong[fundef_cong del]"}?
1328 Note that in some cases there is no \qt{best} congruence rule.