summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/Advanced/WFrec.thy

author | nipkow |

Wed, 11 Oct 2000 10:44:42 +0200 | |

changeset 10187 | 0376cccd9118 |

child 10189 | 865918597b63 |

permissions | -rw-r--r-- |

*** empty log message ***

(*<*)theory WFrec = Main:(*>*) text{*\noindent So far, all recursive definitions where shown to terminate via measure functions. Sometimes this can be quite inconvenient or even impossible. Fortunately, \isacommand{recdef} supports much more general definitions. For example, termination of Ackermann's function can be shown by means of the lexicographic product @{text"<*lex*>"}: *} consts ack :: "nat\<times>nat \<Rightarrow> nat"; recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)" "ack(0,n) = Suc n" "ack(Suc m,0) = ack(m, 1)" "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"; text{*\noindent The lexicographic product decreases if either its first component decreases (as in the second equation and in the outer call in the third equation) or its first component stays the same and the second component decreases (as in the inner call in the third equation). In general, \isacommand{recdef} supports termination proofs based on arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded recursion}\indexbold{recursion!wellfounded}\index{wellfounded recursion|see{recursion, wellfounded}}. A relation $<$ is \bfindex{wellfounded} if it has no infinite descending chain $\cdots < a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set of all pairs $(r,l)$, where $l$ is the argument on the left-hand side of an equation and $r$ the argument of some recursive call on the corresponding right-hand side, induces a wellfounded relation. For a systematic account of termination proofs via wellfounded relations see, for example, \cite{Baader-Nipkow}. Each \isacommand{recdef} definition should be accompanied (after the name of the function) by a wellfounded relation on the argument type of the function. For example, @{term measure} is defined by @{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"} and it has been proved that @{term"measure f"} is always wellfounded. In addition to @{term measure}, the library provides a number of further constructions for obtaining wellfounded relations. wf proof auto if stndard constructions. *} (*<*)end(*>*)