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(*>*)