25260
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{fun{\isadigit{0}}}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
|
17 |
%
|
|
18 |
\begin{isamarkuptext}%
|
|
19 |
\subsection{Definition}
|
|
20 |
\label{sec:fun-examples}
|
|
21 |
|
|
22 |
Here is a simple example, the \rmindex{Fibonacci function}:%
|
|
23 |
\end{isamarkuptext}%
|
|
24 |
\isamarkuptrue%
|
|
25 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
26 |
\ fib\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
27 |
{\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
28 |
{\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
29 |
{\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fib\ x\ {\isaliteral{2B}{\isacharplus}}\ fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
30 |
\begin{isamarkuptext}%
|
|
31 |
\noindent
|
|
32 |
This resembles ordinary functional programming languages. Note the obligatory
|
|
33 |
\isacommand{where} and \isa{|}. Command \isacommand{fun} declares and
|
|
34 |
defines the function in one go. Isabelle establishes termination automatically
|
|
35 |
because \isa{fib}'s argument decreases in every recursive call.
|
|
36 |
|
|
37 |
Slightly more interesting is the insertion of a fixed element
|
|
38 |
between any two elements of a list:%
|
|
39 |
\end{isamarkuptext}%
|
|
40 |
\isamarkuptrue%
|
|
41 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
42 |
\ sep\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
43 |
{\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
44 |
{\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
45 |
{\isaliteral{22}{\isachardoublequoteopen}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ sep\ a\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
46 |
\begin{isamarkuptext}%
|
|
47 |
\noindent
|
|
48 |
This time the length of the list decreases with the
|
|
49 |
recursive call; the first argument is irrelevant for termination.
|
|
50 |
|
|
51 |
Pattern matching\index{pattern matching!and \isacommand{fun}}
|
|
52 |
need not be exhaustive and may employ wildcards:%
|
|
53 |
\end{isamarkuptext}%
|
|
54 |
\isamarkuptrue%
|
|
55 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
56 |
\ last\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
57 |
{\isaliteral{22}{\isachardoublequoteopen}}last\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
58 |
{\isaliteral{22}{\isachardoublequoteopen}}last\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ last\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
59 |
\begin{isamarkuptext}%
|
|
60 |
Overlapping patterns are disambiguated by taking the order of equations into
|
|
61 |
account, just as in functional programming:%
|
|
62 |
\end{isamarkuptext}%
|
|
63 |
\isamarkuptrue%
|
|
64 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
65 |
\ sep{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
66 |
{\isaliteral{22}{\isachardoublequoteopen}}sep{\isadigit{1}}\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{23}{\isacharhash}}\ a\ {\isaliteral{23}{\isacharhash}}\ sep{\isadigit{1}}\ a\ {\isaliteral{28}{\isacharparenleft}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
67 |
{\isaliteral{22}{\isachardoublequoteopen}}sep{\isadigit{1}}\ {\isaliteral{5F}{\isacharunderscore}}\ xs\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
68 |
\begin{isamarkuptext}%
|
|
69 |
\noindent
|
|
70 |
To guarantee that the second equation can only be applied if the first
|
|
71 |
one does not match, Isabelle internally replaces the second equation
|
40406
|
72 |
by the two possibilities that are left: \isa{sep{\isadigit{1}}\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and
|
|
73 |
\isa{sep{\isadigit{1}}\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}. Thus the functions \isa{sep} and
|
25260
|
74 |
\isa{sep{\isadigit{1}}} are identical.
|
|
75 |
|
25263
|
76 |
Because of its pattern matching syntax, \isacommand{fun} is also useful
|
25260
|
77 |
for the definition of non-recursive functions:%
|
|
78 |
\end{isamarkuptext}%
|
|
79 |
\isamarkuptrue%
|
|
80 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
81 |
\ swap{\isadigit{1}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
82 |
{\isaliteral{22}{\isachardoublequoteopen}}swap{\isadigit{1}}{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}y{\isaliteral{23}{\isacharhash}}zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{23}{\isacharhash}}x{\isaliteral{23}{\isacharhash}}zs{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
83 |
{\isaliteral{22}{\isachardoublequoteopen}}swap{\isadigit{1}}{\isadigit{2}}\ zs\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ zs{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
84 |
\begin{isamarkuptext}%
|
|
85 |
After a function~$f$ has been defined via \isacommand{fun},
|
|
86 |
its defining equations (or variants derived from them) are available
|
40406
|
87 |
under the name $f$\isa{{\isaliteral{2E}{\isachardot}}simps} as theorems.
|
25260
|
88 |
For example, look (via \isacommand{thm}) at
|
40406
|
89 |
\isa{sep{\isaliteral{2E}{\isachardot}}simps} and \isa{sep{\isadigit{1}}{\isaliteral{2E}{\isachardot}}simps} to see that they define
|
25260
|
90 |
the same function. What is more, those equations are automatically declared as
|
|
91 |
simplification rules.
|
|
92 |
|
|
93 |
\subsection{Termination}
|
|
94 |
|
|
95 |
Isabelle's automatic termination prover for \isacommand{fun} has a
|
|
96 |
fixed notion of the \emph{size} (of type \isa{nat}) of an
|
|
97 |
argument. The size of a natural number is the number itself. The size
|
25339
|
98 |
of a list is its length. For the general case see \S\ref{sec:general-datatype}.
|
|
99 |
A recursive function is accepted if \isacommand{fun} can
|
25260
|
100 |
show that the size of one fixed argument becomes smaller with each
|
|
101 |
recursive call.
|
|
102 |
|
25261
|
103 |
More generally, \isacommand{fun} allows any \emph{lexicographic
|
25260
|
104 |
combination} of size measures in case there are multiple
|
25261
|
105 |
arguments. For example, the following version of \rmindex{Ackermann's
|
25260
|
106 |
function} is accepted:%
|
|
107 |
\end{isamarkuptext}%
|
|
108 |
\isamarkuptrue%
|
|
109 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
110 |
\ ack{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
111 |
{\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ n\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
112 |
{\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
113 |
{\isaliteral{22}{\isachardoublequoteopen}}ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ack{\isadigit{2}}\ {\isaliteral{28}{\isacharparenleft}}ack{\isadigit{2}}\ n\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ m{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
114 |
\begin{isamarkuptext}%
|
25263
|
115 |
The order of arguments has no influence on whether
|
25260
|
116 |
\isacommand{fun} can prove termination of a function. For more details
|
|
117 |
see elsewhere~\cite{bulwahnKN07}.
|
|
118 |
|
|
119 |
\subsection{Simplification}
|
|
120 |
\label{sec:fun-simplification}
|
|
121 |
|
25265
|
122 |
Upon a successful termination proof, the recursion equations become
|
25260
|
123 |
simplification rules, just as with \isacommand{primrec}.
|
|
124 |
In most cases this works fine, but there is a subtle
|
|
125 |
problem that must be mentioned: simplification may not
|
|
126 |
terminate because of automatic splitting of \isa{if}.
|
|
127 |
\index{*if expressions!splitting of}
|
|
128 |
Let us look at an example:%
|
|
129 |
\end{isamarkuptext}%
|
|
130 |
\isamarkuptrue%
|
|
131 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
132 |
\ gcd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
133 |
{\isaliteral{22}{\isachardoublequoteopen}}gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
134 |
\begin{isamarkuptext}%
|
|
135 |
\noindent
|
|
136 |
The second argument decreases with each recursive call.
|
|
137 |
The termination condition
|
|
138 |
\begin{isabelle}%
|
40406
|
139 |
\ \ \ \ \ n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ mod\ n\ {\isaliteral{3C}{\isacharless}}\ n%
|
25260
|
140 |
\end{isabelle}
|
|
141 |
is proved automatically because it is already present as a lemma in
|
|
142 |
HOL\@. Thus the recursion equation becomes a simplification
|
|
143 |
rule. Of course the equation is nonterminating if we are allowed to unfold
|
|
144 |
the recursive call inside the \isa{else} branch, which is why programming
|
|
145 |
languages and our simplifier don't do that. Unfortunately the simplifier does
|
|
146 |
something else that leads to the same problem: it splits
|
|
147 |
each \isa{if}-expression unless its
|
|
148 |
condition simplifies to \isa{True} or \isa{False}. For
|
|
149 |
example, simplification reduces
|
|
150 |
\begin{isabelle}%
|
40406
|
151 |
\ \ \ \ \ gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ k%
|
25260
|
152 |
\end{isabelle}
|
|
153 |
in one step to
|
|
154 |
\begin{isabelle}%
|
40406
|
155 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ k%
|
25260
|
156 |
\end{isabelle}
|
|
157 |
where the condition cannot be reduced further, and splitting leads to
|
|
158 |
\begin{isabelle}%
|
40406
|
159 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ k{\isaliteral{29}{\isacharparenright}}%
|
25260
|
160 |
\end{isabelle}
|
40406
|
161 |
Since the recursive call \isa{gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}} is no longer protected by
|
25260
|
162 |
an \isa{if}, it is unfolded again, which leads to an infinite chain of
|
|
163 |
simplification steps. Fortunately, this problem can be avoided in many
|
|
164 |
different ways.
|
|
165 |
|
|
166 |
The most radical solution is to disable the offending theorem
|
40406
|
167 |
\isa{split{\isaliteral{5F}{\isacharunderscore}}if},
|
25260
|
168 |
as shown in \S\ref{sec:AutoCaseSplits}. However, we do not recommend this
|
|
169 |
approach: you will often have to invoke the rule explicitly when
|
|
170 |
\isa{if} is involved.
|
|
171 |
|
|
172 |
If possible, the definition should be given by pattern matching on the left
|
|
173 |
rather than \isa{if} on the right. In the case of \isa{gcd} the
|
|
174 |
following alternative definition suggests itself:%
|
|
175 |
\end{isamarkuptext}%
|
|
176 |
\isamarkuptrue%
|
|
177 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
178 |
\ gcd{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
179 |
{\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{1}}\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
180 |
{\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{1}}\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ gcd{\isadigit{1}}\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
181 |
\begin{isamarkuptext}%
|
|
182 |
\noindent
|
|
183 |
The order of equations is important: it hides the side condition
|
40406
|
184 |
\isa{n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}}. Unfortunately, not all conditionals can be
|
25263
|
185 |
expressed by pattern matching.
|
25260
|
186 |
|
|
187 |
A simple alternative is to replace \isa{if} by \isa{case},
|
|
188 |
which is also available for \isa{bool} and is not split automatically:%
|
|
189 |
\end{isamarkuptext}%
|
|
190 |
\isamarkuptrue%
|
|
191 |
\isacommand{fun}\isamarkupfalse%
|
40406
|
192 |
\ gcd{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
|
|
193 |
{\isaliteral{22}{\isachardoublequoteopen}}gcd{\isadigit{2}}\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}case\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ of\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ m\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ gcd{\isadigit{2}}\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
194 |
\begin{isamarkuptext}%
|
|
195 |
\noindent
|
|
196 |
This is probably the neatest solution next to pattern matching, and it is
|
|
197 |
always available.
|
|
198 |
|
|
199 |
A final alternative is to replace the offending simplification rules by
|
|
200 |
derived conditional ones. For \isa{gcd} it means we have to prove
|
|
201 |
these lemmas:%
|
|
202 |
\end{isamarkuptext}%
|
|
203 |
\isamarkuptrue%
|
|
204 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
205 |
\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}gcd\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
25260
|
206 |
%
|
|
207 |
\isadelimproof
|
|
208 |
%
|
|
209 |
\endisadelimproof
|
|
210 |
%
|
|
211 |
\isatagproof
|
|
212 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
213 |
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline
|
25260
|
214 |
\isacommand{done}\isamarkupfalse%
|
|
215 |
%
|
|
216 |
\endisatagproof
|
|
217 |
{\isafoldproof}%
|
|
218 |
%
|
|
219 |
\isadelimproof
|
|
220 |
\isanewline
|
|
221 |
%
|
|
222 |
\endisadelimproof
|
|
223 |
\isanewline
|
|
224 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
225 |
\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}n\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ gcd\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ gcd\ n\ {\isaliteral{28}{\isacharparenleft}}m\ mod\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
25260
|
226 |
%
|
|
227 |
\isadelimproof
|
|
228 |
%
|
|
229 |
\endisadelimproof
|
|
230 |
%
|
|
231 |
\isatagproof
|
|
232 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
233 |
{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}\isanewline
|
25260
|
234 |
\isacommand{done}\isamarkupfalse%
|
|
235 |
%
|
|
236 |
\endisatagproof
|
|
237 |
{\isafoldproof}%
|
|
238 |
%
|
|
239 |
\isadelimproof
|
|
240 |
%
|
|
241 |
\endisadelimproof
|
|
242 |
%
|
|
243 |
\begin{isamarkuptext}%
|
|
244 |
\noindent
|
|
245 |
Simplification terminates for these proofs because the condition of the \isa{if} simplifies to \isa{True} or \isa{False}.
|
|
246 |
Now we can disable the original simplification rule:%
|
|
247 |
\end{isamarkuptext}%
|
|
248 |
\isamarkuptrue%
|
|
249 |
\isacommand{declare}\isamarkupfalse%
|
40406
|
250 |
\ gcd{\isaliteral{2E}{\isachardot}}simps\ {\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}%
|
25260
|
251 |
\begin{isamarkuptext}%
|
|
252 |
\index{induction!recursion|(}
|
|
253 |
\index{recursion induction|(}
|
|
254 |
|
|
255 |
\subsection{Induction}
|
|
256 |
\label{sec:fun-induction}
|
|
257 |
|
|
258 |
Having defined a function we might like to prove something about it.
|
|
259 |
Since the function is recursive, the natural proof principle is
|
|
260 |
again induction. But this time the structural form of induction that comes
|
|
261 |
with datatypes is unlikely to work well --- otherwise we could have defined the
|
|
262 |
function by \isacommand{primrec}. Therefore \isacommand{fun} automatically
|
40406
|
263 |
proves a suitable induction rule $f$\isa{{\isaliteral{2E}{\isachardot}}induct} that follows the
|
25260
|
264 |
recursion pattern of the particular function $f$. We call this
|
|
265 |
\textbf{recursion induction}. Roughly speaking, it
|
|
266 |
requires you to prove for each \isacommand{fun} equation that the property
|
|
267 |
you are trying to establish holds for the left-hand side provided it holds
|
|
268 |
for all recursive calls on the right-hand side. Here is a simple example
|
|
269 |
involving the predefined \isa{map} functional on lists:%
|
|
270 |
\end{isamarkuptext}%
|
|
271 |
\isamarkuptrue%
|
|
272 |
\isacommand{lemma}\isamarkupfalse%
|
40406
|
273 |
\ {\isaliteral{22}{\isachardoublequoteopen}}map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ x\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
25260
|
274 |
\isadelimproof
|
|
275 |
%
|
|
276 |
\endisadelimproof
|
|
277 |
%
|
|
278 |
\isatagproof
|
|
279 |
%
|
|
280 |
\begin{isamarkuptxt}%
|
|
281 |
\noindent
|
|
282 |
Note that \isa{map\ f\ xs}
|
|
283 |
is the result of applying \isa{f} to all elements of \isa{xs}. We prove
|
|
284 |
this lemma by recursion induction over \isa{sep}:%
|
|
285 |
\end{isamarkuptxt}%
|
|
286 |
\isamarkuptrue%
|
|
287 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
288 |
{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ x\ xs\ rule{\isaliteral{3A}{\isacharcolon}}\ sep{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}%
|
25260
|
289 |
\begin{isamarkuptxt}%
|
|
290 |
\noindent
|
|
291 |
The resulting proof state has three subgoals corresponding to the three
|
|
292 |
clauses for \isa{sep}:
|
|
293 |
\begin{isabelle}%
|
40406
|
294 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a{\isaliteral{2E}{\isachardot}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
295 |
\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ x{\isaliteral{2E}{\isachardot}}\ map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
296 |
\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ x\ y\ zs{\isaliteral{2E}{\isachardot}}\isanewline
|
|
297 |
\isaindent{\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\isanewline
|
|
298 |
\isaindent{\ {\isadigit{3}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }map\ f\ {\isaliteral{28}{\isacharparenleft}}sep\ a\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ sep\ {\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ y\ {\isaliteral{23}{\isacharhash}}\ zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
|
25260
|
299 |
\end{isabelle}
|
|
300 |
The rest is pure simplification:%
|
|
301 |
\end{isamarkuptxt}%
|
|
302 |
\isamarkuptrue%
|
|
303 |
\isacommand{apply}\isamarkupfalse%
|
40406
|
304 |
\ simp{\isaliteral{5F}{\isacharunderscore}}all\isanewline
|
25260
|
305 |
\isacommand{done}\isamarkupfalse%
|
|
306 |
%
|
|
307 |
\endisatagproof
|
|
308 |
{\isafoldproof}%
|
|
309 |
%
|
|
310 |
\isadelimproof
|
|
311 |
%
|
|
312 |
\endisadelimproof
|
|
313 |
%
|
|
314 |
\begin{isamarkuptext}%
|
25263
|
315 |
\noindent The proof goes smoothly because the induction rule
|
|
316 |
follows the recursion of \isa{sep}. Try proving the above lemma by
|
|
317 |
structural induction, and you find that you need an additional case
|
|
318 |
distinction.
|
25260
|
319 |
|
|
320 |
In general, the format of invoking recursion induction is
|
|
321 |
\begin{quote}
|
40406
|
322 |
\isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $x@1 \dots x@n$ \isa{rule{\isaliteral{3A}{\isacharcolon}}} $f$\isa{{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}}
|
25260
|
323 |
\end{quote}\index{*induct_tac (method)}%
|
|
324 |
where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
|
27167
|
325 |
name of a function that takes $n$ arguments. Usually the subgoal will
|
25263
|
326 |
contain the term $f x@1 \dots x@n$ but this need not be the case. The
|
40406
|
327 |
induction rules do not mention $f$ at all. Here is \isa{sep{\isaliteral{2E}{\isachardot}}induct}:
|
25260
|
328 |
\begin{isabelle}
|
|
329 |
{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
|
|
330 |
~~{\isasymAnd}a~x.~P~a~[x];\isanewline
|
|
331 |
~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
|
|
332 |
{\isasymLongrightarrow}~P~u~v%
|
|
333 |
\end{isabelle}
|
|
334 |
It merely says that in order to prove a property \isa{P} of \isa{u} and
|
|
335 |
\isa{v} you need to prove it for the three cases where \isa{v} is the
|
|
336 |
empty list, the singleton list, and the list with at least two elements.
|
|
337 |
The final case has an induction hypothesis: you may assume that \isa{P}
|
|
338 |
holds for the tail of that list.
|
|
339 |
\index{induction!recursion|)}
|
|
340 |
\index{recursion induction|)}%
|
|
341 |
\end{isamarkuptext}%
|
|
342 |
\isamarkuptrue%
|
|
343 |
%
|
|
344 |
\isadelimtheory
|
|
345 |
%
|
|
346 |
\endisadelimtheory
|
|
347 |
%
|
|
348 |
\isatagtheory
|
|
349 |
%
|
|
350 |
\endisatagtheory
|
|
351 |
{\isafoldtheory}%
|
|
352 |
%
|
|
353 |
\isadelimtheory
|
|
354 |
%
|
|
355 |
\endisadelimtheory
|
|
356 |
\end{isabellebody}%
|
|
357 |
%%% Local Variables:
|
|
358 |
%%% mode: latex
|
|
359 |
%%% TeX-master: "root"
|
|
360 |
%%% End:
|