9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9673
|
3 |
\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Branch\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}%
|
8749
|
4 |
\begin{isamarkuptext}%
|
|
5 |
\noindent Parameter \isa{'a} is the type of values stored in
|
|
6 |
the \isa{Branch}es of the tree, whereas \isa{'i} is the index
|
|
7 |
type over which the tree branches. If \isa{'i} is instantiated to
|
|
8 |
\isa{bool}, the result is a binary tree; if it is instantiated to
|
|
9 |
\isa{nat}, we have an infinitely branching tree because each node
|
|
10 |
has as many subtrees as there are natural numbers. How can we possibly
|
9541
|
11 |
write down such a tree? Using functional notation! For example, the term
|
|
12 |
\begin{quote}
|
|
13 |
|
|
14 |
\begin{isabelle}%
|
9673
|
15 |
Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}\mbox{i}{\isachardot}\ Branch\ \mbox{i}\ {\isacharparenleft}{\isasymlambda}\mbox{n}{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}
|
9541
|
16 |
\end{isabelle}%
|
|
17 |
|
|
18 |
\end{quote}
|
9673
|
19 |
of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
|
8771
|
20 |
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
|
8749
|
21 |
has merely \isa{Tip}s as further subtrees.
|
|
22 |
|
|
23 |
Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:%
|
|
24 |
\end{isamarkuptext}%
|
9673
|
25 |
\isacommand{consts}\ map{\isacharunderscore}bt\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isanewline
|
8749
|
26 |
\isacommand{primrec}\isanewline
|
9673
|
27 |
{\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
|
|
28 |
{\isachardoublequote}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}f\ a{\isacharparenright}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
|
8749
|
29 |
\begin{isamarkuptext}%
|
|
30 |
\noindent This is a valid \isacommand{primrec} definition because the
|
|
31 |
recursive calls of \isa{map_bt} involve only subtrees obtained from
|
|
32 |
\isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
|
9673
|
33 |
seasoned functional programmer might have written \isa{map{\isacharunderscore}bt\ \mbox{f}\ {\isasymcirc}\ \mbox{F}}
|
|
34 |
instead of \isa{{\isasymlambda}\mbox{i}{\isachardot}\ map{\isacharunderscore}bt\ \mbox{f}\ {\isacharparenleft}\mbox{F}\ \mbox{i}{\isacharparenright}}, but the former is not accepted by
|
8749
|
35 |
Isabelle because the termination proof is not as obvious since
|
|
36 |
\isa{map_bt} is only partially applied.
|
|
37 |
|
|
38 |
The following lemma has a canonical proof%
|
|
39 |
\end{isamarkuptext}%
|
9673
|
40 |
\isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
|
9698
|
41 |
\isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ {\isachardoublequote}T{\isachardoublequote}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
|
8749
|
42 |
\begin{isamarkuptext}%
|
|
43 |
\noindent
|
|
44 |
but it is worth taking a look at the proof state after the induction step
|
|
45 |
to understand what the presence of the function type entails:
|
|
46 |
\begin{isabellepar}%
|
|
47 |
~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
|
|
48 |
~2.~{\isasymAnd}a~F.\isanewline
|
|
49 |
~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
|
|
50 |
~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
|
|
51 |
\end{isabellepar}%%
|
|
52 |
\end{isamarkuptext}%
|
9722
|
53 |
\end{isabellebody}%
|
9145
|
54 |
%%% Local Variables:
|
|
55 |
%%% mode: latex
|
|
56 |
%%% TeX-master: "root"
|
|
57 |
%%% End:
|