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