1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{examples}% |
3 \def\isabellecontext{examples}% |
4 \isamarkupfalse% |
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 \isamarkuptrue% |
5 % |
18 % |
6 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
7 Here is a simple example, the \rmindex{Fibonacci function}:% |
20 Here is a simple example, the \rmindex{Fibonacci function}:% |
8 \end{isamarkuptext}% |
21 \end{isamarkuptext}% |
9 \isamarkuptrue% |
22 \isamarkupfalse% |
10 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
23 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
11 \isamarkupfalse% |
24 \isamarkupfalse% |
12 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
25 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline |
13 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
26 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
14 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
27 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline |
15 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
28 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
16 % |
29 % |
17 \begin{isamarkuptext}% |
30 \begin{isamarkuptext}% |
18 \noindent |
31 \noindent |
19 \index{measure functions}% |
32 \index{measure functions}% |
20 The definition of \isa{fib} is accompanied by a \textbf{measure function} |
33 The definition of \isa{fib} is accompanied by a \textbf{measure function} |
27 \isa{Suc\ x}. |
40 \isa{Suc\ x}. |
28 |
41 |
29 Slightly more interesting is the insertion of a fixed element |
42 Slightly more interesting is the insertion of a fixed element |
30 between any two elements of a list:% |
43 between any two elements of a list:% |
31 \end{isamarkuptext}% |
44 \end{isamarkuptext}% |
32 \isamarkuptrue% |
45 \isamarkupfalse% |
33 \isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
46 \isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
34 \isamarkupfalse% |
47 \isamarkupfalse% |
35 \isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
48 \isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
36 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
49 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
37 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline |
50 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline |
38 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
51 \ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
39 % |
52 % |
40 \begin{isamarkuptext}% |
53 \begin{isamarkuptext}% |
41 \noindent |
54 \noindent |
42 This time the measure is the length of the list, which decreases with the |
55 This time the measure is the length of the list, which decreases with the |
43 recursive call; the first component of the argument tuple is irrelevant. |
56 recursive call; the first component of the argument tuple is irrelevant. |
45 explained in \S\ref{sec:products}, but for now your intuition is all you need. |
58 explained in \S\ref{sec:products}, but for now your intuition is all you need. |
46 |
59 |
47 Pattern matching\index{pattern matching!and \isacommand{recdef}} |
60 Pattern matching\index{pattern matching!and \isacommand{recdef}} |
48 need not be exhaustive:% |
61 need not be exhaustive:% |
49 \end{isamarkuptext}% |
62 \end{isamarkuptext}% |
50 \isamarkuptrue% |
63 \isamarkupfalse% |
51 \isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
64 \isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline |
52 \isamarkupfalse% |
65 \isamarkupfalse% |
53 \isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
66 \isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
54 \ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline |
67 \ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline |
55 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
68 \ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
56 % |
69 % |
57 \begin{isamarkuptext}% |
70 \begin{isamarkuptext}% |
58 Overlapping patterns are disambiguated by taking the order of equations into |
71 Overlapping patterns are disambiguated by taking the order of equations into |
59 account, just as in functional programming:% |
72 account, just as in functional programming:% |
60 \end{isamarkuptext}% |
73 \end{isamarkuptext}% |
61 \isamarkuptrue% |
74 \isamarkupfalse% |
62 \isacommand{consts}\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
75 \isacommand{consts}\ sep{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
63 \isamarkupfalse% |
76 \isamarkupfalse% |
64 \isacommand{recdef}\ sep{\isadigit{1}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
77 \isacommand{recdef}\ sep{\isadigit{1}}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline |
65 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline |
78 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline |
66 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}\isamarkupfalse% |
79 \ \ {\isachardoublequote}sep{\isadigit{1}}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}\isamarkuptrue% |
67 % |
80 % |
68 \begin{isamarkuptext}% |
81 \begin{isamarkuptext}% |
69 \noindent |
82 \noindent |
70 To guarantee that the second equation can only be applied if the first |
83 To guarantee that the second equation can only be applied if the first |
71 one does not match, Isabelle internally replaces the second equation |
84 one does not match, Isabelle internally replaces the second equation |
80 therefore have to combine several arguments into a tuple. In case only one |
93 therefore have to combine several arguments into a tuple. In case only one |
81 argument is relevant for termination, you can also rearrange the order of |
94 argument is relevant for termination, you can also rearrange the order of |
82 arguments as in the following definition: |
95 arguments as in the following definition: |
83 \end{warn}% |
96 \end{warn}% |
84 \end{isamarkuptext}% |
97 \end{isamarkuptext}% |
85 \isamarkuptrue% |
98 \isamarkupfalse% |
86 \isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
99 \isacommand{consts}\ sep{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
87 \isamarkupfalse% |
100 \isamarkupfalse% |
88 \isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
101 \isacommand{recdef}\ sep{\isadigit{2}}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline |
89 \ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ a{\isacharparenright}{\isachardoublequote}\isanewline |
102 \ \ {\isachardoublequote}sep{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isadigit{2}}\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ a{\isacharparenright}{\isachardoublequote}\isanewline |
90 \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
103 \ \ {\isachardoublequote}sep{\isadigit{2}}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
91 % |
104 % |
92 \begin{isamarkuptext}% |
105 \begin{isamarkuptext}% |
93 Because of its pattern-matching syntax, \isacommand{recdef} is also useful |
106 Because of its pattern-matching syntax, \isacommand{recdef} is also useful |
94 for the definition of non-recursive functions, where the termination measure |
107 for the definition of non-recursive functions, where the termination measure |
95 degenerates to the empty set \isa{{\isacharbraceleft}{\isacharbraceright}}:% |
108 degenerates to the empty set \isa{{\isacharbraceleft}{\isacharbraceright}}:% |
96 \end{isamarkuptext}% |
109 \end{isamarkuptext}% |
97 \isamarkuptrue% |
110 \isamarkupfalse% |
98 \isacommand{consts}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
111 \isacommand{consts}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline |
99 \isamarkupfalse% |
112 \isamarkupfalse% |
100 \isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline |
113 \isacommand{recdef}\ swap{\isadigit{1}}{\isadigit{2}}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline |
101 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline |
114 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline |
102 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}\isanewline |
115 \ \ {\isachardoublequote}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}\isanewline |
103 \isamarkupfalse% |
116 % |
104 \isamarkupfalse% |
117 \isadelimtheory |
|
118 % |
|
119 \endisadelimtheory |
|
120 % |
|
121 \isatagtheory |
|
122 % |
|
123 \endisatagtheory |
|
124 {\isafoldtheory}% |
|
125 % |
|
126 \isadelimtheory |
|
127 % |
|
128 \endisadelimtheory |
105 \end{isabellebody}% |
129 \end{isabellebody}% |
106 %%% Local Variables: |
130 %%% Local Variables: |
107 %%% mode: latex |
131 %%% mode: latex |
108 %%% TeX-master: "root" |
132 %%% TeX-master: "root" |
109 %%% End: |
133 %%% End: |