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,
27 and a set of defining recursive equations.
28 If we leave out the type, the most general type will be
29 inferred, which can sometimes lead to surprises: Since both @{term
30 "1::nat"} and @{text "+"} are overloaded, we would end up
31 with @{text "fib :: nat \<Rightarrow> 'a::{one,plus}"}.
35 The function always terminates, since its argument gets smaller in
37 Since HOL is a logic of total functions, termination is a
38 fundamental requirement to prevent inconsistencies\footnote{From the
39 \qt{definition} @{text "f(n) = f(n) + 1"} we could prove
40 @{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}.
41 Isabelle tries to prove termination automatically when a definition
42 is made. In \S\ref{termination}, we will look at cases where this
43 fails and see what to do then.
46 subsection {* Pattern matching *}
48 text {* \label{patmatch}
49 Like in functional programming, we can use pattern matching to
50 define functions. At the moment we will only consider \emph{constructor
51 patterns}, which only consist of datatype constructors and
52 variables. Furthermore, patterns must be linear, i.e.\ all variables
53 on the left hand side of an equation must be distinct. In
54 \S\ref{genpats} we discuss more general pattern matching.
56 If patterns overlap, the order of the equations is taken into
57 account. The following function inserts a fixed element between any
58 two elements of a list:
61 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
63 "sep a (x#y#xs) = x # a # sep a (y # xs)"
67 Overlapping patterns are interpreted as \qt{increments} to what is
68 already there: The second equation is only meant for the cases where
69 the first one does not match. Consequently, Isabelle replaces it
70 internally by the remaining cases, making the patterns disjoint:
75 text {* @{thm [display] sep.simps[no_vars]} *}
78 \noindent The equations from function definitions are automatically used in
82 lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"
85 subsection {* Induction *}
89 Isabelle provides customized induction rules for recursive
90 functions. These rules follow the recursive structure of the
91 definition. Here is the rule @{text sep.induct} arising from the
92 above definition of @{const sep}:
94 @{thm [display] sep.induct}
96 We have a step case for list with at least two elements, and two
97 base cases for the zero- and the one-element list. Here is a simple
98 proof about @{const sep} and @{const map}
101 lemma "map f (sep x ys) = sep (f x) (map f ys)"
102 apply (induct x ys rule: sep.induct)
105 We get three cases, like in the definition.
107 @{subgoals [display]}
114 With the \cmd{fun} command, you can define about 80\% of the
115 functions that occur in practice. The rest of this tutorial explains
120 section {* fun vs.\ function *}
123 The \cmd{fun} command provides a
124 convenient shorthand notation for simple function definitions. In
125 this mode, Isabelle tries to solve all the necessary proof obligations
126 automatically. If a proof fails, the definition is
127 rejected. This can either mean that the definition is indeed faulty,
128 or that the default proof procedures are just not smart enough (or
129 rather: not designed) to handle the definition.
131 By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or
132 solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:
137 \[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}
138 \cmd{fun} @{text "f :: \<tau>"}\\%
140 \hspace*{2ex}{\it equations}\\%
141 \hspace*{2ex}\vdots\vspace*{6pt}
142 \end{minipage}\right]
144 \left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
145 \cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
147 \hspace*{2ex}{\it equations}\\%
148 \hspace*{2ex}\vdots\\%
149 \cmd{by} @{text "pat_completeness auto"}\\%
150 \cmd{termination by} @{text "lexicographic_order"}\vspace{6pt}
154 \begin{isamarkuptext}
156 \noindent Some details have now become explicit:
159 \item The \cmd{sequential} option enables the preprocessing of
160 pattern overlaps which we already saw. Without this option, the equations
161 must already be disjoint and complete. The automatic completion only
162 works with constructor patterns.
164 \item A function definition produces a proof obligation which
165 expresses completeness and compatibility of patterns (we talk about
166 this later). The combination of the methods @{text "pat_completeness"} and
167 @{text "auto"} is used to solve this proof obligation.
169 \item A termination proof follows the definition, started by the
170 \cmd{termination} command. This will be explained in \S\ref{termination}.
172 Whenever a \cmd{fun} command fails, it is usually a good idea to
173 expand the syntax to the more verbose \cmd{function} form, to see
174 what is actually going on.
178 section {* Termination *}
180 text {*\label{termination}
181 The method @{text "lexicographic_order"} is the default method for
182 termination proofs. It can prove termination of a
183 certain class of functions by searching for a suitable lexicographic
184 combination of size measures. Of course, not all functions have such
185 a simple termination argument. For them, we can specify the termination
189 subsection {* The {\tt relation} method *}
191 Consider the following function, which sums up natural numbers up to
192 @{text "N"}, using a counter @{text "i"}:
195 function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
197 "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
198 by pat_completeness auto
201 \noindent The @{text "lexicographic_order"} method fails on this example, because none of the
202 arguments decreases in the recursive call, with respect to the standard size ordering.
203 To prove termination manually, we must provide a custom wellfounded relation.
205 The termination argument for @{text "sum"} is based on the fact that
206 the \emph{difference} between @{text "i"} and @{text "N"} gets
207 smaller in every step, and that the recursion stops when @{text "i"}
208 is greater than @{text "N"}. Phrased differently, the expression
209 @{text "N + 1 - i"} always decreases.
211 We can use this expression as a measure function suitable to prove termination.
215 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
218 The \cmd{termination} command sets up the termination goal for the
219 specified function @{text "sum"}. If the function name is omitted, it
220 implicitly refers to the last function definition.
222 The @{text relation} method takes a relation of
223 type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of
224 the function. If the function has multiple curried arguments, then
225 these are packed together into a tuple, as it happened in the above
228 The predefined function @{term_type "measure"} constructs a
229 wellfounded relation from a mapping into the natural numbers (a
230 \emph{measure function}).
232 After the invocation of @{text "relation"}, we must prove that (a)
233 the relation we supplied is wellfounded, and (b) that the arguments
234 of recursive calls indeed decrease with respect to the
237 @{subgoals[display,indent=0]}
239 These goals are all solved by @{text "auto"}:
246 Let us complicate the function a little, by adding some more
250 function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
253 then (if N = 0 then 0 else foo 0 (N - 1))
254 else i + foo (Suc i) N)"
255 by pat_completeness auto
258 When @{text "i"} has reached @{text "N"}, it starts at zero again
259 and @{text "N"} is decremented.
260 This corresponds to a nested
261 loop where one index counts up and the other down. Termination can
262 be proved using a lexicographic combination of two measures, namely
263 the value of @{text "N"} and the above difference. The @{const
264 "measures"} combinator generalizes @{text "measure"} by taking a
265 list of measure functions.
269 by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
271 subsection {* How @{text "lexicographic_order"} works *}
273 (*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
276 | "fails a (x#xs) = fails (x + a) (x # xs)"
280 To see how the automatic termination proofs work, let's look at an
281 example where it fails\footnote{For a detailed discussion of the
282 termination prover, see \cite{bulwahnKN07}}:
285 \cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
287 \hspace*{2ex}@{text "\"fails a [] = a\""}\\%
288 |\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\
289 \begin{isamarkuptext}
291 \noindent Isabelle responds with the following error:
294 *** Unfinished subgoals:\newline
295 *** (a, 1, <):\newline
296 *** \ 1.~@{text "\<And>x. x = 0"}\newline
297 *** (a, 1, <=):\newline
298 *** \ 1.~False\newline
299 *** (a, 2, <):\newline
300 *** \ 1.~False\newline
302 *** a) @{text "(a, x # xs) -->> (x + a, x # xs)"}\newline
303 *** Measures:\newline
304 *** 1) @{text "\<lambda>x. size (fst x)"}\newline
305 *** 2) @{text "\<lambda>x. size (snd x)"}\newline
306 *** Result matrix:\newline
307 *** \ \ \ \ 1\ \ 2 \newline
309 *** Could not find lexicographic termination order.\newline
310 *** At command "fun".\newline
318 The the key to this error message is the matrix at the bottom. The rows
319 of that matrix correspond to the different recursive calls (In our
320 case, there is just one). The columns are the function's arguments
321 (expressed through different measure functions, which map the
322 argument tuple to a natural number).
324 The contents of the matrix summarize what is known about argument
325 descents: The second argument has a weak descent (@{text "<="}) at the
326 recursive call, and for the first argument nothing could be proved,
327 which is expressed by @{text "?"}. In general, there are the values
328 @{text "<"}, @{text "<="} and @{text "?"}.
330 For the failed proof attempts, the unfinished subgoals are also
331 printed. Looking at these will often point to a missing lemma.
333 % As a more real example, here is quicksort:
336 function qs :: "nat list \<Rightarrow> nat list"
339 | "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
340 by pat_completeness auto
342 termination apply lexicographic_order
344 text {* If we try @{text "lexicographic_order"} method, we get the
346 termination by (lexicographic_order simp:l2)
348 lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
354 section {* Mutual Recursion *}
357 If two or more functions call one another mutually, they have to be defined
358 in one step. Here are @{text "even"} and @{text "odd"}:
361 function even :: "nat \<Rightarrow> bool"
362 and odd :: "nat \<Rightarrow> bool"
366 | "even (Suc n) = odd n"
367 | "odd (Suc n) = even n"
368 by pat_completeness auto
371 To eliminate the mutual dependencies, Isabelle internally
372 creates a single function operating on the sum
373 type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are
374 defined as projections. Consequently, termination has to be proved
375 simultaneously for both functions, by specifying a measure on the
380 by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") auto
383 We could also have used @{text lexicographic_order}, which
384 supports mutual recursive termination proofs to a certain extent.
387 subsection {* Induction for mutual recursion *}
391 When functions are mutually recursive, proving properties about them
392 generally requires simultaneous induction. The induction rule @{text "even_odd.induct"}
393 generated from the above definition reflects this.
395 Let us prove something about @{const even} and @{const odd}:
399 "even n = (n mod 2 = 0)"
400 "odd n = (n mod 2 = 1)"
403 We apply simultaneous induction, specifying the induction variable
404 for both goals, separated by \cmd{and}: *}
406 apply (induct n and n rule: even_odd.induct)
409 We get four subgoals, which correspond to the clauses in the
410 definition of @{const even} and @{const odd}:
411 @{subgoals[display,indent=0]}
412 Simplification solves the first two goals, leaving us with two
413 statements about the @{text "mod"} operation to prove:
419 @{subgoals[display,indent=0]}
421 \noindent These can be handled by Isabelle's arithmetic decision procedures.
430 In proofs like this, the simultaneous induction is really essential:
431 Even if we are just interested in one of the results, the other
432 one is necessary to strengthen the induction hypothesis. If we leave
433 out the statement about @{const odd} (by substituting it with @{term
434 "True"}), the same proof fails:
437 lemma failed_attempt:
438 "even n = (n mod 2 = 0)"
440 apply (induct n rule: even_odd.induct)
443 \noindent Now the third subgoal is a dead end, since we have no
444 useful induction hypothesis available:
446 @{subgoals[display,indent=0]}
451 section {* General pattern matching *}
452 text{*\label{genpats} *}
454 subsection {* Avoiding automatic pattern splitting *}
458 Up to now, we used pattern matching only on datatypes, and the
459 patterns were always disjoint and complete, and if they weren't,
460 they were made disjoint automatically like in the definition of
461 @{const "sep"} in \S\ref{patmatch}.
463 This automatic splitting can significantly increase the number of
464 equations involved, and this is not always desirable. The following
465 example shows the problem:
467 Suppose we are modeling incomplete knowledge about the world by a
468 three-valued datatype, which has values @{term "T"}, @{term "F"}
469 and @{term "X"} for true, false and uncertain propositions, respectively.
472 datatype P3 = T | F | X
474 text {* \noindent Then the conjunction of such values can be defined as follows: *}
476 fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
486 This definition is useful, because the equations can directly be used
487 as simplification rules rules. But the patterns overlap: For example,
488 the expression @{term "And T T"} is matched by both the first and
489 the second equation. By default, Isabelle makes the patterns disjoint by
490 splitting them up, producing instances:
496 @{thm[indent=4] And.simps}
499 \noindent There are several problems with this:
502 \item If the datatype has many constructors, there can be an
503 explosion of equations. For @{const "And"}, we get seven instead of
504 five equations, which can be tolerated, but this is just a small
507 \item Since splitting makes the equations \qt{less general}, they
508 do not always match in rewriting. While the term @{term "And x F"}
509 can be simplified to @{term "F"} with the original equations, a
510 (manual) case split on @{term "x"} is now necessary.
512 \item The splitting also concerns the induction rule @{text
513 "And.induct"}. Instead of five premises it now has seven, which
514 means that our induction proofs will have more cases.
516 \item In general, it increases clarity if we get the same definition
517 back which we put in.
520 If we do not want the automatic splitting, we can switch it off by
521 leaving out the \cmd{sequential} option. However, we will have to
522 prove that our pattern matching is consistent\footnote{This prevents
523 us from defining something like @{term "f x = True"} and @{term "f x
524 = False"} simultaneously.}:
527 function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
536 \noindent Now let's look at the proof obligations generated by a
537 function definition. In this case, they are:
539 @{subgoals[display,indent=0]}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}
541 The first subgoal expresses the completeness of the patterns. It has
542 the form of an elimination rule and states that every @{term x} of
543 the function's input type must match at least one of the patterns\footnote{Completeness could
544 be equivalently stated as a disjunction of existential statements:
545 @{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>
546 (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}.}. If the patterns just involve
547 datatypes, we can solve it with the @{text "pat_completeness"}
551 apply pat_completeness
554 The remaining subgoals express \emph{pattern compatibility}. We do
555 allow that an input value matches multiple patterns, but in this
556 case, the result (i.e.~the right hand sides of the equations) must
557 also be equal. For each pair of two patterns, there is one such
558 subgoal. Usually this needs injectivity of the constructors, which
559 is used automatically by @{text "auto"}.
565 subsection {* Non-constructor patterns *}
568 Most of Isabelle's basic types take the form of inductive datatypes,
569 and usually pattern matching works on the constructors of such types.
570 However, this need not be always the case, and the \cmd{function}
571 command handles other kind of patterns, too.
573 One well-known instance of non-constructor patterns are
574 so-called \emph{$n+k$-patterns}, which are a little controversial in
575 the functional programming world. Here is the initial fibonacci
576 example with $n+k$-patterns:
579 function fib2 :: "nat \<Rightarrow> nat"
583 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
585 (*<*)ML "goals_limit := 1"(*>*)
587 This kind of matching is again justified by the proof of pattern
588 completeness and compatibility.
589 The proof obligation for pattern completeness states that every natural number is
590 either @{term "0::nat"}, @{term "1::nat"} or @{term "n +
593 @{subgoals[display,indent=0]}
595 This is an arithmetic triviality, but unfortunately the
596 @{text arith} method cannot handle this specific form of an
597 elimination rule. However, we can use the method @{text
598 "atomize_elim"} to do an ad-hoc conversion to a disjunction of
599 existentials, which can then be soved by the arithmetic decision procedure.
600 Pattern compatibility and termination are automatic as usual.
602 (*<*)ML "goals_limit := 10"(*>*)
607 termination by lexicographic_order
610 We can stretch the notion of pattern matching even more. The
611 following function is not a sensible functional program, but a
612 perfectly valid mathematical definition:
615 function ev :: "nat \<Rightarrow> bool"
618 | "ev (2 * n + 1) = False"
621 termination by (relation "{}") simp
624 This general notion of pattern matching gives you the full freedom
625 of mathematical specifications. However, as always, freedom should
628 If we leave the area of constructor
629 patterns, we have effectively departed from the world of functional
630 programming. This means that it is no longer possible to use the
631 code generator, and expect it to generate ML code for our
632 definitions. Also, such a specification might not work very well together with
633 simplification. Your mileage may vary.
637 subsection {* Conditional equations *}
640 The function package also supports conditional equations, which are
641 similar to guards in a language like Haskell. Here is Euclid's
642 algorithm written with conditional patterns\footnote{Note that the
643 patterns are also overlapping in the base case}:
646 function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
650 | "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
651 | "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
652 by (atomize_elim, auto, arith)
653 termination by lexicographic_order
656 By now, you can probably guess what the proof obligations for the
657 pattern completeness and compatibility look like.
659 Again, functions with conditional patterns are not supported by the
664 subsection {* Pattern matching on strings *}
667 As strings (as lists of characters) are normal datatypes, pattern
668 matching on them is possible, but somewhat problematic. Consider the
669 following definition:
672 \noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\%
674 \hspace*{2ex}@{text "\"check (''good'') = True\""}\\%
675 @{text "| \"check s = False\""}
676 \begin{isamarkuptext}
678 \noindent An invocation of the above \cmd{fun} command does not
679 terminate. What is the problem? Strings are lists of characters, and
680 characters are a datatype with a lot of constructors. Splitting the
681 catch-all pattern thus leads to an explosion of cases, which cannot
682 be handled by Isabelle.
684 There are two things we can do here. Either we write an explicit
685 @{text "if"} on the right hand side, or we can use conditional patterns:
688 function check :: "string \<Rightarrow> bool"
690 "check (''good'') = True"
691 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
695 section {* Partiality *}
698 In HOL, all functions are total. A function @{term "f"} applied to
699 @{term "x"} always has the value @{term "f x"}, and there is no notion
701 This is why we have to do termination
702 proofs when defining functions: The proof justifies that the
703 function can be defined by wellfounded recursion.
705 However, the \cmd{function} package does support partiality to a
706 certain extent. Let's look at the following function which looks
707 for a zero of a given function f.
710 function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
712 "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
713 by pat_completeness auto
714 (*<*)declare findzero.simps[simp del](*>*)
717 \noindent Clearly, any attempt of a termination proof must fail. And without
718 that, we do not get the usual rules @{text "findzero.simp"} and
719 @{text "findzero.induct"}. So what was the definition good for at all?
722 subsection {* Domain predicates *}
725 The trick is that Isabelle has not only defined the function @{const findzero}, but also
726 a predicate @{term "findzero_dom"} that characterizes the values where the function
727 terminates: the \emph{domain} of the function. If we treat a
728 partial function just as a total function with an additional domain
729 predicate, we can derive simplification and
730 induction rules as we do for total functions. They are guarded
731 by domain conditions and are called @{text psimps} and @{text
736 \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
737 \hfill(@{text "findzero.psimps"})
740 \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
741 \hfill(@{text "findzero.pinduct"})
746 are doing here is use some tricks to make a total function appear
747 as if it was partial. We can still write the term @{term "findzero
748 (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal
749 to some natural number, although we might not be able to find out
750 which one. The function is \emph{underdefined}.
752 But it is defined enough to prove something interesting about it. We
753 can prove that if @{term "findzero f n"}
754 terminates, it indeed returns a zero of @{term f}:
757 lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
759 txt {* \noindent We apply induction as usual, but using the partial induction
762 apply (induct f n rule: findzero.pinduct)
764 txt {* \noindent This gives the following subgoals:
766 @{subgoals[display,indent=0]}
768 \noindent The hypothesis in our lemma was used to satisfy the first premise in
769 the induction rule. However, we also get @{term
770 "findzero_dom (f, n)"} as a local assumption in the induction step. This
771 allows to unfold @{term "findzero f n"} using the @{text psimps}
772 rule, and the rest is trivial. Since the @{text psimps} rules carry the
773 @{text "[simp]"} attribute by default, we just need a single step:
779 Proofs about partial functions are often not harder than for total
780 functions. Fig.~\ref{findzero_isar} shows a slightly more
781 complicated proof written in Isar. It is verbose enough to show how
782 partiality comes into play: From the partial induction, we get an
783 additional domain condition hypothesis. Observe how this condition
784 is applied when calls to @{term findzero} are unfolded.
790 \begin{minipage}{0.8\textwidth}
792 \isastyle\isamarkuptrue
794 lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
795 proof (induct rule: findzero.pinduct)
796 fix f n assume dom: "findzero_dom (f, n)"
797 and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0"
798 and x_range: "x \<in> {n ..< findzero f n}"
799 have "f n \<noteq> 0"
802 with dom have "findzero f n = n" by simp
803 with x_range show False by auto
806 from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
807 thus "f x \<noteq> 0"
810 with `f n \<noteq> 0` show ?thesis by simp
812 assume "x \<in> {Suc n ..< findzero f n}"
813 with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
814 with IH and `f n \<noteq> 0`
819 \isamarkupfalse\isabellestyle{tt}
820 \end{minipage}\vspace{6pt}\hrule
821 \caption{A proof about a partial function}\label{findzero_isar}
825 subsection {* Partial termination proofs *}
828 Now that we have proved some interesting properties about our
829 function, we should turn to the domain predicate and see if it is
830 actually true for some values. Otherwise we would have just proved
831 lemmas with @{term False} as a premise.
833 Essentially, we need some introduction rules for @{text
834 findzero_dom}. The function package can prove such domain
835 introduction rules automatically. But since they are not used very
836 often (they are almost never needed if the function is total), this
837 functionality is disabled by default for efficiency reasons. So we have to go
838 back and ask for them explicitly by passing the @{text
839 "(domintros)"} option to the function package:
842 \noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
843 \cmd{where}\isanewline%
846 \noindent Now the package has proved an introduction rule for @{text findzero_dom}:
849 thm findzero.domintros
852 @{thm[display] findzero.domintros}
854 Domain introduction rules allow to show that a given value lies in the
855 domain of a function, if the arguments of all recursive calls
856 are in the domain as well. They allow to do a \qt{single step} in a
857 termination proof. Usually, you want to combine them with a suitable
860 Since our function increases its argument at recursive calls, we
861 need an induction principle which works \qt{backwards}. We will use
862 @{text inc_induct}, which allows to do induction from a fixed number
865 \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}
867 Figure \ref{findzero_term} gives a detailed Isar proof of the fact
868 that @{text findzero} terminates if there is a zero which is greater
869 or equal to @{term n}. First we derive two useful rules which will
870 solve the base case and the step case of the induction. The
871 induction is then straightforward, except for the unusual induction
879 \begin{minipage}{0.8\textwidth}
881 \isastyle\isamarkuptrue
883 lemma findzero_termination:
884 assumes "x \<ge> n" and "f x = 0"
885 shows "findzero_dom (f, n)"
887 have base: "findzero_dom (f, x)"
888 by (rule findzero.domintros) (simp add:`f x = 0`)
890 have step: "\<And>i. findzero_dom (f, Suc i)
891 \<Longrightarrow> findzero_dom (f, i)"
892 by (rule findzero.domintros) simp
894 from `x \<ge> n` show ?thesis
895 proof (induct rule:inc_induct)
896 show "findzero_dom (f, x)" by (rule base)
898 fix i assume "findzero_dom (f, Suc i)"
899 thus "findzero_dom (f, i)" by (rule step)
903 \isamarkupfalse\isabellestyle{tt}
904 \end{minipage}\vspace{6pt}\hrule
905 \caption{Termination proof for @{text findzero}}\label{findzero_term}
910 Again, the proof given in Fig.~\ref{findzero_term} has a lot of
911 detail in order to explain the principles. Using more automation, we
912 can also have a short proof:
915 lemma findzero_termination_short:
916 assumes zero: "x >= n"
917 assumes [simp]: "f x = 0"
918 shows "findzero_dom (f, n)"
920 by (induct rule:inc_induct) (auto intro: findzero.domintros)
923 \noindent It is simple to combine the partial correctness result with the
927 lemma findzero_total_correctness:
928 "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
929 by (blast intro: findzero_zero findzero_termination)
931 subsection {* Definition of the domain predicate *}
934 Sometimes it is useful to know what the definition of the domain
935 predicate looks like. Actually, @{text findzero_dom} is just an
938 @{abbrev[display] findzero_dom}
940 The domain predicate is the \emph{accessible part} of a relation @{const
941 findzero_rel}, which was also created internally by the function
942 package. @{const findzero_rel} is just a normal
943 inductive predicate, so we can inspect its definition by
944 looking at the introduction rules @{text findzero_rel.intros}.
945 In our case there is just a single rule:
947 @{thm[display] findzero_rel.intros}
949 The predicate @{const findzero_rel}
950 describes the \emph{recursion relation} of the function
951 definition. The recursion relation is a binary relation on
952 the arguments of the function that relates each argument to its
953 recursive calls. In general, there is one introduction rule for each
956 The predicate @{term "accp findzero_rel"} is the accessible part of
957 that relation. An argument belongs to the accessible part, if it can
958 be reached in a finite number of steps (cf.~its definition in @{text
959 "Accessible_Part.thy"}).
961 Since the domain predicate is just an abbreviation, you can use
962 lemmas for @{const accp} and @{const findzero_rel} directly. Some
963 lemmas which are occasionally useful are @{text accpI}, @{text
964 accp_downward}, and of course the introduction and elimination rules
965 for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.
968 (*lemma findzero_nicer_domintros:
969 "f x = 0 \<Longrightarrow> findzero_dom (f, x)"
970 "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"
971 by (rule accpI, erule findzero_rel.cases, auto)+
974 subsection {* A Useful Special Case: Tail recursion *}
977 The domain predicate is our trick that allows us to model partiality
978 in a world of total functions. The downside of this is that we have
979 to carry it around all the time. The termination proof above allowed
980 us to replace the abstract @{term "findzero_dom (f, n)"} by the more
981 concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still
982 there and can only be discharged for special cases.
983 In particular, the domain predicate guards the unfolding of our
984 function, since it is there as a condition in the @{text psimp}
987 Now there is an important special case: We can actually get rid
988 of the condition in the simplification rules, \emph{if the function
989 is tail-recursive}. The reason is that for all tail-recursive
990 equations there is a total function satisfying them, even if they
993 % A function is tail recursive, if each call to the function is either
996 % So the outer form of the
998 %if it can be written in the following
1000 % {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
1003 The function package internally does the right construction and can
1004 derive the unconditional simp rules, if we ask it to do so. Luckily,
1005 our @{const "findzero"} function is tail-recursive, so we can just go
1006 back and add another option to the \cmd{function} command:
1009 \noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
1010 \cmd{where}\isanewline%
1014 \noindent Now, we actually get unconditional simplification rules, even
1015 though the function is partial:
1021 @{thm[display] findzero.simps}
1023 \noindent Of course these would make the simplifier loop, so we better remove
1024 them from the simpset:
1027 declare findzero.simps[simp del]
1030 Getting rid of the domain conditions in the simplification rules is
1031 not only useful because it simplifies proofs. It is also required in
1032 order to use Isabelle's code generator to generate ML code
1033 from a function definition.
1034 Since the code generator only works with equations, it cannot be
1035 used with @{text "psimp"} rules. Thus, in order to generate code for
1036 partial functions, they must be defined as a tail recursion.
1037 Luckily, many functions have a relatively natural tail recursive
1041 section {* Nested recursion *}
1044 Recursive calls which are nested in one another frequently cause
1045 complications, since their termination proof can depend on a partial
1046 correctness property of the function itself.
1048 As a small example, we define the \qt{nested zero} function:
1051 function nz :: "nat \<Rightarrow> nat"
1054 | "nz (Suc n) = nz (nz n)"
1055 by pat_completeness auto
1058 If we attempt to prove termination using the identity measure on
1059 naturals, this fails:
1063 apply (relation "measure (\<lambda>n. n)")
1067 We get stuck with the subgoal
1069 @{subgoals[display]}
1071 Of course this statement is true, since we know that @{const nz} is
1072 the zero function. And in fact we have no problem proving this
1073 property by induction.
1076 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
1077 by (induct rule:nz.pinduct) auto
1080 We formulate this as a partial correctness lemma with the condition
1081 @{term "nz_dom n"}. This allows us to prove it with the @{text
1082 pinduct} rule before we have proved termination. With this lemma,
1083 the termination proof works as expected:
1087 by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
1090 As a general strategy, one should prove the statements needed for
1091 termination as a partial property first. Then they can be used to do
1092 the termination proof. This also works for less trivial
1093 examples. Figure \ref{f91} defines the 91-function, a well-known
1094 challenge problem due to John McCarthy, and proves its termination.
1100 \begin{minipage}{0.8\textwidth}
1102 \isastyle\isamarkuptrue
1105 function f91 :: "nat \<Rightarrow> nat"
1107 "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
1108 by pat_completeness auto
1111 assumes trm: "f91_dom n"
1112 shows "n < f91 n + 11"
1113 using trm by induct auto
1117 let ?R = "measure (\<lambda>x. 101 - x)"
1120 fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
1122 thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
1124 assume inner_trm: "f91_dom (n + 11)" -- "Outer call"
1125 with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
1126 with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp
1130 \isamarkupfalse\isabellestyle{tt}
1133 \caption{McCarthy's 91-function}\label{f91}
1138 section {* Higher-Order Recursion *}
1141 Higher-order recursion occurs when recursive calls
1142 are passed as arguments to higher-order combinators such as @{term
1143 map}, @{term filter} etc.
1144 As an example, imagine a datatype of n-ary trees:
1149 | Branch "'a tree list"
1152 text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the
1153 list functions @{const rev} and @{const map}: *}
1155 lemma [simp]: "x \<in> set l \<Longrightarrow> f x < Suc (list_size f l)"
1159 fun mirror :: "'a tree \<Rightarrow> 'a tree"
1161 "mirror (Leaf n) = Leaf n"
1162 | "mirror (Branch l) = Branch (rev (map mirror l))"
1166 \emph{Note: The handling of size functions is currently changing
1167 in the developers version of Isabelle. So this documentation is outdated.}
1173 As usual, we have to give a wellfounded relation, such that the
1174 arguments of the recursive calls get smaller. But what exactly are
1175 the arguments of the recursive calls? Isabelle gives us the
1178 @{subgoals[display,indent=0]}
1180 So Isabelle seems to know that @{const map} behaves nicely and only
1181 applies the recursive call @{term "mirror"} to elements
1182 of @{term "l"}. Before we discuss where this knowledge comes from,
1183 let us finish the termination proof:
1186 show "wf (measure size)" by simp
1188 fix f l and x :: "'a tree"
1189 assume "x \<in> set l"
1190 thus "(x, Branch l) \<in> measure size"
1193 Simplification returns the following subgoal:
1195 @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"}
1197 We are lacking a property about the function @{term
1198 tree_list_size}, which was generated automatically at the
1199 definition of the @{text tree} type. We should go back and prove
1205 Now the whole termination proof is automatic:
1209 by lexicographic_order
1211 subsection {* Congruence Rules *}
1214 Let's come back to the question how Isabelle knows about @{const
1217 The knowledge about map is encoded in so-called congruence rules,
1218 which are special theorems known to the \cmd{function} command. The
1221 @{thm[display] map_cong}
1223 You can read this in the following way: Two applications of @{const
1224 map} are equal, if the list arguments are equal and the functions
1225 coincide on the elements of the list. This means that for the value
1226 @{term "map f l"} we only have to know how @{term f} behaves on
1229 Usually, one such congruence rule is
1230 needed for each higher-order construct that is used when defining
1231 new functions. In fact, even basic functions like @{const
1232 If} and @{const Let} are handled by this mechanism. The congruence
1233 rule for @{const If} states that the @{text then} branch is only
1234 relevant if the condition is true, and the @{text else} branch only if it
1237 @{thm[display] if_cong}
1239 Congruence rules can be added to the
1240 function package by giving them the @{term fundef_cong} attribute.
1242 The constructs that are predefined in Isabelle, usually
1243 come with the respective congruence rules.
1244 But if you define your own higher-order functions, you will have to
1245 come up with the congruence rules yourself, if you want to use your
1246 functions in recursive definitions.
1249 subsection {* Congruence Rules and Evaluation Order *}
1252 Higher order logic differs from functional programming languages in
1253 that it has no built-in notion of evaluation order. A program is
1254 just a set of equations, and it is not specified how they must be
1257 However for the purpose of function definition, we must talk about
1258 evaluation order implicitly, when we reason about termination.
1259 Congruence rules express that a certain evaluation order is
1260 consistent with the logical definition.
1262 Consider the following function.
1265 function f :: "nat \<Rightarrow> bool"
1267 "f n = (n = 0 \<or> f (n - 1))"
1268 (*<*)by pat_completeness auto(*>*)
1271 As given above, the definition fails. The default configuration
1272 specifies no congruence rule for disjunction. We have to add a
1273 congruence rule that specifies left-to-right evaluation order:
1276 \noindent @{thm disj_cong}\hfill(@{text "disj_cong"})
1279 Now the definition works without problems. Note how the termination
1280 proof depends on the extra condition that we get from the congruence
1283 However, as evaluation is not a hard-wired concept, we
1284 could just turn everything around by declaring a different
1285 congruence rule. Then we can make the reverse definition:
1288 lemma disj_cong2[fundef_cong]:
1289 "(\<not> Q' \<Longrightarrow> P = P') \<Longrightarrow> (Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
1292 fun f' :: "nat \<Rightarrow> bool"
1294 "f' n = (f' (n - 1) \<or> n = 0)"
1297 \noindent These examples show that, in general, there is no \qt{best} set of
1300 However, such tweaking should rarely be necessary in
1301 practice, as most of the time, the default set of congruence rules