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

doc-src/TutorialI/Advanced/WFrec.thy

changeset 10189 | 865918597b63 |

parent 10187 | 0376cccd9118 |

child 10190 | 871772d38b30 |

--- a/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 11 12:52:56 2000 +0200 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Wed Oct 11 13:15:04 2000 +0200 @@ -26,11 +26,14 @@ 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}. +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}. The HOL library formalizes +some of the theory of wellfounded relations. For example +@{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is +wellfounded. Each \isacommand{recdef} definition should be accompanied (after the name of the function) by a wellfounded relation on the argument type @@ -40,7 +43,68 @@ In addition to @{term measure}, the library provides a number of further constructions for obtaining wellfounded relations. +Above we have already met @{text"<*lex*>"} of type +@{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"} +Of course the lexicographic product can also be interated, as in the following +function definition: +*} -wf proof auto if stndard constructions. +consts contrived :: "nat \<times> nat \<times> nat \<Rightarrow> nat" +recdef contrived + "measure(\<lambda>i. i) <*lex*> measure(\<lambda>j. j) <*lex*> measure(\<lambda>k. k)" +"contrived(i,j,Suc k) = contrived(i,j,k)" +"contrived(i,Suc j,0) = contrived(i,j,j)" +"contrived(Suc i,0,0) = contrived(i,i,i)" +"contrived(0,0,0) = 0" + +text{* +Lexicographic products of measure functions already go a long way. A +further useful construction is the embedding of some type in an +existing wellfounded relation via the inverse image of a function: +@{thm[display,show_types]inv_image_def[no_vars]} +\begin{sloppypar} +\noindent +For example, @{term measure} is actually defined as @{term"inv_mage less_than"}, where +@{term less_than} of type @{typ"(nat \<times> nat)set"} is the less-than relation on type @{typ nat} +(as opposed to @{term"op <"}, which is of type @{typ"nat \<Rightarrow> nat \<Rightarrow> bool"}). +\end{sloppypar} + +%Finally there is also {finite_psubset} the proper subset relation on finite sets + +All the above constructions are known to \isacommand{recdef}. Thus you +will never have to prove wellfoundedness of any relation composed +solely of these building blocks. But of course the proof of +termination of your function definition, i.e.\ that the arguments +decrease with every recursive call, may still require you to provide +additional lemmas. + +It is also possible to use your own wellfounded relations with \isacommand{recdef}. +Here is a simplistic example: *} + +consts f :: "nat \<Rightarrow> nat" +recdef f "id(less_than)" +"f 0 = 0" +"f (Suc n) = f n" + +text{* +Since \isacommand{recdef} is not prepared for @{term id}, the identity +function, this leads to the complaint that it could not prove +@{prop"wf (id less_than)"}, the wellfoundedness of @{term"id +less_than"}. We should first have proved that @{term id} preserves wellfoundedness +*} + +lemma wf_id: "wf r \<Longrightarrow> wf(id r)" +by simp; + +text{*\noindent +and should have added the following hint to our above definition: +*} +(*<*) +consts g :: "nat \<Rightarrow> nat" +recdef g "id(less_than)" +"g 0 = 0" +"g (Suc n) = g n" +(*>*) +(hints recdef_wf add: wf_id) (*<*)end(*>*) \ No newline at end of file