1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/Fun/ROOT.ML Fri Nov 02 08:26:01 2007 +0100
1.3 @@ -0,0 +1,2 @@
1.4 +use "../settings";
1.5 +use_thy "fun0";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 08:26:01 2007 +0100
2.3 @@ -0,0 +1,362 @@
2.4 +%
2.5 +\begin{isabellebody}%
2.6 +\def\isabellecontext{fun{\isadigit{0}}}%
2.7 +%
2.8 +\isadelimtheory
2.9 +%
2.10 +\endisadelimtheory
2.11 +%
2.12 +\isatagtheory
2.13 +%
2.14 +\endisatagtheory
2.15 +{\isafoldtheory}%
2.16 +%
2.17 +\isadelimtheory
2.18 +%
2.19 +\endisadelimtheory
2.20 +%
2.21 +\begin{isamarkuptext}%
2.22 +\subsection{Definition}
2.23 +\label{sec:fun-examples}
2.24 +
2.25 +Here is a simple example, the \rmindex{Fibonacci function}:%
2.26 +\end{isamarkuptext}%
2.27 +\isamarkuptrue%
2.28 +\isacommand{fun}\isamarkupfalse%
2.29 +\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.30 +\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.31 +\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.32 +\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequoteclose}%
2.33 +\begin{isamarkuptext}%
2.34 +\noindent
2.35 +This resembles ordinary functional programming languages. Note the obligatory
2.36 +\isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
2.37 +defines the function in one go. Isabelle establishes termination automatically
2.38 +because \isa{fib}'s argument decreases in every recursive call.
2.39 +
2.40 +Slightly more interesting is the insertion of a fixed element
2.41 +between any two elements of a list:%
2.42 +\end{isamarkuptext}%
2.43 +\isamarkuptrue%
2.44 +\isacommand{fun}\isamarkupfalse%
2.45 +\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.46 +\ \ {\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.47 +\ \ {\isachardoublequoteopen}sep\ a\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.48 +\ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
2.49 +\begin{isamarkuptext}%
2.50 +\noindent
2.51 +This time the length of the list decreases with the
2.52 +recursive call; the first argument is irrelevant for termination.
2.53 +
2.54 +Pattern matching\index{pattern matching!and \isacommand{fun}}
2.55 +need not be exhaustive and may employ wildcards:%
2.56 +\end{isamarkuptext}%
2.57 +\isamarkuptrue%
2.58 +\isacommand{fun}\isamarkupfalse%
2.59 +\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.60 +\ \ {\isachardoublequoteopen}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.61 +\ \ {\isachardoublequoteopen}last\ {\isacharparenleft}{\isacharunderscore}{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}%
2.62 +\begin{isamarkuptext}%
2.63 +Overlapping patterns are disambiguated by taking the order of equations into
2.64 +account, just as in functional programming:%
2.65 +\end{isamarkuptext}%
2.66 +\isamarkuptrue%
2.67 +\isacommand{fun}\isamarkupfalse%
2.68 +\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.69 +\ \ {\isachardoublequoteopen}sep{\isadigit{1}}\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}\ a\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.70 +\ \ {\isachardoublequoteopen}sep{\isadigit{1}}\ {\isacharunderscore}\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
2.71 +\begin{isamarkuptext}%
2.72 +\noindent
2.73 +To guarantee that the second equation can only be applied if the first
2.74 +one does not match, Isabelle internally replaces the second equation
2.75 +by the two possibilities that are left: \isa{sep{\isadigit{1}}\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} and
2.76 +\isa{sep{\isadigit{1}}\ a\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}}. Thus the functions \isa{sep} and
2.77 +\isa{sep{\isadigit{1}}} are identical.
2.78 +
2.79 +Because of its pattern-matching syntax, \isacommand{fun} is also useful
2.80 +for the definition of non-recursive functions:%
2.81 +\end{isamarkuptext}%
2.82 +\isamarkuptrue%
2.83 +\isacommand{fun}\isamarkupfalse%
2.84 +\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.85 +\ \ {\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.86 +\ \ {\isachardoublequoteopen}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequoteclose}%
2.87 +\begin{isamarkuptext}%
2.88 +After a function~$f$ has been defined via \isacommand{fun},
2.89 +its defining equations (or variants derived from them) are available
2.90 +under the name $f$\isa{{\isachardot}simps} as theorems.
2.91 +For example, look (via \isacommand{thm}) at
2.92 +\isa{sep{\isachardot}simps} and \isa{sep{\isadigit{1}}{\isachardot}simps} to see that they define
2.93 +the same function. What is more, those equations are automatically declared as
2.94 +simplification rules.
2.95 +
2.96 +\subsection{Termination}
2.97 +
2.98 +Isabelle's automatic termination prover for \isacommand{fun} has a
2.99 +fixed notion of the \emph{size} (of type \isa{nat}) of an
2.100 +argument. The size of a natural number is the number itself. The size
2.101 +of a list is its length. In general, every datatype \isa{t} comes
2.102 +with its own size function (named \isa{t{\isachardot}size}) which counts the
2.103 +number of constructors in a term of type \isa{t} --- more precisely
2.104 +those constructors where one of the arguments is of the type itself:
2.105 +\isa{Suc} in the case of \isa{nat} and \isa{op\ {\isacharhash}} in the case
2.106 +of lists. A recursive function is accepted if \isacommand{fun} can
2.107 +show that the size of one fixed argument becomes smaller with each
2.108 +recursive call.
2.109 +
2.110 +More generally, \isa{fun} allows any \emph{lexicographic
2.111 +combination} of size measures in case there are multiple
2.112 +arguments. For example the following version of \rmindex{Ackermann's
2.113 +function} is accepted:%
2.114 +\end{isamarkuptext}%
2.115 +\isamarkuptrue%
2.116 +\isacommand{fun}\isamarkupfalse%
2.117 +\ ack{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.118 +\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isacharequal}\ Suc\ n{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.119 +\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.120 +\ \ {\isachardoublequoteopen}ack{\isadigit{2}}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ ack{\isadigit{2}}\ {\isacharparenleft}ack{\isadigit{2}}\ n\ {\isacharparenleft}Suc\ m{\isacharparenright}{\isacharparenright}\ m{\isachardoublequoteclose}%
2.121 +\begin{isamarkuptext}%
2.122 +Thus the order of arguments has no influence on whether
2.123 +\isacommand{fun} can prove termination of a function. For more details
2.124 +see elsewhere~\cite{bulwahnKN07}.
2.125 +
2.126 +\subsection{Simplification}
2.127 +\label{sec:fun-simplification}
2.128 +
2.129 +Upon successful termination proof, the recursion equations become
2.130 +simplification rules, just as with \isacommand{primrec}.
2.131 +In most cases this works fine, but there is a subtle
2.132 +problem that must be mentioned: simplification may not
2.133 +terminate because of automatic splitting of \isa{if}.
2.134 +\index{*if expressions!splitting of}
2.135 +Let us look at an example:%
2.136 +\end{isamarkuptext}%
2.137 +\isamarkuptrue%
2.138 +\isacommand{fun}\isamarkupfalse%
2.139 +\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.140 +\ \ {\isachardoublequoteopen}gcd{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
2.141 +\begin{isamarkuptext}%
2.142 +\noindent
2.143 +The second argument decreases with each recursive call.
2.144 +The termination condition
2.145 +\begin{isabelle}%
2.146 +\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
2.147 +\end{isabelle}
2.148 +is proved automatically because it is already present as a lemma in
2.149 +HOL\@. Thus the recursion equation becomes a simplification
2.150 +rule. Of course the equation is nonterminating if we are allowed to unfold
2.151 +the recursive call inside the \isa{else} branch, which is why programming
2.152 +languages and our simplifier don't do that. Unfortunately the simplifier does
2.153 +something else that leads to the same problem: it splits
2.154 +each \isa{if}-expression unless its
2.155 +condition simplifies to \isa{True} or \isa{False}. For
2.156 +example, simplification reduces
2.157 +\begin{isabelle}%
2.158 +\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
2.159 +\end{isabelle}
2.160 +in one step to
2.161 +\begin{isabelle}%
2.162 +\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
2.163 +\end{isabelle}
2.164 +where the condition cannot be reduced further, and splitting leads to
2.165 +\begin{isabelle}%
2.166 +\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
2.167 +\end{isabelle}
2.168 +Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
2.169 +an \isa{if}, it is unfolded again, which leads to an infinite chain of
2.170 +simplification steps. Fortunately, this problem can be avoided in many
2.171 +different ways.
2.172 +
2.173 +The most radical solution is to disable the offending theorem
2.174 +\isa{split{\isacharunderscore}if},
2.175 +as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
2.176 +approach: you will often have to invoke the rule explicitly when
2.177 +\isa{if} is involved.
2.178 +
2.179 +If possible, the definition should be given by pattern matching on the left
2.180 +rather than \isa{if} on the right. In the case of \isa{gcd} the
2.181 +following alternative definition suggests itself:%
2.182 +\end{isamarkuptext}%
2.183 +\isamarkuptrue%
2.184 +\isacommand{fun}\isamarkupfalse%
2.185 +\ gcd{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.186 +\ \ {\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
2.187 +\ \ {\isachardoublequoteopen}gcd{\isadigit{1}}\ m\ n\ {\isacharequal}\ gcd{\isadigit{1}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}%
2.188 +\begin{isamarkuptext}%
2.189 +\noindent
2.190 +The order of equations is important: it hides the side condition
2.191 +\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}. Unfortunately, in general the case distinction
2.192 +may not be expressible by pattern matching.
2.193 +
2.194 +A simple alternative is to replace \isa{if} by \isa{case},
2.195 +which is also available for \isa{bool} and is not split automatically:%
2.196 +\end{isamarkuptext}%
2.197 +\isamarkuptrue%
2.198 +\isacommand{fun}\isamarkupfalse%
2.199 +\ gcd{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
2.200 +\ \ {\isachardoublequoteopen}gcd{\isadigit{2}}\ m\ n\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}{\isadigit{0}}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd{\isadigit{2}}\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
2.201 +\begin{isamarkuptext}%
2.202 +\noindent
2.203 +This is probably the neatest solution next to pattern matching, and it is
2.204 +always available.
2.205 +
2.206 +A final alternative is to replace the offending simplification rules by
2.207 +derived conditional ones. For \isa{gcd} it means we have to prove
2.208 +these lemmas:%
2.209 +\end{isamarkuptext}%
2.210 +\isamarkuptrue%
2.211 +\isacommand{lemma}\isamarkupfalse%
2.212 +\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}gcd{\isacharparenleft}m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
2.213 +%
2.214 +\isadelimproof
2.215 +%
2.216 +\endisadelimproof
2.217 +%
2.218 +\isatagproof
2.219 +\isacommand{apply}\isamarkupfalse%
2.220 +{\isacharparenleft}simp{\isacharparenright}\isanewline
2.221 +\isacommand{done}\isamarkupfalse%
2.222 +%
2.223 +\endisatagproof
2.224 +{\isafoldproof}%
2.225 +%
2.226 +\isadelimproof
2.227 +\isanewline
2.228 +%
2.229 +\endisadelimproof
2.230 +\isanewline
2.231 +\isacommand{lemma}\isamarkupfalse%
2.232 +\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.233 +%
2.234 +\isadelimproof
2.235 +%
2.236 +\endisadelimproof
2.237 +%
2.238 +\isatagproof
2.239 +\isacommand{apply}\isamarkupfalse%
2.240 +{\isacharparenleft}simp{\isacharparenright}\isanewline
2.241 +\isacommand{done}\isamarkupfalse%
2.242 +%
2.243 +\endisatagproof
2.244 +{\isafoldproof}%
2.245 +%
2.246 +\isadelimproof
2.247 +%
2.248 +\endisadelimproof
2.249 +%
2.250 +\begin{isamarkuptext}%
2.251 +\noindent
2.252 +Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}.
2.253 +Now we can disable the original simplification rule:%
2.254 +\end{isamarkuptext}%
2.255 +\isamarkuptrue%
2.256 +\isacommand{declare}\isamarkupfalse%
2.257 +\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
2.258 +\begin{isamarkuptext}%
2.259 +\index{induction!recursion|(}
2.260 +\index{recursion induction|(}
2.261 +
2.262 +\subsection{Induction}
2.263 +\label{sec:fun-induction}
2.264 +
2.265 +Having defined a function we might like to prove something about it.
2.266 +Since the function is recursive, the natural proof principle is
2.267 +again induction. But this time the structural form of induction that comes
2.268 +with datatypes is unlikely to work well --- otherwise we could have defined the
2.269 +function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
2.270 +proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the
2.271 +recursion pattern of the particular function $f$. We call this
2.272 +\textbf{recursion induction}. Roughly speaking, it
2.273 +requires you to prove for each \isacommand{fun} equation that the property
2.274 +you are trying to establish holds for the left-hand side provided it holds
2.275 +for all recursive calls on the right-hand side. Here is a simple example
2.276 +involving the predefined \isa{map} functional on lists:%
2.277 +\end{isamarkuptext}%
2.278 +\isamarkuptrue%
2.279 +\isacommand{lemma}\isamarkupfalse%
2.280 +\ {\isachardoublequoteopen}map\ f\ {\isacharparenleft}sep\ x\ xs{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharparenleft}map\ f\ xs{\isacharparenright}{\isachardoublequoteclose}%
2.281 +\isadelimproof
2.282 +%
2.283 +\endisadelimproof
2.284 +%
2.285 +\isatagproof
2.286 +%
2.287 +\begin{isamarkuptxt}%
2.288 +\noindent
2.289 +Note that \isa{map\ f\ xs}
2.290 +is the result of applying \isa{f} to all elements of \isa{xs}. We prove
2.291 +this lemma by recursion induction over \isa{sep}:%
2.292 +\end{isamarkuptxt}%
2.293 +\isamarkuptrue%
2.294 +\isacommand{apply}\isamarkupfalse%
2.295 +{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
2.296 +\begin{isamarkuptxt}%
2.297 +\noindent
2.298 +The resulting proof state has three subgoals corresponding to the three
2.299 +clauses for \isa{sep}:
2.300 +\begin{isabelle}%
2.301 +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
2.302 +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ x{\isachardot}\ map\ f\ {\isacharparenleft}sep\ a\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\isanewline
2.303 +\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}a\ x\ y\ zs{\isachardot}\isanewline
2.304 +\isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
2.305 +\isaindent{\ {\isadigit{3}}{\isachardot}\ \ \ \ }map\ f\ {\isacharparenleft}sep\ a\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}map\ f\ {\isacharparenleft}x\ {\isacharhash}\ y\ {\isacharhash}\ zs{\isacharparenright}{\isacharparenright}%
2.306 +\end{isabelle}
2.307 +The rest is pure simplification:%
2.308 +\end{isamarkuptxt}%
2.309 +\isamarkuptrue%
2.310 +\isacommand{apply}\isamarkupfalse%
2.311 +\ simp{\isacharunderscore}all\isanewline
2.312 +\isacommand{done}\isamarkupfalse%
2.313 +%
2.314 +\endisatagproof
2.315 +{\isafoldproof}%
2.316 +%
2.317 +\isadelimproof
2.318 +%
2.319 +\endisadelimproof
2.320 +%
2.321 +\begin{isamarkuptext}%
2.322 +Try proving the above lemma by structural induction, and you find that you
2.323 +need an additional case distinction.
2.324 +
2.325 +In general, the format of invoking recursion induction is
2.326 +\begin{quote}
2.327 +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
2.328 +\end{quote}\index{*induct_tac (method)}%
2.329 +where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
2.330 +name of a function that takes an $n$-tuple. Usually the subgoal will
2.331 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
2.332 +induction rules do not mention $f$ at all. Here is \isa{sep{\isachardot}induct}:
2.333 +\begin{isabelle}
2.334 +{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
2.335 +~~{\isasymAnd}a~x.~P~a~[x];\isanewline
2.336 +~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
2.337 +{\isasymLongrightarrow}~P~u~v%
2.338 +\end{isabelle}
2.339 +It merely says that in order to prove a property \isa{P} of \isa{u} and
2.340 +\isa{v} you need to prove it for the three cases where \isa{v} is the
2.341 +empty list, the singleton list, and the list with at least two elements.
2.342 +The final case has an induction hypothesis: you may assume that \isa{P}
2.343 +holds for the tail of that list.
2.344 +\index{induction!recursion|)}
2.345 +\index{recursion induction|)}%
2.346 +\end{isamarkuptext}%
2.347 +\isamarkuptrue%
2.348 +%
2.349 +\isadelimtheory
2.350 +%
2.351 +\endisadelimtheory
2.352 +%
2.353 +\isatagtheory
2.354 +%
2.355 +\endisatagtheory
2.356 +{\isafoldtheory}%
2.357 +%
2.358 +\isadelimtheory
2.359 +%
2.360 +\endisadelimtheory
2.361 +\end{isabellebody}%
2.362 +%%% Local Variables:
2.363 +%%% mode: latex
2.364 +%%% TeX-master: "root"
2.365 +%%% End:
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 08:26:01 2007 +0100
3.3 @@ -0,0 +1,264 @@
3.4 +(*<*)
3.5 +theory fun0 imports Main begin
3.6 +(*>*)
3.7 +
3.8 +text{*
3.9 +\subsection{Definition}
3.10 +\label{sec:fun-examples}
3.11 +
3.12 +Here is a simple example, the \rmindex{Fibonacci function}:
3.13 +*}
3.14 +
3.15 +fun fib :: "nat \<Rightarrow> nat" where
3.16 + "fib 0 = 0" |
3.17 + "fib (Suc 0) = 1" |
3.18 + "fib (Suc(Suc x)) = fib x + fib (Suc x)"
3.19 +
3.20 +text{*\noindent
3.21 +This resembles ordinary functional programming languages. Note the obligatory
3.22 +\isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
3.23 +defines the function in one go. Isabelle establishes termination automatically
3.24 +because @{const fib}'s argument decreases in every recursive call.
3.25 +
3.26 +Slightly more interesting is the insertion of a fixed element
3.27 +between any two elements of a list:
3.28 +*}
3.29 +
3.30 +fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
3.31 + "sep a [] = []" |
3.32 + "sep a [x] = [x]" |
3.33 + "sep a (x#y#zs) = x # a # sep a (y#zs)";
3.34 +
3.35 +text{*\noindent
3.36 +This time the length of the list decreases with the
3.37 +recursive call; the first argument is irrelevant for termination.
3.38 +
3.39 +Pattern matching\index{pattern matching!and \isacommand{fun}}
3.40 +need not be exhaustive and may employ wildcards:
3.41 +*}
3.42 +
3.43 +fun last :: "'a list \<Rightarrow> 'a" where
3.44 + "last [x] = x" |
3.45 + "last (_#y#zs) = last (y#zs)"
3.46 +
3.47 +text{*
3.48 +Overlapping patterns are disambiguated by taking the order of equations into
3.49 +account, just as in functional programming:
3.50 +*}
3.51 +
3.52 +fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
3.53 + "sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
3.54 + "sep1 _ xs = xs"
3.55 +
3.56 +text{*\noindent
3.57 +To guarantee that the second equation can only be applied if the first
3.58 +one does not match, Isabelle internally replaces the second equation
3.59 +by the two possibilities that are left: @{prop"sep1 a [] = []"} and
3.60 +@{prop"sep1 a [x] = [x]"}. Thus the functions @{const sep} and
3.61 +@{const sep1} are identical.
3.62 +
3.63 +Because of its pattern-matching syntax, \isacommand{fun} is also useful
3.64 +for the definition of non-recursive functions:
3.65 +*}
3.66 +
3.67 +fun swap12 :: "'a list \<Rightarrow> 'a list" where
3.68 + "swap12 (x#y#zs) = y#x#zs" |
3.69 + "swap12 zs = zs"
3.70 +
3.71 +text{*
3.72 +After a function~$f$ has been defined via \isacommand{fun},
3.73 +its defining equations (or variants derived from them) are available
3.74 +under the name $f$@{text".simps"} as theorems.
3.75 +For example, look (via \isacommand{thm}) at
3.76 +@{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
3.77 +the same function. What is more, those equations are automatically declared as
3.78 +simplification rules.
3.79 +
3.80 +\subsection{Termination}
3.81 +
3.82 +Isabelle's automatic termination prover for \isacommand{fun} has a
3.83 +fixed notion of the \emph{size} (of type @{typ nat}) of an
3.84 +argument. The size of a natural number is the number itself. The size
3.85 +of a list is its length. In general, every datatype @{text t} comes
3.86 +with its own size function (named @{text"t.size"}) which counts the
3.87 +number of constructors in a term of type @{text t} --- more precisely
3.88 +those constructors where one of the arguments is of the type itself:
3.89 +@{const Suc} in the case of @{typ nat} and @{const "op #"} in the case
3.90 +of lists. A recursive function is accepted if \isacommand{fun} can
3.91 +show that the size of one fixed argument becomes smaller with each
3.92 +recursive call.
3.93 +
3.94 +More generally, @{text fun} allows any \emph{lexicographic
3.95 +combination} of size measures in case there are multiple
3.96 +arguments. For example the following version of \rmindex{Ackermann's
3.97 +function} is accepted: *}
3.98 +
3.99 +fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
3.100 + "ack2 n 0 = Suc n" |
3.101 + "ack2 0 (Suc m) = ack2 (Suc 0) m" |
3.102 + "ack2 (Suc n) (Suc m) = ack2 (ack2 n (Suc m)) m"
3.103 +
3.104 +text{* Thus the order of arguments has no influence on whether
3.105 +\isacommand{fun} can prove termination of a function. For more details
3.106 +see elsewhere~\cite{bulwahnKN07}.
3.107 +
3.108 +\subsection{Simplification}
3.109 +\label{sec:fun-simplification}
3.110 +
3.111 +Upon successful termination proof, the recursion equations become
3.112 +simplification rules, just as with \isacommand{primrec}.
3.113 +In most cases this works fine, but there is a subtle
3.114 +problem that must be mentioned: simplification may not
3.115 +terminate because of automatic splitting of @{text "if"}.
3.116 +\index{*if expressions!splitting of}
3.117 +Let us look at an example:
3.118 +*}
3.119 +
3.120 +fun gcd :: "nat \<times> nat \<Rightarrow> nat" where
3.121 + "gcd(m,n) = (if n=0 then m else gcd(n, m mod n))"
3.122 +
3.123 +text{*\noindent
3.124 +The second argument decreases with each recursive call.
3.125 +The termination condition
3.126 +@{prop[display]"n ~= (0::nat) ==> m mod n < n"}
3.127 +is proved automatically because it is already present as a lemma in
3.128 +HOL\@. Thus the recursion equation becomes a simplification
3.129 +rule. Of course the equation is nonterminating if we are allowed to unfold
3.130 +the recursive call inside the @{text else} branch, which is why programming
3.131 +languages and our simplifier don't do that. Unfortunately the simplifier does
3.132 +something else that leads to the same problem: it splits
3.133 +each @{text "if"}-expression unless its
3.134 +condition simplifies to @{term True} or @{term False}. For
3.135 +example, simplification reduces
3.136 +@{prop[display]"gcd(m,n) = k"}
3.137 +in one step to
3.138 +@{prop[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
3.139 +where the condition cannot be reduced further, and splitting leads to
3.140 +@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
3.141 +Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
3.142 +an @{text "if"}, it is unfolded again, which leads to an infinite chain of
3.143 +simplification steps. Fortunately, this problem can be avoided in many
3.144 +different ways.
3.145 +
3.146 +The most radical solution is to disable the offending theorem
3.147 +@{thm[source]split_if},
3.148 +as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
3.149 +approach: you will often have to invoke the rule explicitly when
3.150 +@{text "if"} is involved.
3.151 +
3.152 +If possible, the definition should be given by pattern matching on the left
3.153 +rather than @{text "if"} on the right. In the case of @{term gcd} the
3.154 +following alternative definition suggests itself:
3.155 +*}
3.156 +
3.157 +fun gcd1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
3.158 + "gcd1 m 0 = m" |
3.159 + "gcd1 m n = gcd1 n (m mod n)"
3.160 +
3.161 +text{*\noindent
3.162 +The order of equations is important: it hides the side condition
3.163 +@{prop"n ~= (0::nat)"}. Unfortunately, in general the case distinction
3.164 +may not be expressible by pattern matching.
3.165 +
3.166 +A simple alternative is to replace @{text "if"} by @{text case},
3.167 +which is also available for @{typ bool} and is not split automatically:
3.168 +*}
3.169 +
3.170 +fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
3.171 + "gcd2 m n = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2 n (m mod n))"
3.172 +
3.173 +text{*\noindent
3.174 +This is probably the neatest solution next to pattern matching, and it is
3.175 +always available.
3.176 +
3.177 +A final alternative is to replace the offending simplification rules by
3.178 +derived conditional ones. For @{term gcd} it means we have to prove
3.179 +these lemmas:
3.180 +*}
3.181 +
3.182 +lemma [simp]: "gcd(m,0) = m"
3.183 +apply(simp)
3.184 +done
3.185 +
3.186 +lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m,n) = gcd(n, m mod n)"
3.187 +apply(simp)
3.188 +done
3.189 +
3.190 +text{*\noindent
3.191 +Simplification terminates for these proofs because the condition of the @{text
3.192 +"if"} simplifies to @{term True} or @{term False}.
3.193 +Now we can disable the original simplification rule:
3.194 +*}
3.195 +
3.196 +declare gcd.simps [simp del]
3.197 +
3.198 +text{*
3.199 +\index{induction!recursion|(}
3.200 +\index{recursion induction|(}
3.201 +
3.202 +\subsection{Induction}
3.203 +\label{sec:fun-induction}
3.204 +
3.205 +Having defined a function we might like to prove something about it.
3.206 +Since the function is recursive, the natural proof principle is
3.207 +again induction. But this time the structural form of induction that comes
3.208 +with datatypes is unlikely to work well --- otherwise we could have defined the
3.209 +function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
3.210 +proves a suitable induction rule $f$@{text".induct"} that follows the
3.211 +recursion pattern of the particular function $f$. We call this
3.212 +\textbf{recursion induction}. Roughly speaking, it
3.213 +requires you to prove for each \isacommand{fun} equation that the property
3.214 +you are trying to establish holds for the left-hand side provided it holds
3.215 +for all recursive calls on the right-hand side. Here is a simple example
3.216 +involving the predefined @{term"map"} functional on lists:
3.217 +*}
3.218 +
3.219 +lemma "map f (sep x xs) = sep (f x) (map f xs)"
3.220 +
3.221 +txt{*\noindent
3.222 +Note that @{term"map f xs"}
3.223 +is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
3.224 +this lemma by recursion induction over @{term"sep"}:
3.225 +*}
3.226 +
3.227 +apply(induct_tac x xs rule: sep.induct);
3.228 +
3.229 +txt{*\noindent
3.230 +The resulting proof state has three subgoals corresponding to the three
3.231 +clauses for @{term"sep"}:
3.232 +@{subgoals[display,indent=0]}
3.233 +The rest is pure simplification:
3.234 +*}
3.235 +
3.236 +apply simp_all;
3.237 +done
3.238 +
3.239 +text{*
3.240 +Try proving the above lemma by structural induction, and you find that you
3.241 +need an additional case distinction.
3.242 +
3.243 +In general, the format of invoking recursion induction is
3.244 +\begin{quote}
3.245 +\isacommand{apply}@{text"(induct_tac"} $x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
3.246 +\end{quote}\index{*induct_tac (method)}%
3.247 +where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
3.248 +name of a function that takes an $n$-tuple. Usually the subgoal will
3.249 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
3.250 +induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
3.251 +\begin{isabelle}
3.252 +{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
3.253 +~~{\isasymAnd}a~x.~P~a~[x];\isanewline
3.254 +~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
3.255 +{\isasymLongrightarrow}~P~u~v%
3.256 +\end{isabelle}
3.257 +It merely says that in order to prove a property @{term"P"} of @{term"u"} and
3.258 +@{term"v"} you need to prove it for the three cases where @{term"v"} is the
3.259 +empty list, the singleton list, and the list with at least two elements.
3.260 +The final case has an induction hypothesis: you may assume that @{term"P"}
3.261 +holds for the tail of that list.
3.262 +\index{induction!recursion|)}
3.263 +\index{recursion induction|)}
3.264 +*}
3.265 +(*<*)
3.266 +end
3.267 +(*>*)