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