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