7 the \isa{Branch}es of the tree, whereas \isa{'i} is the index |
7 the \isa{Branch}es of the tree, whereas \isa{'i} is the index |
8 type over which the tree branches. If \isa{'i} is instantiated to |
8 type over which the tree branches. If \isa{'i} is instantiated to |
9 \isa{bool}, the result is a binary tree; if it is instantiated to |
9 \isa{bool}, the result is a binary tree; if it is instantiated to |
10 \isa{nat}, we have an infinitely branching tree because each node |
10 \isa{nat}, we have an infinitely branching tree because each node |
11 has as many subtrees as there are natural numbers. How can we possibly |
11 has as many subtrees as there are natural numbers. How can we possibly |
12 write down such a tree? Using functional notation! For example, the *} |
12 write down such a tree? Using functional notation! For example, the term |
13 |
13 \begin{quote} |
14 term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))"; |
14 @{term[display]"Branch 0 (%i. Branch i (%n. Tip))"} |
15 |
15 \end{quote} |
16 text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose |
16 of type @{typ"(nat,nat)bigtree"} is the tree whose |
17 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
17 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
18 has merely \isa{Tip}s as further subtrees. |
18 has merely \isa{Tip}s as further subtrees. |
19 |
19 |
20 Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}: |
20 Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}: |
21 *} |
21 *} |
26 "map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))" |
26 "map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))" |
27 |
27 |
28 text{*\noindent This is a valid \isacommand{primrec} definition because the |
28 text{*\noindent This is a valid \isacommand{primrec} definition because the |
29 recursive calls of \isa{map_bt} involve only subtrees obtained from |
29 recursive calls of \isa{map_bt} involve only subtrees obtained from |
30 \isa{F}, i.e.\ the left-hand side. Thus termination is assured. The |
30 \isa{F}, i.e.\ the left-hand side. Thus termination is assured. The |
31 seasoned functional programmer might have written \isa{map_bt~f~o~F} instead |
31 seasoned functional programmer might have written @{term"map_bt f o F"} |
32 of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by |
32 instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by |
33 Isabelle because the termination proof is not as obvious since |
33 Isabelle because the termination proof is not as obvious since |
34 \isa{map_bt} is only partially applied. |
34 \isa{map_bt} is only partially applied. |
35 |
35 |
36 The following lemma has a canonical proof *} |
36 The following lemma has a canonical proof *} |
37 |
37 |