doc-src/TutorialI/Advanced/WFrec.thy
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10545 216388848786
child 10795 9e888d60d3e5
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)theory WFrec = Main:(*>*)
     2 
     3 text{*\noindent
     4 So far, all recursive definitions where shown to terminate via measure
     5 functions. Sometimes this can be quite inconvenient or even
     6 impossible. Fortunately, \isacommand{recdef} supports much more
     7 general definitions. For example, termination of Ackermann's function
     8 can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
     9 *}
    10 
    11 consts ack :: "nat\<times>nat \<Rightarrow> nat";
    12 recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
    13   "ack(0,n)         = Suc n"
    14   "ack(Suc m,0)     = ack(m, 1)"
    15   "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
    16 
    17 text{*\noindent
    18 The lexicographic product decreases if either its first component
    19 decreases (as in the second equation and in the outer call in the
    20 third equation) or its first component stays the same and the second
    21 component decreases (as in the inner call in the third equation).
    22 
    23 In general, \isacommand{recdef} supports termination proofs based on
    24 arbitrary well-founded relations as introduced in \S\ref{sec:Well-founded}.
    25 This is called \textbf{well-founded
    26 recursion}\indexbold{recursion!well-founded}. Clearly, a function definition
    27 is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the
    28 left-hand side of an equation and $r$ the argument of some recursive call on
    29 the corresponding right-hand side, induces a well-founded relation.  For a
    30 systematic account of termination proofs via well-founded relations see, for
    31 example, \cite{Baader-Nipkow}.
    32 
    33 Each \isacommand{recdef} definition should be accompanied (after the name of
    34 the function) by a well-founded relation on the argument type of the
    35 function.  The HOL library formalizes some of the most important
    36 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
    37 example, @{term"measure f"} is always well-founded, and the lexicographic
    38 product of two well-founded relations is again well-founded, which we relied
    39 on when defining Ackermann's function above.
    40 Of course the lexicographic product can also be interated:
    41 *}
    42 
    43 consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat"
    44 recdef contrived
    45   "measure(\<lambda>i. i) <*lex*> measure(\<lambda>j. j) <*lex*> measure(\<lambda>k. k)"
    46 "contrived(i,j,Suc k) = contrived(i,j,k)"
    47 "contrived(i,Suc j,0) = contrived(i,j,j)"
    48 "contrived(Suc i,0,0) = contrived(i,i,i)"
    49 "contrived(0,0,0)     = 0"
    50 
    51 text{*
    52 Lexicographic products of measure functions already go a long
    53 way. Furthermore you may embed some type in an
    54 existing well-founded relation via the inverse image construction @{term
    55 inv_image}. All these constructions are known to \isacommand{recdef}. Thus you
    56 will never have to prove well-foundedness of any relation composed
    57 solely of these building blocks. But of course the proof of
    58 termination of your function definition, i.e.\ that the arguments
    59 decrease with every recursive call, may still require you to provide
    60 additional lemmas.
    61 
    62 It is also possible to use your own well-founded relations with \isacommand{recdef}.
    63 Here is a simplistic example:
    64 *}
    65 
    66 consts f :: "nat \<Rightarrow> nat"
    67 recdef f "id(less_than)"
    68 "f 0 = 0"
    69 "f (Suc n) = f n"
    70 
    71 text{*\noindent
    72 Since \isacommand{recdef} is not prepared for @{term id}, the identity
    73 function, this leads to the complaint that it could not prove
    74 @{prop"wf (id less_than)"}.
    75 We should first have proved that @{term id} preserves well-foundedness
    76 *}
    77 
    78 lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
    79 by simp;
    80 
    81 text{*\noindent
    82 and should have appended the following hint to our above definition:
    83 \indexbold{*recdef_wf}
    84 *}
    85 (*<*)
    86 consts g :: "nat \<Rightarrow> nat"
    87 recdef g "id(less_than)"
    88 "g 0 = 0"
    89 "g (Suc n) = g n"
    90 (*>*)
    91 (hints recdef_wf: wf_id)
    92 (*<*)end(*>*)