summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 11 Oct 2000 13:15:04 +0200 | |

changeset 10189 | 865918597b63 |

parent 10188 | 2899182af616 |

child 10190 | 871772d38b30 |

*** empty log message ***

--- 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

--- a/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 12:52:56 2000 +0200 +++ b/doc-src/TutorialI/Advanced/advanced.tex Wed Oct 11 13:15:04 2000 +0200 @@ -18,6 +18,16 @@ covers two topics: how to define recursive function over nested recursive datatypes and how to establish termination by means other than measure functions. +If, after reading this section, you feel that the definition of recursive +functions is overly and maybe unnecessarily complicated by the requirement of +totality, you should ponder the alternative, a logic of partial functions, +where recursive definitions are always wellformed. For a start, there are many +such logics, and no clear winner has emerged. And in all of these logics you +are (more or less frequently) required to reason about the definedness of +terms explicitly. Thus one shifts definedness arguments from definition to +proof time. In HOL you may have to work hard to define a function, but proofs +can then proceed unencumbered by worries about undefinedness. + \subsection{Recursion over nested datatypes} \label{sec:nested-recdef} \input{Recdef/document/Nested0.tex}

--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Oct 11 12:52:56 2000 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Wed Oct 11 13:15:04 2000 +0200 @@ -28,11 +28,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 +\isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is +wellfounded. Each \isacommand{recdef} definition should be accompanied (after the name of the function) by a wellfounded relation on the argument type @@ -44,10 +47,63 @@ In addition to \isa{measure}, the library provides a number of further constructions for obtaining wellfounded relations. +Above we have already met \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} of type +\begin{isabelle}% +\ \ \ \ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}{\isacharparenright}set{\isachardoublequote}% +\end{isabelle} +Of course the lexicographic product can also be interated, as in the following +function definition:% +\end{isamarkuptext}% +\isacommand{consts}\ contrived\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymtimes}\ nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline +\isacommand{recdef}\ contrived\isanewline +\ \ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}i{\isachardot}\ i{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}j{\isachardot}\ j{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}k{\isachardot}\ k{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}Suc\ k{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}k{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}contrived{\isacharparenleft}i{\isacharcomma}Suc\ j{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}j{\isacharcomma}j{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}contrived{\isacharparenleft}Suc\ i{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ contrived{\isacharparenleft}i{\isacharcomma}i{\isacharcomma}i{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}% +\begin{isamarkuptext}% +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: +\begin{isabelle}% +\ \ \ \ \ inv{\isacharunderscore}image\ {\isacharparenleft}r{\isasymColon}{\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set{\isacharparenright}\ {\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymequiv}\isanewline +\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharcomma}\ y{\isasymColon}{\isacharprime}a{\isacharparenright}{\isachardot}\ {\isacharparenleft}f\ x{\isacharcomma}\ f\ y{\isacharparenright}\ {\isasymin}\ r{\isacharbraceright}% +\end{isabelle} +\begin{sloppypar} +\noindent +For example, \isa{measure} is actually defined as \isa{inv{\isacharunderscore}mage\ less{\isacharunderscore}than}, where +\isa{less{\isacharunderscore}than} of type \isa{{\isacharparenleft}nat\ {\isasymtimes}\ nat{\isacharparenright}\ set} is the less-than relation on type \isa{nat} +(as opposed to \isa{op\ {\isacharless}}, which is of type \isa{{\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool}). +\end{sloppypar} -wf proof auto if stndard constructions.% +%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:% \end{isamarkuptext}% -\end{isabellebody}% +\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline +\isacommand{recdef}\ f\ {\isachardoublequote}id{\isacharparenleft}less{\isacharunderscore}than{\isacharparenright}{\isachardoublequote}\isanewline +{\isachardoublequote}f\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline +{\isachardoublequote}f\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ f\ n{\isachardoublequote}% +\begin{isamarkuptext}% +Since \isacommand{recdef} is not prepared for \isa{id}, the identity +function, this leads to the complaint that it could not prove +\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}, the wellfoundedness of \isa{id\ less{\isacharunderscore}than}. We should first have proved that \isa{id} preserves wellfoundedness% +\end{isamarkuptext}% +\isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{by}\ simp% +\begin{isamarkuptext}% +\noindent +and should have added the following hint to our above definition:% +\end{isamarkuptext}% +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf\ add{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root"

--- a/doc-src/TutorialI/todo.tobias Wed Oct 11 12:52:56 2000 +0200 +++ b/doc-src/TutorialI/todo.tobias Wed Oct 11 13:15:04 2000 +0200 @@ -36,6 +36,8 @@ it would be nice if @term could deal with ?-vars. then a number of (unchecked!) @texts could be converted to @terms. +it would be nice if one could get id to the enclosing quotes in the [source] option. + Minor fixes in the tutorial =========================== @@ -50,20 +52,6 @@ Advanced Ind expects rulify, mp and spec. How much really? -recdef: subsection Beyond Measure on lex, finite_psubset, ... -incl Ackermann, which is now at the end of Recdef/termination.thy. --> Advanced. -Sentence at the end: -If you feel that the definition of recursive functions is overly and maybe -unnecessarily complicated by the requirement of totality you should ponder -the alternative, a logic of partial functions, where recursive definitions -are always wellformed. For a start, there are many -such logics, and no clear winner has emerged. And in all of these logics you -are (more or less frequently) required to reason about the definedness of -terms explicitly. Thus one shifts definedness arguments from definition to -proof time. In HOL you may have to work hard to define a function, but proofs -can then proceed unencumbered by worries about undefinedness. - Appendix: Lexical: long ids. Warning: infixes automatically become reserved words!