doc-src/IsarAdvanced/Functions/Thy/Functions.thy
author krauss
Tue Apr 08 18:30:40 2008 +0200 (2008-04-08)
changeset 26580 c3e597a476fd
parent 25688 6c24a82a98f1
child 26749 397a1aeede7d
permissions -rw-r--r--
Generic conversion and tactic "atomize_elim" to convert elimination rules
to the object logic
     1 (*  Title:      Doc/IsarAdvanced/Functions/Thy/Fundefs.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 Tutorial for function definitions with the new "function" package.
     6 *)
     7 
     8 theory Functions
     9 imports Main
    10 begin
    11 
    12 section {* Function Definitions for Dummies *}
    13 
    14 text {*
    15   In most cases, defining a recursive function is just as simple as other definitions:
    16 *}
    17 
    18 fun fib :: "nat \<Rightarrow> nat"
    19 where
    20   "fib 0 = 1"
    21 | "fib (Suc 0) = 1"
    22 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
    23 
    24 text {*
    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}"}.
    32 *}
    33 
    34 text {*
    35   The function always terminates, since its argument gets smaller in
    36   every recursive call. 
    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.
    44 *}
    45 
    46 subsection {* Pattern matching *}
    47 
    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.
    55 
    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:
    59 *}
    60 
    61 fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    62 where
    63   "sep a (x#y#xs) = x # a # sep a (y # xs)"
    64 | "sep a xs       = xs"
    65 
    66 text {* 
    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:
    71 *}
    72 
    73 thm sep.simps
    74 
    75 text {* @{thm [display] sep.simps[no_vars]} *}
    76 
    77 text {* 
    78   \noindent The equations from function definitions are automatically used in
    79   simplification:
    80 *}
    81 
    82 lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"
    83 by simp
    84 
    85 subsection {* Induction *}
    86 
    87 text {*
    88 
    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}:
    93 
    94   @{thm [display] sep.induct}
    95   
    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}
    99 *}
   100 
   101 lemma "map f (sep x ys) = sep (f x) (map f ys)"
   102 apply (induct x ys rule: sep.induct)
   103 
   104 txt {*
   105   We get three cases, like in the definition.
   106 
   107   @{subgoals [display]}
   108 *}
   109 
   110 apply auto 
   111 done
   112 text {*
   113 
   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
   116   the remaining 20\%.
   117 *}
   118 
   119 
   120 section {* fun vs.\ function *}
   121 
   122 text {* 
   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.
   130 
   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:
   133 
   134 \end{isamarkuptext}
   135 
   136 
   137 \[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}
   138 \cmd{fun} @{text "f :: \<tau>"}\\%
   139 \cmd{where}\\%
   140 \hspace*{2ex}{\it equations}\\%
   141 \hspace*{2ex}\vdots\vspace*{6pt}
   142 \end{minipage}\right]
   143 \quad\equiv\quad
   144 \left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}
   145 \cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%
   146 \cmd{where}\\%
   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}
   151 \end{minipage}
   152 \right]\]
   153 
   154 \begin{isamarkuptext}
   155   \vspace*{1em}
   156   \noindent Some details have now become explicit:
   157 
   158   \begin{enumerate}
   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.
   163 
   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.
   168 
   169   \item A termination proof follows the definition, started by the
   170   \cmd{termination} command. This will be explained in \S\ref{termination}.
   171  \end{enumerate}
   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.
   175  *}
   176 
   177 
   178 section {* Termination *}
   179 
   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
   186   relation manually.
   187 *}
   188 
   189 subsection {* The {\tt relation} method *}
   190 text{*
   191   Consider the following function, which sums up natural numbers up to
   192   @{text "N"}, using a counter @{text "i"}:
   193 *}
   194 
   195 function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   196 where
   197   "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
   198 by pat_completeness auto
   199 
   200 text {*
   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.
   204 
   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.
   210 
   211   We can use this expression as a measure function suitable to prove termination.
   212 *}
   213 
   214 termination
   215 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
   216 
   217 txt {*
   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.
   221 
   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
   226   example.
   227 
   228   The predefined function @{term_type "measure"} constructs a
   229   wellfounded relation from a mapping into the natural numbers (a
   230   \emph{measure function}). 
   231 
   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
   235   relation:
   236 
   237   @{subgoals[display,indent=0]}
   238 
   239   These goals are all solved by @{text "auto"}:
   240 *}
   241 
   242 apply auto
   243 done
   244 
   245 text {*
   246   Let us complicate the function a little, by adding some more
   247   recursive calls: 
   248 *}
   249 
   250 function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   251 where
   252   "foo i N = (if i > N 
   253               then (if N = 0 then 0 else foo 0 (N - 1))
   254               else i + foo (Suc i) N)"
   255 by pat_completeness auto
   256 
   257 text {*
   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.  
   266 *}
   267 
   268 termination 
   269 by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
   270 
   271 subsection {* How @{text "lexicographic_order"} works *}
   272 
   273 (*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
   274 where
   275   "fails a [] = a"
   276 | "fails a (x#xs) = fails (x + a) (x # xs)"
   277 *)
   278 
   279 text {*
   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}}:
   283 
   284 \end{isamarkuptext}  
   285 \cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\%
   286 \cmd{where}\\%
   287 \hspace*{2ex}@{text "\"fails a [] = a\""}\\%
   288 |\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\
   289 \begin{isamarkuptext}
   290 
   291 \noindent Isabelle responds with the following error:
   292 
   293 \begin{isabelle}
   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
   301 *** Calls:\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
   308 *** a:  ?   <= \newline
   309 *** Could not find lexicographic termination order.\newline
   310 *** At command "fun".\newline
   311 \end{isabelle}
   312 *}
   313 
   314 
   315 text {*
   316 
   317 
   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). 
   323 
   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 "?"}.
   329 
   330   For the failed proof attempts, the unfinished subgoals are also
   331   printed. Looking at these will often point to a missing lemma.
   332 
   333 %  As a more real example, here is quicksort:
   334 *}
   335 (*
   336 function qs :: "nat list \<Rightarrow> nat list"
   337 where
   338   "qs [] = []"
   339 | "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
   340 by pat_completeness auto
   341 
   342 termination apply lexicographic_order
   343 
   344 text {* If we try @{text "lexicographic_order"} method, we get the
   345   following error *}
   346 termination by (lexicographic_order simp:l2)
   347 
   348 lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
   349 
   350 function 
   351 
   352 *)
   353 
   354 section {* Mutual Recursion *}
   355 
   356 text {*
   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"}:
   359 *}
   360 
   361 function even :: "nat \<Rightarrow> bool"
   362     and odd  :: "nat \<Rightarrow> bool"
   363 where
   364   "even 0 = True"
   365 | "odd 0 = False"
   366 | "even (Suc n) = odd n"
   367 | "odd (Suc n) = even n"
   368 by pat_completeness auto
   369 
   370 text {*
   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
   376   sum type: 
   377 *}
   378 
   379 termination 
   380 by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") auto
   381 
   382 text {* 
   383   We could also have used @{text lexicographic_order}, which
   384   supports mutual recursive termination proofs to a certain extent.
   385 *}
   386 
   387 subsection {* Induction for mutual recursion *}
   388 
   389 text {*
   390 
   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.
   394 
   395   Let us prove something about @{const even} and @{const odd}:
   396 *}
   397 
   398 lemma even_odd_mod2:
   399   "even n = (n mod 2 = 0)"
   400   "odd n = (n mod 2 = 1)"
   401 
   402 txt {* 
   403   We apply simultaneous induction, specifying the induction variable
   404   for both goals, separated by \cmd{and}:  *}
   405 
   406 apply (induct n and n rule: even_odd.induct)
   407 
   408 txt {* 
   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:
   414 *}
   415 
   416 apply simp_all
   417 
   418 txt {* 
   419   @{subgoals[display,indent=0]} 
   420 
   421   \noindent These can be handled by Isabelle's arithmetic decision procedures.
   422   
   423 *}
   424 
   425 apply arith
   426 apply arith
   427 done
   428 
   429 text {*
   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:
   435 *}
   436 
   437 lemma failed_attempt:
   438   "even n = (n mod 2 = 0)"
   439   "True"
   440 apply (induct n rule: even_odd.induct)
   441 
   442 txt {*
   443   \noindent Now the third subgoal is a dead end, since we have no
   444   useful induction hypothesis available:
   445 
   446   @{subgoals[display,indent=0]} 
   447 *}
   448 
   449 oops
   450 
   451 section {* General pattern matching *}
   452 text{*\label{genpats} *}
   453 
   454 subsection {* Avoiding automatic pattern splitting *}
   455 
   456 text {*
   457 
   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}.
   462 
   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:
   466   
   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. 
   470 *}
   471 
   472 datatype P3 = T | F | X
   473 
   474 text {* \noindent Then the conjunction of such values can be defined as follows: *}
   475 
   476 fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
   477 where
   478   "And T p = p"
   479 | "And p T = p"
   480 | "And p F = F"
   481 | "And F p = F"
   482 | "And X X = X"
   483 
   484 
   485 text {* 
   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:
   491 *}
   492 
   493 thm And.simps
   494 
   495 text {*
   496   @{thm[indent=4] And.simps}
   497   
   498   \vspace*{1em}
   499   \noindent There are several problems with this:
   500 
   501   \begin{enumerate}
   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
   505   example.
   506 
   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.
   511 
   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.
   515 
   516   \item In general, it increases clarity if we get the same definition
   517   back which we put in.
   518   \end{enumerate}
   519 
   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.}:
   525 *}
   526 
   527 function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3"
   528 where
   529   "And2 T p = p"
   530 | "And2 p T = p"
   531 | "And2 p F = F"
   532 | "And2 F p = F"
   533 | "And2 X X = X"
   534 
   535 txt {*
   536   \noindent Now let's look at the proof obligations generated by a
   537   function definition. In this case, they are:
   538 
   539   @{subgoals[display,indent=0]}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}
   540 
   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"}
   548   method:
   549 *}
   550 
   551 apply pat_completeness
   552 
   553 txt {*
   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"}.
   560 *}
   561 
   562 by auto
   563 
   564 
   565 subsection {* Non-constructor patterns *}
   566 
   567 text {*
   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.
   572 
   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:
   577 *}
   578 
   579 function fib2 :: "nat \<Rightarrow> nat"
   580 where
   581   "fib2 0 = 1"
   582 | "fib2 1 = 1"
   583 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
   584 
   585 (*<*)ML "goals_limit := 1"(*>*)
   586 txt {*
   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 +
   591   (2::nat)"}:
   592 
   593   @{subgoals[display,indent=0]}
   594 
   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.
   601 *}
   602 (*<*)ML "goals_limit := 10"(*>*)
   603 apply atomize_elim
   604 apply arith
   605 apply auto
   606 done
   607 termination by lexicographic_order
   608 
   609 text {*
   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:
   613 *}
   614 
   615 function ev :: "nat \<Rightarrow> bool"
   616 where
   617   "ev (2 * n) = True"
   618 | "ev (2 * n + 1) = False"
   619 apply atomize_elim
   620 by arith+
   621 termination by (relation "{}") simp
   622 
   623 text {*
   624   This general notion of pattern matching gives you the full freedom
   625   of mathematical specifications. However, as always, freedom should
   626   be used with care:
   627 
   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.
   634 *}
   635 
   636 
   637 subsection {* Conditional equations *}
   638 
   639 text {* 
   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}:
   644 *}
   645 
   646 function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   647 where
   648   "gcd x 0 = x"
   649 | "gcd 0 y = y"
   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
   654 
   655 text {*
   656   By now, you can probably guess what the proof obligations for the
   657   pattern completeness and compatibility look like. 
   658 
   659   Again, functions with conditional patterns are not supported by the
   660   code generator.
   661 *}
   662 
   663 
   664 subsection {* Pattern matching on strings *}
   665 
   666 text {*
   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:
   670 
   671 \end{isamarkuptext}
   672 \noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\%
   673 \cmd{where}\\%
   674 \hspace*{2ex}@{text "\"check (''good'') = True\""}\\%
   675 @{text "| \"check s = False\""}
   676 \begin{isamarkuptext}
   677 
   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.
   683 
   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:
   686 *}
   687 
   688 function check :: "string \<Rightarrow> bool"
   689 where
   690   "check (''good'') = True"
   691 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
   692 by auto
   693 
   694 
   695 section {* Partiality *}
   696 
   697 text {* 
   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
   700   of undefinedness. 
   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.
   704 
   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. 
   708 *}
   709 
   710 function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"
   711 where
   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](*>*)
   715 
   716 text {*
   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?
   720 *}
   721 
   722 subsection {* Domain predicates *}
   723 
   724 text {*
   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
   732   pinduct}: 
   733 *}
   734 
   735 text {*
   736   \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}
   737   \hfill(@{text "findzero.psimps"})
   738   \vspace{1em}
   739 
   740   \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}
   741   \hfill(@{text "findzero.pinduct"})
   742 *}
   743 
   744 text {*
   745   Remember that all we
   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}.
   751 
   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}:
   755 *}
   756 
   757 lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
   758 
   759 txt {* \noindent We apply induction as usual, but using the partial induction
   760   rule: *}
   761 
   762 apply (induct f n rule: findzero.pinduct)
   763 
   764 txt {* \noindent This gives the following subgoals:
   765 
   766   @{subgoals[display,indent=0]}
   767 
   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:
   774  *}
   775 apply simp
   776 done
   777 
   778 text {*
   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.
   785 *}
   786 
   787 text_raw {*
   788 \begin{figure}
   789 \hrule\vspace{6pt}
   790 \begin{minipage}{0.8\textwidth}
   791 \isabellestyle{it}
   792 \isastyle\isamarkuptrue
   793 *}
   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"
   800   proof 
   801     assume "f n = 0"
   802     with dom have "findzero f n = n" by simp
   803     with x_range show False by auto
   804   qed
   805   
   806   from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto
   807   thus "f x \<noteq> 0"
   808   proof
   809     assume "x = n"
   810     with `f n \<noteq> 0` show ?thesis by simp
   811   next
   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`
   815     show ?thesis by simp
   816   qed
   817 qed
   818 text_raw {*
   819 \isamarkupfalse\isabellestyle{tt}
   820 \end{minipage}\vspace{6pt}\hrule
   821 \caption{A proof about a partial function}\label{findzero_isar}
   822 \end{figure}
   823 *}
   824 
   825 subsection {* Partial termination proofs *}
   826 
   827 text {*
   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.
   832 
   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:
   840 
   841 \vspace{1ex}
   842 \noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
   843 \cmd{where}\isanewline%
   844 \ \ \ldots\\
   845 
   846   \noindent Now the package has proved an introduction rule for @{text findzero_dom}:
   847 *}
   848 
   849 thm findzero.domintros
   850 
   851 text {*
   852   @{thm[display] findzero.domintros}
   853 
   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
   858   induction principle.
   859 
   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
   863   \qt{downwards}:
   864 
   865   \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}
   866 
   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
   872   principle.
   873 
   874 *}
   875 
   876 text_raw {*
   877 \begin{figure}
   878 \hrule\vspace{6pt}
   879 \begin{minipage}{0.8\textwidth}
   880 \isabellestyle{it}
   881 \isastyle\isamarkuptrue
   882 *}
   883 lemma findzero_termination:
   884   assumes "x \<ge> n" and "f x = 0"
   885   shows "findzero_dom (f, n)"
   886 proof - 
   887   have base: "findzero_dom (f, x)"
   888     by (rule findzero.domintros) (simp add:`f x = 0`)
   889 
   890   have step: "\<And>i. findzero_dom (f, Suc i) 
   891     \<Longrightarrow> findzero_dom (f, i)"
   892     by (rule findzero.domintros) simp
   893 
   894   from `x \<ge> n` show ?thesis
   895   proof (induct rule:inc_induct)
   896     show "findzero_dom (f, x)" by (rule base)
   897   next
   898     fix i assume "findzero_dom (f, Suc i)"
   899     thus "findzero_dom (f, i)" by (rule step)
   900   qed
   901 qed      
   902 text_raw {*
   903 \isamarkupfalse\isabellestyle{tt}
   904 \end{minipage}\vspace{6pt}\hrule
   905 \caption{Termination proof for @{text findzero}}\label{findzero_term}
   906 \end{figure}
   907 *}
   908       
   909 text {*
   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:
   913 *}
   914 
   915 lemma findzero_termination_short:
   916   assumes zero: "x >= n" 
   917   assumes [simp]: "f x = 0"
   918   shows "findzero_dom (f, n)"
   919 using zero
   920 by (induct rule:inc_induct) (auto intro: findzero.domintros)
   921     
   922 text {*
   923   \noindent It is simple to combine the partial correctness result with the
   924   termination lemma:
   925 *}
   926 
   927 lemma findzero_total_correctness:
   928   "f x = 0 \<Longrightarrow> f (findzero f 0) = 0"
   929 by (blast intro: findzero_zero findzero_termination)
   930 
   931 subsection {* Definition of the domain predicate *}
   932 
   933 text {*
   934   Sometimes it is useful to know what the definition of the domain
   935   predicate looks like. Actually, @{text findzero_dom} is just an
   936   abbreviation:
   937 
   938   @{abbrev[display] findzero_dom}
   939 
   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:
   946 
   947   @{thm[display] findzero_rel.intros}
   948 
   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
   954   recursive call.
   955 
   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"}).
   960 
   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"}.
   966 *}
   967 
   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)+
   972 *)
   973   
   974 subsection {* A Useful Special Case: Tail recursion *}
   975 
   976 text {*
   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}
   985   rules. 
   986 
   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
   991   are non-terminating. 
   992 
   993 %  A function is tail recursive, if each call to the function is either
   994 %  equal
   995 %
   996 %  So the outer form of the 
   997 %
   998 %if it can be written in the following
   999 %  form:
  1000 %  {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}
  1001 
  1002 
  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:
  1007 
  1008 \vspace{1ex}
  1009 \noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%
  1010 \cmd{where}\isanewline%
  1011 \ \ \ldots\\%
  1012 
  1013   
  1014   \noindent Now, we actually get unconditional simplification rules, even
  1015   though the function is partial:
  1016 *}
  1017 
  1018 thm findzero.simps
  1019 
  1020 text {*
  1021   @{thm[display] findzero.simps}
  1022 
  1023   \noindent Of course these would make the simplifier loop, so we better remove
  1024   them from the simpset:
  1025 *}
  1026 
  1027 declare findzero.simps[simp del]
  1028 
  1029 text {* 
  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
  1038   definition.
  1039 *}
  1040 
  1041 section {* Nested recursion *}
  1042 
  1043 text {*
  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. 
  1047 
  1048   As a small example, we define the \qt{nested zero} function:
  1049 *}
  1050 
  1051 function nz :: "nat \<Rightarrow> nat"
  1052 where
  1053   "nz 0 = 0"
  1054 | "nz (Suc n) = nz (nz n)"
  1055 by pat_completeness auto
  1056 
  1057 text {*
  1058   If we attempt to prove termination using the identity measure on
  1059   naturals, this fails:
  1060 *}
  1061 
  1062 termination
  1063   apply (relation "measure (\<lambda>n. n)")
  1064   apply auto
  1065 
  1066 txt {*
  1067   We get stuck with the subgoal
  1068 
  1069   @{subgoals[display]}
  1070 
  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.
  1074 *}
  1075 (*<*)oops(*>*)
  1076 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
  1077   by (induct rule:nz.pinduct) auto
  1078 
  1079 text {*
  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:
  1084 *}
  1085 
  1086 termination
  1087   by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero)
  1088 
  1089 text {*
  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.
  1095 *}
  1096 
  1097 text_raw {*
  1098 \begin{figure}
  1099 \hrule\vspace{6pt}
  1100 \begin{minipage}{0.8\textwidth}
  1101 \isabellestyle{it}
  1102 \isastyle\isamarkuptrue
  1103 *}
  1104 
  1105 function f91 :: "nat \<Rightarrow> nat"
  1106 where
  1107   "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
  1108 by pat_completeness auto
  1109 
  1110 lemma f91_estimate: 
  1111   assumes trm: "f91_dom n" 
  1112   shows "n < f91 n + 11"
  1113 using trm by induct auto
  1114 
  1115 termination
  1116 proof
  1117   let ?R = "measure (\<lambda>x. 101 - x)"
  1118   show "wf ?R" ..
  1119 
  1120   fix n :: nat assume "\<not> 100 < n" -- "Assumptions for both calls"
  1121 
  1122   thus "(n + 11, n) \<in> ?R" by simp -- "Inner call"
  1123 
  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
  1127 qed
  1128 
  1129 text_raw {*
  1130 \isamarkupfalse\isabellestyle{tt}
  1131 \end{minipage}
  1132 \vspace{6pt}\hrule
  1133 \caption{McCarthy's 91-function}\label{f91}
  1134 \end{figure}
  1135 *}
  1136 
  1137 
  1138 section {* Higher-Order Recursion *}
  1139 
  1140 text {*
  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:
  1145 *}
  1146 
  1147 datatype 'a tree = 
  1148   Leaf 'a 
  1149 | Branch "'a tree list"
  1150 
  1151 
  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}: *}
  1154 
  1155 lemma [simp]: "x \<in> set l \<Longrightarrow> f x < Suc (list_size f l)"
  1156 by (induct l) auto
  1157 
  1158 
  1159 fun mirror :: "'a tree \<Rightarrow> 'a tree"
  1160 where
  1161   "mirror (Leaf n) = Leaf n"
  1162 | "mirror (Branch l) = Branch (rev (map mirror l))"
  1163 
  1164 
  1165 text {*
  1166   \emph{Note: The handling of size functions is currently changing 
  1167   in the developers version of Isabelle. So this documentation is outdated.}
  1168 *}
  1169 
  1170 termination proof
  1171   txt {*
  1172 
  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
  1176   subgoals
  1177 
  1178   @{subgoals[display,indent=0]} 
  1179 
  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:
  1184   *}
  1185 
  1186   show "wf (measure size)" by simp
  1187 next
  1188   fix f l and x :: "'a tree"
  1189   assume "x \<in> set l"
  1190   thus "(x, Branch l) \<in> measure size"
  1191     apply simp
  1192     txt {*
  1193       Simplification returns the following subgoal: 
  1194 
  1195       @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"} 
  1196 
  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
  1200       it, by induction.
  1201       *}
  1202     (*<*)oops(*>*)
  1203 
  1204 text {* 
  1205     Now the whole termination proof is automatic:
  1206   *}
  1207 
  1208 termination 
  1209   by lexicographic_order
  1210 
  1211 subsection {* Congruence Rules *}
  1212 
  1213 text {*
  1214   Let's come back to the question how Isabelle knows about @{const
  1215   map}.
  1216 
  1217   The knowledge about map is encoded in so-called congruence rules,
  1218   which are special theorems known to the \cmd{function} command. The
  1219   rule for map is
  1220 
  1221   @{thm[display] map_cong}
  1222 
  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
  1227   @{term l}.
  1228 
  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
  1235   is false:
  1236 
  1237   @{thm[display] if_cong}
  1238   
  1239   Congruence rules can be added to the
  1240   function package by giving them the @{term fundef_cong} attribute.
  1241 
  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. 
  1247 *}
  1248 
  1249 subsection {* Congruence Rules and Evaluation Order *}
  1250 
  1251 text {* 
  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
  1255   evaluated. 
  1256 
  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. 
  1261 
  1262   Consider the following function.
  1263 *}
  1264 
  1265 function f :: "nat \<Rightarrow> bool"
  1266 where
  1267   "f n = (n = 0 \<or> f (n - 1))"
  1268 (*<*)by pat_completeness auto(*>*)
  1269 
  1270 text {*
  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:
  1274 
  1275   \vspace{1ex}
  1276   \noindent @{thm disj_cong}\hfill(@{text "disj_cong"})
  1277   \vspace{1ex}
  1278 
  1279   Now the definition works without problems. Note how the termination
  1280   proof depends on the extra condition that we get from the congruence
  1281   rule.
  1282 
  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:
  1286 *}
  1287 
  1288 lemma disj_cong2[fundef_cong]: 
  1289   "(\<not> Q' \<Longrightarrow> P = P') \<Longrightarrow> (Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')"
  1290   by blast
  1291 
  1292 fun f' :: "nat \<Rightarrow> bool"
  1293 where
  1294   "f' n = (f' (n - 1) \<or> n = 0)"
  1295 
  1296 text {*
  1297   \noindent These examples show that, in general, there is no \qt{best} set of
  1298   congruence rules.
  1299 
  1300   However, such tweaking should rarely be necessary in
  1301   practice, as most of the time, the default set of congruence rules
  1302   works well.
  1303 *}
  1304 
  1305 end