# HG changeset patch # User krauss # Date 1212159817 -7200 # Node ID 3602b81665b59d28af0a7cf53a85cea2274d9d0b # Parent c1f9fb015ea541a02224b51f26c6bb2daac966ae Updated function tutorial. diff -r c1f9fb015ea5 -r 3602b81665b5 doc-src/IsarAdvanced/Functions/Thy/Functions.thy --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Fri May 30 09:17:44 2008 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Fri May 30 17:03:37 2008 +0200 @@ -123,7 +123,7 @@ The \cmd{fun} command provides a convenient shorthand notation for simple function definitions. In this mode, Isabelle tries to solve all the necessary proof obligations - automatically. If a proof fails, the definition is + automatically. If any proof fails, the definition is rejected. This can either mean that the definition is indeed faulty, or that the default proof procedures are just not smart enough (or rather: not designed) to handle the definition. @@ -141,7 +141,7 @@ \hspace*{2ex}\vdots\vspace*{6pt} \end{minipage}\right] \quad\equiv\quad -\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt} +\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt} \cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \"}\\% \cmd{where}\\% \hspace*{2ex}{\it equations}\\% @@ -211,7 +211,7 @@ We can use this expression as a measure function suitable to prove termination. *} -termination +termination sum apply (relation "measure (\(i,N). N + 1 - i)") txt {* @@ -225,7 +225,7 @@ these are packed together into a tuple, as it happened in the above example. - The predefined function @{term_type "measure"} constructs a + The predefined function @{term[source] "measure :: ('a \ nat) \ ('a \ 'a) set"} constructs a wellfounded relation from a mapping into the natural numbers (a \emph{measure function}). @@ -430,8 +430,8 @@ In proofs like this, the simultaneous induction is really essential: Even if we are just interested in one of the results, the other one is necessary to strengthen the induction hypothesis. If we leave - out the statement about @{const odd} (by substituting it with @{term - "True"}), the same proof fails: + out the statement about @{const odd} and just write @{term True} instead, + the same proof fails: *} lemma failed_attempt: @@ -543,7 +543,7 @@ the function's input type must match at least one of the patterns\footnote{Completeness could be equivalently stated as a disjunction of existential statements: @{term "(\p. x = (T, p)) \ (\p. x = (p, T)) \ (\p. x = (p, F)) \ - (\p. x = (F, p)) \ (x = (X, X))"}.}. If the patterns just involve + (\p. x = (F, p)) \ (x = (X, X))"}, and you can use the method @{text atomize_elim} to get that form instead.}. If the patterns just involve datatypes, we can solve it with the @{text "pat_completeness"} method: *} @@ -605,7 +605,6 @@ apply auto done termination by lexicographic_order - text {* We can stretch the notion of pattern matching even more. The following function is not a sensible functional program, but a @@ -621,8 +620,8 @@ termination by (relation "{}") simp text {* - This general notion of pattern matching gives you the full freedom - of mathematical specifications. However, as always, freedom should + This general notion of pattern matching gives you a certain freedom + in writing down specifications. However, as always, such freedom should be used with care: If we leave the area of constructor @@ -1152,16 +1151,13 @@ text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the list functions @{const rev} and @{const map}: *} -function mirror :: "'a tree \ 'a tree" +fun mirror :: "'a tree \ 'a tree" where "mirror (Leaf n) = Leaf n" | "mirror (Branch l) = Branch (rev (map mirror l))" -by pat_completeness auto - text {* - \emph{Note: The handling of size functions is currently changing - in the developers version of Isabelle. So this documentation is outdated.} + Although the definition is accepted without problems, let us look at the termination proof: *} termination proof @@ -1169,49 +1165,17 @@ As usual, we have to give a wellfounded relation, such that the arguments of the recursive calls get smaller. But what exactly are - the arguments of the recursive calls? Isabelle gives us the + the arguments of the recursive calls when mirror is given as an + argument to map? Isabelle gives us the subgoals @{subgoals[display,indent=0]} - So Isabelle seems to know that @{const map} behaves nicely and only + So the system seems to know that @{const map} only applies the recursive call @{term "mirror"} to elements - of @{term "l"}. Before we discuss where this knowledge comes from, - let us finish the termination proof: - *} - - show "wf (measure size)" by simp -next - fix f l and x :: "'a tree" - assume "x \ set l" - thus "(x, Branch l) \ measure size" - apply simp - txt {* - Simplification returns the following subgoal: - - @{text[display] "1. x \ set l \ size x < Suc (list_size size l)"} + of @{term "l"}, which is essential for the termination proof. - We are lacking a property about the function @{term - tree_list_size}, which was generated automatically at the - definition of the @{text tree} type. We should go back and prove - it, by induction. - *} - (*<*)oops(*>*) - -text {* - Now the whole termination proof is automatic: - *} - -termination - by lexicographic_order - -subsection {* Congruence Rules *} - -text {* - Let's come back to the question how Isabelle knows about @{const - map}. - - The knowledge about map is encoded in so-called congruence rules, + This knowledge about map is encoded in so-called congruence rules, which are special theorems known to the \cmd{function} command. The rule for map is @@ -1221,7 +1185,7 @@ map} are equal, if the list arguments are equal and the functions coincide on the elements of the list. This means that for the value @{term "map f l"} we only have to know how @{term f} behaves on - @{term l}. + the elements of @{term l}. Usually, one such congruence rule is needed for each higher-order construct that is used when defining @@ -1238,10 +1202,11 @@ The constructs that are predefined in Isabelle, usually come with the respective congruence rules. - But if you define your own higher-order functions, you will have to - come up with the congruence rules yourself, if you want to use your + But if you define your own higher-order functions, you may have to + state and prove the required congruence rules yourself, if you want to use your functions in recursive definitions. *} +(*<*)oops(*>*) subsection {* Congruence Rules and Evaluation Order *} @@ -1265,7 +1230,7 @@ (*<*)by pat_completeness auto(*>*) text {* - As given above, the definition fails. The default configuration + For this definition, the termination proof fails. The default configuration specifies no congruence rule for disjunction. We have to add a congruence rule that specifies left-to-right evaluation order: diff -r c1f9fb015ea5 -r 3602b81665b5 doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri May 30 09:17:44 2008 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri May 30 17:03:37 2008 +0200 @@ -188,7 +188,7 @@ The \cmd{fun} command provides a convenient shorthand notation for simple function definitions. In this mode, Isabelle tries to solve all the necessary proof obligations - automatically. If a proof fails, the definition is + automatically. If any proof fails, the definition is rejected. This can either mean that the definition is indeed faulty, or that the default proof procedures are just not smart enough (or rather: not designed) to handle the definition. @@ -206,7 +206,7 @@ \hspace*{2ex}\vdots\vspace*{6pt} \end{minipage}\right] \quad\equiv\quad -\left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt} +\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt} \cmd{function} \isa{{\isacharparenleft}}\cmd{sequential}\isa{{\isacharparenright}\ f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}\\% \cmd{where}\\% \hspace*{2ex}{\it equations}\\% @@ -298,7 +298,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{termination}\isamarkupfalse% -\isanewline +\ sum\isanewline % \isadelimproof % @@ -318,7 +318,7 @@ these are packed together into a tuple, as it happened in the above example. - The predefined function \isa{measure{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} constructs a + The predefined function \isa{{\isachardoublequote}measure\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}} constructs a wellfounded relation from a mapping into the natural numbers (a \emph{measure function}). @@ -593,7 +593,8 @@ In proofs like this, the simultaneous induction is really essential: Even if we are just interested in one of the results, the other one is necessary to strengthen the induction hypothesis. If we leave - out the statement about \isa{odd} (by substituting it with \isa{True}), the same proof fails:% + out the statement about \isa{odd} and just write \isa{True} instead, + the same proof fails:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\isamarkupfalse% @@ -754,7 +755,7 @@ the form of an elimination rule and states that every \isa{x} of the function's input type must match at least one of the patterns\footnote{Completeness could be equivalently stated as a disjunction of existential statements: -\isa{{\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}}.}. If the patterns just involve +\isa{{\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}T{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ T{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}p{\isacharcomma}\ F{\isacharparenright}{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ x\ {\isacharequal}\ {\isacharparenleft}F{\isacharcomma}\ p{\isacharparenright}{\isacharparenright}\ {\isasymor}\ x\ {\isacharequal}\ {\isacharparenleft}X{\isacharcomma}\ X{\isacharparenright}}, and you can use the method \isa{atomize{\isacharunderscore}elim} to get that form instead.}. If the patterns just involve datatypes, we can solve it with the \isa{pat{\isacharunderscore}completeness} method:% \end{isamarkuptxt}% @@ -940,8 +941,8 @@ \endisadelimproof % \begin{isamarkuptext}% -This general notion of pattern matching gives you the full freedom - of mathematical specifications. However, as always, freedom should +This general notion of pattern matching gives you a certain freedom + in writing down specifications. However, as always, such freedom should be used with care: If we leave the area of constructor @@ -1792,29 +1793,13 @@ list functions \isa{rev} and \isa{map}:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{function}\isamarkupfalse% +\isacommand{fun}\isamarkupfalse% \ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline \isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline -{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline -% -\isadelimproof -% -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ pat{\isacharunderscore}completeness\ auto% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% +{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% -\emph{Note: The handling of size functions is currently changing - in the developers version of Isabelle. So this documentation is outdated.}% +Although the definition is accepted without problems, let us look at the termination proof:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{termination}\isamarkupfalse% @@ -1829,7 +1814,8 @@ \begin{isamarkuptxt}% As usual, we have to give a wellfounded relation, such that the arguments of the recursive calls get smaller. But what exactly are - the arguments of the recursive calls? Isabelle gives us the + the arguments of the recursive calls when mirror is given as an + argument to map? Isabelle gives us the subgoals \begin{isabelle}% @@ -1837,74 +1823,11 @@ \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}l\ x{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ {\isacharquery}R% \end{isabelle} - So Isabelle seems to know that \isa{map} behaves nicely and only + So the system seems to know that \isa{map} only applies the recursive call \isa{mirror} to elements - of \isa{l}. Before we discuss where this knowledge comes from, - let us finish the termination proof:% -\end{isamarkuptxt}% -\isamarkuptrue% -\ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}wf\ {\isacharparenleft}measure\ size{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\isacommand{next}\isamarkupfalse% -\isanewline -\ \ \isacommand{fix}\isamarkupfalse% -\ f\ l\ \isakeyword{and}\ x\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline -\ \ \isacommand{assume}\isamarkupfalse% -\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l{\isachardoublequoteclose}\isanewline -\ \ \isacommand{thus}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}\ Branch\ l{\isacharparenright}\ {\isasymin}\ measure\ size{\isachardoublequoteclose}\isanewline -\ \ \ \ \isacommand{apply}\isamarkupfalse% -\ simp% -\begin{isamarkuptxt}% -Simplification returns the following subgoal: - - \begin{isabelle}% -{\isadigit{1}}{\isachardot}\ x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ size\ x\ {\isacharless}\ Suc\ {\isacharparenleft}list{\isacharunderscore}size\ size\ l{\isacharparenright}% -\end{isabelle} + of \isa{l}, which is essential for the termination proof. - We are lacking a property about the function \isa{tree{\isacharunderscore}list{\isacharunderscore}size}, which was generated automatically at the - definition of the \isa{tree} type. We should go back and prove - it, by induction.% -\end{isamarkuptxt}% -\isamarkuptrue% -\ \ \ \ % -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\begin{isamarkuptext}% -Now the whole termination proof is automatic:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{termination}\isamarkupfalse% -\ \isanewline -% -\isadelimproof -\ \ % -\endisadelimproof -% -\isatagproof -\isacommand{by}\isamarkupfalse% -\ lexicographic{\isacharunderscore}order% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof -% -\isamarkupsubsection{Congruence Rules% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -Let's come back to the question how Isabelle knows about \isa{map}. - - The knowledge about map is encoded in so-called congruence rules, + This knowledge about map is encoded in so-called congruence rules, which are special theorems known to the \cmd{function} command. The rule for map is @@ -1915,7 +1838,7 @@ You can read this in the following way: Two applications of \isa{map} are equal, if the list arguments are equal and the functions coincide on the elements of the list. This means that for the value \isa{map\ f\ l} we only have to know how \isa{f} behaves on - \isa{l}. + the elements of \isa{l}. Usually, one such congruence rule is needed for each higher-order construct that is used when defining @@ -1934,12 +1857,19 @@ The constructs that are predefined in Isabelle, usually come with the respective congruence rules. - But if you define your own higher-order functions, you will have to - come up with the congruence rules yourself, if you want to use your + But if you define your own higher-order functions, you may have to + state and prove the required congruence rules yourself, if you want to use your functions in recursive definitions.% -\end{isamarkuptext}% +\end{isamarkuptxt}% \isamarkuptrue% % +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% \isamarkupsubsection{Congruence Rules and Evaluation Order% } \isamarkuptrue% @@ -1976,7 +1906,7 @@ \endisadelimproof % \begin{isamarkuptext}% -As given above, the definition fails. The default configuration +For this definition, the termination proof fails. The default configuration specifies no congruence rule for disjunction. We have to add a congruence rule that specifies left-to-right evaluation order: diff -r c1f9fb015ea5 -r 3602b81665b5 doc-src/IsarAdvanced/Functions/intro.tex --- a/doc-src/IsarAdvanced/Functions/intro.tex Fri May 30 09:17:44 2008 +0200 +++ b/doc-src/IsarAdvanced/Functions/intro.tex Fri May 30 17:03:37 2008 +0200 @@ -1,6 +1,6 @@ \section{Introduction} -Since the release of Isabelle 2007, new facilities for recursive +Starting from Isabelle 2007, new facilities for recursive function definitions~\cite{krauss2006} are available. They provide better support for general recursive definitions than previous packages. But despite all tool support, function definitions can @@ -11,7 +11,7 @@ defining functions quickly. For the more difficult definitions we will discuss what problems can arise, and how they can be solved. -We assume that you have mastered the basics of Isabelle/HOL +We assume that you have mastered the fundamentals of Isabelle/HOL and are able to write basic specifications and proofs. To start out with Isabelle in general, consult the Isabelle/HOL tutorial \cite{isa-tutorial}. @@ -21,13 +21,13 @@ \paragraph{Structure of this tutorial.} Section 2 introduces the syntax and basic operation of the \cmd{fun} command, which provides full automation with reasonable default -behavior. The impatient reader might want to stop after that +behavior. The impatient reader can stop after that section, and consult the remaining sections only when needed. Section 3 introduces the more verbose \cmd{function} command which -gives fine-grained control to the user. This form should be used +gives fine-grained control. This form should be used whenever the short form fails. -After that we discuss different issues that are more specialized: -termination, mutual and nested recursion, partiality, pattern matching +After that we discuss more specialized issues: +termination, mutual, nested and higher-order recursion, partiality, pattern matching and others. @@ -45,9 +45,9 @@ -The new \cmd{function} command, and its short form \cmd{fun} will -replace the traditional \cmd{recdef} command \cite{slind-tfl} in the future. It solves -a few of technical issues around \cmd{recdef}, and allows definitions +The new \cmd{function} command, and its short form \cmd{fun} have mostly +replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve +a few of technical issues around \cmd{recdef}, and allow definitions which were not previously possible.