1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{examples}% |
3 \def\isabellecontext{examples}% |
4 % |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 Here is a simple example, the Fibonacci function:% |
6 Here is a simple example, the \rmindex{Fibonacci function}:% |
7 \end{isamarkuptext}% |
7 \end{isamarkuptext}% |
8 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
8 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
9 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
9 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
10 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
10 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
11 \ \ {\isachardoublequote}fib\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
11 \ \ {\isachardoublequote}fib\ {\isadigit{1}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
12 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}% |
12 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}% |
13 \begin{isamarkuptext}% |
13 \begin{isamarkuptext}% |
14 \noindent |
14 \noindent |
15 The definition of \isa{fib} is accompanied by a \bfindex{measure function} |
15 \index{measure functions}% |
|
16 The definition of \isa{fib} is accompanied by a \textbf{measure function} |
16 \isa{{\isasymlambda}n{\isachardot}\ n} which maps the argument of \isa{fib} to a |
17 \isa{{\isasymlambda}n{\isachardot}\ n} which maps the argument of \isa{fib} to a |
17 natural number. The requirement is that in each equation the measure of the |
18 natural number. The requirement is that in each equation the measure of the |
18 argument on the left-hand side is strictly greater than the measure of the |
19 argument on the left-hand side is strictly greater than the measure of the |
19 argument of each recursive call. In the case of \isa{fib} this is |
20 argument of each recursive call. In the case of \isa{fib} this is |
20 obviously true because the measure function is the identity and |
21 obviously true because the measure function is the identity and |
34 This time the measure is the length of the list, which decreases with the |
35 This time the measure is the length of the list, which decreases with the |
35 recursive call; the first component of the argument tuple is irrelevant. |
36 recursive call; the first component of the argument tuple is irrelevant. |
36 The details of tupled $\lambda$-abstractions \isa{{\isasymlambda}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlsub n{\isacharparenright}} are |
37 The details of tupled $\lambda$-abstractions \isa{{\isasymlambda}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}{\isasymdots}{\isacharcomma}x\isactrlsub n{\isacharparenright}} are |
37 explained in \S\ref{sec:products}, but for now your intuition is all you need. |
38 explained in \S\ref{sec:products}, but for now your intuition is all you need. |
38 |
39 |
39 Pattern matching need not be exhaustive:% |
40 Pattern matching\index{pattern matching!and \isacommand{recdef}} |
|
41 need not be exhaustive:% |
40 \end{isamarkuptext}% |
42 \end{isamarkuptext}% |
41 \isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
43 \isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
42 \isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
44 \isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
43 \ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline |
45 \ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline |
44 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}% |
46 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}% |