3 \def\isabellecontext{Fundata}%
4 \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}%
7 Parameter \isa{{\isacharprime}a} is the type of values stored in
8 the \isa{Branch}es of the tree, whereas \isa{{\isacharprime}i} is the index
9 type over which the tree branches. If \isa{{\isacharprime}i} is instantiated to
10 \isa{bool}, the result is a binary tree; if it is instantiated to
11 \isa{nat}, we have an infinitely branching tree because each node
12 has as many subtrees as there are natural numbers. How can we possibly
13 write down such a tree? Using functional notation! For example, the term
15 \ \ \ \ \ Branch\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
17 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
18 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
19 has merely \isa{Tip}s as further subtrees.
21 Function \isa{map{\isacharunderscore}bt} applies a function to all labels in a \isa{bigtree}:%
23 \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
24 \isacommand{primrec}\isanewline
25 {\isachardoublequote}map{\isacharunderscore}bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ {\isacharequal}\ Tip{\isachardoublequote}\isanewline
26 {\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}%
27 \begin{isamarkuptext}%
28 \noindent This is a valid \isacommand{primrec} definition because the
29 recursive calls of \isa{map{\isacharunderscore}bt} involve only subtrees obtained from
30 \isa{F}, i.e.\ the left-hand side. Thus termination is assured. The
31 seasoned functional programmer might have written \isa{map{\isacharunderscore}bt\ f\ {\isasymcirc}\ F}
32 instead of \isa{{\isasymlambda}i{\isachardot}\ map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ i{\isacharparenright}}, but the former is not accepted by
33 Isabelle because the termination proof is not as obvious since
34 \isa{map{\isacharunderscore}bt} is only partially applied.
36 The following lemma has a canonical proof%
38 \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
39 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
41 \begin{isamarkuptext}%
44 %pr(latex xsymbols symbols)
45 but it is worth taking a look at the proof state after the induction step
46 to understand what the presence of the function type entails:
48 \ \isadigit{1}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
49 \ \isadigit{2}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\isanewline
50 \ \ \ \ \ \ \ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
51 \ \ \ \ \ \ \ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Branch\ a\ F{\isacharparenright}{\isacharparenright}
57 %%% TeX-master: "root"